1樓：林吟風
題目描述裡的「原始數值」有點奇怪，看了一下書裡面寫的是是「primitive number」。我覺得可能是翻譯版沒能有效傳達出書要表達的意思。這裡的 primitive number 指的是 TAPL 第三章圖 3-2 中描述的自然數。
可以發現在第五章的該節中邱奇數的 successor 函式被定義為 suc 以與在第三章中出現的語法 succ 做區分。 這裡 realnat = λ m. m (λx.
succ x) 0 中的 succ 指的就是第三章中的那個，意思是如果我們把無型別 lambda 演算直接加入到圖 3-2 描述的系統中的話，如何把用抽象表示的邱奇數轉換為圖 3-2 描述的系統中的數。
至於在 call by value 的求值策略下對 succ 1 求值的結果和 λf. λx. f (f x) 不一樣問題，雖然它們在項上不一樣，但使用 succ 1 的效果和使用 λf.
λx. f (f x) 是一樣的。所以 succ 1 無法進一步求值成 λf.
λx. f (f x) 沒什麼問題。（問題和原答案中應該是錯誤地使用了規約一詞， 非常感謝 @羅宸 指出）
Lambda 演算 中的 lambda 應該如何翻譯？
hpss 請記住這個符號.Lambda,is the 11th letter of the Greek alphabet,representing the sound l In the system of Greek numerals lambda has a value of 30. 劉羽豐 叫現...
什麼是 Lambda 演算？
song wang 老外寫了系列文章，cgnail 做了中文翻譯，非常棒，每篇翻譯都有原文的鏈結。我的最愛Lambda演算 開篇 cgnail s weblog阿隆佐.丘奇的天才之作 lambda演算中的數字 cgnail s weblog Lambda演算中的布林值和選擇 cgnail s web...
lambda演算求值順序的問題？
彭飛 這是call by value 你沒看懂這個operational semantics 主要有以下幾點原因 1.無論是call by value 還是call by name 都只對引數而言，在決定引數的求值 evaluation 之前先要完成函式的求值 即這裡的t1 因為你不能保證程式中出現...