我没看过你那本书，不过我想那本书应该不会违背大家习惯的用法。 uxxv 通常是 ((ux)x)v 的意思，所以你把他解读成 (ux)(xv) 就不一样了。 根本问题是，省掉括号以後，符号是左结合还右结合？application 通常是 左结合，所以那题答案是这样出来的： [x].uxxv ≡ S([x].uxx)([x].v) by (d) -- uxxv 要理解成 (uxx)v ≡ S(S([x].ux)([x].x))(Kv) by (d), (a) -- uxx 要理解成 (ux)x ≡ S(SuI)(Kv) by (c), (b) 另外本来就可以有很多不同的等价写法。甚至只要 SK 就可以定义 I. 这里顶多是告诉你某个转换方法行得通。大致看过去觉得这组规则在任一 状况下应该只有一条规则可以用，所以转换结果应该是唯一的。 ※ 引述《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会得到不同的答案 : 谢谢 --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 140.112.30.39 ※ 编辑: Favonia 来自: 140.112.30.39 (06/08 04:12) ※ 编辑: Favonia 来自: 140.112.30.39 (06/08 04:12) ※ 编辑: Favonia 来自: 140.112.30.39 (06/16 08:49)