ラムダ計算キホンのキ
はじめに
はじめまして。記事を開いていただきありがとうございます。
これからラムダ計算という形式体系について、基本的な定義を紹介していこうと思います。
ラムダ計算とは、コンピュータが行う「計算」概念を数学的に捉えた種々ある計算モデルの一つであり、関数を基礎として種々の概念を関数として表現するモデルとなっております。
定義自体はプログラミング言語と呼ぶには驚くほど簡素なものですが、その一方で自然数やブール値、if文、リストなど様々な概念を関数として表現する表現力を備えております。
特に、一部の自然数上の関数は(適切な表現方法を定めることで)ラムダ計算の中で表現することが出来るのですが、そのような自然数上の関数のクラスは計算可能な関数と呼ばれるクラスとぴったり一致することが分かっており、その意味でラムダ計算はチューリング完全な計算モデルと呼ばれることがあります。
本記事では、ラムダ計算の初歩的な定義について紹介できればと思っており、やる気があれば続編となる「ラムダ計算キホンのホ」にてCR性や最左戦略による正規化定理、標準化定理などの重要な定理を紹介できればと思っております。
よろしくお願いします。
ラムダ計算とは(インフォーマルな説明)
まずは、ラムダ計算という言葉を初めて聞く人向けにインフォーマルな説明を行います。
ラムダ式について
次のいずれかの形の文字列をラムダ式と言います。
(ラムダ式を
- 変数:
x, y, z... - 関数抽象:
\lambda x.M - 関数適用:
MN
例:ラムダ式の例
x xy \lambda x.xy (\lambda x.x)y \lambda y.(\lambda x.xy)
関数抽象
例えば、
特に、JavaScriptを書いたことがある人ならば、このような記法はアロー関数 x => 2*x + 1
として親しみがあるかもしれません。
今まで単に
そこで、
(ラムダ記法の他にも、
続いて関数適用[1]
例として、 (x => 2*x + 1)(3)
となります。
自己適用もアリなの?
ラムダ式の定義に従えば、
こんな訳わからん形を許容するせいで「任意の関数が不動点を持つ」みたいな訳わからん計算体系になってしまいますが、領域理論を用いればそのような訳わからん体系も上手く捉えることができ面白くなります。
適切な型を導入し、単純型付きラムダ計算STLC (Simply Typed Lambda Calculus)を考えることで上述の事故は防ぐことはできますが、その分計算力が落ちてしまうことには注意が必要です。
型を導入しつつも、さらに再帰的定義を許した計算体系PCF (Programming Computable Functions)まで拡張すれば、チューリング完全性を取り戻すことができます。
ちなみに、型無しラムダ計算は全ての式が単一の型U
を持つ型付きの体系とみなすこともでき、私は「型無しラムダ計算はSTLC (Singly Typed Lmabda Calculus)である」とか訳わからんことを主張しています。
(意味論を考えるときも全てのラムダ式を反射的対象
束縛変数と自由変数
ラムダ式
例として、
束縛変数の概念自体は高校数学まででも馴染みがあり、積分
その際、束縛変数の名前は何でもよいという共通認識を私達は持っており、
このような同一視をラムダ計算の文脈では
「束縛変数かつ自由変数」となる変数
これは各変数を変数名とか言う非本質で区別することにより起きる事故であって、通常は各変数を出現と呼ばれる変数の現れる位置によって区別をし、自由な出現や束縛された出現といった言葉を用います。その上で必要に応じて変数名で区別をします。
(※de Bruijn Indexの話ではありません。)
ところで、自由変数の値はいつ定まるのでしょうか。
本記事では深入りはしませんが、意味を定めるときに環境と呼ばれる各自由変数の値のリストを入力値として受け取った際に自由変数の値が定まります。
すなわち、
このような意味論を扱う文脈では、
束縛変数が関数の引数なんじゃないの?
前者はまさに「
JacaScript風に書けば、前者はx => 2*x + 1
であり、後者は() => (x => 2*x + 1)
となります。
また、型付きラムダ計算では各変数はその型に対応する(構造を持った)集合の要素として解釈され、
型無しラムダ計算では全てが単一の型U
を持っていたため、各変数はすべて型U
に対応する「何らかの集合
(この
\beta -簡約について
ラムダ式
ラムダ計算においては、評価方法も厳密に定まっており、
型無しラムダ計算においては
左の式の
すなわち、以下のように一生同じ形が繰り返され、計算結果が求まることはありません。
ラムダ計算の諸定義
ここからはラムダ計算の諸定義をフォーマルに説明していこうと思います。
部分式と出現
まず、ラムダ式の定義を行います。
定義1: ラムダ式
アルファベットを
また、
変数の定義変じゃない?
あらかじめ変数の可算集合
そこで、変数の集合
以降では簡単のため、変数の記号として
また、カッコも適宜混乱のない範囲で省略をし、関数適用は左結合とします。[4]
続いて、部分式と出現の定義を行います。
定義2: 部分式
ラムダ式
\mathrm{sub}(x)=\{x\} \mathrm{sub}(M_1M_2)=\mathrm{sub}(M_1)\cup\mathrm{sub}(M_2)\cup\{M_1M_2\} \mathrm{sub}(\lambda x.M_0)=\mathrm{sub}(M_0)\cup\{\lambda x.M_0\}
ラムダ式
部分式は下記のような木構造を成します。
図1.
部分式の成す木構造において、各部分式の出現位置を考えます。
上記の例では、部分式
すると、左側の変数
定義3: 出現位置
ラムダ式
(ただし、
\mathcal{O}(x)=\{\epsilon\} \mathcal{O}(M_1M_2)=(1\cdot\mathcal{O}(M_1))\cup(2\cdot\mathcal{O}(M_2))\cup\{\epsilon\} \mathcal{O}(\lambda x.M_0)=(0\cdot\mathcal{O}(M_0))\cup\{\epsilon\}
また、
定義4: 出現
ラムダ式
-
のときu\equiv\epsilon
M/\epsilon\equiv M -
のとき(u\equiv i\cdot v )i\in\{0, 1, 2\}
M/i\cdot v\equiv (M/i)/v
ただし、
(
ラムダ式
ただし、以降では簡単のため出現位置を省略して書くこととします。
これで変数の出現について、自由な出現・束縛された出現を定義することができます。
先程の例で言えば、
また、
定義5: 自由な出現・束縛された出現
ラムダ式
-
かつ\mathrm{Free}(u, M)\iff M/u\in V \forall v<u\in\mathcal{O}(M), \lambda(M/v)\not\equiv M/u -
かつ\mathrm{Bound}(u, v, M)\iff M/u\in V かつ\lambda(M/v)\equiv M/u where\mathrm{Free}(u', M/v\cdot 0) u\equiv v\cdot 0\cdot u'
ただし、
また、これらの定義を用いることで自由変数と束縛変数もそのまま定義できます。
\mathrm{FV}(M)=\{M/u\mid\mathrm{Free}(u, M)\} \mathrm{BV}(M)=\{M/u\mid\exists v\in\mathcal{O}(M), \mathrm{Bound}(u, v, M)\}
\alpha -同値関係と代入
ラムダ式
ただし、代入では変数の補足に注意をする必要があります。
例えば、積分の例において、
そういう代入操作を考えるのはダメなの?
上述の素朴な定義だと、以下のように「代入してから計算」と「計算してから代入」の結果が一致しないためあまりよろしくありません。
- 代入してから計算:
\frac{x^3}{3}+\frac{x^2}{2}+C - 計算してから代入:
x^3+\frac{x^2}{2}+C
このような代入と計算の可換性の他にも、代入と意味の可換性や代入補題などきちんと定義された代入操作にはきれいな性質がいくつかあり、変数名の置き換えがとても重要になります。
ちなみに前者2つも代入補題と呼ばれることがありますが、私は認めていません。(?)
そこで、
すなわち、freshな変数
定義6: 代入
ラムダ式
y[N/x]\equiv\left\{\begin{array}{ll}N & \text{ if }x\equiv y \\ y & \text{ if }x\not\equiv y\end{array}\right. (M_1M_2)[N/x]\equiv (M_1[N/x])(M_2[N/x]) (\lambda y.M_0)[N/x]\equiv\lambda z.(M_0[z/y][N/x])
ただし、最後の
(
同時代入の定義
逐次代入
例:
- 逐次代入:
(x(xy))[vy/x][w/y]\equiv vy(vyy)[w/y]\equiv vw(vww) - 同時代入:
(x(xy))[vy, w/x, y]\equiv vy(vyw)
-
のときx_{n+1}\not\in\mathrm{FV}(N_1\ldots N_n)
M[N_1, \ldots, N_{n+1}/x_1, \ldots, x_{n+1}] := M[N_1, \ldots, N_n/x_1, \ldots, x_n][N_{n+1}/x_{n+1}] -
のときx_{n+1}\in\mathrm{FV}(N_1\ldots N_n)
M[N_1, \ldots, N_{n+1}/x_1, \ldots, x_{n+1}] := M[y/x_{n+1}][N_1, \ldots, N_n/x_1, \ldots, x_n][N_{n+1}/y]
(ただし、
代入の定義の3つ目の正当性を確かめるために、
\alpha -同値関係
定義7: 二項関係
-
-変換\alpha
- 部分式の規則
- 同値関係の規則
例: \alpha -同値なラムダ式
\lambda x.x=_\alpha\lambda y.y -
\lambda x.\lambda y.xy=_\alpha\lambda y.\lambda x.yx - (証明):
\lambda x.\lambda y.xy=_\alpha\lambda y.(\lambda y.xy)[y/x]\equiv\lambda y.\lambda z.yz=_\alpha\lambda y.\lambda x.yx
- (証明):
x(\lambda x.x)=_\alpha x(\lambda y.y) \lambda x.xy\not=_\alpha\lambda y.yy
ここで、代入操作の定義の正当性は以下の命題8によって保証されます。
\alpha -同値関係の両立性
命題8: 代入とラムダ式
証明
この定理に関して、私は真に驚くべき証明を見つけたが、この余白はそれを書くには狭すぎるので300年後に追記します。
そこで、以降では
すなわち、
すると、束縛変数名は好きに思ってよくなるため代入の定義が以下のように修正されます。
定義9: 代入(修正版)
ラムダ式
y[N/x]\equiv\left\{\begin{array}{ll}N & \text{ if }x\equiv y \\ y & \text{ if }x\not\equiv y\end{array}\right. (M_1M_2)[N/x]\equiv (M_1[N/x])(M_2[N/x]) -
(\lambda y.M_0)[N/x]\equiv\lambda y.M_0[N/x] とした(y\not\in\mathrm{FV}(N) )
代入に関しての重要な性質の一つに、代入補題があります。
命題10: 代入補題
ラムダ式
証明
-
のときM\equiv x
-
のときM\equiv y に注意(x\not\in\mathrm{FV}(L) )
-
のときM\equiv z )(z\not\equiv x, y
-
のときM\equiv M_1M_2
-
のときM\equiv\lambda z.M_0 とする(z\not\in\mathrm{FV}(NL) )
ちなみに、
例:代入補題の反例
(\lambda\texttt{v}'. \texttt{v})[\texttt{v}''/\texttt{v}][\texttt{v}'''/\texttt{v}']\equiv(\lambda\texttt{v}'.\texttt{v}'')[\texttt{v}'''/\texttt{v}']=\lambda\texttt{v}.\texttt{v}'' (\lambda\texttt{v}'. \texttt{v})[\texttt{v}'''/\texttt{v}'][\texttt{v}''/\texttt{v}]\equiv(\lambda\texttt{v}'.\texttt{v})[\texttt{v}''/\texttt{v}]\equiv\lambda\texttt{v}'.\texttt{v}''
\beta -変換
このような「計算」のことを
この
\beta -変換
定義11: 二項関係
-
-変換\beta
- 部分式の規則
最後に、代入と計算の可換性、つまり、「計算してから代入した結果」と「代入してから計算した結果」が一致することを証明して終わります。
命題18: 代入と計算の可換性
ラムダ式
証明
規則帰納法で示す。
-
のとき\frac{}{(\lambda y.M_1)M_2\to_\beta M_1[M_2/y]} とする(y\not\in\mathrm{FV}(L) )
-
のとき (もう一方も同様)\frac{M_2\to_\beta N_2}{L_1M_2\to_\beta L_1N_2}
-
のとき\frac{M_0\to_\beta N_0}{\lambda y.M_0\to_\beta \lambda y.N_0} とする(y\not\in\mathrm{FV}(L) )
おわりに
お疲れ様でした。ここまで読んでいただきありがとうございました。
ラムダ計算は厳密に扱おうとすればするほど沼にハマっていくような分野ですが、その分簡単そうな定義にも深みがあって面白いと思います。
また、以下の記事で紹介するBöhm木やhnfの話は、これを知らずに型無しラムダ計算を学んだことがあると主張するのは無理があるレベルで基本的かつ重要な事柄だと思いますので、ぜひ合わせて読んでいただけると嬉しいです。
改めて、本当にありがとうございました。
参考文献
(Barendregtの『The Lambda Calculus: Its Syntax and Semantics』にこの宇宙のすべてが載っています。当然私は全く読めていません。)
-
井田哲雄(1991)『計算モデルの基礎理論』岩波書店.
-
高橋正子(1991) 『計算論 計算可能性とラムダ計算』近代科学社.
-
林晋・小林聡(1991)『構成的プログラミングの基礎』遊星社.
-
横内寛文(1994)『プログラム意味論』共立出版.
-
大堀淳(1997)『プログラミング言語の基礎理論』共立出版.
-
星野直彦 (2013) 『型無しラムダ計算とモデル』(PDF), 取得元 (アクセス日: 2024年10月1日)
-
B. C. Pierce (著), 住井英二郎 (監訳), 遠藤侑介・酒井政裕・今井敬吾 (翻訳) (2013) 『型システム入門 −プログラミング言語と型の理論−』オーム社.
-
G. Winskel (著), 末永幸平 (監修・翻訳), 勝股審也・中澤巧爾 (翻訳) (2023) 『プログラミング言語の形式的意味論入門』共立出版.
-
H. P. Barendregt (1984) "The Lambda Calculus: Its Syntax and Semantics," North-Holland.
-
H. Barendregt (1992) "Lambda Calculi with Types," Handbook of Logic in Computer Science, Volume 2, Oxford University Press.
-
B. Jacobs (1997) "A Tutorial on (Co)Algebras and (Co)Induction," EATCS Bulletin, 62, 222-259.
-
R. Amadio, P.-L. Curien (1998) "Domains and Lambda-calculi," Cambridge University Press.
-
M. H. Sørensen, P. Urzyczyn (2006) "Lectures on the Curry-Howard Isomorphism," Elsevier Science.
-
J. R. Hindley, J. P. Seldin (2008) "Lambda-Calculus and Combinators, an Introduction," 2nd Edition, Cambridge University Press.
-
関数適用
では、「関数MN をM に適用する」という言葉の使い方をします。 ↩︎N -
便宜的に
を「関数」と読んでいますが、定義上M の形でない式を適用しても構いません ↩︎\lambda x.M' -
のような形も見ますが、個人的にx\vdash 2x+1 の左には導出の仮定を起きたいため好きではありません。 ↩︎\vdash -
右結合・左結合は構文の定義ではなく、略記規則の一つであることに注意。『計算モデルの基礎理論』(井田)のp. 73には略記規則の厳密な定義があります。 ↩︎
-
は木領域という構造を成します。(c.f.『計算モデルの基礎理論』(井田)p.77) ↩︎\mathcal{O}(M) -
最後の
の条件は、\mathrm{Free} のようなケースのためです。 ↩︎\lambda x.x(\lambda x.x) -
-同値の定義に関連してNominal Setという話があるらしく、いつか勉強してみます。 ↩︎\alpha -
さて、本当に勝手にこんなことをしてもよいのでしょうか? ↩︎
Discussion