• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Mathematically structured functional programming >Hereditary Substitutions for Simple Types, Formalized
【24h】

Hereditary Substitutions for Simple Types, Formalized

机译：简单类型的遗传替代，正式化

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We analyze a normalization function for the simply typed A-calculus based on hereditary substitutions, a technique developed by Pfenning et al. The normalizer is implemented in Agda, a total language where all programs terminate. It requires no termination proof since it is structurally recursive which is recognized by Agda's termination checker. Using Agda as an interactive theorem prover we establish that our normalization function precisely identifies βη-equivalent terms and hence can be used to decide βη-equality. An interesting feature of this approach is that it is clear from the construction that βη-equality is primitive recursive.
机译：我们分析了基于遗传替代的简单类型A演算的归一化函数，这是Pfenning等人开发的技术。规范化器以Agda（所有程序终止的总语言）实现。它不需要递归证明，因为它在结构上是递归的，可被Agda的递归检查器识别。使用Agda作为交互式定理证明者，我们确定我们的归一化函数可以精确地标识βη等价项，因此可以用来确定βη等价。这种方法的一个有趣特征是，从构造中可以清楚地看出，βη-等式是原始递归的。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号