[LISPプログラミング] ラムダ計算 - 置換(substitution)
LISPプログラミングの課題についての質問(その2)です.
以下に,課題,課題を解くのに必要な知識,試作したプログラム,質問を,この順に載せます.長くなりますがご了承ください.なお,この質問に答えられる方(LISPとラムダ計算の両方の知識がある方)は, http://okwave.jp/qa5152352.html の質問にもお答えいただけると幸いです.
【課題】λ式のリダクションに関する以下の関数を作成せよ.
2. [lexp1/x]lexp2 を表現する関数 substitution
(substitution 'x lexp1 lexp2)
【課題で扱うλ式,ラムダ計算(抜粋)】
A. λ式のシンタックス(を BNF で記述したもの)は以下のとおりである.
<λ-expression> ::= <variable> | <application> | <abstraction>
<application> ::= (<λ-expression>)<λ-expression>
<abstraction> ::= λ<variable>.<λ-expression>
以下,変数(variable)を小文字 x,y,z,... で,任意のλ式を大文字 P,Q,R,... で表す.
B. λ式 P と Q が文字まで含めてまったく同じであるとき,P と Q が等しいといい, P≡Q と記す.また,等しくないときは P≡/≡Q と記す.
C. 自由変数集合
λ式 E の自由変数の集合を φ(E) と記す.
(1) c が定数ならば,φ(c)={}
(2) 任意の変数 x に対して φ(x)={x}
(3) φ(λx.P)=φ(P)-{x}
(4) φ((P)Q)=φ(P)∪φ(Q)
D. λ式 M と N がα合同であることを M=N と記す.
E. P 中のすべての自由変数 x を Q で置換(substitution)することを [Q/x]P と記す.
(1) [Q/x]x=Q
(2) x≡/≡y ならば [Q/x]y=y
(3) 任意のλ式 E に対して [Q/x]λx.E=λx.E
(4) x≡/≡y かつ「xがφ(E)に含まれない,または,yがφ(Q)に含まれない」ならば,任意のλ式 E に対して [Q/x]λy.E=λy.[Q/x]E
(5) x≡/≡y かつ x∈φ(E) かつ y∈φ(Q) ならば,任意のλ式 E ,任意の z(ただし,z は x≡/≡z≡/≡y かつ E(Q) の自由変数でも束縛変数でもない)に対して [Q/x]λy.E=λz.[Q/x]{z/y}E
(6) [Q/x](E1)E2=([Q/x]E1)[Q/x]E2
【試作したプログラム】
; 2. [lexp1/x]lexp2 を表現する関数 substitution
; (substitution 'x lexp1 lexp2)
(defun substitution (x lexp1 lexp2)
(if (= (length lexp2) 1)
(if (equal x (car lexp2)) lexp1 lexp2) ; then (1), else (2)
(if (equal 'L (car lexp2))
(if (equal x (second lexp2))
lexp2 ; (3)
; (4),(5)に対応する処理
)
(if (listp (car lexp2))
(list (list (substitution x lexp1 (car lexp1)))
(substitution x lexp1 (cdr lexp2))) ; (6)
lexp2
)
)
)
)
【質問】
ラムダ計算というもの自体初耳で,良く分からないまま作成したプログラムです.「E. 置換」の (1),(2),(3),(6) をそのままプログラムにしたつもりです.しかし,自由変数とか束縛変数とかいう概念を無視して作成したので,おそらく誤った動作をすると思います.また,(4),(5)に対応する処理をどのように記述したらよいのかが分かりません.誤りの指摘,アドバイスをお願いします.
お礼
わざわざ新たな回答ありがとうございます。 let<->lambdaの変換は自分でも出来るようにがんばります。 おかげで解くことが出来そうです