\begin{array}{l|l}
\begin{array}{l}
新しい構文形式\\
\begin{array}{llr}
t ::= & … & 項：\\
& \bbox[lightgray]{0} & 定数ゼロ\\
& \bbox[lightgray]{succ\;t} & 後者値\\
& \bbox[lightgray]{pred\;t} & 前者値\\
v ::= & … & 値：\\
& \bbox[lightgray]{nv } & 数値\\
\bbox[lightgray]{nv} ::= & & 数値：\\
& \bbox[lightgray]{0} & ゼロ\\
& \bbox[lightgray]{succ\;nv} & 後者値\\
\\
\end{array}
\end{array}
&
\begin{array}{cr}
新しい評価規則 \hspace{150px}& \bbox[3px,border:1px solid black]{t \longrightarrow t’} \\
\bbox[lightgray]{
\dfrac{t_1 \longrightarrow t_1’}{
succ\;t_1 \longrightarrow succ\;t_1’}} & (E-Succ)
\\
\bbox[lightgray]{pred\;0 \longrightarrow 0 } & (E-PredZero)
\\
\bbox[lightgray]{pred(succ\;nv_1) \longrightarrow nv_1 } & (E-PredSucc)
\\
\bbox[lightgray]{
\dfrac{t_1 \longrightarrow t_1’}{
pred\;t_1 \longrightarrow pred\;t_1’}} & \text{(E-Pred)}
\\
\bbox[lightgray]{
iszero\;0 \longrightarrow true } & \text{(E-IsZeroZero)}
\\
\bbox[lightgray]{
iszero(succ\;nv_1) \longrightarrow false } & \text{(E-IsZeroSucc)}
\\
\bbox[lightgray]{
\dfrac{t_1\longrightarrow t_1’}{
iszero\;t_1 \longrightarrow iszero\;t_1’}} & (E-Zero)
\end{array}
\end{array}
/*
新しい構文形式
t ::= … 項：
0 定数ゼロ
succ(t) 後者値
pred(t) 前者値
v ::= … 値：
nv 数値
nv ::= 数値：
0 ゼロ
succ nv 後者値
*/
t(0).
t(succ(T)) :- t(T).
t(pred(T)) :- t(T).
v(NV) :- nv(NV).
nv(0).
nv(succ(NV)) :- nv(NV).
% 新しい評価規則 t ==> t’
T1 ==> T1_
--%---------------------------------- (E-Succ)
succ(T1) ==> succ(T1_).
pred(0) ==> 0. % (E-PredZero)
nv(NV1)
--%---------------------------------- (E-PredSucc)
pred(succ(NV1)) ==> NV1.
T1 ==> T1_
--%---------------------------------- (E-Pred)
pred(T1) ==> pred(T1_).
iszero(0) ==> true. % (E-IsZeroZero)
nv(NV1)
--%---------------------------------- (E-IsZeroSucc)
iszero(succ(NV1)) ==> false.
T1 ==> T1_
--%---------------------------------- (E-Zero)
iszero(T1) ==> iszero(T1_).
tapl03_2.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).
% 評価 t ==> t’
if(true, T2,T3) ==> T2. % (E-IfTrue)
if(false,T2,T3) ==> T3. % (E-IfFalse)
T1 ==> T1_
--%------------------------------ (E-If)
if(T1,T2,T3) ==> if(T1_,T2,T3).
T1 ==> T1_
--%---------------------------------- (E-Succ)
succ(T1) ==> succ(T1_).
pred(0) ==> 0. % (E-PredZero)
nv(NV1)
--%---------------------------------- (E-PredSucc)
pred(succ(NV1)) ==> NV1.
T1 ==> T1_
--%---------------------------------- (E-Pred)
pred(T1) ==> pred(T1_).
iszero(0) ==> true. % (E-IsZeroZero)
nv(NV1)
--%---------------------------------- (E-IsZeroSucc)
iszero(succ(NV1)) ==> false.
T1 ==> T1_
--%---------------------------------- (E-Zero)
iszero(T1) ==> iszero(T1_).
T ==>> T3 :- T ==> T2, T2 ==>> T3.
T ==>> T.
run(T) :- T ==>> T2, writeln(T2).
:- run(true).
:- run(if(true,false,true)).
:- run(if(false,false,true)).
:- run(if(if(true,false,true),if(true,false,true),if(true,false,true))).
:- run(0).
:- run(succ(0)).
:- run(pred(succ(0))).
:- run(iszero(pred(succ(0)))).
:- run(iszero(succ(0))).
:- halt.