LoginSignup
0

More than 5 years have passed since last update.

TAPL3.bigstep

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

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