柯里-霍华德同构維基百科,自由的 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。