TAPL3-2.算術式(NB)

\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.