言語 L の構文と簡約関係

定義 4.1（「プログラミング言語論」§4）

項 $t$ を次の文法で定める。

t ::= \mathtt{true} \mid \mathtt{false} \mid \mathtt{if}\ t\ \mathtt{then}\ t\ \mathtt{else}\ t \mid \mathtt{0} \mid \mathtt{succ}\ t \mid \mathtt{pred}\ t \mid \mathtt{iszero}\ t

数値 $nv$ と値 $v$ を次で定める。

nv ::= \mathtt{0} \mid \mathtt{succ}\ nv, \qquad v ::= \mathtt{true} \mid \mathtt{false} \mid nv

1 ステップ簡約関係 $t \to t'$ を、次の規則で生成される最小の関係とする。

\begin{aligned} &\text{(E-IfTrue)} && \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to t_2 \\ &\text{(E-IfFalse)} && \mathtt{if}\ \mathtt{false}\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to t_3 \\ &\text{(E-If)} && \frac{t_1 \to t_1'}{\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to \mathtt{if}\ t_1'\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3} \\ &\text{(E-Succ)} && \frac{t \to t'}{\mathtt{succ}\ t \to \mathtt{succ}\ t'} \\ &\text{(E-PredZero)} && \mathtt{pred}\ \mathtt{0} \to \mathtt{0} \\ &\text{(E-PredSucc)} && \mathtt{pred}\ (\mathtt{succ}\ nv) \to nv \\ &\text{(E-Pred)} && \frac{t \to t'}{\mathtt{pred}\ t \to \mathtt{pred}\ t'} \\ &\text{(E-IszeroZero)} && \mathtt{iszero}\ \mathtt{0} \to \mathtt{true} \\ &\text{(E-IszeroSucc)} && \mathtt{iszero}\ (\mathtt{succ}\ nv) \to \mathtt{false} \\ &\text{(E-Iszero)} && \frac{t \to t'}{\mathtt{iszero}\ t \to \mathtt{iszero}\ t'} \end{aligned}

どの規則も適用できない項を正規形という。値でない正規形を行き詰まり項（stuck term）という。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。