CEK機械
⟨ ⟨ b , E ⟩ , ⟨ n a r g , ⟨ ⟨ b i , E i ⟩ , . . . , ⟨ b 1 , E ′ ⟩ , o ⟩ , ⟨ ⟩ , K ⟩ ⟩ {\displaystyle \left\langle \left\langle b,E\right\rangle ,\left\langle {\mathsf {narg}},\left\langle \left\langle b_{i},E_{i}\right\rangle ,...,\left\langle b_{1},E'\right\rangle ,o\right\rangle ,\left\langle \right\rangle ,K\right\rangle \right\rangle } ⟼ c e k ⟨ ⟨ V , ∅ ⟩ , K ⟩ {\displaystyle \longmapsto _{\mathsf {cek}}\left\langle \left\langle V,\emptyset \right\rangle ,K\right\rangle } ( V {\displaystyle V} は o {\displaystyle o} に b 1 , . . . , b i , b {\displaystyle b_{1},...,b_{i},b} を適用した結果)
このとき、CEK機械による評価関数 e v a l c e k ( M ) {\displaystyle {\mathit {eval}}_{\mathsf {cek}}(M)} は次のように定義される
⟩ , K ⟩ {\displaystyle |\ \left\langle {\mathsf {narg}},\left\langle v,...,v,o\right\rangle ,\left\langle c,...\right\rangle ,K\right\rangle } (プリミティブ操作の実引数の評価および適用への継続)
このとき、CEK機械の状態は組 ⟨ c , K ⟩ = ⟨ ⟨ M , E ⟩ , K ⟩ {\displaystyle \left\langle c,K\right\rangle =\left\langle \left\langle M,E\right\rangle ,K\right\rangle } と表される。
CEK機械の遷移規則は次のように定義される。
⟨ ⟨ X , E ⟩ , K ⟩ {\displaystyle \left\langle \left\langle X,E\right\rangle ,K\right\rangle } ⟼ c e k ⟨ c , K ⟩ {\displaystyle \longmapsto _{\mathsf {cek}}\left\langle c,K\right\rangle } ( E ( X ) = c {\displaystyle E(X)=c} のとき)
⟨ ⟨ M 1 M 2 , E ⟩ , K ⟩ {\displaystyle \left\langle \left\langle M_{1}\ M_{2},E\right\rangle ,K\right\rangle } ⟼ c e k ⟨ ⟨ M 1 , E ⟩ , ⟨ a r g , ⟨ M 2 , E ⟩ , K ⟩ ⟩ {\displaystyle \longmapsto _{\mathsf {cek}}\left\langle \left\langle M_{1},E\right\rangle ,\left\langle {\mathsf {arg}},\left\langle M_{2},E\right\rangle ,K\right\rangle \right\rangle }