Curry-HOWard同构理论:研究综述

摘要：

@@ 一、引言
理论计算机科学的发展吸取了大量数学和逻辑上的重要成果.逻辑是理论计算机科学十分重要的基础之一,而其中又以直觉主义逻辑对计算机科学的影响最为显著,它的思想比古典逻辑更加切合计算的观点.另一个值得一提的成果就是Alonzo Church在1936年提出的λ-演算系统,λ-演算所依据的是一种完全不同于逻辑的思想,它是计算机科学中函数式程序设计语言的理论基础.这是两种无论从语法上还是从语义上去观察都区别甚大的形式系统,然而它们之间却存在着某种奇妙的对应关系,这就是本文所要介绍的Curry-Howard同构理论(Curry-Howard Isomorphism).

机标关键词：理论计算机科学、直觉主义逻辑、函数式程序设计语言、演算系统、形式系统、同构理论、思想、基础、古典逻辑、对应关系、成果、语义、语法、数学

所属期刊栏目：29

分类号：TP31(计算技术、计算机技术)

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：9-11