A big step from finite to infinite computations

被引：2

作者：

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

Abel, Andreas ;

Chapman, James .

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (153) :51-67

[2]

Aczel P., 1977, HDB MATH LOGIC, P739

[3] Type Soundness Proofs with Definitional Interpreters [J].

Amin, Nada ;

Rompf, Tiark .

ACM SIGPLAN NOTICES, 2017, 52 (01) :666-679

[4]

Ancona D., 2017, PACMPL 1 OOPSLA, V1

[5]

Ancona D., 2014, FTFJP 14 FORMAL TECH

[6]

Ancona D., 2018, LIPICS, V109

[7] Extending Coinductive Logic Programming with Co-Facts [J].

Ancona, Davide ;

Dagnino, Francesco ;

Zucca, Elena .

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (258) :1-18

[8] Generalizing Inference Systems by Coaxioms [J].

Ancona, Davide ;

Dagnino, Francesco ;

Zucca, Elena .

PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 :29-55

[9] A Theoretical Perspective of Coinductive Logic Programming [J].

Ancona, Davide ;

Dovier, Agostino .

FUNDAMENTA INFORMATICAE, 2015, 140 (3-4) :221-246

[10]

[Anonymous], 1972, Proceedings of the ACM Annual Conference - Volume 2. ACM'72, DOI [DOI 10.1023/A:1010027404223, DOI 10.1145/800194.805852]

← 1 2 3 4 →