0

More than 5 years have passed since last update.

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

Last updated at Posted at 2016-12-07
\begin{array}{lr}

\begin{array}{llr}
\bbox[lightgray]T ::= & …    & \hspace{170px} 型：\\
& \bbox[lightgray]{Bool} & ブール値型\\
\end{array}\\
\\
\begin{array}{cr}

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


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