Cedille 中的值历程归纳
计算机科学中的逻辑
2019-03-08 v2
摘要
在范畴论设定中，histomorphism 对建模一种值历程递归模式，该模式允许使用任意先前计算的值来定义函数。在本文中，我们使用依赖 Lambda 消去演算（CDLE）推导出一种归纳数据类型的 lambda 编码，其支持值历程归纳。类似于值历程递归，值历程归纳可在函数归纳参数的任意深度处访问归纳假设。我们通过证明 Lambek 引理并刻画该归纳原理的计算行为，表明所推导的值历程数据类型具有良好性质。我们的工作在 Cedille 编程语言中形式化，并包含若干值历程函数的示例。
引用
@article{arxiv.1811.11961,
title = {Course-of-Value Induction in Cedille},
author = {Denis Firsov and Larry Diehl and Christopher Jenkins and Aaron Stump},
journal= {arXiv preprint arXiv:1811.11961},
year = {2019}
}