条件表达式规范化函数的终止性证明
计算机科学中的逻辑
2009-09-25 v1
摘要
Boyer 和 Moore 讨论了一个将条件表达式转化为范式的递归函数 [1]。证明该函数在所有输入上终止是困难的。本文比较了三种终止性证明：(1) 使用测度函数，(2) 在域理论中使用 LCF，(3) 证明由递归调用模式定义的递归关系是良基的。后两个证明本质上是相同的，尽管它们在显著不同的逻辑框架中进行。该 normalize 函数的一个明显全变体被呈现为这两个证明的“计算含义”。一个相关的函数进行嵌套递归调用。这三种终止性证明变得更加复杂：终止性和正确性必须同时证明。递归关系方法似乎足够灵活，能够处理微妙的终止性证明，而以前这些证明似乎需要域理论。
引用
@article{arxiv.cs/9301103,
title = {Proving Termination of Normalization Functions for Conditional Expressions},
author = {Lawrence C. Paulson},
journal= {arXiv preprint arXiv:cs/9301103},
year = {2009}
}