DIBRIS, University of Genova,
Italydavide.ancona@unige.ithttp://orcid.org/0000-0002-6297-2011Member of GNCS
(Gruppo Nazionale per il Calcolo Scientifico), INdAM (Istituto Nazionale di
Alta Matematica "F. Severi") DIBRIS, University of Genova,
Italypietro.barbieri@edu.unige.ithttps://orcid.org/0000-0003-3193-5549 DIBRIS,
University of Genova,
Italyfrancesco.dagnino@dibris.unige.ithttps://orcid.org/0000-0003-3599-3535
DIBRIS, University of Genova,
Italyelena.zucca@unige.ithttp://orcid.org/0000-0002-6833-6470 Davide Ancona,
Pietro Barbieri, Francesco Dagnino, Elena Zucca <ccs2012> <concept>
<concept_id>10003752.10010124.10010131.10010134</concept_id>
<concept_desc>Theory of computation Operational semantics</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10011007.10011006.10011008.10011024.10011033</concept_id>
<concept_desc>Software and its engineering Recursion</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10011007.10011006.10011039.10011311</concept_id>
<concept_desc>Software and its engineering Semantics</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Operational semantics [500]Software and its
engineering Recursion [500]Software and its engineering SemanticsJohn Q. Open
and Joan R. Access 2 34th European Conference on Object-Oriented Programming
ECOOP 2020 ECOOP 2020 July 13–17, 2020 Berlin, Germany

# Sound regular corecursion in $\coFJ$

Davide Ancona  Pietro Barbieri  Francesco Dagnino  Elena Zucca

###### Abstract

The aim of the paper is to provide solid foundations for a programming
paradigm natively supporting the creation and manipulation of cyclic data
structures. To this end, we describe $\coFJ$, a Java-like calculus where
objects can be _infinite_ and methods are equipped with a _codefinition_ (an
alternative body). We provide an abstract semantics of the calculus based on
the framework of _inference systems with corules_. In $\coFJ$ with this
semantics, FJ recursive methods on finite objects can be extended to infinite
objects as well, and behave as desired by the programmer, by specifying a
codefinition. We also describe an operational semantics which can be directly
implemented in a programming language, and prove the soundness of such
semantics with respect to the abstract one.

###### keywords:

Operational semantics, coinduction, programming paradigms, regular terms

###### category:

## Introduction

Applications often deal with data structures which are conceptually infinite,
such as streams or infinite trees. Thus, a major problem for programming
languages is how to finitely represent something which is infinite, and, even
harder, how to correctly manipulate such finite representations to reflect the
expected behaviour on the infinite structure.

A well-established solution is _lazy evaluation_ , as, e.g., in Haskell. In
this approach, the conceptually infinite structure is represented as the
result of a function call, which is evaluated only as much as needed. Focusing
on the paradigmatic example of streams (infinite lists) of integers, we can
define two_one = 2:1:two_one, or even represent the list of natural numbers as
from 0, where from n = n:from(n+1). In this way, functions which only need to
inspect a finite portion of the structure, e.g., getting the $i$-th element,
can be correctly implemented. On the other hand, functions which need to
inspect the whole structure, e.g., min getting the minimal element, or allPos
checking that all elements are positive, have an undefined result (that is,
non-termination, operationally).

More recently, a different, in a sense complementary111As we will discuss
further in the Conclusion., approach has been considered [17, 8, 3], which
focuses on _cyclic_ structures (e.g., cyclic lists, trees and graphs). They
can be regarded as a particular case of infinite structures: abstractly, they
correspond to regular terms (or trees), that is, finitely branching trees
whose depth can be infinite, but contain only a finite set of subtrees. For
instance, the list two_one is regular, whereas the list of natural numbers is
not. Typically, cyclic data structures are handled by programming languages by
relying on imperative features or ad hoc data structures for bookkeeping. For
instance, we can build a cyclic object by assigning to a field of an object a
reference to the object itself, or we can visit a graph by marking already
encountered nodes. In this approach [17, 8, 3], instead, the programming
language natively supports regular structures, as outlined below:

  * •

Data constructors are enriched by allowing equations, e.g.,
$\textit{x}=2:1:\textit{x}$.

  * •

Functions are _regularly corecursive_ , that is, execution keeps track of
pending function calls, so that, when the same call is encountered the second
time, this is detected, avoiding non-termination as with ordinary recursion.
For instance, when calling min on the list $\textit{x}=2:1:\textit{x}$, after
an intermediate call on the list $y=1:2:y$, the same call is encountered.

Regular corecursion originates from _co-SLD resolution_ [20, 21, 7], where
already encountered goals (up to unification), called _coinductive hypotheses_
, are considered successful. However, co-SLD resolution is not flexible enough
to to correctly express certain predicates on regular terms; for instance, in
the min example, the intuitively correct corecursive definition is not sound,
because the predicate succeeds for all lower bounds of $l$, as shown in the
following.

When moving from goals to functions calls, the same problem manifests more
urgently because a result should always be provided for already encountered
calls. To solve this issue, the mechanism of _flexible regular corecursion_
can be adopted to allow the programmer to correctly specify the behaviour of
recursive functions on cyclic structures. For instance, for function min, the
programmer specifies that the head of the list should be returned when
detecting a cyclic call; in this way, on the list $\textit{x}=2:1:\textit{x}$,
the result of the cyclic call is $2$, so that the result of the original call
is $1$, as expected.

Flexible regular corecursion as outlined above has been proposed in the
object-oriented [8], functional [17], and logic [3] paradigms (see Section 7
for more details). However, none of these proposals provides formal arguments
for the correctness of the given operational semantics, by proving that it is
sound with respect to some model of the behaviour of functions (or predicates)
on infinite structures. The aim of this paper is to bridge this gap, by
providing solid foundations for a programming paradigm natively supporting
cyclic data structures. This is achieved thanks to the recently introduced
framework of _inference systems with corules_ [4, 13], allowing definitions
which are neither inductive, nor purely coinductive. We present the approach
in the context of Java-like languages, namely on an extension of Featherweight
Java (FJ) [15] called $\coFJ$, outlined as follows:

  * •

FJ objects are smoothly generalized from finite to infinite by interpreting
their definition coinductively, and methods are equipped with a _codefinition_
(an alternative body).

  * •

We provide an abstract big-step semantics for $\coFJ$ by an inference system
with corules. In $\coFJ$ with this semantics, FJ recursive methods on finite
objects can be extended to infinite objects as well, and behave as desired by
the programmer, by specifying a codefinition. For instance, if the
codefinitions for min and allPos are specified to return the head, and true,
respectively, then min returns $1$ on $\textit{x}=2:1:\textit{x}$, and $0$ on
the list of the natural numbers, whereas allPos returns true on both lists.

  * •

Then, we provide an operational (hence, executable) semantics where infinite
objects are restricted to regular ones and methods are regularly corecursive,
and we show that such operational semantics is sound with respect to the
abstract one.

At https://person.dibris.unige.it/zucca-elena/coFJ_implementation.zip we
provide a prototype implementation of $\coFJ$, briefly described in the
Conclusion. A preliminary version of the operational semantics, with no
soundness proof with respect to a formal model, has been given in [10].

Section 1 is a quick introduction to inference systems with corules. Section 2
describes FJ and informally introduces our approach. In Section 3 we define
$\coFJ$ and its abstract semantics, in Section 4 the operational semantics, in
Section 5 we show some advanced examples, and in Section 6 we prove soundness.
Finally, we discuss related work and draw conclusions in Section 7 and Section
8, respectively.

##  1 Inference systems with corules

First we recall standard notions on inference systems [1, 19]. Assuming a
_universe_ ${\cal U}$ of _judgments_ , an _inference system_ ${\cal I}$ is a
set of _(inference) rules_ , which are pairs
$\displaystyle\frac{\textit{Pr}}{\textit{c}}$, with $\textit{Pr}\subseteq{\cal
U}$ the set of _premises_ , and $\textit{c}\in{\cal U}$ the _consequence_
(a.k.a. _conclusion_). A rule with an empty set of premises is an _axiom_. A
_proof tree_ (a.k.a. _derivation_) for a judgment $\mathit{j}$ is a tree whose
nodes are (labeled with) judgments, $\mathit{j}$ is the root, and there is a
node $c$ with children Pr only if there is a rule
$\displaystyle\frac{\textit{Pr}}{\textit{c}}$.

The _inductive_ and the _coinductive interpretation_ of ${\cal I}$, denoted
$\textit{Ind}({\cal I})$ and $\textit{CoInd}({\cal I})$, are the sets of
judgments with, respectively, a finite222Under the common assumption that sets
of premises are finite, otherwise we should say well-founded., and a possibly
infinite proof tree. In set-theoretic terms, let ${\textit{F}_{{\cal
I}}}:\wp({\cal U})\rightarrow\wp({\cal U})$ be defined by ${\textit{F}_{{\cal
I}}}(S)=\\{\textit{c}\mid\textit{Pr}\subseteq
S,\displaystyle\frac{\textit{Pr}}{\textit{c}}\in{\cal I}\\}$, and say that a
set $S$ is _closed_ if ${\textit{F}_{{\cal I}}}(S)\subseteq S$, _consistent_
if $S\subseteq{\textit{F}_{{\cal I}}}(S)$. Then, it can be proved that
$\textit{Ind}({\cal I})$ is the smallest closed set, and $\textit{CoInd}({\cal
I})$ is the largest consistent set. We write ${\cal
I}\\!\vdash\\!{\mathit{j}}$ when $\mathit{j}$ has a finite derivation in
${\cal I}$, that is, $\mathit{j}\in\textit{Ind}({\cal I})$.

An _inference system with corules_ , or _generalized inference system_ , is a
pair $({{{\cal I}},{{\cal I}^{co}}})$ where ${\cal I}$ and ${\cal I}^{co}$ are
inference systems, whose elements are called _rules_ and _corules_ ,
respectively. Corules can only be used in a special way, as defined below.

For a subset $S$ of the universe, let ${{\cal I}_{{\sqcap}S}}$ denote the
inference system obtained from ${\cal I}$ by keeping only rules with
consequence in $S$. Let $({{{\cal I}},{{\cal I}^{co}}})$ be a generalized
inference system. Then, its _interpretation_ $\textit{Gen}({\cal I},{\cal
I}^{co})$ is defined by $\textit{Gen}({\cal I},{\cal
I}^{co})=\textit{CoInd}({{\cal I}_{{\sqcap}\textit{Ind}({\cal I}\cup{\cal
I}^{co})}})$.

In proof-theoretic terms, $\textit{Gen}({\cal I},{\cal I}^{co})$ is the set of
judgments that have a possibly infinite proof tree in ${\cal I}$, where all
nodes have a finite proof tree in ${\cal I}\cup{\cal I}^{co}$, that is, the
(standard) inference system consisting of rules and corules. We write
$({{{\cal I}},{{\cal I}^{co}}})\\!\vdash\\!{\mathit{j}}$ when $\mathit{j}$ is
derivable in $({{{\cal I}},{{\cal I}^{co}}})$, that is,
$\mathit{j}\in\textit{Gen}({\cal I},{\cal I}^{co})$. Note that $({{{\cal
I}},{\emptyset}})\\!\vdash\\!{\mathit{j}}$ is the same as ${\cal
I}\\!\vdash\\!{\mathit{j}}$.

We illustrate these notions by a simple example. As usual, sets of rules are
expressed by _meta-rules_ with side conditions, and analogously sets of
corules are expressed by _meta-corules_ with side conditions. (Meta-)corules
will be written with thicker lines, to be distinguished from (meta-)rules. The
following inference system defines the minimum element of a list, where
$[\textit{x}]$ is the list consisting of only x, and $\textit{x}:u$ the list
with head x and tail $u$.

$\displaystyle\frac{}{\textit{min}({[\textit{x}]},\textit{x})}\hskip
15.00002pt\displaystyle\frac{\textit{min}(u,y)}{\textit{min}(x{:}u,z)}z=\min(x,y)$

The inductive interpretation gives the correct result only on finite lists,
since for infinite lists an infinite proof is clearly needed. However, the
coinductive one fails to be a function. For instance, for $L$ the infinite
list $2:1:2:1:2:1:\ldots$, any judgment $\textit{min}(L,x)$ with $x\leq 1$ can
be derived, as shown below.

$\displaystyle\frac{\displaystyle\frac{\displaystyle\frac{\ldots}{\textit{min}(L,1)}}{\textit{min}(1{:}L,1)}}{\textit{min}(2{:}1{:}L,1)}\hskip
15.00002pt\displaystyle\frac{\displaystyle\frac{\displaystyle\frac{\ldots}{\textit{min}(L,0)}}{\textit{min}(1{:}L,0)}}{\textit{min}(2{:}1{:}L,0)}$

By adding a corule (in this case a coaxiom), wrong results are “filtered out”:

$\displaystyle\frac{}{\textit{min}(x{:}\epsilon,x)}\hskip
15.00002pt\displaystyle\frac{\textit{min}(u,y)}{\textit{min}(x{:}u,z)}z=\min(x,y)\hskip
15.00002pt\genfrac{}{}{1.7pt}{0}{}{\textit{min}(x{:}u,x)}$

Indeed, the judgment $\textit{min}(2{:}1{:}L,1)$ has the infinite proof tree
shown above, and each node has a finite proof tree in the inference system
extended by the corule:

$\displaystyle\frac{\displaystyle\frac{\displaystyle\frac{\ldots}{\textit{min}(L,1)}}{\textit{min}(1{:}L,1)}}{\textit{min}(2{:}1{:}L,1)}\hskip
15.00002pt\displaystyle\frac{\genfrac{}{}{1.7pt}{0}{}{\textit{min}(1{:}L,1)}}{\textit{min}(2{:}1{:}L,1)}$

The judgment $\textit{min}(2{:}1{:}L,0)$, instead, has the infinite proof tree
shown above, but has _no finite proof tree_ in the inference system extended
by the corule. Indeed, since $0$ does not belong to the list, the corule can
never be applied. On the other hand, the judgment $\textit{min}(L,2)$ has a
finite proof tree with the corule, but cannot be derived since they it has no
infinite proof tree. We refer to [4, 5, 6, 13] for other examples.

As final remark, note that requiring the existence of a finite proof tree with
corules only for the root is not enough. For regular proof trees, the
requirement to have such a proof tree for each node can be simplified in two
ways:

  * •

either requiring a sufficiently large finite proof-with-corules for the root,
that is, a finite proof tree for the root which includes all the nodes of the
regular proof tree

  * •

or requiring a finite proof-with-corules for one node taken from each infinite
path.

Let $({{{\cal I}},{{\cal I}^{co}}})$ be a generalized inference system. The
_bounded coinduction principle_ [4], a generalization of the standard
coinduction principle, can be used to prove _completeness_ of $({{{\cal
I}},{{\cal I}^{co}}})$ w.r.t. a set S (for “specification”) of _valid_
judgments.

######  Theorem 1.1 (Bounded coinduction).

If the following two conditions hold:

  1. 1.

$\textit{S}\subseteq\textit{Ind}({\cal I}\cup{\cal I}^{co})$, that is, each
valid judgment has a finite proof tree in ${\cal I}\cup{\cal I}^{co}$;

  2. 2.

$\textit{S}\\!\subseteq\\!{\textit{F}_{{\cal I}}}(\textit{S})$, that is, each
valid judgment is the consequence of a rule in ${\cal I}$ with premises in S

then $\textit{S}\subseteq\textit{Gen}({\cal I},{\cal I}^{co})$.

##  2 From FJ to $\coFJ$

We recall FJ, and informally explain its extension with infinite objects and
codefinitions.

Featherweight Java The standard syntax and semantics in big-step style of FJ
are shown in Figure 1. We omit cast since this feature does not add
significant issues. We adopt a big-step, rather than a small-step style as in
the original FJ definition, since in this way the semantics is directly
defined by an inference system, denoted ${\cal I}_{\textsc{FJ}}$ in the
following, which will be equipped with corules to support infinite objects. We
write $\overline{\textit{cd}}$ as metavariable for
$\textit{cd}_{1}\ldots\textit{cd}_{n}$, $n\geq 0$, and analogously for other
sequences. We sometimes use the wildcard $\\_$ when the corresponding
metavariable is not relevant.

A sequence of class declarations $\overline{\textit{cd}}$ is called a _class
table_. Each class has a canonical constructor whose parameters match the
fields of the class, the inherited ones first. We assume standard FJ
constraints, e.g., no field hiding and no method overloading. The only
variables occurring in method bodies are parameters (including
$\texttt{this})$. Values are _objects_ , that is, constructor invocations
where arguments are values in turn.

The judgment $\textit{e}\\!\Downarrow\\!\textit{v}$ is implicitly
parameterized on a fixed class table. In the rules we use standard FJ
auxiliary functions, omitting their formal definition. Notably,
$\mathit{fields}(\mathit{C})$ returns the sequence
$\mathit{f}_{1}\ldots\mathit{f}_{n}$ of the field names333We omit types since
not relevant here. We discuss about type systems for $\coFJ$ in the
conclusion. of the class, in declaration order with the inherited first, and
$\mathit{mbody}(\mathit{C},\textit{m})$, for method m of the class, the pair
of the sequence of parameters and the definition. Substitution
$\textit{e}[\overline{\textit{e}}/\overline{\textit{x}}]$, for
$\overline{\textit{e}}$ and $\overline{\textit{x}}$ of the same length, is
defined in the customary manner. Finally, for
$\overline{\textit{e}}=\textit{e}_{1}\ldots\textit{e}_{n}$ and
$\overline{\textit{v}}=\textit{v}_{1}\ldots\textit{v}_{n}$,
$\overline{\textit{e}}\\!\Downarrow\\!\overline{\textit{v}}$ is an
abbreviation for
$\textit{e}_{1}\\!\Downarrow\\!\textit{v}_{1}\ldots\textit{e}_{n}\\!\Downarrow\\!\textit{v}_{n}$.

$\begin{array}[t]{llll}\\\ \textit{cd}&{:}{:}=&\texttt{class}\ \mathit{C}\
\texttt{extends}\ \mathit{C}^{\prime}\ \\{\ \overline{\mathit{fd}}\
\overline{{\textit{md}}}\ \\}&\mbox{{\small{class declaration}}}\\\
\mathit{fd}&{:}{:}=&\mathit{C}\,\mathit{f}\texttt{;}&\mbox{{\small{field
declaration}}}\\\ {\textit{md}}&{:}{:}=&\mathit{C}\
\textit{m}({\mathit{C}_{1}\,\textit{x}_{1},\ldots,\mathit{C}_{n}\,\textit{x}_{n}})\
\\{\textit{e}\\}&\mbox{{\small{method declaration}}}\\\ \textit{e}\in{\cal
E}&{:}{:}=&\textit{x}\mid\textit{e}.\mathit{f}\mid\texttt{new}\
\mathit{C}(\overline{\textit{e}})\mid\textit{e}.\textit{m}(\overline{\textit{e}})&\mbox{{\small{expression}}}\\\
\\\ \textit{v}\in{\cal V}&{:}{:}=&\texttt{new}\
\mathit{C}(\overline{\textit{v}})&\mbox{{\small{{(finite)}
object}}}\end{array}$

$\begin{array}[]{l}\\\
{\tiny\textsc{({$\textsc{FJ}$-field})}}\displaystyle\frac{\textit{e}\\!\Downarrow\\!\textit{v}}{\textit{e}.\mathit{f}\\!\Downarrow\\!\textit{v}_{i}}\
\begin{array}[]{l}\begin{array}[]{l}\textit{v}=\texttt{new}\
\mathit{C}({\textit{v}_{1},\ldots,\textit{v}_{n}})\\\
\mathit{fields}(\mathit{C})={\mathit{f}_{1}\ldots\mathit{f}_{n}}\\\
\mathit{f}=\mathit{f}_{i},i\in 1..n\end{array}\end{array}\hskip
15.00002pt{\tiny\textsc{({$\textsc{FJ}$-new})}}\displaystyle\frac{\overline{\textit{e}}\\!\Downarrow\\!\overline{\textit{v}}}{\texttt{new}\
\mathit{C}(\overline{\textit{e}})\\!\Downarrow\\!\texttt{new}\
\mathit{C}(\overline{\textit{v}})}\
\begin{array}[]{l}\end{array}\\\\[25.83325pt]
{\tiny\textsc{({$\textsc{FJ}$-invk})}}\displaystyle\frac{\textit{e}_{0}\\!\Downarrow\\!\textit{v}_{0}\hskip
8.00003pt\overline{\textit{e}}\\!\Downarrow\\!\overline{\textit{v}}\hskip
8.00003pt\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}]\\!\Downarrow\\!\textit{v}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}})\\!\Downarrow\\!\textit{v}}\
\begin{array}[]{l}\begin{array}[]{l}\textit{v}_{0}=\texttt{new}\
\mathit{C}(\\_)\\\
\mathit{mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}}})\end{array}\end{array}\\\\[8.61108pt]
\end{array}$

Figure 1: FJ syntax and big-step rules

Rule (FJ-field) models field access. If the selected field is actually a field
of the receiver’s class, then the corresponding value is returned as result.
Rule (FJ-new) models object creation: if the argument expressions
$\overline{\textit{e}}$ evaluate to values $\overline{\textit{v}}$, then the
result is an object of class C. Rule (FJ-invk) models method invocation. The
receiver and argument expressions are evaluated first. Then, method look-up is
performed, starting from the receiver’s class, by the auxiliary function
$\mathit{mbody}$. Lastly, the definition e of the method, where this is
replaced by the receiver, and the parameters by the arguments, is evaluated,
and its result is returned.

Infinite objects and codefinitions We take as running example the following FJ
implementation of lists of integers, equipped with some typical methods:
isEmpty tests the emptiness, incr returns the list where all elements have
been incremented by one, allPos checks whether all elements are positive,
member checks whether the argument is in the list, and min returns the minimal
element.

⬇

class List extends Object {

bool isEmpty() {true}

List incr() {new EmptyList()}

bool allPos() {true}

bool member(int x) {false}

}

class EmptyList extends List { }

class NonEmptyList extends List {

int head; List tail;

bool isEmpty() {false}

List incr() {new NonEmptyList(this.head+1,this.tail.incr())}

bool allPos() {if (this.head<=0) false else this.tail.allPos()}

bool member(int x) {if (this.head==x) true else this.tail.member(x)}

int min() {

if (this.tail.isEmpty()) this.head

else Math.min(this.tail.min(),this.head)

}

}

We used some additional standard constructs, such as conditional and primitive
types bool and int with their operations; to avoid to use abstract methods,
List provides the default implementation on empty lists, overridden in
NonEmptyList, except for method min which is only defined on non empty lists.

In FJ we can represent finite lists. For instance, the object

⬇

new NonEmptyList(2, new NonEmptyList(1, new EmptyList()))

which we will abbreviate $[2,1]$, represents a list of two elements, and it is
easy to see that all the above method definitions provide the expected meaning
on finite lists.

On the other hand, since the syntactic definition for objects is interpreted,
like the others, inductively, in FJ objects are _finite_ , hence we cannot
represent, e.g., the infinite list of natural numbers $[0,1,2,3,\ldots]$,
abbreviated $[0..]$, or the infinite list $[2,1,2,1,2,1,\ldots]$, abbreviated
$[2,1]^{\omega}$. To move from finite to infinite objects, it is enough to
interpret the syntactic definition for values _coinductively_ , so to obtain
infinite terms as well. However, to make the extension significant, we should
be able to _generate_ such infinite objects as results of expressions, and to
appropriately _handle_ them by methods.

To generate infinite objects, e.g., the infinite lists mentioned above, a
natural approach is to consider method definitions as _corecursive_ , that is,
to take the _coinductive_ interpretation of the inference system in Figure 1.
Consider the following class:

⬇

class ListFactory extends Object {

NonEmptyList from(int x) {new NonEmptyList(x, this.from(x+1)}

NonEmptyList two_one() {new NonEmptyList(2, this.one_two())}

NonEmptyList one_two() {new NonEmptyList(1, this.two_one())}

}

With the standard FJ semantics, given by the inductive interpretation of the
inference system in Figure 1, the method invocation new ListFactory().from(0)
(abbreviated $\texttt{from}_{0}$ in the following) has no result, since there
is no finite proof tree for a judgment of shape
$\texttt{from}_{0}\\!\Downarrow\\!\\_$. Taking the coinductive interpretation,
instead, such call returns as result the infinite list of natural numbers
$[0..]$, since there is an infinite proof tree for the judgment
$\texttt{from}_{0}\\!\Downarrow\\![0..]$. Analogously, the method invocation
new ListFactory().two_one() returns $[2,1]^{\omega}$. Moreover, the method
invocations $[0..].\texttt{incr}()$ and $[2,1]^{\omega}.\texttt{incr}($)
correctly return as result the infinite lists $[1..]$ and $[3,2]^{\omega}$,
respectively.

However, in many cases to consider method definitions as corecursive is not
satisfactory, since it leads to non-determinism, as shown for inference
systems in Section 1. For instance, for the method invocation
$[0..].\texttt{allPos}()$ both judgments
$[0..].\texttt{allPos}()\\!\Downarrow\\!\texttt{true}$ and
$[0..].\texttt{allPos}()\\!\Downarrow\\!\texttt{false}$ are derivable, and
analogously for $[2,1]^{\omega}.\texttt{allPos}()$. In general, both results
can be obtained for any infinite list of all positive numbers. A similar
behavior is exhibited by method member: given an infinite list $L$ which does
not contain x, both judgments
$L.\texttt{member}(\textit{x})\\!\Downarrow\\!\texttt{true}$ and
$L.\texttt{member}(\textit{x})\\!\Downarrow\\!\texttt{false}$ are derivable.
Finally, for the method invocation $[2,1]^{\omega}.\texttt{min}()$, any
judgment $[2,1]^{\omega}.\texttt{min}()\\!\Downarrow\\!\textit{x}$ with
$\textit{x}\leq 1$ can be derived.

To solve this problem, $\coFJ$ allows the programmer to _control_ the
semantics of corecursive methods by adding a _codefinition_ 444The term
“codefinition” is meant to suggest “alternative definition used to handle
corecursion”., that is, an alternative method body playing a special role.
Depending on the codefinition, the purely coinductive interpretation is
refined, by filtering out some judgments. In the example, to achieve the
expected meaning, the programmer should provide the following codefinitions.

⬇

class ListFactory extends Object {

NonEmptyList from(int x) {

new NonEmptyList(x, this.from(x+1)} corec {any}

NonEmptyList one_two() {

new NonEmptyList(1, this.two_one())} corec {any}

NonEmptyList two_one() {

new NonEmptyList(2, this.one_two())} corec {any}

}

class NonEmptyList extends List {

int head; List tail;

bool isEmpty() {false}

List incr() {

new NonEmptyList(this.head+1,this.tail.incr())} corec {any}

bool allPos() {

if (this.head <= 0) false else this.tail.allPos()} corec {true}

bool member(int x) {

if (this.head == x) true else this.tail.member(x)} corec {false}

int min() {

if (this.tail.isEmpty()) this.head

else Math.min(this.tail.min(),this.head)

} corec {this.head}

}

For the three methods of ListFactory and for the method incr the codefinition
is any. This corresponds to keeping the coinductive interpretation as it is,
as is appropriate in these cases since it provides only the expected result.
In the other three methods, instead, the effect of the codefinition is to
filter the results obtained by the coinductive interpretation. The way this is
achieved is explained in the following section. Finally, for method isEmpty no
codefinition is added, since the inductive behaviour works on infinite lists
as well.

##  3 $\coFJ$ and its abstract semantics

We formally define $\coFJ$, illustrate how the previous examples get the
expected semantics, and show that, despite its non-determinism, $\coFJ$ is a
conservative extension of FJ.

Formal definition of $\coFJ$ The $\coFJ$ syntax is given in Figure 2.

$\begin{array}[t]{llll}\textit{cd}&{:}{:}=&\texttt{class}\ \mathit{C}\
\texttt{extends}\ \mathit{C}^{\prime}\ \\{\ \overline{\mathit{fd}}\
\overline{{\textit{md}}}\ \\}&\mbox{{\small{class declaration}}}\\\
\mathit{fd}&{:}{:}=&\mathit{C}\,\mathit{f}\texttt{;}&\mbox{{\small{field
declaration}}}\\\ {\textit{md}}&{:}{:}=&\mathit{C}\
\textit{m}({\mathit{C}_{1}\,\textit{x}_{1},\ldots,\mathit{C}_{n}\,\textit{x}_{n}})\
\\{\textit{e}\\}\ [\texttt{corec}\
\\{\textit{e}^{\prime}\\}]&\mbox{{\small{method declaration with
codefinition}}}\\\ \textit{e}\in{\cal
E}&{:}{:}=&\textit{x}\mid\textit{e}.\mathit{f}\mid{\texttt{new}\
\mathit{C}(\overline{\textit{e}})\mid\textit{e}.\textit{m}(\overline{\textit{e}})}&\mbox{{\small{expression}}}\\\\[7.74997pt]
\textit{v}\in{\cal V}\textsuperscript{a}&{:}{:}=_{\textsc{co}}&\texttt{new}\
\mathit{C}(\overline{\textit{v}})&\mbox{{\small{{possibly infinite
object}}}}\\\ \textit{e}\in{\cal
E}\textsuperscript{a}&{:}{:}=&\textit{x}\mid\textit{e}.\mathit{f}\mid{\texttt{new}\
\mathit{C}(\overline{\textit{e}})\mid\textit{e}.\textit{m}(\overline{\textit{e}})}\mid\textit{v}&\mbox{{\small{{runtime
expression}}}}\end{array}$

$\begin{array}[]{l}\\\ {\tiny\textsc{({abs-
field})}}\displaystyle\frac{\textit{e}\\!\Downarrow\\!\textit{v}}{\textit{e}.\mathit{f}\\!\Downarrow\\!\textit{v}_{i}}\
\begin{array}[]{l}\begin{array}[]{l}\textit{v}=\texttt{new}\
\mathit{C}({\textit{v}_{1},\ldots,\textit{v}_{n}})\\\
\mathit{fields}(\mathit{C})={\mathit{f}_{1}...\mathit{f}_{n}}\\\
\mathit{f}=\mathit{f}_{i},i\in 1..n\end{array}\end{array}\hskip
13.50002pt{\tiny\textsc{({abs-
new})}}\displaystyle\frac{\overline{\textit{e}}\\!\Downarrow\\!\overline{\textit{v}}}{\texttt{new}\
\mathit{C}(\overline{\textit{e}})\\!\Downarrow\\!\texttt{new}\
\mathit{C}(\overline{\textit{v}})}\
\begin{array}[]{l}\end{array}\\\\[23.24991pt] {\tiny\textsc{({abs-
invk})}}\displaystyle\frac{\textit{e}_{0}\\!\Downarrow\\!\textit{v}_{0}\hskip
7.20003pt\overline{\textit{e}}\\!\Downarrow\\!\overline{\textit{v}}\hskip
7.20003pt\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}]\\!\Downarrow\\!\textit{v}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}})\\!\Downarrow\\!\textit{v}}\
\begin{array}[]{l}\textit{v}_{0}=\texttt{new}\ \mathit{C}(\\_)\\\
{\mathit{mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}}})}\end{array}\hskip
13.50002pt{\tiny\textsc{({{abs-co-
val}})}}\displaystyle\genfrac{}{}{1.5pt}{}{}{\textit{v}\\!\Downarrow\\!\textit{v}}\
\begin{array}[]{l}\end{array}\\\\[23.24991pt] {\tiny\textsc{({abs-co-
invk})}}\displaystyle\genfrac{}{}{1.5pt}{}{\textit{e}_{0}\\!\Downarrow\\!\textit{v}_{0}\hskip
7.20003pt\overline{\textit{e}}\\!\Downarrow\\!\overline{\textit{v}}\hskip
7.20003pt\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}][\textit{v}/\texttt{any}]\\!\Downarrow\\!\textit{v}_{\textit{co}}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}})\\!\Downarrow\\!\textit{v}_{\textit{co}}}\
\begin{array}[]{l}\textit{v}_{0}=\texttt{new}\ \mathit{C}(\\_)\\\ {\textit{co-
mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}^{\prime}}})}\end{array}\end{array}$

Figure 2: $\coFJ$ syntax and abstract semantics

As the reader can note, the only difference is that method declarations
include now, besides a definition e, an optional _codefinition_
$\textit{e}^{\prime}$, as denoted by the square brackets in the production.
Furthermore, besides this, there is another special variable any, which can
only occur in codefinitions. The codefinition will be used to provide an
abstract semantics through an inference system with corules, where the role of
any is to be a placeholder for an arbitrary value. For simplicity, we require
the codefinition $\textit{e}^{\prime}$ to be statically restricted to avoid
recursive (even indirect) calls to the same method (we omit the standard
formalization). Note that FJ is a (proper) subset of $\coFJ$: indeed, an FJ
class table is a $\coFJ$ class table with no codefinitions.

The syntactic definition for values is the same as before, but is now
interpreted _coinductively_ , as indicated by the symbol $::=_{\textsc{co}}$.
In this way, infinite objects are supported. By replacing method parameters by
arguments, we obtain _runtime expressions_ admitting infinite objects as
subterms. The sets ${\cal V}$ and ${\cal E}$ of FJ objects and expressions are
subsets of ${\cal V}\textsuperscript{a}$ and ${\cal E}\textsuperscript{a}$,
respectively. The judgment $\textit{e}\\!\Downarrow\\!\textit{v}$, with
$\textit{e}\in{\cal E}\textsuperscript{a}$ and $\textit{v}\in{\cal
V}\textsuperscript{a}$, is defined by an inference system with corules
$({{{\cal I}_{\scriptscriptstyle\textsc{FJ}}},{{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}}})$ where the rules ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}$ are those555To be precise, meta-rules are
the same, with meta-variables e and v ranging on ${\cal
E}\textsuperscript{a}$, and ${\cal V}\textsuperscript{a}$, respectively.
However, we could have taken this larger universe in FJ as well without
affecting the defined relation. of FJ, as in Figure 1, and the corules ${\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}$ are instances of two metacorules.

Corule (abs-co-val) is needed to obtain a value for infinite objects, as shown
below. Corule (abs-co-invk) is analogous to the standard rule for method
invocation, but uses the codefinition, and the variable any can be non-
deterministically substituted with an arbitrary value. The auxiliary function
co-mbody is defined analogously to mbody, but it returns the codefinition.
Note that, even when $\mathit{mbody}(\mathit{C},\textit{m})$ is defined,
$\textit{co-mbody}(\mathit{C},\textit{m})$ can be undefined since no
codefinition has been specified. This can be done to force a purely inductive
behaviour for the method.

Examples As an example, we illustrate in Figure 3 the role of the two corules
for the call new ListFactory().from(0). For brevity, we write abbreviated
class names. Furthermore, $\texttt{from}_{n}$ stands for the call new
ListFactory().from(n) and $[n..]$ for the infinite object new
NonEmptyList(n,new NonEmptyList(n+1,...))).

${T_{n}{=}}{\tiny\textsc{({abs-invk})}}\displaystyle\frac{{\tiny\textsc{({abs-
new})}}\displaystyle\frac{}{\texttt{new LF()}\\!\Downarrow\\!\texttt{new
LF()}}\quad{\tiny\textsc{({n-val})}}\displaystyle\frac{}{n\\!\Downarrow\\!n}\quad{\tiny\textsc{({abs-
new})}}\displaystyle\frac{{\tiny\textsc{({n-val})}}\displaystyle\frac{}{n\\!\Downarrow\\!n}\qquad\genfrac{}{}{0.0pt}{0}{}{T_{n}}}{\texttt{new
NEL($n$,}\texttt{new
LF().from($n$+1)})\\!\Downarrow\\![n..]}}{\texttt{from}_{n}\\!\Downarrow\\![n..]}\\\
T_{{n+1}}{=}{\tiny\textsc{({abs-
invk})}}\displaystyle\frac{{\tiny\textsc{({abs-
new})}}\displaystyle\frac{}{\texttt{new LF()}\\!\Downarrow\\!\texttt{new
LF()}}\quad{\tiny\textsc{({+})}}\displaystyle\frac{\cdots}{\texttt{$n$+1}\\!\Downarrow\\!n{+}1}\quad{{\tiny\textsc{({abs-
new})}}\displaystyle\frac{{\tiny\textsc{({n-val})}}\displaystyle\frac{}{n{+}1\\!\Downarrow\\!n{+}1}\quad\genfrac{}{}{0.0pt}{0}{}{T_{{n+2}}}}{\scriptsize\texttt{new
NEL($n{+}1$,}\texttt{new
LF().from($n{+}1$+1)})\\!\Downarrow\\![n{+1}..]}}}{\texttt{new
LF().from($n$+1)}\\!\Downarrow\\![n{+}1..]}\\\ {\tiny\textsc{({abs-co-
invk})}}\displaystyle\genfrac{}{}{1.5pt}{}{{\tiny\textsc{({abs-
new})}}\displaystyle\frac{}{\texttt{new LF()}\\!\Downarrow\\!\texttt{new
LF()}}\ \begin{array}[]{l}\end{array}\hskip
6.40002pt{{\tiny\textsc{({n-val})}}\displaystyle\frac{}{n\\!\Downarrow\\!n}\
\begin{array}[]{l}\end{array}}\hskip 6.40002pt{\tiny\textsc{({abs-co-
val})}}\displaystyle\genfrac{}{}{1.5pt}{}{}{[n..]\equiv\texttt{any}[{\texttt{new
LF()}}/\texttt{this}][[n..]/\texttt{any}]\\!\Downarrow\\![n..]}\
\begin{array}[]{l}\end{array}}{\texttt{from}_{n}\\!\Downarrow\\![n..]}\
\begin{array}[]{l}\end{array}$

Figure 3: Infinite (top) and finite (bottom) proof trees for
$\texttt{from}_{n}\\!\Downarrow\\![n..]$

In the top part of Figure 3, we show the infinite proof tree $T_{n}$ which can
be constructed, for any natural number $n$, for the judgment
$\texttt{from}_{n}\\!\Downarrow\\![n..]$ without the use of corules. We use
standard rules (n-val) and (+) to deal with integer constants and addition.

To derive the judgment in the inference system with corules, each node in this
infinite tree should have a finite proof tree with the corules. Notably, this
should hold for nodes of shape $\texttt{from}_{n}\\!\Downarrow\\![n..]$, and
indeed the finite proof tree for such nodes is shown in the bottom part of the
figure. Note that, in this example, the result for the call
$\texttt{from}_{n}$ is uniquely determined by the rules, hence the role of the
corules is just to “validate” this result. To this end, the codefinition of
the method from is the special variable any, which, when evaluating the
codefinition, can be replaced by any value, hence, in particular, by the
correct result $[n..]$. Corule (abs-co-val) is needed to obtain a finite proof
tree for the infinite objects of shape $[n..]$. Analogous infinite and finite
proof trees can be constructed for the judgments $\texttt{new
ListFactory().two\\_one()}\\!\Downarrow\\![2,1]^{\omega}$,
$[0..].\texttt{incr}()\\!\Downarrow\\![1..]$ and
$[2,1]^{\omega}.\texttt{incr}(\\!)\Downarrow\\![3,2]^{\omega}$.

For the method call $[0..].\texttt{allPos}()$, instead, both judgments
$[0..].\texttt{allPos}()\\!\Downarrow\\!\texttt{true}$ and
$[0..].\texttt{allPos}()\\!\Downarrow\\!\texttt{false}$ have an infinite proof
tree. However, no finite proof tree using the codefinition can be constructed
for the latter, whereas this is trivially possible for the former.
Analogously, given an infinite list $L$ which does not contain x, only the
judgment $L.\texttt{member}(\textit{x})\\!\Downarrow\\!\texttt{false}$ has a
finite proof tree using the codefinition.

Finally, for the method invocation $[2,1]^{\omega}.\texttt{min}()$, for any
$\textit{v}\leq 1$ there is an infinite proof tree built without corules for
the judgment $\mathtt{[2,1]^{\omega}.min()}\\!\Downarrow\\!\textit{v}$ as
shown in Figure 4.

${\tiny\textsc{({abs-invk})}}\displaystyle\frac{T_{0}\qquad
T_{1}}{\mathtt{[2,1]^{\omega}.min()}\\!\Downarrow\\!\textit{v}}$
$T_{0}{=}{\tiny\textsc{({abs-
new})}}\displaystyle\frac{{\tiny\textsc{({n-val})}}\displaystyle\frac{}{\mathtt{2}\\!\Downarrow\\!\mathtt{2}}\qquad{\tiny\textsc{({abs-
new})}}\displaystyle\frac{{\tiny\textsc{({n-val})}}\displaystyle\frac{}{\mathtt{1}\\!\Downarrow\\!\mathtt{1}}\qquad\genfrac{}{}{0.0pt}{0}{}{T_{0}}}{\mathtt{[1,2]^{\omega}}\\!\Downarrow\\!\mathtt{[1,2]^{\omega}}}}{\mathtt{[2,1]^{\omega}}\\!\Downarrow\\!\mathtt{[2,1]^{\omega}}}$
$T_{1}{=}{\tiny\textsc{({{if-f}})}}\displaystyle\frac{\displaystyle\frac{\vdots}{\mathtt{[2,1]^{\omega}.tail.isEmpty()}\\!\Downarrow\\!\mathtt{false}}\quad\displaystyle\frac{\displaystyle\frac{\genfrac{}{}{0.0pt}{0}{T_{2}}{\vdots}}{\mathtt{[2,1]^{\omega}.tail.min()}\\!\Downarrow\\!\textit{v}}\quad\displaystyle\frac{\vdots}{\mathtt{[2,1]^{\omega}.head}\\!\Downarrow\\!\mathtt{2}}}{\mathtt{Math.min([2,1]^{\omega}.tail.min(),[2,1]^{\omega}.head)}\\!\Downarrow\\!\textit{v}}}{\mathtt{\mathbf{if}\
[2,1]^{\omega}.tail.isEmpty()\ \mathbf{then}\ [2,1]^{\omega}.head\
\mathbf{else}\
Math.min([2,1]^{\omega}.tail.min(),[2,1]^{\omega}.head)}\\!\Downarrow\\!\textit{v}}$
$T_{2}{=}{\tiny\textsc{({{if-f}})}}\displaystyle\frac{\displaystyle\frac{\vdots}{\mathtt{[1,2]^{\omega}.tail.isEmpty()}\\!\Downarrow\\!\mathtt{false}}\quad\displaystyle\frac{\displaystyle\frac{\genfrac{}{}{0.0pt}{0}{T_{1}}{\vdots}}{\mathtt{[1,2]^{\omega}.tail.min()}\\!\Downarrow\\!\textit{v}}\quad\displaystyle\frac{\vdots}{\mathtt{[1,2]^{\omega}.head}\\!\Downarrow\\!\mathtt{1}}}{\mathtt{Math.min([1,2]^{\omega}.tail.min(),[1,2]^{\omega}.head)}\\!\Downarrow\\!\textit{v}}}{\mathtt{\mathbf{if}\
[1,2]^{\omega}.tail.isEmpty()\ \mathbf{then}\ [1,2]^{\omega}.head\
\mathbf{else}\
Math.min([1,2]^{\omega}.tail.min(),[1,2]^{\omega}.head)}\\!\Downarrow\\!\textit{v}}$

Figure 4: Infinite proof tree for
$\mathtt{[2,1]^{\omega}.min()}\\!\Downarrow\\!\textit{v}$ with $\textit{v}\leq
1$ (main tree at the top left corner)

However, only the judgment $[2,1]^{\omega}.\texttt{min}()\\!\Downarrow\\!1$
has a finite proof tree using the codefinition (Figure 5). For space reasons
in both figures ellipses are used to omit the less interesting parts of the
proof trees; we use the standard rule (if-f) for conditional, and the
predefined function Math.min on integers.

${\tiny\textsc{({abs-
invk})}}\displaystyle\frac{\genfrac{}{}{0.0pt}{0}{}{T_{0}}\
{\tiny\textsc{({{if-f}})}}\displaystyle\frac{\displaystyle\frac{\vdots}{\mathtt{[2,1]^{\omega}.tail.isEmpty()}\\!\Downarrow\\!\mathtt{false}}{}\quad\displaystyle\frac{{\tiny\textsc{({abs-
co-
invk})}}\displaystyle\genfrac{}{}{1.5pt}{}{\cdots\quad\displaystyle\frac{{\tiny\textsc{({abs-
co-
val})}}\displaystyle\genfrac{}{}{1.5pt}{}{}{\mathtt{[1,2]^{\omega}}\\!\Downarrow\\!\mathtt{[1,2]^{\omega}}}}{\mathtt{[1,2]^{\omega}.head}\\!\Downarrow\\!\mathtt{1}}}{\mathtt{[2,1]^{\omega}.tail.min()}\\!\Downarrow\\!\mathtt{1}}\quad\displaystyle\frac{\vdots}{\mathtt{[2,1]^{\omega}.head}\\!\Downarrow\\!\mathtt{2}}}{\mathtt{Math.min([2,1]^{\omega}.tail.min(),[2,1]^{\omega}.head)}\\!\Downarrow\\!\mathtt{1}}}{\mathtt{\mathbf{if}\
[2,1]^{\omega}.tail.isEmpty()\ \mathbf{then}\ [2,1]^{\omega}.head\
\mathbf{else}\
Math.min([2,1]^{\omega}.tail.min(),[2,1]^{\omega}.head)}\\!\Downarrow\\!\mathtt{1}}\
\begin{array}[]{l}\end{array}}{\mathtt{[2,1]^{\omega}.min()}\\!\Downarrow\\!\mathtt{1}}\
\begin{array}[]{l}\end{array}$

Figure 5: Finite proof tree with codefinition for
$\mathtt{[2,1]^{\omega}.min()}\\!\Downarrow\\!\mathtt{1}$ ($T_{0}$ as in
Figure 4)

Non-determinism and conservativity The $\coFJ$ abstract semantics is
inherently non-deterministic. Indeed, depending on the codefinition, the non-
determinism of the coinductive interpretation may be kept. For instance,
consider the following method declaration:

⬇

class C {

C m() { this.m() } corec { any }

}

Method m() recursively calls itself. In the abstract semantics, the judgment
$\texttt{new}\ \texttt{C}().\texttt{m}()\\!\Downarrow\\!\textit{v}$ can be
derived for any value v. In the operational semantics defined in Section 4,
such method call evaluates to $({{\textit{x}},{\textit{x}:\textit{x}}})$, that
is, the representation of _undetermined_.

However, determinism of FJ evaluation is preserved. Indeed, $\coFJ$ abstract
semantics is a _conservative_ extension of FJ semantics, as formally stated
below.

######  Theorem 3.1 (Conservativity).

If ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$,
then $({{{\cal I}_{\scriptscriptstyle\textsc{FJ}}},{{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}}})\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}^{\prime}}$
iff $\textit{v}=\textit{v}^{\prime}$.

######  Proof 3.2.

Both directions can be easily proved by induction on the definition of ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$.
For the left-to-right direction, the fact that each syntactic category has a
unique applicable meta-rule is crucial.

This theorem states that, whichever the codefinitions chosen, $\coFJ$ does not
change the semantics of expressions evaluating to some value in FJ. That is,
$\coFJ$ abstract semantics allows derivation of new values only for
expressions whose semantics is undefined in standard FJ, as in the examples
shown above. Note also that, if no codefinition is specified, then the $\coFJ$
abstract semantics _coincides_ with the FJ one, because corule (abs-co-invk)
cannot be applied, hence no infinite proof trees can be built for the
evaluation of FJ expressions.

##  4 Operational semantics

We informally introduce the operational semantics of $\coFJ$, provide its
formal definition, and prove that it is deterministic and conservative.

Outline In contrast to the abstract semantics of the previous section, the aim
is to define a semantics which leads to an interpreter for the calculus. To
obtain this, there are two issues to be considered:

  1. 1.

infinite (regular) objects should be represented in a finite way;

  2. 2.

infinite (regular) proof trees should be replaced by finite proof trees.

In the following we explain how these issues are handled in the $\coFJ$
operational semantics.

To obtain (1), we use an approach based on _capsules_ [16], which are
essentially expressions supporting cyclic references. In our context, capsules
are pairs $({{\textit{e}},{\sigma}})$ where e is an FJ expression and $\sigma$
is an _environment_ , that is, a finite mapping from variables into FJ
expressions. Moreover, the following _capsule property_ is satisfied: writing
$\textit{FV}(\textit{e})$ for the set of free variables in e,
$\textit{FV}(\textit{e})\subseteq\mathit{dom}(\sigma)$ and, for all
$\textit{x}\in\mathit{dom}(\sigma)$,
$\textit{FV}(\sigma(\textit{x}))\subseteq\mathit{dom}(\sigma)$. An FJ source
expression e is represented by the capsule $({{\textit{e}},{\emptyset}})$,
where $\emptyset$ denotes the empty environment. In particular, values are
pairs $({{{\mathrm{v}}},{\sigma}})$ where ${\mathrm{v}}$ is an _open_ FJ
object, that is, an object possibly containing variables. In this way, cyclic
objects can be obtained: for instance,
$({{\textit{x}},{\textit{x}:\texttt{new}\ \texttt{NEL}(2,\texttt{new}\
\texttt{NEL}(1,\textit{x}))}})$ represents the infinite regular list
$[2,1]^{\omega}$ considered before.

To obtain (2), methods are _regularly corecursive_. This means that execution
keeps track of the pending method calls, so that, when a call is encountered
the second time, this is detected666The semantics detects an already
encountered call by relying on capsule equivalence (Figure 7)., avoiding non-
termination as it would happen with ordinary recursion. Regular corecursion in
$\coFJ$ is _flexible_ , since the behaviour of the method when a cycle is
detected is specified by the codefinition.

Consider, for instance, the method call new ListFactory().two_one(); thanks to
regular corecursion, the result is the cyclic object
$({{\textit{x}},{\textit{x}:\texttt{new}\ \texttt{NEL}(2,\texttt{new}\
\texttt{NEL}(1,\textit{x}))}})$. Indeed, the operational semantics associates
a fresh variable, say, x, to the initial call, so that, when the same call is
encountered the second time, the association $\textit{x}:{\textit{x}}$ is
added in the environment, and the codefinition is evaluated where any is
replaced by x. Hence, $({{\textit{x}},{\textit{x}:\textit{x}}})$ is returned
as result, so that the result of the original call is
$({{\textit{x}},{\textit{x}:\texttt{new}\ \texttt{NEL}(2,\texttt{new}\
\texttt{NEL}(1,\textit{x}))}})$. The call new ListFactory().from(0), instead,
does not terminate in the operational semantics, since no call is encountered
more than once (the resulting infinite object is non-regular).

Consider now the call $[2,1]^{\omega}.\texttt{allPos}()$. In this case, when
the call is encountered the second time, after an intermediate call
$[1,2]^{\omega}.\texttt{allPos}()$, the result of the evaluation of the
codefinition is true, so that the result of the original call is true as
well.777To be rigorous, a capsule of shape $({{\texttt{true}},{\\_}})$. If the
codefinition were any, then the result would be
$({{\textit{x}},{\textit{x}:\textit{x}}})$, that is, undetermined. Note that,
if the list is finite, then no regular corecursion is involved, since the same
call cannot occur more than once; the same holds if the list is cyclic, but
contains a non-positive element, hence the method invocation returns false.
The only case requiring regular corecursion is when the method is invoked on a
cyclic list with all positive elements, as $[2,1]^{\omega}$.

In the case of $[2,1]^{\omega}.\texttt{min}()$, when the call is encountered
the second time the result of the evaluation of the codefinition is $2$, so
that the result of the intermediate call $[1,2]^{\omega}.\texttt{min}()$ is
$1$, and this is also the result of the original call.

Formal definition To formally express the approach described above, the
judgment of the operational semantics has shape
$\textit{e},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$ where:
$({{\textit{e}},{\sigma}})$ is the capsule to be evaluated; $\tau$ is a _call
trace_ , used to keep track of already encountered calls, that is, an
injective map from _calls_
${\mathrm{v}}_{0}.\textit{m}(\overline{{\mathrm{v}}})$ to (possibly tagged)
variables, and $({{{\mathrm{v}}},{{\sigma^{\prime}}}})$ is the capsule result.
Variables in the codomain of the call trace have a tag ck during the checking
step for the corresponding call, as detailed below. The pair
$({{\textit{e}},{\sigma}})$ and $({{{\mathrm{v}}},{{\sigma^{\prime}}}})$ are
assumed to satisfy the capsule property.

The semantic rules are given in Figure 6. We denote by
${\sigma}\\{\textit{x}:\\!{\mathrm{v}}\\}$ the environment which gives
${\mathrm{v}}$ on x, and is equal to $\sigma$ elsewhere, and analogously for
other maps. Furthermore, we use the following notations, formally defined in
Figure 7.

  * •

$\mathit{unfold}({\mathrm{v}},\sigma)$ is the _unfolding_ of ${\mathrm{v}}$ in
$\sigma$, that is, the corresponding object, if any.

  * •

$\sigma_{1}{\sqcup}\sigma_{2}$ is the _union of environments_ , defined if
they agree on the common domain.

  * •

$({{{\mathrm{v}}},{\sigma}}){\approx}({{{\mathrm{v}}^{\prime}},{\sigma^{\prime}}})$
is the _equivalence of capsules_. As will be formalized in the first part of
Section 6, equivalent capsules denote the same sets of abstract objects. This
equivalence is extended by congruence to expressions, in particular to calls
${\mathrm{v}}_{0}.\textit{m}(\overline{{\mathrm{v}}})$.

  * •

$\tau_{\approx\sigma}$ is obtained by extending $\tau$ _up to equivalence_ in
$\sigma$. That is, detection of already encountered calls is performed up-to
equivalence in the current environment.

$\begin{array}[t]{llll}{\mathrm{v}}\in{\cal
V}\textsuperscript{op}&{:}{:}=&\texttt{new}\
\mathit{C}(\overline{{\mathrm{v}}})\mid x&\mbox{{\small{open {object}}}}\\\
\sigma&{:}{:}=&\textit{x}_{1}:{\mathrm{v}}_{1}\ldots\
\textit{x}_{n}:{\mathrm{v}}_{n}\hskip 8.00003pt(n\geq
0)&\mbox{{\small{environment}}}\\\
\mathit{c}&{:}{:}=&{\mathrm{v}}.\textit{m}(\overline{{\mathrm{v}}})&\mbox{{\small{call}}}\\\
{t}&{:}{:}=&[\textsf{ck}]&\mbox{{\small{{optional checking tag}}}}\\\
\tau&{:}{:}=&{\mathit{c}_{1}:\\!\textit{x}_{1}^{{t}_{1}},\ldots,\mathit{c}_{n}:\\!\textit{x}_{n}^{{t}_{n}}}\hskip
8.00003pt(n\geq 0)&\mbox{{\small{call trace}}}\end{array}$

$\begin{array}[]{l}{\tiny\textsc{({val})}}\displaystyle\frac{}{{\mathrm{v}},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma}}\
\begin{array}[]{l}\end{array}\hskip
15.00002pt{\tiny\textsc{({field})}}\displaystyle\frac{\textit{e},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}}{\textit{e}.\mathit{f},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{\sigma^{\prime}}}\
\begin{array}[]{l}\mathit{unfold}({\mathrm{v}},{\sigma^{\prime}})=\texttt{new}\
\mathit{C}({{\mathrm{v}}_{1},\ldots,{\mathrm{v}}_{n}})\\\
\mathit{fields}(\mathit{C})=\mathit{f}_{1}...\mathit{f}_{n}\\\
\mathit{f}=\mathit{f}_{i},i\in 1..n\end{array}\\\\[30.1388pt]
{\tiny\textsc{({new})}}\displaystyle\frac{\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},\sigma^{\prime}_{i}\hskip
8.00003pt\forall i\in 1..n}{\texttt{new}\
\mathit{C}(\textit{e}_{1},\ldots,\textit{e}_{n}),\sigma,\tau\\!\Downarrow\\!\texttt{new}\
\mathit{C}({{\mathrm{v}}_{1},\ldots,{\mathrm{v}}_{n}}),\bigsqcup_{i\in
1..n}{\sigma^{\prime}_{i}}}\ \begin{array}[]{l}\end{array}\\\\[34.44434pt]
\mbox{In all the following
rules:}\begin{array}[]{l}\overline{\textit{e}}=\textit{e}_{1},\ldots,\textit{e}_{n}\\\
\overline{{\mathrm{v}}}={\mathrm{v}}_{1}\ldots{\mathrm{v}}_{n}\\\
\mathit{c}={\mathrm{v}}_{0}.\textit{m}(\overline{{\mathrm{v}}})\\\
{\widehat{\sigma}}=\bigsqcup_{i\in 0..n}{\sigma^{\prime}_{i}}\\\
\mathit{unfold}({\mathrm{v}}_{0},\sigma^{\prime}_{0})=\texttt{new}\
\mathit{C}(\\_)\\\ \end{array}\\\\[47.36096pt] {\tiny\textsc{({invk-
ok})}}\displaystyle\frac{\begin{array}[]{l}\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{\sigma^{\prime}_{i}}\hskip
8.00003pt\forall i\in 0..n\\\
\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}],{\widehat{\sigma}},{{{\tau}\\{\mathit{c}:\\!\textit{x}\\}}}\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}\end{array}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}}\
\begin{array}[]{l}{\mathit{c}\not\in\mathit{dom}(\tau_{\approx{\widehat{\sigma}}})}\\\
\textit{x}\ \mbox{fresh}\\\
\mathit{mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}}})\\\
\textit{x}\not\in\mathit{dom}({\sigma^{\prime}})\end{array}\\\\[34.44434pt]
{\tiny\textsc{({invk-
check})}}\displaystyle\frac{\begin{array}[]{l}\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{\sigma^{\prime}_{i}}\hskip
8.00003pt\forall i\in 0..n\\\
\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}],{\widehat{\sigma}},{{\tau}\\{{\mathit{c}}:\\!\textit{x}\\}}\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}\\\
\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}],{\widehat{\sigma}}\sqcup{\sigma^{\prime}}\\{\textit{x}:\\!{\mathrm{v}}\\},{\tau}\\{{\mathit{c}}:\\!\textit{x}^{{\textsf{ck}}}\\}\\!\Downarrow\\!{\mathrm{v}}^{\prime},\sigma^{\prime\prime}\end{array}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\sigma,\tau\\!\Downarrow\\!\textit{x},{{\sigma^{\prime}}}\\{\textit{x}:\\!{\mathrm{v}}\\}}\
\begin{array}[]{l}{\mathit{c}\not\in\mathit{dom}(\tau_{\approx{\widehat{\sigma}}})}\\\
\textit{x}\ \mbox{fresh}\\\
\mathit{mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}}})\\\
\textit{x}\in\mathit{dom}({\sigma^{\prime}})\\\
({{\textit{x}},{{{\sigma^{\prime}}}\\{\textit{x}:\\!{\mathrm{v}}\\}}}){\approx}({{{\mathrm{v}}^{\prime}},{\sigma^{\prime\prime}}})\end{array}\\\\[34.44434pt]
{\tiny\textsc{({corec})}}\displaystyle\frac{\begin{array}[]{l}\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{\sigma^{\prime}_{i}}\hskip
8.00003pt\forall i\in 0..n\\\
\textit{e}^{\prime}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}][x/\texttt{any}],{{\widehat{\sigma}}}\\{\textit{x}:\\!\textit{x}\\},\tau\\!\Downarrow\\!{\mathrm{v}},{{\sigma^{\prime}}}\end{array}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{{\sigma^{\prime}}}\\{\textit{x}:\\!\textit{x}\\}}\
\begin{array}[]{l}\tau_{\approx{\widehat{\sigma}}}({\mathit{c}})=\textit{x}\\\
\textit{co-
mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}^{\prime}}})\end{array}\\\\[34.44434pt]
{\tiny\textsc{({look-
up})}}\displaystyle\frac{\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{\sigma^{\prime}_{i}}\hskip
8.00003pt\forall i\in
0..n}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\sigma,\tau\\!\Downarrow\\!\textit{x},{{\widehat{\sigma}}}}\
\begin{array}[]{l}\tau_{\approx{\widehat{\sigma}}}({\mathit{c}})={\textit{x}^{\textsf{ck}}}\\\
\end{array}\end{array}$

Figure 6: $\coFJ$ operational semantics

Rule (val) is needed for objects which are not FJ objects. Rule (field) is
similar to that of FJ except that the capsule
$({{{\mathrm{v}}},{{\sigma^{\prime}}}})$ must be unfolded to retrieve the
corresponding object. Furthermore, the resulting environment is that obtained
by evaluating the receiver. Rule (new) is analogous to that of FJ. The
resulting environment is the union of those obtained by evaluating the
arguments.

There are four rules for method invocation. In all of them, as in the FJ rule,
the receiver and argument expressions are evaluated first to obtain the call
$\mathit{c}={\mathrm{v}}.\textit{m}(\overline{{\mathrm{v}}})$. The environment
${\widehat{\sigma}}$ is the union of those obtained by these evaluations.
Then, the behavior is different depending whether such call (meaning a call
equivalent to $\mathit{c}$ in ${\widehat{\sigma}}$) has been already
encountered.

Rules (invk-ok) and (invk-check) handle888The two rules could be merged
together, but we prefer to make explicit the difference for sake of clarity. a
call $\mathit{c}$ which is encountered the first time, as expressed by the
side condition
$\mathit{c}\not\in{\mathit{dom}(\tau_{\approx{\widehat{\sigma}}})}$. In both,
the definition e, where the receiver replaces this and the arguments replace
the parameters, is evaluated. Such evaluation is performed in the call trace
$\tau$ updated to associate the call $\mathit{c}$ with an unused variable x
(in these two rules “x fresh” means that x does not occur in the derivations
of
$\textit{e}_{i},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},{\sigma^{\prime}_{i}}$,
for all $i\in 0..n$), and produces the capsule
$({{{\mathrm{v}}},{{\sigma^{\prime}}}})$. Then there are two cases, depending
on whether $\textit{x}\in\mathit{dom}({\sigma^{\prime}})$ holds.

If $\textit{x}\not\in\mathit{dom}({\sigma^{\prime}})$, then the evaluation of
the definition for $\mathit{c}$ has been performed without evaluating the
codefinition. That is, the same call has not been encountered, hence the
result has been obtained by standard recursion, and no additional check is
needed.

If $\textit{x}\in\mathit{dom}({\sigma^{\prime}})$, instead, then the
evaluation of the definition for ${\mathit{c}}$ has required to evaluate the
codefinition. In this case, an additional check is required (third premise).
That is,
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}]$
is evaluated once more under the assumption that ${\mathrm{v}}$ is the result
of the call. Formally, evaluation takes place in an environment updated to
associate x with ${\mathrm{v}}$, and the variable x corresponding to the call
is tagged with ck. The capsule result obtained in this way must be (equivalent
to) that obtained by the first evaluation of the body of the method. In
Section 5 we discuss in detail the role of this additional check, showing an
example where it is necessary. If the check succeeds, then the final result is
the variable x in the environment updated to associate x with ${\mathrm{v}}$.
Otherwise, rule (invk-check) cannot be applied since the last premise does not
hold. For simplicity, we assume the result of ${\mathit{c}}$ to be undefined
in this case; an additional rule could be added raising a runtime error in
case the result is different from the expected one, as should be done in an
implementation.

The remaining rules handle an already encountered call $\mathit{c}$, that is,
$\tau_{\approx{\widehat{\sigma}}}(\mathit{c})$ is defined. The behaviour is
different depending on whether the corresponding variable x is tagged or not.

If x is not tagged, then rule (corec) evaluates the codefinition where the
receiver object replaces this, the arguments replace the parameters, and,
furthermore, the variable x found in the call trace replaces any. In addition,
${\widehat{\sigma}}$ is updated to associate x with x. In this way, the
semantics keeps track of the application of rule (corec).

If x is tagged, instead, then we are in a checking step for the corresponding
call. In this case, rule (look-up) simply returns the associated variable for
a call; by definition of the operational semantics, in this case such a
variable is always defined in the environment.

Figure 7 contains the formal definitions of the notations used in the rules.

$\begin{array}[]{l}\mathit{unfold}({\mathrm{v}},\sigma)=\begin{cases}\texttt{new}\
\mathit{C}(\overline{{\mathrm{v}}})&$ if ${\mathrm{v}}=\texttt{new}\
\mathit{C}(\overline{{\mathrm{v}}})\\\
\mathit{unfold}(\sigma({\mathrm{v}}),\sigma)&$ if ${\mathrm{v}}=\textit{x}\\\
\end{cases}\\\
\mathit{undet}(\sigma)=\\{\textit{x}\in\mathit{dom}(\sigma)\mid\mathit{unfold}(\textit{x},\sigma)\uparrow\\}\end{array}$

$\begin{array}[]{l}\text{For $\sigma_{1}$ and $\sigma_{2}$ such that
$\sigma_{1}(\textit{x})=\sigma_{2}(\textit{x})$ for all
$\textit{x}\in\mathit{dom}(\sigma_{1})\cap\mathit{dom}(\sigma_{2})$}\\\\[7.74997pt]
(\sigma_{1}{\sqcup}\sigma_{2})(\textit{x})=\begin{cases}\sigma_{1}(\textit{x})&\textit{x}\in\mathit{dom}(\sigma_{1})\\\
\sigma_{2}(\textit{x})&\textit{x}\in\mathit{dom}(\sigma_{2})\end{cases}\end{array}$

Set $\stackrel{{\scriptstyle\sigma}}{{\leftrightarrow}}$ the least equivalence
relation on $\mathit{undet}(\sigma)$ such that
$\textit{x}\stackrel{{\scriptstyle\sigma}}{{\leftrightarrow}}y$ if
$\sigma(x)=y$, $[\textit{x}]$ the equivalence class of x, and
$\mathit{undet}_{\leftrightarrow}(\sigma)$ the quotient. A relation
$\alpha\subseteq\mathit{undet}(\sigma_{1})\times\mathit{undet}(\sigma_{2})$ is
a _$\sigma_{1},\sigma_{2}$ -renaming_ if it induces a (partial) bijection from
$\mathit{undet}_{\leftrightarrow}(\sigma_{1})$, still denoted $\alpha$, to
$\mathit{undet}_{\leftrightarrow}(\sigma_{2})$. Given $\alpha$ a
$\sigma_{1},\sigma_{2}$-renaming, the relation
$({{\textit{x}},{\sigma_{1}}}){\approx_{\alpha}}({{\textit{x}^{\prime}},{\sigma_{2}}})$
is coinductively defined by:

$\begin{array}[]{l}\displaystyle\frac{}{({{\textit{x}},{\sigma}}){\approx_{\alpha}}({{\textit{x}^{\prime}},{\sigma^{\prime}}})}\
\begin{array}[]{l}x\alpha x^{\prime}\end{array}\hskip
13.50002pt\displaystyle\frac{({{{\mathrm{v}}_{i}},{\sigma}}){\approx_{\alpha}}({{{\mathrm{v}}^{\prime}_{i}},{\sigma^{\prime}}})\quad\forall
i\in
1..n}{({{{\mathrm{v}}},{\sigma}}){\approx_{\alpha}}({{{\mathrm{v}}^{\prime}},{\sigma^{\prime}}})}\
\begin{array}[]{l}\mathit{unfold}({\mathrm{v}},\sigma)=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1},..,{\mathrm{v}}_{n})\\\
\mathit{unfold}({\mathrm{v}}^{\prime},\sigma^{\prime})=\texttt{new}\
\mathit{C}({\mathrm{v}}^{\prime}_{1},..,{\mathrm{v}}^{\prime}_{n})\end{array}\end{array}$

A $\sigma_{1},\sigma_{2}$-renaming $\alpha$ is _strict_ if, for
$\textit{x},y\in\mathit{undet}(\sigma_{1})\cap\mathit{undet}(\sigma_{2})$,
$[\textit{x}]\alpha[y]$ iff
$\textit{x}\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}y$ and
$\textit{x}\stackrel{{\scriptstyle\sigma_{2}}}{{\leftrightarrow}}y$.
We write
$({{{\mathrm{v}}},{\sigma}}){\approx}({{{\mathrm{v}}^{\prime}},{\sigma^{\prime}}})$
if
$({{{\mathrm{v}}},{\sigma}}){\approx_{\alpha}}({{{\mathrm{v}}^{\prime}},{\sigma^{\prime}}})$
for some strict $\alpha$.

$\tau_{\approx\sigma}(\mathit{c}^{\prime})=\tau(\mathit{c})foreach\mathit{c}^{\prime}suchthat({{\mathit{c}^{\prime}},{\sigma}}){\approx}({{\mathit{c}},{\sigma}})$

Figure 7: $\coFJ$ auxiliary definitions

Note that $\mathit{unfold}$, being inductively defined, can be undefined,
denoted $\uparrow$, in presence of unguarded cycles among variables. Capsule
equivalence, instead, is defined coinductively, so that, e.g.,
$({{\textit{x}},{\textit{x}:\texttt{new}\ \mathit{C}(\textit{x})}})$ is
equivalent to $({{\textit{x}},{\textit{x}:\texttt{new}\
\mathit{C}(\texttt{new}\ \mathit{C}(\textit{x}))}})$. Capsule equivalence
implicitly subsumes $\alpha$-equivalence of variables whose unfolding is
defined, e.g., $({{\textit{x}},{\textit{x}:\texttt{new}\
\mathit{C}(\textit{x})}})$ is equivalent to $({{y},{y:\texttt{new}\
\mathit{C}(y)}})$. Instead, $\alpha$-equivalence of undetermined variables is
given by an explicit renaming, which should preserve disjointness of cycles.
For instance, $({{\texttt{new}\
\mathit{C}(\textit{x},y)},{(\textit{x}:y,y:\textit{x})}})$ is equivalent to
$({{\texttt{new}\
\mathit{C}(\textit{x},\textit{x})},{\textit{x}:\textit{x}}})$, but is _not_
equivalent to $({{\texttt{new}\
\mathit{C}(\textit{x},y)},{(\textit{x}:\textit{x},y:y)}})$. Indeed, in the
latter case x and $y$ can be instantiated independently. We will prove in
Section 6 (Theorem 6.1) that the relation ${\approx_{\alpha}}$, for some
$\sigma_{1},\sigma_{2}$-renaming $\alpha$, is the operational counterpart of
the fact that two capsules denote the same set of abstract values. The
stronger strictness condition prevents erroneous identification of objects
during evaluation, e.g., $({{\texttt{new}\
\mathit{C}(\textit{x},y)},{(\textit{x}:\textit{x},y:y)}})$ is not equivalent
to $({{\texttt{new}\ \mathit{C}(y,\textit{x})},{(y:y,x:x)}})$.

Determinism and conservativity In contrast to $\coFJ$ abstract semantics, but
like FJ, $\coFJ$ operational semantics is deterministic.

######  Theorem 4.1 (Determinism).

If $\textit{e},\sigma,\tau_{1}\\!\Downarrow\\!{\mathrm{v}}_{1},\sigma_{1}$ and
$\textit{e},\sigma,\tau_{2}\\!\Downarrow\\!{\mathrm{v}}_{2},\sigma_{2}$ hold
and $\mathit{dom}(\tau_{1})=\mathit{dom}(\tau_{2})$, then
$({{{\mathrm{v}}_{1}},{\sigma_{1}}})$ and
$({{{\mathrm{v}}_{2}},{\sigma_{2}}})$ are equal up-to $\alpha$-equivalence.

######  Proof 4.2.

The proof is by induction on the derivation for
$\textit{e},\sigma,\tau_{1}\\!\Downarrow\\!{\mathrm{v}}_{1},\sigma_{1}$. The
key point is that, once fixed e, $\sigma$ and $\mathit{dom}(\tau_{1})$, there
is a unique applicable rule, hence both
$\textit{e},\sigma,\tau_{1}\\!\Downarrow\\!{\mathrm{v}}_{1},\sigma_{1}$ and
$\textit{e},\sigma,\tau_{2}\\!\Downarrow\\!{\mathrm{v}}_{2},\sigma_{2}$ are
derived by the same rule.

As the abstract one, the operational semantics is a conservative extension of
the standard FJ semantics. This result follows from soundness with respect to
the abstract semantics in next section, however the direct proof below
provides some useful insight.

######  Theorem 4.3 (Conservativity).

If ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$,
then $\textit{e},\emptyset,\emptyset\\!\Downarrow\\!{{\mathrm{v}}},\sigma$
holds iff ${{\mathrm{v}}}=\textit{v}$ and $\sigma=\emptyset$.

For the proof, we need some auxiliary lemmas and definitions. First, we note
that FJ has the _strong determinism_ property: each expression has at most one
finite proof tree in ${\cal I}_{\scriptscriptstyle\textsc{FJ}}$.

######  Lemma 4.4 (FJ strong determinism).

If ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}_{1}}$
by a proof tree $t_{1}$ and ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}_{2}}$
by a proof tree $t_{2}$, then $t_{1}=t_{2}$ and
$\textit{v}_{1}=\textit{v}_{2}$.

######  Proof 4.5.

By induction on the definition of $\textit{e}\\!\Downarrow\\!\textit{v}_{1}$.
The key point is that each judgement is the consequence of exactly one rule.

By relying on strong determinism, it is easy to see that in FJ a proof tree
for an expression cannot contain another node labelled by the same expression.
In other words, if the evaluation of e requires to evaluate e again, then the
FJ semantics is undefined on e, as expected.

######  Lemma 4.6.

A proof tree in ${\cal I}_{\scriptscriptstyle\textsc{FJ}}$ for
$\textit{e}\\!\Downarrow\\!\textit{v}$ cannot contain any other node
$\textit{e}\\!\Downarrow\\!\textit{v}^{\prime}$, for any
$\textit{v}^{\prime}$.

######  Proof 4.7.

By Lemma 4.4, there is a unique proof tree $t$ for the expression e. Hence, a
node $\textit{e}\\!\Downarrow\\!\textit{v}^{\prime}$ in $t$ would be
necessarily the root of a subtree of $t$ equal to $t$, that is, it is the root
of $t$.

######  Definition 4.8.

Let ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$.
A call trace $\tau$ is _disjoint_ from $\textit{e}\\!\Downarrow\\!\textit{v}$
if in its proof tree999Unique thanks to Lemma 4.4. there are no instances of
(FJ-invk) where
$\textit{v}_{0}.\textit{m}(\overline{\textit{v}})\in\mathit{dom}(\tau)$.

######  Lemma 4.9.

If ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$,
then, for all $\tau$ disjoint from $\textit{e}\\!\Downarrow\\!\textit{v}$, we
have $\textit{e},\emptyset,\tau\\!\Downarrow\\!\textit{v},\emptyset$.

######  Proof 4.10.

The proof is by induction on the definition of
$\textit{e}\\!\Downarrow\\!\textit{v}$.

(FJ-field)

Let $\tau$ be a call trace disjoint from
$\textit{e}.\mathit{f}\\!\Downarrow\\!\textit{v}_{i}$. Since ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$,
with $\textit{v}=\texttt{new}\
\mathit{C}(\textit{v}_{1},\ldots,\textit{v}_{n})$, holds by hypothesis, and
$\tau$ is, by definition, also disjoint from
$\textit{e}\\!\Downarrow\\!\textit{v}$, we get
$\textit{e},\emptyset,\tau\\!\Downarrow\\!\textit{v},\emptyset$ by induction
hypothesis. Then, since $\mathit{unfold}(\textit{v},\emptyset)=\textit{v}$, we
get
$\textit{e}.\mathit{f},\emptyset,\tau\\!\Downarrow\\!\textit{v}_{i},\emptyset$
by rule (field).

(FJ-new)

Let $\tau$ be a call trace disjoint from $\texttt{new}\
\mathit{C}(\textit{e}_{1},\ldots,\textit{e}_{n})\\!\Downarrow\\!\texttt{new}\
\mathit{C}(\textit{v}_{1},\ldots,\textit{v}_{n})$. For all $i\in 1..n$, since
${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}_{1}\\!\Downarrow\\!\textit{v}_{i}}$
holds by hypothesis, and $\tau$ is, by definition, also disjoint from
$\textit{e}_{i}\\!\Downarrow\\!\textit{v}_{i}$, we get
$\textit{e}_{{i}},\emptyset,\tau\\!\Downarrow\\!\textit{v}_{i},\emptyset$ by
induction hypothesis. Then, we get $\texttt{new}\
\mathit{C}(\textit{e}_{1},\ldots,\textit{e}_{n}),\emptyset,\tau\\!\Downarrow\\!\texttt{new}\
\mathit{C}(\textit{v}_{1},\ldots,\textit{v}_{n}),\emptyset$ by rule (new).

(FJ-invk)

Let $\tau$ be a call trace disjoint from
$\textit{e}_{0}.\textit{m}(\textit{e}_{1},\ldots,\textit{e}_{n})\\!\Downarrow\\!\textit{v}$.
For all $i\in 0..n$, since ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}_{i}\\!\Downarrow\\!\textit{v}_{i}}$
holds by hypothesis, and $\tau$ is, by definition, also disjoint from
$\textit{e}_{{i}}\\!\Downarrow\\!\textit{v}_{i}$, we get
$\textit{e}_{i},\emptyset,\tau\\!\Downarrow\\!\textit{v}_{i},\emptyset$ by
induction hypothesis. Set
$\overline{\textit{v}}=\textit{v}_{1}\ldots\textit{v}_{n}$ and
$\textit{e}^{\prime}=\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}]$.
By hypothesis, ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}^{\prime}\\!\Downarrow\\!\textit{v}}$
and, by definition, $\tau$ is also disjoint from
$\textit{e}^{\prime}\\!\Downarrow\\!\textit{v}$; furthermore, by Lemma 4.6,
$\textit{e}^{\prime}$ cannot occur twice in the proof tree for
$\textit{e}^{\prime}\\!\Downarrow\\!\textit{v}$, hence
${{\tau}\\{\textit{v}_{0}.\textit{m}(\overline{\textit{v}}):\\!\textit{x}\\}}$
is disjoint from $\textit{e}^{\prime}\\!\Downarrow\\!\textit{v}$, for any
fresh variable x. Then, by induction hypothesis, we have
$\textit{e}^{\prime},\emptyset,{{\tau}\\{\textit{v}_{0}.\textit{m}(\overline{\textit{v}}):\\!\textit{x}\\}}\\!\Downarrow\\!\textit{v},\emptyset$,
thus we get
$\textit{e}_{0}.\textit{m}(\textit{e}_{1},\ldots,\textit{e}_{n}),\emptyset,\tau\\!\Downarrow\\!\textit{v},\emptyset$
by rule (invk-ok).

We can now prove the conservativity result for $\coFJ$ operational semantics.

######  Proof 4.11 (Proof of Theorem 4.3).

The right-to-left direction follows from Lemma 4.9, since $\emptyset$ is
disjoint from any expression, while the other direction follows from the
right-to-left one and Theorem 4.1.

For $\coFJ$ operational semantics we can prove an additional result,
characterizing derivable judgements which produce an empty environment. The
meaning is that all results obtained _without using the codefinitions_ are
original FJ results.

######  Lemma 4.12.

If $\textit{e},\emptyset,\tau\\!\Downarrow\\!{\mathrm{v}},\emptyset$ holds,
then ${\mathrm{v}}$ is an FJ value v, and ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$.

##  5 Advanced examples

This section provides some more complex examples to better understand the
operational semantics of $\coFJ$ in Section 4 and its relationship with the
abstract semantics in Section 3.

Examples on lists We first show an example motivating the additional checking
step (third premise) in rule (invk-check). Essentially, the success of this
check for some capsule result corresponds to the existence of an infinite tree
in the abstract semantics, whereas the fact that this capsule result is
obtained by assuming the codefinition as result of the cyclic call (second
premise) corresponds to the existence of a finite tree which uses the
codefinition.

Assume to add to our running example of lists of integers a method that
returns the sum of the elements. For infinite regular lists, that is, lists
ending with a cycle, a result should be returned if the cycle has sum $0$, for
instance for a list ending with infinitely many $0$s, and no result if the
cycle has sum different from $0$. This can be achieved as follows.

⬇

class List extends Object { ...

int sum() {0}

}

class NonEmptyList extends List { ...

int sum() {this.head + this.tail.sum()} corec {0}

}

It is easy to see that the abstract semantics of the previous section
formalizes the expected behavior. For instance, an infinite tree for a
judgment $[2,1]^{\omega}.\texttt{sum}()\\!\Downarrow\\!\textit{v}$ only exists
for $\textit{v}=2+1+\textit{v}$, and there are no solutions of this equation,
hence there is no result. In the operational semantics, by evaluating the body
assuming the codefinition as result of the cyclic call (second premise of rule
(invk-check)) the spurious result $3$ would be returned. This is avoided by
the third premise, which evaluates the method body assuming $3$ as result of
the cyclic call. Since we _do not_ get $3$ in turn as result, evaluation is
stuck, as expected.

Note that the stuckness situation is detected: the last side-condition of rule
(invk-check) fails, and a dynamic error (not modeled for simplicity, see the
comments to the rule) is raised, likely an exception in an implementation. On
the other hand, computations which _never_ reach (a base case or) an already
encountered call still do not terminate in this operational semantics, exactly
as in the standard one, and the fact that this does not happen should be
_proved_ by suitable techniques, see the Conclusion.

All the examples shown until now have a constant codefinition. We show now an
example where this is not enough. Consider the method remPos() that removes
positive elements. A first attempt at a $\coFJ$ definition is the following:

⬇

class NonEmptyList extends List { ...

List remPos() {

if(this.head > 0) this.tail.remPos()

else new NonEmptyList(this.head,this.tail.remPos())}

corec {new EmptyList()}

Is this definition correct? Actually, it provides the expected behavior on
finite lists, and cyclic lists where the cycle contains only positive
elements. However, when the cycle contains at least one non positive element,
there is no result. For instance, consider the method call
$[0,1]^{\omega}.\texttt{remPos}()$. In the abstract semantics, an infinite
tree can be constructed for the judgment
$[0,1]^{\omega}.\texttt{remPos}()\\!\Downarrow\\!\textit{v}$ only if
$\textit{v}=0:\textit{v}$, and this clearly only holds for
$\textit{v}=[0]^{\omega}$. However, no finite tree can be constructed for this
judgment using the codefinition. Note that, in the operational semantics,
without the additional check (third premise of rule (invk-check)), we would
get the spurious result $[0]$. In order to have a $\coFJ$ definition complete
with respect to the expected behavior, we should provide a different
codefinition for lists with infinitely many non-positive elements.

⬇

class NonEmptyList extends List { ...

List remPos() {

if(this.head > 0) this.tail.remPos()

else new NonEmptyList(this.head,this.tail.remPos())}

corec {if (this.allPos() then new EmptyList() else any}

Arithmetic with rational and real numbers All real numbers in the closed
interval $\\{0..1\\}$ can be represented by infinite lists
$[d_{1},d_{2},\ldots]$ of decimal digits; more precisely, the infinite list
$[d_{1},d_{2},\ldots]$ represents the real number which is the limit of the
series $\sum_{i=1}^{\infty}10^{-i}d_{i}$.

It is well-known that all rational numbers in $\\{0..1\\}$ correspond to
either a terminating or repeating decimal, hence they can be represented by
infinite regular lists of digits, where terminating decimals end with either
an infinite sequence of $0$ or an infinite sequence of $9$; for instance, the
terminating decimal $\frac{1}{2}$ can be represented equivalently by either
$[5,0,0,\ldots]$ or $[4,9,9,\ldots]$, while the repeating decimal
$\frac{1}{3}$ is represented by $[3,3,\ldots]$.

Therefore, in $\coFJ$ all rational numbers in $\\{0..1\\}$ can be effectively
represented with infinite precision at the level of the operational semantics;
to this aim, we can declare a class Number with the two fields digit of type
int and others of type Number: digit contains the leftmost digit, that is, the
most significant, while others refers to the remaining digits, that is, the
number we would obtain by a single left shift (corresponding to multiplication
by $10$). Since also non-regular values are allowed, in the abstract semantics
class Number can be used to represent also all irrational numbers in
$\\{0..1\\}$.

We now show how it is possible to compute in $\coFJ$ the addition of rational
numbers in $\\{0..1\\}$ with infinite precision. We first define the method
carry which computes the carry of the addition of two numbers: its result is
$0$ if the sum belongs to $\\{0..1\\}$, $1$ otherwise.

⬇

class Number extends Object { // numbers in {0..1}

int digit; // leftmost digit

Number others; // all other digits

int carry(Number num){ // returns 0 if this+num<=1, 1 otherwise

if (this.digit+num.digit!=9) (this.digit+num.digit)/10

else this.others.carry(num.others)

} corec {0}

}

The two numbers this and num are inspected starting from the most significant
digits: if their sum is different from $9$, then the carry can be computed
without inspecting the other digits, hence the integer division by $10$ of the
sum is returned. Corecursion is needed when the sum of the two digits equals
$9$; in this case the carry is the same obtained from the addition of
this.others and num.others.

Finally, in the codefinition the carry $0$ is returned; indeed, the
codefinition is evaluated only when the sum of the digits for all positions
inspected so far is $9$ and the same patterns of digits are encountered for
the second time. This can only happen for pairs of numbers whose addition is
$[9,9,\ldots]$, that is, $1$, hence the computed carry must be $0$.

Based on method carry, we can define method add which computes the addition of
two numbers, excluding the possible carry in case of overflow.

⬇

class Number extends Object { ... // declarations as above

Number add(Number num){ // returns this+num

new Number(

(this.digit+num.digit+this.others.carry(num.others))%10,

this.others.add(num.others))} corec {any}

}

For each position, the corresponding digits of this and num are added to the
carry computed for the other digits (this.others.carry(num.others)), then the
reminder of the division by $10$ gives the most significant digit of the
result, whereas the others are obtained by corecursively calling the method on
the remaining digits (this.others.add(num.others)). Since this call is guarded
by a constructor call, the codefinition is any.

Note that, in the abstract semantics, methods carry and add correctly work
also for irrational numbers.

Method add above is simple, but has the drawback that the same carries are
computed more times; hence, in the worst case, the time complexity is
quadratic in the period101010Indeed, the worst case scenario is when the carry
propagates over all digits because their sum is always $9$, and this can
happen only if the two numbers have the same period. of the two involved
repeating decimals. To overcome this issue, we present a more elaborate
example where carries are computed only once for any position; this is
achieved by method all_carries below, which returns the sequence of all
carries (hence, a list of binary digits).

Method simple_add corecursively adds all digits without considering carries,
while method add, defined on top of simple_add and all_carries, computes the
final result. This new version of add is not recursive and, hence. does not
need a codefinition.

⬇

class Number extends Object { ... // declarations as above

Number all_carries(Number num){ // carries for all positions

this.simple_carries(num).complete()

}

Number simple_carries(Number num){ // carries computed immediately

if(this.digit+num.digit!=9)

new Number((this.digit+num.digit)/10,

this.others.simple_carries(num.others))

else new Number(9,this.others.simple_carries(num.others))

} corec {any}

Number complete(){ // computes missing carries marked with 9

if(this.digit!=9) new Number(this.digit,this.others.complete())

else this.fill(this.carry_lookahead()).complete()

} corec {any}

Number fill(int dig){ // fills with dig all next missing carries

if(this.digit!=9) this else new Number(dig,this.others.fill(dig))

} corec {any}

int carry_lookahead(){ // returns the next computed carry

if(this.digit!=9) this.digit else this.others.carry_lookahead()

} corec {0}

Number simple_add(Number num){ // addition without carries

new Number((this.digit+num.digit)%10,

this.others.simple_add(num.others))

} corec {any}

Number add(Number num){

this.simple_add(num).simple_add(this.all_carries(num).others)

}

}

Distances on graphs The last example of this section involves graphs, which
are the paradigmatic example of cyclic data structure. Our aim is to compute
the _distance_ , that is, the minimal length of a path, between two
vertexes111111The example can be easily adapted to weighted paths.. Consider a
graph ($V$, adj) where $V$ is the set of vertexes and $adj:V\rightarrow\wp(V)$
gives, for each vertex, the set of the adjacent vertexes. Each vertex has an
identifier id assumed to be unique. We assume a class $\texttt{Nat}^{\infty}$,
with subclasses Nat with an integer field, and Infty with no fields, for
naturals and $\infty$ (distance between unconnected nodes), respectively. Such
classes offer methods succ() for the successor, and
min($\texttt{Nat}^{\infty}$ n) for the minimum, with the expected behaviour
(e.g., succ in class $\texttt{Nat}^{\infty}$ returns $\infty$).

⬇

class Vertex extends Object {

Id id; AdjList adjVerts;

$\texttt{Nat}^{\infty}$dist(Id id) {

this.id==id?new Nat(0):this.adjVerts.dist(id).succ()}

corec {new Infty()}

}

class AdjList extends Object { }

class EAdjList extends AdjList {

$\texttt{Nat}^{\infty}$dist(Id id) { new Infty() }

}

class NEAdjList extends AdjList {

Vertex vert; AdjList adjVerts;

$\texttt{Nat}^{\infty}$dist(Id id)
{this.vert.dist(id).min(this.adjVerts.dist(id))}

}

Clearly, if the destination id and the source node coincide, then the distance
is 0. Otherwise, the distance is obtained by incrementing by one the minimal
distance from an adjacent to id, computed by method dist() of AdjList called
on the adjacency list. The codefinition of method dist() of class Vertex is
needed since, in presence of a cycle, $\infty$ is returned and non-termination
is avoided. The same approach can be adopted for visiting a graph: instead of
keeping trace of already encountered nodes, cycles are implicitly handled by
the loop detection mechanism of $\coFJ$.

##  6 Soundness

Soundness of the operational semantics with respect to the abstract one means,
roughly, that a value derived using the rules in Figure 6 can also be derived
by those in Figure 2. However, this statement needs to be refined, since
values in the two semantics are different: possibly infinite objects in the
abstract semantics, and capsules in the operational semantics.

We define a relation from capsules to abstract objects, formally express
soundness through this relation, and introduce an intermediate semantics to
carry out the proof in two steps.

From capsules to infinite objects Intuitively, given a capsule
$({{{\mathrm{v}}},{\sigma}})$, we get an abstract value by instantiating
variables in ${\mathrm{v}}$ with abstract values, in a way consistent with
$\sigma$. To make this formal, we need some preliminary definitions.

A _substitution_ $\theta$ is a function from variables to abstract values. We
denote by $\textit{e}\,\theta$ the abstract expression obtained by applying
$\theta$ to e. In particular, if e is an open value ${\mathrm{v}}$, then
${\mathrm{v}}\,\theta$ is an abstract value. Given an environment $\sigma$ and
a substitution $\theta$, the substitution $\sigma[\theta]$ is defined by:

$\sigma[\theta](\textit{x})=\begin{cases}\sigma(\textit{x})\,\theta&\textit{x}\in\mathit{dom}(\sigma)\\\
\theta(x)&\textit{x}\notin\mathit{dom}(\sigma)\end{cases}$

Then, a _solution_ of $\sigma$ is a substitution $\theta$ such that
$\sigma[\theta]=\theta$. Let $\textsf{Sol}(\sigma)$ be the set of solutions of
$\sigma$. Finally, if $({{\textit{e}},{\sigma}})$ is a capsule, we define the
set of abstract expressions it denotes as
$\llbracket\textit{e},\sigma\rrbracket=\\{\textit{e}\,\theta\mid\theta\in\textsf{Sol}(\sigma)\\}$.
Note that $\llbracket{\mathrm{v}},\sigma\rrbracket\subseteq{\cal
V}\textsuperscript{a}$, for any capsule $({{{\mathrm{v}}},{\sigma}})$. We now
show an operational characterization of the semantic equality.

######  Theorem 6.1.

$\llbracket{\mathrm{v}}_{1},\sigma_{1}\rrbracket{=}\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket$
iff
$({{{\mathrm{v}}_{1}},{\sigma_{1}}}){\approx_{\alpha}}({{{\mathrm{v}}_{2}},{\sigma_{2}}})$,
for some $\sigma_{1},\sigma_{2}$-renaming $\alpha$.

To prove this result we need some auxiliary definitions and lemmas. The _tree
expansion_ of a capsule $({{{\mathrm{v}}},{\sigma}})$ is the possibly infinite
open value coinductively defined as follows:

$\mathit{T}({\mathrm{v}},\sigma)=\begin{cases}\textit{x}&{\mathrm{v}}=\textit{x}\text{
and }\mathit{unfold}(\textit{x},\sigma)\uparrow\\\ \texttt{new}\
\mathit{C}(\mathit{T}({\mathrm{v}}_{1},\sigma),\ldots,\mathit{T}({\mathrm{v}}_{n},\sigma))&\mathit{unfold}({\mathrm{v}},\sigma)=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1},\ldots,{\mathrm{v}}_{n})\end{cases}$

The next proposition shows relations between solutions and tree expansion of a
capsule.

######  Proposition 6.2.

Let $({{{\mathrm{v}}},{\sigma}})$ be a capsule and
$\theta\in\textsf{Sol}(\sigma)$, then

  1. 1.

if $\mathit{unfold}({\mathrm{v}},\sigma)\uparrow$ then
${\mathrm{v}}=\textit{x}$ and
$\textit{x}\stackrel{{\scriptstyle\sigma}}{{\leftrightarrow}}\textit{x}$

  2. 2.

$\textit{FV}(\mathit{T}({\mathrm{v}},\sigma))\subseteq\\{\textit{x}\in\mathit{dom}(\sigma)\mid\textit{x}\stackrel{{\scriptstyle\sigma}}{{\leftrightarrow}}\textit{x}\\}$

  3. 3.

if $x\stackrel{{\scriptstyle\sigma}}{{\leftrightarrow}}y$ then
$\theta(x)=\theta(y)$

  4. 4.

if $\mathit{unfold}({\mathrm{v}},\sigma)=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1},\ldots,{\mathrm{v}}_{n})$ then
${\mathrm{v}}\,\theta=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1}\,\theta,\ldots,{\mathrm{v}}_{n}\,\theta)$

  5. 5.

${\mathrm{v}}\,\theta=\mathit{T}({\mathrm{v}},\sigma)\,\theta$

Given a relation $\alpha$ on variables, we will denote by $\alpha^{\circ}$ the
opposite relation and by $=_{\alpha}$ the equality of possibly infinite open
values up-to $\alpha$, coinductively defined by the following rules:

$\displaystyle\frac{}{x=_{\alpha}y}\ \begin{array}[]{l}x\alpha
y\end{array}\hskip
15.00002pt\displaystyle\frac{t_{i}=_{\alpha}s_{i}\quad\forall i\in
1..n}{\texttt{new}\ \mathit{C}(t_{1},\ldots,t_{n})=_{\alpha}\texttt{new}\
\mathit{C}(s_{1},\ldots,s_{n})}\ \begin{array}[]{l}\end{array}$

It is easy to check that

  * •

$\alpha$ is a $\sigma_{1},\sigma_{2}$-renaming iff $\alpha^{\circ}$ is a
$\sigma_{2},\sigma_{1}$-renaming,

  * •

$({{{\mathrm{v}}_{1}},{\sigma_{1}}}){\approx_{\alpha}}({{{\mathrm{v}}_{2}},{\sigma_{2}}})$
iff
$({{{\mathrm{v}}_{2}},{\sigma_{2}}}){\approx_{\alpha^{\circ}}}({{{\mathrm{v}}_{1}},{\sigma_{1}}})$,

  * •

$t_{1}=_{\alpha}t_{2}$ iff $t_{2}=_{\alpha^{\circ}}t_{1}$.

We have the following lemmas:

######  Lemma 6.3.

$({{{\mathrm{v}}_{1}},{\sigma_{1}}}){\approx_{\alpha}}({{{\mathrm{v}}_{2}},{\sigma_{2}}})$
iff
$\mathit{T}({\mathrm{v}}_{1},\sigma_{1}){=_{\alpha}}\mathit{T}({\mathrm{v}}_{2},\sigma_{2})$,
for each $\sigma_{1},\sigma_{2}$-renaming $\alpha$.

######  Proof 6.4.

The proof is immediate by coinduction in both directions.

######  Lemma 6.5.

If
$\mathit{T}({\mathrm{v}}_{1},\sigma_{1}){=_{\alpha}}\mathit{T}({\mathrm{v}}_{2},\sigma_{2})$,
where $\alpha$ is a $\sigma_{1},\sigma_{2}$-renaming, then
$\llbracket{\mathrm{v}}_{1},\sigma_{1}\rrbracket=\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket$.

######  Proposition 6.6.

If
$\llbracket{\mathrm{v}}_{1},\sigma_{1}\rrbracket=\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket$
then

  1. 1.

if $\mathit{unfold}({\mathrm{v}}_{1},\sigma_{1})\uparrow$ then
$\mathit{unfold}({\mathrm{v}}_{2},\sigma_{2})\uparrow$,

  2. 2.

if $\mathit{unfold}({\mathrm{v}}_{1},\sigma_{1})=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1,1},\ldots,{\mathrm{v}}_{1,n})$ then
$\mathit{unfold}({\mathrm{v}}_{2},\sigma_{2})=\texttt{new}\
\mathit{C}({\mathrm{v}}_{2,1},\ldots,{\mathrm{v}}_{2,n})$ and, for all $i\in
1..n$,
$\llbracket{\mathrm{v}}_{1,i},\sigma_{1}\rrbracket=\llbracket{\mathrm{v}}_{2,i},\sigma_{2}\rrbracket$.

######  Lemma 6.7.

If
$\llbracket{\mathrm{v}}_{1},\sigma_{1}\rrbracket{=}\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket$
then
$\mathit{T}({\mathrm{v}}_{1},\sigma_{1})=_{\alpha}\mathit{T}({\mathrm{v}}_{2},\sigma_{2})$,
for some $\sigma_{1},\sigma_{2}$-renaming $\alpha$.

######  Proof 6.8 (Proof of Theorem 6.1).

The right-to-left direction follows from Lemma 6.3 and Lemma 6.5, while the
other direction follows from Lemma 6.7 and Lemma 6.3.

Since by definition ${\approx}$ is equal to ${\approx_{\alpha}}$ for some
$\alpha$, applying Lemma 6.3 and Lemma 6.5 we get that if
$({{{\mathrm{v}}_{1}},{\sigma_{1}}}){\approx}({{{\mathrm{v}}_{2}},{\sigma_{2}}})$
then
$\llbracket{\mathrm{v}}_{1},\sigma_{1}\rrbracket=\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket$.
Actually we can prove a stronger result:

######  Lemma 6.9.

If
$({{{\mathrm{v}}_{1}},{\sigma_{1}}}){\approx_{\alpha}}({{{\mathrm{v}}_{2}},{\sigma_{2}}})$
for some strict $\sigma_{1},\sigma_{2}$-renaming $\alpha$, then, for each
solution $\theta\in\textsf{Sol}(\sigma_{1}\cap\sigma_{2})$, there are
$\theta_{1}\in\textsf{Sol}(\sigma_{1})$ and
$\theta_{2}\in\textsf{Sol}(\sigma_{2})$ such that
${\mathrm{v}}_{1}\,\theta_{1}={\mathrm{v}}_{2}\,\theta_{2}$ and, for all
$\textit{x}\in\mathit{dom}(\sigma_{1}\cap\sigma_{2})$,
$\theta_{1}(\textit{x})=\theta(\textit{x})=\theta_{2}(\textit{x})$.

Soundness statement We can now formally state the soundness result:

######  Theorem 6.10.

If $\textit{e},\emptyset,\emptyset\\!\Downarrow\\!{\mathrm{v}},\sigma$, then,
for all $\textit{v}\in\llbracket{\mathrm{v}},\sigma\rrbracket$, $({{{\cal
I}_{\scriptscriptstyle\textsc{FJ}}},{{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}}})\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$.

This main result is about the evaluation of source expressions, hence both the
environment and the call trace are empty. To carry out the proof we need to
generalize the statement.

######  Theorem 6.11 (Soundness).

If
$\textit{e},\sigma,\emptyset\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$,
then, for all $\theta\in\textsf{Sol}({\sigma^{\prime}})$, $({{{\cal
I}_{\scriptscriptstyle\textsc{FJ}}},{{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}}})\\!\vdash\\!{\textit{e}\,\theta\\!\Downarrow\\!{\mathrm{v}}\,\theta}$.

To show that this is actually a generalization, set $\sigma_{1}\leq\sigma_{2}$
if $\mathit{dom}(\sigma_{1})\subseteq\mathit{dom}(\sigma_{2})$, and, for all
$\textit{x}\in\mathit{dom}(\sigma_{1})$,
$\sigma_{1}(\textit{x})=\sigma_{2}(\textit{x})$. We use the following lemmas.

######  Lemma 6.12.

If $\sigma_{1}\leq\sigma_{2}$, then
$\textsf{Sol}(\sigma_{2})\subseteq\textsf{Sol}(\sigma_{1})$.

######  Lemma 6.13.

If $\textit{e},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$,
then $\sigma\leq{\sigma^{\prime}}$.

In the statement of Theorem 6.11, thanks to Lemma 6.13, we know that
$\sigma\leq{\sigma^{\prime}}$, hence, by Lemma 6.12,
$\theta\in\textsf{Sol}(\sigma)$, thus
$\textit{e}\,\theta\in\llbracket\textit{e},\sigma\rrbracket$. Theorem 6.11
implies Theorem 6.10, since, when $\sigma=\emptyset$, e is closed, hence
$\textit{e}\,\theta=\textit{e}$, and all elements in
$\llbracket{\mathrm{v}},{\sigma^{\prime}}\rrbracket$ have shape
${\mathrm{v}}\,\theta$ with $\theta\in\textsf{Sol}({\sigma^{\prime}})$.

Proof through intermediate semantics In order to prove Theorem 6.11, we
introduce a new semantics called _intermediate_ , defined in Figure 8. Values
are those of the abstract semantics, hence calls are of shape
$\textit{v}.\textit{m}(\overline{\textit{v}})$ (_abstract_ calls). The
judgment has shape
$\textit{e},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$, with
$S,S^{\prime}$ sets of abstract calls, $\rho$ map from abstract calls to
values. Comparing with
$\textit{e},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$ in the
operational semantics, no variables are introduced for calls; $\rho$ and $S$
play the role of the ck and non ck part of $\tau$, respectively, keeping trace
of already encountered calls. Moreover, $\rho$ directly associates to a call
its value to be used in the checking step, which in $\sigma$ is associated to
the corresponding variable. Finally, $S^{\prime}$ plays the role of
${\sigma^{\prime}}$, tracing the calls for which the codefinition has been
evaluated, hence the checking step will be needed. This correspondence is made
precise below. The rules are analogous to those of Figure 6, with the
difference that, for an already encountered call $\mathit{c}\in S$, either
rule (IN-invk-ok) or rule (IN-corec) can be applied. In other words,
evaluation of the codefinition is not necessarily triggered when the _first_
cycle is detected. This non-determinism makes the relation with the abstract
semantics simpler.

$\begin{array}[t]{llll}\textit{v}\in{\cal
V}\textsuperscript{a}&{:}{:}=_{\textsc{co}}&\texttt{new}\
\mathit{C}(\overline{\textit{v}})&\mbox{{\small{possibly infinite object}}}\\\
\mathit{c}&{:}{:}=&\textit{v}.\textit{m}(\overline{\textit{v}})&\mbox{{\small{abstract
call}}}\\\ S&{:}{:}=&\mathit{c}_{1}\ \ldots\ \mathit{c}_{n}\hskip
8.00003pt(n\geq 0)&\mbox{{\small{set of {abstract} calls}}}\\\
\rho&{:}{:}=&\mathit{c}_{1}:\textit{v}_{1}\ldots\mathit{c}_{n}:\textit{v}_{n}\hskip
8.00003pt(n\geq 0)&\mbox{{\small{}}}\\\ \end{array}$

$\begin{array}[]{l}{\tiny\textsc{({IN-
val})}}\displaystyle\frac{}{\textit{v},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset}\
\begin{array}[]{l}\end{array}\hskip 15.00002pt{\tiny\textsc{({IN-
field})}}\displaystyle\frac{\textit{e},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}}{\textit{e}.\mathit{f},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}}\
\begin{array}[]{l}\textit{v}=\texttt{new}\
\mathit{C}(\textit{v}_{1},\ldots,\textit{v}_{n})\\\
\mathit{fields}(\mathit{C})=\mathit{f}_{1}...\mathit{f}_{n}\\\
\mathit{f}=\mathit{f}_{i},i\in 1..n\end{array}\\\\[25.83325pt]
{\tiny\textsc{({IN-
new})}}\displaystyle\frac{\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}\hskip
8.00003pt\forall i\in 1..n}{\texttt{new}\
\mathit{C}(\textit{e}_{1},\ldots,\textit{e}_{n}),\rho,S\\!\Downarrow_{\textsc{IN}}\\!\texttt{new}\
\mathit{C}(\textit{v}_{1},\ldots,\textit{v}_{n}),\bigcup_{i\in
1..n}{S^{\prime}_{i}}}\ \begin{array}[]{l}\end{array}\\\\[21.52771pt] \mbox{In
all the following
rules:}\begin{array}[]{l}\overline{\textit{e}}=\textit{e}_{1},\ldots,\textit{e}_{n}\\\
\overline{\textit{v}}=\textit{v}_{1}\ldots\textit{v}_{n}\\\
\mathit{c}=\textit{v}_{0}.\textit{m}(\overline{\textit{v}})\\\
\textit{v}_{0}=\texttt{new}\ \mathit{C}(\\_)\\\ \end{array}\\\\[30.1388pt]
{\tiny\textsc{({IN-invk-
ok})}}\displaystyle\frac{\begin{array}[]{l}\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}\hskip
8.00003pt\forall i\in 0..n\\\
\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}\end{array}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\bigcup_{i\in
0..n}S^{\prime}_{i}{\cup}S^{\prime}}\ \begin{array}[]{l}{\mathit{c}\not\in
S^{\prime}\ \mbox{or}\ \mathit{c}\in S}\\\
\mathit{mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}}})\end{array}\\\\[30.1388pt]
{\tiny\textsc{({IN-invk-
check})}}\displaystyle\frac{\begin{array}[]{l}\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},{S^{\prime}_{i}}\hskip
8.00003pt\forall i\in 0..n\\\
\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}\\\
\textit{e}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],{\rho}\\{\mathit{c}:\\!\textit{v}\\},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},{S^{\prime\prime}}\end{array}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\bigcup_{i\in
0..n}S^{\prime}_{i}\cup(S^{\prime}\setminus\\{\mathit{c}\\})}\
\begin{array}[]{l}{\mathit{c}\not\in S}\\\
\mathit{mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}}})\\\
\mathit{c}\in S^{\prime}\end{array}\par\\\\[30.1388pt] {\tiny\textsc{({IN-
corec})}}\displaystyle\frac{\begin{array}[]{l}\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}\hskip
8.00003pt\forall i\in 0..n\\\
\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}][u/\texttt{any}],\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}\end{array}}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\bigcup_{i\in
0..n}S^{\prime}_{i}\cup S^{\prime}\cup\\{\mathit{c}\\}}\
\begin{array}[]{l}\mathit{c}\in S\\\ \textit{co-
mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}^{\prime}}})\\\
\mathit{c}\not\in\mathit{dom}(\rho)\end{array}\\\\[30.1388pt]
{\tiny\textsc{({IN-look-
up})}}\displaystyle\frac{\textit{e}_{i},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},S^{\prime}_{i}\hskip
8.00003pt\forall i\in
0..n}{\textit{e}_{0}.\textit{m}(\overline{\textit{e}}),\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\bigcup_{i\in
0..n}S^{\prime}_{i}}\
\begin{array}[]{l}\rho(\mathit{c})=\textit{v}\end{array}\end{array}$

Figure 8: $\coFJ$ intermediate semantics

By relying on the intermediate semantics, we can prove Theorem 6.11 by two
steps:

  1. 1.

The operational semantics is sound w.r.t. the intermediate semantics (Theorem
6.14).

  2. 2.

The intermediate semantics is sound w.r.t. the abstract semantics (Theorem
6.16).

At the beginning of Section 4, we mentioned two issues for an operational
semantics: representing infinite objects in a finite way, and replacing
infinite (regular) proof trees by finite proof trees. This proof technique
nicely shows that the two issues are orthogonal: notably, detection of cyclic
calls is independent from the format of values.

To express the soundness of the operational semantics w.r.t. the intermediate
one, we need to formally relate the two judgments. First of all, a call trace
$\tau$ is the disjoint union of two maps $\tau^{\textsf{ck}}$ and
$\tau^{\neg\textsf{ck}}$ into tagged and non-tagged variables, respectively.
Then, given an environment $\sigma$, we define the following sets of
(operational) calls:

  * •

$S^{\tau}=\mathit{dom}(\tau^{\neg\textsf{ck}})$

  * •

$S^{\tau,\sigma}=\mathit{dom}(\sigma\circ\tau^{\neg\textsf{ck}})$, where
$\circ$ is the composition of partial functions

  * •

$S^{\tau,\sigma,\sigma^{\prime}}=S^{\tau,\sigma^{\prime}}\setminus
S^{\tau,\sigma}$

For $S$ set of calls and $\theta$ substitution, we abbreviate by $S_{\theta}$
the set of abstract calls $S\,\theta$. Note that
$S^{\tau,\sigma}_{\theta}\subseteq S^{\tau}_{\theta}$ and, if
$\sigma_{1}\leq\sigma_{2}$, then $S^{\tau,\sigma_{1}}_{\theta}\subseteq
S^{\tau,\sigma_{2}}_{\theta}$. Finally,
$\rho^{\tau}_{\theta}(\mathit{c}\,\theta)=\textit{v}$ iff
$\textit{v}=\theta(\tau^{\textsf{ck}}(\mathit{c}))$.

Then, the soundness result can be stated as follows:

######  Theorem 6.14 (Soundness operational w.r.t. intermediate).

If $\textit{e},\sigma,\tau\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$
then, for all $\theta\in\textsf{Sol}(\sigma^{\prime})$, there exists $S$ such
that $S^{\tau,\sigma,\sigma^{\prime}}_{\theta}\subseteq S\subseteq
S^{\tau,\sigma^{\prime}}_{\theta}$ and,
$\textit{e}\,\theta,\rho^{\tau}_{\theta},S^{\tau}_{\theta}\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}\,\theta,S$.

In particular, the bounds on $S$ ensure that it is empty when
$\tau=\emptyset$. Hence, if
$\textit{e},\sigma,\emptyset\\!\Downarrow\\!{\mathrm{v}},{\sigma^{\prime}}$
(hypothesis of Theorem 6.11), then
$\textit{e}\,\theta,\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!{\mathrm{v}}\,\theta,\emptyset$,
that is, the hypothesis of Theorem 6.16 below holds.

The proof of the theorem uses the following corollary of Lemma 6.9.

######  Corollary 6.15.

If
$({{{\mathrm{v}}_{1}},{\sigma_{1}}}){\approx}({{{\mathrm{v}}_{2}},{\sigma_{2}}})$,
$\theta_{1}{\in}\textsf{Sol}(\sigma_{1})$, $\sigma_{1}\leq\sigma_{2}$, then
there is $\theta_{2}\in\textsf{Sol}(\sigma_{2})$ such that
${\mathrm{v}}_{1}\,\theta_{1}={\mathrm{v}}_{2}\,\theta_{2}$ and, for all
$x\in\mathit{dom}(\sigma_{1})$, $\theta_{1}(x)=\theta_{2}(x)$. Moreover, if
$\sigma_{1}=\sigma_{2}$, then
${\mathrm{v}}_{1}\,\theta_{1}={\mathrm{v}}_{2}\,\theta_{1}$.

We now state the second step of the proof: the soundness result of the
intermediate semantics with respect to the abstract semantics.

######  Theorem 6.16 (Soundness intermediate w.r.t. abstract).

If
$\textit{e},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$,
then $({{{\cal I}_{\scriptscriptstyle\textsc{FJ}}},{{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}}})\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$.

The proof uses the bounded coinduction principle (Theorem 1.1), and requires
some lemmas. Recall that ${\cal I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$
means that the judgment $\textit{e}\\!\Downarrow\\!\textit{v}$ has a finite
proof tree in the (standard) inference system consisting of FJ rules and
$\coFJ$ corules.

######  Lemma 6.17.

If $\textit{e},\emptyset,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
then ${\cal I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$
holds.

######  Lemma 6.18.

If
$\textit{e},\rho,S\cup\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
holds, and ${\mathit{c}\not\in S^{\prime}}$, then
$\textit{e},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.

######  Lemma 6.19.

If
$\textit{e},{\rho}\\{\mathit{c}:\\!\textit{v}^{\prime}\\},S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$
and
$\mathit{c},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v}^{\prime},\emptyset$,
then $\textit{e},\rho,S\\!\Downarrow_{\textsc{IN}}\\!\textit{v},S^{\prime}$.

We can now prove Theorem 6.16.

######  Proof 6.20 (Proof of Theorem 6.16).

We take as specification the set
$A=\\{({{\textit{e}},{\textit{v}}})\mid\textit{e},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset\\}$,
and we use bounded coinduction (Theorem 1.1). We have to prove the following:

Boundedness

For all $({{\textit{e}},{\textit{v}}})\in A$, ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}{\cup}{\cal
I}^{co}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!\textit{v}}$
holds.

Consistency

For all $({{\textit{e}},{\textit{v}}})\in A$, there exist a rule in the
abstract semantics having $\textit{e}\\!\Downarrow\\!\textit{v}$ as
consequence, and such that all its premises are elements of $A$.

Boundedness follows immediately from Lemma 6.17. We now prove consistency.

Consider a pair $({{\textit{e}},{\textit{v}}})\in A$, hence we know that
$\textit{e},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$
is derivable. We proceed by case analysis on the last applied rule in the
derivation of this judgement.

(IN-val)

We know that $\textit{e}=\textit{v}=\texttt{new}\
\mathit{C}(\textit{v}_{1},\ldots,\textit{v}_{n})$. We choose as candidate rule
(abs-new). We have to show that, for all $i\in 1..n$,
$({{\textit{v}_{i}},{\textit{v}_{i}}})\in A$, that is,
$\textit{v}_{i},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},\emptyset$
holds We can get the thesis thanks to rule (IN-val).

(IN-field)

We know that $\textit{e}=\textit{e}^{\prime}.\mathit{f}$ and
$\textit{e}^{\prime},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\texttt{new}\
\mathit{C}(\textit{v}_{1}\ldots\textit{v}_{n}),\emptyset$. We choose as
candidate rule (abs-field), with conclusion
$\textit{e}^{\prime}.\mathit{f}\\!\Downarrow\\!\textit{v}_{i}$. We have to
show that $({{\textit{e}^{\prime}},{\texttt{new}\
\mathit{C}(\textit{v}_{1}\ldots\textit{v}_{v})}})\in A$, that is,
$\textit{e}^{\prime},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\texttt{new}\
\mathit{C}(\textit{v}_{1}\ldots\textit{v}_{v}),\emptyset$ holds, but this is
true by hypothesis.

(IN-new)

We know that
$\textit{e}_{i},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},\emptyset$
holds for all $i\in 1..n$. We choose as candidate rule (abs-new). We have to
show that, for all $i\in 1..n$, $({{\textit{e}_{i}},{\textit{v}_{i}}})\in A$,
that is,
$\textit{e}_{i},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},\emptyset$
holds, but this is true by hypothesis.

(IN-invk-ok)

We know that $\textit{e}=\textit{e}_{0}.\textit{m}(\overline{\textit{e}})$,
$\textit{e}_{i},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},\emptyset$
holds for all $i\in 0..n$,
$\mathit{c}=\textit{v}_{0}.\textit{m}(\overline{\textit{v}})$,
$\mathit{mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}^{\prime}}})$,
and
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\emptyset,\\{\mathit{c}\\}\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$
holds. We choose as candidate rule (abs-invk). We have to show that, for all
$i\in 0..n$, $({{\textit{e}_{i}},{\textit{v}_{i}}})\in A$, and
$({{\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}]},{\textit{v}}})\in
A$. That is, that the following judgments hold:
$\textit{e}_{i},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},\emptyset$
for all $i\in 0..n$, and
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$.
The judgments in the first set hold by hypothesis. The last judgment holds
thanks to Lemma 6.18, where $S^{\prime}=\emptyset$.

(IN-invk-check)

We know that $\textit{e}=\textit{e}_{0}.\textit{m}(\overline{\textit{e}})$,
$\textit{e}_{i},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},\emptyset$
holds for all $i\in 0..n$,
$\mathit{c}=\textit{v}_{0}.\textit{m}(\overline{\textit{v}})$,
$\mathit{mbody}(\mathit{C},\textit{m})=({{\overline{\textit{x}}},{\textit{e}^{\prime}}})$,
and
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],{}\\{\mathit{c}:\\!\textit{v}\\},\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$
holds. We choose as candidate rule (abs-invk). We have to show that for all
$i\in 0..n$, $({{\textit{e}_{i}},{\textit{v}_{i}}})\in A$, and
$({{\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}]},{\textit{v}}})\in
A$. That is, that the following judgments hold:
$\textit{e}_{i},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v}_{i},\emptyset$
for all $i\in 0..n$, and
$\textit{e}^{\prime}[\textit{v}_{0}/\texttt{this}][\overline{\textit{v}}/\overline{\textit{x}}],\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$.
The judgments in the first set hold by hypothesis. The last judgment holds
thanks to Lemma 6.19, since from the hypothesis we easily get
$\mathit{c},\emptyset,\emptyset\\!\Downarrow_{\textsc{IN}}\\!\textit{v},\emptyset$.

(IN-corec)

Empty case since to apply the rule it should be $S\neq\emptyset$.

(IN-look-up)

Empty case since to apply the rule it should be $\rho\neq\emptyset$.

##  7 Related work

As already mentioned, the idea of regular corecursion (keeping track of
pending method calls, so to detect cyclic calls), originates from co-SLD
resolution [20, 21, 7]. Making regular corecursion _flexible_ means that the
programmer can specify the behaviour in case a cycle is detected. Language
constructs to achieve such flexibility have been proposed in the logic [2, 3],
functional [17], and object-oriented [8, 9] paradigm.

Logic paradigm The above mentioned _co-SLD resolution_ [20, 21, 7] is a sound
resolution procedure based on cycle detection. That is, the interpreter keeps
track of resolved atoms and an atom selected from the current goal can be
resolved if it unifies with an atom that has been already resolved. In this
way it is possible to define coinductive predicates. Correspondingly, models
are subsets of the _complete Herbrand basis_ , that is, the set of ground
atoms built on arbitrary (finite or infinite) terms, and the declarative
semantics is the greatest fixed point of the monotone function associated with
a program. Structural resolution [18, 14] (a.k.a. S-resolution) is a proposed
generalization for cases when formulas computable at infinity are not regular;
infinite derivations that cannot be built in finite time are generated lazily,
and only partial answers are shown. More recently, a comprehensive theory has
been proposed [11] to provide operational semantics that go beyond loop
detection.

Anyway, in coinductive logic programming, only standard coinduction is
supported. The notion of finally clause, introduced in [2], allows the
programmer to specify a fact to be resolved when a cycle is detected, instead
of simply accepting the atom. The approach has been refined in [3], following
the guidelines given by the formal framework of generalized inference systems.
That is, the programmer can write special clauses corresponding to corules, so
that, when an atom is found for the second time, standard SLD resolution is
triggered in the program enriched by the corules. However, this paradigm is
very different from the object-oriented one, since based on relations rather
than functions: cycles are detected on the same atom, where input and output
are not distinguished, by unification.

Functional paradigm _CoCaml_ (www.cs.cornell.edu/Projects/CoCaml) [17, 16] is
a fully-fledged extension of OCaml supporting non-well-founded data types and
corecursive functions. CoCaml, as OCaml, allows programmers to declare regular
values through the let-rec construct, and, moreover, detects cyclic calls as
in our approach. However, whereas $\coFJ$ immediately evaluates the cyclic
call by using the codefinition, the CoCaml approach is in two phases. First, a
system of equations is constructed, associating with each call a variable and
partially evaluating the body of functions, where calls are replaced with
associated variables. Then, the system of equations is given to a _solver_
specified in the function definition. Solvers can be either pre-defined or
written by the programmer in order to enhance flexibility. An advantage that
we see in our approach is that the programmer has to write the codefinition
(standard code) rather than working at the meta-level to write a solver, which
is in a sense a fragment of the interpreter. A precise comparison is difficult
for the lack of a simple operational model of the CoCaml mechanism. In future
work, we plan to develop such model, and to relate the two approaches on a
formal basis.

Object-oriented paradigm A previous version of $\coFJ$ has been proposed in
[8]. At this time, however, the framework of inference systems with corules
was still to come, so there was no formal model against which to check the
given operational semantics, which, indeed, derived spurious results in some
cases, as illustrated in Section 4 at page 5. The operational semantics
provided in the current paper solves this problem, and is proved to be sound
with respect to the abstract semantics. Moreover, we adopt a simpler
representation of cyclic objects through capsules [16]. A type system has been
proposed [9] for the previous version of $\coFJ$ to prevent _unsafe_ use of
the “undetermined” value. We leave to further work the investigation of typing
issues for the approach presented in this paper.

##  8 Conclusion

The Java-like calculus presented in this paper promotes a novel programming
style, which smoothly incorporates support for cyclic data structures and
coinductive reasoning, in the object-oriented paradigm. Our contribution is
foundational: we provide an abstract semantics based on corules and show that
it is possible to define a _sound_ operational model; such operational
semantics is inductive, syntax-directed and deterministic, hence can be
directly turned into an interpreter. In order to get a “real-world” language,
of course many other issues should be taken into account.

Our prototype implements the _abstract_ semantics on top of a Prolog meta-
interpreter supporting flexible regular corecursion [3]. In this way, the
inference system is naturally translated in Prolog121212A logic program can be
seen as an inference system where judgments are atoms., cyclic terms are
natively supported, and their equality handled by unification. A fully-fledged
interpreter of the _operational_ semantics should directly handle these issues
and, moreover, attempt at some optimization.

The current paper does not deal with types: an important concern is to
guarantee _type soundness_ , statically ensuring that an undetermined value
never occurs as receiver of field access or method invocation, as investigated
in [9] for the previous $\coFJ$ version [8].

Another issue is how to train developers to write codefinitions. Standard
recursion is non-trivial as well for beginners, whereas it becomes quite
natural after understanding its mechanism. For regular corecursion the same
holds, with is the additional difficulty of reasoning on infinite structures.
Intuitively, the codefinition can be regarded as a base case to be applied
when a loop is detected. Moreover, again as for standard recursion, this novel
programming style could be integrated with proof techniques to show the
correctness of algorithms on cyclic data structures. Such proofs could be
mechanized in proof assistants, as Agda, that provide built-in support for
coinductive definitions and proofs by coinduction.

Finally, a non-trivial challenge is how to integrate regular corecursion,
requiring to detect “the same call”, with the notion of mutable state. Likely,
some immutability constraints will be needed, or a variant of the model where
such a check requires a stateless computation. Another solution is to consider
the check as an assertion that can be disabled if the programmer has verified
the correctness of the method by hand or assisted by a tool.

The semantics of flexible regular corecursion in the paper is the operational
counterpart of that obtained by considering recursive functions as relations,
and recursive definitions (with codefinition) as inference systems (with
corules). We prove that the operational semantics is _sound_ with respect to
that interpretation. Obviously, _completeness_ does not hold in general, since
the abstract semantics deals with not only cyclic data structures (such as
$[2,1]^{\omega}$), but arbitrary non-well-founded structures (such as the list
of natural numbers). Even considering only regular proof trees in the abstract
semantics, in some subtle cases there is more than one admissible
result131313For instance, the list with no repetitions extracted from
$[1,2]^{\omega}$ can be either $[1,2]$ or $[2,1]$. , whereas the operational
semantics, being deterministic, finds “the first” among such results, as
reasonable in an implementation. We plan to investigate such completeness
issues in further work, also in the more general framework of inference
systems, that is, to characterize judgments which have a regular proof tree.

We also plan to study how to deal with flexible corecursion in other
programming paradigms, notably in the functional paradigm, and to compare on a
formal basis this approach with the CoCaml approach relying on solvers, rather
than codefinitions.

As already discussed in the Introduction, lazy evaluation and regular
corecursion are complementary approaches to deal with infinite data
structures. With the lazy approach, arbitrary (computable) non-well-founded
data structures are supported. However, we cannot compute results which need
to explore the whole structure, whereas, with regular corecursion, this
becomes possible for cyclic structures: for instance we can compute allPos
one_two, which diverges in Haskell. A natural question is then whether it is
possible to extend the regular corecursion approach to manage also non-regular
objects, thus overcoming the principal drawback with respect to the lazy
approach. A possible interesting direction, exploiting the work of Courcelle
[12] on infinite trees, could be to move from regular to _algebraic_ objects.

## References

  * [1] P. Aczel.  An introduction to inductive definitions.  In Handbook of Mathematical logic. North Holland, 1977.
  * [2] Davide Ancona.  Regular corecursion in Prolog.  Computer Languages, Systems & Structures, 39(4):142–162, 2013\.
  * [3] Davide Ancona, Francesco Dagnino, and Elena Zucca.  Extending coinductive logic programming with co-facts.  In Ekaterina Komendantskaya and John Power, editors, First Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty’16, volume 258 of Electronic Proceedings in Theoretical Computer Science, pages 1–18. Open Publishing Association, 2017.  doi:10.4204/EPTCS.258.1.
  * [4] Davide Ancona, Francesco Dagnino, and Elena Zucca.  Generalizing inference systems by coaxioms.  In Hongseok Yang, editor, 26th European Symposium on Programming, ESOP 2017, volume 10201 of Lecture Notes in Computer Science, pages 29–55. Springer, 2017.  doi:10.1007/978-3-662-54434-1_2.
  * [5] Davide Ancona, Francesco Dagnino, and Elena Zucca.  Reasoning on divergent computations with coaxioms.  PACMPL, 1(OOPSLA):81:1–81:26, 2017.
  * [6] Davide Ancona, Francesco Dagnino, and Elena Zucca.  Modeling infinite behaviour by corules.  In ECOOP’18 - Object-Oriented Programming, pages 21:1–21:31, 2018\.
  * [7] Davide Ancona and Agostino Dovier.  A theoretical perspective of coinductive logic programming.  Fundamenta Informaticae, 140(3-4):221–246, 2015.
  * [8] Davide Ancona and Elena Zucca.  Corecursive Featherweight Java.  In FTfJP’12 - Formal Techniques for Java-like Programs, pages 3–10. ACM Press, 2012.
  * [9] Davide Ancona and Elena Zucca.  Safe corecursion in coFJ.  In FTfJP’13 - Formal Techniques for Java-like Programs, page 2. ACM Press, 2013.
  * [10] Pietro Barbieri, Francesco Dagnino, Elena Zucca, and Davide Ancona.  Corecursive Featherweight Java revisited.  In Alessandra Cherubini, Nicoletta Sabadini, and Simone Tini, editors, ICTCS’19 - Italian Conf. on Theoretical Computer Science, volume 2504 of CEUR Workshop Proceedings, pages 158–170. CEUR-WS.org, 2019.  URL: http://ceur-ws.org/Vol-2504/paper19.pdf.
  * [11] Henning Basold, Ekaterina Komendantskaya, and Yue Li.  Coinduction in uniform: Foundations for corecursive proof search with Horn clauses.  In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, pages 783–813, 2019.
  * [12] B. Courcelle.  Fundamental properties of infinite trees.  Theoretical Computer Science, 25:95–169, 1983.
  * [13] Francesco Dagnino.  Coaxioms: flexible coinductive definitions by inference systems.  Logical Methods in Computer Science, 15(1), 2019.  URL: https://lmcs.episciences.org/5277.
  * [14] E.Komendantskaya et al.  A productivity checker for logic programming.  Post-proc. LOPSTR’16, 2017.  URL: http://arxiv.org/abs/1608.04415.
  * [15] Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler.  Featherweight Java: A minimal core calculus for Java and GJ.  In ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1999, pages 132–146. ACM Press, 1999.  doi:10.1145/320384.320395.
  * [16] Jean-Baptiste Jeannin and Dexter Kozen.  Computing with capsules.  Journal of Automata, Languages and Combinatorics, 17(2-4):185–204, 2012.  doi:10.25596/jalc-2012-185.
  * [17] Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva.  Cocaml: Functional programming with regular coinductive types.  Fundamenta Informaticae, 150:347–377, 2017.
  * [18] E. Komendantskaya et al.  Coalgebraic logic programming: from semantics to implementation.  J. Logic and Computation, 26(2):745, 2016.  doi:10.1093/logcom/exu026.
  * [19] X. Leroy and H. Grall.  Coinductive big-step operational semantics.  Information and Computation, 207(2):284–304, 2009.
  * [20] L. Simon.  Extending logic programming with coinduction.  PhD thesis, University of Texas at Dallas, 2006.
  * [21] L. Simon, A. Bansal, A. Mallya, and G. Gupta.  Co-logic programming: Extending logic programming with coinduction.  In ICALP 2007, pages 472–483, 2007.

##  Appendix A Proofs

######  Proof A.1 (Proof of Lemma 4.12).

The proof is by induction on the definition of
$\textit{e},\emptyset,\tau\\!\Downarrow\\!{\mathrm{v}},\emptyset$.

(val)

By hypothesis $({{{\mathrm{v}}},{\emptyset}})$ is a capsule, then, since the
environment is empty, ${\mathrm{v}}$ is a closed FJvalue, hence, we can prove
by induction on ${\mathrm{v}}$ that ${{\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{v}\\!\Downarrow\\!\textit{v}}}$.

(field)

By hypothesis we have
$\textit{e},\emptyset,\tau\\!\Downarrow\\!{\mathrm{v}},\emptyset$, with
$\mathit{unfold}({\mathrm{v}},\emptyset)={\mathrm{v}}=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1},\ldots,{\mathrm{v}}_{n})$ and $n\geq 1$, then we
get ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}\\!\Downarrow\\!{\mathrm{v}}}$
by induction hypothesis. Hence we get the thesis by rule (FJ-field).

(new)

By hypothesis, we have
$\textit{e}_{i},\emptyset,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},\sigma^{\prime}_{i}$,
for all $i\in 1..n$. Since $\bigsqcup_{i\in
1..n}\sigma^{\prime}_{i}=\emptyset$, we have $\sigma^{\prime}_{i}=\emptyset$
for all $i\in 1..n$, hence, by induction hypothesis, we get ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}_{i}\\!\Downarrow\\!{\mathrm{v}}_{i}}$.
Then, we get the thesis by rule (FJ-new).

(invk-ok)

By hypothesis we have
$\textit{e}_{i},\emptyset,\tau\\!\Downarrow\\!{\mathrm{v}}_{i},\sigma^{\prime}_{i}$
for all $i\in 0..n$, and
$\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}],{\widehat{\sigma}},{{\tau}\\{\mathit{c}:\\!\textit{x}\\}}\\!\Downarrow\\!{\mathrm{v}},\emptyset$.
Then, by Lemma 6.13, we get ${\widehat{\sigma}}\leq\emptyset$, thus
${\widehat{\sigma}}=\emptyset$, and, since
$\sigma^{\prime}_{i}\leq{\widehat{\sigma}}$, for all $i\in 0..n$, by
definition, we also get $\sigma^{\prime}_{i}=\emptyset$ for all $i\in 0..n$.
Therefore, by induction hypothesis, we get ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}_{i}\\!\Downarrow\\!{\mathrm{v}}_{i}}$,
for all $i\in 0..n$, and ${\cal
I}_{\scriptscriptstyle\textsc{FJ}}\\!\vdash\\!{\textit{e}[{\mathrm{v}}_{0}/\texttt{this}][\overline{{\mathrm{v}}}/\overline{\textit{x}}]\\!\Downarrow\\!{\mathrm{v}}}$,
hence, we get the thesis by rule (FJ-invk).

(invk-check)

This case is empty since to apply the rule it should be
${{\sigma^{\prime}}}\\{\textit{x}:\\!{\mathrm{v}}\\}\neq\emptyset$.

(corec)

This case is empty since to apply the rule it should be
${{\sigma^{\prime}}}\\{\textit{x}:\\!\textit{x}\\}\neq\emptyset$.

(look-up)

This case is empty since to apply the rule it should be $\sigma\neq\emptyset$,
while $\textit{x}\in\mathit{dom}(\sigma)$.

######  Proof A.2 (Proof of Prop. 6.2).

  1. 1.

If $\mathit{unfold}({\mathrm{v}},\sigma)\uparrow$, then trivially
${\mathrm{v}}=\textit{x}$ and
$\mathit{unfold}(\sigma(\textit{x}),\sigma)\uparrow$. Hence, by definition of
$\stackrel{{\scriptstyle\sigma}}{{\leftrightarrow}}$, we get the thesis.

  2. 2.

If x is a free variable in $\mathit{T}({\mathrm{v}},\sigma)$, then by
definition of tree expansion we have
$\mathit{unfold}(\textit{x},\sigma)\uparrow$, hence the thesis follows by 1.

  3. 3.

It is enough to show that, if $\sigma(x)=y$, then $\theta(x)=\theta(y)$, and
this is true as $\theta(x)=\sigma(x)\,\theta=\theta(y)$, since
$\theta\in\textsf{Sol}(\sigma)$.

  4. 4.

We know that either ${\mathrm{v}}=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1},\ldots,{\mathrm{v}}_{n})$ or
${\mathrm{v}}=\textit{x}$ and $\sigma^{n}(\textit{x})=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1},\ldots,{\mathrm{v}}_{n})$. In the former case, the
thesis is immediate. In the latter, it follows by induction on $n$, since
$\textit{x}\,\theta=\theta(\textit{x})=\sigma(\textit{x})\,\theta$, as
$\theta\in\textsf{Sol}(\sigma)$.

  5. 5.

The proof is by coinduction. If
$\mathit{unfold}({\mathrm{v}},\sigma)\uparrow$, then
${\mathrm{v}}=\textit{x}\in\mathit{dom}(\sigma)$,
$\mathit{T}(\textit{x},\sigma)=\textit{x}$ hance the thesis is immeidate. If
$\mathit{unfold}({\mathrm{v}},\sigma)=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1},\ldots,{\mathrm{v}}_{n})$, then
$\mathit{T}({\mathrm{v}},\sigma)=\texttt{new}\
\mathit{C}(\mathit{T}({\mathrm{v}}_{1},\sigma),\ldots,\mathit{T}({\mathrm{v}}_{n},\sigma))$.
If ${\mathrm{v}}\,\theta=\mathit{T}({\mathrm{v}},\sigma)\,\theta$, since by
point 4 we have ${\mathrm{v}}\,\theta=\texttt{new}\
\mathit{C}({\mathrm{v}}_{1}\,\theta,\ldots,{\mathrm{v}}_{n}\,\theta)$ and, by
definition, $\mathit{T}({\mathrm{v}},\sigma)\,\theta=\texttt{new}\
\mathit{C}(\mathit{T}({\mathrm{v}}_{1},\sigma)\,\theta,\ldots,\mathit{T}({\mathrm{v}}_{n},\sigma)\,\theta)$,
hence we get
${\mathrm{v}}_{i}\,\theta=\mathit{T}({\mathrm{v}}_{i},\sigma)\,\theta$ for all
$i\in 1..n$, as needed.

######  Proof A.3 (Proof of Lemma 6.5).

We first prove that
$\llbracket{\mathrm{v}}_{2},\sigma_{2}\rrbracket\subseteq\llbracket{\mathrm{v}}_{1},\sigma_{1}\rrbracket$.
Let $\theta_{2}\in\textsf{Sol}(\sigma_{2}$. We have to find
$\theta_{1}\in\textsf{Sol}(\sigma_{1})$ such that
${\mathrm{v}}_{2}\,\theta_{2}={\mathrm{v}}_{1}\,\theta_{1}$. We define a
regular system of equations, with variables in $\mathit{dom}(\sigma_{1})$,
which is finite by definition, as follows:

$s(x)=\begin{cases}\theta_{2}(y)&\exists
x^{\prime}\in\mathit{undet}(\sigma_{1}).x\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x^{\prime}\text{
and }x^{\prime}\alpha y\\\ \sigma_{1}(x)&\text{otherwise}\end{cases}$

The system is well-defined because, if there are
$x_{1},x_{2}\in\mathit{undet}(\sigma_{1})$ such that
$x\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x_{1}$,
$x\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x_{2}$, $x_{1}\alpha
y_{1}$ and $x_{2}\alpha y_{2}$, then
$x_{1}\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}x_{2}$, since
$\stackrel{{\scriptstyle\sigma_{1}}}{{\leftrightarrow}}$ is an equivalence
relaition, thus
$y_{1}\stackrel{{\scriptstyle\sigma_{2}}}{{\leftrightarrow}}y_{2}$, as
$\alpha$ is a $\sigma_{1},\sigma_{2}$-renaming; hence, by Prop. 6.2(3), we
have $\theta_{2}(y_{1})=\theta_{2}(y_{2})$. By results in [12], there exists a
solution $\theta_{1}$ of $s$, we now show that
$\theta_{1}\in\textsf{Sol}(\sigma_{1})$, that is, for all
$x\in\mathit{dom}(\sigma_{1})$, $\theta_{1}(x)=\sigma_{1}(x)\,\theta_{1}$.
There are two cases: if there is $x^{\prime}\in\mathit{undet}(\sigma_{1})$