🦔

ラムダ計算キホンのキ

2025/01/23に公開

はじめに

はじめまして。記事を開いていただきありがとうございます。
これからラムダ計算という形式体系について、基本的な定義を紹介していこうと思います。

ラムダ計算とは、コンピュータが行う「計算」概念を数学的に捉えた種々ある計算モデルの一つであり、関数を基礎として種々の概念を関数として表現するモデルとなっております。

定義自体はプログラミング言語と呼ぶには驚くほど簡素なものですが、その一方で自然数やブール値、if文、リストなど様々な概念を関数として表現する表現力を備えております。

特に、一部の自然数上の関数は(適切な表現方法を定めることで)ラムダ計算の中で表現することが出来るのですが、そのような自然数上の関数のクラスは計算可能な関数と呼ばれるクラスとぴったり一致することが分かっており、その意味でラムダ計算はチューリング完全な計算モデルと呼ばれることがあります。

本記事では、ラムダ計算の初歩的な定義について紹介できればと思っており、やる気があれば続編となる「ラムダ計算キホンのホ」にてCR性や最左戦略による正規化定理、標準化定理などの重要な定理を紹介できればと思っております。

よろしくお願いします。

ラムダ計算とは(インフォーマルな説明)

まずは、ラムダ計算という言葉を初めて聞く人向けにインフォーマルな説明を行います。

ラムダ式について

次のいずれかの形の文字列をラムダ式と言います。
(ラムダ式をM, N, ...で表すこととします。)

  • 変数: x, y, z...
  • 関数抽象: \lambda x.M
  • 関数適用: MN
例:ラムダ式の例
  • x
  • xy
  • \lambda x.xy
  • (\lambda x.x)y
  • \lambda y.(\lambda x.xy)

関数抽象\lambda x.Mは、xを引数に取る匿名関数を表します。
例えば、\lambda x.(2x+1)のようなラムダ式で f(x)=2x+1となる関数fを表します。
fのような具体的な関数名を用意せずとも\lambda x.(2x+1)で関数を表現できることから匿名関数や無名関数と呼ばれることがあります。

特に、JavaScriptを書いたことがある人ならば、このような記法はアロー関数 x => 2*x + 1として親しみがあるかもしれません。

今まで単に2x+1と書いたときに、これが関数なのかただの多項式なのか見分けがつきませんでした。また、y=2x+aと書いても変数がxなのかaなのか分かりませんでした。

そこで、\lambda x.(2x+1)のようなラムダ記法を用いることで曖昧さなく匿名関数を表すことができ、ラムダ計算とは無関係の文脈でもインフォーマルにラムダ記法が用いられることもあります。
(ラムダ記法の他にも、x\mapsto 2x+1のような記法もよく見かけます。)

続いて関数適用[1]MNですが、これはお察しの通り関数[2]Mを引数Nに適用しているだけです。単純なラムダ計算には関数名を付ける機能は備わっていないため、常にJavaScriptでいう即時実行関数式 (IIFE)のような形となっています。

例として、 (\lambda x. 2x+1)3のようなラムダ式が関数適用の例であり、JavaScript風に書けば (x => 2*x + 1)(3)となります。

自己適用もアリなの?

ラムダ式の定義に従えば、xxのような自分に自分を適用する形も正しいラムダ式になります。

こんな訳わからん形を許容するせいで「任意の関数が不動点を持つ」みたいな訳わからん計算体系になってしまいますが、領域理論を用いればそのような訳わからん体系も上手く捉えることができ面白くなります。

適切な型を導入し、単純型付きラムダ計算STLC (Simply Typed Lambda Calculus)を考えることで上述の事故は防ぐことはできますが、その分計算力が落ちてしまうことには注意が必要です。
型を導入しつつも、さらに再帰的定義を許した計算体系PCF (Programming Computable Functions)まで拡張すれば、チューリング完全性を取り戻すことができます。

ちなみに、型無しラムダ計算は全ての式が単一の型Uを持つ型付きの体系とみなすこともでき、私は「型無しラムダ計算はSTLC (Singly Typed Lmabda Calculus)である」とか訳わからんことを主張しています。
(意味論を考えるときも全てのラムダ式を反射的対象U上の関数として捉えるみたいなことをするので、普通にSTLCの意味論の延長線上として捉えることができます。)

束縛変数と自由変数

ラムダ式\lambda x.(2x+y)においての変数xのように\lambdaによって束縛された変数を束縛変数と言い、yのようなその他の変数を自由変数と言います。

例として、x(\lambda x.\lambda y.(y+z))のようなラムダ式においては、x, zが自由変数であり、yが束縛変数となっています。

束縛変数の概念自体は高校数学まででも馴染みがあり、積分\int x^2dxにおいてのxや総和\sum_{k=0}^n(2k+1)においてのkなどが束縛変数の例となっております。

その際、束縛変数の名前は何でもよいという共通認識を私達は持っており、\int x^2dx\int t^2dtを区別しません。
このような同一視をラムダ計算の文脈では\alpha-同値性と呼び、実際\lambda x.x\lambda y.yといったラムダ式を同一視することが多いです。

「束縛変数かつ自由変数」となる変数

(\lambda x.x(\lambda x.x))xにおけるxは、素朴な定義のもとでは束縛変数でもあり自由変数でもあるという不可思議な状況になってしまいます。

これは各変数を変数名とか言う非本質で区別することにより起きる事故であって、通常は各変数を出現と呼ばれる変数の現れる位置によって区別をし、自由な出現束縛された出現といった言葉を用います。その上で必要に応じて変数名で区別をします。
(※de Bruijn Indexの話ではありません。)

ところで、自由変数の値はいつ定まるのでしょうか。
本記事では深入りはしませんが、意味を定めるときに環境と呼ばれる各自由変数の値のリストを入力値として受け取った際に自由変数の値が定まります。

すなわち、2x+1のようなラムダ式は意味論を定める際には「xを入力として受け取り、2x+1を出力として吐き出す関数」として解釈されます。
このような意味論を扱う文脈では、x\triangleright 2x+1のように引数のリストまで明示した形[3]として扱うことが多く、この引数のリストのことを文脈環境と呼びます。

束縛変数が関数の引数なんじゃないの?

x\triangleright 2x+1\triangleright\lambda x.(2x+1)似て非なるものです。

前者はまさに「xを入力として受け取り、2x+1を出力として受け取る関数」ですが、後者は「()を入力として受け取り、『xを入力として受け取り、2x+1を出力として吐き出す関数』を出力として吐き出す関数」となります。

JacaScript風に書けば、前者はx => 2*x + 1であり、後者は() => (x => 2*x + 1)となります。

また、型付きラムダ計算では各変数はその型に対応する(構造を持った)集合の要素として解釈され、x: \texttt{int}\triangleright 2x+1: \texttt{int}は(雑に言えば)整数上の関数f(x)=2x+1: \mathbb{Z}\to\mathbb{Z}として解釈されます。
型無しラムダ計算では全てが単一の型Uを持っていたため、各変数はすべて型Uに対応する「何らかの集合U」の要素として解釈され、各ラムダ式はU上の特殊な関数として解釈されます。
(このUの正体が知りたい方はScottモデルD_\inftyへGO!)

\beta-簡約について

ラムダ式(\lambda x. 2x+1)3は「計算」すれば7になりそうです。このように式の計算結果を求めることを、式を評価すると言います。

ラムダ計算においては、評価方法も厳密に定まっており、\beta-簡約と呼ばれる次の計算ルール(+部分式の簡約ルール)が存在します。

(\lambda x.M)N \rightarrow_\beta M[N/x]

M[N/x]はラムダ式Mの各変数xにラムダ式N代入したラムダ式を表す記法であり、(2x+1)[3/x]2*3+1を表すこととなります。

型無しラムダ計算においては\beta-簡約は必ず止まるとは限りません。\Omega\equiv(\lambda x.xx)(\lambda x.xx)というラムダ式の評価を考えてみてください。
左の式のxxの各xに、右の式の\lambda x.xxを代入することになり、再び(\lambda x.xx)(\lambda x.xx)が得られてしまいます。

すなわち、以下のように一生同じ形が繰り返され、計算結果が求まることはありません。

(\lambda x.xx)(\lambda x.xx) \rightarrow_\beta (\lambda x.xx)(\lambda x.xx) \rightarrow_\beta ...

ラムダ計算の諸定義

ここからはラムダ計算の諸定義をフォーマルに説明していこうと思います。

部分式と出現

まず、ラムダ式の定義を行います。


定義1: ラムダ式

アルファベットを\Sigma=\{\lambda, \texttt{v}, ', (, ), .\}とする。以下のBNF記法が定める集合V, \Lambda\subseteq\Sigma^*の元をそれぞれ変数ラムダ式という。

\begin{array}{ll} x ::= & \texttt{v}\mid x' \\ e ::= & x\mid (\lambda x.e)\mid (ee) \end{array}

(\lambda\texttt{v}.(\texttt{v}''\texttt{v}'))((\lambda\texttt{v}'.\texttt{v}')\texttt{v})などがラムダ式の一例となります。
また、\Lambdaは自由に生成された集合になることに注意してください。

変数の定義変じゃない?

あらかじめ変数の可算集合V=\{x, y, z, ...\}を用意する流儀もあるのですが、アルファベットが無限集合となってしまうため個人的には好きではありません。(この世界にある記号は有限個なので)
そこで、変数の集合VをBNF記法によりV=\{\texttt{v}, \texttt{v}', ...\}と定義する流儀を採用しました。

以降では簡単のため、変数の記号としてx, y, z,...を用いることとします。
また、カッコも適宜混乱のない範囲で省略をし、関数適用は左結合とします。[4]

続いて、部分式と出現の定義を行います。


定義2: 部分式

ラムダ式M\in\Lambdaに対し、M部分式の集合\mathrm{sub}(M)\subseteq\Lambdaを以下で定める。

  • \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\}

ラムダ式M, N\in\Lambdaに対して、M\subseteq N\iff M\in\mathrm{sub}(N)と定義します。

部分式は下記のような木構造を成します。

図1. (\lambda x. xy)(z(\lambda y. \lambda z. y))の部分式の成す木構造

部分式の成す木構造において、各部分式の出現位置を考えます。

上記の例では、部分式\lambda z.yは頂点から「右-右-下」の位置にあり、これを2\cdot 2\cdot 0と表現することとします。
すると、左側の変数yの出現位置は1\cdot 0\cdot 2、右側の変数yの出現位置は2\cdot 2\cdot 0\cdot 0となり、それぞれのyを区別して表現することができます。
(\lambda x. xy)(z(\lambda y. \lambda z. y))の出現位置は空列\epsilonとしましょう。


定義3: 出現位置

ラムダ式M\in\Lambdaに対し、M上の出現位置の集合[5]\mathcal{O}(M)\subseteq\{0, 1, 2\}^*を以下で定める。
(ただし、\cdotを列の連結演算子として、a\cdot S=\{a\cdot s\mid s\in S\}とする。)

  • \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\}

また、u, v\in\{0, 1, 2\}^*に対して、接頭辞関係u\le v\iff\exists w\in\{0, 1, 2\}^*, v\equiv u\cdot wと定義する。



定義4: 出現

ラムダ式M\in\Lambda、出現位置u\in\mathcal{O}(M)に対して、M/u\subseteq Mを以下で定める。

  • 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

ただし、\lambda x.M_0/0\equiv M_0, M_1M_2/1\equiv M_1, M_1M_2/2\equiv M_2とする。
M_1M_2/0などは未定義だが、\mathcal{O}(M)の定義よりM/uは常に定義されることに注意。)


ラムダ式M\in\Lambdaに対して、ラムダ式N\in\mathrm{sub}(M)、出現位置u\in\mathcal{O}(M)N\equiv M/uを満たすとき、組(u, N)\in\mathcal{O}(M)\times\mathrm{sub}(M)M上のuにおける出現と言います。
ただし、以降では簡単のため出現位置を省略して書くこととします。

これで変数の出現について、自由な出現・束縛された出現を定義することができます。
先程の例で言えば、1\cdot 0\cdot 2における出現y2\cdot 1における出現zが自由な出現となります。
また、1\cdot 0\cdot 1における出現x1において束縛された出現となり、2\cdot 2\cdot 0\cdot 0における出現y2\cdot 2において束縛された出現となります。


定義5: 自由な出現・束縛された出現

ラムダ式M\in\Lambda、出現位置u, v\in\mathcal{O}(M)に対して、述語\mathrm{Free}(u, M), \mathrm{Bound}(u, v, M)を以下で定める。[6]

  • \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 かつ \mathrm{Free}(u', M/v\cdot 0) where u\equiv v\cdot 0\cdot u'

ただし、x\in V, M\in\Lambdaに対して、以下の定義をした。

\lambda(M)\equiv x\iff\exists M_0\in\Lambda,M\equiv\lambda x.M_0

また、これらの定義を用いることで自由変数と束縛変数もそのまま定義できます。

  • \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-同値関係と代入

ラムダ式y(\lambda x. xy)の自由変数y\lambda s.stなどの別のラムダ式に置き換えてラムダ式(\lambda s.st)(\lambda x.x(\lambda s.st))を得るような操作を代入と言います。
ただし、代入では変数の補足に注意をする必要があります。

例えば、積分の例において、\int(x+y)dxの自由変数yx^2を「代入」すると、変数xが束縛され\int(x+x^2)dxとなってしまいます。

そういう代入操作を考えるのはダメなの?

上述の素朴な定義だと、以下のように「代入してから計算」と「計算してから代入」の結果が一致しないためあまりよろしくありません。

  • 代入してから計算:\frac{x^3}{3}+\frac{x^2}{2}+C
  • 計算してから代入:x^3+\frac{x^2}{2}+C

このような代入と計算の可換性の他にも、代入と意味の可換性代入補題などきちんと定義された代入操作にはきれいな性質がいくつかあり、変数名の置き換えがとても重要になります。
ちなみに前者2つも代入補題と呼ばれることがありますが、私は認めていません。(?)

そこで、\int(x+y)dx\int(t+y)dtも同じだという\alpha-同値性を利用して、代入の定義においては元のラムダ式の変数名を置き換えてから置き換えるするという工夫を行います。

すなわち、freshな変数tを適当に用意して、「\int(x+y)dxの自由変数yx^2を代入」するという操作の結果が\int(t+x^2)dtとなるように定義します。


定義6: 代入

ラムダ式M, N\in\Lambda、変数x\in Vに対し、代入M[N/x]を以下で定める。

  • 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])

ただし、最後のz\in VV/\mathrm{FV}(M_0N)上の最小の変数。
x<:y\iff y\equiv x'の反射推移閉包としてV上の全順序を定義した。つまり、\texttt{v}<\texttt{v}'<\texttt{v}''<\cdotsとした。V/\mathrm{FV}(M_0N)上の最小値は当然存在する。)


同時代入の定義

逐次代入M[N/x][L/y]と同時代入M[N, L/x, y]の結果は等しいとは限らない。

例:
  • 逐次代入:(x(xy))[vy/x][w/y]\equiv vy(vyy)[w/y]\equiv vw(vww)
  • 同時代入:(x(xy))[vy, w/x, y]\equiv vy(vyw)

n個の変数を同時に置き換えるM[N_1, \ldots, N_n/x_1, \ldots, x_n]は次のように変数の個数についての帰納法で定義される。

  • 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]

(ただし、y\not\in\mathrm{FV}(MN_1\ldots N_n)とする。yの選び方に依存しないことは要証明。)

代入の定義の3つ目の正当性を確かめるために、\alpha-同値関係[7]を導入します。


定義7: \alpha-同値関係

二項関係=_\alpha\subseteq\Lambda\times\Lambdaを次を満たす最小の集合として定義する。

  • \alpha-変換
\frac{y\not\in\mathrm{FV}(M)}{\lambda x.M=_\alpha\lambda y.(M[y/x])}
  • 部分式の規則
\frac{M=_\alpha N}{LM=_\alpha LN}
\frac{M=_\alpha N}{ML=_\alpha NL}
\frac{M=_\alpha N}{\lambda x.M=_\alpha \lambda x.N}
  • 同値関係の規則
\frac{}{M=_\alpha M}
\frac{M=_\alpha N\quad N=_\alpha L}{M=_\alpha L}
\frac{M=_\alpha N}{N=_\alpha M}

例: \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によって保証されます。


命題8: 代入と\alpha-同値関係の両立性

ラムダ式M, M', N, N'\in\Lambda, 変数x\in Vに対して以下が成り立つ。

M=_\alpha M'\text{ かつ }N=_\alpha N'\implies M[N/x]=_\alpha M'[N'/x]
証明

この定理に関して、私は真に驚くべき証明を見つけたが、この余白はそれを書くには狭すぎるので300年後に追記します。
\square


そこで、以降では\alpha-同値なラムダ式を区別しないこととします。
すなわち、\Lambda/\mathord{=}_\alphaをの上で理論を展開するものとし、単に\Lambdaで集合\Lambda/\mathord{=}_\alphaを指すとします。[8]

すると、束縛変数名は好きに思ってよくなるため代入の定義が以下のように修正されます。


定義9: 代入(修正版)

ラムダ式M, N\in\Lambda、変数x\in Vに対し、代入M[N/x]を以下で定める。

  • 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, N, L\in\Lambda, 変数x, y\in V (x\not\in\mathrm{FV}(L))に対して、次が成り立つ。

M[N/x][L/y]\equiv M[L/y][N[L/y]/x]
証明
  • M\equiv xのとき
\begin{array}{rcl} x[N/x][L/y] & \equiv & N[L/y] \\ & \equiv & x[N[L/y]/x] \\ & \equiv & x[L/y][N[L/y]/x] \end{array}
  • M\equiv yのとき (x\not\in\mathrm{FV}(L)に注意)
\begin{array}{rcl} y[N/x][L/y] & \equiv & L \\ & \equiv & L[N[L/y]/x] \\ & \equiv & y[L/y][N[L/y]/x] \end{array}
  • M\equiv zのとき (z\not\equiv x, y)
\begin{array}{rcl} z[N/x][L/y] & \equiv & z \\ & \equiv & z[L/y][N[L/y]/x] \end{array}
  • M\equiv M_1M_2のとき
\begin{array}{rcl} (M_1M_2)[N/x][L/y] & \equiv & (M_1[N/x][L/y])(M_2[N/x][L/y]) \\ & \equiv & (M_1[L/y][N[L/y]/x])(M_2[L/y][N[L/y]/x]) \\ & \equiv & (M_1M_2)([L/y][N[L/y]/x]) \end{array}
  • M\equiv\lambda z.M_0のとき (z\not\in\mathrm{FV}(NL)とする)
\begin{array}{rcl} (\lambda z.M_0)[N/x][L/y] & \equiv & \lambda z.M_0[N/x][L/y] \\ & \equiv & \lambda z.M_0[L/y][N[L/y]/x] \\ & \equiv & (\lambda z.M_0)[L/y][N[L/y]/x] \end{array}

\square


ちなみに、\alpha-同値なラムダ式を同一視せずに初期の代入の定義のままだと代入補題は成り立ちません。

例:代入補題の反例
  • (\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-変換

(\lambda x. yx)zのようなラムダ式は、「計算」をすることができ、ラムダ式yzが得られます。
このような「計算」のことを\beta-変換といい、(\lambda x.M)Nの形のラムダ式のことを\beta-基と呼びます。

この\beta-変換には、CR性、正規化定理、標準化定理など非常に重要な性質がたくさんありますが、それは次回に回してここでは定義のみ紹介します。


定義11: \beta-変換

二項関係\to_\beta\subseteq\Lambda\times\Lambdaを次を満たす最小の集合として定義する。

  • \beta-変換
\frac{}{(\lambda x.M)N\to_\beta M[N/x]}
  • 部分式の規則
\frac{M\to_\beta N}{LM\to_\beta LN}
\frac{M\to_\beta N}{ML\to_\beta NL}
\frac{M\to_\beta N}{\lambda x.M\to_\beta \lambda x.N}

最後に、代入と計算の可換性、つまり、「計算してから代入した結果」と「代入してから計算した結果」が一致することを証明して終わります。


命題18: 代入と計算の可換性

ラムダ式M, N, L及び変数x\in Vに対して、次が成り立つ。

M\to_\beta N\implies M[L/x]\to_\beta N[L/x]
証明

規則帰納法で示す。

  • \frac{}{(\lambda y.M_1)M_2\to_\beta M_1[M_2/y]}のとき (y\not\in\mathrm{FV}(L)とする)
\begin{array}{rll} ((\lambda y.M_1)M_2)[L/x] & \equiv & (\lambda y.M_1[L/x])M_2[L/x] \\ & \to_\beta & M_1[L/x][M_2[L/x]/y] \\ & \equiv & M_1[M_2/y][L/x]\ \because\text{代入補題} \end{array}
  • \frac{M_2\to_\beta N_2}{L_1M_2\to_\beta L_1N_2}のとき (もう一方も同様)
\begin{array}{rll} (L_1M_2)[L/x] & \equiv & (L_1[L/x])(M_2[L/x]) \\ & \to_\beta & (L_1[L/x])(N_2[L/x]) \\ & \equiv & (L_1N_2)[L/x] \end{array}
  • \frac{M_0\to_\beta N_0}{\lambda y.M_0\to_\beta \lambda y.N_0}のとき (y\not\in\mathrm{FV}(L)とする)
\begin{array}{rcl} (\lambda y.M_0)[L/x] & \equiv & \lambda y.M_0[L/x] \\ & \to_\beta & \lambda y.N_0[L/x] \\ & \equiv & (\lambda y.N_0)[L/x] \end{array}

\square


おわりに

お疲れ様でした。ここまで読んでいただきありがとうございました。

ラムダ計算は厳密に扱おうとすればするほど沼にハマっていくような分野ですが、その分簡単そうな定義にも深みがあって面白いと思います。

また、以下の記事で紹介するBöhm木やhnfの話は、これを知らずに型無しラムダ計算を学んだことがあると主張するのは無理があるレベルで基本的かつ重要な事柄だと思いますので、ぜひ合わせて読んでいただけると嬉しいです。

https://zenn.dev/mineel5/articles/bohm_tree_lambda

改めて、本当にありがとうございました。

参考文献

(Barendregtの『The Lambda Calculus: Its Syntax and Semantics』にこの宇宙のすべてが載っています。当然私は全く読めていません。)

  1. 井田哲雄(1991)『計算モデルの基礎理論』岩波書店.

  2. 高橋正子(1991) 『計算論 計算可能性とラムダ計算』近代科学社.

  3. 林晋・小林聡(1991)『構成的プログラミングの基礎』遊星社.

  4. 横内寛文(1994)『プログラム意味論』共立出版.

  5. 大堀淳(1997)『プログラミング言語の基礎理論』共立出版.

  6. 星野直彦 (2013) 『型無しラムダ計算とモデル』(PDF), 取得元 (アクセス日: 2024年10月1日)

  7. B. C. Pierce (著), 住井英二郎 (監訳), 遠藤侑介・酒井政裕・今井敬吾 (翻訳) (2013) 『型システム入門 −プログラミング言語と型の理論−』オーム社.

  8. G. Winskel (著), 末永幸平 (監修・翻訳), 勝股審也・中澤巧爾 (翻訳) (2023) 『プログラミング言語の形式的意味論入門』共立出版.

  9. H. P. Barendregt (1984) "The Lambda Calculus: Its Syntax and Semantics," North-Holland.

  10. H. Barendregt (1992) "Lambda Calculi with Types," Handbook of Logic in Computer Science, Volume 2, Oxford University Press.

  11. B. Jacobs (1997) "A Tutorial on (Co)Algebras and (Co)Induction," EATCS Bulletin, 62, 222-259.

  12. R. Amadio, P.-L. Curien (1998) "Domains and Lambda-calculi," Cambridge University Press.

  13. M. H. Sørensen, P. Urzyczyn (2006) "Lectures on the Curry-Howard Isomorphism," Elsevier Science.

  14. J. R. Hindley, J. P. Seldin (2008) "Lambda-Calculus and Combinators, an Introduction," 2nd Edition, Cambridge University Press.

脚注
  1. 関数適用MNでは、「関数MNに適用する」という言葉の使い方をします。 ↩︎

  2. 便宜的にMを「関数」と読んでいますが、定義上\lambda x.M'の形でない式を適用しても構いません ↩︎

  3. x\vdash 2x+1のような形も見ますが、個人的に\vdashの左には導出の仮定を起きたいため好きではありません。 ↩︎

  4. 右結合・左結合は構文の定義ではなく、略記規則の一つであることに注意。『計算モデルの基礎理論』(井田)のp. 73には略記規則の厳密な定義があります。 ↩︎

  5. \mathcal{O}(M)木領域という構造を成します。(c.f.『計算モデルの基礎理論』(井田)p.77) ↩︎

  6. 最後の\mathrm{Free}の条件は、\lambda x.x(\lambda x.x)のようなケースのためです。 ↩︎

  7. \alpha-同値の定義に関連してNominal Setという話があるらしく、いつか勉強してみます。 ↩︎

  8. さて、本当に勝手にこんなことをしてもよいのでしょうか? ↩︎

Discussion