CEK機械
拡張ラムダ計算に対するCEKは次のように定義される。
まず、拡張ラムダ計算を次のように定義する。
(式) M ::= {\displaystyle M::=} X {\displaystyle X} (変数) | λ X . M {\displaystyle |\ \lambda X.M} (λ抽象) | M M {\displaystyle |\ M\ M} (関数適用) | b {\displaystyle |\ b} (基本定数) | o n M . . . M {\displaystyle |\ o^{n}\ M\ ...\ M} (プリミティブ操作の適用)
(値) V ::= λ X . M | b {\displaystyle V::=\lambda X.M\ |\ b}
次に、CEK機械の状態を構成する要素を次のように定義する。
(環境) E ::= { ⟨ X , c ⟩ , . . . } {\displaystyle E::=\left\lbrace \left\langle X,c\right\rangle ,...\right\rbrace } (変数から、クロージャへの関数(変数とクロージャのペアの集合)) E [ X ← c ] = { ⟨ X , c ⟩ } ∪ { ⟨ Y , c ′ ⟩ | ⟨ Y , c ′ ⟩ ∈ E ∧ Y ≠ X } {\displaystyle E[X\leftarrow c]=\left\lbrace \left\langle X,c\right\rangle \right\rbrace \cup \left\lbrace \left\langle Y,c'\right\rangle |\left\langle Y,c'\right\rangle \in E\land Y\neq X\right\rbrace }