Curry-Howard 對應是在電腦程式和數學證明之間的緊密聯繫；這種對應也叫做 Curry-Howard 同構或公式為類型對應。已經採用了一些不同的公式化，它的原理現在被認為是由美國數學家 Haskell Curry 和邏輯學家 William Alvin Howard 獨立發現的。
基本介紹
- 中文名：Curry-Howard同構
- 外文名：Curry-Howard
- 發現：美國數學家 Haskell Curry
- 作用：加顯著的地位的動機所推動
介紹,對應,
介紹
Curry-Howard 對應是在電腦程式和數學證明之間的緊密聯繫；這種對應也叫做 Curry-Howard 同構或公式為類型對應。已經採用了一些不同的公式化，它的原理現在被認為是由美國數學家 Haskell Curry 和邏輯學家 William Alvin Howard 獨立發現的。
對應可以在兩個層面上看到，首先是類比層次，它聲稱一個函式計算出的值的類型的斷言類比於一個邏輯定理，計算這個值的程式類比於這個定理的證明。在理論計算機科學中，這是連線lambda 演算和類型論的毗鄰領域的一個重要的底層原理。它被經常以下列形式陳述為證明是程式。一個可選擇的形式化為命題為類型。其次，更加正式的，它指定了在兩個數學領域之間的同構，就是以一種特定方式形式化的自然演繹，和簡單類型 lambda 演算之間是雙射，首先是證明和項，其次是證明歸約步驟和 beta 歸約。
對應
有多種方式考慮 Curry-Howard 對應。在一個方向上，它工作於編譯證明為程式級別上。這裡的證明，最初被限定為構造性邏輯 — 典型的是直覺邏輯系統中的證明。而程式是在常規的函式式編程的意義上的；從語法的觀點上看，這種程式是用某種 lambda 演算表達的。所以 Curry-Howard 同構的具體實現是詳細研究如何把來自直覺邏輯的證明寫成 lambda 項。(這是 Howard 的貢獻；Curry 貢獻了組合子，它是相對於是高級語言的 lambda 演算是能寫所有東西的機器語言)。最近，同樣處理經典邏輯的 Curry-Howard 對應的擴展可被公式化了，通過對經典有效規則比如雙重否定除去和 Peirce 定律關聯上明確的用續體比如 call/cc 處理的一類項。
還有一個相反的方向，對一個程式的正確性關聯上證明提取的可能性。這在非常豐富的類型論環境中是可行的。實際上理論家對非常豐富類型的函式式程式語言的開發，已經部分的被希望帶給 Curry-Howard 對應更加顯著的地位的動機所推動。
