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

コード

コードは下記の通り格納してある。テストコードはChurch encoding - Wikipediaを実行してみただけなので、異常系のテストはしていない。

実装

デモ

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

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

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 検索

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

以上

おわり。