2019-12-22

Ehrenfeucht-Fresse ゲーム

こんにちは，19erの東條です．
この記事はISer Advent Calendar 2019の23日目の記事として書かれたものです．
adventar.org

ちなみに，記事の題名にある人名は，エーレンフォイヒトとフレーゼと読みます．

はじめに

最近，一階述語論理などの論理に対する構造を有限構造に制限して考える有限モデル理論という分野を勉強していて，そこで用いられる「ゲーム」という基本的道具を紹介したいと思います．
と言っても，パズルと思って適当に読んでいただければ幸いです．

なお，本記事は全面的に[1]を参考にしています．

ゲームの紹介

いきなりですが...
一階論理で書けるような性質についての(有限)構造の類似性を次のようなゲームで特徴付けることができます．言語(非論理記号の集合) $\sigma$ としては述語記号のみを含む(関数記号は含まない)有限集合を考えます．

定義

構造 $\mathcal{A}, \mathcal{B}$ と自然数 $m \in \mathbb{N}$ が与えられたとき，Ehrenfeucht-Fresseゲーム $G_m(A,B)$ とは二人の競技者spl(spoiler)とdup(duplicater)によって次のようにplayされるゲームである．
以下を $j \in 1..m$ について $m$ 回繰り返す．

splはどちらかの構造 $\mathcal{A}$ か $\mathcal{B}$ を選ぶ

splは選んだ構造 (仮に $A$ とする)から要素 $a_j \in A$ を１つ選ぶ

dupは逆の構造(この場合は $B$ )から要素 $b_j \in B$ を１つ選ぶ

勝利条件

このゲームの結果として2つの有限列 $a_1\dots a_m, b_1 \dots b_m$ が得られるわけですが(ゲームの進行過程でsplが選んだ構造に応じて，例えば $a_1$ はsplが選んだ〜つまり $b_1$ はdupが選んだ〜が $a_3$ はdupが選んだ，という状況もあり得ます)．この列が次の条件を満たしている時にdupは勝利します(その他の時はsplの勝利)

$a_i = a_j \implies b_i = b_j$ つまり，これらの列は部分関数 $A \rightharpoonup B$ を定める.

項数 $n$ のどのような述語記号 $R \in \sigma$ と重複を許した長さ $n$ の部分列 $a_{i_1}\dots a_{i_n}, b_{i_1}\dots b_{i_n}$ ( $i_{k} \in 1..m$ )に対しても $\mathcal{A} \vDash R a_{i_1}\dots a_{i_n} \Leftrightarrow \mathcal{B} \vDash R b_{i_1}\dots b_{i_n}$ が成り立つ．つまり $a_1\dots a_m$ と $b_1 \dots b_m$ は $R$ によっては区別できない．

条件2は要するに $a_1\dots a_m$ が $\mathcal{A}$ に生成する部分構造と $b_1\dots b_m$ が $\mathcal{B}$ に生成する部分構造が列の順番も含めて全く同じ(つまり $a_1\dots a_m \mapsto b_1 \dots b_m$ が部分構造どうしの同型である)ということを言っています．

例をみる前に，このようなゲームを考えると嬉しいこととして，次のような定理があります．

定理1

有限個の関係記号からなる言語 $\sigma$ と有限 $\sigma-$ 構造 $\mathcal{A}, \mathcal{B}$ に対してdupが $G_m(\mathcal{A}, \mathcal{B})$ に必勝とする．この時， $\mathcal{A}$ と $\mathcal{B}$ はquantifier-rankが $m$ 以下の一階述語論理の文(閉論理式)で区別できない．

注

言語が定数記号を含んでいても上の定理は成り立つのですが，簡単のためにこの記事では述語記号しか含まない言語 $\sigma$ に制限しています．
quantifier-rankとは論理式の構文木を辿った時に量化が現れる個数の最大値のことです．

定理を証明するのは簡単だし面白いのですが，話を先に進めるためにまずはこの定理を認めてしまいましょう．

少し話は変わりますが...
有限 $\sigma-$ 構造の性質は，その性質を満たすような $\sigma$ 構造の部分クラスと同一視できます(例えば，グラフの連結性を連結なグラフ全体の集まりと考える)．
この時，このようなクラス(性質)が一階述語論理で公理化できるとは，ある一階述語論理の文 $\phi$ が存在して任意の構造 $\mathcal{A}$ に対して
$\mathcal{A}$ がこのクラスに属することと $\mathcal{A} \vDash \phi$ となることが同値になることであると定義できます．

さて，すごく勘のいい人は気づいたと思うのですが．ゲームに関する上の定理を使えば次のようなことが言えてしまいます．

定理2

$K$ を有限 $\sigma-$ 構造のあるクラス(性質)とする．もし任意の $m\in \mathbb{N}$ に対して有限 $\sigma-$ 構造 $\mathcal{A}\in K, \mathcal{B}\not\in K$ でdupが $G_m(\mathcal{A}, \mathcal{B})$ に必勝するようなものが存在するとすると，クラス $K$ を定義する一階述語論理の文は存在しない．

証明は簡単です．
どんな一階述語論理の文 $\phi$ もある有限のquantifier-rankを持つのだから，それより大きい $m$ をとるとある２つの構造 $\mathcal{A}\in K, \mathcal{B}\not \in K$ があってdupは $G_m(A,B)$ に必勝する．よって定理1よりこれらの構造は $\phi$ では区別できない．

注意し忘れていたのですが，この記事では構造といえば有限構造を考えることにします．つまり任意の構造について~という主張は任意の有限構造について〜と読み換えます．

さて，この定理2を用いていくつかの有限構造のクラスの定義不能性を見てみましょう．

例1

空言語(つまり，論理式に現れる関係記号が相当関係 $=$ のみ)のとき，偶数構造全体のクラスは定義不能．

解説

空言語 $\sigma = \emptyset$ における $\sigma-$ 構造とは単に集合 $A,B$ のことであることに注意しましょう．任意に与えられた $m \in \mathbb{N}$ に対して $m$ 元集合 $A$ と $m+1$ 元集合 $B$ を取ると，dupは明らかに $G_m(A,B)$ に必勝になってしまいます．実際，各手番において
splがそれまでに選んだ要素と異なる要素を選んだのならdupはもう片方の構造において今までと異なる要素を選べば良く，
以前打った手と同じ手を打ってきたときは前回の手番の時の対応する要素を打ち返せば良いです．

ポイントは $A,B$ ともサイズが $m$ 以上であることで，splが $m$ 手全て異なる要素を打ってきたとしてもdupは小さい方の構造の要素を尽きさせてしまう心配がないので， $m$ 手の間ならいわばdupは片方の構造のサイズが小さいことがバレないようにやり過ごせるという感じでしょうか．

さて，次はどうでしょうか

例2

順序の言語 $\sigma = \{<\}$ において偶数全順序全体のクラスは一階述語論理で公理化不能．

解説

有限構造を考えているときは，定義できなかったクラスに適当な(「適切な」ではなく「デタラメな」の意味)全順序を入れるだけで定義可能になってしまうということがしばしばあるのですが，この場合はそれをやっても無理という主張です．

順序の公理：
$\phi := \forall x[\lnot x < x]\land \forall x y z [x < y \land y < z \rightarrow x < z]\land \forall x y [\lnot x = y \rightarrow x < y \lor y < x]$
を満たすような有限構造全体のサブクラスとして偶数構造のクラスが定義できないことを示したいので，任意に与えられた自然数 $m \in N$ に対して文 $\phi$ を満たす $\{<\}-$ 構造 $\mathcal{A}, \mathcal{B}$ でサイズが $|\mathcal{A}| = l+1, |\mathcal{B}| = l$ のものについてdupが $G_m(\mathcal{A}, \mathcal{B})$ に必勝になることを示せば十分です．ここで $l$ は任意の大きい値です．

dupの必勝戦略を考えるために，まず有限線形順序を次のように両端点のある線分と見なします．
　　小・ー・ー・ー・ー・ー・ー・ー・大

それでは，長さが1だけ違う線分を２つ用意して実際に $G_3(A,B)$ をplayしてみます．
　　 $A$ ・ー・ー・ー・ー・ー・ー・ー・
　　 $B$ ・ー・ー・ー・ー・ー・ー・
splの初手は
　　 $A$ ・ー $\overset{spl}{a_1}$ ー・ー・ー・ー・ー・ー・
だったとしましょう．これに対しdupが
　　 $B$ ・ー・ー $\overset{dup}{b_1}$ ー・ー・ー・ー・
と返したとします．

手を１つ打ったことで線分が前と後ろに2分割されたというのは重要な視点です．
分割された２つの区間のうち，小さいほうの区間の長さに相違があるので
splはここにつけ込んで2手目を
　　 $B$ ・ー $\overset{spl}{b_2}$ ー $\overset{dup}{b_1}$ ー・ー・ー・ー・
と打つとdupは
　　 $A$ $\overset{dup}{a_2}$ ー $\overset{spl}{a_1}$ ー・ー・ー・ー・ー・ー・
と打ち返すしかないでしょう．そこでsplが最後の一手を
　　 $B$ $\overset{spl}{b_3}$ ー $\overset{spl}{b_2}$ ー $\overset{dup}{b_1}$ ー・ー・ー・ー・
と打てばdupが $A$ のどの・に3手目を打っても $a_3 < a_2$ とすることはできません．
例えば
　　 $A$ $\overset{dup}{a_2}$ ー $\overset{spl}{a_1}$ ー・ー $\overset{dup}{a_3}$ ー・ー・ー・ー・
$\rightarrow$ dupの負け( $a_2 < a_3$ だが $b_3 < b_2$ )

dupの敗因は，まだ十分な手番が残っているにも関わらず大きさの異なる小さい区間を作ってしまったことにあります．一方で，残りの手数に比べて十分大きい区間の長さが $A,B$ 間でちょっとくらい違っていたところで，dupはその区間の点が尽きることが無いようにうまく手を返していくことができそうです．

つまり，dupの必勝戦略を一言で表すなら「残りの手数に対して大きい区間はとりあえずどうでも良いが，小さい区間はとにかく完全再現する」ということになります．実際先の例でdupが初手を
　　 $B$ ・ー $\overset{dup}{b_1}$ ー・ー・ー・ー・ー・
と返していれば，少なくとも同じ方法ではsplは勝つことができなかったでしょう．

では具体的に $m$ 手ゲームに対するdupの必勝戦略を構成してみます．構造のサイズはなんでも良いので $|A| = 2^m+2,\ |B| = 2^m + 1$ と取ることにします．

先ほども注意した通り，splが手を置くごとにどれかの区間が2分割されます(区間の端，つまり最大，最小元や既に置かれた点に再び手が置かれた時は２つの区間のうち片方の長さが0になったと考える)．

dupはsplが選んだのと逆の構造で，splが手を置いた区間と同一の区間( $n$ 手うつと $n+1$ 区間できるが，そのうち初めから見て同じ $i$ 番目の区間)に手を置く必要がありますが，残りの手番から考えて基準を下回るような長さの区間(特に長さ0の区間はどんな手番においても)が生じた時はそちら側の区間の長さは完全に揃えるように手を打つ必要があります．
$j$ 手目の攻防
　　　　　 $\mathrm{len}< 2^{m-j}$
　　　〜 $a_i$ ー・ー・ー $\overset{spl}{a_j}$ ー・ー・〜・〜・ー $a_{i'}$ 〜
　　　〜 $b_i$ ー・ー・ー $\overset{dup}{b_j}$ ー・ー・〜・〜・ー $b_{i'}$ 〜
　　　　　ここの長さを　　こちらは長いので
　　　　　揃える　　　　　どうでも良い

大きさを揃えた区間と逆の区間は構造 $A,\ B$ 間で一般に長さが異なりますが，この部分が十分大きければこの違いは問題になりません．

この基準長を残りの手数 $j$ に対して $2^j$ としてみましょう．

初めの構造のサイズは $2^m+2$ と $2^{m}+1$ なので，splの初手でどちらかの構造に小さい区間が作られてdupがもう片方でそれを再現したとしても，大きい方の区間はどちらも基準長 $2^{m-1}$ を超えていて問題ありません．

この考え(基準長未満の長さの区間は再現)に基づいて打っていけば残り $j$ 手の状態で $\mathcal{A}$ と $\mathcal{B}$ の $i$ 番目の区間 $I^i_A,\ I^i_B$ が
　　 $|I^i_A| = |I^i_B|$ であるか， $|I^i_A| \not= |I^i_B|$ かつ $|I^i_A|,|I^i_B|\geq 2^j$
を満たすように打っていくことができます(考えてみてください)．

小さい区間は大きさが一致しているので，分割の片方の大きさを揃えるように打つと自動的にもう片方も揃うことも利用しています．

これで， $m$ 手までならdupはsplの手を耐えきる方法が確立されました．つまり，dupは $G_m(\mathcal{A}, \mathcal{B})$ に必勝ということになります．

おまけ

以降はおまけです．暇で暇で仕方のないときに考えてみてください．

定理1の証明

定理1の対偶は

$\mathcal{A} \vDash \phi$ かつ $\mathcal{B} \not\vDash \phi$ となるquantifier-rank $\leq m$ の $\sigma-$ 文 $\phi$ があるとき，dupは $G_m(\mathcal{A}, \mathcal{B})$ に必勝にならない．

となります．ここではより強くこのような $\phi$ からsplの必勝戦略を論理式の構造に関する帰納法で構成してみましょう．

$\phi = \psi_1 \lor \psi_2$ のときは，適切な $\psi_i$ を選べば
$\mathcal{A} \vDash \psi_i$ かつ $\mathcal{B} \not\vDash \psi_i$
とできます． $\phi = \psi_1 \land \psi_2$ のときも同様．
$\phi = \lnot \psi$ のときは $\mathcal{A}$ と $\mathcal{B}$ の役割を反転すれば良いです．

以上の操作にはsplの手番は消費しません．
splが帰納法を潜るのに手を消費するのは以下の量化子の場合です．

では， $\phi = \exists x \psi(x)$ のとき
このときは上手く $a \in \mathcal{A}$ を選べばどんな $b \in \mathcal{B}$ を選んでも
$\mathcal{A} \vDash \psi[a$ ]かつ $\mathcal{B} \not\vDash \psi[b$ ]
とできます．つまりsplはこのような $a\in\mathcal{A}$ を選べばdupが何を打ち返してこようが構造帰納法を１つ潜ることができます．

上のように手を打っていけば， $\phi$ のquantifier-rankが $m$ 以下なのでsplは $m$ 手以内に $\mathcal{A}$ と $\mathcal{B}$ を区別するatomic sentenceに到達するでしょう．

例3

有限連結グラフ全体のクラスは一階述語論理で公理化不能
ただし，グラフの言語は $\sigma = \{E\}$ ( $E$ はarty 2)で単純無向グラフの公理
$\forall x[\lnot Exx]\land\forall xy[Exy \rightarrow Eyx]$ を満たす構造を考える．

ヒント

基本的なアイデアは例2(順序)と同じです．任意に与えられた $m\in\mathbb{N}$ に対して何かとても大きい連結グラフ $\mathcal{A}$ と非連結グラフ $\mathcal{B}$ を持ち出して $G_m(\mathcal{A},\mathcal{B})$ に対するdupの必勝戦略を与えると良いです．

このような構造を探すのに時間をかけさせてしまうのはこの記事の趣旨に反するので，上手くいく $\mathcal{A}$ と $\mathcal{B}$ の組の例を１つ挙げるとすると．

$\mathcal{A}$ はとても大きなサイクル
$\mathcal{B}$ は $\mathcal{A}$ ２つのdisjoint union

というのがあります．アイデアは，「手数に対して長さが大きいサイクル(ここでは $\mathcal{A}$ )では直径の両側にあたる2点は非連結であるのと変わりない」というものです．

例2で用いた「分割の短い方を再現」作戦も役に立つと思います．

例4

atomが偶数個の有限ブール代数全体のクラスは一階述語論理で公理化不能

注
atomが $k$ 個の有限ブール代数とは，集合 $X := \{1,\dots,k\}$ の冪集合 $2^{X}$ に真の包含関係 $\subset$ を用いて半順序を入れたものです(もちろん言語は $\sigma = \{\subset\}$ )．~~ならはじめからそう書けよ...~~

ヒント

以前までと違うように見えますが実は同様の手法が適用できます．
ゲーム中で手を打つという操作は全体を $X$ とするベン図に新しく１つ丸を描くという行為に対応しており，dupが再現しなければならないのはベン図の幾何的な配置です．

$X,\ Y := X\bigsqcup\{v\}$ を十分大きくとって $\mathcal{A}:=2^X,\ \mathcal{B}:=2^Y$ に「小さい分割たちを完全再現作戦」を使いましょう．

面白いことに，「atomが偶数個の有限ブール代数」は構造に何かある任意の線型順序が(ブール代数の関係 $\subset$ とは独立に)入っていることが仮定できれば一階述語論理で公理化可能です．

実はこの結果を用いて一階述語論理が有限の範囲内でInterpolation性を持たないことを示すこともできます．

おわりに

正直ここまでちゃんと読んでくださった方はあまりいないんじゃないかと思うのですが，まあ人生でこんなことを考える機会が一回くらいあってもいいよね，というくらいの気分になっていただけたならとても嬉しいです．

ちなみに，上でも見たように一階述語論理は有限構造を扱うには弱すぎる(強すぎるという側面もあるのですが，とりあえず適してはいません)ので，例えば二階の量化子を導入したり変数の個数をある有限個に制限したりと様々な工夫をして有限の範囲でも適切な他の論理が用いられます．このような論理に対しても，上で使ったゲームという枠組みはとてもよく当てはまり便利な道具立てとなっています．面白いですね．

参考文献

[1] Ebbinghaus, and Flum, Finite Model Theory 2nd ed., Springer, 1999.

2018-12-17

schemeとλ計算

　この記事はISer Advent Calendar 2018 - Adventarの17日目の記事として書かれました．昨日の記事はmin-caml compiler pwn （ISer advent calendar 12/2出題）writeup - cookies.txt .scrでした．

19erの@iojjoo(twitter)です．記事など書くのははじめてですが，いい機会なので何か書いてみることにしました．よろしくお願いします．

　この記事は，λ計算にちょっと触れたあとに scheme の quote 構文を使って色々遊んでみた，というものです．プログラミングをちゃんと触り始めて日が浅く，コードが汚かったり読みにくかったりすると思いますが，その点は申し訳ないです．

導入，定義

　さて，λ計算に関する授業を取っていない方（19erにもしいたら）でも読めるようにしたいのと，体系を制限して話を簡単にするために，以下で少し定義を行います．

生成規則

　λ計算とは「計算」の理論を形式的に展開するための体系の一つです．形式言語理論で触れたオートマトンを考えてもらえばわかりやすいですが，計算の形式理論ではまず現在の計算状態に当たるものを用意して，それらの内有限個のものの間をあらかじめ定まった規則で遷移していく，というモデルが基本です．このとき，あらかじめ用意される状態のセットは必ずしも有限であるとは限りません（状態間の遷移は有限）．λ計算では状態は次の規則で定帰納的に定まる，λ式と呼ばれる記号列で表されます：

　 $V$ を可算個の変数の集合とする；

　　（変数） $x \in V$ のとき，x はλ式；

　　（適用） $M, N$ がλ式のとき， $(M\ N)$ はλ式；

　　（抽象） $M$ がλ式， $x \in V$ のとき， $(\lambda x.\ M)$ はλ式．

最も外側のかっこはよく省略されます．例はラムダ計算 - Wikipediaなどを参照してください．（抽象）において $M$ の内側にある変数 $x$ を束縛変数と言います（ただし，より内側で束縛されていないもの）．以降では全ての変数が束縛されているようなλ式（閉λ式，コンビネータと呼ばれる）のみを考えます．

計算規則

　さて，次は計算（遷移）規則です．以下では， $M[x:=N$ ] は $M$ の束縛されていない（自由な） $x$ を全てλ式 $N$ で置き換えたものです．

　　（簡約） $(\lambda x.M)\ N \rightarrow M[x:=N$ ].

今，閉λ式のみを考えているので，難しいことは考えずに $\lambda x.$ を取り除いたせいで自由になってしまった $x$ に $N$ を代入してしまえば大丈夫です．また，この規則をλ式中の一部分（部分λ式）に適用することもあります．

scheme上のλ計算

　さて，これで実際に計算をしてみます．ここで，scheme の次の式を考えます．

　　(define fact (lambda (x) (if (= n 0) 1 (fact (- x 1)))))

この式はが再帰を計算するのはプログラミング言語が再帰を処理してくれるからですが，この再帰をもう少しだけλ計算っぽくやってみます．そのために，次のλ式を使います：

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

これはYコンビネータと呼ばれるλ式で，任意のλ式 M に対して YM -> M (YM) という簡約を持ち，この性質を使うと次のように再帰ができます．

　　 fact = (λf. (λx. (if (= x 0) 1 (* x (f (- x 1)...)

とすると，

　　(Y fact) 2 -> (fact (Y fact)) 2 -> ~ -> (if (= 2 0) 1 (* 2 ( (Y fact) (- 2 1) )))

-> (* 2 ( (Y fact) (- 2 1) ))

赤字の部分にまた同じ簡約を繰り返せばこれで再帰ができることがわかります．

評価戦略

　今，簡約の順番は自由でした．しかし，通常（プログラミング言語上など）の場合簡約の順番がちゃんと決まっていて，それを評価戦略と言います．また，ある評価戦略でそれ以上簡約出来ないλ式を標準形と言い，λ式を繰り返し簡約して標準形を求めることを評価と言います．schemeの評価戦略は値呼びというもので，この戦略は以下の簡約列をたどるので Yコンビネータを使えません：

　　　(Y fact) -> (fact (Y fact)) -> (fact (fact (Y fact))) -> ...

schemeでYコンビネータを使う場合，このような無限ループ生じないようにYの定義を少しいじれば大丈夫ですが，やはりせっかくなのでYコンビネータを使ってみたいということで，ここでは別の評価戦略を採用する方法を考えます．つまり，shceme上に別の計算体系を作ってしまって，その上で式を評価してみます．

　このとき使うのがquoteという構文です．実験の資料を参照してもらうと基本的なことがわかるのですが，今回の使い道は，λ式にquoteを適用してその抽象構文木をlist構造で取得するというものです．

計算体系の実装

　各λ式について構文木が簡単に手に入るのであれば，簡約などの定義を構造帰納法に乗せれば，形式的に実装するのは簡単です．よって以下では，計算体系の定義を帰納的に整理します．このとき，定義，実装を，代入，簡約，評価の3つに分けて考えるのが有用です．また，話を簡単にするために以下では純粋なλ式のみを考え，+, -, 1, 2, #t, if, ... などはいったんおいておきます．

　以下で用いる評価戦略は正規順序というものです．さて，まず代入の定義です．

　　（base1） $x \in V,\ x[x:=N] \equiv N;$

　　（base2） $y \in V,\ y[x:=N] \equiv y;$

　　（step App） $(L\ M) [x:=N] \equiv (L[x:=N])\ (M[x:=N]);$

　　（base Abs） $(\lambda x. M) [x:=N] \equiv \lambda x. M;$ 　　；内側の束縛に触らない

　　（step Abs） $(\lambda y. M) [x:=N] \equiv \lambda y. (M[x:=N]).$

次に，簡約（ $\rightarrow$ ）の定義です．

　　（base1） $x \in V, \Rightarrow\ x\rightarrow x;$

　　（base2） $(\lambda x. M)\ N\ \rightarrow\ M[x:=N] ;$

　　（step App1） $M\rightarrow M' \Rightarrow M\ N \rightarrow M'\ N$

　　（step App2） $x \in V,\ M\rightarrow M'\ \Rightarrow\ x\ M\rightarrow x\ M'$

　　（step Abs） $M \rightarrow M' \Rightarrow (\lambda x. M) \rightarrow (\lambda x. M')$

最後に，評価です． $M$ に上の簡約規則を用いて一回簡約したものを $\operatorname{red}(M)$ と書きます．

　　 $\operatorname{eval}(M)$ ＝

　　　　 $\operatorname{if}\ M \equiv \operatorname{red}(M)\ \operatorname{then}\ M\ \operatorname{else}\ \operatorname{eval}(\operatorname{red}(M))$ ．

　さて，あとはこれをそのままschemeの構文に落とします．以下は準備です．

(define snd (lambda (x) (car (cdr x))))
(define thrd (lambda (x) (car (cdr (cdr x)))))

(define length
  (lambda (x)
    (if (not (list? x))
	1
	(if (null? x)
	    0
	    (+ 1 (length (cdr x)))))))

lengthはリストデータに対しては長さを返し，その他のデータには1を返す関数で，λ式がどの形かを判定するのはこの length を使うと簡単です．また，listデータとして同一であるかどうかの判定は equal? でできます（ = は整数の演算なので使えない）．次が代入，簡約，評価の関数です．

(define sbst
  (lambda (M x N)
    (let* ((ver (car x)) (lh (length M)))                              
      (cond 
            ;Base Case
            ((= lh 1) (if (equal? M ver) N M))  
            ;Step App                                       
	    ((= lh 2) (list (sbst (car M) x N) (sbst (snd M) x N)))    
            ;Step Abs          
	    ((= lh 3) (if (equal? (snd M) x)                                                 
			   M
			   (list (car M) (snd M) (sbst (thrd M) x N))))))))

(define red (lambda (M)
	      (let ((lh1 (length M)))
		(cond 
                       ;Base Case1
                      ((= lh1 1) M)
                       ;when in App form
		      ((= lh1 2)
		       (let ((lh2 (length (car M))))
			 (cond 
                                ;Base Case2
                               ((= lh2 3) (sbst (thrd (car M)) (snd (car M)) (snd M)))
                                ;Step App
			       ((= lh2 2) (list (red (car M)) (snd M)))
			       ((= lh2 1) (list (car M) (red (snd M)))))))
                        ;Step Abs
		      ((= lh1 3) (list 'lambda (snd M) (red (thrd M))))))))

(define eval
  (lambda (M)
    (if (equal? M (red M))
	M
	(eval (red M)))))

　これで，evalを使えばquoteをかけたλ式を標準形まで簡約することが出来ます．現時点で扱えるのはλ式だけですが，λ計算の理論を使えばλ式だけで自然数の計算を行うことが出来ます．アイデアは，何かある特定の形のλ式を自然数に対応させておいて，引数と出力をその形で行うと約束しておくというものです．このとき，各自然数はチャーチ数と呼ばれる閉λ式で表されます．このあたりの理論はラムダ計算 - Wikipediaがよくまとまっているので，必要であればそちらを参照してください．使う道具を以下で定めます．定義した式を後の定義に流用するときは list 構文を使わないと，変数名がそのまま quote されてしまうことに注意が必要です．

(define zero '(lambda (f) (lambda (x) x)))
(define one '(lambda (f) (lambda (x) (f x))))
(define two '(lambda (f) (lambda (x) (f (f x)))))
(define three '(lambda (f) (lambda (x) (f (f (f x))))))
(define four '(lambda (f) (lambda (x) (f (f (f (f x)))))))
(define five '(lambda (f) (lambda (x) (f (f (f (f (f x))))))))

(define suc '(lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(define add '(lambda (n) (lambda (m) (lambda (f) (lambda (x) ((n f) ((m f) x))))))) 
(define mult '(lambda (n) (lambda (m) (lambda (f) (lambda (x) ((n (m f)) x))))))

(define true '(lambda (x) (lambda (y) x)))
(define false '(lambda (x) (lambda (y) y)))

(define iszero (list 'lambda '(n) (list (list 'n (list true false)) true)))

(define if* '(lambda (p) (lambda (x) (lambda (y) ((p x) y)))))
(define if-iszero?
  (list 'lambda '(n)
	(list 'lambda '(x)
	      (list 'lambda '(y)
		    (list (list (list if* (list iszero 'n)) 'x) 'y)))))

(define pair '(lambda (x) (lambda (y) (lambda (p) ((p x) y)))))

(define car* (list 'lambda '(x) (list 'x true)))
(define cdr* (list 'lambda '(x) (list 'x false)))

(define ss (list 'lambda '(x) (list (list pair (list cdr* 'x)) (list suc (list cdr* 'x)))))
(define pred (list 'lambda '(n) (list car* (list (list 'n ss) (list (list pair zero) zero)))))

(define Y '(lambda (f) ((lambda (x) (f (x x))) (lambda (x) (f (x x))))))

(define fact-func
  (list 'lambda '(f)
	(list 'lambda '(x)
	      (list (list (list if-iszero? 'x)
			  one)
		    (list (list mult 'x) (list 'f (list pred 'x)))))))

(define fact (list Y fact-func))

細かい部分がよくわからない場合は気にしないでください．ここで言いたいのは，例えば (eval (list (list add two) three)) というλ式をschemeで評価すると，(lambda (f) (lambda (x) (f (f (f (f (f x))))))) が表示され，(eval (list fact four)) を評価すると f を24個含むチャーチ数が表示される，というものです．five の fact は少し時間がかかりますが，ちゃんと出来ます．

計算体系の拡張

　さて，Yコンビネータを使うという目的はなんとか達成されたものの，このままでは信じられないくらい遅いです．それに加え，120の代わりに f が120個入っているλ式を返されても知らんがなという気持ちにしかなりません．これを解決する方法も作ってみたのですが，それをかくと記事が終わらないので，概略だけ書きます．

定数とその上の演算

　上の体系に1, 2, #f, #t, +, *, if, ... などの定数やその上の演算を加えた拡張を行います．やり方は簡単で，代入と簡約で新たにこれらの構文をトラップして処理するケースを付け加えればOKです．例えば，term := (quote (+ 1 2)) の形のデータをトラップして，
　　(+ (snd term) (thrd term))
という式を評価すれば良いです．ここで，(quote 1) が 1 と同様の定数データとして扱われることが本質的です．つまり，(+ '1 1) を評価するとちゃんと 2 になります．ただし，('+ 1 1) などはエラー（quote前後で同じなのは定数 1, 2, #t, ...）になることと，''1 はもう同じとして扱われないことに注意が必要です．

評価戦略

　評価を手取り早く高速にするために，正規順序簡約の規則のうち（App2）と（Abs）を除きます．このままだとめちゃくちゃ早くなる代わりに簡約が途中で止まってしまうようになるので，値呼び戦略で補います．値呼びは簡約と評価の間での同時再帰で実現できます．例えば，簡約規則（base2）を，

　　（Val base 2） $(\lambda x. M)N \rightarrow M[x:=\operatorname{eval}(N)]$

とすれば良いです．しかし，このままでは Yコンビネータが使えない元の状態に後戻りなので，値呼びをする部分を，上で追加した演算のうち自然数演算の引数と if の第一引数に限定します．こうするとちゃんと Yコンビネータが使えるまま拡張できます．試してみましたが，10の階乗くらいなら数秒でできるようになりました（正規簡約は6の階乗で全然値が帰って来なくなってしまった）．「10の階乗に数秒かかる」というのがなかなかの怪文な気もしますが．．．

終わりに

　さて，長くなりましたがこの記事はこの辺りで終わりにします．このようなわかりにくくて長い記事を最後まで読んでいただきありがとうがざいました．自分は勘違いが多いタイプなので，〜がおかしいんじゃないかと思った場合は教えてくださるとありがたいです．本記事では純粋なλ計算の理論にはほとんど何も触ることができなかった（悲しい）ので，興味を持たれた方はぜひ何かちゃんとした本を読んでみてください．下に参考にした文献一覧をつけておきます．[1]は型無しλ計算全般について教科書的に使いました．[2]は有名な本で，λ計算を拡張するところを少しだけ参照しました．[3]は評価戦略がちゃんと書いてあってとても参考になりました．関係ないですが，様相論理のところも面白かったです．

　明日はkammer0820さんの記事です．どんな文章が生成されるのか楽しみですね．

参考文献

[1]Cardon, Hindley, 2009: Lambda-Calculus and Combinators an Introduction, Cambridge Press.
[2]Benjamin C. Pierce, 2002: Types and Programming Languages, MIT Press.
[3]萩谷昌己, 西崎真也, 2007: 論理と計算の仕組み, 岩波