TAPL3-1.ブール値(B)

この記事はProlog Advent Calendar 2016の５日目の記事です。

今日はTAPL図3-1をPrologで実装してみます。

\begin{array}{l|l}

\begin{array}{l}
構文\\
\begin{array}{lcr}
t ::=  &             & 項：\\
 &true               & 定数真\\
 &false              & 定数偽\\
 &if \;t\;then\;t\;else\;t & 条件式\\

v ::= & &              値：\\
   & true &             定数真\\
   & false &            定数偽\\
\end{array}
\end{array}
&
\begin{array}{l}
\begin{array}{cr}
評価  \hspace{320px} & \bbox[3px,border:1px solid black]{t \longrightarrow t’}\\
if\;true\;then\;t_2\;else\;t_3 \longrightarrow t_2   & \text{(E-IfTrue)}\\
if\;false\;then\;t_2\;else\;t_3 \longrightarrow t_3  & \text{(E-IfFalse)}\\

\dfrac{t_1 \longrightarrow t_1’}
{if\; t_1\; then\; t_2\; else\; t_3
\longrightarrow if\; t_1’\; then\; t_2\; else\; t_3}
& \text{(E-IfTrue)}
\\
\\
\\
\\
\end{array}
\end{array}
\end{array}

が元のTAPLの構文と、評価規則ですが、if then elseはprologの項として表すのは優先順位をちゃんと表すのはめんどうなので、楽にif(t,t,t)としてみます。

tapl03_1.pl

/*
構文

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

v::=                 値：
　true               定数真
　false              定数偽
*/
:- 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 ==>> T3 :- T ==> T2, T2 ==>> T3.
T ==>> T.

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