0

More than 5 years have passed since last update.

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

Posted at
\begin{array}{l}

\begin{array}{llr}
\bbox[lightgray]T ::= & …   & \hspace{90px}型：\\
& \bbox[lightgray]{Nat} & 自然数型\\
\end{array}\\
\\
\begin{array}{cr}

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


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