Foundational judgments and untyped operational semantics

The elementary judgments of chapter 1 use the finite constructors displayed in their conclusions. The primitive rules, in the sense of section 1.4, are

$\mathsf{0}\mathsf{nat}$

$a\mathsf{nat}$

$\mathsf{suc}(a)\mathsf{nat}$

$\mathsf{emp}\mathsf{tree}$

$a_1\mathsf{tree}$$a_2\mathsf{tree}$

$\mathsf{node}(a_1;a_2)\mathsf{tree}$

$\mathsf{0}\mathsf{is}\mathsf{0}$

$a\mathsf{is}b$

$\mathsf{suc}(a)\mathsf{is}\mathsf{suc}(b)$

$\mathsf{nil}\mathsf{list}$

$a\mathsf{nat}$$\ell \mathsf{list}$

$\mathsf{cons}(a;\ell )\mathsf{list}$

Parity is a simultaneous definition. The sum definition refers to the numeral judgment through the premise $b\mathsf{nat}$ of Sum-Z:

$\mathsf{0}\mathsf{even}$

$b\mathsf{odd}$

$\mathsf{suc}(b)\mathsf{even}$

$a\mathsf{even}$

$\mathsf{suc}(a)\mathsf{odd}$

$b\mathsf{nat}$

$\mathsf{sum}(\mathsf{0};b;b)$

$\mathsf{sum}(a;b;c)$

$\mathsf{sum}(\mathsf{suc}(a);b;\mathsf{suc}(c))$

The following two displayed schemes are not primitive. Nat-SS is derivable from Nat-S; Ev-Inv is admissible for the parity system but is not derivable there:

$a\mathsf{nat}$

$\mathsf{suc}(\mathsf{suc}(a))\mathsf{nat}$

$\mathsf{suc}(a)\mathsf{even}$

$a\mathsf{odd}$

Hypothetical derivations have one additional metarule. An assumed judgment is available as

$J\in \mathrm{\Gamma }$

$J$

where the premise is the metalevel check that $J$ belongs to the finite hypothesis set $\mathrm{\Gamma }$; it is not a rule added to the object system.

The arithmetic language and its values are $$e::=\mathsf{0}\mid \mathsf{suc}(e)\mid \mathsf{add}(e;e),$$

$\mathsf{0}\mathsf{num}$

$n\mathsf{num}$

$\mathsf{suc}(n)\mathsf{num}$

Its arithmetic small-step relation is

$e{⟼}_{\mathsf{A}}{e}^{\prime }$

$\mathsf{suc}(e){⟼}_{\mathsf{A}}\mathsf{suc}(e^{\prime })$

$e_1{⟼}_{\mathsf{A}}{e}_1^{\prime }$

$\mathsf{add}(e_1;e_2){⟼}_{\mathsf{A}}\mathsf{add}(e_1^{\prime };e_2)$

$n_1\mathsf{num}$$e_2{⟼}_{\mathsf{A}}{e}_2^{\prime }$

$\mathsf{add}(n_1;e_2){⟼}_{\mathsf{A}}\mathsf{add}(n_1;e_2^{\prime })$

$n_2\mathsf{num}$

$\mathsf{add}(\mathsf{0};n_2){⟼}_{\mathsf{A}}{n}_2$

$n_1\mathsf{num}$$n_2\mathsf{num}$

$\mathsf{add}(\mathsf{suc}(n_1);n_2){⟼}_{\mathsf{A}}\mathsf{suc}(\mathsf{add}(n_1;n_2))$

Reflexive transitive closure and big-step arithmetic evaluation are generated by

$e{⟼}_{\mathsf{A}}^{\ast }e$

$e{⟼}_{\mathsf{A}}{e}_1$$e_1{⟼}_{\mathsf{A}}^{\ast }{e}_2$

$e{⟼}_{\mathsf{A}}^{\ast }{e}_2$

$\mathsf{0}{\Downarrow }_{\mathsf{A}}\mathsf{0}$

$e{\Downarrow }_{\mathsf{A}}n$

$\mathsf{suc}(e){\Downarrow }_{\mathsf{A}}\mathsf{suc}(n)$

$e_1{\Downarrow }_{\mathsf{A}}{n}_1$$e_2{\Downarrow }_{\mathsf{A}}{n}_2$$\mathsf{sum}(n_1;n_2;n_3)$

$\mathsf{add}(e_1;e_2){\Downarrow }_{\mathsf{A}}{n}_3$

The full untyped language is Terms are alpha-equivalence classes of raw expressions. The notation $e[a/x]$ denotes capture-avoiding substitution. Values and numeric values are generated by

$\lambda x.b\mathsf{val}$

$\mathsf{tt}\mathsf{val}$

$\mathsf{ff}\mathsf{val}$

$n\mathsf{num}$

$n\mathsf{val}$

Here $n\mathsf{num}$ is the judgment generated by Num-Z and Num-S above; the full grammar adds no new numeric values. The full-language call-by-value relation is

$e_1⟼e_1^{\prime }$

$e_1{e}_2⟼e_1^{\prime }{e}_2$

$v_1\mathsf{val}$$e_2⟼e_2^{\prime }$

$v_1{e}_2⟼v_1{e}_2^{\prime }$

$v\mathsf{val}$

$(\lambda x.b)v⟼b[v/x]$

$e⟼e^{\prime }$

$\mathsf{if}(e;e_1;e_2)⟼\mathsf{if}(e^{\prime };e_1;e_2)$

$\mathsf{if}(\mathsf{tt};e_1;e_2)⟼e_1$

$\mathsf{if}(\mathsf{ff};e_1;e_2)⟼e_2$

$e⟼e^{\prime }$

$\mathsf{suc}(e)⟼\mathsf{suc}(e^{\prime })$

$e_1⟼e_1^{\prime }$

$\mathsf{add}(e_1;e_2)⟼\mathsf{add}(e_1^{\prime };e_2)$

$n_1\mathsf{num}$$e_2⟼e_2^{\prime }$

$\mathsf{add}(n_1;e_2)⟼\mathsf{add}(n_1;e_2^{\prime })$

$n_2\mathsf{num}$

$\mathsf{add}(\mathsf{0};n_2)⟼n_2$

$n_1\mathsf{num}$$n_2\mathsf{num}$

$\mathsf{add}(\mathsf{suc}(n_1);n_2)⟼\mathsf{suc}(\mathsf{add}(n_1;n_2))$

Its reflexive–transitive closure is generated by

$e{⟼}^{\ast }e$

$e⟼e_1$$e_1{⟼}^{\ast }{e}_2$

$e{⟼}^{\ast }{e}_2$

Equivalently, evaluation contexts and root contractions are where $v\mathsf{val}$ and $n,n_1,n_2\mathsf{num}$. One step is exactly compatible closure by these contexts. The same language’s big-step relation is

$v\mathsf{val}$

$v\Downarrow v$

$e_1\Downarrow \lambda x.b$$e_2\Downarrow v_2$$b[v_2/x]\Downarrow v$

$e_1{e}_2\Downarrow v$

$e\Downarrow \mathsf{tt}$$e_1\Downarrow v$

$\mathsf{if}(e;e_1;e_2)\Downarrow v$

$e\Downarrow \mathsf{ff}$$e_2\Downarrow v$

$\mathsf{if}(e;e_1;e_2)\Downarrow v$

$e\Downarrow n$$n\mathsf{num}$

$\mathsf{suc}(e)\Downarrow \mathsf{suc}(n)$

$e_1\Downarrow n_1$$e_2\Downarrow n_2$$\mathsf{sum}(n_1;n_2;n_3)$

$\mathsf{add}(e_1;e_2)\Downarrow n_3$

The arithmetic and full-language big-step relations use different judgment macros and rule names; the chapter proves their agreement on arithmetic expressions.