\begin{array}{l|l}
\begin{array}{l}
構文\\
\begin{array}{llr}
t ::= & & 項：\\
& x & 変数\\
& \lambda x.t & ラムダ抽象\\
& t\;t & 関数適用\\
v::= & & 値：\\
& \lambda x.t & ラムダ抽象値\\
\end{array}
\end{array}&
\begin{array}{cr}
評価 \hspace{180px} & \bbox[3px,border:1px solid black]{t \longrightarrow t’} \\
\dfrac{t_1 \longrightarrow t_1’}
{t_1 \;t_2 \longrightarrow t_1’ \;t_2} & \text{(E-App1)} \\
\dfrac{t_2 \longrightarrow t_2’}
{v_1 \; t_2 \longrightarrow v_1 \; t_2’} & \text{(E-App2)}\\
(\lambda x.t_{12}) v_2 \longrightarrow [x \mapsto v_2]t_{12} & \text{(E-AppAbs)}\\
\\
\end{array}
\end{array}
tapl05_3.pl
:- op(500, yfx, $).
:- op(920, xfx, [ ==>, ==>> ]).
:- op(1200, xfx, [ -- ]).
:- style_check(-singleton).
term_expansion(A -- B, B :- A).
/*
構文
t ::= 項：
x 変数
x -> t ラムダ抽象
t $ t 関数適用
v::= 値：
x->t ラムダ抽象値
*/
t(X) :- var(X).
t(X->T) :- var(X), t(T).
t(T1$T2) :- t(T1),t(T2).
v(X->T) :- var(X), t(T).
% 評価 t ==> t’
\+ v(T1), T1 ==> T1_
--%---------------------------------------- (E-App1)
T1 $ T2 ==> T1_ $ T2.
T2 ==> T2_
--%---------------------------------------- (E-App2)
V1 $ T2 ==> V1 $ T2_.
copy_term(X->T12, V2->T12_)
--%---------------------------------------- (E-AppAbs)
(X->T12) $ V2 ==> T12_.
T ==>> T3 :- T ==> T2, T2 ==>> T3.
T ==>> T.
run(T) :- T ==>> T2, writeln(T==>>T2).
:- run(X->X).
:- run((X->X) $ (Y->Y)).
:- halt.