Article ID Journal Published Year Pages File Type
432973 Journal of Logical and Algebraic Methods in Programming 2015 15 Pages PDF
Abstract

•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.

Keywords
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
,