ラムダ計算でコーディング

どうもAaronです。

今回はみんな大好きラムダ計算です。

早速行ってみよう！

1. 計算モデルについて

今回の記事中この章のみラムダ計算に関する話題ではなく、理論計算機科学で使われる計算モデルという概念についてになっています。若干連続性に欠けますが、僕は何か話をするとき、それがどんな理論に位置づけられるのかとか、別の理論での対応物は何かという話を最初にするのが好きなので今回もそういうことにします。

1.1 計算モデル

ラムダ計算は一般に計算モデルの一つとして多くの論理学や計算理論の教科書に登場します。

では計算モデルというのは何かという事になりますが、これは物理的な実装やその他外部状況に影響されない計算機や計算手順、アルゴリズムなどを記述する数理モデルのことを言います。少し比喩的に言ってしまえば非常に理想化されたプログラム言語の仕様のようなものだと思ってもよいです。

しかしここで問題なのが計算モデルという言葉は恐らく形式的に定義される語ではないということです。少なくとも僕の知っている講義・資料・和文英文Wikipediaなどから形式的な定義と呼べるものは見つけられませんでした（もし「あるよ」って方がいたら教えてください）。

これがなぜかというと多くの計算モデルは

  1. ある決まった種類の対象から同じ種類の対象への関数、またはその対象に関する述語を、
  2. あらかじめ定められた、直感的に言って人間、あるいは既存のコンピュータが容易に行えそうないくつかの操作の、
  3. 一定の形式の組み合わせ（関数としてみるなら合成）や繰り返し（いわゆる再帰）によって定義する定義方法の枠組みである。

という程度の共通点を持っていますが、

1.に関して、そもそもその「同じ種類の対象」（計算モデルの上で定義される関数の定義域）は計算モデルごとに全く異なります。比較的有名なところでいえば

  • Turing機械ならば、任意の長さの（典型的には）\{0,1\}が刻まれたテープ。
  • 今回扱うラムダ計算ならば、ラムダ項と呼ばれるある種類の項。
  • （計算モデルかは怪しいが）Kleeneの公理化された再帰関数なら自然数。
  • （有限型、プッシュダウン、線形拘束…）オートマトンでは固定された文字からなる文字列。

等見事にバラバラです。

2.や3.に関してもそもそも定義域が決まっていない状況で、「（その定義域上の対象に対する）直感的に人間や既存のコンピュータが容易に行えそうな操作」や、「その合成や再帰の一定の形式」を特徴づけるのはやはり無理があるようです。

このような理由から計算モデルという言葉自体の定義は難しく、割とふわっとつかわれるようです。

一方で計算モデルの具体的な例はこの世に数えきれないほどあげる（or 作る）ことができます。というのも上で上げたものの他、殆どのプログラミング言語はある程度の修正や抽象化の元に計算モデルと思うことができるし、既に知られた計算モデルに記号を追加するなどしたマイナーチェンジ版も無数に作ることができるからです。

そこで我々は何が計算モデルなのかを議論するより、与えられた二つの計算モデルの間の関係を定義して議論した方が実りがあります。計算モデル全体が上手く定義できずとも、二つの計算モデルが与えられたときにそれらを「比較」することができるからです。

次の節ではそれを行うことにします。

1.2 解釈可能性、エミュレート可能性

前節でお話しした通り、計算モデルによる関数定義の仕方自体に共通の特徴を洗い出すのは難しいので、ここでは計算モデルの枠組みで定義された関数や述語とその定義域を用いて、三個組

A=(C_A,F_A,P_A)

(ただし
\displaystyle F_A\subset\bigcup_n Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n-times},C_A\cup\{\uparrow\})\\P_A\subset\bigcup_n Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n-times},\{true,false,\uparrow\})
を満たす。）
をして計算モデルと呼ぶことにします。ここで唐突に出てきた記号\uparrowは直感的にはプログラムが無限ループを引き起こすことを表し、普通の文脈で出てくる関数や述語に比べて無限ループを起こす可能性がある分だけある意味拡張された概念になっています。

ここでちょっとした問題があり、計算モデル上の関数や述語は、例え関数、述語として外延的に等しくても*1、定義の仕方（プログラムでいう実装やアルゴリズム）の違いにも着目することが自然であるため、F_A,P_A上の等号は集合論的なそれとは違うと考えないとうまくいかないことがあり*2、どう定義したものか悩ましいのです。その意味で上の\displaystyle\bigcup_n Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},C_A\cup\{\uparrow\}) や\displaystyle\bigcup_n Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\{true,false,\uparrow\})の部分集合というのは非厳密な言い方ですし、正式にどう定義するかは難しいのですが、正直に白状すればこの記事は全体を通して、割とその点を誤魔化しています。

またここで用いた定義ではF_AとP_Aを分けていますが、この辺の区別も計算モデルによるところが大きく、一般に「～オートマトン」と呼ばれるような種類の多くの計算モデルは定義に受理状態と拒否状態を含むことで述語を陽に扱いますし、多くのプログラム言語を計算モデルとみた場合ならばAの中にプリミティブなBool値（の対応物）を持っているでしょうからそれで表現するかもしれませんし、Kleeneの再帰関数や今回扱うラムダ計算では陽に述語を扱う機構もプリミティブなBool値も持たないため体系内の特定の値をBool値のコードとして用います（体系内にプリミティブなBool値やBool値のコーディングを持つ計算モデルではF_A\supset P_Aと見做せることになります。）。

さて補足と脱線で長くなりました。そろそろ本題に入りましょう。

A=(C_A, F_A, P_A), B=(C_B, F_B, P_B)をそれぞれ計算モデルとしたとき、ある関数の三個組\mathcal{I}=({}^{I_C}:C_A\cup\{\uparrow\}\to C_B\cup\{\uparrow\},\ {}^{I_F}:F_A\to F_B,\ {}^{I_P}:P_A\to P_B)が

\forall a\in C_A\cup\{\uparrow\}.a^{I_C}=\uparrow\iff a=\uparrow

\forall a,b\in C_A.a^{I_C}=b^{I_C}\Rightarrow a=b

\forall \vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\ f\in F_A.f^{I_F}(\vec{a}^{I_C})=(f(\vec{a}))^{I_C}

\forall \vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\ p\in P_A.p^{I_P}(\vec{a}^{I_C})\iff p(\vec{a})

(但しここで\vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times}に対して\vec{a}^{I_C}=(a_0^{I_C},\ a_1^{I_C},...,\ a_{n-1}^{I_C})とする。)

を満たすとき\mathcal{I}をAのBでの解釈と呼び、そのような\mathcal{I}が存在するとき、AはBで解釈可能であるという事にします。

更にもう一歩進めて今度は五個組

\mathcal{E}=(\varphi_F,\varphi_P,\ {}^{E_C}:C_A\cup\{\uparrow\}\to C_B\cup\{\uparrow\},\ {}^{E_F}:F_A\to C_B,\ {}^{E_P}:P_A\to C_B)

（\varphi_F,\varphi_PはそれぞれF_B,P_Bに属する関数、述語の列でその第n項を\varphi_{F,n},\varphi_{P,n}と書けば、

\varphi_{F,n}\in F_B\cap Map(\underbrace{C_B\times C_B\times\cdots\times C_B}_{n+1\ times},C_B\cup\{\uparrow\})\\\varphi_{P,n}\in P_B\cap Map(\underbrace{C_B\times C_B\times\cdots\times C_B}_{n+1\ times},\{True,False,\uparrow\})

を満たす。但し

F_A\cap Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},C_B\cup\{\uparrow\})=\emptyset

の時に限り、\varphi_{F,n}=undefinedとなることを許す。\varphi_{P,n}についても同様。）

が

 \forall a\in C_A\cup\{\uparrow\}.a^{E_C}=\uparrow\iff a=\uparrow

\forall a,b\in C_A.a^{E_C}=b^{E_C}\Rightarrow a=b

\forall \vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\ f\in F_A.\varphi_{F,n}(f^{E_F},\vec{a}^{E_C})=(f(\vec{a}))^{E_C}

\forall \vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\ p\in P_A.\varphi_{P,n}(p^{E_P},\vec{a}^{E_C})\iff p(\vec{a})

を満たすならば、\mathcal{E}をAのBでのエミュレータと呼び、そのような\mathcal{E}が存在するとき、AはBの中でエミュレート可能という事にします。実際に特定のAを固定して考えるときは、より多くの条件を課したエミュレータを考えるのが自然です。例えばAが関数合成や部分適用に閉じているならば、それらによって得られる関数fのf^{E_F}がBの中でもととなる関数や値から計算できることを要求したり、Aが帰納的に関数を定めるような系であるなら各インダクティブステップに対応する変換がBの中で計算可能であることを要求するのは自然でしょう。

容易にわかるように計算モデルが部分適用に閉じている（即ち

f(x_0,...x_{n-1})\in F_B\to\forall c\in B.\forall m\lt n.f(x_0,...x_{m-1},c,x_{m+1},...,x_{n-1})\in F_B\\p(x_0,...x_{n-1})\in P_B\to\forall c\in B.\forall m\lt n.p(x_0,...x_{m-1},c,x_{m+1},...,x_{n-1})\in P_B

を満たす）限りエミュレート可能性は解釈可能性よりも強い条件です。

解釈とエミュレートの関係は、言語間のトランスパイルと一方の言語を他方の言語で作られたヴァーチャルマシン上で実行することとの関係とほぼ同じなのです。

特にある計算モデルは自分自身を自明な方法で解釈できますが、エミュレートできるかどうかは相当非自明であることに注意してください。すなわち、ほかの言語をエミュレートするためにはまず自分自身がヴァーチャルマシンを構築するのに足りるだけの強さを持たなくてはならないのです。次の節ではこの事実が主要な役割を果たします。

1.3 Church-Turingの提唱

前節で定義された解釈可能性やエミュレート可能性によって知られている計算モデル同士を比較すると興味深いことがわかります。

実は「自然な」計算モデルのうち、かなりの大部分は互いに互いをエミュレート可能であり*3、残りはその大部分の計算モデルによってエミュレートされるが、逆にそれのクラスを解釈することはできないという意味でより弱いものであることがわかっているのです。言い換えると自然な計算モデル（≒人間にできる計算）に対して、既に性能の限界が経験的に知られており、それより真に弱いものを作ることはできても、強いものを作ることはできないとされているのです。「経験的に」というのは重要で、再三繰り返すように計算モデル自体には明確な定義がないので、これは何らかの数学的事実では（今のところ）ないのです。

この（繰り返すようにあくまで経験的な）事実に基づいてその「大部分のクラス」の計算モデルによって定義できる関数を計算可能関数と呼ぼう、と提唱したのがChurchとTuringで（実はこのあたり歴史的には結構ややこしいのですが）、この提唱による計算可能関数の「定義」をChurch-Turingの提唱と呼んでいます。

さて、実は先ほどから急に主役を張り出したこの「大部分の計算モデルのクラス」にはTuring完全クラスという名前がついています。このTuring完全クラスには以下のような特徴づけで定義することができます。

Def.1.3.1 (Turing完全)

\text{計算モデル}A\text{がTuring完全}\iff\text{Turing機械と}A\text{は、}I_C\text{が互いに逆関数となるような解釈で相互に解釈可能}

 「Turing機械」のところは単なる基準なので、お好きなTuring完全性がメタ的に既知である計算モデルに変更できます（定食屋さんのメニューに書いてある「セットの麺物は以下からお好きな物に変更できます」のイントネーションでお読みください）。


この条件を満たすクラスが節の冒頭で言った通り相互にエミュレート（解釈よりも強いに注意）できるのは以下のように証明できます。

Prop.1.3.2 Turing機械は自身をE_C=idであるようなエミュレータでエミュレート可能。

証明)略（Turing機械で実際にプログラムを書くことになる。難しくはないが非常に時間と紙幅がかかる。）。

Cor.1.3.3 AがTuring機械で解釈可能ならば、Turing機械でエミュレート可能。

証明)上の命題からTuring機械上の自身のエミュレータ

\mathcal{E}=(\varphi_F,\ \varphi_P,\ id,\ {}^{E_F},\ {}^{E_P})

がとれる。

また仮定からAのTuring機械上での解釈

\mathcal{I}=({}^{I_C},\ {}^{I_F},\ {}^{I_P})

が取れる。

そこで\mathcal{E}'=(\varphi_F,\ \varphi_P,{}^{I_C},\ {}^{E_F}\circ{}^{I_F},\ {}^{E_P}\circ{}^{I_P})

とするとこれはTuring機械上でのAのエミュレータである。

実際

\varphi_{F,n}( (f^{I_F})^{E_F},\vec{x}^{I_C})=f^{I_F}(\vec{x}^{I_C})=f(\vec{x})^{I_C}

\varphi_{P,n}( (p^{I_P})^{E_P},\vec{x}^{I_C})\iff p^{I_P}(\vec{x}^{I_C})\iff p(\vec{x})

Lem.1.3.4 AがTuring機械と、I_Cが互いに逆関数となるような解釈によって相互に解釈可能ならば、AはE_C=idであるようなエミュレータで自身をエミュレート可能。

Turing機械上でのAの解釈を

\mathcal{I}=({}^{I_C},\ {}^{I_F},\ {}^{I_P})、

A上でのTuring機械の解釈を

\mathcal{I}'=({}^{I_C^{-1}},\ {}^{I'_F},\ {}^{I'_P})、

Turing機械の自己エミュレータを

\mathcal{E}=(\varphi_F,\ \varphi_P,\ id,\ {}^{E_F},\ {}^{E_P})

とすると、
\mathcal{E}'=(\varphi_F^{I'_F},\ \varphi_P^{I'_P},id,\ {}^{I_C^{-1}}\circ{}^{E_F}\circ{}^{I_F},\ {}^{I_C^{-1}}\circ{}^{E_P}\circ{}^{I_P})

はAの自己エミュレータである。

実際

\varphi_{F,n}^{I'_F}( ( (f^{I_F})^{E_F})^{I_C^{-1}},\vec{x})\\(=\varphi_{F,n}^{I'_F}( ( (f^{I_F})^{E_F})^{I_C^{-1}},(\vec{x}^{I_C})^{I_C^{-1}}))\\=(\varphi_{F,n}( (f^{I_F})^{E_F},\vec{x}^{I_C}))^{I_C^{-1}}\\=(f^{I_F}(\vec{x}^{I_C}))^{I_C^{-1}}\\=(f(\vec{x})^{I_C})^{I_C^{-1}}=f(\vec{x})

\varphi_{P,n}^{I'_P}( ( (f^{I_P})^{E_P})^{I_C^{-1}},\vec{x})\\(\iff\varphi_{P,n}^{I'_P}( ( (p^{I_P})^{E_P})^{I_C^{-1}},(\vec{x}^{I_C})^{I_C^{-1}}))\\\iff \varphi_{P,n}( (p^{I_P})^{E_P},\vec{x}^{I_C})\\\iff p^{I_P}(\vec{x}^{I_C})\iff p(\vec{x})

Lem.1.3.5 AがBで解釈可能で、BがCでエミュレート可能ならばAはCでエミュレート可能。

証明)Cor.1.3.4を用いれば、Cor.1.3.3とほとんど同様の証明に帰着する。

Thm.1.3.6 A,BがTuring完全なら相互にエミュレート可能。

証明)1.3.2-1.3.5から直ちに従う。

 
結果であるThm.1.3.6は勿論ですが、Lem1.3.4やLem1.3.5も極めて重要な性質です。特にLem.1.3.4の性質はTuring完全な計算モデルの際立った特徴だと言われます。

またLem.1.3.5からわかるように自分自身をエミュレートできる体系AでBが解釈できるなら、実際にはBはAでエミュレートもできるのでエミュレート可能性と解釈可能性の違いに注目するべきなのはTuring完全よりも能力の小さい計算モデルを研究するときに限られます。

さて、今回扱うラムダ計算もTuring完全であることが知られています。

従ってラムダ計算でのコーディング手法を知れば全ての計算可能な関数を理論上は定義することができるわけです。

2. ラムダ計算

2.1 構文とその直感的意味

ラムダ計算のオリジナル版はChurchによって導入されました。その後現在に至るまで、多くの拡張や亜種が定義されたり、これから紹介する「λ抽象」と呼ばれる独特な関数定義のノーテーションが便利な記法として（ある意味ではここで紹介するような理論的なラムダ計算の議論とはほとんど独立に）使われたり*4してきましたが、その中でもオリジナル版のラムダ計算は極端なまでに簡潔な文法を持ちます。なんと構文はたった三種類しかないのです。すなわちBNFで書けば

<lambda term>=
<variable>
| "("<lambda term><lambda term>")"
| "(""λ"<variable>"."<lambda term>")"

となります。ただしここで<variable>と書いているのは「プリミティブな記号」の意味で、普通は可算無限個用意されていると考えます。ほかの用途で使う"λ"や"."や"(",")"はここに含まれてはいけません。

次に上で定義される構文の直感的意味を説明しますが、その前に一つ重要な注意として、ラムダ計算においては、全ての項や変数は「（高階）関数」であるとみなされ（得）ることを指摘しておきます。誤解を恐れず言えば、「自然数」とか「実数」といった「それ以上分解できない値」という概念が存在せず、定義された値は全て関数として（も）見られるのです。その為、前章で使ったノーテーションで言えばC_Aがラムダ項の（この記事のかなり後のほうで見るある条件を満たす）集合になっていて、C_A\subset F_A\supset P_Aという構図になります。これを念頭に次を読んでください。

上で上げた各構文は左から順にそれぞれ「原子項」、「関数適用」、「λ抽象」と呼ばれることがあります。これが各構文の直感的意味を表していて、

  1. 原子項は、変数一個のみによる構文がラムダ項であること
  2. 関数適用はそのまま、前者のラムダ項を関数とみて、後者のラムダ項をその引数に与えるという構文が新たな項を与えること

をそれぞれ意味します。ラムダ計算の文脈では関数に引数を与えることに括弧を使わない慣例があることを知っておいてください。（e.g.fにxを引数として与えるときはfxのように書く。f(x)とはしない。）

λ抽象はややとっつきにくい概念です。まず次の例を見てみてください。

f(x)=x^2

だれしもが高校生のころ、こんな式を見たことがあると思います。ここで「xが関数の仮引数を意味する」というのを左辺のxが表しているわけです。

f(2)=4

のように書くことと比較すれば、これは一種のパターンマッチングによる定義だという事もできます。

更に別の言い方をすれば、パターンマッチによって変数xが「fの仮引数」という意味を込めて「抽象化（つまりある決められた値のためのプレースホルダーでなく、あらゆる値が入りうる仮引数として働くことを明示）」されているわけです。fと常にともにあるというニュアンスで「束縛」と呼ぶ人もいます。

ラムダ計算では変数の抽象化（≒関数定義）にこの種のパターンマッチを用いるのではなく\lambda x.T（Tはラムダ項）のように書きます。これでラムダ項Tを関数と見て、xが仮引数として働く、という意味になります。例えば\lambda x.xはラムダ項であり、それが意味するところはxを受け取って、xを返す関数、即ち恒等関数になるわけです。そして\lambda x.の後に出てきたxはこの関数の仮引数として「抽象化」されているわけですが、ここでのxのように抽象化された変数を「束縛変数」、そうでない変数を「自由変数」とよびます。


いくつか合法なラムダ項の例をのせてこの節を終わりましょう。

x

(xy)

( (xy)z)

(\lambda x.x)

(\lambda z.(xy) )

( ( (\lambda z.(xy) )z)x)

2.1.1 略記

前節の最後の例でわかる通り、ラムダ項を完全に構文的に正しく書くのは大変な手間です*5。
そこで標準的には以下の四つの略記を用います。

  • 最外の項およびλ抽象の直後の項の括弧は省いてよい。

(e.g.(xy)\to xy,\lambda x.(xy)\to\lambda x.xy)

  • 関数適用が連続するときに括弧を省いたなら、それは左結合だったものと読む。

(e.g.( (xy)z)\to xyz,(x(yz) )\not\to xyz)

  • 反復適用に関する略記、\underbrace{T(T(\dots(T}_{n\text{-}times\ T}U)\dots)\to T^nU。特に勝手なTに対してU\to T^0U。
  • 連続したλ抽象があるなら、最初以外のλ(と括弧)を省略してよい。

e.g)(\lambda x.(\lambda y.(\lambda z.( (xy)z) ) ) )\to\lambda x.y.z.xyz

これらの省略法のうち、一番目と二番目は文字通りの意味で略記/省略ですが、三番目と四番目は意味づけの上で自然になるような工夫でもあります。

三番目の略記はラムダ計算が扱うオブジェクトが関数で、関数適用が「前者の項に後者の項を適用する」という意味であったことを思い出せば、

\underbrace{f(f(\dots(f}_{n\text{-}times\ f}(x))\dots)

を

f^n(x)

と略記するのと同じノリであることがわかります。

最後の略記は実は極めて重要な考え方を示唆していますので、それを次節で説明しましょう。

2.1.2 Curry化された多変数関数

ここまで一通りラムダ計算の定義を読んできた中で、もしかしたらこんな風に疑問に思われた方がいるかもしれません。

「λ抽象の構文は<variable>を一つしかとらなくていいの<variable>+じゃないの？多変数関数表現できなくない？」

と。

答えは「とらなくていいし、この条件でも多変数関数を表現する方法はある」のです。

これを説明するために、まずラムダ計算の事はいったんこちらにおいて一般的な集合論を考えてみます。

集合論でMap(X,Y)をY^Xと書くことがあります。

ここでちょっとしたメタ読みをしてみましょう。なぜ指数の形の記号を使うのでしょう？答えは簡単で指数法則を（ある意味で）満たすからなのです。

すなわち

  1. X^{Y_1\sqcup Y_2}\simeq X^{Y_1}\times X^{Y_2}
  2. X^{(Y_1\times Y_2)}\simeq(X^{Y_1})^{Y_2}

が成り立つのです。ここでA\simeq BはA,B間にいい感じの全単射が生えることを意味しています。いい感じってなんやねんという話ですが、多分両辺をXに関する自己関手と見た時、自然同型とかで定式化できそうですが圏論弱者なのでわからないです…。単なる全単射よりは条件が必要なことを主張している自覚があるのでとりあえず「いい感じ」としておきます。

ここでそのいい感じの全単射は明確に構成出来て、

1.に対応する全単射は

split:X^{Y_1\sqcup Y_2}\to X^{Y_1}\times X^{Y_2}\\ split(f)=(f|_{Y_1},f|_{Y_2})

2.に対応するのは

curry:X^{(Y_1\times Y_2)}\to(X^{Y_1})^{Y_2}\\curry(f)=g:a\mapsto (h:b\mapsto f(a,b))

となります。

さて、2のほうを見て、なぜ突然集合論の話をし始めたか、お判りいただけたでしょうか？ここのcurryによって、多変数関数（\iff多変数を「同時に」受け取る関数\iffなんらかの直積集合からの関数）が、同じ数の変数を「順次に」受け取っていく一変数（関数値）関数と同型になっているのです。これが一変数関数しか定義できない状況で多変数関数を表現する、Curry化と呼ばれる手法です。


さてここで前節の第四の略記を見てみましょう。実はこの略記はCurry化によって表現された疑似的な多変数関数を、多変数関数らしく書くための略記なのです。

実際前節で挙げた例を見ると、略記にする前の形は一変数を受け取って一変数関数を返す関数値関数ですし、略記の形は\lambda (x.y.z).xyzと隠れた括弧が入ると思えば多変数関数らしく見えませんか？

また構文上は一変数関数のみを扱い、Curry化によって多変数関数を表現する方法は、単に構文の定義を簡潔にできるというだけでなく、実効的な意味で、プリミティブに多変数関数を許す方法よりも優れている面もあります。

例えばプリミティブに多変数関数を許している方式で

f(x,y)=x+y

と定義したとします。この時特にx=1とした関数を扱いたい場合、基本的には関数を再定義するしかありません。

しかしCurry化による表現方針ではf\ 1と書いてそのような関数を表現する「部分適用」が可能なのです。これは「引数を『順次に』受け取っている」からに他なりません。

このようにCurry化というのは関数をプリミティブに扱う文脈では非常に優れた表現方針なのです。実際、非常に理論的なモデルであるラムダ計算だけにとどまらず、それをベースとした実用的な言語であるHaskellも、プリミティブな多変数関数を持たずCurry化による表現を行っていることからも、その有効性が知れるでしょう。

2.2 代入

さて突然ですが、何か変数的な概念が出てきたとき、最初に考えることは何でしょう？

そう「代入」ですね。ラムダ計算においても原子項は変数でしたから当然代入を考えたくなります。

ラムダ項Sをラムダ項Tの自由変数xに代入すること（この操作および結果として得られる項を記号でT[x\leftarrow S]と書きます）は直感的にT中の自由変数xをSに置き換えるだけで8割方良いのですが、二つだけ注意すべきことがあります（厳密な定義は僕の気が向いたら注釈に書きます。*6）。

第一の注意は代入によって束縛変数は置き換えられないということです。これはプログラム言語でいう変数のシャドーイングのような状況で問題になり、こう定義することで安全にシャドーイングされた状態になります。

第二の注意が「代入によるアブストラクタの新たな変数の捕捉」などと呼ばれる問題です。こちらを例を使って説明しましょう。

まずxyというラムダ項を考えると、これは原始項二つによる関数適用の形のラムダ項でx,yはともに自由変数です。もうひとつ\lambda x.xzというラムダ項を考えます。今度のxは束縛変数で関数の仮引数です。ここまでは良いでしょう。ではここで第二のラムダ項のzに第一のラムダ項を代入することを考えると結果はどうなるでしょうか？

\lambda x.x(xy)でしょうか？そうだとするとこんな違和感があります。\lambda x.x(xy)のxはどちらも全体を関数として見てその仮引数ですから、自由変数がいつの間にか束縛変数に化けているのです。すなわち代入によって\lambda（アブストラクタ）がもともと自由だったxを「捉え」て、束縛変数にしてしまっているのです。これは意味論上問題を引き起こします。

この問題の解決策は実は著者によって異なります。一致しているのは、直接代入すると新たに変数を「捕捉」してしまうλの仮引数名を、本質的にはすぐ後で説明するα変換によって「捕捉」しない仮引数名に入れ替えるという事なのですが、このケースでの代入自体の定義は人によって異なり

  1. そのようなケースでの代入の定義の中でα変換（やそれに対応する代入）を使ってしまい、再帰的定義とする人
  2. そのようなケースでは代入が「失敗する」、すなわち「結果がない」としておき、そのようなケースの発生自体をα変換を使って回避する人
  3. そのようなケースでも先に挙げたような違和感を押し殺して素直に機械的に置き換えることにしておき、そのようなケースの発生自体をα変換を使って回避する人

等がいます。この記事ではどれでもいいとしておきます。ただこの問題があることだけを認識しておいてくれればいいのです。

2.3 α変換

さて今度は急に哲学的な問いになりますが、「計算」とは何でしょうか？

様々な答えはあり得るでしょうが、一応現時点での僕の答えは


「ある対象をある意味で『同じ』であると言えるような、それでいてやはり何らかの意味で『より簡潔な』形へと変換する行為やその繰り返し」


という事になります。

例えば2+3=5という式を書いて「計算をした」と主張するとき、人は2+3と5がある意味で同じであるにもかかわらず5のほうが簡潔であると考える故にそうするわけです。

「ある意味で『同じ』であると言える」というのは数学でいえば「ある同値関係で同値」という事になるでしょうから、最初に与えられた『ある対象』と同値な同値類のうち、何らかの意味で『より簡潔な』代表元をとると言い換えることができそうです。

この見地に立つとラムダ計算には重要な二つの同値関係が定義されています。それが今節と次節で扱う「α同値」と「β同値」です*7。「α変換」や「β変換」という言い方をした場合はこれらの同値関係にある者同士での変換、言い換えれば代表元の取り換えを意味します。

さてではα同値の定義を見てみましょう。二つの項がα同値である（t\equiv_\alpha sと書くことにする）は以下のように定義されます。

\lambda x.T\equiv_\alpha \lambda y.T[x\leftarrow y]\text{(但しここで}y\text{は}T\text{に自由変数としては現れない)}\\T\equiv_\alpha S\land U\equiv_\alpha V \Rightarrow TU\equiv_\alpha SV\\T\equiv_\alpha S\Rightarrow\lambda x.T\equiv_\alpha\lambda x.S

論理式でややこしいので直感的に言ってしまえば、これは単に関数の仮引数名の付け替えです。「関数の仮引数名を付け替えても『意味』が同じ」というのは聞いたことがある方も多いでしょうし、納得もしやすいでしょう。

しかし名前の付け替えではどちらが簡単とは言えないと思った方もいらっしゃるでしょう。それはごもっともな指摘で、実はラムダ計算において上記の意味で「真に」計算をしていると言えるのは実は次の節で説明するβ変換のみだとも考えられます。すなわち「α変換」はあまり表舞台に出てこないのです。それでもα変換をここで紹介するのには二つの意味があります。

第一には、前節で匂わせた通りラムダ計算においての代入の定義はα変換と本質的に一種の相互依存関係を持っており、そしてβ変換では代入が核心的な役割を果たすためにα変換が必要なのです*8。ここでは前節でご紹介した「そのまま代入すると『新たな変数の捕捉』が起きるような代入」を回避できるように仮引数名を付け替えた形を、「より簡潔な形」と定義したと思っていただければよいかと思います。

第二には、やはりβ変換の定義と関係してしまうのですが、これ以降では特に計算の結果得られた項の、α同値な違いをほとんど無視します。そのため「α変換」はあまり表舞台に出てこなくても、「α同値（で割ること）」は本質的に重要な役割を果たすのです。

これら二つの事から、α同値はやはり詳しく述べる必要があると考えてここに置いた次第です。

2.4 β変換

さていよいよこの話がやってきました。β変換です！前節でも少し言ったようにβ変換はほとんどラムダ計算という計算モデルの「計算」部分を一手に担っているといっても過言ではないほど重要なものです。そのため実際にコーディングをするのが目標の我々にとっても勿論重要な部分です。しっかりと学んでいきましょう。

大げさに喧伝したにふさわしくβ変換の定義はα変換のように一発ではいきません。段階を踏まなくてはいけないのです。

まずラムダ項をラムダ項に変換する変換としてβ-1変換、記号ではラムダ項T,Sに対してT\to_{1\beta}Sというものを定義します。

(\lambda x.T)S\to_{1\beta}T[x\leftarrow S]\\T\to_{1\beta}S\Rightarrow TU\to_{1\beta} SU\\T\to_{1\beta}S\Rightarrow UT\to_{1\beta} US\\T\to_{1\beta}S\Rightarrow \lambda x.T\to_{1\beta} \lambda x.S

これだけみてもなんのこっちゃらなので、直感的意味を説明します。

β-1変換の直感的意味は、関数適用の「解決」にあります。

例えばλ抽象の時と同じ例ですが、日常的な文脈でf(x)=x^2,f(2)=2^2=4と書く場合の事を考えてみてください。このときf(2)というのはfに引数として2を与えるという「意味」を持っていて、それを実際に実行、解決したのが2^2です。

これと同様に関数適用というのは関数に値（ラムダ計算ではラムダ項）を与えることでしたから、それを解決するという事は仮引数に代入をすることで…そうなっていますね。このことからこの二つが「ある意味で同じ」と言えそうな気持もわかるでしょう。

さてこれでβ変換を定義できます。

ラムダ項Tがラムダ項Sにβ変換される（記号ではT\to S）とは、有限回のβ-1変換およびα変換の組み合わせでTがSに到達できるときに言う。

単にβ-1変換の推移閉包ではないことに注意してください（僕は一度大学の友人に説明しているときに間違いました。）。α変換を途中に挟んでいいことにしているのは、先に述べた通りβ-1変換で代入が起こるとき、新たな変数の捕捉問題が起きるのを回避できるようにするためです。そしてまた前節で計算（これはβ変換と言い換えてよいでしょう）の結果のα同値の違いは無視するといった理由もここにあります。すなわちβ変換の定義でα変換を任意に挟めることにより、最後にα変換をしたと考えれば、結局β変換の「仕方」次第では構文論的な等号が成り立っていたともいえるのでα同値の違いは気にしても仕方がないのです。
もっと形式的な定義もあるのですが、記述が本当に面倒くさいのでやりません。

また「β変換によって移る」という関係の同値閉包をβ同値と呼び、a=_\beta bのように書くことを付け加えておきます。

2.5 Church-Rosser性

先に言っておくと、ここでは証明は扱いません。というより僕もこの証明は理解も記憶もしておらず、何か参照しなくてはいけない状態です。

しかしそれでもこの性質が成り立つという事実だけは安心してコーディングをするうえで欠かせないので指摘しておきます。

ラムダ計算のβ変換は明らかに任意性があります。そもそもβ-1変換からして、4つのうち最初のルールが適用できる場所（β簡約基といいます）が複数あるかもしれないし、間に好きなだけα変換を挟んでもいいのだからかなりなんだってできそうに見えます。

しかし「ラムダ項Tが、異なるラムダ項SとUにβ変換されたとすると、SとUをさらに『うまく』β変換してやると同じラムダ項Vにできる」という事が知られています。

このような性質をChurch-Rosser性あるいは合流性と言い（微妙に異なった性質にこれらの用語を使い分ける流派もあるとか）、この性質があれば、特にもうβ-1変換できないようなラムダ項（β標準形、もしくは単に標準形と言います）にまで変換出来た場合には、α同値の分だけしか結果に差が出ないことがわかります。

この性質のおかげで我々はコーディングするとき、「少なくとも一つβ同値なβ標準形があるならば、それに変換してくれ。」とだけ、β変換をする人、または機械、または神、に注文しておけば、その誰かさんが自分の意図通りに変換してくれるかに悩む必要は、少なくともβ標準形を持つラムダ項に関しては、ないということになります。この後しばらくは出てくるラムダ項がほとんどがβ標準形を持ちますから、上の事実によって安心してコーディングができます。後にそうではない事態が出現しますが、それはその時にまた説明します。

3. ラムダ計算でコーディング

この章以降ではラムダ計算上に数学的概念（自然数や真理値、リストなど）を埋め込み、それによって実際にプログラム・計算が行えることを見ることによってラムダ計算が計算のモデル出ることを示すのが目的となります。

3.1 Church数項と加法・乗法

実は二章でラムダ計算の定義については全てお話ししてしまったのです。

こういわれてこう思った方もいるでしょう。「え？数学的概念は？」と。

ないんです。先に言った通りラムダ計算においては全ての対象が関数であり、従って自然数も実数もないと先に言った通りです。

しかし我々が計算と言われて想像するのは少なくとも自然数が登場するもののはずです。

ではどうするか、ある形の関数を自然数（のコード）だと「見做して」やるのです。

もったいぶらずに言いましょう（すでにもったいぶっている気もしますが）。

我々は以下のように「見做し」を「定義」します（知っている人向けに言えば集合論で0:=\emptyset,1:=\{\emptyset\},2:=\{\emptyset,\{\emptyset\}\},\cdots n+1:=n\cup\{n\},\cdotsと「定義」するのと同じです。）。

0:=\lambda S.Z.Z\\1:=\lambda S.Z.SZ\\2:=\lambda S.Z.S(SZ)\\n:=\lambda S.Z.S^nZ

すなわち関数と初期値を受け取って関数を初期値にn回反復合成した値を返すという高階関数（ラムダ項は全て高階関数なのですが）をnのコードとするのです。この方法でコードされた自然数の事をChurch数項と呼んだりします。

しかしながら自然数がコードされたからといって安心してはいられません。これはあくまでも「見做し」であって、本来は自然数でも何でもないのですから、我々の知っている自然数にできること、即ち計算、がこの「自然数」にできるかテストしてやらなくてはいけません。より具体的に言えば自然数を対象とする計算ができる関数、すなわちラムダ項、がラムダ計算の中でつくれるかを確かめるのです。そこでこの節ではまず「足す1」、「一般の加法」、「乗法」ができるかをテストしてやります。そしてこの章の終わりまでには四則演算が、さらにこの記事の最後までにはすべての自然数を対象としたプログラムが書けることをテストするのです。

ではまず「足す1」のテストから始めましょう。

これは種を明かしてしまった方が簡単なのでそうしてしまいます。「足す1」関数（後者関数、successorと呼ばれます）に対応するラムダ項はSuc=\lambda n.f.x.f(nfx)です。

実際に計算してみましょう。

(\lambda n.f.x.f(nfx) )(\lambda S.Z. S^nZ)\\\to_{1\beta} \lambda f.x. f((\lambda S.Z. S^nZ)fx)\\\to_{1\beta} \lambda f.x. f((\lambda Z. f^nZ)x)\\\to_{1\beta}\lambda f.x.f(f^nx)\\\to_\text{abbreviation}\lambda f.x.f^{n+1}x

（最後の変形はラムダ計算の体系内部での変換ではなく我々の略記に由来するものなので\to_\text{abbreviation}と書いた。）

となり、これは確かにn+1のコードである\lambda S.Z.S^{n+1}Zとα同値です。

では一般の加法はどうでしょう？

ここで自然数の「定義」を思い出してみましょう。自然数nとは「関数と初期値を受け取って初期値に関数をn回適用する高階関数」でした。そして加法というのは「足す1」の反復です。
つまり

Add=\lambda m.n.m\ Suc\ n

が加法関数になるのです。ここでSucは先の「足す1」関数で（先ほど名前を付けてあります）、あの関数をもう一度ここに書くのは、書く僕は面倒くさいだけ、読む皆さんは読みづらいだけで誰も得をしないので今後はこういう略記をよく使います。なおこの略記のせいで仮変数がかぶるみたいなことが若干心配になるかもしれませんが、そこは実在のプログラム言語でいう変数のシャドーイングをするようにラムダ抽象の定義を拡張したうえで、α変換でよろしくできるので大丈夫です。

では乗法はというとこれも同じ考え方です。乗法n\times mは0への「足すm」の反復適用です。そして「足すm」をつくるには？二章で学んだ部分適用が使えますね。即ち乗法は

Mul:=\lambda n.m.n\ (Add\ m)\ 0

となるのです。この方法を応用すれば指数関数、テトレーション…と作っていくことももちろん可能ですから演習問題代わりにやってみてください。

これでめでたく我々の自然数のコードは少なくとも加法と乗法が定義できる程度には自然数だという事がわかりました。

3.2 IsZero?述語とコードされたブーリアン、タプル

さて、我々が計算をしたいとき、扱いたいのは何も自然数だけではありません。

条件分岐やそれに伴う論理演算もまた計算に必要です。

そのためにはまずブーリアンの定義が必要なのですが次のようになります（これをここではコードされたブーリアンと呼ぶことにします）。

True:=\lambda F.S.F\\False:=\lambda F.S.S\equiv_\alpha 0

このブーリアンに対しても、先ほどの「自然数」と同様、我々が望ましいと思う性質を満たすかどうかの試験をせねばなりません。

我々がブーリアンに求めることと言えば、一にも二にもif式でしょう。

実はif式は大変簡潔な以下の表示を持ちます。

If:=\lambda\ bool.\ positive\text{-}case.\ negative\text{-}case.\ bool\ positive\text{-c}ase\ negative\text{-}case

実際に計算してみましょう。こんどはSucの時より少しだけ変形途中を飛ばすことにします（書く僕が面倒くさいので）。

If\ True\ P\ N\\\to_{\beta}(\lambda F.S.F)\ P\ N\\\to_{\beta}P

If\ False\ P\ N\\\to_{\beta}(\lambda F.S.S)\ P\ N\\\to_{\beta}N

（ここでP,Nはそれぞれラムダ項）

となり、確かにこれはif式です。

また、我々がブーリアンに求めるものには命題論理結合子もありますが、if文があれば命題論理結合子を作るのは容易ですから、それは省略することにします（\iff演習問題とします）。

我々がブーリアンに求めるものは、これらの他に何があるでしょう？そうです、算術の基本的な判定ですね、ゼロ判定、等号判定、大小判定ぐらいは欲しいところです。

ゼロ判定ができれば、あとで減法を作れば他の二つができますから（減法ができた後考えてみましょう。）、とりあえずゼロ判定を作りましょう。こうなります。

IsZero?:=\lambda n.n\ (\lambda x.False)\ True

これでなぜゼロ判定になるかわかるでしょうか？

まず、何度も言うようにこの世界ではnは「n回の反復適用を行う高階関数」ですから、もしnが0ならば、0回の反復適用、即ち初期値をそのまま返すことになり、初期値であるTrueを返します。

そして、反復適用するべき関数として渡している\lambda x.Falseは、引数によらずFalseを返す、いわゆるFalseへの定数関数ですから一度でも適用されればFalseになり、その後何度適用されてもずっとFalseを返すことになります。

これによってゼロ判定ができるのです。

さてこれでブーリアンについては（減法の後に回すということで棚上げした等号判定、大小判定を除いて）一通り説明したのですが、ここでお気づきの方はいるでしょうか？このブーリアン、ほとんどそのままタプルとも思えるのです。

その方法はこうです。

Cons:=Flip_2\ if\\\text{(where }Flip_i:=\lambda f.x.y_0.\cdots.y_{i-1}. f y_0\cdots y_{i-1}x\text{)}\\Car:=\lambda x. x\ True\\Cdr:=\lambda x. x\ False

僕はLispを書いていた時間が長いので、タプルのコンストラクタ、デストラクタの名前をLispのものにしていますが、意味論的に良い名前ではないのでお好きな名前で考えてください。またFlip_iの表記は自然数添え字iに対して、一般にこう定義するという意味です。これは多変数関数の第一引数を「後回し」にする、言い換えると引数を並べ替える高階関数です。Haskellの組み込み関数のflipはFlip_1に対応します。

このようにしてタプル型を得られることは、実際に計算してみてもわかりますが（演習問題とします。）、Trueの時とFalseの時の値をそれぞれ持っておくのがタプル型だと思えば自然なことだとも言えます。

（筆者からの注意: 次の段落以降急に難しくなったと感じる人がいるかもしれません。この記事はできるだけ大学の数学系や情報系なら1-2年次で習う程度の論理学や集合論の知識と、ほんの少しのコーディング経験があれば本筋を終えるように書くつもりだったのですが、ここから先はそもそも内容が難しいので、関数型プログラミングと手続き型プログラミングをどちらもある程度やったことがないと厳しいのかもしれません。）

そしてここで我々がタプル型を得たことは極めて重要です。というのも自然数が反復適用として定義されている現状、我々は事実上（自然数についての）forループ（もしくは知っている人向けに言えば原始再帰）を得ていることになるのですが、このforループ（原始再帰）はインデックスを使った処理が出来ないのです。しかしながらタプル型があれば我々は添え字と本命のアキュミュレータのタプルに関してループを回し、更新では添え字をSucしたものと本命の処理をしたアキュミュレータのタプルに更新するという方針によって、真のforループ（原始再帰）を得ることができるのです。

文章で書かれてもわかりにくいでしょうから、インデックスを使ったforループ（原始再帰）の簡単な例として階乗を計算するコードを書いてみましょう。こうなります。

Fact:=\lambda n.Cdr (n\ (\lambda x.(Cons\ (Suc(Car\ x) )\ (Mul\ (Car\ x)\ (Cdr\ x) ) ) )(Cons\ 1\ 1) )

これが確かに階乗計算になっていることは各自で確かめてください。方針は上に書いた通りです。このような方針で我々は一般にforループ（原始再帰）を得ることができるのです。

その他にも、タプルを得たことで、Lispのような方針でリストを扱うこともできますので、ここでタプルが手に入ったことは非常に表現力を引き上げているわけです*9。

3.3 減法

さてでは我々の主目的に戻って、Church数項が「自然数らしい」ことを確かめるために減法と除法をやっていきたいと思います。先にお断りしておくと、この記事でいう減法は\dot{-}と書かれることも多い演算で、第二引数が第一引数より大きいときも、マイナスにはならずに「0で止まる」（すなわちx\dot{-}y=\max(x-y,0)）減法です。

これから減法の定義をしたいのですが、減法は極めて難しく、定義を自分で考えだすことはおろか、正しい定義を見ても正しいと納得することも大変な感じです。この記事を書いている間に、ようやく筋の通った正当性の説明を見つけましたのでここでお話ししようと思います。とりあえずまず方針は以下の2ステップに分かれています。

  1. 「引く1」をする関数（前者関数、predecessorと言います）を作る。
  2. 1.をループさせる。

御覧の通り方針自体は加法を定義した時と同じなのですが、違うのは後者関数に比べて前者関数の構成が圧倒的に難しいことです。

とりあえずまず定義を見ましょう。

Pred:=\lambda n.[n\ \{\lambda f.If\ (IsZero?\ (f\ 1) )\ (\lambda m.m) (Compose\ Suc\ f)\} (\lambda l.0)]0\\\text{(where }compose:=\lambda f.g.x. f(gx)\text{)}

定義中の\{\},[]は、この後の説明のために強調の意味で()の代わりに使いました（つまりラムダ計算にとっては()として認識されていることにします。）。また、Composeは「（一変数の）関数合成」を意味しています。

さて、一見してこれが「引く1」だと納得できる人は恐らく、ほとんどというか、居ないと言っていいでしょう。即ちこの関数が「引く1」だという正当性の証明が必要です。

以降この関数に渡す引数をNとします。N=0のケースを考えてみましょう。このとき[]の中は反復適用の初期値になりますから、即ち\lambda l.0、つまりは0の定数関数になります。それに0を与えれば当然返り値は0です。

さて、ではN>0のケースはどうでしょう。これを考えるためには少しの逆算というか天下りというかを用いるのが楽です。すなわち[]内を計算した後、最終的にその結果に0を与えるとn-1になるようにしたいのですから、[]内は\lambda n.Suc^{N-1}n（と少なくともα同値）になるはずです。そう思って読むと…

一回目の\{\}内の適用では、If式は必ずTrue側に行きます。なぜならば初期値は0への定数関数だからです。True側には仮引数のfが出てきませんから、元の関数に関係なく[]内は\lambda m.m、即ち恒等関数になります。このことから翻ってPred\ 1=0がわかります。

そして二回目以降、N回目までの適用ではIf式は必ずFalse側に行きます。なぜならば数学的帰納法によってN-1回の反復適用の結果は\lambda n.Suc^{N-2}nになっているものとしてよいため、これに1を適用した結果は0にはなり得ないからです。そしてFalse側の処理は仮引数のfにSucを合成するものでしたから、結果は\lambda n.Suc^{N-1}nとなります。これは所望でした。

これによってあの突如出てきた関数が「引く1」だとわかったことになるのですが、納得いただけたでしょうか？

ちなみに余談ですが英語版wikipediaにはこれとほぼ同じ構成のPredが"Boolean"（記事中の言い回しでは"logic"）のところに乗っているのですが、日本語版はちょっとした工夫によってIf,IsZero?を使わずに同様の効果を得ているので、かえって難読コードと化しています。

ちょっとした自慢ですがComposeを一個の関数として切り出すのは僕のアイデアで、これで結構読みやすくなる気がしています。

さて、このとても大変な構成を終えてしまえば、本節の残りはウイニングランです。減法の定義は先に触れた通り加法と全く同じ

Sub:=\lambda n.m. m\ Pred\ n

で済みます。

また前節の「宿題」も片付けておきましょう。

\dot{-}の定義からn\leq mはx\dot{-}y=0と同値ですから、

Leq?:=\lambda n.m.Iszero?\ (n\ Sub\ m)

で、大小関係が定義できます。

さらに両向きの大小関係が成り立つことを等号とすれば等号判定、不等号が成り立ってかつ逆向きの不等号が成り立たないことを記述すれば狭義の不等号を手に入れることができるのです（ここで論理積と否定（下のコードではAnd,Notとして登場しています）が必要になります。これは演習問題としていましたが解けましたか？）。

Eq?:=\lambda n.m.And\ (Leq?\ n\ m)(Leq?\ n\ m)

Less?:=\lambda n.m.And\ (Leq?\ n\ m)(Not\ (Leq?\ n\ m))

3.4 有界探索と除法、残った課題

n未満の自然数で述語（:\iff返り値がTrueかFalseの関数）pを満たすもののうち最も小さいものを探索したい、というシチュエーションはよくあります。これは有界探索と呼ばれており、一般的な方法は次の関数を用います。

BoundedSearch:=\lambda p.n.n\ (\lambda m.If\ (p\ m)\ (Suc\ m)\ m)\ 0

これは前にも述べた通り、Church数項の自然数による反復適用が実質的にforループであることを考えれば理解しやすいかと思います。反復適用に使われている関数は、ある数m(\lt n)でp\ mが成り立たなければ引数を1大きくし、成り立てば引数をそのまま返すので、ループするたびにp\ mが成り立つようなmが見つかるまでは引数が増大していき、一度見つかったらそれ以降は変わらないわけです。もしも、そのようなn未満の自然数が発見できなければ、値はnまで増加することになりますから、もし返り値がn未満の自然数でなくnになっていたら「探索失敗」を意味するわけです。

この有界探索を知っていれば除法は極めて容易です。割る数が0でない、自然数による除法の商はかならず割られる数以下なので

Div:=\lambda n.m.If (IsZero?\ m)\ 0\ (BoundedSearch\ (\lambda l.(Less? (Sub\ n\ (Mul\ m\ l) ) m) n)

これでn-m\times lがmを下回る最小の自然数、即ち定義よりnをmで割った商が計算できます。（mが0の時通常の除法は定義されませんので仮に0を返すようにしてあります。またm=1だとn未満には商がないのですがその時はnを返すことになっていましたから、やはり問題ありません。）

商ができてしまえば余りはもっと簡単で割られる数から割る数と商をかけたものを引くだけです。

Rem:=\lambda n.m.Sub\ n\ (Mul\ m\ (Div\ n\ m) )

こうしてついに我々は四則演算全てを手に入れたのです。

ここまでの我々の成功とこの過程で得た大量の副産物から、「これだけあれば普通にプログラムできるじゃん」と思われる方も多いと思います。実際ここまでのコーディングテクニックを応用すれば、相当多くのものが手に入るのは間違いないのですが、一つだけ我々がまだ得ていないものがあります。それは再帰呼び出し、あるいはwhileループに対応するものです。

実はTuring完全性には一章で述べた定義のほかに非形式的な判定基準があり、

  1. If文に対応する構造
  2. while文、もしくは再帰呼び出しに対応する構造
  3. ごく基本的な算術演算（ここに何が必要かは体系によって微妙に変わります。）

が備わっていればTuring完全になるという基準が存在します（これはKleeneの公理化された再帰関数について少し知ると妥当であるとわかります。）。

このうち我々にはまだwhile式,、より一般に再帰呼び出しがないのです。

この再帰呼び出しを見つけるために次章に進みます。

4. 無制限再帰

4.1 不動点コンビネータと無制限再帰

我々の目的を達成するためには不動点コンビネータと呼ばれるラムダ項Rを手に入れれば十分です。これは全てのラムダ項fに対して、

Rf=_\beta f(Rf)(=_\beta f(f(Rf) )=_\beta\cdots)

を満たすRを言います。どうして不動点コンビネータというのかと言えばfを関数、Rを高階関数と見た時、これはx=_\beta fxであるようなx、つまり関数fの不動点をfから生成しているように見えるからです。

より重要かつ難しいのは、どうしてこのようなRがあれば再帰呼び出しが実装されたと言えるかという点です。

これは実装を見ながら説明しましょう。

上で我々は既にforループによる階乗を得ていますが、例の簡明さのために再び階乗を、今度は再帰呼び出しで作ることを目標にしましょう。

まず何も考えずに書けば

Fact1:=\lambda x.(If\ (Iszero?\ x)\ 1\ (Mul\ x\ (Fact1\ (Pred\ x) ) ) )

となりますが、ラムダ計算の定義にこのような「名前による再帰」は含まれていないのでこの定義はこのままではラムダ計算による関数定義になりません。

そこで一旦右辺のFact1をλ抽象したものを考えます。即ち

Fact1!:=\lambda Fact1!.(\lambda x.(If\ (Iszero?\ x)\ 1\ (Mul\ x\ (Fact1!\ (Pred\ x) ) ) ) )

とを考えます。

後はどうにかして「Fact1!の第一引数に自分自身を代入し、しかもその突っ込まれた第一引数としての自分自身の第一引数にも自分自身が代入されており…」という状況を作れれば目的達成となるのですが、これを達成するために先の不動点コンビネータを用いるのです。

つまりここでR\ Fact1!を考えます。すると

R\ Fact1!\\=Fact1!(R\ Fact1!)\\=Fact1!(Fact1!(R\ Fact1!) )\\=\cdots

となり、即ちFact1!の第一引数にFact1!が代入されているのですが、その第一引数にもFact1!が代入されており…となっており、所望の状況を得たことになります。

しかし…これで納得できる人はいるのでしょうか？ちょっと難しすぎますね。

もう少し簡単な例で考えてみましょう。今度はリストを（左から）潰す関数、普通のプログラム言語でいうとreduceやfold-light(foldl)と呼ばれるような関数を作ってみましょう。

まず先ほどと同じように普通に再帰で書くと

Reduce:=\lambda list.f.start.\ (If\ (Null?\ list)\ start\ (Reduce\ (Cdr\ lst)\ f\ (f\ start\ (Car\ acc) ) ) )

となります。これを先ほどと同じように処理すれば

Reduce!:=\lambda Reduce!.list.f.start.\ (If\ (Null?\ list)\ start\ (Reduce!\ (Cdr\ lst)\ f\ (f\ start\ (Car\ acc) ) ) )\\Reduce:=R\ Reduce!

となります。

ここでもう一度何が起きているのか考えてみましょう。

Reduceは受け取ったリストが空でなかった場合、ある処理（つまりこの後使う引数の計算）をした後、ある引数で自分自身を呼び出そうとします。

つまり比喩的に言えば、Reduceは引数の計算という仕事をした後、残りの仕事を誰か（といっても自分自身なのですが）に委任するようになっています。自分自身が現れる部分を仮引数に置き換えたReduce!では、代わりに引数に受け取った何かしらの関数を呼び出そうとする、比喩でいえば自分自身ではなく本当に他人に残りの仕事を委任しようとするわけです。

しかしR\ Reduce!を考えれば、不動点コンビネータの性質により、仮引数（仕事の委任先）は自分自身（の仮引数（委任先）にさらに自分自身が代入されて…なもの）になるわけです（知っている人向けに言えば継続渡し形式の継続として自分自身を、そのまた継続としてさらに自分自身を…呼び出したことになります。）。

僕が二つ目の例を挙げた理由は、第一の例では自分自身を呼び出した後にnを掛けるという処理が続いており（つまり末尾再帰になっておらず）、本質が見えにくいかと思ったからです。

もしあなたがこのような不動点コンビネータによる再帰に初めて触れるなら、この節の説明が全く理解できなかったとしてもむしろ当然のことです。僕もこれが直観的に納得できるようになるまでずいぶん時間がかかりました。しかしとりあえずそのようなラムダ式を得る方法だけは簡単に覚えることが出来ます。再帰を使ったラムダ式を書いたならば、再帰に使った自分の名前を一番外側でλ抽象して仮引数にし、最後にそれをRに適用すればそれで出来上がりです。

もし、継続という概念は知っているが、不動点コンビネータ周りがずっと腑に落ちていなかったという方がいらっしゃれば、この節の括弧内で触れたように不動点コンビネータは継続渡しに自分自身を与えてくれるものだと考えると少なくとも末尾再帰についてはすっきり理解できるはずです。末尾再帰でない場合には、継続が複雑化（自分自身と他の関数の合成が継続となる）しますが、その場合でも継続渡しに少なくとも渡す継続として自分自身が選択可能であるという状況を作り出すものだと考えると考えやすいと思います。

ではこの節の最後にこの節ではずっとRと書いてきた不動点コンビネータがラムダ項として実在することを示します。実際には無限に多くのこのような例があることが知られていますが、ここでは最も簡単なものを紹介します。

R:=\lambda f.(\lambda g.f(gg) )(\lambda g.f(gg) )

これにはCurryのYコンビネータという名前がついています。これが不動点コンビネータであることを確かめてみましょう。

RF\\\to_{\beta 1}(\lambda g.F(gg) )(\lambda g.F(gg) )\\\to_{\beta 1}F( (\lambda g.F(gg) )(\lambda g.F(gg) ) )\\\leftarrow_{\beta 1}F(RF)

これにより、めでたく我々は再帰的な定義をする方法を手に入れたのです。

4.2 無限ループへの対処、定義の明確化

ここまでで皆さんは「ラムダ計算でコーディング」するのに必要な技術を本質的には全て知ったことになります。後は通常のプログラミング言語でのコーディングの知識や経験と多少の思索があれば、本質的には通常のコンピュータができることを何だってラムダ計算の上ですることが出来ます。例えばラムダ計算の上でラムダ計算のインタープリタを書くことも原理的には可能です（それなりに大変でしょうけど）。

ではなぜこの記事が続いているかというと実は前節の不動点コンビネータはここまでにない新たな状況を生じさせているからです。

それは何かというと前節でCurryのYコンビネータが不動点コンビネータであることを示したとき、

RF\to_{\beta 1}(\lambda g.F(gg) )(\lambda g.F(gg) )\\\to_{\beta 1}F( (\lambda g.F(gg) )(\lambda g.F(gg) ) )\\\leftarrow_{\beta 1}F(RF)

としましたが、ここで二行目の式はまだβ1簡約出来ます。できる限りβ1簡約を続けようとすれば

RF\to_{\beta 1}(\lambda g.F(gg) )(\lambda g.F(gg) )\\\to_{\beta 1}F( (\lambda g.F(gg) )(\lambda g.F(gg) ) )\\\to_{\beta 1}F(F( (\lambda g.F(gg) )(\lambda g.F(gg) ) ) )\\\to_{\beta 1}F(F(F( (\lambda g.F(gg) )(\lambda g.F(gg) ) ) ) )\\\to_{\beta 1}\cdots

となり、Fが増えていくばかりで簡約列が止まらないことがわかります。これは実際にはCurryのYコンビネータだけでなく、不動点コンビネータに共通の性質になるのは不動点コンビネータの定義式に類似の無限列が出現していたことからわかると思います。

このことからこんなことがわかります。

実際には、例えばR\ Fact1!\ nは正規形を持ち、それがn!であるのは前節でみた通りですが、そのような「意図した答え」に簡約されるのは「うまい順序で簡約したとき」に限るのです。なぜならばR\ Fact1!の部分を簡約し続ける限り、先ほどと同じ無限ループに陥るからです。

そこで我々が最初にβ変換をしてくれる誰かさんとした約束「一つでも標準形を持つならば、それに簡約してくれ」というのが生きてくるのです。この約束の上では上記のような心配はいらず、我々の欲しい結果にラムダ項は簡約されます。ここには一つ問題があり、「『標準形があるならばそれになるような簡約』というのを簡約してくれる誰かさんはどうやって知るのか？」ということです。「誰かさん」が神様の場合ならばいいでしょうが、多くの我々は神と交信する手段を持たないので、β簡約を実際に行ってくれるのは大抵はコンピュータであり、コンピュータは今行っている方針で簡約が終わるのかどうか判断する手段を持ちません。しかし実は以下のようなことが知られています。

Def.5.1 最左最外戦略とはβ簡約の手順を定義するものであり、関数適用があればその左側に着目し、構文木上もっとも浅いβ簡約基から簡約するような手順である。

Fact.5.2 対象となるラムダ項に一つでも正規形が存在すれば、それに最左最外戦略で到達できる。

これらにより、実はコンピュータにも上記のような「依頼」をすることが出来ることがわかるのです。

Fact5.2の証明はここでは扱わないのでHenk P. Barendregt, ”The Lambda Calculus, its Syntax and Semantics''などをお読みください。

実際には多くのプログラム言語のインタープリタやコンパイラは最左最外戦略で簡約するわけではないので、そのような状況ではより複雑なことが起きます。実は不動点コンビネータの選び方によって意図したとおりに簡約されたりされなかったりするのです。しかし我々は現在理論的な興味でラムダ計算を扱っているので、このあたりの話題には深入りしません。ともかく、簡約してくれる誰かさんに一つでも正規形があればそれに簡約してもらうことにし、特に誰かさんがコンピュータの場合であってもこれが可能であるという点を指摘するだけにとどめます。

またここで「ラムダ計算でコーディング」したことで我々が実際に何を得たのかを明確にするため、ラムダ計算における関数や値についてをキチンと定義してみましょう。というのもこのようにβ標準形で表示できない関数が出現したことで、我々は少しラムダ計算の中での「関数」や「値」という概念について注意深くなる必要があるからです。我々は関数に値を適用して計算した結果の値についてはβ標準形であることを要求しているため、関数はβ標準形で書けないこともあるというのは若干片手落ちな気もしてしまうからです（実際前章までに定義した関数はβ標準形になっているか、何段階か簡約すればβ標準形になるようになっていました。もしよければ名前による略記をそれが表すラムダ項に置きなおして計算してみてください）。さらに言えば最初のほうで計算モデルにおける関数は「値がないこと(\uparrow)」も許していることについて述べましたが、まだラムダ計算において定義された関数の値がないとはどういうことかも定義していませんでした。お察しの通りこれがまさに標準形がないことなのですが、それについても定義しておく必要があるでしょう。

このように定義しましょう。

Def 5.3

  • ラムダ計算における値とは、β標準形の事である。
  • ラムダ計算における関数とは「ラムダ項」と「『意図した入力』となる標準形のラムダ項の集合」のペアの事である。
  • ラムダ計算における述語とはラムダ計算における関数であって、それが意図した入力を適用されて、かつ正規形に簡約されるならばその値がTrueかFalse（とα同値）になることである。
  • ラムダ計算における関数Fが入力Aで値を持たない（\uparrow）とは、FAが正規形を持たないことである。
  • ラムダ計算において関数Fが自然数値部分関数fを表現するとは、Fの意図した入力がチャーチ数項を含み、Fにチャーチ数項としてのnを与えた項Fnが正規形を持つこととnがfの定義域に属することが同値で、かつFnが正規形を持つ限りその正規形はf(n)をチャーチ数項として表現したものと（α同値の意味で）同じになることである。
  • ラムダ計算において関数Pが自然数値部分述語pを表現するとは、Pの意図した入力がチャーチ数項を含み、Pにチャーチ数項としてのnを与えた項Pnが正規形を持つこととnがpの定義域に属することが同値で、かつPnが正規形を持つ限りその正規形はp(n)をコードされたブーリアンとして表現したものと（α同値の意味で）同じになることである。
  • ラムダ計算において関数（述語）Fが全域であるとは、FにFのどの意図した入力を適用した結果も標準形を持つことである。

（「意図した入力」という言葉が新たに出てきましたが、これは我々が今まで作ってきた多くは自然数値関数を表現するラムダ項に、もしも自然数でないラムダ項を適用すれば、その結果は全く予測できない、という事態に対処するためです。これは本来は今回の記事では扱わない型付きラムダ計算と呼ばれる体系で対処するべきことなのですが、ここでは便宜上このように定めておきます。個々の関数に対して「意図した入力」となる集合を実際に記述しようと思うと、それはほとんど型付きラムダ計算を導入するのと同じことになるので、ここでは第五、第六の定義から自然数値関数をプログラムする際には意図した入力は自然数のスーパーセットである必要がある、という事だけを指摘しておきます。）

この定義によって、値と関数を区別されたことで我々は関数の表現がβ標準形で書けないことに後ろめたさを感じずに済み、また値がないというプログラミング的な状況を標準形がないことだとして数学的に取り扱うことが出来るようになったわけです。

長々とお付き合いありがとうございました。これにてようやく「ラムダ計算でコーディング」は全編終了です。最後に定義が出てくるという数学としては珍妙なスタイルになりましたが、ラムダ計算で「実際にコーディングをする」ことを重視した結果なのでどうかご容赦いただければと思います。

6. 謝辞など

Twitter:@hennin_Itn いつも議論相手になって頂いています。参考文献の中にあるラムダ計算インタープリタも彼の作。
Git Hub:github.com/tani 僕に継続を教えてくれたり、下の参考になるブログを教えてくれたりした方。
リアル同研究室の皆様 普段のゼミがこの記事を書くモチベーションになったり、細かいながら定義次第でバグりがちなところの相談に乗ってもらったり。

7. 参考文献など

Benjamin C. Pierce著: Types and Programming Languages
J. Roger Hindley著:Basic Simple Type Theory
Henk P. Barendregt著:The Lambda Calculus, its Syntax and Semantics

日Wikipedia:

ラムダ計算(https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97#)

計算モデル(https://ja.wikipedia.org/wiki/%E8%A8%88%E7%AE%97%E3%83%A2%E3%83%87%E3%83%AB)

英Wikipedia:

Lambda calculus(https://en.wikipedia.org/wiki/Lambda_calculus)

Model of Computation(https://en.wikipedia.org/wiki/Model_of_computation)


@hennin 作ラムダ計算インタープリタ（リンク先→REAdME.md→WebREPLからブラウザ上でも使えます）https://github.com/utatatata/untyped-lambda-calculus

*1:これが普通の（集合論的な）意味での関数、述語の等しさでした

*2:この節で出てくるエミュレータの定義は実はまさにそうで、外延的に同じ関数が異なる定数に移されることを認めないといろいろとうまくいかないことが知られています。

*3:「自然な」といったのは特に1.1節で書いた計算モデルの（非形式的な）共通点のうち、2.や3.をわざと失わせ、人間や既存のコンピュータにできそうにないほど複雑な操作（e.g. プログラムの停止性の判定、真の乱数の生成、無限回ステップの繰り返し…etc）を加えた計算モデルを考えることもあるからです。オラクル付き計算モデルなどと呼ばれることもあるこれらは、ある意味当然ですが、この先で説明する一種の「限界」を突破することができます。

*4:多くのプログラム言語で無名関数を定義するときに使われる"lambda"や"\"というキーワードはここに端を発しています。

*5:完全に余談ですがはてなブログは"(("や"))"を脚注の記法だと思って読んでしまうので、僕はエスケープシーケンスを使ったり、間にスペースを入れるなどの対策をしなくてはならず、普通にLaTeXで同じものを書くのに比べてさらに五割増しぐらいで大変です

*6:形式的な定義の一つ（節の後半でいうところの1.の変数捕捉回避のアプローチ）は以下のようになる。 1.x[x\leftarrow T]=T\\2.y[x\leftarrow T]=y\ (\text{$x\neq y$の時。})\\3.(UV)[x\leftarrow T]=(U[x\leftarrow T])(V[x\leftarrow T])\\4.(\lambda y.U)[x\leftarrow T]=\lambda y.U[x\leftarrow T](\text{$x\neq y$かつ$x$は$T$の自由変数でない時。})\\5.(\lambda x.U)[x\leftarrow T]=U\\6.(\lambda y.U)[x\leftarrow T]=\lambda z.( (U[y\leftarrow z])[x\leftarrow T])\\(\text{$x\neq y$かつ$x$が$T$の自由変数である時。ここで$z$は$T$の自由変数でも$U$の自由変数でもないような変数から任意に取る。})

*7:実はもう一つ「η同値」と呼ばれる同値があるのですが、これがなくともラムダ計算の体系としてTuring完全になるためここでは扱いません

*8:といってもうまくやればα変換を回避する実装上の工夫も存在します。興味のある方はNameless Lambdaやde Bruijn indexでググってみてください

*9:この記事ではリスト処理について詳しくはやりませんが、例えば空リストをFalseで表し、Listについて、Listへの要素の追加を\lambda x.Cons\ x\ List、先頭要素の取り出しをCar\ List、先頭要素を取り出した残りのリストをCdr\ Lispとするなどして、以降はLisp言語でのコーディングテクニックに合流しますので、SICP（参考文献参照）などを参考にしてください。この時、Lispに標準的に備わっている機能のうち、リストの空判定のみ明らかでありませんが、Null?:=\lambda list.list\ (\lambda x.y.\lambda z. False)\ True)で与えらます（λが連続したときの略記を一部しか使っていない理由は、正当性を実際に計算して確かめてみればわかります。）。