Curry-Howard同構

標籤: 暫無標籤

8

更新時間: 2013-08-30

廣告

Curry-Howard 對應是在計算機程序和數學證明之間的緊密聯繫;這種對應也叫做 Curry-Howard 同構或公式為類型對應。已經採用了一些不同的公式化,它的原理現在被認為是由美國數學家 Haskell Curry 和邏輯學家 William Alvin Howard 獨立發現的。

 

Curry-Howard同構 -簡介

對應可以在兩個層面上看到,首先是類比層次,它聲稱一個函數計算出的值的類型的斷言類比於一個邏輯定理,計算這個值的程序類比於這個定理的證明。在理論計算機科學中,這是連接lambda 演算和類型論的毗鄰領域的一個重要的底層原理。它被經常以下列形式陳述為證明是程序。一個可選擇的形式化為命題為類型。其次,更加正式的,它指定了在兩個數學領域之間的同構,就是以一種特定方式形式化的自然演繹,和簡單類型 lambda 演算之間是雙射,首先是證明和項,其次是證明歸約步驟和 beta 歸約。

有多種方式考慮 Curry-Howard 對應。在一個方向上,它工作於編譯證明為程序級別上。這裡的證明,最初被限定為構造性邏輯 — 典型的是直覺邏輯系統中的證明。而程序是在常規的函數式編程的意義上的;從語法的觀點上看,這種程序是用某種 lambda 演算表達的。所以 Curry-Howard 同構的具體實現是詳細研究如何把來自直覺邏輯的證明寫成 lambda 項。(這是 Howard 的貢獻;Curry 貢獻了組合子,它是相對於是高級語言的 lambda 演算是能寫所有東西的機器語言)。最近,同樣處理經典邏輯的 Curry-Howard 對應的擴展可被公式化了,通過對經典有效規則比如雙重否定除去和 Peirce 定律關聯上明確的用續體比如 call/cc 處理的一類項。

還有一個相反的方向,對一個程序的正確性關聯上證明提取的可能性。這在非常豐富的類型論環境中是可行的。實際上理論家對非常豐富類型的函數式編程語言的開發,已經部分的被希望帶給 Curry-Howard 對應更加顯著的地位的動機所推動。

Curry-Howard同構 -相關

計算機

廣告

廣告