【入門】CommonLisp【質問よろず】

【入門】CommonLisp【質問よろず】 at TECH

543:535
05/07/26 18:02:54
>>542
その通りです。
では、具体的な話。

λ計算中に現れる[lexp1/x]lexp2を表現する関数
(defun substitution (x lexp1 lexp2))の中で

x≠yかつφ(E)∋x、φ(Q)∋yをどちらも満たすなら
任意のλ式E、任意のz(ただしzはx≠z≠yかつ
(E)Qの自由変数でも束縛変数でもない)に対して
[Q/x]Ly.E → Lz.[Q/x]{z/y}E

って書き換えたいんです。
ここで、Lx.Ly.(y)xは(L x L y (y) x)と表現します。

次ページ

続きを表示

1を表示