Curry—Howard同构理论:研究综述 |
| |
引用本文: | 张昱. Curry—Howard同构理论:研究综述[J]. 计算机科学, 2002, 29(4): 9-11 |
| |
作者姓名: | 张昱 |
| |
作者单位: | 软件新技术国家重点实验室,南京大学计算机科学与技术系南京 210093 |
| |
摘 要: | 一、引言理论计算机科学的发展吸取了大量数学和逻辑上的重要成果。逻辑是理论计算机科学十分重要的基础之一,而其中又以直觉主义逻辑对计算机科学的影响最为显著,它的思想比古典逻辑更加切合计算的观点。另一个值得一提的成果就是Alonzo Church在1936年提出的λ-演算系统,λ-演算所依据的是一种完全不同于逻辑的思想,它是计算机科学中函数式程序设计语言的理论基础。这是两种无论从语祛上还是从语义上去观察都区别甚大的形式系统,然而它们之间却存在着某种奇妙的对应关系,这就是本文所要介绍的Curry-Howard同构理论(Curry-Howard Isomorphism)。
|
关 键 词: | 计算机科学 Curry-Howard同构理论 直觉主义逻辑 命题演算 |
A Survey of Curry-Howard Isomorphism |
| |
Abstract: | |
| |
Keywords: | |
本文献已被 CNKI 维普 万方数据 等数据库收录! |
|
点击此处可从《计算机科学》下载全文 |
|