A semantics of loops (and while-loops) where objects are types (not predicates) can be found in @InProceedings(Jay91d, Author={Jay, C.B.}, Title={Fixpoint and loop constructions as colimits}, Booktitle="Proceedings Summer Conference on Category Theory, Como 1990", Editor="A.~Carboni, M.C.~Pedicchio and G.~Rosolini", Series=Lecture Notes in Mathematics, Volume=1488, Publisher=sv, Year=1991, Pages={187--192}) and their use to account for tail-recursion is in @Article(Jay93a, Author={Jay, C.B.}, Title={Tail recursion through universal invariants}, Journal=Theoretcial Computer Science, Volume=115, Year=1993, Pages={151--189}) Barry Jay