ラムダ計算

ラムダ計算（ λ計算とも表記）は、変数の束縛と置換を用いた関数の抽象化と適用に基づく計算を表現する数理論理学の形式体系である。この記事のテーマである型なしラムダ計算は、あらゆるチューリングマシンをシミュレートするために使用できる（逆もまた同様）計算の汎用モデルである。これは、数学者アロンゾ・チャーチが1930年代に数学の基礎に関する研究の一環として導入した。1936年、チャーチは論理的に一貫した定式化を発見し、1940年にそれを文書化した。

ラムダ計算は、ラムダ項の構築とそれに対する簡約演算の実行から成ります。最も単純なラムダ計算では、項は以下の規則のみを使用して構築されます。^[a]

1. ${\textstyle x}$変数はパラメータを表す文字または文字列です。
2. ${\textstyle (\lambda xM)}$: ラムダ抽象化は、境界変数(λ と点/ドット.の間) を入力として受け取り、本体を返す関数定義です。${\displaystyle x}$${\textstyle M}$
3. ${\textstyle (M\ N)}$: 関数を引数に適用するアプリケーション。 と はどちらもラムダ項です。${\textstyle M}$${\textstyle N}$${\textstyle M}$${\textstyle N}$

削減操作には以下が含まれます。

• ${\textstyle (\lambda x.M[x])\rightarrow (\lambda y.M[y])}$ : α変換。式内のバインドされた変数の名前を変更します。名前の衝突を回避するために使用されます。
• ${\textstyle ((\lambda x.M)\ N)\rightarrow (M[x:=N])}$ : β-削減、^[b]抽象化の本体内の引数式で束縛変数を置き換える。

De Bruijn インデックスを使用すると、名前の衝突がなくなるため、α 変換は不要になります。削減手順を繰り返し適用して最終的に終了すると、 Church–Rosser 定理によりβ 正規形が生成されます。

Iota や Jotなどのユニバーサル ラムダ関数を使用する場合、変数名は必要ありません。これらの関数は、さまざまな組み合わせで自分自身を呼び出すことで、任意の関数の動作を作成できます。

ラムダ計算はチューリング完全であり、つまりあらゆるチューリングマシンをシミュレートするために使用できる計算の汎用モデルです。^{[3]その名前の由来であるギリシャ文字のラムダ（λ）は、ラムダ式とラムダ項で}関数内の変数のバインディングを示すために使用されます。

ラムダ計算は、型なしまたは型付きです。型付きラムダ計算では、関数は、与えられた入力の「型」のデータを受け入れられる場合にのみ適用できます。型付きラムダ計算は、型なしラムダ計算よりも表現できるものが少ないという意味で、この記事の主な主題である型なしラムダ計算よりも弱いです。一方、型付きラムダ計算では、より多くのことを証明できます。たとえば、単純型付きラムダ計算では、すべての評価戦略がすべての単純型付きラムダ項に対して終了するのに対し、型なしラムダ項の評価は終了する必要がないという定理があります (以下を参照)。さまざまな型付きラムダ計算が存在する理由の 1 つは、計算に関する強力な定理を証明できることを諦めずに、より多くのこと (型なし計算でできること) を実行したいという要望です。

ラムダ計算は、数学、哲学、^[4] 言語学、^{[5] [6]}コンピュータサイエンスのさまざまな分野で応用されています。^{[7] [8]ラムダ計算は、}プログラミング言語の理論の発展に重要な役割を果たしてきました。関数型プログラミング言語はラムダ計算を実装しています。ラムダ計算は、圏論の現在の研究テーマでもあります。^[9]

ラムダ計算は、1930年代に数学者アロンゾ・チャーチによって数学の基礎研究の一環として導入されました。^{[10] [c]}元のシステムは、1935年にスティーブン・クリーネとJB・ロッサーがクリーネ・ロッサーのパラドックスを考案したときに論理的に矛盾していることが示されました。^{[11] [12]}

その後、1936年にチャーチは計算に関連する部分だけを切り出して出版しました。これは現在では型なしラムダ計算と呼ばれています。 ^[13] 1940年には、計算的には弱いが論理的に一貫性のあるシステムも発表しました。これは単純型付きラムダ計算と呼ばれています。^[14]

1960年代にプログラミング言語との関係が明らかになるまで、ラムダ計算は単なる形式論に過ぎなかった。リチャード・モンタギューや他の言語学者による自然言語の意味論への応用により、ラムダ計算は言語学^{[15]とコンピュータサイエンス[16]}の両方で尊敬される地位を獲得し始めた。

チャーチがラムダ計算における関数抽象化の表記としてギリシャ文字のラムダ(λ) を使用した理由については不明な点があるが、これはチャーチ自身の説明が矛盾しているからかもしれない。Cardone と Hindley (2006) によると、

ところで、チャーチはなぜ「λ」という表記法を選んだのでしょうか。[1964年にハラルド・ディクソンに宛てた未発表の手紙]で、チャーチは、それがホワイトヘッドとラッセルがクラス抽象化に使用した表記法「 」から来ており、関数抽象化とクラス抽象化を区別するために「 」を「 」に変更し、次に印刷しやすいように「 」を「λ」に変更したと明言しています。 ${\displaystyle {\hat {x}}}$${\displaystyle {\hat {x}}}$${\displaystyle \land x}$${\displaystyle \land }$

この起源は[Rosser, 1984, p.338]でも報告されています。一方、チャーチは晩年、2人の質問者に対し、この選択はより偶然のものであり、記号が必要だったが、たまたまλが選ばれただけだと語っています。

ダナ・スコットも、さまざまな公開講演でこの問題に取り組んでいます。^[17] スコットは、かつてチャーチの元教え子で義理の息子であるジョン・W・アディソン・ジュニアにラムダ記号の起源について質問したところ、アディソンは義父に次のようなポストカードを書いたと語っています。

チャーチ教授様

ラッセルにはイオタ演算子があり、ヒルベルトにはイプシロン演算子がありました。演算子としてラムダを選んだのはなぜですか?

スコットによれば、チャーチの返答は、次のような注釈を付けてポストカードを返送することだけだった。「イニー、ミーニー、ミニー、モー」。

計算可能な関数は、コンピュータ サイエンスと数学における基本的な概念です。ラムダ計算は、計算の特性を形式的に研究するのに役立つ、計算のシンプルなセマンティクスを提供します。ラムダ計算には、セマンティクスをシンプルにする 2 つの簡略化が組み込まれています。 最初の単純化は、ラムダ計算が関数を「匿名」で扱うことです。関数に明示的な名前は与えません。たとえば、関数

${\displaystyle \operatorname {square\_sum} (x,y)=x^{2}+y^{2}}$

匿名形式では次のように 書き直すことができる。

${\displaystyle (x,y)\mapsto x^{2}+y^{2}}$

（これは「 xとyのタプルが」にマッピングされるという意味です）。^[d]同様に、関数 ${\textstyle x^{2}+y^{2}}$

${\displaystyle \operatorname {id} (x)=x}$

匿名形式では次のように書き直すことができる。

${\displaystyle x\mapsto x}$

入力は単純にそれ自身にマッピングされます。^[d]

2 つ目の単純化は、ラムダ計算では単一の入力の関数のみを使用するという点です。たとえば関数のように 2 つの入力を必要とする通常の関数は、単一の入力を受け取り、出力として別の関数を返す同等の関数に作り直すことができます。この関数も単一の入力を受け取ります。たとえば、 ${\textstyle \operatorname {square\_sum} }$

${\displaystyle (x,y)\mapsto x^{2}+y^{2}}$

作り直すことができる

${\displaystyle x\mapsto (y\mapsto x^{2}+y^{2})}$

カリー化と呼ばれるこの方法は、複数の引数を取る関数を、それぞれが 1 つの引数を取る関数のチェーンに変換します。

関数を引数(5, 2)に 適用すると、次の式が得られます。${\textstyle \operatorname {square\_sum} }$

${\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}$

${\textstyle =5^{2}+2^{2}}$

${\textstyle =29}$、

一方、カリー化されたバージョンの評価にはもう1つのステップが必要です

${\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}$

${\textstyle =(y\mapsto 5^{2}+y^{2})(2)}$// の定義は内部式で使用されています。これは β 削減のようなものです。${\displaystyle x}$${\displaystyle 5}$

${\textstyle =5^{2}+2^{2}}$// の定義はで使用されています。これも β 削減と同様です。${\displaystyle y}$${\displaystyle 2}$

${\textstyle =29}$

同じ結果に到達します。

ラムダ計算は、特定の形式構文で定義されるラムダ項の言語と、ラムダ項を操作するための一連の変換規則で構成されます。これらの変換規則は、方程式理論または操作的定義として見ることができます。

上で説明したように、ラムダ計算のすべての関数は名前がないため、無名関数です。これらは 1 つの入力変数のみを受け入れるため、複数の変数の関数を実装するにはカリー化が使用されます。

ラムダ計算の構文では、一部の文字列がCプログラムとして有効で一部が無効であるのと同様に、一部の式は有効なラムダ計算式として定義され、一部は無効として定義されます。有効なラムダ計算式は、「ラムダ項」と呼ばれます。

次の3つの規則は、すべての構文的に有効なラムダ項を構築するために適用できる帰納的定義を与える: ^[e]

• 変数x自体は有効なラムダ項です。
• tがラムダ項でxが変数の場合、 ^{[f] は}ラムダ項（抽象化と呼ばれる）になります。${\displaystyle (\lambda x.t)}$
• tとs がラムダ項である場合、 はラムダ項です（アプリケーションと呼ばれます）。${\displaystyle (t}$  ${\displaystyle s)}$

それ以外はラムダ項ではありません。つまり、ラムダ項は、これら 3 つの規則を繰り返し適用することで得られる場合にのみ有効です。便宜上、ラムダ項を書くときに一部の括弧を省略できます。たとえば、最も外側の括弧は通常は書きません。どの括弧が省略可能であるかを明示的に説明するには、以下の § 表記法 を参照してください。また、ここで紹介した構文を追加演算で拡張することも一般的であり、これにより、次のような用語の意味を理解できるようになります。この記事の焦点は、拡張のない純粋なラムダ計算ですが、算術演算で拡張されたラムダ項は説明目的で使用されています。 ${\displaystyle \lambda x.x^{2}.}$

抽象化は、 単一の入力x を受け取り、tを返す§ 無名関数^[g]を表します。たとえば、は、tの項を使用して定義された関数を表す抽象化です。抽象化を使用する場合、名前は不要です。構文は、t の項で変数x をバインドします。抽象化を使用した関数の定義は、関数を「設定」するだけで、関数を呼び出すことはありません。 ${\displaystyle \lambda x.t}$${\displaystyle \lambda x.(x^{2}+2)}$${\displaystyle f}$${\displaystyle f(x)=x^{2}+2,}$${\displaystyle x^{2}+2}$${\displaystyle f}$${\displaystyle (\lambda x.t)}$

アプリケーションは 、関数tを入力sに適用することを表します。つまり、入力sに対して関数t を呼び出してを生成するという動作を表します。 ${\displaystyle t}$  ${\displaystyle s}$${\displaystyle t(s)}$

ラムダ項は、項(関数定義を表す)などの、バインドされていない変数を参照する場合があります。この項では、変数y は定義されておらず、未知数とみなされます。抽象化は構文的に有効な項であり、入力をまだ不明なyに追加する関数を表します。 ${\displaystyle \lambda x.(x+y)}$${\displaystyle f(x)=x+y}$${\displaystyle \lambda x.(x+y)}$

括弧は用語の曖昧さを解消するために必要になる場合があります。例えば、

1. ${\displaystyle \lambda x.((\lambda x.x)x)}$は形式的であり、したがって抽象的であるが、${\displaystyle \lambda x.B}$
2. ${\displaystyle (\lambda x.(\lambda x.x))}$ ${\displaystyle x}$形式であるため、アプリケーションです。${\displaystyle M}$  ${\displaystyle N}$

例 1 と 2 は異なる用語を表し、括弧の位置のみが異なります。これらは意味が異なります。例 1 は関数定義ですが、例 2 は関数適用です。ラムダ変数x は、両方の例でプレースホルダーです。

ここで、例 1 は関数を定義します。ここで、 は入力 を持つ無名関数です。一方、例 2 は、 N に適用される M です。ここで、は入力 に適用されるラムダ項です。例 1 と例 2 はどちらも恒等関数に評価されます。 ${\displaystyle \lambda x.B}$${\displaystyle B}$${\displaystyle (\lambda x.x)x}$${\displaystyle (\lambda x.x)}$${\displaystyle x}$${\displaystyle M}$ ${\displaystyle N}$${\displaystyle M}$${\displaystyle (\lambda x.(\lambda x.x))}$${\displaystyle N}$${\displaystyle x}$ ${\displaystyle \lambda x.x}$

ラムダ計算では、関数は「ファーストクラスの値」として扱われるため、関数は入力として使用されることもあれば、他の関数からの出力として返されることもあります。

たとえば、ラムダ項は恒等関数を表します。さらに、は定数関数 を表します。定数関数は、入力に関係なく常に を返す関数です。関数を操作する関数の例として、関数合成はと定義できます。 ${\displaystyle \lambda x.x}$${\displaystyle x\mapsto x}$${\displaystyle \lambda x.y}$ ${\displaystyle x\mapsto y}$${\displaystyle y}$${\displaystyle \lambda f.\lambda g.\lambda x.(f(gx))}$

「同等性」と「削減」には、ラムダ項を「同等の」ラムダ項に「削減」できるようにする概念がいくつかあります。

ラムダ項で定義できる同値性の基本的な形式は、アルファ同値性です。これは、抽象化における束縛変数の特定の選択は（通常は）重要ではないという直感を捉えています。たとえば、およびはアルファ同値なラムダ項であり、どちらも同じ関数（恒等関数）を表します。項およびは抽象化で束縛されていないため、アルファ同値ではありません。多くのプレゼンテーションでは、アルファ同値なラムダ項を識別するのが一般的です。 ${\displaystyle \lambda x.x}$${\displaystyle \lambda y.y}$${\displaystyle x}$${\displaystyle y}$

β 減少を定義するには、次の定義が必要です。

項の自由変数 [ ^h]は抽象化によって束縛されていない変数です。式の自由変数の集合は帰納的に定義されます。

• の自由変数は、${\displaystyle x}$${\displaystyle x}$
• の自由変数の集合は、の自由変数の集合であるが、${\displaystyle \lambda x.t}$${\displaystyle t}$${\displaystyle x}$
• の自由変数の集合は、 の自由変数の集合と の自由変数の集合の和集合です。${\displaystyle t}$ ${\displaystyle s}$${\displaystyle t}$${\displaystyle s}$

たとえば、恒等式を表すラムダ項には自由変数はありませんが、関数には 1 つの自由変数があります。 ${\displaystyle \lambda x.x}$${\displaystyle \lambda x.y}$ ${\displaystyle x}$${\displaystyle y}$

、および がラムダ項であり、およびが変数であるとします。この表記は、キャプチャを回避する方法でを に置き換えることを示しています。これは次のように定義されます。 ${\displaystyle t}$${\displaystyle s}$${\displaystyle r}$${\displaystyle x}$${\displaystyle y}$${\displaystyle t[x:=r]}$${\displaystyle r}$${\displaystyle x}$${\displaystyle t}$

• ${\displaystyle x[x:=r]=r}$;をに置き換える と、${\displaystyle r}$${\displaystyle x}$${\displaystyle x}$${\displaystyle r}$
• ${\displaystyle y[x:=r]=y}$ ;を に置き換えた場合、（ ではない）は残る${\displaystyle x\neq y}$${\displaystyle r}$${\displaystyle x}$${\displaystyle y}$${\displaystyle x}$${\displaystyle y}$
• ${\displaystyle (t}$ ${\displaystyle s)[x:=r]=(t[x:=r])(s[x:=r])}$ ; 置換はアプリケーションの両側に分配されます
• ${\displaystyle (\lambda x.t)[x:=r]=\lambda x.t}$ ; 抽象化によって束縛された変数は置換の対象とならない。そのような変数を置換しても抽象化は変更されない。
• ${\displaystyle (\lambda y.t)[x:=r]=\lambda y.(t[x:=r])}$およびが の自由変数の中に現れない場合(は に対して「新鮮」であると言われる)、抽象化によって束縛されていない変数の置換は、抽象化された変数が置換項に対して「新鮮」である限り、抽象化の本体内で進行します。${\displaystyle x\neq y}$${\displaystyle y}$${\displaystyle r}$${\displaystyle y}$${\displaystyle r}$${\displaystyle y}$${\displaystyle r}$

たとえば、、 などです。 ${\displaystyle (\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x}$${\displaystyle ((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y}$

新鮮さの条件（が の自由変数に含まれていないことを要求する）は、置換によって関数の意味が変わらないようにするために重要です。 ${\displaystyle y}$${\displaystyle r}$

たとえば、鮮度条件を無視する置換はエラーを引き起こす可能性があります: 。この誤った置換により、定数関数が恒等関数 に変換されます。 ${\displaystyle (\lambda x.y)[y:=x]=\lambda x.(y[y:=x])=\lambda x.x}$${\displaystyle \lambda x.y}$${\displaystyle \lambda x.x}$

一般に、新鮮さの条件を満たさない場合は、まず適切な新しい変数を使用してアルファ名前変更することで改善できます。たとえば、置換の正しい概念に戻ると、抽象化では、新しい変数 で名前を変更して を取得し、関数の意味は置換によって保持されます。 ${\displaystyle (\lambda x.y)[y:=x]}$${\displaystyle z}$${\displaystyle (\lambda z.y)[y:=x]=\lambda z.(y[y:=x])=\lambda z.x}$

β-簡約規則^{[b] は}、形式 を適用すると項 に簡約されると述べています。 表記は、 β-簡約されて になることを示すために使用されます。たとえば、任意の に対して、となります。これは、 が実際に恒等関数であることを示しています。同様に、は、 が定数関数であることを示しています。 ${\displaystyle (\lambda x.t)s}$${\displaystyle t[x:=s]}$${\displaystyle (\lambda x.t)s\to t[x:=s]}$${\displaystyle (\lambda x.t)s}$${\displaystyle t[x:=s]}$${\displaystyle s}$${\displaystyle (\lambda x.x)s\to x[x:=s]=s}$${\displaystyle \lambda x.x}$${\displaystyle (\lambda x.y)s\to y[x:=s]=y}$${\displaystyle \lambda x.y}$

ラムダ計算は、 HaskellやStandard MLのような関数型プログラミング言語の理想化されたバージョンとして見ることができます。この見方では、β 還元は計算ステップに対応します。このステップは、還元するアプリケーションがなくなるまで、追加の β 還元によって繰り返すことができます。ここで示す型なしラムダ計算では、この還元プロセスは終了しない場合があります。たとえば、項 を考えてみましょう。ここではです。つまり、項 は単一の β 還元でそれ自体に還元されるため、還元プロセスが終了することはありません。 ${\displaystyle \Omega =(\lambda x.xx)(\lambda x.xx)}$${\displaystyle (\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)}$

型なしラムダ計算のもう 1 つの側面は、異なる種類のデータを区別しないことです。たとえば、数値のみを操作する関数を記述することが望ましい場合があります。ただし、型なしラムダ計算では、関数が真理値、文字列、またはその他の数値以外のオブジェクトに適用されることを防ぐ方法はありません。

ラムダ式は次の要素で構成されます。

• 変数v ₁、v ₂、 ...;
• 抽象記号 λ (ラムダ) と . (ドット)
• 括弧()。

ラムダ式の集合Λは、帰納的に定義できます。

1. xが変数の場合、 x ∈ Λ です。
2. xが変数でM ∈ Λの場合、(λ x . M ) ∈ Λ です。
3. M、N∈Λならば、( MN )∈Λです。

ルール2のインスタンスは抽象化と呼ばれ、ルール3のインスタンスは応用と呼ばれます。^[18] § 還元可能な表現を参照

この規則セットは、バッカス・ナウア形式で次のように記述できます。

 <式>   :== <抽象> | <アプリケーション> | <変数> 
 <抽象>  :== λ <変数> . <式> 
 <アプリケーション>  :== ( <式>  <式> )
  <変数>     :== v1 | v2 | ...

ラムダ式の表記を整理するために、通常は次の規則が適用されます。

• 一番外側の括弧は削除されます: ( M N ) の代わりにM N になります。
• アプリケーションは左結合であると仮定されており、 ( ( MN ) P )の代わりにMNPと書くこともできる。 [ 19 ^]
• 全ての変数が1文字の場合、応用部分のスペースは省略できる：MNPではなくMNP 。^[20]
• 抽象化の本体は可能な限り右に拡張されます。つまり、λ x . MN はλ x .( MN ) を意味し、(λ x . M ) Nを意味するわけではありません。
• 抽象化のシーケンスは短縮される：λ x .λ y .λ z . Nはλ xyz . Nと略される。^{[21] [19]}

抽象化演算子 λ は、抽象化の本体のどこにあっても、その変数をバインドすると言われます。抽象化のスコープ内にある変数は、バインドされていると言われます。式 λ x . Mでは、 λ x の部分は、変数x がλ x をMの前に追加することによってバインドされることを示すヒントとして、バインダーと呼ばれることがよくあります。その他のすべての変数は、フリーと呼ばれます。たとえば、式 λ y . xxyでは、yはバインド変数で、xはフリー変数です。また、変数は最も近い抽象化によってバインドされます。次の例では、式内のxの単一の出現は、2 番目のラムダによってバインドされています: λ x . y (λ x . zx )。

ラムダ式の自由変数の集合Mは FV( M )と表され、項の構造の再帰によって次のように定義されます。

1. FV( x ) = { x }、ここでxは変数です。
2. FV(λ x . M ) = FV( M ) \ { x }. ^[i]
3. FV( MN ) = FV( M ) ∪ FV( N )。^[j]

自由変数を含まない式は閉じていると言われます。閉じたラムダ式はコンビネータとも呼ばれ、組み合わせ論理の項と同等です。

ラムダ式の意味は、式をどのように簡約できるかによって定義されます。^[22]

削減には3つの種類があります:

• α変換：結合変数の変更。
• β-削減: 関数をその引数に適用する;
• η-還元: 外延性の概念を捉えます。

また、結果として生じる同値性についても言及します。2 つの式が同じ式に α 変換できる場合、それらの式 はα 同値です。β 同値性と η 同値性も同様に定義されます。

redexという用語は、簡約可能な表現の略で、簡約規則の 1 つによって簡約できる部分項を指します。たとえば、 (λ x . M ) N は、 MのxをNに置き換えることを表す β-redex です。redex が簡約される式は、その縮約と呼ばれます。 (λ x . M ) Nの縮約はM [ x  := N ]です。^[b]

xがMにおいて自由でない場合、 λ x。M xも η-redex であり、Mの縮約を持つ。

α変換（アルファ変換）はα名前変更とも呼ばれ、^[23]バインドされた変数名を変更することができます。たとえば、λ x . xのα変換はλ y . yを生成する可能性があります。α変換によってのみ異なる項はα同等と呼ばれます。ラムダ計算の使用では、α同等の項は同等であるとみなされることがよくあります。

α 変換の正確なルールは、完全に自明というわけではありません。まず、抽象化を α 変換する場合、名前が変更される変数出現は、同じ抽象化にバインドされているものだけです。たとえば、 λ x .λ x . xの α 変換は λ y .λ x . xになる可能性がありますが、 λ y .λ x . yになることはできません。後者は元の意味とは異なります。これは、変数シャドウイングというプログラミング概念に似ています。

2 番目に、変数が異なる抽象化によってキャプチャされる結果になる場合、α 変換は不可能です。たとえば、λ x .λ y . xでx をyに置き換えると、λ y .λ y . yになりますが、これはまったく同じではありません。

静的スコープを持つプログラミング言語では、α 変換を使用して、変数名が包含スコープ内の名前をマスクしないようにすることで、名前解決を簡素化できます( 「名前解決を容易にするための α 名変更」を参照)。

De Bruijn 指数表記では、任意の 2 つの α 同値項は構文的に同一です。

置換はM [ x  := N ] と書かれ、式M内の変数xのすべての自由な出現を式Nに置き換えるプロセスです。ラムダ計算の項の置換は、項の構造の再帰によって次のように定義されます (注: x と y は変数のみですが、 M と N は任意のラムダ式です)。

x [ x  := N ] = N

y [ x  := N ] = y、x ≠ yの場合

( M ₁ M ₂ )[ x  := N ] = M ₁ [ x  := N ] M ₂ [ x  := N ]

(λ x . M )[ x  := N ] = λ x . M

(λ y . M )[ x  := N ] = λ y .( M [ x  := N ])、x ≠ yかつy ∉ FV( N ) の場合FVについては上記を参照

抽象表現に代入するには、式をα変換する必要がある場合があります。たとえば、(λ x . y )[ y  := x ] が λ x . xになるのは正しくありません。代入されたx は自由であるはずが、結局は束縛されているからです。この場合の正しい代入は、α同値性までλ z . xです。代入は、α同値性まで一意に定義されます。上記のキャプチャ回避代入を参照してください。

β-還元（ベータ還元）は関数適用の考え方を捉えたものである。β-還元は置換の観点から定義される。すなわち、(λ x . M ) Nのβ-還元はM [ x  := N ]である。^[b]

たとえば、2、7、× のエンコードを想定すると、次の β 縮小が得られます: (λ n . n × 2) 7 → 7 × 2。

β-還元は、カリー・ハワード同型性を介して、自然演繹における局所還元の概念と同じであると見ることができます。

η-還元（イータ還元）は拡張性^[24]の考え方を表現しており、この文脈では、2つの関数が同じであるためには、すべての引数に対して同じ結果を返す必要があるというものである。η-還元は、 xがf内で自由に現れない場合は常に、λx.fxとfの間で変換を行う。

η-還元は、カリー・ハワード同型性を介して、自然演繹における局所完全性の概念と同じであると見ることができます。

型なしラムダ計算の場合、書き換え規則としての β 還元は、強く正規化することも弱く正規化することもありません。

しかし、β 還元は α 変換まで進むと合流することが示されます(つまり、2 つの正規形は、一方を他方に α 変換できる場合は等しいとみなします)。

したがって、強く正規化する項と弱く正規化する項はどちらも、一意の正規形を持ちます。強く正規化する項の場合、どの削減戦略でも正規形が得られることが保証されますが、弱く正規化する項の場合、一部の削減戦略では正規形を見つけられない場合があります。

基本的なラムダ計算は、次のサブセクションi、ii、iii、および§ ivに 示すように、算術、ブール値、データ構造、および再帰をモデル化するために使用できます。

ラムダ計算で自然数を定義する方法はいくつかありますが、最も一般的なのはチャーチ数であり、次のように定義できます。

0 := λ f .λ x . x

1 := λ f .λ x . f x

2 := λ f .λ x . f ( f x )

3 := λ f .λ x . f ( f ( f x ))

など。または、上記の表記法で示した代替構文を使用します。

0 := λ fx . x

1 := λ fx . f x

2 := λ fx . f ( f x )

3 := λ fx . f ( f ( f x ))

チャーチ数とは高階関数であり、引数が 1 つの関数fを受け取り、引数が 1 つの別の関数を返します。チャーチ数n は、関数f を引数として受け取り、fのn次合成、つまり関数fをn回合成したものを返す関数です。これはf ^{( n )}と表記され、実際はfのn乗です(演算子として考えた場合)。f ⁽⁰⁾は恒等関数として定義されます。このような繰り返し合成 (単一関数fの) は指数法則に従うため、これらの数を算術に使用できます。 (チャーチのオリジナルのラムダ計算では、ラムダ式の形式パラメータは関数本体に少なくとも 1 回出現する必要があり、上記の0の定義は不可能でした。)

プログラムを分析するときによく役立つチャーチ数nについての考え方の1つは、「 n回繰り返す」という命令として考えることです。たとえば、以下に定義するPAIR関数とNIL関数を使用すると、空のリストから始めて「別のx要素を先頭に追加する」をn回繰り返すことで、すべてxに等しいn要素の（連結）リストを構築する関数を定義できます。ラムダ項は

λ n .λ x . n (ペアx ) NIL

何が繰り返されるか、また、その繰り返される関数がどの引数に適用されるかを変更することで、非常に多くの異なる効果を実現できます。

チャーチ数nを受け取り、fをもう一度適用してn + 1を返す後継関数を定義できます。ここで、「(mf)x」は、関数「f」が「x」に「m」回適用されることを意味します。

SUCC := λ n .λ f .λ x . f ( n f x )

fのm番目の合成とfのn番目の合成を組み合わせると、 fのm + n番目の合成が得られるため、加算は次のように定義できます。

プラス := λ m .λ n .λ f .λ x。m f ( n f x )

PLUSは、 2つの自然数を引数として受け取り、自然数を返す関数と考えることができます。

プラス2 3

そして

5

はβ-等価なラムダ式です。mをnに加算することは1をm回加算することで達成できるので、別の定義は次のようになります。

プラス := λ m .λ n。m成功n  ^[25]

同様に、掛け算は次のように定義できる。

MULT := λ m .λ n .λ f . m ( n f ) ^[21]

あるいは

MULT := λ m .λ n。m (プラスn ) 0

mとnを掛け合わせることは、nを足す関数をm回繰り返し、それをゼロに適用すること と同じである。べき乗はチャーチ数字ではかなり単純な表現で表され、すなわち

POW := λ b .λ e . e b ^[1]

正の整数nに対してPRED n = n − 1、PRED 0 = 0で定義される先行関数はかなり難しい。式

PRED := λ n .λ f .λ x。n (λ g .λ h . h ( g f )) (λ u . x ) (λ u . u )

は、T が(λ g .λ h . h ( g f ))を表す場合、n > 0 に対してT ^{( n )} (λ u . x ) = (λ h . h ( f ^{( n −1)} ( x )))であることを帰納的に証明することで検証できます。PREDの他の 2 つの定義を以下で示します。1 つは条件文を使用し、もう 1 つはペアを使用します。先行関数を使用すると、減算は簡単です。定義

SUB := λ m .λ n。n PRED m、

SUB m n は、m > nの場合はm − n を返し、それ以外の場合は0 を返します。

慣例により、ブール値TRUEとFALSEには次の 2 つの定義 (Church ブール値と呼ばれる) が使用されます。

真 := λ x .λ y . x

偽 := λ x .λ y . y

次に、これら 2 つのラムダ項を使用して、いくつかの論理演算子を定義できます (これらは単なる可能な定式化であり、他の表現も同様に正しい可能性があります)。

そして := λ p .λ q . p q p

または := λ p .λ q . p p q

NOT := λ p . p偽 真

IFTHENELSE := λ p .λ a .λ b。p a b

これで、次のような論理関数を計算できるようになりました。

そして真実偽り

≡ (λ p .λ q . p q p ) TRUE FALSE → _β TRUE FALSE TRUE

≡ (λ x .λ y . x ) FALSE TRUE → _β FALSE

AND TRUE FALSE はFALSEと同等であることがわかります。

述語はブール値を返す関数です。最も基本的な述語はISZEROで、引数がチャーチ数値0の場合はTRUEを返し、引数がその他のチャーチ数値の場合は FALSE を返します。

ISZERO := λ n。n (λ x .FALSE) TRUE

次の述語は、最初の引数が 2 番目の引数以下かどうかをテストします。

LEQ := λ m .λ n .ISZERO (SUB m n )、

m = nなので、LEQ m nかつLEQ n mであれば、数値的等価性の述語を構築するのは簡単です。

述語の利用可能性と、上記のTRUEおよびFALSEの定義により、ラムダ計算で「if-then-else」式を記述することが簡単になります。たとえば、先行関数は次のように定義できます。

PRED := λ n。n (λ g .λ k .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) 0

これは、 n (λ g .λ k .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0)がn > 0 に対してn − 1 の加算関数であることを帰納的に示すことで検証できます。

ペア (2 組) は、ペアの Church エンコーディングを使用してTRUEとFALSEで定義できます。たとえば、PAIR はペア ( x、y ) をカプセル化し、FIRST はペアの最初の要素を返し、SECOND は2 番目の要素を返します。

ペア := λ x .λ y .λ f . f x y

最初 := λ p . p真

2番目 := λ p . p偽

NIL := λ x .TRUE

NULL := λ p。p (λ x .λ y .FALSE)

リンク リストは、空のリストの場合は NIL、要素と小さいリストのペアの場合は NIL として定義できます。述語NULL は、値NILをテストします。(または、NIL := FALSEの場合、構文l (λ h .λ t .λ z .deal_with_head_ h _and_tail_ t ) (deal_with_nil)によって明示的な NULL テストが不要になります)。

ペアの使用例として、 ( m , n )を( n , n + 1)にマッピングするシフト・インクリメント関数は次のように定義できます 。

Φ := λ x .PAIR (SECOND x ) (SUCC (SECOND x ))

これにより、おそらく前身関数の最も透過的なバージョンを提供できるようになります。

PRED := λ n .FIRST ( n Φ (PAIR 0 0)).

ラムダ計算には、かなりの数のプログラミング イディオムがあります。これらの多くは、もともとラムダ計算をプログラミング言語セマンティクスの基礎として使用するという文脈で開発され、実質的にはラムダ計算を低レベル プログラミング言語として使用していました。いくつかのプログラミング言語にはラムダ計算 (または非常に類似したもの) がフラグメントとして含まれているため、これらのテクニックは実際のプログラミングでも使用されていますが、わかりにくい、または外国語として認識される可能性があります。

ラムダ計算では、ライブラリは、以前に定義された関数のコレクションの形をとります。ラムダ項は特定の定数にすぎません。純粋なラムダ計算では、すべてのアトミック ラムダ項が変数であるため、名前付き定数の概念はありませんが、定数の名前として変数を用意し、抽象化を使用してその変数を本体にバインドし、その抽象化を意図した定義に適用することで、名前付き定数をエミュレートできます。したがって、f を使用して、 M (別のラムダ項、"メイン プログラム") 内のN (明示的なラムダ項)を意味するには、次のようにします。

(λf . M ) Nの

著者は、let、^[k]などの構文糖を導入して、上記をより直感的な順序で記述できるようにすること が多い。

f = N in Mとする

このような定義を連鎖させることで、ラムダ計算「プログラム」を 0 個以上の関数定義として記述し、その後にそれらの関数を使用してプログラムの本体を構成する 1 つのラムダ項を記述することができます。

このletの注目すべき制限は、名前fがNで定義されていないことです。これは、 N が抽象バインディングfのスコープ外になるためです。つまり、再帰関数定義をletのNとして使用することはできません。letrec ^[l]構造を使用すると、再帰関数定義を記述できます。

再帰とは、関数が自分自身を呼び出す定義です。定義が自分自身の中に値によって含まれると、値全体が無限サイズになります。再帰をネイティブにサポートする他の表記法では、関数定義を名前で参照することでこれを克服しています。ラムダ計算ではこれを表現できません。ラムダ計算ではすべての関数が匿名であるため、同じ値を定義するラムダ項内で、まだ定義されていない値を名前で参照することはできません。ただし、ラムダ式は、たとえば  (λ x . x x ) Eのように、自分自身を引数として受け取ることができます。ここで、E は抽象化である必要があり、そのパラメーターを値に適用して再帰を表現します。

再帰的に定義された 階乗関数F( n )を考える。

n = 0の場合はF( n ) = 1、それ以外の場合はn × F( n −1)。

この関数を表すラムダ式では、パラメータ（通常は最初のパラメータ）はラムダ式自体を値として受け取るものと想定されるため、それを呼び出す（引数に適用する）と再帰が発生します。したがって、再帰を実現するには、自己参照として意図された引数（ここではrと呼びます）を、関数本体内の呼び出しポイントで常に自分自身に渡す必要があります。

G := λ r . λ n .( n = 0の場合は1、それ以外の場合はn × ( r r ( n −1)))

r r x = F x = G r xが  成り立つので、  r = Gであり   、

F := GG = (λ x . x x ) G

自己アプリケーションはここでレプリケーションを実現し、関数のラムダ式を引数値として次の呼び出しに渡し、そこで参照および呼び出しできるようにします。

これで問題は解決しますが、各再帰呼び出しを自己適用として書き直す必要があります。書き直す必要のない汎用的なソリューションが欲しいです。

G := λ r . λ n .( n = 0の場合は1、それ以外の場合はn × ( r ( n −1)))

r x = F x = G r xが  成り立つので、  r = G r =: FIX Gとなり   、

F := FIX G  ただし  FIX g  := ( rただしr = g r ) = g (FIX g )

つまり、  FIX G = G (FIX G) = (λ n .(1, if n = 0; else n × ((FIX G) ( n −1))))

最初の引数が再帰呼び出しを表すラムダ項 (ここではGなど) が指定されると、固定小数点コンビネータFIX は、再帰関数 (ここではF )を表す自己複製ラムダ式を返します。関数は、呼び出されるたびに実行されるように事前に作成時に自己複製が準備されているため、どの時点でも明示的に関数自体に渡す必要はありません。したがって、元のラムダ式(FIX G)は呼び出し時点でそれ自体の内部で再作成され、自己参照を実現します。

実際、このFIX演算子にはさまざまな定義が可能ですが、最も単純なものは次のとおりです。

Y  := λ g .(λ x . g ( x x )) (λ x . g ( x x ))

ラムダ計算では、Y g はg  の不動点であり、次のように展開されます。

Y g

(λ h .(λ x . h ( x x )) (λ x . h ( x x ))) g

(λ x . g ( x x )) (λ x . g ( x x ))

g ((λ x . g ( x x )) (λ x . g ( x x )))

g ( Y g )

さて、階乗関数への再帰呼び出しを実行するには、単に( Y G) n を呼び出します。ここで、 n は階乗を計算する数です。たとえば、 n = 4 の場合、次のようになります。

（YG）4

G ( Y G) 4

(λ r .λ n .(1, n = 0の場合; それ以外の場合はn × ( r ( n −1)))) ( Y G) 4

(λ n .(1, n = 0の場合; それ以外の場合はn × (( Y G) ( n −1)))) 4

4 = 0の場合は1、それ以外の場合は4 × (( Y G) (4−1))

4 × (G ( Y G) (4−1))

4 × ((λ n .(1, n = 0の場合; それ以外の場合はn × (( Y G) ( n −1)))) (4−1))

4 × (1, 3 = 0の場合; それ以外の場合は3 × (( Y G) (3−1)))

4 × (3 × (G ( Y G) (3−1)))

4 × (3 × ((λ n .(1, n = 0の場合; それ以外の場合はn × (( Y G) ( n −1)))) (3−1)))

4 × (3 × (1, 2 = 0の場合; それ以外の場合は2 × (( Y G) (2−1))))

4 × (3 × (2 × (G ( Y G) (2−1))))

4 × (3 × (2 × ((λ n .(1, n = 0の場合; それ以外の場合はn × (( Y G) ( n −1)))) (2−1))))

4 × (3 × (2 × (1、1 = 0の場合; それ以外の場合は1 × (( Y G) (1−1)))))

4 × (3 × (2 × (1 × (G ( Y G) (1−1)))))

4 × (3 × (2 × (1 × ((λ n .(1, n = 0の場合; それ以外の場合はn × (( Y G) ( n −1)))) (1−1)))))

4 × (3 × (2 × (1 × (1、0 = 0の場合;それ以外の場合は0 × (( Y G) (0−1))))))

4 × (3 × (2 × (1 × (1))))

24