λ式 e からβ簡約をくりかえしてλ式 e' が得られるとき，e→→e' と書く． 定理 e→→e1，e→→e2 ならば，λ式 e3 が存在して，e1→→e3，e2→→e3 となる． 以下これを証明する．

V を変数の集合とする． 二分木から V∪{*} への写像 e でe(σ)∈V ( val(σ) = 0, 1 ), e(σ) = * ( val(σ) = 2 )をみたすものはλ式と1対1に対応する． 価数0の頂点が変数，価数1の頂点が抽象，価数2の頂点が適用に対応する． 二分木は変数が1種類のλ式と1対1に…

集合 S に対して，S の元の有限列全体の集合を S* とする．S* は空な列εを含む． S* を自由モノイドという．これはモノイドの圏から集合の圏への忘却関手の左随伴を与える． S* 上に σ≤στ によって順序を定義する． A⊂S* が prefix 閉であるとは，στ∈A なら…

定義 変数はλ式． （適用）λ式 M，N に対し，MN はλ式． （抽象）変数 x とλ式 M に対し，λx . M はλ式． 1，2，3からλ式 M が構成されるとき，途中に現れるλ式を M の部分式という． 定義 変数 x は x の自由変数． λ式 M，N に対し，変数 x が M の自由変…

ならば，-log の凸性により，