کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
432973 | 689180 | 2015 | 15 صفحه PDF | دانلود رایگان |
• 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.
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 84, Issue 3, May 2015, Pages 326–340