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