このテキストは、λ計算に関する古典的なモノグラフの非常に簡潔な大要です（H. Barendregt、「Lambda calculus。その構文とセマンティクス」、G。E. Mintsによる英語からの翻訳、A。S. Kuzichev、モスクワ、「Mir」 、1985）。 このトピックの体系的な研究に着手する予定のすべての人々にとって興味深いことが判明する可能性があります。すでに一般的にそれに慣れていますが、主要なモノグラフの複雑な構造のためにそれを延期しました。その定義と主な結果はかなり散在しています。 ここでは、反対に、絶対に線形で、そしてもちろん、比較できないほど短く、不必要な定義と例を避け、順番に元のテキストの近くに記載されている必要な用語、表記法、およびステートメントに焦点を当てようとします。 まず、システムλβη、つまり古典的な型のない拡張λ計算を定義します。 次に、組み合わせ論理、固定小数点定理、および構文糖に進みます。 最後に、あらすじの最後の部分は、明らかな矛盾を説明するために設計された、このシステムの式のトポロジの構築です。式のセット自体へのマッピングは、カウント可能な場合、このセット自体に含まれます。 実際、セットには、式が連続マッピングである適切なトポロジが備わっています。
理論
λ-
式 Λのセットは、
変数から帰納的に構築され
ますx、y、z ...∈Λ
抽象化の使用
M∈Λ⇒λx.M∈Λ
および
アプリケーションM、N∈Λ⇒MN∈Λ、
アプリケーションは左結合型です：
（M）≣M、MNP≣（MN）P.
再帰的推移関係Μ⊂Nは、Mが式Nの
部分式であることを意味します。
M⊂M⊂λx.M;
M⊂MN⊃N;
M⊂N∧N⊂P⇒M⊂P.
FV（M）は、式Mの
自由変数のセットです。
FV（x）≣{x};
FV（λx.M）≣FV（M）∖{x};
FV（MN）≣FV（M）∪FV（N）。
自由ではない変数は
バウンドと呼ば
れ 、別の変数に置き換えることができます（このような変換はα変換と呼ばれます）。
y∉FV（M）⇒λx.M≣λy.M[x：= y]、ここでM [x：= N]は
置換の結果です：
x [x：= P]≣P;
y [x：= P]≣y;
（λx.M）[x：= P]≣λx.M;
（λy.M）[x：= P]≣λy.M[x：= P];
（MN）[x：= P]≣M [x：= P] N [x：= P]。
4番目の段落では、条件「x≢yおよびy∉FV（P）」を特に規定する必要はありません。変数に関する合意によって満たされるためです。用語M
1 、...、M
nが特定の数学的文脈で発生する場合、それらの関連変数は、自由変数とは異なるように選択されます。
セットFV（M）が空の場合、Mは
コンビネーターと呼ばれます。 すべてのコンビネータのセットは、Λ0で示され
ます 。
Λ0≣{M∈Λ| FV（M）=∅}。
次の比率β、η、βηは
減少です。
β≣{（（λx.M）N、M [x：= N]）| M、N∈Λ};
η≣{（λx.Mx、M）| M∈Λ、x∉FV（M）};
βη≣β∪η。
穴の部分式が
コンテキストと呼ばれる式はC []で示され、C [M]は式[M]をC []のコンテキストの穴に置き換えた結果です。
σが還元の場合、式MはifN：（M、N）∈σの場合、σ-redexです。 σ-
変換 "=
σ "についても説明できます。
（M、N）∈σ⇒C [Μ]→
σC [N];
M↠σM;
M→σN⇒M↠σN;
M→σN∧N→σP⇒M↠σP;
∃P：M↠σP∧N↠σP⇒M =σN
σ-
正規形は、expression：M→σΝの場合、式isです。 拡張λ計算では、redexによってβη-redex
を意味し、
標準形によって、βη-normal形式
を意味します。 さらに、M↠Nの場合、Mの正規形はNであると言われ
ています。さらに、βη変換は通常「=」で表され、これは偶然ではありません。正式には、システムλβηは方程式論です。 そのような理論には論理がないので、それらの一貫性はやや異なって定義されます。
等式は、M = Nという形式の式と見なされます。ここで、M、Nはλ式です。 MとNがコンビネータである場合、そのような等式は
閉じられます。 Tを公式が等式である形式理論とする。 そして、彼らは、すべての閉じた等式がTで証明可能でない場合、Tは
一貫していると言います（そして、彼らはCon（T）を書きます）。 そうでなければ、彼らはTが
矛盾していると言います。 λβηを考慮する理由の1つは、この理論に特定の完全性があるということです。 等式理論Tは、理論の言語でM = Nが等しいか、M = Nが証明可能であるか、またはT +（M = N）が矛盾する場合、
ヒルベルトポスト完全 （HP
完全と略す）と呼ばれます。 HP完全理論は、一次論理のモデル理論における最大一貫理論に対応します。
戦略は、F M：M↠F（M）となるようなマッピングF：Λ→Λです。
ワンステップ戦略の場合、M：F→M（M）が成り立ちます。 戦略は、正規形Nを持つ式Mに対して、ある数nでF
n （M）≣Nが成り立つ場合、
正規化と呼ばれます。
左簡約 F
lは、最も単純な1ステップ正規化戦略の1つです。 「Λ」は、他のβ-redexeよりも左にテキストで、β-redexeがそうでない場合は
左に η-redexである。 したがって、2つの項に共通の正規形がある場合、左簡約を使用すると、対応する式の証明を有限の多くの単純なステップで取得できます。 数式が証明できない場合、プロセスはまったく完了しないか、別の標準形式で終了します。
砂糖
コンビネータのセットTheは、アプリケーションによるクロージャとして最小のセットΞ
+を
生成します。
Ξ⊆Ξ
+ ;
M、N∈Ξ
+ ⇒ΜΝ∈Ξ
+ 。
ΞM∈Λ0：setN∈Ξ
+ ：M = Nの場合、集合Aは
基底と呼ばれ
ます 。
SとKを使用して、任意の抽象化をモデル化できます。
S≣λx.λy.λz.xz（yz）;
K≣λx.λy.x;
I≣λx.x= SKK;
x∉FV（P）⇒λx.P= KP;
λx.PQ= S（λx.P）（λx.Q）。
したがって、コンビネータKおよびSは基底を定義します。 Mの任意の組み合わせ子は、λ式の形式ではなく、公理を使用して記述されることがよくあります。 たとえば、
組み合わせロジック CLの正式なシステムは、2つの公理によって定義されます。
KPQ = P;
SPQR = PR（QR）。
単一点ベースが存在します：これらのベースの1つはコンビネーターによって定義されます
X≣λx.xKS K.
実際、XXX = KおよびX（XX）= Sであることを確認するのは簡単です。
標準のコンビネータは、組み合わせロジックの基礎を構成するだけでなく、他の多くの有用なλ式も構成すると見なされます。 最初の例の1つは通常、通常の形状を持たない単純なコンビネーターによって与えられます。
Ω≣ωω、ここでω≣λx.xx。
さらに、真理値T≣KおよびF≣λx.Iは、BMNによって「BならばM、そうでなければN」という操作を示すことを可能にします。 実際、B = Tの場合、式はMです。 B = Fの場合、式はNです。BがTおよびFと異なる場合、結果は任意です。
集合論のように、λ計算では順序ペアを定義できます。
[M、N]≣λx.xMN、[M、N] T↠M、[M、N] F↠N.
デジタルシステムは、コンビネータ⎡0⎤、⎡1⎤、⎡2sequence ...のシーケンスであり、
それに続く S
+とゼロゼロの
チェックがあります 。
S
+ ⎡n⎤=⎡n+1⎤;
ゼロ⎡0⎤= T;
ゼロ⎡n+1⎤= F
選択された
標準デジタルシステム
⎡0⎤≣I;
S
+ ≣λx。[F、x];
ゼロ≣λx.xT.
デジタルシステムは、すべての再帰関数がそれに対して定義可能である場合に
適切と呼ばれます。 このプロパティを実現するには
、優先度関数 P-
が検出されれば十分です。 標準的なデジタルシステムの場合、これはコンビネータです
P
- ≣λx.xF.
λ計算の主な結果の1つは不動点定理です。任意のFに対して、FX = XとなるXが存在します。その証明は建設的です。 W≣λx.F（xx）およびX≣W Wとしましょう。次に、必要に応じてX≣（λx.F（xx））W = F（WW）= FXとします。 読者は、この定理の証明に1つの特徴があることに気付いたかもしれません。 FX = Xを確立するために、用語Xから始めてFXに変換します。逆も同様です。
固定小数点コンビネーターは、任意のFに対してMF = F（MF）であるような用語Mです。つまり、MFはFの固定小数点です。ほとんどの場合、固定小数点コンビネーターの例は次のとおりです。
Y≣λf。（Λx.f（xx））（λx.f（xx））。
固定小数点コンビネーターを使用すると、次のタイプの問題を解決できます。
F xy = F yx F
実際、ソリューションは簡単です。
F xy = F yx Fは、等式F =λx.λy.Fyx Fから得られます。
そして、F =（λf.λx.λy.fyxf）F.
ここで、F≣Y（λf.λx.λy.fyxf）を入力します。これで問題ありません。
トポロジー
いくつかの表記を紹介します。 最初に、
メタラムダの抽象化 λx.f（x）は、集合論関数fの名前のない表記です。たとえば、（λx.x
2 + 1）（3）= 10です。次に、有限シーケンスの
コードのセットを定義します（標準自然数によるエンコード）
Seq = {<n
1 、...、n
k > | k∈N、n
1 、...、n k∈N}∪{<>};
lh（<>）= 0;
α= <n
1 、...、n
k >∈Seq⇒lh（α）= k;
α= <m
1 、...、m
p >、β= <n
1 、...、n
q >∈Seq⇒a * b = <m
1 、...、m
p 、n
1 、...、n
q >;
α= <m
1 、...、m
p >、β= <n
1 、...、n
q >∈Seq∧p≤q∧m
1 = n 1∧...∧m
p = n p⇒α≤β
D =（D、⊑）を再帰関係withの半順序集合とします。 次に、サブセットX⊆Dは、次の場合に
有向と呼ばれます。
X≠∅∧∀x、y∈X：∃z∈X：x⊑z∧y⊑z。
さらに、任意の有向サブセットX⊆Dについて、極大∈X∈Dが存在し、
底 ⊥がある場合、Dは
完全と呼ばれます。
∃⊥∈D：∀x∈D：⊥⊑x。
完全に部分的に順序付けられたセット（D、⊑）
のスコットトポロジは、次のように定義されます。セットO⊆Dは、
1）x∈O∧x⊑y⇒y∈O;
2）X⊆D∧⊔X∈O⇒X∩O≠∅。
部分マップ φ：X↝Yは、Dom（φ）⊆Xの定義の領域であるよう
なマップ φです。x∈Xの表記法φ（x）↓は、φ（x）が定義されていること、つまり、x∈Dom（φ ）; φ（x）↑は、φ（x）が定義されていないこと、つまりx∉Dom（φ）を意味します。
Σが特定のシンボルのセットである場合、
部分的にΣラベルが付けられたツリーは、部分マッピングφです：Seq↝Σ×N
1）φ（σ）↓ττ≤σ⇒φ（τ）↓;
2）φ（σ）= <a、n>⇒∀k≥n：φ（σ* <k>）↑。
部分的にΣラベル付けされたツリーφの
基礎となるヌードツリーはツリーです。
Tφ = {<>}∪{σ| σ=σ '* <k>∧φ（σ'）= <a、n>∧k <n}。
σ∈Tφかつφ（σ）= <a、n>の場合、aは
ノード σで
ラベルと呼ばれ
ます 。 σ∈Tの場合、φφ（σ）↑の場合、ノードσはラベル付けされていません。 部分的にマークされたツリーは大文字で示され、A（α）↑のときσ∈T
AおよびA（α）=⊥の代わりにσ∈Aを書きますが、それでもα∈Aです。
Σ= {λx1
. ...λxn .x | n≥0、x
1 、...、x
n 、x∈Λ}の場合、部分的にΣラベル付けされたツリーは
Boehmタイプツリーと呼ばれ
ます 。 このようなすべてのツリーのセットをBで示し
ます。ノード α
から始まるAの
サブツリーは、 Aα=λβ.A（α*β）です。 明らかに、∀A∈B：∀α：Aα∈B
組み合わせMは次の場合に
解くことが
できます
∃n：∃N1、...、N n∈Λ0：MN
1 ... N
n = I
たとえば、Y（KI）= KI（Y（KI））= Iであるため、固定小数点コンビネーターは決定可能です。一方、Ωは解決不可能です。 任意のλ式は、コンビネータλx1
. ...λxn .Mの場合に
解くことができ
ます 。ここで、{x
1 、...、x
n } = FV（M）。
λ式Mは、次の形式を持つ場合、
主要な正規形です。
M≣λx1
. ...λxn .x M
1 ... M
m 、m、n≥0。
M = Nの場合
、 M
には頭標準形Nがあると言われています。左の縮小によって最初に達成される式
の頭標準形は、メイン形と呼ばれます。
Wadsworthは、主要な正規形を持たないλ式のクラスを導入し、このクラスの要素はλ計算で無意味な式と見なされるべきであると主張しました。 また、次の重要な結果が得られます。λ式は、先行正規形がある場合にのみ決定可能です。 したがって、Mの不溶性から、式N
1 、...、N
nの場合、式MN
1 ... N
nは正規形を持たないことになります。
BT（M）で表される項Mのベームツリーは、次のように定義されたタイプのベームツリーです。
1）Mが解けない場合、∀σ：BT（Μ）（σ）↑、
2）Mが可解であり、プリンシパルプリンシパル正規形λx1 ...λxn .x M
0 ... M
m-1を持っている場合
BT（M）（<>）= <λx1
. ...λxn .x、m>;
k <m⇒BT（M）（<k> *σ）= BT（M
k ）（σ）;
k≥m⇒BT（M）（<k> *σ）↑。
スコットトポロジで完全に部分的に順序付けられたセットB =（B、⊆）を考えます。 セットΛ上
のツリートポロジは、マップBTが連続する最小のトポロジです。Λ→B。言い換えると、Λの開いたサブセットの形式はBT
-1 （O）です。ここで、OはBのスコットトポロジで開いています。
木のトポロジーを使用して、トポロジー計算でλ計算に関連する通常の概念を表現できます。 たとえば、正規形は孤立した点であり、不溶性の式
はコンパクト化の点であることが
わかります 。つまり、そのような点だけがトポロジ空間そのものである点です。
Λ上のツリーのトポロジでは、アプリケーションと抽象化が連続していることが証明されており、アプリケーションにとってこれは興味深い結果を伴う重要な結果です。 たとえば、可解な項の集合SolΛΛは開いています。 実際、完全に部分的に順序付けられたセットでは、セット{x | x≠⊥}スコットが開いています。 したがって、セットSol = BT
-1 {A | A≠⊥}はΛで開いています。