(式)


$M\; ::=$

    $X$ (変数)

  $|\; \backslash \; \backslash lambda\; X.\; M$ (λ抽象)

  $|\; \backslash \; M\; \backslash \; M$ (関数適用)

  $|\; \backslash \; b$ (基本定数)

  $|\; \backslash \; o^n\; \backslash \; M\; \backslash \; ...\; \backslash \; M$ (プリミティブ操作の適用)
(値)

$V\; ::=\; \backslash lambda\; X.\; M\; \backslash \; |\; \backslash \; b$

(環境)

$E\; ::=\; \backslash left\backslash lbrace\backslash left\backslash langle\; X,\; c\backslash right\backslash rangle\; ,\; ...\backslash right\backslash rbrace$ (変数から、クロージャへの関数(変数とクロージャのペアの集合))

$E$\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 \ne X\right\rbrace
(クロージャ)

$c\; ::=\; \backslash left\backslash langle\; M,\; E\backslash right\backslash rangle$ (ただし、$M$の自由変数は全て$E$の定義域に含まれる)
(値)

$v\; ::=\; \backslash left\backslash langle\; V,\; E\backslash right\backslash rangle$ (ただし、$V$の自由変数は全て$E$の定義域に含まれる)
(継続)

$K\; ::=$

    $\backslash mathsf$ (初期継続)

  $|\backslash \; \backslash left\backslash langle\; \backslash mathsf,\; V,\; K\backslash right\backslash rangle$ (関数適用への継続)

  $|\backslash \; \backslash left\backslash langle\; \backslash mathsf,\; M,\; K\backslash right\backslash rangle$ (実引数評価への継続)

  $|\backslash \; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; v,\; ...,\; v,\; o\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; c,\; ...\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle$ (プリミティブ操作の実引数の評価および適用への継続)

$\backslash left\backslash langle\; \backslash left\backslash langle\; X,\; E\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle$
      $\backslash longmapsto\_\backslash mathsf\; \backslash left\backslash langle\; c,\; K\backslash right\backslash rangle$ ($E(X)\; =\; c$ のとき)
$\backslash left\backslash langle\; \backslash left\backslash langle\; M\_1\; \backslash \; M\_2,\; E\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle$
      $\backslash longmapsto\_\backslash mathsf\; \backslash left\backslash langle\; \backslash left\backslash langle\; M\_1,\; E\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; M\_2,\; E\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle\; \backslash right\backslash rangle$
$\backslash left\backslash langle\; \backslash left\backslash langle\; o\; \backslash \; M\_1\; \backslash \; M\_2\; \backslash \; ...,\; E\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle$
      $\backslash longmapsto\_\backslash mathsf\; \backslash left\backslash langle\; \backslash left\backslash langle\; M\_1,\; E\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; o\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash left\backslash langle\; M\_2,\; E\backslash right\backslash rangle\; ,\; ...\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle\; \backslash right\backslash rangle$
$\backslash left\backslash langle\; \backslash left\backslash langle\; V,\; E\text{'}\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; \backslash lambda\; X.\; M,\; E\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle\; \backslash right\backslash rangle$
      $\backslash longmapsto\_\backslash mathsf\; \backslash left\backslash langle\; \backslash left\backslash langle\; M,\; E$\leftarrow \left\langle V, E'\right\rangle \right\rangle , K\right\rangle ($V$が変数でない場合)
$\backslash left\backslash langle\; \backslash left\backslash langle\; V,\; E\text{'}\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; M,\; E\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle\; \backslash right\backslash rangle$
      $\backslash longmapsto\_\backslash mathsf\; \backslash left\backslash langle\; \backslash left\backslash langle\; M,\; E\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; V,\; E\text{'}\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle\; \backslash right\backslash rangle$ ($V$が変数でない場合)
$\backslash left\backslash langle\; \backslash left\backslash langle\; V,\; E\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; c\text{'},\; ...\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash left\backslash langle\; N,\; E\text{'}\backslash right\backslash rangle\; ,\; c,\; ...\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle\; \backslash right\backslash rangle$
      $\backslash longmapsto\_\backslash mathsf\; \backslash left\backslash langle\; \backslash left\backslash langle\; N,\; E\text{'}\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; \backslash left\backslash langle\; V,\; E\backslash right\backslash rangle\; ,\; c\text{'},\; ...\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; c,\; ...\backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle\; \backslash right\backslash rangle$ ($V$が変数でない場合)
$\backslash left\backslash langle\; \backslash left\backslash langle\; b,\; E\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash mathsf,\; \backslash left\backslash langle\; \backslash left\backslash langle\; b\_i,\; E\_i\backslash right\backslash rangle\; ,\; ...,\; \backslash left\backslash langle\; b\_1,\; E\text{'}\backslash right\backslash rangle\; ,\; o\backslash right\backslash rangle\; ,\; \backslash left\backslash langle\; \backslash right\backslash rangle\; ,\; K\backslash right\backslash rangle\; \backslash right\backslash rangle$
      $\backslash longmapsto\_\backslash mathsf\; \backslash left\backslash langle\; \backslash left\backslash langle\; V,\; \backslash emptyset\; \backslash right\backslash rangle,\; K\backslash right\backslash rangle$ ($V$は$o$に$b\_1,\; ...,\; b\_i,\; b$を適用した結果)

$\backslash mathit\_\backslash mathsf(M)\; =\; b$    ($\backslash left\backslash langle\; \backslash left\backslash langle\; M,\; \backslash emptyset\backslash right\backslash rangle\; ,\; \backslash mathsf\backslash right\backslash rangle\; \backslash longmapsto\_\backslash mathsf^\; \backslash left\backslash langle\; \backslash left\backslash langle\; b,\; E\backslash right\backslash rangle\; ,\; \backslash mathsf\backslash right\backslash rangle$ のとき)
$\backslash mathit\_\backslash mathsf(M)\; =\; \backslash mathsf$    ($\backslash left\backslash langle\; \backslash left\backslash langle\; M,\; \backslash emptyset\backslash right\backslash rangle\; ,\; \backslash mathsf\backslash right\backslash rangle\; \backslash longmapsto\_\backslash mathsf^\; \backslash left\backslash langle\; \backslash left\backslash langle\; \backslash lambda\; X.\; M,\; E\backslash right\backslash rangle\; ,\; \backslash mathsf\backslash right\backslash rangle$ のとき)