Correct Computation Rules for Recursive Languages
Peter J. Downey, Ravi Sethi · SIAM Journal on Computing · 1976
This paper considers simple, LISP-like languages for the recursive definition of functions. We focus on the connections between formal computation rules for calculation with recursive definitions, and the mathematical semantics of such definitions. A computation rule is correct when it is capable of computing the least fixpoint of a recursive definition. We give necessary and sufficient conditions for the correctness of rules under (a) all possible interpretations and (b) particular interpretations.