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)と表現します。