[問題] abstration in combinatory logic

[etwas (i'm only dust)]

大家好,
小弟在看 Hindley & Seldin 的 Lambada-Calculus and Combinators -- an Introduction
遇到一個問題
想請教各位大大.
Exercise 2.22 裡面要 evaluate
[x].uxxv
答案是
S(SuI)(Kv)

根據的是
Definition 2.18(Abstraction) for combinatory logic terms
(a) [x].M ≡ KM  if x    FV(M);
(b) [x].x ≡ I;
(c) [x].Ux ≡ U;  if x    FV(U);
(d) [x].UV ≡ S([x].U)([x].V)  if either (a) nor (c) applies.

假如apply不同的rule會得到不同的答案
e.g.
[x].uxxv
≡ S([x].ux)([x].xv)    by (d)
≡ Su([x].xv)           by (c)
≡ Su(S([x].x)([x].v))  by (d)
≡ Su(SI(Kv))

除了definition 明寫 (d)需要是if either (a) nor (c) applies
我沒有讀到有其他的限制
所以不知道是不是本來就是apply不同的rule會得到不同的答案


謝謝


--

'TIS better to be vile than vile esteem'd
                                ~William Shakespeare

--
※ 發信站: 批踢踢實業坊(ptt.cc) 
◆ From: 188.74.78.60
→ etwas:(a)和(c) 的是 if x doesn't occur in FV(M) 和
→ etwas:if x doesn't occur in FV(U)
→ etwas:呃 doesn't belong to FV...
推 SansWord:這是parse問題， [x].uxxv 實際ast是？