کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
432973 689180 2015 15 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Infinite executions of lazy and strict computations
ترجمه فارسی عنوان
اعدام بی انتها محاسبات تنبل و سخت
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی


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

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 84, Issue 3, May 2015, Pages 326–340
نویسندگان
,