柯里-霍华德同构维基百科,自由的 encyclopedia 柯里-霍华德对应(英语:Curry-Howard correspondence)是在计算机程序和数学证明之间的紧密联系;这种对应也叫做柯里-霍华德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和数学运算之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德(英语: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)是在计算机程序和数学证明之间的紧密联系;这种对应也叫做柯里-霍华德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和数学运算之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德(英语:William Alvin Howard)独立发现的。 此条目已列出参考资料,但文内引注不足,部分内容的来源仍然不明。 (2019年3月6日) 以函数式编程写作的:在Coq软件中自然数加法交换性的证明。nat_ind 代表数学归纳,eq_ind 代替等于,f_equal 代表在等式两边取同样的函数。 前面的定理参照显示 m = m + 0和S(m + y)= m + S y。