We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Algebras for iteration and infinite computations.
- Authors
Guttmann, Walter
- Abstract
We give axioms for an operation that describes iteration in various relational models of computations. The models differ in their treatment of finite, infinite and aborting executions, covering partial, total and general correctness and extensions thereof. Based on the common axioms we derive separation, refinement and program transformation results hitherto known from particular models, henceforth recognised to hold in many different models. We introduce a new model that independently describes the finite, infinite and aborting executions of a computation, and axiomatise an operation that extracts the infinite executions in this model and others. From these unifying axioms we derive explicit representations for recursion and iteration. We show that also the new model is an instance of our general theory of iteration. All results are verified in Isabelle heavily using automated theorem provers.
- Subjects
ITERATIVE methods (Mathematics); INFINITY (Mathematics); AXIOMS; MATHEMATICAL models; RECURSION theory; FINITE, The; NUMERICAL analysis
- Publication
Acta Informatica, 2012, Vol 49, Issue 5, p343
- ISSN
0001-5903
- Publication type
Article
- DOI
10.1007/s00236-012-0162-2