Agdaでラムダ計算

# Agdaでラムダ計算をやってみる
AgdaはCoqやIdrisのような定理証明支援系の一つです．Haskellのような構文で依存型を持ち，論理学における$\forall,\exists$などが扱えるようになる．カーリー・ハワード対応により命題を型，証明をプログラムと見る事ができるため，これらが扱えるのは非常に有用である．

本記事は以下のtutolialのPart2 Programming Language Foundations をもとに進めていきます．
https://plfa.github.io

:::note 
定理証明支援系について全くの素人がoutputを兼ねて書いている記事です．
ぜひ元のtutolialを読んでいただき，つまみ食い程度に見ていただければと思います．
また，ご指摘も大歓迎ですのでぜひお願いします！
:::

## Introduction to Lambda Calculus

### 構文の項

``` :構文(BNF)
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で書くとこんな感じになります．

```Agda:Term
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_Plus_Example
two : Term
two = `suc `suc `zero

plus : Term
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
         case ` "m"
           [zero⇒ ` "n"
           |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
```

高階関数を用いた実装は以下の通りである．
```:Higher_Order_Example
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"を用いていました．以下の定義を追加すると，λ項の例を書きやすくなります．
```:Easy_Example
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を定義します．
```:Value
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で置き換えた項である．
以下が代入の定義である．
```:Substitution
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を簡約する．

```:Reduction
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は変数と型を関連づけます．以下のように表します．
```:Context
infixl 5  _,_⦂_

data Context : Set where
  ∅     : Context
  _,_⦂_ : Context → Id → Type → Context
```
変数の型がどの型に対応しているのかを検査する機構を導入します．
以下のように表します．
```:Lookup_Judgement
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
```

### 型チェック
```:Type_Judgement
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のチュートリアルをやってみました．このチュートリアルをする前に，ラムダ計算に関する文献を当たってみる必要があると思いますが，ラムダ計算の実装としては非常に優れているチュートリアルだと思います．
以下に練習問題なども行なったリポジトリを置いておきます．ぜひご指摘お願いします．

https://github.com/zaki5m/basic_lambda