• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Type Theory based on Dependent Inductive and Coinductive Types
【24h】

Type Theory based on Dependent Inductive and Coinductive Types

机译：基于从属归纳和共归类型的类型理论

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For example, all well-known basic types and type formers that are needed for using this type theory as a logic are definable: propositional connectives, like falsity, conjunction, disjunction, and function space, dependent function space, existential quantification, equality, natural numbers, vectors etc. The reduction relation on terms consists solely of a rule for recursion and a rule for corecursion. The reduction relations for well-known types arise from that. To further support the introduction of this new type theory, we also prove fundamental properties of its term calculus. Most importantly, we prove subject reduction and strong normalisation of the reduction relation, which gives computational meaning to the terms. The presented type theory is based on ideas from categorical logic that have been investigated before by the first author, and it extends Hagino's categorical data types to a dependently typed setting. By basing the type theory on concepts from category theory we maintain the duality between inductive and coinductive types, and it allows us to describe, for example, the function space as a coinductive type.
机译：我们开发了一个纯粹基于归纳和共归类型以及相应的递归和共归原则的从属类型理论。这样就产生了具有少量规则的类型理论，同时仍然具有相当的表现力。例如，使用这种类型理论作为逻辑所需要的所有众所周知的基本类型和类型形成器都是可定义的：命题连接词，如虚假性，合取性，析取性和函数空间，从属函数空间，存在性量化，等式，自然数字，向量等。术语的约简关系仅包含递归规则和核心递归规则。由此产生公知类型的归约关系。为了进一步支持这种新型理论的引入，我们还证明了其术语演算的基本性质。最重要的是，我们证明了主题约简和约简关系的强归一化，这给这些术语带来了计算上的意义。提出的类型理论基于第一位作者之前研究过的分类逻辑思想，并将Hagino的分类数据类型扩展为依存类型设置。通过将类型理论基于类别理论中的概念，我们保持了归纳类型和共归类型之间的对偶性，并允许我们将例如功能空间描述为共归类型。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号