ラムダ計算機(lambda calculus)における自由変数の求め方

Question

ラムダ計算機について理解するために、自由変数を求めたいのですが、うまく求められないのでお力添えをいただきたいです。

定義:
FV(x) = x
FV(λx.e) = FV(e){x}
FV(e_1, e_2) = FV(e1) ∪ FV(e2)

但し、xは変数、e,e_1及びe_2は関数です

問題:
FV(((λf.λy.λx.f(y(x)))(λx.y+z))(λz.y-x))

理解のために計算の過程まで書いていただけますようお願いします。
お手数ですがよろしくお願いいたします。

Comments

[ikedas]

勉強するのに使っている教科書を明記してください。題名と著者名があればいいですが、ご質問に関連する事項が書いてあるページ数があればより良いです。

Answer 1

上述定義通りにやったところ、求めることができました。