TAPL8-2.数(NB)のための型付け規則

\begin{array}{l}
新しい構文形式\\
\begin{array}{llr}
\bbox[lightgray]T ::= & …   & \hspace{90px}型：\\
      & \bbox[lightgray]{Nat} & 自然数型\\
\end{array}\\
\\
\begin{array}{cr}
新しい型付け規則 & \bbox[3px,border:1px solid black]{t : T}\\

\bbox[lightgray]{0 : Nat} & \text{(T-Zero)}\\

\bbox[lightgray]{\dfrac{t_1 : Nat}
{succ\;t_1 : Nat}} & \text{(T-Succ)}\\

\bbox[lightgray]{\dfrac{t_1 : Nat}
{pred\;t_1 : Nat}} & \text{(T-Pred)}\\

\bbox[lightgray]{\dfrac{t_1 : Nat}
{iszero\;t_1 : Bool}} & \text{(T-IsZero)}\\
\end{array}\\

\end{array}

tapl08_2.pl

/*
構文

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

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

Ty ::= … 型：
  nat                自然数型

*/
:- op(900, xfx, [ : ]).
:- op(910, fx, [ ⊢ ]).
:- 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 : T

⊢ true : bool.                    % (T-True)

⊢ false : bool.                   % (T-False)

⊢ T1 : bool, ⊢ T2 : Ty, ⊢ T3 : Ty 
--%-------------------------------- (T-If)
⊢ if(T1,T2,T3) : Ty.

⊢ 0 : nat.                        % (T-Zero)

⊢ T1 : nat
--%-------------------------------- (T-Succ)
⊢ succ(T1) : nat.

⊢ T1 : nat
--%-------------------------------- (T-Pred)
⊢ pred(T1) : nat.

⊢ T1 : nat
--%-------------------------------- (T-IsZero)
⊢ iszero(T1) : bool.

T ==>> T3 :- T ==> T2, T2 ==>> T3.
T ==>> T.

run(T) :- ⊢ T : Ty, T ==>> T2, writeln(T:Ty==>>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.