Ancona, Davide ;
Dagnino, Francesco ;
Rot, Jurriaan ;
Zucca, Elena
A Big Step from Finite to Infinite Computations (SCICO Journalfirst)
Abstract
The known is finite, the unknown infinite  Thomas Henry Huxley
The behaviour of programs can be described by the final results of computations, and/or their interactions with the context, also seen as observations. For instance, a function call can terminate and return a value, as well as have output effects during its execution.
Here, we deal with semantic definitions covering both results and observations. Often, such definitions are provided for finite computations only. Notably, in bigstep style, infinite computations are simply not modelled, hence diverging and stuck terms are not distinguished. This becomes even more unsatisfactory if we have observations, since a nonterminating program may have significant infinite behaviour.
Recently, examples of bigstep semantics modeling divergence have been provided [Davide Ancona et al., 2017; Davide Ancona et al., 2018] by means of generalized inference systems [Davide Ancona et al., 2017; Francesco Dagnino, 2019], which allow corules to control coinduction. Indeed, modeling infinite behaviour by a purely coinductive interpretation of bigstep rules would lead to spurious results [Xavier Leroy and Hervé Grall, 2009] and undetermined observation, whereas, by adding appropriate corules, we can correctly get divergence (∞) as the only result, and a uniquely determined observation. This approach has been adopted in [Davide Ancona et al., 2017; Davide Ancona et al., 2018] to design bigstep definitions including infinite behaviour for lambdacalculus and a simple imperative Javalike language. However, in such works the designer of the semantics is in charge of finding the appropriate corules, and this is a nontrivial task.
In this paper, we show a general construction that extends a given bigstep semantics, modeling finite computations, to include infinite behaviour as well, notably by generating appropriate corules. The construction consists of two steps:
1) Starting from a monoid O modeling finite observations (e.g., finite traces), we construct an ωmonoid ⟨O, O_∞⟩ also modeling infinite observations (e.g., infinite traces). The latter structure is a variation of the notion of ωsemigroup [Dominique Perrin and JeanEric Pin, 2004], including a mixed product composing a finite with a possibly infinite observation, and an infinite product mapping an infinite sequence of finite observations into a single one (possibly infinite).
2) Starting from an inference system defining a bigstep judgment c⇒⟨r, o⟩, with c denoting a configuration, r ∈ R a result, and o ∈ O a finite observation, we construct an inference system with corules defining an extended bigstep judgment c⇒c ⇒ ⟨r_∞, o_∞⟩ with r_∞ ∈ R_∞ = R+{∞}, and o_∞ ∈ O_∞ a "possibly infinite" observation. The construction generates additional rules for propagating divergence, and corules for introducing divergence in a controlled way.
The exact corules added in the construction depend on the type of observations that one starts with. To show the effectiveness of our approach, we provide several instances of the framework, with different kinds of (finite) observations.
Finally, we prove a correctness result for the construction. To this end, we assume the original bigstep semantics to be equivalent to (finite sequences of steps in) a reference smallstep semantics, and we show that, by applying the construction, we obtain an extended bigstep semantics which is still equivalent to the smallstep semantics, where we consider possibly infinite sequences of steps.} As hypotheses, rather than {just} equivalence in the finite case {(which would be not enough)}, we assume a set of equivalence conditions between individual bigstep rules and the smallstep relation. This proof of equivalence holds for deterministic semantics; issues arising in the nondeterministic case and a possible solution are sketched in the conclusion of the full paper.
BibTeX  Entry
@InProceedings{ancona_et_al:LIPIcs:2020:13189,
author = {Davide Ancona and Francesco Dagnino and Jurriaan Rot and Elena Zucca},
title = {{A Big Step from Finite to Infinite Computations (SCICO Journalfirst)}},
booktitle = {34th European Conference on ObjectOriented Programming (ECOOP 2020)},
pages = {32:132:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771542},
ISSN = {18688969},
year = {2020},
volume = {166},
editor = {Robert Hirschfeld and Tobias Pape},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13189},
URN = {urn:nbn:de:0030drops131895},
doi = {10.4230/LIPIcs.ECOOP.2020.32},
annote = {Keywords: Operational semantics, coinduction, infinite behaviour}
}
06.11.2020
Keywords: 

Operational semantics, coinduction, infinite behaviour 
Seminar: 

34th European Conference on ObjectOriented Programming (ECOOP 2020)

Issue date: 

2020 
Date of publication: 

06.11.2020 