λ計算

構文

まず無限個の変数が与えられているとする。変数は通常x, yなどど記述される。変数から出発し、次の操作を繰り返して得られるものをλ式と呼ぶ。

λ抽象

λ式Mと変数xから、式λx. Mを生成する操作。これは、変数xに引数を受け取り、値Mを返す関数を意図する。Mに含まれる変数xはこのλにより束縛されるという。ただし、すでに束縛されているものは除く。

関数適用

二つのλ式M, Nを並べて結合した式MNを作る操作。これは式Mが表す関数に引数としてNを与えることを意図する。

またλ抽象や関数適用の範囲を明確にするために括弧を用いる。

例: (λx. xx)(λx. xx),λf.(λx.(f (x x)) λx.(f (x x)))

計算ルール

M[N/x]はMに含まれる束縛されていない変数xをλ式Nで置き換えたものとする。

α変換

λ式中のλx. Mの形の持つ式をλy. M[y/x]で置き換えること（「名前の付け替え」の意味を持つ）。

β変換

λ式中の(λx. M)Nの形の持つ式をM[N/x]で置き換えること（関数適用，インライン展開の意味を持つ）．

厳密に言うと、β変換では、Mの中でλ抽象されている変数名を付け替えて、Nに含まれる変数をMのλ抽象が束縛しないようにする。束縛変数の名前の付け替え、つまりα変換で移りあう式は同一視されることが多い。また

η変換

λ式中のλx. Mxの形を持ち、Mにxが含まれない(束縛されている場合は除く)式をMで置き換えること（冗長なλ抽象を消し去る意味を持つ）

を追加することもある。

de Bruijn指数

束縛変数をあるやり方で一意に決めることにより、α変換(およびある意味で束縛変数そのもの)をλ計算から除去できる。これは、コンパイラが局所変数をスタック上の位置として解釈するのと同じである。

チャーチ数

λ計算の中で自然数を表すことができる。

    0 := λ f. λ x. x
    1 := λ f. λ x. f x
    2 := λ f. λ x. f (f x)
    3 := λ f. λ x. f (f (f x)) 

こうすると、足し算はλ m. λ n. λ f. λ x. m f (n f x)、掛け算はλ m. λ n. λ f. m (n f)と表すことができる。

一般に、コンストラクタc1, ..., cnを持つ自由代数は、コンストラクタをci := λa1...λamλc1...λcn.ci a1 ... am (mはciの持つ引数の数)として表すことができる。

条件分岐

ブール値は次のように定義できる。

    TRUE := λ x. λ y. x
    FALSE := λ x. λ y. y

論理演算は

    AND := λ p. λ q. p q FALSE
    OR := λ p. λ q. p TRUE q
    NOT := λ p. p FALSE TRUE

条件分岐は

    IFTHENELSE := λ p. λ x. λ y. p x y 

と定義できる。また、ゼロ判定関数を

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

と定めることにより、自然数についてのゼロ条件判定ができる。

再帰

Y := λf.(λx.(f (x x)) λx.(f (x x)))をYコンビネーターと呼ぶ。Yコンビネーターは任意のλ式Mに対して、YM⇒M(YM)となる性質がある。(⇒はα、β変換の繰り返しを表す。)これを利用して再帰を定義することができる。たとえば、階乗は次のように書ける。

f = λg.λn. if n = 0 then 1 else n * g(n-1)
fact = λn. Y(f) n

足し算、条件分岐、再帰ができることにより一般帰納関数(計算可能な関数)すべてをλ計算で定義できることになる。

チャーチ・ロッサー性

一般に、一つのλ式にはα、β変換を適応する複数の方法がある。よって、あるλ式Mは二つの異なったλ式N1,N2に変換されうる。しかし、N1,N2に適当な順でさらにα、β変換を施すことにより、同一のλ式Lに変換することができる。これをチャーチ・ロッサー性または合流性と呼ぶ。

特に、N1がこれ以上変換できない形(正規形)であった場合を考えると、チャーチ・ロッサー性は正規形が唯一であることを意味する。これは、λ式で表されたプログラムは、演算の順序にかかわらず同一の値を返すことを示しており、λ計算の宣言的な性格が伺える。

意味論

計算規則を与えることは、計算言語としての意味を与えることと考えることができる。このような立場を計算機科学上は操作的意味論と呼ぶ。これに対して、言語の各要素に対して、それが指示する対象を与えることで意味を与える立場を(計算機科学では)表示的意味論と呼ぶ。λ計算は数学上の関数の概念から出発してはいるものの、(λx. xx)(λx. xx)のように関数に自己自身を適用できるなど通常の集合論的な関数を逸脱している。

この困難に対して、λ計算の表示的な意味論を与えたのがD.S. Scottの領域理論である。領域理論では、λ計算は完備半順序集合上の点として解釈される。λ計算内の関数は、完備半順序集合上の単調増加かつ連続*1な関数として表現される。完備半順序集合上の単調増加連続関数は、それ自体完備半順序集合をなし、さらに不動点を持つ。この性質を利用してλ計算の表示的意味論が構成される。Schemeの規格文書は領域理論による意味論を含んでいる。

また、近年ではOng, Hylandらによるゲーム意味論が注目されている。ゲーム意味論ではデータ型をゲーム、その型の値を求めるプログラムをそのゲームの戦略として解釈する。用いることのできる戦略の違いにより、並列プログラムや手続き型プログラムを特徴付けることができる。

拡張と変形

静的型付けを行うもの

単純型付λ計算、システムF(多相型を持つ)、F< (Fにサブタイプを加えたもの)

実際のプログラミング言語に近づけたもの

評価戦略を導入したもの、PCF(単純型付きに制限した上、基本型と高階型に対するYコンビネータを追加したもの)、call/ccや例外など大域的な制御構造を導入したもの

論理と関連付けたもの

型付きλ計算は、直観主義論理の自然演繹体系とおなじ形式を持つ。よって、λ計算により直観主義数学の形式的体系を記述することができる。この事をカリー・ハワード対応と呼ぶ。Martin-Löfの直観主義的型理論やCoquandのCalculus of Constructionなどがこれにあたる。これらは、プログラム導出に応用でき、定理証明系であるCoqやAgdaに利用されている。

計算過程をより分析したもの

β変換で現れる代入の操作を明示的に含んだ体系などがある。

書籍

The Lambda Calculus: Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics)

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)