ラムダ計算
A ⌜ x ⌝ ⌜ y ⌝ → β ⌜ ( x y ) ⌝ {\displaystyle A\ulcorner x\urcorner \ulcorner y\urcorner \to ^{\beta }\ulcorner (xy)\urcorner }
N ⌜ x ⌝ → β ⌜ ⌜ x ⌝ ⌝ {\displaystyle N\ulcorner x\urcorner \to ^{\beta }\ulcorner \ulcorner x\urcorner \urcorner }
が成り立つ。ここで ⌜ x ⌝ {\displaystyle \ulcorner x\urcorner } はラムダ式 x {\displaystyle x} のゲーデル数を表すラムダ式の表現である。 いま、ラムダ式 e {\displaystyle e} を
e := λ x . if X ( A x ( N x ) ) then Ω else λ y . y {\displaystyle e:=\lambda x.{\text{ if }}X(Ax(Nx)){\text{ then }}\Omega {\text{ else }}\lambda y.y}
と定める。ここで Ω {\displaystyle \Omega } は正規形を持たないラムダ式 ( λ x . x x ) ( λ x . x x ) {\displaystyle (\lambda x.
Pascalなど、多くの命令型言語ではある関数を他の関数の引数として与える操作が許されている。CやC++では関数を指すポインタやクラス型関数オブジェクトを用いて同じことが実現できる。このような機能はサブ関数が明示的に書かれている場合にのみ用いることができ、したがってこの機能がそのまま高階関数をサポートしていることにはならない。いくつかの手続的なオブジェクト指向言語では関数を任意の階数に書くことができる。Smalltalkや、より最近の言語ではEiffel(エージェント)やC#(デリゲート)などで用意されている機能がそれである。例えば、Eiffelのインライン・エージェントの機能を用いた以下のコード
はラムダ式 λx. x * x (値呼び出し)に相当するオブジェクトを表している。このオブジェクトは他のあらゆるオブジェクトと同様に、変数に代入したり関数に渡したりすることができる。変数 square の値が上のエージェントのオブジェクトであるとすれば、 square に値 a を適用した結果(β-簡約)は square.item([a]) と書ける。ただしここでの引数はタプルであるとみなされる。
引数を2つとる関数は、1つの引数をとり、1つの引数をとる関数を返す関数として表現される(カリー化)。例えば、関数 f(x, y) = x − y は λx. (λy. x − y) となる。この式は慣例で λxy. x − yと省略して書かれることが多い。以下の3つの式
(λxy. x − y) 7 2 と (λy. 7 − y) 2 と 7 − 2
は全て同値となる。
ラムダ計算そのものには上で用いた整数や加算などは存在しないが、算術演算や整数は特定のラムダ式の省略であると定義することによってエンコードできる。その具体的な定義については改めて後に述べる。
ラムダ式は自由変数( λ によって束縛されていない変数)を含むこともできる。例えば、入力に関係なく常に y を返す関数を表す式 λx. y において、変数 y は自由変数である。このようなときに変数名の付け替えが必要になることがある。つまり、式 (λxy. y x) (λx. y) は λy. y (λx. y) ではなく、 λz.z (λx. y) と同値である。