一千萬個為什麽

搜索

Y組合符是否與Curry-Howard對應相矛盾?

Y組合子的類型為$(a \ rightarrow a)\ rightarrow a $。通過Curry-Howard函數,因為類型$(a \ rightarrow a)\ rightarrow a $有人居住,它必須對應於一個真正的定理。但是$ a \ rightarrow a $總是如此,所以看起來好像Y組合子的類型對應於定理$ a $,這並不總是正確的。怎麽會這樣?

最佳答案

原始的庫裏 - 霍華德對應是直覺主義命題邏輯和簡單類型的lambda演算之間的同構。

當然還有其他類似庫裏 - 霍華德的同構;菲爾·瓦德勒(Phil Wadler)著名地指出,雙管名稱“庫裏 - 霍華德”(Curry-Howard)預測其他雙管名稱如“Hindley-Milner”和“Girard-Reynolds”。如果“Martin-Löf”就是其中之一,那將會很有趣,但事實並非如此。但我離題了。

由於一個關鍵原因,Y組合子與此並不矛盾:它在簡單類型的lambda演算中是不可表達的。

事實上,這就是重點。 Haskell Curry在無類型lambda演算中發現了固定點組合子,並用它來證明無類型lambda演算不是一個合理的演繹系統。

有趣的是,Y的類型對應於一個邏輯悖論,這個悖論並不像它應該的那樣眾所周知,稱為庫裏的悖論。考慮這句話:

如果這句話是真的,那麽聖誕老人就存在了。

假設這句話是真的。然後,顯然,聖誕老人會存在。但這正是句子所說的,所以句子是真的。因此,聖誕老人存在。 QED

轉載註明原文: Y組合符是否與Curry-Howard對應相矛盾?