TAPL3.bigstep

\begin{array}{l}
評価規則\\
\begin{array}{cr}
v \Downarrow v                             & \text{(B-Value)} \\
\dfrac{t1 \Downarrow true \quad t2 \Downarrow v2}
{if\;t1\;then\;t2\;else\;t3 \Downarrow v2} & \text{(B-IfTrue)} \\
\dfrac{t1 \Downarrow false \quad t3 \Downarrow v3}
{if\;t1\;then\;t2\;else\;t3 \Downarrow v3} & \text{(B-IfFalse)} \\
\dfrac{t1 \Downarrow nv1}
{succ t1 \Downarrow succ nv1}              & \text{(B-Succ)} \\
\dfrac{t1 \Downarrow 0}
{pred \; t1 \Downarrow 0}                  & \text{(B-PredZero)} \\
\dfrac{t1 \Downarrow succ \; nv1}
{pred \; t1 \Downarrow nv1}                & \text{(B-PredSucc)} \\
\dfrac{t1 \Downarrow 0}
{iszero t1 \Downarrow true}                & \text{(B-IszeroZero)} \\
\dfrac{t1 \Downarrow succ \; nv1}
{iszero \; t1 \Downarrow false}            & \text{(B-IszeroSucc)} \\
\end{array}
\end{array}

tapl03_bigstep.pl

/*
構文

t ::=                項：
　true               定数真
　false              定数偽
　if(t,t,t)          条件式
  0                  定数ゼロ
  succ(t)            後者値
  pred(t)            前者値

v::=                 値：
　true               定数真
　false              定数偽
  nv                 数値
nv ::=               数値：
  0                  ゼロ
  succ(nv)           後者値

*/
:- op(920, xfx, [ ⇓ ]).
:- op(1200, xfx, [ -- ]).
:- style_check(-singleton).
term_expansion(A -- B, B :- A).

t(true).
t(false).
t(if(T1,T2,T3)) :- t(T1),t(T2),t(T3).
t(0).
t(succ(T)) :- t(T).
t(pred(T)) :- t(T).
v(true).
v(false).
v(NV) :- nv(NV).
nv(0).
nv(succ(NV)) :- nv(NV).

v(V)
--%---------------------------------------- (B-Value)
V ⇓ V.
T1 ⇓ true, T2 ⇓ V2, v(V2)
--%---------------------------------------- (B-IfTrue)
if(T1,T2,T3) ⇓ V2.
T1 ⇓ false, T3 ⇓ V3, v(V3)
--%---------------------------------------- (B-IfFalse)
if(T1,T2,T3) ⇓ V3.
T1 ⇓ NV1, nv(NV1)
--%---------------------------------------- (B-Succ)
succ(T1) ⇓ succ(NV1).
T1 ⇓ 0
--%---------------------------------------- (B-PredZero)
pred(T1) ⇓ 0.
T1 ⇓ succ(NV1), nv(NV1)
--%---------------------------------------- (B-PredSucc)
pred(T1) ⇓ NV1.
T1 ⇓ 0
--%---------------------------------------- (B-IszeroZero)
iszero(T1) ⇓ true.
T1 ⇓ succ(NV1), nv(NV1)
--%---------------------------------------- (B-IszeroSucc)
iszero(T1) ⇓ false.

run(T,V2) :- T ⇓ V, writeln(V), V=V2.

:- run(true,true).
:- run(if(true,false,true),false).
:- run(if(false,false,true),true).
:- run(if(if(true,false,true),if(true,false,true),if(true,false,true)),false).
:- run(0,0).
:- run(succ(0),succ(0)).
:- run(pred(succ(0)),0).
:- run(iszero(pred(succ(0))),true).
:- run(iszero(succ(0)),false).
:- halt.