LoginSignup
0

More than 5 years have passed since last update.

TAPL3-2.算術式(NB)

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

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
0