上一页

ⓘ 类型论




类型论
                                     

ⓘ 类型论

在最广泛的层面上, 类型论 (英語: type theory )是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。在这种意义上,它与类型的形而上学概念有关。现代类型论在部分上是响应罗素悖论而发明的,并在伯特兰 罗素和阿弗烈 诺夫 怀海德的中起到重要作用。

在计算机科学分支中的编程语言理论中, 类型论 提供了设计分析和研究类型系统的形式基础。实际上,很多计算机科学家使用术语" 类型论”来称呼对编程语言的类型语言的形式研究,尽管有些人把它限制于对更加抽象的形式化如有类型lambda演算的研究。

                                     

1. 类型论体系

主要

  • 构造演算及其衍生理论。
  • 简单类型λ演算,一种高阶逻辑;
  • 系统F;
  • LF经常用来定义其他类型论;
  • 直觉类型论;

次要

  • 其他 纯类型系统 。
  • Automath ;
  • ST类型论;
  • 组合逻辑的一些形式;
  • λ立方体中定义的其他;
  • 其他有类型λ演算;

活跃

  • 正在研究中的同伦类型论
                                     

2. 参见

  • 类型系统
  • 范畴论
  • 有类型lambda演算
  • 罗素公理体系
  • 直觉类型论
  • 域理论