PowerShellで型無しラムダ計算（α-変換、β-簡約）

ラムダ計算をPowerShellで実装した。ただ、何を実装したか忘れそうなので、機能をメモしておく。

# コード

コードは下記の通り格納してある。テストコードは[Church encoding - Wikipedia](https://en.wikipedia.org/wiki/Church_encoding)を実行してみただけなので、異常系のテストはしていない。

* [実装](https://gist.github.com/yumura/d22146f63fea915391e090205810ccdf)


# デモ

下記は、チャーチエンコーディングした `3 - 2` が `1` （`λ f x . f x`）になるまで、PowerShellで１ステップずつβ簡約していった様子。

![Animation.gif](https://qiita-image-store.s3.amazonaws.com/0/36744/07b0aaeb-cc8a-7121-1256-10b7bde65203.gif)

テキストで貼り付けるとそれなりに長い。

```
PS C:\demo\lambda> ls .\lambda.psm1


    ディレクトリ: C:\demo\lambda


Mode                LastWriteTime         Length Name
----                -------------         ------ ----
-a----       2017/01/05     22:03          18272 lambda.psm1


PS C:\demo\lambda> ipmo .\lambda.psm1 -Force
PS C:\demo\lambda> $cPred  = \ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)
PS C:\demo\lambda> $cMinus = \ m n . n $cPred m
PS C:\demo\lambda> $cMinus |\str
\ m n . n (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) m
PS C:\demo\lambda> $c2 = \ f x . f (\ f x)
PS C:\demo\lambda> $c3 = \ f x . f (\ f (\ f x))
PS C:\demo\lambda> \ $cMinus $c3 $c2 |\bnf -Step |\str |%{"-" * 100; $_}
----------------------------------------------------------------------------------------------------
\ (\ m n . n (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) m) (\ f x . f (\ f (\ f x))) (\ f x . f (\ f x))
----------------------------------------------------------------------------------------------------
\ (\ n . n (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) (\ f x . f (\ f (\ f x)))) (\ f x . f (\ f x))
----------------------------------------------------------------------------------------------------
\ (\ f x . f (\ f x)) (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) (\ f x . f (\ f (\ f x)))
----------------------------------------------------------------------------------------------------
\ (\ x . (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) (\ (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) x)) (\ f x . f (\ f (\ f x)))
----------------------------------------------------------------------------------------------------
\ (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) (\ (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) (\ f x . f (\ f (\ f x))))
----------------------------------------------------------------------------------------------------
\ f x . (\ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)) (\ f x . f (\ f (\ f x))) (\ g h . h (\ g f)) (\ u . x) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ f x . (\ f x . f (\ f (\ f x))) (\ g h . h (\ g f)) (\ u . x) (\ u . u)) (\ g h . h (\ g f)) (\ u . x) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ x . (\ f x . f (\ f (\ f x))) (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u . x) (\ u . u)) (\ u . x) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ f x . f (\ f (\ f x))) (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x) (\ u . u) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ x . (\ g h . h (\ g (\ g h . h (\ g f)))) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) x))) (\ u u . x) (\ u . u) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ g h . h (\ g (\ g h . h (\ g f)))) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x))) (\ u . u) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ h . h (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x)) (\ g h . h (\ g f)))) (\ u . u) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ u . u) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x)) (\ g h . h (\ g f))) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ g h . h (\ g (\ g h . h (\ g f)))) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x)) (\ g h . h (\ g f)) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ h . h (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x) (\ g h . h (\ g f)))) (\ g h . h (\ g f)) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ g h . h (\ g f)) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x) (\ g h . h (\ g f))) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ h . h (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x) (\ g h . h (\ g f)) f)) (\ u . u)
----------------------------------------------------------------------------------------------------
\ f x . (\ u . u) (\ (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x) (\ g h . h (\ g f)) f)
----------------------------------------------------------------------------------------------------
\ f x . (\ g h . h (\ g (\ g h . h (\ g f)))) (\ u u . x) (\ g h . h (\ g f)) f
----------------------------------------------------------------------------------------------------
\ f x . (\ h . h (\ (\ u u . x) (\ g h . h (\ g f)))) (\ g h . h (\ g f)) f
----------------------------------------------------------------------------------------------------
\ f x . (\ g h . h (\ g f)) (\ (\ u u . x) (\ g h . h (\ g f))) f
----------------------------------------------------------------------------------------------------
\ f x . (\ h . h (\ (\ u u . x) (\ g h . h (\ g f)) f)) f
----------------------------------------------------------------------------------------------------
\ f x . f (\ (\ u u . x) (\ g h . h (\ g f)) f)
----------------------------------------------------------------------------------------------------
\ f x . f (\ (\ u . x) f)
----------------------------------------------------------------------------------------------------
\ f x . f x
```

# 各機能

最初に書いたが、以降は機能のメモしか書かない。ラムダ式について知りたい人やラムダ計算を実装したい人は、別の資料をググってください。

* [ラムダ計算 filetype:pdf - Google 検索](https://www.google.co.jp/search?q=%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97+filetype:pdf)



## 1.ラムダ式の構築

上のデモで言うと、チャーチエンコーディングした前者関数 $\text{pred} ≡ λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)$ を、今回の実装では次のように書ける。

```.ps1
$cPred  = \ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)
```

ラムダ式の表記と、今回の実装での表記は、下表の通り、対応する。ただし下表で $x$は任意の変数、$M$、$N$ は任意のラムダ式を表す。

| ラムダ式の構成要素 | ラムダ式の表記 | 今回の実装での表記 |
|:----:|:--------:|:-----------:|
| 変数 | $x$      | (\ x)       |
| 適用 | $(M N)$  | (\ \$M \$N) |
| 抽象 | $(λx.M)$ | (\ x . \$M) |

| 略記法 | ラムダ式の表記 | 今回の実装での表記 |
|:----:|:------:|:-----------:|
| 適用 | $((...((M_1 M_2) M_3)...)M_n)$  | (\ \$M1 \$M2 \$M3 ... \$Mn) |
| 抽象 | $(λx_1.(λx_2.(...(λx_n.(M)...)))$ | (\ x1 x2 ... xn . \$M) |


## 2.ラムダ式の文字列化

構築したラムダ式を文字列化する場合は　\str　を使用する。なお、次の例の通り略記法を使った表記で文字列化される。

```
PS C:\demo\lambda> \ n . (\ f . (\ x . (\ f (\ (\ n f) x)))) |\str
\ n f x . f (\ n f x)
```

また、文字列化されたものを eval すると元のラムダ式が再構築される。

```
PS C:\demo\lambda> \ n . (\ f . (\ x . (\ f (\ (\ n f) x)))) |\str |iex |\str
\ n f x . f (\ n f x)
```


## 3.変数の取得

変数を取得する場合は \var を使用する。

ラムダ式 $λx.λy.x y (y z)$ に含まれている変数、束縛変数、自由変数は次のようにして取得できる。

```
PS C:\demo\lambda> \ x y . x y (\ y z) |\var
x
y
z
PS C:\demo\lambda> \ x y . x y (\ y z) |\var -Bind
x
y
PS C:\demo\lambda> \ x y . x y (\ y z) |\var -Free
z
```

## 4.α-変換

α-変換する場合は \alpha を使用する。左から数えて何番目のラムダ抽象の変数を変換するか、指定する必要がある（0 始まり）。

```
PS C:\demo\lambda> \ (\ x . x x) (\ x . x x) |\alpha 0 y |\str
\ (\ y . y y) (\ x . x x)
PS C:\demo\lambda> \ (\ x . x x) (\ x . x x) |\alpha 1 y |\str
\ (\ x . x x) (\ y . y y)
PS C:\demo\lambda> \ (\ x . x x) (\ x . x x) |\alpha 0 a |\alpha 1 b |\str
\ (\ a . a a) (\ b . b b)
```

## 5. 置換

ラムダ式の自由変数を置換する場合は \sub を使用する。

```
PS C:\demo\lambda> \ x y . z y x |\sub z (\ a b) |\str
\ x y . a b y x
```

ただし、変数条件が満たされない場合は、自動的にα-変換される。

```
PS C:\demo\lambda> \ x y . z y x |\sub z (\ x y) |\str
\ _0 _1 . x y _1 _0
```

## 6. β-簡約

β-簡約する場合は \beta を使用する。左から数えて何番目のβ-基を簡約するか指定する必要がある（0 始まり）。


```
PS C:\demo\lambda> (\ (\ x . x) (\ (\ y . y y) z)) |\beta 0 |\str
\ (\ y . y y) z
PS C:\demo\lambda> (\ (\ x . x) (\ (\ y . y y) z)) |\beta 1 |\str
\ (\ x . x) (\ z z)
```

ただし、変数条件が満たされない場合は、自動的にα-変換される。

```
PS C:\demo\lambda> \ (\ x y . x y) (\ z . z y) |\beta 0 |\str
\ _0 . (\ z . z y) _0
```

## 7. β-正規形への簡約

β-正規形へ簡約する場合は、 \bnf を使用する。Stepスイッチを使用すると、β-基が１つづつ簡約される。

```
PS C:\demo\lambda> (\ (\ x . x) (\ (\ y . y y) x)) |\bnf |\str
\ x x
PS C:\demo\lambda> (\ (\ x . x) (\ (\ y . y y) x)) |\bnf -Step |\str
\ (\ x . x) (\ (\ y . y y) x)
\ (\ y . y y) x
\ x x
```

## 以上

おわり。