tnomuraのブログ

有限集合のみで構成される世界

有限集合のみで構成される世界を考えてみた。まず、有限集合を有限個集めてみる。次にそれらの集合とその要素ををすべて集めて領域 R を作る。すると、領域 R はそのような集合の系の全ての要素と集合を含むことができる。そのような世界では、全ての集合について集合和、共通部分、補集合などの全ての演算が閉じている。

しかし、それらの集合の演算を定義するためには、要素と集合の所属関係が定義されていなければならない。それは、領域 R の要素の直積を作り、所属関係があれば 1 なければ 0 となるような対照表を作ればいい。そのような対照表には領域全ての要素について互いの所属関係が記述される。

ところが、この対照表は領域の直積であるので、それは領域には含まれない。つまり、有限集合を有限個集めた領域にあっても、集合の所属関係のような基本的な関係でさえ、領域内で完結することができない。それらは集合の世界の外の論理になるのだ。

また、この対照表自体にも問題がある。この対照表は n 個までの集合しか表現できないが、領域に n 個の要素がある場合、それらの要素を含む可能な集合は 2^ n 個になるからだ。この意味でも領域 R の要素では全ての集合を表せないことが分かる。

おそらく、集合の数や要素の数を無限に増やしてもこれらの事情は変わらないのではないだろうか。

ラッセルのパラドックスのようなものも、本来は集合の領域内で完結できないはずの論理を、その集合の領域内で完結させようとしたところに問題が発生したのではないだろうか。

そこで、どのような集合の系であれば、論理と整合性を保てるのだろうかと考えてみた。最も単純なモデルは、領域 R を先に決めておいて、集合とはその部分集合だけを指すことにする場合だ。一言で言うとベン図の世界だ。このモデルでは集合を表すのに領域の要素は用いない。集合の名前空間は領域とは別のところに作る。そうすると、領域の要素数による集合の名前空間の制限がないので、領域で考えられる可能な集合を列挙することができる。

そこで、領域 R で考えられる全ての集合を指す名前空間を Set とする。Set と 領域 R の直積から真理値への関数を elem :: Set -> R -> Bool とすると、これは領域 R の部分集合と領域 R の要素の間の全ての帰属関係を記述できる。また、Set を行に、R の要素を列に並べて elem の値を表にした対照表を作ると、これは n × (2^n) の表になる。この対照表は領域 R の部分集合を全て記述することができる。このとき、Set に集合和、共通部分、補集合などの集合演算を定義することができ、それは Set について閉じている。

また述語 P(x) を

P(x) = elem (S, x)

で定義できて、P(x) は領域 R の全ての要素について True または False の値をとる。このような定義ではなく任意の述語 Q(x) を考えこれは R の要素 x について True または False の値を取るものと考えると、これは P(x) = elem (S, x) のどれかと一致する。すなわち、任意の述語 Q(x) は elem (S,x) のどれかと同値である。このモデルについては、素朴集合論の演算と、一階述語論理について閉じている。これが、論理と整合性のある素朴集合のモデルだ。このモデルには自分自身を要素とする集合は存在しない。名前空間が異なるので、帰属関係が定義できないからだ。

集合には冪集合が存在する。それは Set の要素の集合である。したがって、集合 S の冪集合の名前空間は Set とは異なる名前空間になる。また、集合の直積 A × B もまた、Set とは異なる名前空間に属する。このように、集合の集合のような Set の要素から作られる集合は Set とは異なる名前空間を与えると、ラッセルのパラドックスのような矛盾は一切生じない。

このような型付きラムダ計算ではどのように集合が複雑に構成されていっても論理との矛盾が生じないのではないだろうか。型付きラムダ計算は煩雑に見えるが、Haskell でプログラムが自在に記述できるのを見ると。取扱はそうむずかしいものでもないような気がする。

型なしラムダ計算とラッセルのパラドックス

型なしラムダ計算の学習をしていたら、これが、ラッセルのパラドックスをすっきり説明できるのではないかと思いついたので書いてみる。

初めに、集合を全て集めたクラスを考える。そのクラスについて述語 P(x) と集合 P を次のように定義する。

x ∈ P ⇔ P(x) = True

P(x) は集合 x を引数とし、真か偽の真理値をとる関数である。これは集合の内包的定義を用いると次のように表せる。

P = {x | P(x) = true }

これは P(x) が真となるような集合 x を集めると集合 P になることを示している。

そこで、上の定義を利用してラッセルのパラドックスにあるような x ∈ x のような自己言及を定義できないかどうか考えてみるが、これは上の定義から次のようになる。

x ∈ x ⇔ x(x) = True

この定義には、しかし問題がある。x(x) の右側の x は述語でなければならないのに対し、左側の x は集合であるからだ。集合 x を集合の関数である述語として使うのは問題があるので、本来 x(x) のような自己言及は上のような集合の内包的定義では定義できない。

そこで少し工夫をして集合を表すのに述語を使うことを考えてみる。つまり集合 P の述語 P(x) で集合を表すことを考える。P(x) は集合ではないが P = {x | P(x)} のようにいつでも内包的定義で集合にすることができる。そして集合 P の集合 a への関数適用を次のように定義する。

P a(x) = P(a(x))

こうすれば述語 P の引数は述語であり、述語 a(x) を引数とすることができる。そうして P (a(x)) は述語になる。このようにすれば、集合の世界と、集合の述語からなる世界の対応が作られるので、集合の述語の世界で x(x) のような自己言及を作ることができる。述語 P(x) を集合 P と同一視し、述語 a(x) を A として集合 A と同一視することにすると、上の関数適用は、

P A = (P . a) (x)

となる。これで、めでたく集合 P を 集合 A に関数適用できることになる。もちろん自己言及 X X も可能である。全てが関数である述語の世界を考えると自己言及は可能になる。

そこで、関数適用 P A に対し関数抽象 λ を導入すると、次の λA.(P A) は集合 A を引数とし集合 P A を返す関数となる。

λA.(P A)

したがって、

(λA.(P A)) B = (P B)

である。さらに、

λPA.(P A)

は集合 P を引数とし、集合 A を引数とする関数 λA.(P A) を返す高階関数である。これは集合と集合の関数適用を考えたときに、集合が型のないラムダ計算のなかに埋め込まれることを意味している。集合の述語は型のないラムダ計算の要素と考えることができるのだ。このように集合の述語による言及が型なしラムダ計算の世界で表現できることが分かったので、集合の自己言及を型なしラムダ計算の枠組みで考えてみる。

さて、集合 A を集合 A に自己言及させた次のラムダ項は何になるのだろうか。

A A

これは A が A に属していれば true で属していなければ false である。ただし、この true や false はラムダ計算の世界で定義されたものになる。

したがって、上の自己言及を λ 抽象した次のラムダ項は任意の集合についてそれが自分自身を要素としていれば true 要素としていなければ false を返す述語になる。

λx.(x x)

また、集合をラムダ計算に埋め込むことで、上の述語は集合と同一視することができる。したがって、次のラムダ項は自分自身を要素として含む集合が自分自身を集合として含むかどうかを判別する関数適用になる。

(λx.xx) (λx.xx)

しかし、これは次のように β 簡約しても無限に自分自身となるのでどうやっても true にも false にもたどり着くことができない。

(λx.xx) (λx.xx) = (λx.xx) (λx.xx) = (λx.xx) (λx.xx) = ...

それではラッセルの集合はどうだろうか。これは自分自身を要素としては含まない集合の集合だから次のようになる。

￢(λx.xx)

これが自分自身を要素として含むかどうかの関数適用は次のようになる。

(￢(λx.xx))(￢(λx.xx)) = ￢(￢(λx.xx))(￢(λx.xx)) = ￢(￢(￢(λx.xx))(￢(λx.xx)))) = ...

と、これもやはり true にも false にもたどり着けない。

自分自身を要素として含む集合や、自分自身を要素として含まない集合は本来は内包的定義にそぐわない表現だが、自然言語で表現すると見逃がしやすい。ふつうに考える集合の世界には、これらの述語は発生しないはずだ。ただし、これはラムダ計算の体系の中では表現できる。しかし、この場合もまた不動点コンビネータを形成してしまうので真理値を得ることはできない。

ラッセルのパラドックスは結局のところ内包的定義としては表現できない定義を導入したためにおこったものではないだろうか。自己言及を含む述語は集合の定義には使えないのだ。

自己言及を含む内包的定義は、型不適合で排除できる。素朴集合論を型つきラムダ計算の枠組みで記述出来たら、ラッセルのパラドックスは発生しないので矛盾が起きなくなるのではないだろうかと思うが、それを検証する知識がない。

GitHub にアカウントを作った

GitHub にアカウントを作りました。ラムダ計算機がダウンロードできます。その他の使い方は勉強中。というかよく分かりません。

https://github.com/tnomura9/lambda-calculus

Git とは何か

GIT についての TeckAcademy の Youtube の動画が分かりやすかった。

はじめての GIT 入門講座

ラムダ計算 SKI コンビネータ 4

ラムダ計算

Y - コンビネータを SKI に変換してみた。Y - コンビネータの定義は次のようになる。

Y = λf.(λx.fxx)(λx.fxx)

手順は次のようになる。まず、lambda.hs を起動して、:load コマンドで設定ファイルを読み込み SKI コンビネータを使えるようにする。

C:\Users\****>runghc lambda.hs
lambda> :load
filename: defined.txt
lambda>

Y - コンビネータの body 部分は λx.fxx の自己言及になっているのでまず fxx を SKI コンビネータに変換したあと Yf = S(fxx)(fxx)f を作った。最後に (Yg) 3 で3の階乗を計算した。g は設定ファイルに記述した階乗のプログラム。

lambda> (f (x x))　......　fxx を取り出す。
(f (x x))
lambda> (((K f) x) (((S I) I) x))　......　f -> (K f) x, xx -> SIIx へ変形
(f (x x))
lambda> (((S (K f)) ((S I) I)) x)　......　S(Kf)(SII)x で x をくくりだす
(f (x x))
lambda> (((((K S) f) (K f)) ((S I) I)) x)　......　SKY -> (KSf)(Kf) に変形
(f (x x))
lambda> (((((S (K S)) K) f) ((S I) I)) x)　......　S(KS)Kf で f をくくりだす
(f (x x))
lambda> (((((S (K S)) K) f) ((K ((S I) I)) f)) x)　......　(S(KS)Kf)(K(SII)f) に変形
(f (x x))
lambda> ((((S ((S (K S)) K)) (K ((S I) I))) f) x)　......　S(S(KS)K)(K(SII)f で f をくくりだす
(f (x x))
lambda> (= M ((S ((S (K S)) K)) (K ((S I) I))))　.......　M = S(S(KS)K)(K(SII))
lambda> (= Ys ((S M) M)))　......　Ys = SMM
lambda> ((Ys g) 3)　......　(Ys g) 3 で factorial 3 を計算
(ls.(lz.(s (s (s (s (s (s z))))))))　......　factorial 3 = 6

SKI - コンビネータでも自己言及関数のテストができた。

ラムダ計算 SKI コンビネータ 3

ラムダ計算

ラムダ記法の関数を SKI コンビネータで表すのは機械的にできる。次の３つのルールを機械的に適用していくだけだ。

１）λx.M = M ... λ抽象は外して良い

２）((x z) (y z)) = (S x y) z ..... (x z) (y z) の形の関数適用は変数 z をくくり出せる。

３）x = I x ..... 変数 x だけの項は (I x) の形に変えることができる。

４）a = (K a) x ..... 項 a は (Ka) x の形に変えることできる。このとき、(K a) を関数適用する x は任意の項を使うことができる。

このルールに従って、前回も紹介した、

λxyz.x(yz)

を SKI コンビネータで置き換えてみると、次のようになる。

lambda> (lx.(ly.(lz.(x (y z)))))
(lx.(ly.(lz.(x (y z)))))
lambda> (x (y z)) ...... ルール１）を使ってラムダ抽象を除去して body だけにする。
(x (y z))
lambda> (((K x) z) (y z)) ..... ルール４）を使って x --> (K x) z にする。
(x (y z))
lambda> (((S (K x)) y) z) ..... ルール２）を使って z をくくりだす。
(x (y z))
lambda> (((((K S) x) (K x)) y) z) .... ルール４）を使って S -> (K S) x にする。
(x (y z))
lambda> (((((S (K S)) K) x) y) z) ..... ルール２）を使って x をくくりだす。
(x (y z))
lambda> (= M ((S (K S)) K)) .... 求めるコンビネータは S(KS)K である。
lambda> (((M x) y) z)
(x (y z))

ラムダ記法の関数は、atom か、関数抽象か、関数適用のどれかで記述されているので上のルールを適用していけば、どのようなラムダ項も SKI コンビネータで記述することができる（はずだ）。

しかし、上のルールは変数が１回しか現れないときは機械的に適用できるが、(x (x x)) の様に同じ変数が何回も現れる場合は適用できるのだろうか。

lambda> (x (x x))
(x (x x))
lambda> (x ((I x) (I x)))
(x (x x))
lambda> (x (((S I) I) x))
(x (x x))
lambda> ((I x) (((S I) I) x))
(x (x x))
lambda> (((S I) ((S I) I)) x)
(x (x x))
lambda> ((S I) ((S I) I))
(lz.(z (z z)))

問題ないようだ。

ラムダ計算機 設定ファイル

ラムダ計算

ラムダ計算機に関数の定義を読み込ませる設定ファイル defined.txtもだいぶ充実してきたので別記事として紹介することにした。ラムダ計算機に設定ファイルを読み込ませるためには次のように :load コマンドを用いる。ラムダ計算機 lambda.hs は runghc で起動することもできるし、ghc lambda.hs でコンパイルすれば lambda コマンドで実行できる。

$ runghc lambda.hs
lambda> :load
filename: defined.txt
lambda> ((Y g) 3)
(ls.(lz.(s (s (s (s (s (s z))))))))

設定ファイル： defined.txt

$ cat defined.txt
(= true (lx.(ly.x)))
(= false (lx.(ly.y)))
(= NOT (lx.((x false) true))))
(= AND (lx.(ly.((x y) false)))))
(= OR (lx.(ly.((x true) y)))))
(= IMPLY (lx.(ly.((OR (NOT x)) y))))
(= 0 (ls.(lz.z)))
(= succ (lw.(ls.(lz.(s ((w s) z))))))
(= pred (ln.(ls.(lz.(((n (lx.(ly.(y (x s))))) (lx.z)) (lx.x))))))
(= add (lx.(ly.((x succ) y))))
(= mult (lx.(ly.((x (y succ)) 0))))
(= 1 (succ 0))
(= 2 (succ 1))
(= 3 (succ 2))
(= 4 (succ 3))
(= 5 (succ 4))
(= 6 (succ 5))
(= 7 (succ 6))
(= 8 (succ 7))
(= 9 (succ 8))
(= isZero (lz.(((z false) NOT) false)))
(= pair (lx.(ly.(ls.((s x) y)))))
(= fst (lp.(p true)))
(= snd (lp.(p false)))
(= cons (la.(lb.(lf.((f a) b)))))
(= car (lx.(x true)))
(= cdr (lx.(x false)))
(= Y (lf.((lx.(f (x x))) (lx.(f (x x))))))
(= g (lf.(ln.(((isZero n) 1) ((mult n) (f (pred n)))))))
(= Z (lf.((lx.(f (ly.((x x) y)))) (lx.(f (ly.((x x) y)))))))
(= I (lx.x))
(= K (lx.(ly.x)))
(= S (lx.(ly.(lz.((x z) (y z))))))

ラムダ計算 SKI コンビネータ ２

ラムダ計算

SKI コンビネータでどんなコンビネータが作れるか試してみた。まず I コンビネータは恒等関数だし、K コンビネータは定数関数だ。これは論理値の true に当たる。これを利用して KI コンビネータで論理値の false が作れる。その他、SKK コンビネータは I コンビネータと同じ。SII コンビネータで自己言及コンビネータが作れる。

lambda> I
(lx.x)
lambda> K
(lx.(ly.x))
lambda> (K I)
(ly.(lx.x))
lambda> ((S K) K)
(lz.z)
lambda> ((S I) I)
(lz.(z z))

これは端末から色々と入力すると自然に見つかるが、目的のラムダ項を作るための方法はないのだろうか。そこで単なる関数適用 (x y) を SKI コンビネータで記述するにはどうすればいいか考えてみた。

lambda> (x y)
(x y)

(I x) = x だから ((I x) y) = (x y) になる。

lambda> (I x)
x
lambda> ((I x) y)
(x y)

これは I コンビネータに x と y の２つの引数を与えると、関数適用になることを示している。つまり、関数適用を行うコンビネータは I だ。

それでは、 (x (y z)) の場合はどうすればいいだろうか。

 lambda> (x (y z))
(x (y z))

変数 z は (S (x z)) ((y z)) の形を取ると引数として外にくくり出せる。そこでまず、x を (K x) z の形に変える。

lambda> (((K x) z) (y z))
(x (y z))

これで z をくくりだして body の部分を ((S (K x)) y) の形にまとめることができる。

lambda> (((S (K x)) y) z)
(x (y z))

この時点で変数 y も z もくくりだされてしまったので後は x を外に出すだけだ。変数 x が含まれるのは (K x) の部分なので (S (K x)) の関数適用の部分を (S (x z)) (y z)) の形に整える必要がある。K コンビネータを利用すれば S = ((K S) x) に置き換えることができる。

lambda> (((((K S) x) (K x)) y) z)
(x (y z))

((K S) x)) (K x) の関数適用の部分は S コンビネータを利用して変数を外にくくりだすことができる。すなわち、((K S) x)) (K x)) = ((S (K S)) K)) (x) である。

lambda> (((((S (K S)) K) x) y) z)
(x (y z))

無事に全ての変数をくくり出せたので、

S(KS)K

が求めるコンビネータである。

lambda> (= M ((S (K S)) K))
lambda> (((M x) y) z)
(x (y z))

ラムダ計算 SKI コンビネータ

ラムダ計算

コンビネータとはラムダ式の body の変数が全て束縛変数となるラムダ式（関数）のことだ。例えば λx.x は引数の値をそのまま返す恒等関数だが、ラムダ抽象された変数は x で body の部分の変数も x しかない。

lambda> ((lx.x) a)
a

このようなコンビネータには名前がつけられているものがある。上の恒等関数にも名前がつけられており I (Identity combinator) コンビネータと呼ばれる。

I = λx.x

ラムダ計算機で検証すると次のようになる。

lambda> (= I (lx.x))
lambda> (I a)
a

また、K コンビネータ (Constrant combinator) は２つの引数を持ち、第一の引数を渡すと、引数１個の関数になる。この関数は引数にどのような値を与えても最初に与えられた第１引数の値を返す。このため定数関数と呼ばれている。

K = λxy.x

ラムダ計算機では次のようになる。

lambda> (= K (lx.(ly.x)))
lambda> ((K a) x)
a

S コンビネータ (Substitution Combinator) は構造が複雑で、第３引数に第１引数を関数適用したものを、第３引数に第２引数を関数適用したものに関数適用する。

S = λxyz.(xz)(yz)

ラムダ計算機では次のようになるが、あまり有り難みがわからない。

lambda> (= S (lx.(ly.(lz.((x z) (y z))))))
lambda> (((S x) y) z)
((x z) (y z))

実は、この SKI コンビネータには特別な性質がある。この３つを組み合わせると、ラムダ抽象を使わずにどのようなラムダ式でも記述できるのだ。そこで、それを検証してみることにする。

先ず、恒等関数だが、これは I コンビネータそのものだ。

lambda> I
(lx.x)
lambda> (I a)
a

また、K コンビネータは論理式の true そのものだ。

lambda> K
(lx.(ly.x))
lambda> ((K a) b)
a

そこで K コンビネータを I コンビネータに関数適用すると、それは false になる。

lambda> (K I)
(ly.(lx.x))
lambda> (((K I) a) b)
b

true と false ができたので、条件分岐を作ってみたいが、ラムダ抽象を使わずにどうやって作ればいいのだろうか。条件分岐は引数が c x y の３つなので I コンビネータや K コンビネータでは役不足だ。それで、S コンビネータを使うことを考えてみる。作りたいラムダ式は次のようなものだ、

λcab.cab

このラムダ式の body の部分を取り出すとこれは ((c a) b) である。これは変数 a を変数 b と c に順に関数適用していることを示している。

lambda> ((c a) b)
((c a) b)

そこで I コンビネータを c に関数適用すると次のようになる。

lambda> (((I c) a) b)
((c a) b)

すなわち I コンビネータが条件分岐を表す関数である。I = λx.x なので I は引数を一つしか取らないが、(I a) の値は関数なので引数を取れる。したがって、I は結果的に３つの引数を取ることが可能なのだ。これがラムダ式が高階関数であることの威力だ。

lambda> I
(lx.x)
lambda> (I true)
(lx.(ly.x))
lambda> (((I true) a) b)
a

Ω - コンビネータ λ.(x x) は最も単純な自己言及関数だが、これも SKI コンビネータで表現できる。Ω - コンビネータの body の部分を次のように等価なラムダ式に置き換えていけばいい。

lambda> (x x)
(x x)
lambda> ((I x) (I x))
(x x)
lambda> (((S I) I) x)
(x x)

したがって、Ω = SII である。

ラムダ式を SKI コンビネータで表すと、束縛変数が表に出てこない。ラムダ抽象を使わずに関数適用のみでラムダ式を記述することができるからだ。スタックにプッシュしたデータをやり取りする場合のように、束縛変数の名前が不要になってしまう。すなわち、α変換に関して考慮しなくて良くなる。コンビネータにはこのようにプログラミングのフレームワークを変える性質もあるようだ。そうして、この SKI コンビネータはラムダ記法と同じ様にチューリング機械と同等の表現力がある「チューリング完全」らしい。

SKI コンビネータのうち I コンビネータは次のように SKK で定義できるので、理論的には S コンビネータと K コンビネータだけで全ての関数が表現できる。しかし、上の例でも分かるように I コンビネータを利用したほうが使いやすい。

lambda> ((S K) K)
(lz.z)
lambda> (((S K) K) hello)
hello

ラムダ計算 括弧の対応

ラムダ計算

ラムダ計算機では括弧の省略ができないので、どうしても括弧の対応の管理が大変になる。しかしラムダ式の文法の単純さを考えたら、入力のやり方で煩雑さを減らせる。

ラムダ計算で括弧が出現するのは、ラムダ抽象の (λx.M) と関数適用 (M N) の２つだけだ。そのうえ、カッコ内に存在する項は２つしかない。そこで、入力するときに、これらの場合に括弧の対応を先にやってしまっておけば対応する括弧の検討もしなくて済む。

先ずラムダ抽象の場合、(lx.) 括弧の中に変数のラムダ抽象だけを記入する。ボディは後で記入するようにする。たとえば、ラムダ記法の true は次の順序で入力していくとよい。

(lx.)

(lx.(ly.))

(lx.(ly.x))

また、これを変数に束縛するときは (= true ) のように = と 変数名とスペースを括弧でくくったものを最初に作成する。そうしてそのスペースのあとに上の要領でラムダ項を記入していく。

(= true )

(= true (lx.))

(= true (lx.(ly.)))

(= true (lx.(ly.x)))

また関数適用の場合は、何も入れない括弧 ( ) を入力する。そうしてその中に関数適用を記入していくのだ。

()

(() )

((lx.x) )

((lx.x) a)

ユーザーが定義した関数を使うときは、先頭に関数の引数分の括弧を記入する。たとえば、true の様に引数が２個の場合最初に括弧を２つ記入し、そのあとに関数とスペースを置く。それに続けて第１引数とその後ろに閉じ括弧、スペース、第２引数、閉じ括弧という風に記入していく。

((true

((true a)

((true a) b)

このラムダ抽象と、関数適用の書き方の原則を守っていれば比較的複雑な項も括弧の対応をあまり気にしないで記入していくことができる。たとえば if 文の場合引数の文のラムダ抽象を先に作成し、そのあとにボディの部分を記入する。

(= if )

(= if (lc.))

(= if (lc.(lx.)))

(= if (lc.(lx.(ly.))))

(= if (lc.(lx.(ly.( )))))

(= if (lc.(lx.(ly.(( ) y))))

(= if (lc.(lx.(ly((c x) y)))))

if を使うときは、引数が c, x, y の３つなので先頭に３つの括弧を置く。そうして引数を与えるたびに閉じ括弧で閉じる。

(((if

(((if ture)

(((if true) a)

(((if true) a) b)

NOT の定義を if 関数を利用して行うときは上のやり方を組み合わせて次のようにする。ユーザ定義のif 文は引数が３つなので、先頭に３つの括弧を記入する。

(= NOT )

(= NOT (lx.))

(= NOT (lx.(((if ))

(= NOT (lx.(((if x))

(= NOT (lx.(((if x) false)))

(= NOT (lx.(((if x) false) true)))

これらのルールで Y コンビネータのような複雑な項も記述が簡単になる。

(= Y )

(= Y (lf.))

(= Y (lf.(() ())))

(= Y (lf.((lx.) (lx.)))

(= Y (lf.((lx.(f ()) (lx.(f ())))))

(= Y (lf.((lx.(f (x x)) (lx.(f (x x))))))

実際にラムダ計算機で入力した結果は次のようになる。

lambda> (= true (lx.(ly.x)))
lambda> (= false (lx.(ly.y)))
lambda> (= if (lc.(lx.(ly.((c x) y))))
lambda> (= if (lc.(lx.(ly.((c x) y)))))
lambda> (((if true) a) b)
a
lambda> (= NOT (lx.(((if x) false) true)))
lambda> (NOT true)
(lx.(ly.y))
lambda> (= Y (lf.((lx.(f (x x))) (lx.(f (x x))))))

このように、括弧の対応づけは要素的な項が現れるたびに行っておけば煩雑さを免れる。