[Prev][Next][Index][Thread]
Categorial View of Loop Invariants
Date: Wed, 24 Apr 91 11:12:27 bst
Program loops have a very simple categorical interpretation, as loop
diagrams, i.e. as diagrams with one object C and one morphism f,
necessarily an endomorphism of C.
--
/ \
| |
| \/
|
f | C
|
| |
\ /
--
Of course, the limit of the loop is its fixpoints. The colimit,
however, is even more interesting. A cocone for the diagram is a
morphism g:C-->Q such that f;g = g. That is, an *invariant* for the
loop. Thus the colimit is the universal invariant of the loop.
Definition
A loop *converges* if it has an object of invariants Inv(f)
which is also an object of fixpoints such that the canonical composite
Inv(f) --> C --> Inv(f)
is the identity.
This property captures the desirable property of a loop that its
iteration approaches a fixpoint. The simplest way to achieve this is
if the loop always terminates after a finite number of steps. While
such *termination* is equivalent to convergence in the category of
Sets, the topological nature of domain theory allows convergence
without termination.
There are two technical reports available which exploit such loops.
Fixpoint and loop constructions as colimits
and
Tail recursion via universal invariants
The first shows how to interpret while-loops in domains, and give
termination conditions. The second gives a categorical account of tail
recursion, and establishes conditions under which a tail recursive
characterisation of finite lists is equivalent to the usual intial
algera construction.
Copies of the latex code for either paper can be obtained by e-mail
request (sorry - no ftp here yet!). Please specify if you need a copy
of Paul Taylor's diagrams package: diagrams3.
Barry Jay