アリティ付きフラット・ラムダ計算の記法

• ρ、τ ： 値割り当て、環境
• X, Y ： 束縛セット
• let X in t ： let式、letrecを含む
• X!u : 束縛（モジュール）X内で、uを定義する最小のlet式
• 【t|τ】 : 環境τのもとでの、項tの意味
• Ev(t) ： 閉じた項tの評価結果（意味を与える）
• Ev(t, τ) ： 環境τにおけるtの評価結果
• t[τ] ： 項tの環境τによる具体化（置換）
• X[Y] ： 束縛セットXの束縛セットYによる置換
• X :+ Y ： 束縛セットの非対称マージ
• τ :+ ρ : 環境の非対称マージ
• 《t|τ》 ： t[τ] と同じ。
• 《X|τ》 ： 束縛セットXの環境τによる具体化
• 《X|Y》 ： 束縛セットXの束縛セットYによる置換
• 【X|τ】 ： 束縛セットXの環境τにおける意味＝新しい環境

追加：

• D[n] ： [Dⁿ, D] のこと
• D[n, m] ： (D[n])^m のこと
• Term(D)[n] ： アリティnの擬似項、D[n] を含む。
• Term(D)[n, m] ： (Term(D)[n])^m、D[n, m] を含む。