Delay Monad 中的归一化求值：通过 Copatterns 和 Sized Types 进行共归纳的案例研究
计算机科学中的逻辑
2014-06-10 v1 编程语言
摘要
本文展示了简单类型 lambda 项归一化器的 Agda 形式化。该归一化器由 delay monad 中两个共归纳定义的函数组成：一个是将 lambda 项求值为闭包的标准求值器，另一个是从值到 eta-long beta-正规形的类型导向重ifier。它们的组合，即归一化求值，通过使用标准的逻辑关系论证被事后证明为全函数。这一成功的形式化作为使用 sized types 和 copatterns 进行共归纳编程和推理的概念验证，这是 Agda 的一项新颖且目前处于实验阶段的特性。
引用
@article{arxiv.1406.2059,
title = {Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types},
author = {Andreas Abel and James Chapman},
journal= {arXiv preprint arXiv:1406.2059},
year = {2014}
}
备注
In Proceedings MSFP 2014, arXiv:1406.1534