Agdaでラムダ計算をやってみる
AgdaはCoqやIdrisのような定理証明支援系の一つです．Haskellのような構文で依存型を持ち，論理学における$\forall,\exists$などが扱えるようになる．カーリー・ハワード対応により命題を型，証明をプログラムと見る事ができるため，これらが扱えるのは非常に有用である．
本記事は以下のtutolialのPart2 Programming Language Foundations をもとに進めていきます．
https://plfa.github.io
定理証明支援系について全くの素人がoutputを兼ねて書いている記事です．
ぜひ元のtutolialを読んでいただき，つまみ食い程度に見ていただければと思います．
また，ご指摘も大歓迎ですのでぜひお願いします！
Introduction to Lambda Calculus
構文の項
L, M, N ::=
` x | ƛ x ⇒ N | L · M |
`zero | `suc M | case L [zero⇒ M |suc x ⇒ N ] |
μ x ⇒ M
7種類の項を定義します．
ラムダ計算の3種類の項
- 変数 ` x
- ラムダ抽象 ƛ x ⇒ N
- 関数適用 L · M
自然数のための項
- 定数ゼロ `zero
- 後者関数 `suc M
- 条件分岐 case L [zero⇒ M |suc x ⇒ N ]
再帰のための項
- 不動点 μ x ⇒ M
Agdaで書くとこんな感じになります．
Id : Set
Id = String
infix 5 ƛ_⇒_
infix 5 μ_⇒_
infixl 7 _·_
infix 8 `suc_
infix 9 `_
data Term : Set where
`_ : Id → Term
ƛ_⇒_ : Id → Term → Term
_·_ : Term → Term → Term
`zero : Term
`suc_ : Term → Term
case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term
μ_⇒_ : Id → Term → Term
infix 数字 は，優先順位を表しており，infixlは左結合，infixrは右結合となっている．
例
上で定義した構文を用いて，以下のように2はtwo，+はplusとして定義できる．
plusが加算の再帰的な定義なっている事がわかります．
two : Term
two = `suc `suc `zero
plus : Term
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
case ` "m"
[zero⇒ ` "n"
|suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
高階関数を用いた実装は以下の通りである．
twoᶜ : Term
twoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")
plusᶜ : Term
plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
` "m" · ` "s" · (` "n" · ` "s" · ` "z")
sucᶜ : Term
sucᶜ = ƛ "n" ⇒ `suc (` "n")
ここまでは，変数を定義する際にxではなく，` "x"を用いていました．以下の定義を追加すると，λ項の例を書きやすくなります．
var? : (t : Term) → Bool
var? (` _) = true
var? _ = false
ƛ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
ƛ′_⇒_ (` x) N = ƛ x ⇒ N
case′_[zero⇒_|suc_⇒_] : Term → Term → (t : Term) → {_ : T (var? t)} → Term → Term
case′ L [zero⇒ M |suc (` x) ⇒ N ] = case L [zero⇒ M |suc x ⇒ N ]
μ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
μ′ (` x) ⇒ N = μ x ⇒ N
値(Value)
計算結果に対応する項のことを値(Value)と言います．
ラムダ抽象は値とし，その他zeroとsucを定義します．
data Value : Term → Set where
V-ƛ : ∀ {x N}
---------------
→ Value (ƛ x ⇒ N)
V-zero :
-----------
Value `zero
V-suc : ∀ {V}
→ Value V
--------------
→ Value (`suc V)
束縛変数と自由変数
Agdaには直接関係ないので省略．
わからない場合は，別の文献を参照してください．
代入(substitution)
項に現れる自由変数をある項で置き換える処理である．
例えば，N [ x := V ]は項Nに現れる変数xをVで置き換えた項である．
以下が代入の定義である．
infix 9 _[_:=_]
_[_:=_] : Term → Id → Term → Term
(` x) [ y := V ] with x ≟ y
... | yes _ = V
... | no _ = ` x
(ƛ x ⇒ N) [ y := V ] with x ≟ y
... | yes _ = ƛ x ⇒ N
... | no _ = ƛ x ⇒ N [ y := V ]
(L · M) [ y := V ] = L [ y := V ] · M [ y := V ]
(`zero) [ y := V ] = `zero
(`suc M) [ y := V ] = `suc M [ y := V ]
(case L [zero⇒ M |suc x ⇒ N ]) [ y := V ] with x ≟ y
... | yes _ = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N ]
... | no _ = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N [ y := V ] ]
(μ x ⇒ N) [ y := V ] with x ≟ y
... | yes _ = μ x ⇒ N
... | no _ = μ x ⇒ N [ y := V ]
_≟_は左右の文字列が一致しているかどうかを判定するものである．
簡約(reduction)
call-by-valueの簡約規則をここでは与える．
項が値である場合は，簡約は適用されず，簡約が項に適用される場合は値ではない．
また，数値はzeroは簡約されず，sucはsubtermを簡約する．
infix 4 _—→_
data _—→_ : Term → Term → Set where
ξ-·₁ : ∀ {L L′ M}
→ L —→ L′
-----------------
→ L · M —→ L′ · M
ξ-·₂ : ∀ {V M M′}
→ Value V
→ M —→ M′
-----------------
→ V · M —→ V · M′
β-ƛ : ∀ {x N V}
→ Value V
------------------------------
→ (ƛ x ⇒ N) · V —→ N [ x := V ]
ξ-suc : ∀ {M M′}
→ M —→ M′
------------------
→ `suc M —→ `suc M′
ξ-case : ∀ {x L L′ M N}
→ L —→ L′
-----------------------------------------------------------------
→ case L [zero⇒ M |suc x ⇒ N ] —→ case L′ [zero⇒ M |suc x ⇒ N ]
β-zero : ∀ {x M N}
----------------------------------------
→ case `zero [zero⇒ M |suc x ⇒ N ] —→ M
β-suc : ∀ {x V M N}
→ Value V
---------------------------------------------------
→ case `suc V [zero⇒ M |suc x ⇒ N ] —→ N [ x := V ]
β-μ : ∀ {x M}
------------------------------
→ μ x ⇒ M —→ M [ x := μ x ⇒ M ]
型付け(typing)
簡約は閉じた項のみを考慮するが，型付けでは自由変数を持つ項も考慮する必要があります．
contextは変数と型を関連づけます．以下のように表します．
infixl 5 _,_⦂_
data Context : Set where
∅ : Context
_,_⦂_ : Context → Id → Type → Context
変数の型がどの型に対応しているのかを検査する機構を導入します．
以下のように表します．
infix 4 _∋_⦂_
data _∋_⦂_ : Context → Id → Type → Set where
Z : ∀ {Γ x A}
------------------
→ Γ , x ⦂ A ∋ x ⦂ A
S : ∀ {Γ x y A B}
→ x ≢ y
→ Γ ∋ x ⦂ A
------------------
→ Γ , y ⦂ B ∋ x ⦂ A
S′ : ∀ {Γ x y A B}
→ {x≢y : False (x ≟ y)}
→ Γ ∋ x ⦂ A
------------------
→ Γ , y ⦂ B ∋ x ⦂ A
型チェック
infix 4 _⊢_⦂_
data _⊢_⦂_ : Context → Term → Type → Set where
-- Axiom
⊢` : ∀ {Γ x A}
→ Γ ∋ x ⦂ A
-----------
→ Γ ⊢ ` x ⦂ A
-- ⇒-I
⊢ƛ : ∀ {Γ x N A B}
→ Γ , x ⦂ A ⊢ N ⦂ B
-------------------
→ Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B
-- ⇒-E
_·_ : ∀ {Γ L M A B}
→ Γ ⊢ L ⦂ A ⇒ B
→ Γ ⊢ M ⦂ A
-------------
→ Γ ⊢ L · M ⦂ B
-- ℕ-I₁
⊢zero : ∀ {Γ}
--------------
→ Γ ⊢ `zero ⦂ `ℕ
-- ℕ-I₂
⊢suc : ∀ {Γ M}
→ Γ ⊢ M ⦂ `ℕ
---------------
→ Γ ⊢ `suc M ⦂ `ℕ
-- ℕ-E
⊢case : ∀ {Γ L M x N A}
→ Γ ⊢ L ⦂ `ℕ
→ Γ ⊢ M ⦂ A
→ Γ , x ⦂ `ℕ ⊢ N ⦂ A
-------------------------------------
→ Γ ⊢ case L [zero⇒ M |suc x ⇒ N ] ⦂ A
⊢μ : ∀ {Γ x M A}
→ Γ , x ⦂ A ⊢ M ⦂ A
-----------------
→ Γ ⊢ μ x ⇒ M ⦂ A
おわりに
Agdaのチュートリアルをやってみました．このチュートリアルをする前に，ラムダ計算に関する文献を当たってみる必要があると思いますが，ラムダ計算の実装としては非常に優れているチュートリアルだと思います．
以下に練習問題なども行なったリポジトリを置いておきます．ぜひご指摘お願いします．