Re: [問題] abstration in combinatory logic

看板PLT (程式語言與理論)作者Favonia (貓貓最乖了)時間13年前 (2011/06/08 04:11)推噓1(1推 0噓 0→)

留言1則, 1人參與討論串2/2 (看更多)

我沒看過你那本書，不過我想那本書應該不會違背大家習慣的用法。 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)