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

構文領域で：

• 関数記号の集合： F = F₀ + ...
• 変数記号の集合： V = V₀ + ...
• 関数記号（のメタ変数）： f, g, h
• 変数記号（のメタ変数）： u, v, w
• アリティ0の変数記号（のメタ変数）： x, y, z
• ラムダ項（のメタ変数）： s, t
• 束縛セット： X, Y
• 束縛セットの変数uのボディ： X(u)
• uを定義する最小のlet式： X!u
• 束縛セットの置換： X[Y]、《X|Y》
• 束縛セットの“和”： X:+Y、X+:Y、X++Y

意味領域で：

• 意味論の圏： C
• 値の領域： D∈|C|
• 基本意味論： α、β : F_*→D[*]
• 値割り当て、環境: ρ、τ
• 環境τのもとでの、項tの意味： Eval(t, τ) = 【t|τ】
• 環境τのもとでの、束縛セットXtの意味： 【X|τ】
• 環境の“和”： ρ:+τ、ρ+:τ、ρ++τ