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.
Previous | Index | Next