LoginSignup
0

More than 5 years have passed since last update.

TAPL3-1.ブール値(B)

Last updated at Posted at 2016-12-03

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

今日は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.

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