TAPL8-1.ブール値のための型付け規則

\begin{array}{lr}
新しい構文形式\\

\begin{array}{llr}
\bbox[lightgray]T ::= & …    & \hspace{170px} 型：\\
      & \bbox[lightgray]{Bool} & ブール値型\\
\end{array}\\
\\
\begin{array}{cr}
新しい型付け規則 \hspace{100px} & \bbox[3px,border:1px solid black]{t : T}\\
\bbox[lightgray]{true : Bool}                          & \text{(T-True)}\\

\bbox[lightgray]{false : Bool}                         & \text{(T-False)}\\

\bbox[lightgray]{
\dfrac{t_1 : Bool \quad t_2 : T \quad t_3 : T}
{if\;t_1\;then\;t_2\;else\;t_3 : T}} & \text{(T-If)}\\
\end{array}
\end{array}

tapl08_1.pl

/*
構文

t ::=                項：
　true               定数真
　false              定数偽
　if(t,t,t)          条件式

v ::=                値：
　true               定数真
　false              定数偽

Ty ::=               型：
　bool               ブール値型
*/
:- 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).
v(true).
v(false).

% 評価 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).

% 新しい型付け規則 t : T

⊢ true : bool.                    % (T-True)

⊢ false : bool.                   % (T-False)

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

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))).
:- halt.