柯里-霍華德同構維基百科,自由的 encyclopedia 柯里-霍華德對應(英語:Curry-Howard correspondence)是在計算機程序和數學證明之間的緊密聯繫;這種對應也叫做柯里-霍華德同構、公式為類型對應或命題為類型對應。這是對形式邏輯系統和公式計算(computational calculus)之間符號的相似性的推廣。它被認為是由美國數學家哈斯凱爾·柯里和邏輯學家威廉·阿爾文·霍瓦德(William Alvin Howard)獨立發現的。 此條目已列出參考資料,但文內引註不足,部分內容的來源仍然不明。 (2019年3月6日) 以函數式編程寫作的:在Coq軟件中自然數加法交換性的證明。nat_ind 代表數學歸納,eq_ind 代替等於,f_equal 代表在等式兩邊取同樣的函數。 前面的定理參照顯示 m = m + 0和S(m + y)= m + S y。
柯里-霍華德對應(英語:Curry-Howard correspondence)是在計算機程序和數學證明之間的緊密聯繫;這種對應也叫做柯里-霍華德同構、公式為類型對應或命題為類型對應。這是對形式邏輯系統和公式計算(computational calculus)之間符號的相似性的推廣。它被認為是由美國數學家哈斯凱爾·柯里和邏輯學家威廉·阿爾文·霍瓦德(William Alvin Howard)獨立發現的。 此條目已列出參考資料,但文內引註不足,部分內容的來源仍然不明。 (2019年3月6日) 以函數式編程寫作的:在Coq軟件中自然數加法交換性的證明。nat_ind 代表數學歸納,eq_ind 代替等於,f_equal 代表在等式兩邊取同樣的函數。 前面的定理參照顯示 m = m + 0和S(m + y)= m + S y。