Tail Recursion Through Universal Invariants

C Barry Jay

Abstract: Tail recursive constructions suggest a new semantics for datatypes, which allows a direct match between specifications and tail recursive programs. The semantics focusses on loops, their fixpoints, invariants and convergence. Convergent models of the natural numbers and lists are examined in detail, and, under very mild conditions, are shown to be equivalent to the corresponding initial algebra models.

LFCS report ECS-LFCS-92-205

Previous | Index | Next