LoginSignup
1

More than 5 years have passed since last update.

TAPL5-3. 型無しラムダ計算(λ)

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

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
1