Go to Qiita Advent Calendar 2024 Top
LoginSignup
1
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

@yumura_s

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

Last updated at Posted at 2017-01-14

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

コード

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

デモ

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

Animation.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

各機能

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

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

以上

おわり。

1
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
1
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?