A big step from finite to infinite computations

被引：3

作者：

Ancona, Davide ^{[1
]}

Dagnino, Francesco ^{[1
]}

Rot, Jurriaan ^{[2
]}

Zucca, Elena ^{[1
]}

机构：

[1] Univ Genoa, DIBRIS, Genoa, Italy

[2] Radboud Univ Nijmegen, Nijmegen, Netherlands

来源：

SCIENCE OF COMPUTER PROGRAMMING | 2020年 / 197卷

关键词：

Operational semantics; Infinite behavior; Coinduction; OPERATIONAL SEMANTICS; LOGIC;

D O I：

10.1016/j.scico.2020.102492

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We provide a construction that, given a big-step semantics describing finite computations and their observations, extends it to include infinite computations as well. The basic idea is that the finite behavior uniquely determines the infinite behavior once observations and their composition operators are fixed. Technically, the construction relies on the framework of inference systems with corules. The effectiveness and scope of the approach are illustrated by several examples. The correctness is formally justified by proving that, starting from a big-step semantics equivalent to a reference small-step semantics, this equivalence is preserved by the construction. (C) 2020 Elsevier B.V. All rights reserved.

引用

页数：28

共 38 条

[1] Normalization by Evaluation in the Delay Monad A Case Study for Coinduction via Copatterns and Sized Types [J].