Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
432973 | Journal of Logical and Algebraic Methods in Programming | 2015 | 15 Pages |
•We axiomatise the states from which a computation has infinite executions.•We uniformly cover relational and matrix-based models of non-strict and strict computations.•We give a new instance of binary iterings.•We verify all results in Isabelle, heavily using its automated theorem provers.
We give axioms for an operation that describes the states from which a computation has infinite executions in several relational and matrix-based models. The models cover non-strict and strict computations which represent finite, infinite and aborting executions with varying precision. Based on the operation we provide an approximation order for a unified description of recursion. Least fixpoints in the approximation order are reduced to least and greatest fixpoints in the underlying semilattice order. We specialise this to a unified description of iteration which satisfies the axioms of a binary operation introduced in previous work. Previous consequences therefore generalise to all discussed computation models in a uniform way. All algebraic results are verified in Isabelle using its integrated automated theorem provers and SMT solvers.