［LISPプログラミング］ ラムダ計算 － 置換（substitution）

質問

LISPプログラミングの課題についての質問（その２）です．

以下に，課題，課題を解くのに必要な知識，試作したプログラム，質問を，この順に載せます．長くなりますがご了承ください．なお，この質問に答えられる方（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)に対応する処理をどのように記述したらよいのかが分かりません．誤りの指摘，アドバイスをお願いします．

回答No.1

nininonick · ベストアンサー

λx.E1という式の場合、
(E1の中に現れる)xはE1における束縛変数といいます。
同様に、λx.λy.E2の場合、
(E2の中に現れる)xとyはE2における束縛変数です。

E3という式の中で、λx.E4の形の式が現れず、かつxがE3の中に現れれば、
xはE3における自由変数といいます。
ここではこれをx∈φ(E3)と書き表します。

> (4) x≡/≡y かつ「xがφ(E)に含まれない，または，yがφ(Q)に含まれない」ならば，任意のλ式 E に対して [Q/x]λy.E＝λy.[Q/x]E
xがφ(E)に含まれない場合は、そもそも置換による影響がでません。
よって、(4)はyがφ(Q)に含まれない場合に、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
y∈φ(Q)なので、Qの中に現れるyは「自由変数」です。
しかし、これをEの中のxと置き換えてしまうと、
Qの中のyが「束縛変数」になってしまいます。
そこで、先にEの中に現れるyをすべて別名に書き換えてから
置換を行うというのが(5)です。

以下は実際に動作するプログラムです。

---
;;; このプログラムはCommon Lispで記述しています。
;;; ラムダ式をどのようにLispのリストに変換するかの規則が載っていなかったので、
;;; 変換規則を次のようなものとしてプログラムを作成しました。
;;; x ===> (x)
;;; λx.E ===> (l x . E)
;;; (E1)E2 ===> (E1 . E2)
;;;
(defun free-vars (lexp)
　(cond ((= (length lexp) 1)
　　　　 lexp)　; atom is variable (Don't think about constant).
　　　　((eq (car lexp) 'l)
　　　　 (remove (cadr lexp)
　　　　　　　　 (free-vars (cddr lexp))))
　　　　((consp (car lexp))
　　　　 (union (free-vars (car lexp))
　　　　　　　　(free-vars (cdr lexp))))
　　　　(t (error "Bad lambda expression."))))

(defun substitution (x lexp1 lexp2)
　(cond ((= (length lexp2) 1)
　　　　 (if (eq x (car lexp2)) lexp1 lexp2))
　　　　((eq (car lexp2) 'l)
　　　　 (cond ((eq x (cadr lexp2))
　　　　　　　　lexp2)
　　　　　　　　((or (not (member x (free-vars (cddr lexp2))))
　　　　　　　　　　 (not (member (cadr lexp2) (free-vars lexp1))))
　　　　　　　　 (print 1)
　　　　　　　　 (list* 'l (cadr lexp2) (substitution x lexp1 (cddr lexp2))))
　　　　　　　　((and (member x (free-vars (cddr lexp2)))
　　　　　　　　　　　(member (cadr lexp2) (free-vars lexp1)))
　　　　　　　　 (print 2)
　　　　　　　　 (let ((z (gensym)))
　　　　　　　　　 (list* 'l z (substitution
　　　　　　　　　　　　　　　　x
　　　　　　　　　　　　　　　　lexp1
　　　　　　　　　　　　　　　　(substitution (cadr lexp2) z (cddr lexp2))))))
　　　　　　　　(t (error "Bad lambda abstraction."))))
　　　　((consp (car lexp2))
　　　　 (cons (substitution x lexp1 (car lexp2))
　　　　　　　 (substitution x lexp1 (cdr lexp2))))
　　　　(t (error "Bad lambda expression."))))

お礼

ご回答ありがとうございました．大変参考になりました．