λ計算

programming-paradigmcomputer-sciencetype-theory

「関数の定義と適用」だけですべての計算を表現する形式体系。1930年代にアロンゾ・チャーチが考案。

プログラマ向けの一言

アロー関数だけでプログラムを書く世界。 if も for も数値もない。あるのは (x) => ... と関数呼び出しだけ。それだけでチューリング完全。

コードで理解する

// λ計算の3つの要素:
// 1. 変数:      x
// 2. 抽象(λ):   (x) => body    ← 関数を作る
// 3. 適用:      f(x)           ← 関数を呼ぶ
// これだけ。

// λ計算で数を表現する（チャーチ数）
// 数 = 「関数を n 回適用する関数」
const zero = (f: Function) => (x: any) => x;              // 0回適用
const one  = (f: Function) => (x: any) => f(x);           // 1回適用
const two  = (f: Function) => (x: any) => f(f(x));        // 2回適用
const three = (f: Function) => (x: any) => f(f(f(x)));    // 3回適用

// 普通の数に変換して確認
const toNumber = (n: Function) => n((x: number) => x + 1)(0);
toNumber(zero);  // 0
toNumber(three); // 3

// 足し算
const add = (m: Function) => (n: Function) => (f: Function) => (x: any) =>
  m(f)(n(f)(x));
toNumber(add(two)(three)); // 5

// 真偽値
const TRUE  = (a: any) => (_b: any) => a;  // 2つの選択肢から1つ目を選ぶ
const FALSE = (_a: any) => (b: any) => b;  // 2つの選択肢から2つ目を選ぶ
const IF    = (cond: Function) => (then_: any) => (else_: any) => cond(then_)(else_);
IF(TRUE)("yes")("no");  // "yes"
IF(FALSE)("yes")("no"); // "no"

簡約

λ計算の「計算」= 式を書き換えるルール。詳細は 簡約 を参照。

// β簡約（ベータ簡約）: 関数適用を実行する
// ((x) => x + 1)(3)  →  3 + 1  →  4
// 引数を本体に代入するだけ

// これがλ計算における「計算の1ステップ」

評価戦略 — どの簡約基（redex）を先に潰すか

1つの式に複数の β-redex があるとき、どれから簡約するかが評価戦略。同じ式でも戦略で停止性が変わる。

戦略簡約順引数の扱い身近な対応
正規順序 (normal order)最も外側・最も左の redex から引数を未評価のまま関数に代入名前呼び（call-by-name）
作用順序 (applicative order)最も内側の redex から引数を先に正規形まで評価値呼び（call-by-value）
// (λx. λy. x) ((λz.z) 1) (loop)   ← loop は発散する式
// 正規順序: 外側の λx を先に適用 → 第2引数 (loop) に触れず 1 を返す【停止】
// 作用順序: 引数を先に評価 → loop を評価しようとして発散【停止しない】

正規化定理：式に正規形が存在するなら、正規順序は必ずそれに到達する（作用順序は到達しないことがある）。正規順序が「最も安全」と言われる所以。

合流性（Church–Rosser）

λ計算は合流的（confluent）：ある式から複数の簡約経路を取っても、それぞれの結果はさらに簡約すれば共通の式に合流できる。

      e
     / \
    e₁   e₂      どちらの順で簡約しても…
     \ /
      e₃         …同じ e₃ に到達できる（菱形性質）

帰結として 正規形は（存在すれば）一意。つまり「計算結果」は簡約順序に依存しない。戦略が変えるのは「結果に到達できるか（停止性）」だけで、到達したときの値そのものは同じ。これが「λ計算は決定的な計算結果を持つ」ことの形式的保証。

型なし vs 型付き

型なしλ計算単純型付きλ計算 (STLC)
表現力チューリング完全チューリング不完全
停止性発散しうる（Ω = (λx.xx)(λx.xx)）強正規化：必ず停止する
不動点Y コンビネータで再帰を表現組めない（再帰は fix を原始追加）
対応—カリー＝ハワード：型=命題、項=証明

型を付けると Ω のような自己適用が型エラーで弾かれ、その代償として（純粋な STLC では）無限ループが書けなくなる＝強正規化。だから依存型や定理証明系の言語（停止する＝証明になる）は型付きλ計算の拡張の上に立つ。実用言語は fix / letrec を原始追加してチューリング完全性を取り戻す。

押さえどころ（カード化候補）

関連

Graph

Backlinks