1 ラムダ計算の基礎
ラムダ計算は、関数を記号操作の対象として扱うための形式体系である。数値計算そのものよりも、式の構造と変形の規則に重点が置かれ、後の関数型プログラミングや計算理論の土台となった。
1.1 ラムダ抽象
ラムダ抽象は、入力を受け取って処理を行う関数を表す記法である。通常は、引数名を明示し、その変数を用いて本体の式を記述する。
1.1.1 変数
変数は、式の中で値や対象を指し示す記号である。ラムダ計算では、変数は単独でも現れ、式の部品として機能する。
1.1.2 抽象と適用
抽象は、変数を受け取る関数の定義を表し、適用はその関数に実際の引数を与える操作である。両者の組合せにより、関数呼び出しに相当する式が作られる。
1.2 式の構成
ラムダ計算の式は、変数、抽象、適用という少数の要素から組み立てられる。これらの構成規則によって、複雑な関数表現も簡潔に記述できる。
1.2.1 項
項は、ラムダ計算における式の総称である。単一の変数からなるものもあれば、抽象や適用を含む複合的なものもある。
1.2.2 自由変数と束縛変数
自由変数は、外部から意味が与えられる変数であり、束縛変数は特定の抽象の内部で意味が固定される変数である。この区別は、置換や簡約の正しさを判断するうえで重要である。
1.3 代入の考え方
ラムダ計算では、関数適用の際に引数を本体へ反映させる発想が中心となる。これが後に、β簡約の直観的な理解へとつながる。
1.3.1 置換の直観
置換は、式の中のある変数を別の式で置き換える操作である。関数に実引数を与えると、その引数が本体中の対応する変数に反映されると考えると理解しやすい。
1.3.2 変数捕獲の回避
単純な置換では、外側の変数が内側の束縛に取り込まれて意味が変わることがある。これを避けるため、必要に応じて変数名を変更してから代入を行う。
2 β簡約の定義
β簡約は、ラムダ抽象を引数に適用した式を、より直接的な形へと変形する規則である。ラムダ計算における実行の中心に位置し、関数適用の結果を形式的に与える。
2.1 基本規則
基本規則は、関数の定義と引数の組合せが、どのように一段階で書き換えられるかを示す。これにより、計算の進行が明確になる。
2.1.1 適用可能な形
β簡約が適用されるのは、抽象がそのまま引数に結びついた形である。一般に、関数本体が引数によって置き換えられる構造を持つ場合に成立する。
2.1.2 簡約の結果
簡約の結果では、抽象部分は取り除かれ、引数が本体中の対応箇所へ反映される。これによって、式は一段階だけ具体的な表現に近づく。
2.2 代入の形式化
直観的な置換を厳密に扱うために、ラムダ計算では代入を形式的に定義する。これにより、曖昧さを避けて機械的な変形が可能になる。
2.2.1 置換記号
置換記号は、どの変数をどの式で置き換えるかを記述するための表記である。通常は、対象となる変数と代入される項を組にして表す。
2.2.2 α変換との関係
α変換は、束縛変数の名前を意味を変えずに変更する操作である。代入の前にα変換を用いることで、変数捕獲を避け、β簡約を安全に行える。
2.3 β変換との区別
β簡約は実際の書き換えを指し、β変換はそれを含むより広い等価関係として扱われることがある。両者は密接だが、用法には文脈上の差がある。
2.3.1 β簡約
β簡約は、一回の書き換えとしての操作を意味する。計算手順の各段階は、この規則の反復として理解できる。
2.3.2 β同値
β同値は、互いにβ簡約を繰り返して到達できる式どうしの関係である。式の見かけが違っても、計算内容が同じとみなされる場合に用いられる。
3 β簡約の性質
β簡約は単なる変形規則ではなく、式の最終形や簡約の進め方に関する多様な性質を持つ。これらは、計算がどこで止まるか、あるいはどの順序で進めるかを考える際に重要である。
3.1 正規形
正規形は、それ以上β簡約できない式の形を指す。計算の最終結果に相当することが多く、標準的な到達点として扱われる。
3.1.1 β正規形
β正規形は、β簡約の対象となる部分を含まない項である。すでにこれ以上の書き換えが不要な状態を表す。
3.1.2 既約項
既約項は、与えられた簡約規則ではこれ以上変形できない項である。β簡約の文脈では、β正規形とほぼ同じ意味で使われる。
3.2 簡約順序
簡約順序は、どの部分から先に書き換えるかを定める考え方である。順序の違いは、途中経過や効率に影響を与えることがある。
3.2.1 外側優先
外側優先では、式の外側にある適用を先に簡約する。最終結果に早く到達できる場合があり、理論的な解析でも扱われる。
3.2.2 内側優先
内側優先では、内部の赤exに当たる部分を先に処理する。必要以上に計算を進めることもあるが、評価の一形態として理解される。
3.3 終了性と合流性
終了性は簡約が有限回で止まるかどうかを示し、合流性は異なる変形経路が同じ結果へ合流するかを表す。これらは、ラムダ計算の安定した振る舞いを理解するうえで欠かせない。
3.3.1 強正規化
強正規化は、どの簡約列を選んでも必ず有限回で停止する性質である。全ての経路が終端に達するため、計算の予測可能性が高い。
3.3.2 弱正規化
弱正規化は、少なくとも一つの簡約順序を選べば正規形に到達できる性質である。停止する道筋が存在することを意味し、強正規化より条件が緩い。
3.3.3 クリーネ・ロッサー性
クリーネ・ロッサー性は、異なる簡約経路をたどっても、後で共通の結果に到達できるという性質である。ラムダ計算における式の同一視を支える重要な結果として知られる。
4 応用と関連分野
β簡約は、純粋な理論概念にとどまらず、プログラム実行の解釈や型付き体系の分析に広く関係する。特に、関数の評価、式の同値性、計算可能性の研究に深く結びついている。
4.1 関数型プログラミング
関数型プログラミングでは、計算を関数の合成と評価として記述する。β簡約は、その動作を抽象的に説明する基本モデルとなる。
4.1.1 評価戦略
評価戦略は、式をどの順番で計算するかを定める方針である。β簡約は、戦略ごとの違いを形式的に比較するための基盤となる。
4.1.2 遅延評価
遅延評価は、必要になるまで計算を先送りする方式である。ラムダ計算では、どの簡約を先に行うかという問題として表現できる。
4.2 型理論
型理論では、式がどのような値を表すかを体系的に管理する。β簡約は、型付けされた式の変形や意味保存を考える際に利用される。
4.2.1 単純型付きラムダ計算
単純型付きラムダ計算は、各項に型を与えて整合性を保つ拡張である。型の制約により、意味のない式を排除しやすくなる。
4.2.2 項の同値性
項の同値性は、見かけが異なる式が同じ計算内容を持つかどうかを扱う。β同値は、この判断基準の中心的な要素である。
4.3 計算論
計算論は、計算そのものの性質を数学的に研究する分野である。β簡約は、計算手続きの抽象モデルとして広く利用される。
4.3.1 計算可能性
計算可能性は、ある問題が有限の手順で解けるかを問う概念である。ラムダ計算では、β簡約によって到達可能な結果として表現される。
4.3.2 チャーチ＝ロッサーの定理
チャーチ＝ロッサーの定理は、ラムダ計算における変形の分岐があっても、適切に進めれば同じ結論に合流できることを述べる。これは、式の等価性と簡約の整合性を支える基本定理である。