Proving Termination of Normalization Functions for Conditional Expressions
<|reference_start|>Proving Termination of Normalization Functions for Conditional Expressions: Boyer and Moore have discussed a recursive function that puts conditional expressions into normal form [1]. It is difficult to prove that this function terminates on all inputs. Three termination proofs are compared: (1) using a measure function, (2) in domain theory using LCF, (3) showing that its recursion relation, defined by the pattern of recursive calls, is well-founded. The last two proofs are essentially the same though conducted in markedly different logical frameworks. An obviously total variant of the normalize function is presented as the `computational meaning' of those two proofs. A related function makes nested recursive calls. The three termination proofs become more complex: termination and correctness must be proved simultaneously. The recursion relation approach seems flexible enough to handle subtle termination proofs where previously domain theory seemed essential.<|reference_end|>
@article{paulson2000proving,
    title={Proving Termination of Normalization Functions for Conditional
  Expressions},
    author={Lawrence C. Paulson},
    journal={Journal of Automated Reasoning 2 (1986), 63-74},
    year={2000},
    archivePrefix={arXiv},
    eprint={cs/9301103},
    primaryClass={cs.LO}
}