1

# Formalizing $\varphi$-calculus: a purely object-oriented calculus of
decorated objects

Nikolai Kudasov  0000-0001-6572-7292 Innopolis UniversityUniversitetskaya
1InnopolisTatarstan Republic420500Russia<EMAIL_ADDRESS>and  Violetta
Sim  Innopolis UniversityUniversitetskaya 1InnopolisTatarstan
Republic420500Russia<EMAIL_ADDRESS>
###### Abstract.

Many calculi exist for modelling various features of object-oriented
languages. Many of them are based on $\lambda$-calculus and focus either on
statically typed class-based languages or dynamic prototype-based languages.
We formalize untyped calculus of decorated objects, informally presented by
Bugayenko, which is defined in terms of _objects_ and relies on _decoration_
as a primary mechanism of object extension. It is not based on
$\lambda$-calculus, yet with only four basic syntactic constructions is just
as complete. We prove the calculus is confluent (i.e. possesses Church-Rosser
property), and introduce an abstract machine for call-by-name evaluation.
Finally, we provide a sound translation to $\lambda$-calculus with records.

models of computation, $\varphi$-calculus, object-oriented programming

††conference: ACM SIGPLAN Conference on Programming Languages; January 01–03,
2018; New York, NY, USA††journalyear: 2018††doi: ††copyright: none††ccs:
Theory of computation Models of computation

##  1\. Introduction

Formalizing object-oriented features of programming languages is an old but
still vibrant topic in computer science (Black and Palsberg, 1994).
Researchers have extended many specification languages, such as Z notation, to
support object-oriented concepts to some degree (Smith, 2000). Similarly,
modelling languages, such as VDM, have been extended (Durr and Van Katwijk,
1992) to support classes, objects and a certain notion of inheritance. Later,
Wolczko (Wolczko and Jones, 1988) used VDM++ notation to define semantics of
object-oriented languages.

At the same time, models based on $\lambda$-calculus have also been studied.
Pierce and Turner have introduced type-theoretic foundations for object-
oriented programming (Pierce and Turner, 1993). Fisher et al. (Fisher et al.,
1993) have introduced $\lambda$-calculus with object primitives able to
express the capabilities of delegation-based object-oriented languages where
an object is created from another one, inheriting properties of the original.
Abadi and Cardelli introduced $\lambda$-calculus with primitive objects (Abadi
and Cardelli, 1996). $\varsigma$-calculus relies on external memory to store
and modify the states of objects. The calculus has a sound type system with
basic subtyping via subsumption. The work has been expanded in (Abadi and
Cardelli, 1994) with $\text{{FOb}}_{<:\mu}$ calculus which is an extension of
System F (Girard et al., 1989, Chapter 11). Clarke et al. have continued this
line of research (Clarke et al., 2001) presenting an object calculus based on
“ownership types” adding object ownership and nesting between objects. Wand
has proposed a type system with row types and row polymorphism to facilitate
type inference in object-oriented languages, modelled by $\lambda$-calculus
with records (Wand, 1991). In (Ciaffaglione et al., 2021) Ciaffaglione et al.
have introduced $\lambda\mathcal{O}bj^{\oplus}$ system based on
$\lambda$-calculus, with objects that can modify their interface upon
receiving a message. The calculus is intended to model object evolution in
prototype-based languages such as JavaScript.

The above models differ in their approach to subtyping and subclasses, but
rely significantly on $\lambda$-calculus as their foundation. At the same
time, many modern programming languages do not properly support
$\lambda$-abstraction. For example, Java provides lambda expressions which are
essentially instances of anonymous classes with a single method.

When modelling object-oriented languages some formalizations focus on
statically typed class-based languages (Pierce and Turner, 1993; Abadi and
Cardelli, 1996; Wand, 1991) while others prefer prototype-based approach
(Ciaffaglione et al., 2021).

Bugayenko (Bugayenko, 2021a) introduced programming language EO and its
semantics in terms of an informally specified calculus which he called
$\varphi$-calculus. To the best of our knowledge, his work is the only attempt
to introduce an object-oriented calculus that incorporates Decorator pattern
(Gamma et al., 1995, Chapter 4) as the mechanism of extending objects.
Bugayenko’s paper expresses interesting ideas, but suffers from inaccuracies
and insufficient formalization of the calculus, as the paper lacks reduction
semantics and any soundness results. His paper also uses custom terminology
that conflicts the established conventions in the computer science literature.

In this paper, we extract the key ideas from Bugayenko’s paper and formalize
$\varphi$-calculus, a calculus of objects with decoration as the main
mechanism for object extension, in a more formal way. Moreover, our
interpretation of $\varphi$-calculus is not based on $\lambda$-calculus, so
object methods are also represented as objects.

In contrast with Bugayenko’s work, we focus on the object-oriented core of the
calculus, and do not introduce primitives such as numbers, booleans, mutable
memory. Similarly to $\lambda$-calculus, these primitives can either be added
via a straightforward extension, or by using an encoding, such as Church
numerals. We leave details of such extensions and encodings outside the scope
of this paper.

Our specific contributions are the following:

  * •

We present syntax and introduce reduction semantics of $\varphi$-calculus, a
calculus of objects with decoration.

  * •

We prove that $\varphi$-calculus possesses Church-Rosser property.

  * •

We define normal order evaluation of $\varphi$-terms and prove its
completeness, i.e. any term will be reduced to its normal form under such
evaluation order, whenever the normal form exists.

  * •

We define an abstract machine for call-by-name evaluation of $\varphi$-terms.

  * •

We introduce translation to $\lambda$-calculus with records and prove this
translation to be sound.

  * •

We show how to extend $\varphi$-calculus with primitives and mutable
references.

##  2\. Calculus of decorated objects

In this section, we introduce syntax and evaluation rules, providing the
intuition behind those. The central concept in $\varphi$-calculus is that of
an object. In fact, every term in $\varphi$-calculus is essentially an object.

###### Definition 2.1.

Assuming a set of labels $\mathcal{L}$ and a set of terms $T$, an _object_ $X$
is a mapping from $\mathcal{L}$ to $T\cup\\{\varnothing,\bot\\}$. The labels
that map to $\bot$ are called _missing_ , the labels that map to $\varnothing$
are called _void attributes_ of $X$ and labels that map to terms are called
_attached attributes_ of $X$. Void and attached attributes of $X$ are
collectively called _attributes_ of $X$ and are denoted
$\operatorname{\mathsf{attr}}(X)\subseteq\mathcal{L}$.
An object with an non-empty set of void attributes is called _abstract_.
Otherwise an object is called _concrete_.

###### Example 2.2.

A constant mapping from $\mathcal{L}$ to $\bot$ is an _empty object_ and is
denoted $\llbracket\rrbracket$.

###### Example 2.3.

Let $t_{1},t_{2}$ be terms. Then the following is an object:

$\displaystyle X$ $\displaystyle:\mathcal{L}\to T\cup\\{\varnothing,\bot\\}$
$\displaystyle x$ $\displaystyle\mapsto\varnothing;y\mapsto
t_{1};z\mapsto\llbracket\rrbracket;\ell\mapsto\bot$

For convenience we will denote objects by listing void and attached attributes
inside double brackets. For example, the object from Example 2.3 can be
written succinctly as $\llbracket x\mapsto\varnothing,y\mapsto
t_{1},z\mapsto\llbracket\rrbracket\rrbracket$.

###  2.1. Syntax

The entire syntax of $\varphi$-calculus has only four syntactic constructions:

###### Definition 2.4.

Let $\mathcal{L}$ be the set of attribute names extended with _decorator
attribute_ $\varphi$. Then the set of $\varphi$-terms $T$ is defined
inductively as following:

  1. (1)

if $n\in\mathbb{N}$ then $\rho^{n}\in T$; here $\rho$ is merely a symbol used
in the syntax, it is not a variable or a meta variable;

  2. (2)

if $t\in T$ and $a\in\mathcal{L}$ then $t.a\in T$;

  3. (3)

if $t,u\in T$ and $a\in\mathcal{L}$ then $t(a\mapsto u)\in T$;

  4. (4)

if $t_{1},\ldots,t_{n}\in T$ and
$a_{1},\ldots,a_{k},b_{1},\ldots,b_{n}\in\mathcal{L}$ then $\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots b_{n}\mapsto t_{n}\rrbracket\in T$.

The instance of rule 1 is called _locator_. The instance of rule 2 is called
_attribute access_. The instance of rule 3 is called _application_ or
_attribute instantiation_. The instance of rule 4 is called _object term_ (or
just _object_).

An object term is essentially the same as object from Definition 2.1 with the
restriction that mapping has finitely many attributes.

Locators allow to reference enclosing objects, and consequently, their
attributes. For example, consider object $\llbracket
x\mapsto\rho^{0}.y,y\mapsto\llbracket\rrbracket\rrbracket$. Here $\rho^{0}$
references the closest enclosing object, which is the entire term, and so
attribute $x$ is attached to a term that essentially references attribute $y$
of the same object. The index in the locator tells us how many levels of
enclosing objects one needs to go to arrive at the referenced object. In fact,
locators are effectively de Bruijn indices (de Bruijn, 1972) of nested
objects. For example, locator $\rho^{2}$ in the term $\llbracket
x\mapsto\llbracket y\mapsto\llbracket
z\mapsto\rho^{2}\rrbracket\rrbracket\rrbracket$ references the entire term.
This correspondence is made more precise in Section 5 where we give a
translation to lambda calculus.

The idea behind attribute access terms is fairly straightforward: we simply
intend to extract the associated value. For example, evaluating $\llbracket
x\mapsto\llbracket\rrbracket\rrbracket.x$ should produce an empty object.
However, because of locators, we cannot do a simple extraction in general and
have to perform locator substitution: evaluating $\llbracket
x\mapsto\rho^{0}\rrbracket.x$ requires understanding what object $\rho^{0}$
references. This limitation makes it very different from syntactically similar
construction in $\lambda$-calculus with records.

Attribute instantiation attaches terms to void attributes. Importantly,
attached attributes may reference void attributes as in $\llbracket
x\mapsto\varnothing,y\mapsto\rho^{0}.x\rrbracket$. Obviously, accessing
attribute $y$ of such an object would require accessing void attribute $x$
which does not have an attached value. However, after instantiating the
attribute $\llbracket
x\mapsto\varnothing,y\mapsto\rho^{0}.x\rrbracket(x\mapsto\llbracket\rrbracket)$,
we can now access attribute $y$ and get the empty object. This example shows
that locators are not just references to syntactic objects, but can also
reference the result of attribute instantiation.

Decorator attribute $\varphi$ plays an important role in evaluation. This
attribute contains the component of the decorator, and an object with
$\varphi$ will redirect attribute access to its component whenever the object
does not possess the attribute itself. For example, accessing attribute $.x$
of the object $\llbracket\varphi\mapsto\llbracket x\mapsto
t_{1}\rrbracket,y\mapsto t_{2}\rrbracket$ will be redirected to accessing
$.\varphi.x$ of the object since the original object does not have $x$ as its
attribute.

###  2.2. Locators

Before we can properly talk about evaluation, we need to define how locators
work. As locators are de Bruijn indices of nested objects, we have to be able
to adjust locator indices when moving terms in and out of objects, and replace
locators with an actual object they reference when that object disappears.

Attribute instantiation requires putting a term in an object. This requirement
may demand updating certain locators. Consider term $\llbracket
x\mapsto\varnothing\rrbracket(x\mapsto\rho^{0})$ where $\rho^{0}$ references
some outer object. Simply replacing $\varnothing$ with $\rho^{0}$ will result
in $\llbracket x\mapsto\rho^{0}\rrbracket$ which would change the meaning of
$\rho^{0}$. Instead, since we are placing $\rho^{0}$ inside of an object, we
have to increment its index. In general though, given $t(a\mapsto u)$ we do
not increment all locators in $u$, but only those referencing outside of $u$.
For example, if $u\equiv\llbracket
y\mapsto\rho^{0},z\mapsto\rho^{1}\rrbracket$ then we only increment
$\rho^{1}$, since otherwise its reference object will change when we put $u$
in an object. So we define locator increment as follows:

###### Definition 2.5.

_Locator increment_ $t\uparrow{}^{n}$ is defined inductively on
$\varphi$-terms:

(1) $\displaystyle\rho^{m}\uparrow{}^{n}$
$\displaystyle:=\rho^{m}\quad\text{if $m<n$}$ (2)
$\displaystyle\rho^{m}\uparrow{}^{n}$ $\displaystyle:=\rho^{m+1}\quad\text{if
$n\leq m$}$ (3) $\displaystyle t.a\uparrow{}^{n}$
$\displaystyle:=t\uparrow{}^{n}.a$ (4) $\displaystyle t_{1}(a\mapsto
t_{2})\uparrow{}^{n}$ $\displaystyle:=t_{1}\uparrow{}^{n}(a\mapsto
t_{2}\uparrow{}^{n})$ $\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto
t_{n}\rrbracket\uparrow{}^{n}$ (5) $\displaystyle:=\llbracket
a_{1}\mapsto\varnothing,\ldots,b_{1}\mapsto
t_{1}\uparrow{}^{n+1},\ldots,b_{n}\mapsto t_{n}\uparrow{}^{n+1}\rrbracket$

We write $t\uparrow$ short for $t\uparrow{}^{0}$.

When accessing an attribute $a$ of an object $u\equiv\llbracket\ldots,a\mapsto
t,\ldots\rrbracket$, we cannot simply return $t$ as it may contain locators
that need adjustment. We can split locators in $t$ into three groups:

  1. (1)

Locators that reference some object _inside_ of $t$ require no adjustment as
corresponding objects are still present after extraction.

  2. (2)

Locators that reference object $u$, which we are extracting from, have to be
substituted with $u$ itself, to avoid losing information when we extract the
subterm $t$.

  3. (3)

Locators that reference some object _outside_ of $u$ have to be decremented
since one nested object ($u$) disappeared.

We define locator substitution with the usual notation $t[\rho^{n}\mapsto u]$
meaning that we intend to substitute all locators referencing the same object
as $\rho^{n}$ in $t$ with term $u$ (with all locators updated properly).

###### Definition 2.6.

_Locator substitution_ $t[\rho^{n}\mapsto u]$ is defined inductively on
$\varphi$-terms (see Figure 1).

###### Definition 2.7.

A $\varphi$-term $t$ is called _closed_ if all its locators reference some
object in $t$. Otherwise it is _open_.

###  2.3. Evaluation

In this section we define small step reduction semantics for
$\varphi$-calculus. We introduce four congruence rules, to enable reduction in
subterms, as well as three main reduction rules. Attribute access and
attribute instantiation provide two reduction rules given an object term.
Then, considering the presence of the decorator attribute $\varphi$, we get
one extra rule for attribute access. Figure 1 shows the complete set of
reduction rules.

Rule DOTc formalizes the idea that extracting attribute $c$ from an object $t$
is straightforward as long as we substitute all locators that reference to $t$
in the resulting term. Rule DOT${}_{c}^{\varphi}$ specifies further that
whenever $c$ is not an attribute of $t$ but $\varphi$ is, we should extract
$c$ from $t.\varphi$. Importantly, we do extract the term attached to
$\varphi$ immediately. Such extraction would require to check recursively
whether we should go to $t.\varphi.\varphi$ and further. Instead we want our
rules to perform just a single step of reduction.

Rule APPc shows that attaching a term $u$ to the attribute $c$ requires
incrementing locators in $u$.

####  2.3.1. Decorated instantiation

As we are following the idea of Decorator pattern (Gamma et al., 1995, Chapter
4), in $\varphi$-calculus only concrete objects are supposed to be decorated.
That said, one could consider a variation of our calculus where decoration and
later instantiation of abstract objects is possible as well. For example, we
can introduce the following evaluation rule:

$t\equiv\llbracket\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\varphi\mapsto
t_{\varphi}},\ldots\rrbracket$ $c\notin\operatorname{\mathsf{attr}}(t)$
APP${}_{c}^{\varphi}$ $t(c\mapsto
u)\rightsquigarrow\llbracket\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\varphi\mapsto
t_{\varphi}(c\mapsto u\uparrow)},\ldots\rrbracket$

For the rest of this paper we will assume $\varphi$-calculus without
APP${}_{c}^{\varphi}$ rule. However, all results still hold for a variation of
the calculus with it.

_Syntax_ (terms) $\displaystyle t$ $\displaystyle:=$ (attribute)
$\displaystyle\phantom{\mid\;\;}t.a$ (application) $\displaystyle\mid
t_{1}(a\mapsto t_{2})$ (object) $\displaystyle\mid\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ ($n$-th parent object locator)
$\displaystyle\mid\rho^{n}$ _Evaluation_ $t_{i}\rightsquigarrow
t_{i}^{\prime}$ cong${}_{\text{OBJ}}$ $\llbracket\ldots,b_{i}\mapsto
t_{i},\ldots\rrbracket\rightsquigarrow\llbracket\ldots,b_{i}\mapsto
t_{i}^{\prime},\ldots\rrbracket$ $t\rightsquigarrow t^{\prime}$
cong${}_{\text{DOT}}$ $t.a\rightsquigarrow t^{\prime}.a$ $t\rightsquigarrow
t^{\prime}$ cong${}_{\text{APP}^{\text{L}}}$ $t(a\mapsto u)\rightsquigarrow
t^{\prime}(a\mapsto u)$ $u\rightsquigarrow u^{\prime}$
cong${}_{\text{APP}^{\text{R}}}$ $t(a\mapsto u)\rightsquigarrow
t^{\prime}(a\mapsto u^{\prime})$
$t\equiv\llbracket\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto
t_{c}},\ldots\rrbracket$ DOTc
$t.c\rightsquigarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t_{c}}\left[\rho^{0}\mapsto
t\right]$ $t\equiv\llbracket\ldots\rrbracket$
$c\notin\operatorname{\mathsf{attr}}(t)$
$\varphi\in\operatorname{\mathsf{attr}}(t)$ DOT${}_{c}^{\varphi}$
$t.c\rightsquigarrow t.\varphi.c$ $t\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto\varnothing},b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ APPc $t(c\mapsto
u)\rightsquigarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto
u\uparrow},b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ _Locator
substitution_ $\displaystyle\rho^{n}[\rho^{m}\mapsto u]$
$\displaystyle:=\rho^{n}\quad\text{if $n<m$}$
$\displaystyle\rho^{n}[\rho^{n}\mapsto u]$ $\displaystyle:=u$
$\displaystyle\rho^{n}[\rho^{m}\mapsto u]$
$\displaystyle:=\rho^{n-1}\quad\text{if $n>m$}$ $\displaystyle
t.a[\rho^{n}\mapsto u]$ $\displaystyle:=t[\rho^{n}\mapsto u].a$ $\displaystyle
t_{1}(a\mapsto t_{2})[\rho^{n}\mapsto u]$
$\displaystyle:=t_{1}[\rho^{n}\mapsto u](a\mapsto t_{2}[\rho^{n}\mapsto u])$
$\displaystyle\llbracket a_{1}\mapsto\varnothing,\ldots,b_{1}\mapsto
t_{1},\ldots\rrbracket[\rho^{n}\mapsto u]$ $\displaystyle:=\llbracket
a_{1}\mapsto\varnothing,\ldots,b_{1}\mapsto t_{1}[\rho^{n+1}\mapsto
u\uparrow],\ldots\rrbracket$ Figure 1. Syntax and evaluation rules for
$\varphi$-calculus.

###  2.4. Modelling object-oriented languages

Bugayenko (Bugayenko, 2021a) introduced $\varphi$-calculus as a semi-formal
mathematical model for EO programming language. EO language is an object-
oriented programming language that relies on decoration instead of inheritance
to work with object hierarchies. In (Bugayenko, 2021b), Bugayenko showed
approaches to encode advanced features of mainstream object-oriented languages
in EO. In this subsection, we revisit Bugayenko’s ideas (Bugayenko, 2021b)
regarding encoding mechanisms of code reuse in class-based and prototype-based
constructs in terms of $\varphi$-calculus.

####  2.4.1. Class-based

Classes can be modelled as the so called “object factories” — objects with a
special method $\mathsf{new}$, that produces an instance of the class. To
model inheritance, this method can take an object as input and extend it with
all the necessary methods using decoration.

###### Example 2.8.

Consider the following code snippet in Java:

⬇

class Base {

Integer g() { return h(); }

Integer h() { return 3; }

}

class Derived extends Base {

Integer f() { return 2 + this.g(); }

Integer h() { return 5; }

}

Derived d = new Derived();

In the following translation scheme from Java to $\varphi$-calculus, it is
made explicit that methods accept $\mathsf{this}$ argument. It allows to
distinguish derived class, when it calls a method that is defined in a
subclass.

$\displaystyle\mathsf{Base}$ $\displaystyle:=\llbracket\mathsf{new}\mapsto$
$\displaystyle\phantom{:=\llbracket\mathsf{new}}\llbracket\mathsf{g}\mapsto\llbracket\mathsf{this}\mapsto\varnothing,\;\varphi\mapsto\mathsf{\rho^{0}.this.h(this\mapsto\rho^{0}.this).\varphi}\rrbracket,$
$\displaystyle\phantom{:=\llbracket\mathsf{new}\llbracket}\mathsf{h}\mapsto\llbracket\mathsf{this}\mapsto\varnothing,\;\varphi\mapsto
3\rrbracket\rrbracket$ $\displaystyle\phantom{:=\llbracket}\rrbracket$
$\displaystyle\mathsf{Derived}$ $\displaystyle:=\llbracket\mathsf{new}\mapsto$
$\displaystyle\phantom{:=\llbracket\mathsf{new}}\llbracket\varphi\mapsto\mathsf{Base.new},$
$\displaystyle\phantom{:=\llbracket\mathsf{new}\llbracket}\mathsf{f}\mapsto\llbracket\mathsf{this}\mapsto\varnothing,\;\varphi\mapsto\mathsf{2.add(n\mapsto\rho^{0}.this.g(this\mapsto\rho^{0}.this).\varphi)}\rrbracket,$
$\displaystyle\phantom{:=\llbracket\mathsf{new}\llbracket}\mathsf{h}\mapsto\llbracket\mathsf{this}\mapsto\varnothing,\;\varphi\mapsto
5\rrbracket\rrbracket$ $\displaystyle\phantom{:=\llbracket}\rrbracket$
$\displaystyle d$ $\displaystyle:=\mathsf{Derived}.\mathsf{new}$

In Java, the method invocation d.f() computes to 7: the method f() of the
derived class calls g(), defined in the base class, which, in turn, calls h(),
which is overridden in the the derived class. In $\varphi$-terms, with
explicit $\mathsf{this}$ arguments, the chain of calls is the same, so the
semantics is preserved:

(6) $\displaystyle\mathsf{d.f(this\mapsto d).\varphi}$
$\displaystyle\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}\mathsf{2.add(n\mapsto
d.g(this\mapsto d).\varphi)}$ (7)
$\displaystyle\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}\mathsf{2.add(n\mapsto
d.\varphi.g(this\mapsto d).\varphi)}$ (8)
$\displaystyle\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}\mathsf{2.add(n\mapsto
Base.new.g(this\mapsto d).\varphi)}$ (9)
$\displaystyle\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}\mathsf{2.add(n\mapsto
d.h(this\mapsto d).\varphi)}$ (10)
$\displaystyle\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}\mathsf{2.add(n\mapsto
5)}$

Note that in (8), ‘method’ $\mathsf{g}$ is called from the $\mathsf{Base}$
‘class’ with $(\mathsf{this\mapsto d})$. This is what provides proper support
of the dynamic dispatch (open recursion) in modeling of classes in
$\varphi$-calculus.

The above example aims to provide intuition for $\varphi$-calculus. A proper
mapping from Java to $\varphi$-calculus would require more technical details,
such as dealing with mutable attributes, generics, interfaces, and other
features.

####  2.4.2. Prototype-based

Prototypes in object-oriented languages, such as JavaScript, work similarly to
decorators in $\varphi$-calculus: when looking for a method in a JavaScript
object, the interpreter checks object’s _own properties_ first and then, if
such properties are absent, the interpreter proceeds to look for the method in
the object’s _prototype_ , unless the prototype is _null_. Importantly,
JavaScript’s objects are mutable allowing for dynamic prototypes and
properties, whereas in $\varphi$-calculus objects are immutable.

###### Example 2.9.

Consider the following code snippet in JavaScript:

⬇

let A = function() { this.x = 3; }

A.prototype.f = function() { return this.x; }

let b = new A();

let c = b.f()

This snippet would translate to $\varphi$-calculus as follows:

$\displaystyle\mathsf{A}:=$
$\displaystyle\llbracket\mathsf{new}\mapsto\llbracket\mathsf{x}\mapsto
3,\varphi\mapsto\rho^{1}.\mathsf{prototype}\rrbracket,$
$\displaystyle\;\;\mathsf{prototype}\mapsto\llbracket\mathsf{f}\mapsto\llbracket\mathsf{this}\mapsto\varnothing,\varphi\mapsto\rho^{0}.\mathsf{this}.\mathsf{x}\rrbracket\rrbracket\rrbracket$
$\displaystyle\mathsf{b}:=$ $\displaystyle\mathsf{A}.\mathsf{new}$
$\displaystyle\mathsf{c}:=$
$\displaystyle\mathsf{b}.f(\mathsf{this}\mapsto\mathsf{b})$

Similarly to the translation of Java’s class-based constructs, here
$\mathsf{b}$ is passed as $\mathsf{this}$ argument in the method call
(application of) $\mathsf{b.f}$ in order to preserve information about an
object that originally called $f$; this is essential whenever attributes are
resolved in decoratees (higher in the hierarchy of objects, representing
prototypes).

##  3\. Confluence

Intuitively, we think of $\varphi$-terms as programs in terms of objects.
Moreover, we assume a single meaning to each such program. In other words,
every program either diverges (e.g. falls into an infinite loop) or produces
the final object (normal form). To justify the use of “the” in “the normal
form” we require the uniqueness of normal form.

In this section we prove a more general result. We show that
$\varphi$-calculus possesses the following property: if some term $t$ can be
reduced in different ways to terms $u$ and $v$ then there exists some term $w$
such that both $u$ and $v$ reduce to $w$. This is known as Church-Rosser
property:

###### Definition 3.1.

A relation $\xrightarrow[]{X}$ on terms is said to satisfy _Church-Rosser
property_ if for any terms $t$, $u$ and $v$, if $t\xrightarrow[]{X}u$ and
$t\xrightarrow[]{X}v$, then there exists some term $w$ such that
$u\xrightarrow[]{X}w$ and $v\xrightarrow[]{X}w$.

In general, a $\varphi$-term can be rewritten in different ways, since it may
contain several redexes. For example, here is a graph with all possible
reductions for a term:

${\llbracket x\mapsto\llbracket
y\mapsto\varnothing\rrbracket\rrbracket.x(y\mapsto\llbracket z\mapsto
w\rrbracket.z)}$${\llbracket y\mapsto\varnothing\rrbracket(y\mapsto\llbracket
z\mapsto w\rrbracket.z)}$${\llbracket x\mapsto\llbracket
y\mapsto\varnothing\rrbracket\rrbracket.x(y\mapsto w)}$${\llbracket
y\mapsto\llbracket z\mapsto w\rrbracket.z\rrbracket}$${\llbracket
y\mapsto\varnothing\rrbracket(y\mapsto w)}$${\llbracket y\mapsto w\rrbracket}$

Other terms may have infinite rewrite sequences, e.g.:

${\llbracket x\mapsto\rho^{0}.y,y\mapsto\rho^{0}.x\rrbracket.x}$${\llbracket
x\mapsto\rho^{0}.y,y\mapsto\rho^{0}.x\rrbracket.y}$

In these two examples, we can see diamond property satisfied for
$\rightsquigarrow$, but unfortunately, the property does not hold in general.

###### Example 3.2.

Consider the following $\varphi$-terms $A$ and $B$:

$\displaystyle A$ $\displaystyle\equiv\llbracket x\mapsto\llbracket a\mapsto$
$\displaystyle\llbracket z\mapsto\varnothing\rrbracket\rrbracket.a$
$\displaystyle,y\mapsto\rho^{0}.x(z\mapsto\rho^{0}.x)\rrbracket$
$\displaystyle B$ $\displaystyle\equiv\llbracket x\mapsto$
$\displaystyle\llbracket z\mapsto\varnothing\rrbracket$
$\displaystyle,y\mapsto\rho^{0}.x(z\mapsto\rho^{0}.x)\rrbracket$

Note that $A\operatorname{\rightsquigarrow}B$ by $\text{cong}_{\text{OBJ}}$
and $\text{DOT}_{a}$. Reduction of $A.y$ illustrates that substitution can
introduce multiple redexes, that cannot be reduced in a single step of
$\operatorname{\rightsquigarrow}$:

${A.y}$${B.y}$${A.x(z\mapsto A.x)}$${B.x(z\mapsto A.x)}$${B.x(z\mapsto
A.x)}$${B.x(z\mapsto B.x)}$no $\scriptstyle\operatorname{\rightsquigarrow}$
here

To prove confluence for $\varphi$-calculus we follow these steps:

  1. (1)

We introduce parallel reduction on $\varphi$-terms; this kind of reduction
possesses the diamond property. Using parallel reduction in a proof of
confluence is due to Tait and Löf (Barendregt and Barendsen, 1984, Section
3.2)

  2. (2)

We show that parallel reduction is equivalent to regular reduction.

  3. (3)

We show that parallel reduction possesses the diamond property via complete
development, following Takahashi’s technique (Takahashi, 1995).

  4. (4)

We prove confluence for regular reduction via equivalence with parallel
reduction, also using the fact that confluence for parallel reduction follows
from its diamond property via (Krivine, 1993, Lemma 1.17).

While regular reduction performs exactly one reduction step somewhere in a
term, the idea of parallel reduction is to perform arbitrary number of
reductions _in parallel_. Performing reductions in parallel intuitively means
that we do not reduce a term after performing substitution or adding
$.\varphi$. Figure 2 gives the rules for parallel reduction. Observe that
$\varphi$-terms in Example 3.2 satisfy the diamond property with single step
parallel reduction: $A.x(z\mapsto A.x)\Rrightarrow B.x(z\mapsto B.x)$ by
cong${}_{\text{APP}}^{\Rrightarrow}$.

$t_{1}\Rrightarrow t_{1}^{\prime}\quad\ldots\quad t_{n}\Rrightarrow
t_{n}^{\prime}$ cong${}_{\text{OBJ}}^{\Rrightarrow}$ $\llbracket
a_{i}\mapsto\varnothing,b_{j}\mapsto t_{j}\rrbracket\Rrightarrow\llbracket
a_{i}\mapsto\varnothing,b_{j}\mapsto t_{j}^{\prime}\rrbracket$ for
$i\in\\{1,\ldots,k\\},j\in\\{1,\ldots,n\\}$ cong${}_{\rho}^{\Rrightarrow}$
$\rho^{n}\Rrightarrow\rho^{n}$ $t\Rrightarrow t^{\prime}$
cong${}_{\text{DOT}}^{\Rrightarrow}$ $t.a\Rrightarrow t^{\prime}.a$
$t\Rrightarrow t^{\prime}$ $u\Rrightarrow u^{\prime}$
cong${}_{\text{APP}}^{\Rrightarrow}$ $t(a\mapsto u)\Rrightarrow
t^{\prime}(a\mapsto u^{\prime})$ $t\Rrightarrow t^{\prime}\quad
t^{\prime}\equiv\llbracket\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto
t_{c}},\ldots\rrbracket$ DOT${}_{c}^{\Rrightarrow}$
$t.c\Rrightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t_{c}}\left[\rho^{0}\mapsto
t^{\prime}\right]$ $t\Rrightarrow t^{\prime}\quad
t^{\prime}\equiv\llbracket\ldots\rrbracket$
$c\notin\operatorname{\mathsf{attr}}(t^{\prime})\quad\varphi\in\operatorname{\mathsf{attr}}(t^{\prime})$
DOT${}_{c}^{\varphi\Rrightarrow}$ $t.c\Rrightarrow t^{\prime}.\varphi.c$
$t\Rrightarrow t^{\prime}\quad t^{\prime}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto\varnothing},b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ $u\Rrightarrow u^{\prime}$
APP${}_{c}^{\Rrightarrow}$ $t(c\mapsto u)\Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto
u^{\prime}\uparrow},b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$
Figure 2. Parallel reduction rules for $\varphi$-calculus.

One important property of parallel reduction is that “doing nothing” is also a
parallel reduction. We justify this with the following proposition:

###### Proposition 3.3 (Reflexivity of parallel reduction).

Let $t$ be a $\varphi$-term. Then $t\Rrightarrow t$.

###### Proof.

Straightforward by structural induction on $t$. ∎

Since our goal is to prove confluence for regular reduction via parallel
reduction, we need to establish that the two kinds of reduction are
equivalent, meaning that if one term reduces regularly to another term, then
those terms are also related via parallel reduction and vice versa.

###### Proposition 3.4 (Equivalence of $\Rrightarrow$ and $\rightsquigarrow$).

Parallel reduction ($\Rrightarrow$) is equivalent to regular reduction
($\rightsquigarrow$):

  1. (1)

$t\rightsquigarrow t^{\prime}$ implies $t\Rrightarrow t^{\prime}$

  2. (2)

$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime}$

  3. (3)

$t\Rrightarrow t^{\prime}$ implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$

  4. (4)

$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime}$
implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$

###### Proof.

Straightforward by structural induction. ∎

In the following proofs we need to know that if $t\Rrightarrow t^{\prime}$ and
$u\Rrightarrow u^{\prime}$ then $t[\rho^{0}\mapsto u]\Rrightarrow
t^{\prime}[\rho^{0}\mapsto u^{\prime}]$. We prove a slightly more general
lemma:

###### Lemma 3.5 (Substitution lemma).

Let $t,t^{\prime},u,u^{\prime}$ be $\varphi$-terms and $t\Rrightarrow
t^{\prime}$ and $u\Rrightarrow u^{\prime}$. Then $t[\rho^{i}\mapsto
u]\Rrightarrow t^{\prime}[\rho^{i}\mapsto u^{\prime}]$.

To show that parallel reduction satisfies the diamond property, we adapt
Takahashi’s technique (Takahashi, 1995) and define complete development of a
term, which is intuitively the maximum possible one-step parallel reduction of
a term. The idea is that if $t\Rrightarrow t^{\prime}$ then simply by
performing all parallel reductions that were “skipped” when producing
$t^{\prime}$, we get from $t^{\prime}$ to the complete development of $t$.
More formally:

###### Definition 3.6.

Let $t$ be a $\varphi$-term. Then a term $t^{+}$ denotes the _complete
development_ of $t$, defined recursively as follows:

$\displaystyle(\rho^{n})^{+}$ $\displaystyle:=\rho^{n}$
$\displaystyle(t.a)^{+}$ $\displaystyle:=\begin{cases}t_{a}[\rho^{0}\mapsto
t^{+}],&\text{if $t^{+}\equiv\llbracket\ldots,a\mapsto
t_{a},\ldots\rrbracket$}\\\ t^{+}.\varphi.a,&\text{if
$a\notin\operatorname{\mathsf{attr}}(t^{+})$ and
$\varphi\in\operatorname{\mathsf{attr}}(t^{+})$}\\\
t^{+}.a&\text{otherwise}\end{cases}$ $\displaystyle(t(a\mapsto u))^{+}$
$\displaystyle:=\begin{cases}\llbracket a\mapsto
u^{+}\uparrow,\ldots\rrbracket,&\text{if $t^{+}\equiv\llbracket
a\mapsto\varnothing,\ldots\rrbracket$}\\\ t^{+}(a\mapsto
u^{+})&\text{otherwise}\end{cases}$ $\displaystyle(\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket)^{+}$ $\displaystyle:=\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{+},\ldots,b_{n}\mapsto t_{n}^{+}\rrbracket$

The definition clearly shows that we basically follow rules of parallel
reduction, but always choose the rule that does the most work. In particular,
if both $\text{APP}_{c}^{\Rrightarrow}$ and
$\text{cong}_{\text{APP}}^{\Rrightarrow}$ are applicable, we prioritize rule
$\text{APP}_{c}^{\Rrightarrow}$ since it performs strictly more reductions.
Consequently, a term can always be parallel reduced to its complete
development:

###### Proposition 3.7.

Let $t$ be a $\varphi$-term. Then $t\Rrightarrow t^{+}$.

###### Proof.

Straightforward by induction on $t$. ∎

Before we prove the diamond property, we need a simpler result for just one
half of the diamond:

###### Proposition 3.8.

Let $t,t^{\prime}$ be $\varphi$-terms and $t\Rrightarrow t^{\prime}$. Then
$t^{\prime}~{}\Rrightarrow~{}t^{+}$.

###### Corollary 3.9 (Diamond property of parallel reduction).

Let $t,u,v$ be $\varphi$-terms and $t\Rrightarrow u$ and $t\Rrightarrow v$.
Then there exists a $\varphi$-term $w$ such that $u\Rrightarrow w$ and
$v\Rrightarrow w$.

###### Proof.

Let $w\equiv t^{+}$. With 3.8, $u\Rrightarrow w$ and $v\Rrightarrow w$. ∎

###### Corollary 3.10 (Confluence of parallel reduction).

Let $t,u,v$ be $\varphi$-terms and
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}u$ and
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}v$. Then there
exists a $\varphi$-term $w$ such that
$u\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}w$ and
$v\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}w$.

###### Proof.

Follows from the diamond property (see (Krivine, 1993, Lemma 1.17)). ∎

###### Theorem 3.11 (Confluence).

Let $t,u,v$ be $\varphi$-terms and
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}u$ and
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}v$. Then
there exists a $\varphi$-term $w$ such that
$u\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}w$ and
$v\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}w$.

###### Proof.

Follows from Proposition 3.4 and Corollary 3.10. ∎

As usual, a term $t$ is in _normal form_ if it has no redexes. In
$\varphi$-calculus, it means:

###### Definition 3.12.

$\varphi$-term $t$ is said to have the normal form if

$\displaystyle t\equiv\begin{cases}\rho^{n}\\\ \llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket,&\text{if $t_{j}$ is in NF}\\\
s.a,&\text{if $s$ is in NF and $s.a$ is not a redex}\\\ s(a\mapsto
u),&\text{if $s$ and $u$ are in NF and $s(a\mapsto u)$ is not a redex}\\\
\end{cases}$

With this definition we have a trivial corollary of Theorem 3.11:

###### Corollary 3.13.

Every $\varphi$-term has at most one normal form.

For the reasoning about the abstract machine in the section 4, weak head
normal form needs to be defined:

###### Definition 3.14.

$\varphi$-term $t$ is said to be in a weak head normal form if

$\displaystyle t\equiv\begin{cases}\rho^{n}\\\ \llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket\\\ s.a,&\text{if $s$ is in WHNF and
$s.a$ is not a redex}\\\ s(a\mapsto u),&\text{if $s$ is in WHNF and
$s(a\mapsto u)$ is not a redex}\\\ \end{cases}$

Equivalently, one might have said that $t$ is in a weak head normal if no head
reductions (defined in the figure 3) starting from $t$ are possible.

###### Example 3.15.

Term $\llbracket z\mapsto\llbracket
x\mapsto\rho^{0}.y,y\mapsto\rho^{0}.x\rrbracket.x\rrbracket$ is in weak head
normal form, but it does not have a normal form.

###  3.1. Completeness of normal order evaluation

In this subsection, we define normal order reduction strategy and prove that
this strategy reduces a term to its normal form, if such a form exists.

Similarly to $\lambda$-calculus, normal order reduction in $\varphi$-calculus
is defined in terms of head reduction. Head reduction does not apply to
redexes inside objects and to arguments of object application. If possible,
normal order reduction performs head reduction, otherwise it performs
reduction in the leftmost subterm that can be reduced.

Our proof of completeness of normal order evaluation relies on the
standardization theorem: if $t$ reduces to $u$, then there exists a reduction
path, where head reductions are performed first, and internal reductions
follow.

Contrary to the head reduction, internal reduction applies to redexes inside
objects and in arguments of application. During the proof, we exploit internal
parallel reduction which is the intersection of parallel reduction and
reflexive-transitive closure of the internal regular reduction.

_Head reduction_
$t\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}$
cong${}_{\text{DOT}}^{h}$
$t.a\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}.a$
$t\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}$
cong${}_{\text{APP}}^{h}$ $t(a\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}(a\mapsto
u)$
$t\equiv\llbracket\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto
t_{c}},\ldots\rrbracket$ DOTc
$t.c\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t_{c}\left[\rho^{0}\mapsto
t\right]$ $t\equiv\llbracket\ldots\rrbracket$
$c\notin\operatorname{\mathsf{attr}}(t)$
$\varphi\in\operatorname{\mathsf{attr}}(t)$ DOT${}_{c}^{\varphi}$
$t.c\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t.\varphi.c$
$t\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto\varnothing},b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ APPc $t(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}c\mapsto
u\uparrow},b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ _Normal
order_ $\displaystyle t.a$
$\displaystyle\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}\begin{cases}s,&\text{if
$t.a\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}s$}\\\
t^{\prime}.a,&\text{else if
$t\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}t^{\prime}$}\end{cases}$
$\displaystyle t(a\mapsto u)$
$\displaystyle\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}\begin{cases}s,&\text{if
$t(a\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}s$}\\\
t^{\prime}(a\mapsto u),&\text{else if
$t\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}t^{\prime}$}\\\
t(a\mapsto u^{\prime}),&\text{else if
$u\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}u^{\prime}$}\end{cases}$
$\displaystyle\llbracket a_{i}\mapsto\varnothing,b_{j}\mapsto t_{j}\rrbracket$
$\displaystyle\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}\llbracket
a_{i}\mapsto\varnothing,b_{j}\mapsto t_{j}^{\prime}\rrbracket,\text{ if
$t_{j}\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}t_{j}^{\prime}$}$
_Regular internal reduction_ $t_{i}\rightsquigarrow t_{i}^{\prime}$
cong${}^{i}_{\text{OBJ}}$ $\llbracket\ldots,b_{i}\mapsto
t_{i},\ldots\rrbracket\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\rightsquigarrow}}}\llbracket\ldots,b_{i}\mapsto
t_{i}^{\prime},\ldots\rrbracket$
$t\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\rightsquigarrow}}}t^{\prime}$
cong${}^{i}_{\text{DOT}}$
$t.a\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\rightsquigarrow}}}t^{\prime}.a$
$t\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\rightsquigarrow}}}t^{\prime}$
cong${}^{i}_{\text{APP}^{\text{L}}}$ $t(a\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\rightsquigarrow}}}t^{\prime}(a\mapsto
u)$ $u\rightsquigarrow u^{\prime}$ cong${}^{i}_{\text{APP}^{\text{R}}}$
$t(a\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\rightsquigarrow}}}t^{\prime}(a\mapsto
u^{\prime})$ _Parallel internal reduction_ $t_{1}\Rrightarrow
t_{1}^{\prime}\quad\ldots\quad t_{n}\Rrightarrow t_{n}^{\prime}$
cong${}_{\text{OBJ}}^{\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}}$
$\llbracket a_{i}\mapsto\varnothing,b_{j}\mapsto
t_{j}\rrbracket\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}\llbracket
a_{i}\mapsto\varnothing,\ldots,b_{j}\mapsto t_{j}^{\prime}\rrbracket$
cong${}_{\rho}^{\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}}$
$\rho^{n}\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}\rho^{n}$
$t\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}t^{\prime}$
cong${}_{\text{DOT}}^{\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}}$
$t.a\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}t^{\prime}.a$
$t\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}t^{\prime}$
$u\Rrightarrow u^{\prime}$
cong${}_{\text{APP}}^{\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}}$
$t(a\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}t^{\prime}(a\mapsto
u^{\prime})$ Figure 3. Head, internal and normal order reductions

The proof is developed in a close relation to the one of Takahashi (Takahashi,
1995). First, we show that one step of parallel reduction can be decomposed to
multiple head reductions and one internal parallel reduction step.

###### Lemma 3.16 (Main Lemma).

$t\Rrightarrow s$ implies
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s$
for some $r$.

###### Lemma 3.17 (Substitution Lemma for
$\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}$).

If $t\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}s$,
then $t[\rho^{n}\mapsto
q]\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}s[\rho^{n}\mapsto
q]$.

###### Lemma 3.18 (Substitution Lemma for
$\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}$).

If $t\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s$ and
$q\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}r$, then
$t[\rho^{n}\mapsto
q]\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s[\rho^{n}\mapsto
r]$.

Then, we show that if head reduction follows internal parallel reduction,
reductions can be reordered so that head reductions occur first.

###### Lemma 3.19 (Standardizing Reductions).

For any $\varphi$-terms $t,r,s$ such that
$t\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}s$,
there exists $\varphi$-term $q$, such that
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}q\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s$.

###### Proof.

By induction on the structure of
$r\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}s$. ∎

Standardization theorem is then a corollary:

###### Corollary 3.20.

$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}s$ implies
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{i}^{\ast}}}{{\rightsquigarrow}}}s$
for some $\varphi$-term $r$.

###### Proof.

Recall that equivalence of
$\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}$ and
$\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}$ (4) implies
that $t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}s$.

By induction on
$\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}$,

  1. (1)

if $t\equiv s$, then
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{i}^{\ast}}}{{\rightsquigarrow}}}s$
for $r\equiv s$

  2. (2)

else, $t\Rrightarrow q$ and
$q\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}s$. By Main
Lemma, there exists $p$, such that
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}p\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}q$.
By induction hypothesis, there exists $r^{\prime}$, such that
$q\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{i}^{\ast}}}{{\rightsquigarrow}}}s$.
Repeated application of the Standardizing Reductions Lemma propagates
$\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}$ in
$p\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}q\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}$
to the end, and the equivalence of
$\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}$ and
$\operatorname{\stackrel{{\scriptstyle\textit{i}^{\ast}}}{{\rightsquigarrow}}}$
completes the proof.

∎

###### Theorem 3.21 (Completeness of normal order evaluation).

If $t$ has normal form $s$, then
$t\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}s$.

###### Proof.

With the corollary,
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{i}^{\ast}}}{{\rightsquigarrow}}}s$
for some $\varphi$-term $r$.

By induction on the structure of $s$,

  1. (1)

if $s\equiv\rho^{n}$, then $r\equiv\rho^{n}$. As
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r$,
$t\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}r$,
which follows from the definition of
$\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}$.

  2. (2)

if $s\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$, the $r\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{n}\mapsto t_{n}^{\prime}\rrbracket$ and $t_{j}$ is NF
of $t_{j}^{\prime}$. By induction hypothesis,
$t_{j}^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}t_{j}$,
so
$r\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}s$,
hence
$t\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}s$.

  3. (3)

if $s\equiv q.a$, then $q$ is in NF and $q.a$ is not a redex, hence $r\equiv
q^{\prime}.a$, and $q$ is NF of $q^{\prime}$. By induction hypothesis,
$q^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}q$,
and since $q.a$ is not a redex,
$q^{\prime}.a\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}q.a$.
So,
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}s$,
and by definition of
$\operatorname{\stackrel{{\scriptstyle\textit{n.o.}}}{{\rightsquigarrow}}}$,
$t\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}s$.

  4. (4)

if $s\equiv q(a\mapsto u)$, then $q$ and $u$ are in NF and $q(a\mapsto u)$ is
not a redex, hence $r\equiv q^{\prime}(a\mapsto u^{\prime})$, and $q$ is NF of
$q^{\prime}$ and $u$ is NF of $u^{\prime}$. By induction hypothesis,
$q^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}q$
and
$u^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}u$,
and since $q(a\mapsto u)$ is not a redex, $q^{\prime}(a\mapsto
u^{\prime})\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}q(a\mapsto
u^{\prime})\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}q(a\mapsto
u)$. So,
$t\operatorname{\stackrel{{\scriptstyle\textit{n.o.}^{\ast}}}{{\rightsquigarrow}}}s$.

∎

##  4\. Abstract machine

Bugayenko (Bugayenko, 2021a) gives graph-based operational semantics. Although
the general idea is clear, his description lacks precision, in particular
regarding the handling of parent locators. Still, the existing implementations
of EO programming language and descriptions of graph-based semantics hint
strongly that intended semantics are those of a non-strict evaluation.

In this section, we introduce an abstract machine à la Krivine that performs
call-by-name reduction of $\varphi$-terms, therefore computing their weak head
normal form (defined in 3.14).

###  4.1. Call-by-name abstract machine

Here we present _term-actions-parents_ abstract machine (TAP machine) for
call-by-name evaluation of $\varphi$-terms.

We begin by introducing configurations of TAP machine:

###### Definition 4.1.

An _object closure_ is a tuple $(t,e)$ of a $\varphi$-term $t$ and a parent
stack, described below. A _parent_ is a tuple $(t,o)$ of an object
$\varphi$-term $t$ and a partial mapping $o$ (called _application mapping_)
from $\mathcal{L}$ to a set of object closures. A _parent stack_ is a finite
sequence of parents. An empty parent stack is denoted $\epsilon$. An _action_
is either an attribute access denoted $.a$ for some attribute
$a\in\mathcal{L}$, or an application denoted $(a\mapsto c)$ for some attribute
$a\in\mathcal{L}$ and an object closure $c$. An _action stack_ is a finite
sequence of actions. An empty action stack is denoted $\epsilon$. A
_configuration_ of TAP machine is a triple $\langle T,A,P\rangle$, where $T$
is either a $\varphi$-term in focus or an empty symbol $\epsilon$, $A$ is a
stack of actions, and $P$ — a parent stack.

The machine operates by following transition rules between the configurations.
Figure 4 gives the transition rules. The first two rules instruct how to
dereference parent locator $\rho^{n}$. Attribute access and application terms
are broken down into a smaller term and an action. For application $t(a\mapsto
u)$ we save the current parent stack $e$ and put an action $(a\mapsto(u,e))$
on the stack of actions. This effectively captures the necessary context
required to compute term $u$ later. Rule 15 puts an object term on the stack
with an empty application mapping (denoted $\varnothing$). The remaining four
rules describe effects of actions on the parent on the top of the stack. If
the parent object on the stack has an attribute that we want to access, we
extract the corresponding subterm and set it as our new current term. On the
other hand, if the attribute is mapped by the parent application mapping to
some object closure, then we take the term from that closure as our new
current term and replace current parent stack with the one from the closure.
If a parent has no required attribute, but has $\varphi$, we simply add
$.\varphi$ action to the action stack. Finally, an application action merely
updates the parent at the top of the parent stack, by replacing its
application mapping correspondingly: $o\cup\\{a\mapsto(u,e^{\prime})\\}$
denotes a mapping that maps attribute $a$ to object closure $(u,e^{\prime})$
and maps any other attribute $x$ to $o(x)$.

_Initial configuration_ $\displaystyle t\longrightarrow\langle
t,\epsilon,\epsilon\rangle$ _Transition rules for configurations_ (11)
$\displaystyle\langle\rho^{0},p,e\rangle$
$\displaystyle\longrightarrow\langle\epsilon,p,e\rangle$ (12)
$\displaystyle\langle\rho^{n+1},p,(c,o):e\rangle$
$\displaystyle\longrightarrow\langle\rho^{n},p,e\rangle$ (13)
$\displaystyle\langle t.a,p,e\rangle$ $\displaystyle\longrightarrow\langle
t,.a:p,e\rangle$ (14) $\displaystyle\langle t(a\mapsto u),p,e\rangle$
$\displaystyle\longrightarrow\langle t,(a\mapsto(u,e)):p,e\rangle$ (15)
$\displaystyle\langle\llbracket a_{1}\mapsto\varnothing,\ldots,b_{1}\mapsto
t_{1},\ldots\rrbracket,p,e\rangle$
$\displaystyle\longrightarrow\langle\epsilon,p,(\llbracket
a_{1}\mapsto\varnothing,\ldots,b_{1}\mapsto
t_{1},\ldots\rrbracket,\varnothing):e\rangle$ (16)
$\displaystyle\langle\epsilon,.a:p,(\llbracket a\mapsto
u,\ldots\rrbracket,o):e\rangle$ $\displaystyle\longrightarrow\langle
u,p,(\llbracket a\mapsto u,\ldots\rrbracket,o):e\rangle$ (17)
$\displaystyle\langle\epsilon,.a:p,(\llbracket
a\mapsto\varnothing,\ldots\rrbracket,\\{(a\mapsto(u,e^{\prime})),\ldots\\}):e\rangle$
$\displaystyle\longrightarrow\langle u,p,e^{\prime}\rangle$ (18)
$\displaystyle\langle\epsilon,.a:p,(t,o):e\rangle$
$\displaystyle\longrightarrow\langle\epsilon,.\varphi.a:p,(t,o):e\rangle\text{,}$
if $t\equiv\llbracket\ldots\rrbracket$,
$\varphi\in\operatorname{\mathsf{attr}}(t)$,
$c\notin\operatorname{\mathsf{attr}}(t)$ (19)
$\displaystyle\langle\epsilon,(a\mapsto(u,e^{\prime})):p,(\llbracket
a\mapsto\varnothing,\ldots\rrbracket,o):e\rangle$
$\displaystyle\longrightarrow\langle\epsilon,p,(\llbracket
a\mapsto\varnothing,\ldots\rrbracket,o\cup\\{a\mapsto(u,e^{\prime})\\}):e\rangle\text{,}$
if $o$ is not defined for attribute $a$ Figure 4. TAP machine for call-by-name
evaluation of $\varphi$-terms.

An object closure can be converted back to a $\varphi$-term by converting
every parent into a $\varphi$-term and then performing locator substitution,
instantiating corresponding parents. A parent $(t,o)$ is converted into a
$\varphi$-term by joining its object term $t$ with its application mapping and
converting every object closure in that mapping to a $\varphi$-term. Any
configuration $\langle t,A,P\rangle$ (or $\langle\epsilon,A,p:P\rangle$) can
be converted back to a $\varphi$-term by appending the stack of actions, where
object closures are converted to $\varphi$-terms, to the term produced from
the closure $(t,P)$ (resp. $(t,P)$ where $t$ is produced from $p$).

###### Proposition 4.2 (Soundness of TAP machine).

Let $t$ be a closed $\varphi$-term. Then starting from configuration
$C_{0}=\langle t,\epsilon,\epsilon\rangle$ TAP machine operates for finitely
many steps if and only if $t$ has a weak head normal form. Moreover, if it
stops with configuration $C_{n}$ then this configuration corresponds to the
weak head normal form of $t$.

###### Proof.

Each reduction in call-by-name evaluation sequence corresponds unambiguously
to zero or more transitions of the TAP machine. Transitions from equivalent
configurations, corresponding to the same $\varphi$-term, destructure current
term, so there can only be a finite sequence of them. ∎

##  5\. Translation to $\lambda$-calculus

In this section we compare $\varphi$-calculus with $\lambda$-calculus, present
translation rules from one to the other, and prove soundness of the
translation.

###  5.1. $\lambda$-calculus with records

We will use Mitchell Wand’s $\lambda$-calculus with records (Wand, 1991),
including both record extension (via with-expression) and record
concatenation. As we will be translating locators approximately to de Bruijn
indices in $\lambda$-terms, we will focus on a nameless variation of the
syntax.

One important detail for us will be the computation rule for record extension.
We will consider a term of the form $e\;\text{{with}}\;\\{\ldots\\}$ in weak
head normal form, and extend the $\lambda$-calculus with the following
evaluation rules:

$\displaystyle(e\;\text{{with}}\;\\{a=e_{a},\ldots\\}).a$
$\displaystyle\longrightarrow e_{a}$
$\displaystyle(e\;\text{{with}}\;\\{\ldots\\}).a$
$\displaystyle\longrightarrow e.a\quad\text{if $a$ is not in \\{\ldots\\}}$

This slight modification of Wand’s calculus allows strictly more terms to
avoid diverging computation, and is crucial for translation of decorators from
$\varphi$-calculus.

###  5.2. Translation from $\varphi$-calculus to $\lambda$-calculus

_Syntax of nameless $\lambda$-calculus with records_ (de Bruijn index)
$\displaystyle e$ $\displaystyle:=\underline{n}$ (abstraction)
$\displaystyle\mid\lambda e$ (application) $\displaystyle\mid(e_{1})e_{2}$
(record) $\displaystyle\mid\\{a_{1}=e_{1},\ldots,a_{n}=e_{n}\\}$ (attribute)
$\displaystyle\mid e.a$ (record extension) $\displaystyle\mid
e\;\text{{with}}\;\\{a_{1}=e_{1},\ldots,a_{n}=e_{n}\\}$ (record concatenation)
$\displaystyle\mid e_{1}\;\|\;e_{2}$ (fixed point)
$\displaystyle\mid\operatorname{\mathsf{fix}}e$ _Translation from
$\varphi$-calculus to $\lambda$-calculus_
$\displaystyle\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(\rho^{n})$
$\displaystyle:=\lambda\underline{(2n+2)}(\underline{(2n+1)}\;\|\;\underline{0})$
$\displaystyle\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t.a)$
$\displaystyle:=(\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t)\;\\{\\}).a$
$\displaystyle\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t(a\mapsto
u))$
$\displaystyle:=\lambda(\operatorname{\mathsf{inc}}_{\lambda}(\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t)))(\underline{0}\;\text{{with}}\;\\{a=\operatorname{\mathsf{inc}}_{\lambda}(\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(u))\\})$
$\displaystyle\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(\llbracket
a_{i}\mapsto\varnothing,\ldots,b_{j}\mapsto
t_{j},\varphi\mapsto\ldots\rrbracket)$
$\displaystyle:=\operatorname{\mathsf{fix}}(\lambda\lambda((\underline{1}\;\underline{0}).\varphi\;\\{\\})\;\text{{with}}\;\\{a_{i}=0.a_{i},\ldots,b_{j}=\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t_{j})\\})$
$\displaystyle\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(\llbracket
a_{i}\mapsto\varnothing,\ldots,b_{j}\mapsto t_{j}\rrbracket)$
$\displaystyle:=\operatorname{\mathsf{fix}}(\lambda\lambda\\{\ldots,a_{i}=0.a_{i},\ldots,b_{j}=\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t_{j}),\ldots\\})$
Figure 5. Translation from $\varphi$-calculus to $\lambda$-calculus with
records.

To translate $\varphi$-terms to $\lambda$-terms, one must understand how to
represent objects. Since records have nothing like void attributes, we cannot
map void attributes directly to record attributes. So, instead, we will
represent objects as functions taking records with instantiated void
attributes. For example, we would like to represent an empty object
$\llbracket\rrbracket$ as a constant function $\lambda\\{\\}$, and an object
$\llbracket x\mapsto\varnothing,y\mapsto\llbracket\rrbracket\rrbracket$ as a
function $\lambda\\{x=0.x,y=\lambda\\{\\}\\}$.

Since locators enable referencing outer terms, for translation we will also
make use of the fixpoint combinator. In particular, a term $\llbracket
x\mapsto\rho^{0}\rrbracket$ should be translated into
$\operatorname{\mathsf{fix}}(\lambda\lambda\\{x=\lambda(2\;(1\;\text{{with}}\;0)\\})$.
Note that the outermost $\lambda$ introduces the translated object
(represented as a function) that is then referenced as $2$ in
$2\;(1\;\text{{with}}\;0)$. $1$ references the instantiated void attributes
passed to the outer term, and $0$ references the instantiated void attributes
passed to the locator $\rho^{0}$.

In general, translation objects terms involves two $\lambda$-abstractions. One
abstraction is used together with the fixed point combinator, to allow
locators. And another one is used to properly represent void attributes. So,
when translating locator $\rho^{n}$ we need to represent it so that it
references the proper outer term and corresponding void attributes. That is
why we translate $\rho^{n}$ to
$\lambda\underline{2n+2}(\underline{2n+1}\;\|\;\underline{0})$. All the other
translation rules follow naturally and are presented in Figure 5.

###  5.3. Soundness of translation

The translation is sound if it commutes with computation. That is, given
$\varphi$-terms $t$ and $u$ such that
$t\operatorname{\rightsquigarrow}_{\varphi}u$, we have
$\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t)\approx\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(u)$.
Intuitively, by $e_{1}\approx e_{2}$ we mean that $e_{1}$ and $e_{2}$ are
observationally equivalent. More precisely, $e_{1}\approx e_{2}$ if and only
if $e_{1}$ is $\beta\eta\zeta$-equivalent to $e_{2}$. Here by
$\zeta$-equivalence we mean the obvious congruence rules, like associativity
of $\|$: $x\;\|\;(y\;\|\;z)\approx_{\zeta}(x\;\|\;y)\;\|\;z$.

###### Proposition 5.1.

Let $t,u$ be $\varphi$-terms and
$t\operatorname{\rightsquigarrow}_{\varphi}u$. Then

$\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t)\approx\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(u)$

###### Proof.

Straightforward by induction on $t\operatorname{\rightsquigarrow}_{\varphi}u$.
∎

###### Theorem 5.2 (Soundness of
$\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}$).

Let $t,t^{\prime}$ be $\varphi$-terms such that
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}_{\varphi}t^{\prime}$.
Then

$\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t)\approx\operatorname{\operatorname*{\mathsf{trans}}_{\varphi\to\lambda}}(t^{\prime})$

###### Proof.

Follows from Proposition 5.1 and confluence of $\lambda$-calculus. ∎

###  5.4. Translation from $\lambda$-calculus to $\varphi$-calculus

The translation from $\varphi$-calculus aimed to map attributes of objects in
$\varphi$-terms to attributes of records in $\lambda$-calculus. Unfortunately,
such mapping is impossible in the backwards direction, unless we drop the
record concatenation. Indeed, record concatenation cannot be translated to
$\varphi$-calculus directly, as the latter does not support any mechanism for
merging objects.

There exist two remaining options for translation from $\lambda$-calculus.
First, we could translate only the segment without record concatenation. Such
translation is possible under assumption that attributes map to attributes.
However, as record concatenation is important for translation of locators from
$\varphi$-calculus, this option is not ideal, as we only have full translation
in one direction. Second, we can encode attributes and records, for example,
using Church encoding. This would effectively translate $\lambda$-terms with
records to mere $\lambda$-terms, which can then be translated to
$\varphi$-calculus.

As we do not see a satisfactory translation from $\lambda$-calculus to
$\varphi$-calculus, we propose, as a potential future work, an extension of
$\varphi$-calculus with object concatenation.

###  5.5. $\varphi$-calculus versus $\lambda$-calculus

$\varphi$-calculus shares some common features with various $\lambda$-calculi
as both are confluent term-rewriting systems capturing the notion of
computability. Yet, $\varphi$-calculus focused on objects differs from
$\lambda$-calculus in the following important ways:

  1. (1)

$\varphi$-calculus does not rely on $\lambda$-terms to represent functions. In
$\varphi$-calculus everything is an object (in the sense of Definition 2.1).

  2. (2)

The attribute access in $\varphi$-calculus is more powerful than that of
$\lambda$-calculus with records, since evaluation of the former involves
substitution, essentially incorporating the expressive power of a fixpoint
combinator. In fact attribute access shares certain similarities with with
$\beta$-reduction in $\lambda$-calculus because of the substitution involved.

  3. (3)

Because of the decorators, $\varphi$-calculus requires no explicit analogue of
fixpoint combinator. In a sense, objects have a recursive
$\mathsf{let}$-construction built into them.

  4. (4)

The locators in $\varphi$-calculus are arguably more natural than de Bruijn
indices used in $\lambda$-calculi. Here, by “more natural” we mean the
following properties of locators as compared to de Bruijn indices:

    1. (a)

In $\lambda$-calculi de Bruijn indices are used primarily for the convenience
of algorithms, while humans prefer named function arguments. In
$\varphi$-calculus, most objects already have a name as they are typically
bound to some attribute. In fact, as we show in Section 6.1, locators can be
omitted (most of the time).

    2. (b)

When presented in text (for humans), nested objects typically are indented, so
for many examples it is easy to see which outer object the locator refers to.
This is less convenient for $\lambda$-calculi where body of
$\lambda$-abstraction is rarely indented. Besides, curried functions have
arguments numbered in ”reversed” order when using de Bruijn indices: $\lambda
x_{0}.\lambda x_{1}.\lambda x_{2}.(x_{0})\;((x_{1})\;x_{2})$ becomes
$\lambda\lambda\lambda(2)\;((1)\;0)$ when using de Bruijn indices.

Note that $\varphi$-calculus is Turing complete, as can be shown by embedding
pure $\lambda$-calculus (in de Bruijn notation) into $\varphi$-calculus:

  1. (1)

(var) $n\longleftrightarrow\rho^{n}.\mathsf{arg}$

  2. (2)

(abs) $(t\longleftrightarrow u)\Rightarrow(\lambda
t\;\longleftrightarrow\;\llbracket\mathsf{arg}\mapsto\varnothing,\mathsf{body}\mapsto
u\rrbracket)$

  3. (3)

(app) $((t_{1}\longleftrightarrow u_{1})\land(t_{2}\longleftrightarrow
u_{2}))\Rightarrow((t_{1})\;t_{2}\longleftrightarrow u_{1}(\mathsf{arg}\mapsto
u_{2}).\mathsf{body})$

This embedding can be shown to be faithful in the sense that whenever
$t\rightsquigarrow u$ we can encode $t$ in $\varphi$-calculus, compute, and
decode the result: $t\longleftrightarrow
t_{\varphi}\rightsquigarrow^{*}u_{\varphi}\longleftrightarrow u$.

As both calculi are Turing complete, it is not surprising that
$\lambda$-calculus can be embedded into $\varphi$-calculus, or vice versa.
However, $\varphi$-calculus shares enough similarities with $\lambda$-calculus
with records to enable a particular kind of a translation, where objects of
$\varphi$-calculus are, more or less, directly transated as records of
$\lambda$-calculus. Such a direct translation is possible in one direction,
and a partial111it is impossible to translate concatenation of records in this
way translation is possible the other. These translations can be used not only
to improve understanding of the two formalizations, but also to translate
certain useful properties between the systems. In particular, such a
translation might be useful to develop a sound type system for
$\varphi$-calculus in the future.

##  6\. Extensions

Bugayenko (Bugayenko, 2021a) introduces a calculus that reflects capabilities
of his EO programming language. As such it is richer than $\varphi$-calculus
we have presented in Section 2. In this section, we give examples of possible
syntactic extensions to our calculus closing the gap between the two
presentations. We leave out the more complicated extensions, such as mutable
memory, primitive data types, or modelling input/output for future work.

###  6.1. Attribute-variables

Locators are often used in combination with attribute access: $\rho^{n}.a$. In
practice, though, attribute names can be descriptive and unique (at least in a
certain scope or subterm) so that a person can understand easily which object
this attribute belongs to. Such practice prompts a version of the syntax where
locators are optional and can be omitted. For example, instead of $\llbracket
x\mapsto\rho^{0}.y,y\mapsto\llbracket z\mapsto\rho^{1}.x\rrbracket\rrbracket$
one could omit both locators and it would still be clear where attributes
should come from: $\llbracket x\mapsto y,y\mapsto{z\mapsto x}\rrbracket$.

More formally, we extend syntax of $\varphi$-terms with _attribute-variables_
:

###### Definition 6.1.

A set of $\varphi$-terms with attribute-variables $T_{a}$ is defined
inductively as follows:

  1. (1)

if $t\in T$ ($t$ is a $\varphi$-term) then $t\in T_{a}$;

  2. (2)

if $a\in\mathcal{L}$ then $a\in T_{a}$.

As long as all attributes are defined in some enclosing object, we can restore
locators. To do so we, have to traverse the term while keeping track of
locators for known attributes. For the latter we will use a context
represented by a mapping $\Gamma:\mathcal{L}\to\mathbb{N}\cup\\{\bot\\}$. For
convenience we will write $\Gamma,a\in\rho^{n}$ to mean context
$\Gamma^{\prime}$ defined as follows:

$\displaystyle\Gamma^{\prime}(a)$ $\displaystyle:=n$
$\displaystyle\Gamma^{\prime}(x)$ $\displaystyle:=\Gamma(x)\quad\text{when
$x\not=a$}$

We will also define an increment operation on the context:

$\displaystyle\Gamma\uparrow(a):=\Gamma(a)+1$

Translation from $\varphi$-terms with attribute-variables to regular
$\varphi$-terms can be summarized with the following rules:

$\Gamma,a\in\rho^{n}\vdash a\longrightarrow\rho^{n}.a$
$\Gamma\vdash\rho^{n}\longrightarrow\rho^{n}$

$\Gamma\vdash t\longrightarrow t^{\prime}$ $\Gamma\vdash t.a\longrightarrow
t^{\prime}.a$ $\Gamma\vdash t\longrightarrow t^{\prime}$ $\Gamma\vdash
u\longrightarrow u^{\prime}$ $\Gamma\vdash t(a\mapsto u)\longrightarrow
t(a\mapsto u^{\prime})$

$\Gamma\uparrow,a_{0}\in\rho^{0},\ldots,b_{1}\in\rho^{0},\ldots\vdash
t_{j}\longrightarrow t^{\prime}_{j}\quad\text{for all $j\in\\{1,\ldots,n\\}$}$
$\Gamma\vdash\llbracket a_{1}\mapsto\varnothing,\ldots,b_{1}\mapsto
t_{1},\ldots\rrbracket\longrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,b_{1}\mapsto t^{\prime}_{1},\ldots\rrbracket$

Note that, by reversing the first rule, we can similarly erase unnecessary
locators, yielding translation in the other direction.

###  6.2. Global object

Sometimes tracking nested objects might be inconvenient, and it might be
easier to reference objects “from the top-level”. This statement is especially
true in an actual programming language. One can extend calculus with explicit
names for objects to use instead of locators, but Section 6.1 already provides
a clean solution to provide a name for all terms, except for those at the top-
level.

To reference top-level object by name, we may extend syntax with _global
object locator_ $\Phi$. Similarly to attribute-variables, this extension is
purely syntactic and requires no extension of evaluation rules as a proper
locator can safely replace each occurrence of $\Phi$.

###  6.3. Positional arguments

Void attributes often serve as method arguments. To emphasize this role, we
extend the syntax with positional arguments and nameless application.

We denote by

$\llbracket\ldots,f(a_{1},\ldots,a_{k})\mapsto\llbracket\ldots\rrbracket,\ldots\rrbracket$

an object where attribute $f$ is mapped to object with attributes
$a_{1},\ldots,a_{k}$ that are mapped to special void _positional attributes_
$\pi_{1},\ldots,\pi_{k}$:

$\llbracket\pi_{1}\mapsto\varnothing,\ldots,\pi_{k}\mapsto\varnothing,a_{1}\mapsto\rho^{0}.\pi_{1},\ldots,a_{k}\mapsto\rho^{0}.\pi_{k},\ldots\rrbracket$

We denote by

$t\;t_{1}\;\ldots\;t_{n}$

an application using positional attributes:

$t(\pi_{1}\mapsto t_{1},\ldots,\pi_{n}\mapsto t_{n})$

With this syntax abstract objects can be more easily identified as methods:

###### Example 6.2.

Using extended syntax, we can rewrite Example 2.8 as follows

$\displaystyle\mathsf{Base}$ $\displaystyle:=\llbracket\mathsf{new}\mapsto$
$\displaystyle\phantom{:=\llbracket\mathsf{new}}\llbracket\mathsf{g}(\mathsf{this})\mapsto\llbracket\varphi\mapsto\mathsf{\rho^{0}.this.h(this\mapsto\rho^{0}.this).\varphi}\rrbracket,$
$\displaystyle\phantom{:=\llbracket\mathsf{new}\llbracket}\mathsf{h}(\mathsf{this})\mapsto\llbracket\varphi\mapsto
3\rrbracket\rrbracket$ $\displaystyle\phantom{:=\llbracket}\rrbracket$
$\displaystyle\mathsf{Derived}$ $\displaystyle:=\llbracket\mathsf{new}\mapsto$
$\displaystyle\phantom{:=\llbracket\mathsf{new}}\llbracket\varphi\mapsto\mathsf{Base.new},$
$\displaystyle\phantom{:=\llbracket\mathsf{new}\llbracket}\mathsf{f}(\mathsf{this})\mapsto\llbracket\varphi\mapsto\mathsf{2.add(n\mapsto\rho^{0}.this.g(this\mapsto\rho^{0}.this).\varphi)}\rrbracket,$
$\displaystyle\phantom{:=\llbracket\mathsf{new}\llbracket}\mathsf{h}(\mathsf{this})\mapsto\llbracket\varphi\mapsto
5\rrbracket\rrbracket$ $\displaystyle\phantom{:=\llbracket}\rrbracket$
$\displaystyle d$ $\displaystyle:=\mathsf{Derived}.\mathsf{new}$

##  7\. Related work

Systems based on row types and row polymorphism (Wand, 1987) were originally
introduced to model inheritance. Row types combine structural typing for
records and variants with parametric polymorphism, which simplifies type
inference. Rows can be extended (by adding new entries to the existing row)
and concatenated (by combining several rows), which can be challenging for
adoption in different typing settings and require new approaches (Chlipala,
2010). The last one introduces the Rose language, based on row types and
supporting record concatenation through its monoidal nature of row extension.
Rose uses qualified types to bind records to the rows and to abstract them
from each other and allow them to evolve independently.

Some of these theoretical attempts define only the restricted set of language
features or focus on language particular aspects to simplify the formal
reasoning and proofs. In (Igarashi, 2002), Igarashi et al. have introduced
Featherweight Java (FJ), a minimal core calculus for Java and generics. This
model supports classes (including generics), methods, fields, inheritance, and
dynamic typecasts, but omits complex features, such as interfaces,
concurrency, reflection, etc. Later, Bettini et al. has extended Featherweight
Java (Bettini et al., 2018) with a new core calculus including interfaces,
multiple inheritance, lambda-expressions and intersection types. The intention
behind the FJ&$\lambda$ tool was to add the support of a Java 8 subset to a
FJ. Bettini et al. used intersection types to typecast lambda-expressions and
conditional expressions. In (Cardelli, 1984), Cardelli presents a semantics of
multiple inheritance. In (Hailpern and Nguyen, 1987), Hailpern and Nguyen
presented a model for object-based inheritance. In (Attardi and Simi, 1982),
Attardi and Simi introduced Semantics of Inheritance and Attributions for the
Description System Omega. In (Bono and Patel, 1970), Bono et al. have
introduced a calculus for classes and mixins, and a calculus for classes and
objects.

In (Lumpe et al., 2000) Nierstrasz criticized the lack of formal semantics for
describing the concurrent-based programming languages. To address this issue
he has created the OC language which combines agents of process calculi with
functions of lambda calculi. An object is presented as a function (or agent)
with state and by making functional composition (or combining agents) software
composition is gained.

##  8\. Conclusion and future work

In this paper, we have formalized $\varphi$-calculus, a calculus of objects
with decoration as a primary mechanism of object extension. We have shown that
even though our variant of $\varphi$-calculus is not based on
$\lambda$-calculus, it possess the important properties, such as confluence
(Church-Rosser property) and completeness of normal order evaluation.

Then we introduced an abstract machine for call-by-name evaluation of
$\varphi$-terms. This machine can serve as reasoning tool for compilers and
interpreters of $\varphi$-calculus and languages based on it, such as EO
programming language.

We have also provided a sound translation from $\varphi$-calculus to
$\lambda$-calculus with records. This translation emphasizes the differences
between decoration and object extension using with-expression. Finally, we
discussed some syntactic extensions to the calculus, closing the gap between
our presentation and that of Bugayenko (Bugayenko, 2021a).

We expect two main departures for the future work. First, we could add type
system for the calculus, probably based on row types to facilitate type
inference. We suspect that typed $\varphi$-calculus can be directly translated
to $\lambda$-calculus with records and without concatenation operator, thus it
would be possible to state equivalence (in a sense of having direct
translation in both directions) between the two calculi. Second, we could
extend the calculus with the ability to decorate or compose multiple objects,
enabling simpler models for languages with multiple inheritance.

###### Acknowledgements.

This research has been generously funded by Huawei in the framework of
Polystat project. We thank Yegor Bugayenko for taking his time to explain
ideas behind EO, his version of $\varphi$-calculus, and especially his vision
regarding decorator and parent object locators. We thank Bertrand Meyer for
giving his feedback on the early version of the calculus and suggesting
terminology for “void” and “attached” attributes. We also thank Nickolay
Shilov and Larisa Safina for their feedback on the paper and different
versions of the calculus, and Georgii Gelvanovskii, for proofreading the
paper. Finally, we thank anonymous reviewers of PLDI 2022 for thorough reading
and helpful suggestions.

## References

  * (1)
  * Abadi and Cardelli (1994) Martín Abadi and Luca Cardelli. 1994.  A semantics of object types. In _Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science_. IEEE Comput. Soc. Press, Paris, France, 332–341.  https://doi.org/10.1109/LICS.1994.316056
  * Abadi and Cardelli (1996) Martín Abadi and Luca Cardelli. 1996.  A Theory of Primitive Objects: Untyped and First-Order Systems.  _Information and Computation_ 125, 2 (1996), 78–102.  https://doi.org/10.1006/inco.1996.0024
  * Attardi and Simi (1982) Giuseppe Attardi and Maria Simi. 1982.  Semantics of Inheritance and Attributions in the Description System Omega.
  * Barendregt and Barendsen (1984) Henk Barendregt and Erik Barendsen. 1984.  Introduction to lambda calculus.  _Nieuw archief voor wisenkunde_ 4 (01 1984), 337–372.
  * Bettini et al. (2018) Lorenzo Bettini, Viviana Bono, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. 2018\.  Java & Lambda: a Featherweight Story.  _Logical Methods in Computer Science ; Volume 14_ (2018).  https://doi.org/10.23638/LMCS-14(3:17)2018 arXiv: 1801.05052.
  * Black and Palsberg (1994) Andrew P. Black and Jens Palsberg. 1994.  Foundations of Object-Oriented Languages - Workshop Report.  _ACM SIGPLAN Notices_ 29, 3 (1994), 3–11.  https://doi.org/10.1145/181587.181588
  * Bono and Patel (1970) Viviana Bono and Amit Patel. 1970.  A Core Calculus of Classes and Mixins.  https://doi.org/10.1007/3-540-48743-3_3
  * Bugayenko (2021a) Yegor Bugayenko. 2021a.  EOLANG and $\varphi$-calculus.  _arXiv preprint arXiv:2111.13384_ (2021).
  * Bugayenko (2021b) Yegor Bugayenko. 2021b.  Reducing Programs to Objects.  _arXiv preprint arXiv:2112.11988_ (2021).
  * Cardelli (1984) Luca Cardelli. 1984\.  A semantics of multiple inheritance.  (1984), 51–67.
  * Chlipala (2010) Adam Chlipala. 2010\.  Ur: statically-typed metaprogramming with type-level record computation. In _PLDI ’10_.
  * Ciaffaglione et al. (2021) Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, and Luigi Liquori. 2021.  A prototype-based approach to object evolution.  _The Journal of Object Technology_ 20 (01 2021), 4:1.  https://doi.org/10.5381/jot.2021.20.2.a4
  * Clarke et al. (2001) David G. Clarke, James Noble, and John M. Potter. 2001\.  Simple Ownership Types for Object Containment.  In _ECOOP 2001 — Object-Oriented Programming_ , Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, and Jørgen Lindskov Knudsen (Eds.). Vol. 2072. Springer Berlin Heidelberg, Berlin, Heidelberg, 53–76.  https://doi.org/10.1007/3-540-45337-7_4 Series Title: Lecture Notes in Computer Science.
  * de Bruijn (1972) Nicolaas G. de Bruijn. 1972\.  Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem.  _Indagationes Mathematicae (Proceedings)_ 75, 5 (1972), 381–392.  https://doi.org/10.1016/1385-7258(72)90034-0
  * Durr and Van Katwijk (1992) Eugene Durr and Jan Van Katwijk. 1992.  VDM++, a formal specification language for object-oriented designs. In _CompEuro 1992 Proceedings Computer Systems and Software Engineering_. IEEE Comput. Soc. Press, The Hague, Netherlands, 214–219.  https://doi.org/10.1109/CMPEUR.1992.218511
  * Fisher et al. (1993) Kathleen Fisher, Furio Honsell, and John C. Mitchell. 1993\.  A lambda calculus of objects and method specialization.  _Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science_ (1993), 26–38.
  * Gamma et al. (1995) Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. 1995.  _Design Patterns: Elements of Reusable Object-Oriented Software_.  Addison-Wesley Longman Publishing Co., Inc., USA.
  * Girard et al. (1989) Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989\.  _Proofs and Types_.  Cambridge University Press, USA.
  * Hailpern and Nguyen (1987) Brent Hailpern and Van Nguyen. 1987.  A Model for Object-Based Inheritance. In _Research Directions in Object-Oriented Programming_.
  * Igarashi (2002) Atsushi Igarashi. 2002\.  Featherweight Java: A Minimal Core Calculus for Java and GJ.  _ACM Transactions on Programming Languages and Systems_ 23, 3 (2002), 55\.
  * Krivine (1993) Jean L. Krivine. 1993\.  _Lambda-Calculus, Types and Models_.  Ellis Horwood, USA.
  * Lumpe et al. (2000) Markus Lumpe, Franz Achermann, and Oscar Nierstrasz. 2000\.  A Formal Language for Composition.  (07 2000).
  * Pierce and Turner (1993) Benjamin C. Pierce and David N. Turner. 1993.  Simple Type-Theoretic Foundations for Object-Oriented Programming.
  * Smith (2000) Graeme Smith. 2000\.  Concrete Syntax.  In _The Object-Z Specification Language_ , Graeme Smith (Ed.). Springer US, Boston, MA, 133–142.  https://doi.org/10.1007/978-1-4615-5265-9_6
  * Takahashi (1995) Masako Takahashi. 1995\.  Parallel Reductions in $\lambda$-Calculus.  _Information and Computation_ 118, 1 (1995), 120–127.  https://doi.org/10.1006/inco.1995.1057
  * Wand (1987) Mitchell Wand. 1987\.  Complete Type Inference for Simple Objects. In _LICS_.
  * Wand (1991) Mitchell Wand. 1991\.  Type inference for record concatenation and multiple inheritance.  _Information and Computation_ 93, 1 (1991), 1–15.  https://doi.org/10.1016/0890-5401(91)90050-C Selections from 1989 IEEE Symposium on Logic in Computer Science.
  * Wolczko and Jones (1988) Mario I Wolczko and Cliff Jones. 1988.  _Semantics of object-oriented languages_.  Ph.D. Dissertation. Citeseer.

##  Appendix A Complete proofs

###  A.1. Confluence

###### Proposition A.1 (Reflexivity of parallel reduction).

Let $t$ be a $\varphi$-term. Then $t\Rrightarrow t$.

###### Proof.

We prove this by induction on the structure of $t$:

  1. (1)

if $t=u.c$ then by the inductive assumption $u\Rrightarrow u$ and by rule
$\text{cong}_{\text{DOT}}^{\Rrightarrow}$ we have $u.c\Rrightarrow u.c$, i.e.
$t\Rrightarrow t$;

  2. (2)

if $t=t_{1}(c\mapsto t_{2})$ then by the inductive assumption
$t_{1}\Rrightarrow t_{1}$ and $t_{2}\Rrightarrow t_{2}$; but then by
$\text{cong}_{\text{APP}}^{\Rrightarrow}$ we have $t_{1}(c\mapsto
t_{2})\Rrightarrow t_{1}(c\mapsto t_{2})$;

  3. (3)

if $t=\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ then by inductive assumption we
have $t_{i}\Rrightarrow t_{i}$ for each $i\in\\{1,\ldots,n\\}$ and by
$\text{cong}_{\text{OBJ}}^{\Rrightarrow}$ we have $t\Rrightarrow t$;

  4. (4)

finally, if $t=\rho^{n}$ then $t\Rrightarrow t$ by
$\text{cong}_{\rho}^{\Rrightarrow}$.

∎

###### Definition A.2.

Relation $\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}$ is
given by

$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t$
$t\operatorname{\rightsquigarrow}t^{\prime}$
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime\prime}$
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime\prime}$

###### Lemma A.3 (Transitivity of
$\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}$).

For any $\varphi$-terms $t,t^{\prime},t^{\prime\prime}$, if
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
and
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime\prime}$,
then
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime\prime}$.

###### Lemma A.4 (Congruence reductions for
$\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}$).

For any $\varphi$-terms $t,t^{\prime}$,
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
implies

  1. (1)

$\llbracket\ldots,b\mapsto
t,\ldots\rrbracket\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}\llbracket\ldots,b\mapsto
t^{\prime},\ldots\rrbracket$,

  2. (2)

$t.c\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}.c$,

  3. (3)

$t(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}(c\mapsto
u)$,

  4. (4)

$s(c\mapsto
t)\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}s(c\mapsto
t^{\prime})$.

###### Proof.

Proof by induction on the definition of
$\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}$.

Assume as an induction hypothesis that
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
implies congruent reductions for
$\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}$, stated
above. Let $t^{\prime\prime}\operatorname{\rightsquigarrow}t$, so that
$t^{\prime\prime}\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t$.
Then

  1. (1)

$\llbracket\ldots,b\mapsto
t^{\prime\prime},\ldots\rrbracket\operatorname{\rightsquigarrow}\llbracket\ldots,b\mapsto
t,\ldots\rrbracket$ by $\text{cong}_{\text{OBJ}}$, so
$\llbracket\ldots,b\mapsto
t^{\prime\prime},\ldots\rrbracket\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}\llbracket\ldots,b\mapsto
t^{\prime},\ldots\rrbracket$

  2. (2)

$t^{\prime\prime}.c\operatorname{\rightsquigarrow}t.c$ by
$\text{cong}_{\text{DOT}}$, so
$t^{\prime\prime}.c\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}.c$

  3. (3)

$t^{\prime\prime}(c\mapsto u)\operatorname{\rightsquigarrow}t(c\mapsto u)$ by
cong${}_{\text{APP}^{\text{L}}}$, so $t^{\prime\prime}(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}(c\mapsto
u)$

  4. (4)

$s.(c\mapsto t)\operatorname{\rightsquigarrow}s(c\mapsto t^{\prime})$ by
cong${}_{\text{APP}^{\text{R}}}$, so $s(c\mapsto
t^{\prime\prime})\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}s(c\mapsto
t^{\prime})$

∎

###### Proposition A.5 (Equivalence of $\Rrightarrow$ and $\rightsquigarrow$).

Parallel reduction ($\Rrightarrow$) is equivalent to regular reduction
($\rightsquigarrow$):

  1. (1)

$t\rightsquigarrow t^{\prime}$ implies $t\Rrightarrow t^{\prime}$

  2. (2)

$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime}$

  3. (3)

$t\Rrightarrow t^{\prime}$ implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$

  4. (4)

$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime}$
implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$

###### Proof.

Since parallel reduction does “zero or more” reductions in a term, it is easy
to see that regular reduction implies parallel reduction. On the other hand, a
single step of parallel reduction implies several consecutive steps of regular
reduction. This is a bit harder to prove, but is still rather straightforward.

  1. (1)

If $t\rightsquigarrow t^{\prime}$ by DOTc, DOT${}_{c}^{\varphi}$, or APPc,
then by reflexivity and corresponding rules of parallel reduction
(DOT${}_{c}^{\Rrightarrow}$, DOT${}_{c}^{\varphi\Rrightarrow}$,
APP${}_{c}^{\Rrightarrow}$), $t\Rrightarrow t^{\prime}$. To prove this
implication for congruence reductions, assume as the induction hypothesis that
$t\rightsquigarrow t^{\prime}$ implies $t\Rrightarrow t^{\prime}$. Then

    1. (a)

$\llbracket\ldots,c\mapsto
t,\ldots\rrbracket\rightsquigarrow\llbracket\ldots,c\mapsto
t^{\prime},\ldots\rrbracket$ implies $\llbracket\ldots,c\mapsto
t,\ldots\rrbracket\Rrightarrow\llbracket\ldots,c\mapsto
t^{\prime},\ldots\rrbracket$ by induction hypothesis, reflexivity of parallel
reduction and $\text{cong}_{\text{OBJ}}^{\Rrightarrow}$.

    2. (b)

$t.c\rightsquigarrow t^{\prime}.c$ implies $t.c\Rrightarrow t^{\prime}.c$ by
induction hypothesis and DOT${}_{c}^{\Rrightarrow}$.

    3. (c)

$t(c\mapsto u)\rightsquigarrow t^{\prime}(c\mapsto u)$ implies $t(c\mapsto
u)\Rrightarrow t^{\prime}(c\mapsto u)$ and $t_{1}(c\mapsto t)\rightsquigarrow
t_{1}(c\mapsto t^{\prime})$ implies $t_{1}(c\mapsto t)\Rrightarrow
t_{1}(c\mapsto t^{\prime})$ by induction hypothesis, reflexivity of parallel
reduction and APP${}_{c}^{\Rrightarrow}$.

  2. (2)

$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t$ holds due to
reflexivity; assume as an induction hypothesis that
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime}$. As
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime\prime}$,
these exists $t^{\prime}$, such that
$t\operatorname{\rightsquigarrow}t^{\prime}$ and
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime\prime}$.
By (1) of this proposition, $t\Rrightarrow t^{\prime}$, which, combined with
the induction hypothesis, results in
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime\prime}$.

  3. (3)

Assume $t\Rrightarrow t^{\prime}$ implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
as an induction hypothesis.

    1. (a)

cong${}_{\text{OBJ}}^{\Rrightarrow}$. If $t\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ and $t^{\prime}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{n}\mapsto t_{n}^{\prime}\rrbracket$, then
$t_{i}\Rrightarrow t_{i}^{\prime}$ for $i\in\\{1,\ldots,n\\}$, and, by
induction hypothesis,
$t_{i}\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t_{i}^{\prime}$.

Let $t^{\\_i}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{i}\mapsto t_{i}^{\prime},b_{i+1}\mapsto
t_{i+1},\ldots b_{n}\mapsto t_{n}\rrbracket$ for $i\in\\{0,\ldots,n\\}$.
Observe that $t^{\\_0}\equiv t$, $t^{\\_n}\equiv t^{\prime}$, and, by lemma
for congruence reductions for
($\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}$),
$t^{\\_i-1}\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\\_i}$.
Finally, by lemma about transitivity,
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$.

    2. (b)

cong${}_{\rho}^{\Rrightarrow}$.
$\rho^{n}\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}\rho^{n}$
holds due to reflexivity of
($\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}$).

    3. (c)

cong${}_{\text{DOT}}^{\Rrightarrow}$. If $t.c\Rrightarrow t^{\prime}.c$, then
$t\Rrightarrow t^{\prime}$, then
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
by induction hypothesis and
$t.c\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}.c$
by lemma 2.

    4. (d)

cong${}_{\text{APP}}^{\Rrightarrow}$. If $t(c\mapsto u)\Rrightarrow
t^{\prime}(c\mapsto u^{\prime})$, then $t\Rrightarrow t^{\prime}$ and
$u\Rrightarrow u^{\prime}$. By induction hypothesis,
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
and
$u\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}u^{\prime}$.
By lemma 2, $t(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}(c\mapsto
u)$ and $t^{\prime}(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}(c\mapsto
u^{\prime})$, which can be combined by lemma 1 to yield $t(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}(c\mapsto
u^{\prime})$.

    5. (e)

DOT${}_{c}^{\Rrightarrow}$. Let reduction $t.c\Rrightarrow
t_{c}\left[\xi\mapsto t^{\prime}\right]$ happen because $t\Rrightarrow
t^{\prime}$ and $t^{\prime}\equiv\llbracket\ldots,c\mapsto
t_{c},\ldots\rrbracket$. By inductive hypothesis,
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$;
by lemma 2,
$t.c\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}.c$.
By rule DOTc of regular reduction,
$t^{\prime}.c\operatorname{\rightsquigarrow}t_{c}\left[\xi\mapsto
t^{\prime}\right]$ (and hence
$t^{\prime}.c\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t_{c}\left[\xi\mapsto
t^{\prime}\right]$). By lemma about transitivity,
$t.c\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t_{c}\left[\xi\mapsto
t^{\prime}\right]$.

    6. (f)

Proof for other rules (DOT${}_{c}^{\varphi\Rrightarrow}$,
APP${}_{c}^{\Rrightarrow}$) is analogous to the one for
DOT${}_{c}^{\Rrightarrow}$: by induction hypothesis, establish
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$
(and
$u\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}u^{\prime}$
in case of APP), apply congruence for rt-closure of regular reduction, use
respective rule of regular reduction, and combine results with the lemma about
transitivity.

  4. (4)

$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t$ holds by
definition. Assume as an induction hypothesis that
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime}$
implies
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$.
Let
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime\prime}$
hold because $t\Rrightarrow t^{\prime}$ and
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\ast}}{{\Rrightarrow}}}t^{\prime\prime}$.
By (3) of this proposition,
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime}$.
By the induction hypothesis,
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime\prime}$,
and with A.3,
$t\operatorname{\stackrel{{\scriptstyle\ast}}{{\rightsquigarrow}}}t^{\prime\prime}$.

∎

###### Proposition A.6 (Proposition 3.8).

Let $t,t^{\prime}$ be $\varphi$-terms and $t\Rrightarrow t^{\prime}$. Then
$t^{\prime}~{}\Rrightarrow~{}t^{+}$.

###### Proof.

Assume as an induction hypothesis that if $t\Rrightarrow t^{\prime}$ then
$t^{\prime}\Rrightarrow t^{+}$.

  1. (1)

cong${}_{\text{OBJ}}^{\Rrightarrow}$: If $\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket\Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{n}\mapsto t_{n}^{\prime}\rrbracket$, then
$t_{i}\Rrightarrow t_{i}^{\prime}$ for all $i\in\\{1,\ldots,n\\}$. By
induction hypothesis, $t_{i}\Rrightarrow t_{i}^{+}$, hence $\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{n}\mapsto
t_{n}^{\prime}\rrbracket\Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{+},\ldots,b_{n}\mapsto t_{n}^{+}\rrbracket$ by
cong${}_{\text{OBJ}}^{\Rrightarrow}$.

  2. (2)

cong${}_{\rho}^{\Rrightarrow}$: $t\equiv\rho^{i}\Rrightarrow\rho^{i}\equiv
t^{\prime}\equiv\rho^{i}\Rrightarrow\rho^{i}\equiv t^{+}$.

  3. (3)

cong${}_{\text{DOT}}^{\Rrightarrow}$: If $t.c\Rrightarrow t^{\prime}.c$, then
$t\Rrightarrow t^{\prime}$ and by induction hypothesis,
$t^{\prime}\Rrightarrow t^{+}$.

$\displaystyle t^{\prime}.c\Rrightarrow\begin{cases}t_{c}[\rho^{0}\mapsto
t^{+}],&\text{by DOT${}_{c}^{\Rrightarrow}$, if
$t^{+}\equiv\llbracket\ldots,c\mapsto t_{c},\ldots\rrbracket$}\\\
t^{+}.\varphi.c,&\text{by DOT${}_{c}^{\varphi\Rrightarrow}$, if
$c\notin\operatorname{\mathsf{attr}}(t^{+})$ and
$\varphi\in\operatorname{\mathsf{attr}}(t^{+})$}\\\ t^{+}.c&\text{by
cong${}_{\text{DOT}}^{\Rrightarrow}$, otherwise}\end{cases}$

Hence, $t^{\prime}.c\Rrightarrow(t.c)^{+}$.

  4. (4)

cong${}_{\text{APP}}^{\Rrightarrow}$: If $t(c\mapsto u)\Rrightarrow
t^{\prime}(c\mapsto u^{\prime})$, then $t\Rrightarrow t^{\prime}$ and
$u\Rrightarrow u^{\prime}$. By induction hypothesis, $t^{\prime}\Rrightarrow
t^{+}$ and $u^{\prime}\Rrightarrow u^{+}$.

$\displaystyle t^{\prime}(c\mapsto
u^{\prime})\Rrightarrow\begin{cases}\llbracket\ldots,c\mapsto
u^{+}\uparrow,\ldots\rrbracket,&\text{by APP${}_{c}^{\Rrightarrow}$, if
$t^{+}\equiv\llbracket\ldots,a\mapsto\varnothing,\ldots\rrbracket$}\\\
t^{+}(c\mapsto u^{+})&\text{by cong${}_{\text{APP}}^{\Rrightarrow}$,
otherwise}\end{cases}$

Hence, $t^{\prime}(c\mapsto u^{\prime})\Rrightarrow(t(c\mapsto u))^{+}$.

  5. (5)

DOT${}_{c}^{\Rrightarrow}$: If $t.c\Rrightarrow t_{c}[\xi\mapsto t^{\prime}]$,
where $t\Rrightarrow t^{\prime}\equiv\llbracket\ldots,c\mapsto
t_{c},\ldots\rrbracket$, then, by induction hypothesis,
$t^{\prime}\Rrightarrow t^{+}$, and as there is unique rule that allows
reduction of an object (cong${}_{\text{OBJ}}^{\Rrightarrow}$),
$t^{+}\equiv\llbracket\ldots,c\mapsto t_{c}^{\prime},\ldots\rrbracket$, with
$t_{c}\Rrightarrow t_{c}^{\prime}$. By substitution lemma, $t_{c}[\xi\mapsto
t^{\prime}]\Rrightarrow t_{c}^{\prime}[\xi\mapsto t_{c}^{+}]\equiv(t.c)^{+}$.

  6. (6)

DOT${}_{c}^{\varphi\Rrightarrow}$: Let $t.c\Rrightarrow t^{\prime}.\varphi.c$,
where $t\Rrightarrow t^{\prime}\equiv\llbracket\ldots\rrbracket$, and
$c\notin\operatorname{\mathsf{attr}}(t^{\prime})$ and
$\varphi\in\operatorname{\mathsf{attr}}(t^{\prime})$. By induction hypothesis,
$t^{\prime}\Rrightarrow t^{+}$, and $t^{+}\equiv\llbracket\ldots\rrbracket$,
s.t. as for $t^{\prime}$, $c\notin\operatorname{\mathsf{attr}}(t^{+})$ and
$\varphi\in\operatorname{\mathsf{attr}}(t^{+})$. Hence, $(t.c)^{+}\equiv
t^{+}.\varphi.c$. By cong${}_{\text{DOT}}^{\Rrightarrow}$,
$t^{\prime}.\varphi\Rrightarrow t^{+}.\varphi$ and
$t^{\prime}.\varphi.c\Rrightarrow t^{+}.\varphi.c$.

  7. (7)

APP${}_{c}^{\Rrightarrow}$: Let $t(c\mapsto u)\Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
u^{\prime}\uparrow,b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$,
where $t\Rrightarrow t^{\prime}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ and $u\Rrightarrow u^{\prime}$. By
induction hypothesis, $u^{\prime}\Rrightarrow u^{+}$ and
$t^{\prime}\Rrightarrow t^{+}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{n}\mapsto t_{n}^{\prime}\rrbracket$. Observe that for
all $i\in\\{1,\ldots,n\\}$, $t_{i}\Rrightarrow t_{i}^{\prime}$. Note that it
is not required that $t_{i}^{\prime}\equiv t_{i}^{+}$. Complete development of
$(t(c\mapsto u))$ is $\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
u^{+}\uparrow,b_{1}\mapsto t_{1}^{\prime},\ldots,b_{n}\mapsto
t_{n}^{\prime}\rrbracket$. By cong${}_{\text{OBJ}}^{\Rrightarrow}$,
$\llbracket a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
u^{\prime}\uparrow,b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto
t_{n}\rrbracket\Rrightarrow t(c\mapsto u)^{+}$

∎

###### Lemma A.7 (Substitutions reordering).

For all $i,j\in\mathbb{N}$, $j\leq i$,

$t[\rho^{j}\mapsto u][\rho^{i}\mapsto v]\equiv t[\rho^{i+1}\mapsto
v\uparrow][\rho^{j}\mapsto u[\rho^{i}\mapsto v]]$

This lemma encapsulates equivalence between multiple substitutions resulting
from several DOTc reductions performed in a different order, respecting
nesting relationship between objects.

###### Proof.

By induction on $t$:

  1. (1)

$t\equiv\rho^{k}$

if $k<j$ then $\displaystyle\rho^{k}[\rho^{j}\mapsto u][\rho^{i}\mapsto
v]\equiv\rho^{k}[\rho^{i}\mapsto v]\equiv\rho^{k}$
$\displaystyle\rho^{k}[\rho^{i+1}\mapsto v\uparrow][\rho^{j}\mapsto
u[\rho^{i}\mapsto v]]\equiv\rho^{k}[\rho^{j}\mapsto u[\rho^{i}\mapsto
v]]\equiv\rho^{k}$ if $k\equiv j$ then $\displaystyle\rho^{j}[\rho^{j}\mapsto
u][\rho^{i}\mapsto v]\equiv u[\rho^{i}\mapsto v]$
$\displaystyle\rho^{j}[\rho^{i+1}\mapsto v\uparrow][\rho^{j}\mapsto
u[\rho^{i}\mapsto v]]\equiv\rho^{j}[\rho^{j}\mapsto u[\rho^{i}\mapsto
v]]\equiv u[\rho^{i}\mapsto v]$ if $j<k\leq i$ then
$\displaystyle\rho^{k}[\rho^{j}\mapsto u][\rho^{i}\mapsto
v]\equiv\rho^{k-1}[\rho^{i}\mapsto v]\equiv\rho^{k-1}$
$\displaystyle\rho^{k}[\rho^{i+1}\mapsto v\uparrow][\rho^{j}\mapsto
u[\rho^{i}\mapsto v]]\equiv\rho^{k}[\rho^{j}\mapsto u[\rho^{i}\mapsto
v]]\equiv\rho^{k-1}$ if $k\equiv i+1$ then
$\displaystyle\rho^{i+1}[\rho^{j}\mapsto u][\rho^{i}\mapsto
v]\equiv\rho^{i}[\rho^{i}\mapsto v]\equiv v$
$\displaystyle\rho^{i+1}[\rho^{i+1}\mapsto v\uparrow][\rho^{j}\mapsto
u[\rho^{i}\mapsto v]]\equiv v\uparrow[\rho^{j}\mapsto u[\rho^{i}\mapsto
v]]\equiv v$ if $k\geq i+2$ then $\displaystyle\rho^{k}[\rho^{j}\mapsto
u][\rho^{i}\mapsto v]\equiv\rho^{k-1}[\rho^{i}\mapsto v]\equiv\rho^{k-2}$
$\displaystyle\rho^{k}[\rho^{i+1}\mapsto v\uparrow][\rho^{j}\mapsto
u[\rho^{i}\mapsto v]]\equiv\rho^{k-1}[\rho^{j}\mapsto u[\rho^{i}\mapsto
v]]\equiv\rho^{k-2}$

  2. (2)

$t\equiv s.a$

$s.a[\rho^{j}\mapsto u][\rho^{i}\mapsto v]\equiv s[\rho^{j}\mapsto
u][\rho^{i}\mapsto v].a\equiv\\\ s[\rho^{i+1}\mapsto
v\uparrow][\rho^{j}\mapsto u[\rho^{i}\mapsto v]].a\equiv s.a[\rho^{i+1}\mapsto
v\uparrow][\rho^{j}\mapsto u[\rho^{i}\mapsto v]]$

  3. (3)

$t\equiv s_{1}(a\mapsto s_{2})$

$s_{1}(a\mapsto s_{2})[\rho^{j}\mapsto u][\rho^{i}\mapsto v]\equiv
s_{1}[\rho^{j}\mapsto u][\rho^{i}\mapsto v](a\mapsto s_{2}[\rho^{j}\mapsto
u][\rho^{i}\mapsto v])\equiv\\\ s_{1}[\rho^{i+1}\mapsto
v\uparrow][\rho^{j}\mapsto u[\rho^{i}\mapsto v]](a\mapsto
s_{2}[\rho^{i+1}\mapsto v\uparrow][\rho^{j}\mapsto u[\rho^{i}\mapsto
v]])\equiv\\\ s_{1}(a\mapsto s_{2})[\rho^{i+1}\mapsto
v\uparrow][\rho^{j}\mapsto u[\rho^{i}\mapsto v]]$

  4. (4)

$t\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$

$\displaystyle t[\rho^{j}\mapsto u]$ $\displaystyle[\rho^{i}\mapsto v]$
$\displaystyle\equiv\llbracket\ldots,b_{l}\mapsto t_{l}[\rho^{j+1}\mapsto
u][\rho^{i+1}\mapsto v],\ldots\rrbracket$
$\displaystyle\equiv\llbracket\ldots,b_{l}\mapsto t_{l}[\rho^{i+2}\mapsto
v\uparrow][\rho^{j+1}\mapsto u[\rho^{i+1}\mapsto v]],\ldots\rrbracket$
$\displaystyle\equiv t[\rho^{i+1}\mapsto v\uparrow][\rho^{j}\mapsto
u[\rho^{i}\mapsto v]]$

∎

###### Lemma A.8 (Increment and substitution swap).

For any $\varphi$-term $t$, for any $i,j\in\mathbb{N}$ such that $j\leq i$,
$t\uparrow{}^{j}[\rho^{i+1}\mapsto u\uparrow{}^{j}]\equiv t[\rho^{i}\mapsto
u]\uparrow{}^{j}$.

###### Proof.

By induction on $t$:

  1. (1)

$t\equiv\rho^{k}$

if $k<j$ then $\displaystyle\rho^{k}\uparrow{}^{j}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv\rho^{k}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv\rho^{k}$ $\displaystyle\rho^{k}[\rho^{i}\mapsto
u]\uparrow{}^{j}\equiv\rho^{k}\uparrow{}^{j}\equiv\rho^{k}$ if $j\leq k<i$
then $\displaystyle\rho^{k}\uparrow{}^{j}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv\rho^{k+1}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv\rho^{k+1}$ $\displaystyle\rho^{k}[\rho^{i}\mapsto
u]\uparrow{}^{j}\equiv\rho^{k}\uparrow{}^{j}\equiv\rho^{k+1}$ if $k\equiv i$
then $\displaystyle\rho^{i}\uparrow{}^{j}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv\rho^{i+1}[\rho^{i+1}\mapsto u\uparrow{}^{j}]\equiv
u\uparrow{}^{j}$ $\displaystyle\rho^{i}[\rho^{i}\mapsto u]\uparrow{}^{j}\equiv
u\uparrow{}^{j}$ if $k>i$ then
$\displaystyle\rho^{k}\uparrow{}^{j}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv\rho^{k+1}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv\rho^{k}$ $\displaystyle\rho^{k}[\rho^{i}\mapsto
u]\uparrow{}^{j}\equiv\rho^{k-1}\uparrow{}^{j}\equiv\rho^{k}$

  2. (2)

$t\equiv s.a$

$s.a\uparrow{}^{j}[\rho^{i+1}\mapsto u\uparrow{}^{j}]\equiv
s\uparrow{}^{j}[\rho^{i+1}\mapsto u\uparrow{}^{j}].a\equiv s[\rho^{i}\mapsto
u]\uparrow{}^{j}.a\equiv s.a[\rho^{i}\mapsto u]\uparrow{}^{j}$

  3. (3)

$t\equiv s_{1}(a\mapsto s_{2})$

$\displaystyle s_{1}(a\mapsto s_{2})\uparrow{}^{j}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv s_{1}\uparrow{}^{j}[\rho^{i+1}\mapsto
u\uparrow{}^{j}](a\mapsto s_{2}\uparrow{}^{j}[\rho^{i+1}\mapsto
u\uparrow{}^{j}])$ $\displaystyle\equiv s_{1}[\rho^{i}\mapsto
u]\uparrow{}^{j}(a\mapsto s_{2}[\rho^{i}\mapsto u]\uparrow{}^{j})\equiv
s_{1}(a\mapsto s_{2})[\rho^{i}\mapsto u]\uparrow{}^{j}$

  4. (4)

$t\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$. Proof by unfolding the definitions
of substitution and increment, swapping increments, applying induction
hypothesis, and folding the definitions back:

$\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket\uparrow{}^{j}[\rho^{i+1}\mapsto
u\uparrow{}^{j}]\equiv$ $\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}\uparrow{}^{j+1}[\rho^{i+2}\mapsto
u\uparrow{}^{j}\uparrow],\ldots,b_{n}\mapsto
t_{n}\uparrow{}^{j+1}[\rho^{i+2}\mapsto
u\uparrow{}^{j}\uparrow]\rrbracket\equiv$ $\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}\uparrow{}^{j+1}[\rho^{i+2}\mapsto
u\uparrow\uparrow{}^{j+1}],\ldots,b_{n}\mapsto
t_{n}\uparrow{}^{j+1}[\rho^{i+2}\mapsto
u\uparrow\uparrow{}^{j+1}]\rrbracket\equiv$ $\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}[\rho^{i+1}\mapsto u\uparrow]\uparrow{}^{j+1},\ldots,b_{n}\mapsto
t_{n}[\rho^{i+1}\mapsto u\uparrow]\uparrow{}^{j+1}\rrbracket\equiv$
$\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket[\rho^{i}\mapsto u]\uparrow{}^{j}$

∎

###### Lemma A.9 (Increment swap).

For any $\varphi$-term $t$, for any $i,j\in\mathbb{N}$ such that $i\leq j$,
$t\uparrow{}^{j}\uparrow{}^{i}\equiv t\uparrow{}^{i}\uparrow{}^{j+1}$.

###### Proof.

By induction on $t$:

  1. (1)

$t\equiv\rho^{k}$

if $k<i$ then
$\displaystyle\rho^{k}\uparrow{}^{j}\uparrow{}^{i}\equiv\rho^{k}\uparrow{}^{i}\equiv\rho^{k}$
$\displaystyle\rho^{k}\uparrow{}^{i}\uparrow{}^{j+1}\equiv\rho^{k}\uparrow{}^{j+1}\equiv\rho^{k}$
if $i\leq k<j$ then
$\displaystyle\rho^{k}\uparrow{}^{j}\uparrow{}^{i}\equiv\rho^{k}\uparrow{}^{i}\equiv\rho^{k+1}$
$\displaystyle\rho^{k}\uparrow{}^{i}\uparrow{}^{j+1}\equiv\rho^{k+1}\uparrow{}^{j+1}\equiv\rho^{k+1}$
if $k\geq j$ then
$\displaystyle\rho^{k}\uparrow{}^{j}\uparrow{}^{i}\equiv\rho^{k+1}\uparrow{}^{i}\equiv\rho^{k+2}$
$\displaystyle\rho^{k}\uparrow{}^{i}\uparrow{}^{j+1}\equiv\rho^{k+1}\uparrow{}^{j+1}\equiv\rho^{k+2}$

  2. (2)

$t\equiv s.a$

  3. (3)

$t\equiv s_{1}(a\mapsto s_{2})$

  4. (4)

$t\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$

$\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket\uparrow{}^{j}\uparrow{}^{i}\equiv$
$\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}\uparrow{}^{j+1}\uparrow{}^{i+1},\ldots,b_{n}\mapsto
t_{n}\uparrow{}^{j+1}\uparrow{}^{i+1}\rrbracket\equiv$
$\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}\uparrow{}^{i+1}\uparrow{}^{j+2},\ldots,b_{n}\mapsto
t_{n}\uparrow{}^{i+1}\uparrow{}^{j+2}\rrbracket\equiv$
$\displaystyle\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket\uparrow{}^{i}\uparrow{}^{j+1}$

∎

###### Lemma A.10 (Substitution lemma).

Let $t,t^{\prime},u,u^{\prime}$ be $\varphi$-terms and $t\Rrightarrow
t^{\prime}$ and $u\Rrightarrow u^{\prime}$. Then $t[\rho^{i}\mapsto
u]\Rrightarrow t^{\prime}[\rho^{i}\mapsto u^{\prime}]$.

###### Proof.

To prove by induction on $\Rrightarrow$, assume that if $t\Rrightarrow
t^{\prime}$ and $u\Rrightarrow u^{\prime}$, then for all $i\in\mathbb{N}$,
$t[\rho^{i}\mapsto u]\Rrightarrow t^{\prime}[\rho^{i}\mapsto u^{\prime}]$.

  1. (1)

cong${}_{\text{OBJ}}^{\Rrightarrow}$:

By cong${}_{\text{OBJ}}^{\Rrightarrow}$ and induction hypothesis,

$\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket[\rho^{k}\mapsto u]\\\
\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}[\rho^{k+1}\mapsto u],\ldots,b_{n}\mapsto t_{n}[\rho^{k+1}\mapsto
u]\rrbracket\\\ \Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime}[\rho^{k+1}\mapsto u^{\prime}],\ldots,b_{n}\mapsto
t_{n}^{\prime}[\rho^{k+1}\mapsto u^{\prime}]\rrbracket\\\ \equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{n}\mapsto t_{n}^{\prime}\rrbracket[\rho^{k}\mapsto
u^{\prime}]$

  2. (2)

cong${}_{\rho}^{\Rrightarrow}$:

     * •

if $k>i$, $\rho^{i}[\rho^{k}\mapsto
u]\equiv\rho^{i}\Rrightarrow\rho^{i}\equiv\rho^{i}[\rho^{k}\mapsto
u^{\prime}]$, with reflexivity of ($\Rrightarrow$).

     * •

if $k=i$, $\rho^{i}[\rho^{k}\mapsto u]\equiv u\Rrightarrow
u^{\prime}\equiv\rho^{i}[\rho^{k}\mapsto u^{\prime}]$, with the assumption of
this lemma.

     * •

if $k<i$, $\rho^{i}[\rho^{k}\mapsto
u]\equiv\rho^{i-1}\Rrightarrow\rho^{i-1}\equiv\rho^{i}[\rho^{k}\mapsto
u^{\prime}]$, with reflexivity of ($\Rrightarrow$).

  3. (3)

cong${}_{\text{DOT}}^{\Rrightarrow}$:

By inductive hypothesis and cong${}_{\text{DOT}}^{\Rrightarrow}$,

$\displaystyle t.c[\rho^{i}\mapsto u]\equiv t[\rho^{i}\mapsto u].c\Rrightarrow
t^{\prime}[\rho^{i}\mapsto u^{\prime}].c\equiv$ $\displaystyle
t^{\prime}.c[\rho^{i}\mapsto u^{\prime}]$

  4. (4)

cong${}_{\text{APP}}^{\Rrightarrow}$:

By inductive hypothesis and cong${}_{\text{APP}}^{\Rrightarrow}$,

$\displaystyle t(c\mapsto v)[\rho^{i}\mapsto u]\equiv t[\rho^{i}\mapsto
u](c\mapsto v[\rho^{i}\mapsto u])\Rrightarrow t^{\prime}[\rho^{i}\mapsto
u^{\prime}](c\mapsto v^{\prime}[\rho^{i}\mapsto u^{\prime}])\equiv
t^{\prime}(c\mapsto v^{\prime})[\rho^{i}\mapsto u^{\prime}]$

  5. (5)

DOT${}_{c}^{\Rrightarrow}$: Let $t\equiv s.c$, $s\Rrightarrow
s^{\prime}\equiv\llbracket\ldots,c\mapsto t_{c},\ldots\rrbracket$,
$t^{\prime}\equiv t_{c}[\xi\mapsto s^{\prime}]$.

Since $s\Rrightarrow s^{\prime}$ and $u\Rrightarrow u^{\prime}$, by induction
hypothesis we have

$s[\rho^{i}\mapsto u]\Rrightarrow s^{\prime}[\rho^{i}\mapsto u^{\prime}]$

Furthermore, since $s^{\prime}\equiv\llbracket\ldots,c\mapsto
t_{c},\ldots\rrbracket$,

$s^{\prime}[\rho^{i}\mapsto u^{\prime}]\equiv\llbracket\ldots,c\mapsto
t_{c}[\rho^{i+1}\mapsto u^{\prime}],\ldots\rrbracket$

and by rule DOT${}_{c}^{\Rrightarrow}$ we have

$s[\rho^{i}\mapsto u].c\Rrightarrow t_{c}[\rho^{i+1}\mapsto
u^{\prime}][\xi\mapsto s^{\prime}[\rho^{i}\mapsto u^{\prime}]]$

By A.7, we have

$t_{c}[\rho^{i+1}\mapsto u^{\prime}][\xi\mapsto s^{\prime}[\rho^{i}\mapsto
u^{\prime}]]\equiv t_{c}[\xi\mapsto s^{\prime}][\rho^{i}\mapsto u^{\prime}]$

Thus

$t[\rho^{i}\mapsto u]\equiv s.c[\rho^{i}\mapsto u]\equiv s[\rho^{i}\mapsto
u].c\Rrightarrow\\\ t_{c}[\rho^{i+1}\mapsto u^{\prime}][\xi\mapsto
s^{\prime}[\rho^{i}\mapsto u^{\prime}]]\equiv t_{c}[\xi\mapsto
s^{\prime}][\rho^{i}\mapsto u^{\prime}]\equiv t^{\prime}[\rho^{i}\mapsto
u^{\prime}]$

  6. (6)

DOT${}_{c}^{\varphi\Rrightarrow}$: Let $t\equiv s.c$ and $t^{\prime}\equiv
s^{\prime}.\varphi.c$ with $s\Rrightarrow s^{\prime}$.

By induction hypothesis, $s[\rho^{i}\mapsto u]\Rrightarrow
s^{\prime}[\rho^{i}\mapsto u^{\prime}]$. Substitution in object does not
change its attributes set (domain):
$c\notin\operatorname{\mathsf{attr}}(s^{\prime}[\rho^{i}\mapsto u^{\prime}])$
and $\varphi\in\operatorname{\mathsf{attr}}(s^{\prime}[\rho^{i}\mapsto
u^{\prime}])$. So, rule DOT${}_{c}^{\varphi\Rrightarrow}$ can be applied to
get

$s[\rho^{i}\mapsto u].c\Rrightarrow s^{\prime}[\rho^{i}\mapsto
u^{\prime}].\varphi.c$

which, with the definition of substitution, brings to the goal:

$s.c[\rho^{i}\mapsto u]\Rrightarrow s^{\prime}.\varphi.c[\rho^{i}\mapsto
u^{\prime}]$

  7. (7)

APP${}_{c}^{\Rrightarrow}$: Let $t\equiv s(c\mapsto v)$, $v\Rrightarrow
v^{\prime}$, $s^{\prime}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ and $t^{\prime}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
v^{\prime}\uparrow,b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$.

By induction hypothesis, $s[\rho^{i}\mapsto u]\Rrightarrow
s^{\prime}[\rho^{i}\mapsto u^{\prime}]$ and $v[\rho^{i}\mapsto u]\Rrightarrow
v^{\prime}[\rho^{i}\mapsto u^{\prime}]$. As in $s^{\prime}$, in
$s^{\prime}[\rho^{i}\mapsto u^{\prime}]$ there is attribute $c$ and it is
free. So, reduction via APP${}_{c}^{\Rrightarrow}$ is possible.

$t[\rho^{i}\mapsto u]\equiv s(c\mapsto v)[\rho^{i}\mapsto u]\equiv
s[\rho^{i}\mapsto u](c\mapsto v[\rho^{i}\mapsto u])\\\ \Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
v^{\prime}[\rho^{i}\mapsto u^{\prime}]\uparrow,b_{1}\mapsto
t_{1}[\rho^{i+1}\mapsto u^{\prime}\uparrow],\ldots,b_{n}\mapsto
t_{n}[\rho^{i+1}\mapsto u^{\prime}\uparrow]\rrbracket\\\ \equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
v^{\prime}\uparrow[\rho^{i+1}\mapsto u^{\prime}\uparrow],b_{1}\mapsto
t_{1}[\rho^{i+1}\mapsto u^{\prime}\uparrow],\ldots,b_{n}\mapsto
t_{n}[\rho^{i+1}\mapsto u^{\prime}\uparrow]\rrbracket\\\ \equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
v^{\prime}\uparrow,b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto
t_{n}\rrbracket[\rho^{i}\mapsto u^{\prime}]$

∎

###### Proposition A.11.

Let $t$ be a $\varphi$-term. Then $t\Rrightarrow t^{+}$.

###### Proof.

By induction on structure of $t$,

  1. (1)

if $t\equiv\rho^{n}$, then by cong${}_{\rho}^{\Rrightarrow}$,
$t\Rrightarrow\rho^{n}\equiv(\rho^{n})^{+}$.

  2. (2)

if $t\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$, then by induction hypothesis,
$t_{i}\Rrightarrow t_{i}^{+}$, and by cong${}_{\text{OBJ}}^{\Rrightarrow}$,
$t\Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{+},\ldots,b_{n}\mapsto t_{n}^{+}\rrbracket\equiv t^{+}$.

  3. (3)

if $t\equiv t_{1}.c$, then by induction hypothesis, $t_{1}\Rrightarrow
t_{1}^{+}$, and

    1. (a)

if $t_{1}^{+}\equiv\llbracket\ldots,a\mapsto t_{a},\ldots\rrbracket$, then by
DOT${}_{c}^{\Rrightarrow}$, $t\Rrightarrow t_{a}[\phi^{0}\mapsto t_{1}^{+}]$

    2. (b)

if $c\notin\operatorname{\mathsf{attr}}(t_{1}^{+})$ and
$\varphi\in\operatorname{\mathsf{attr}}(t_{1}^{+})$, then by
DOT${}_{c}^{\varphi\Rrightarrow}$, $t\Rrightarrow t_{1}^{+}.\varphi.c\equiv
t^{+}$

    3. (c)

otherwise, by cong${}_{DOT}^{\Rrightarrow}$, $t\Rrightarrow t_{1}^{+}.c\equiv
t^{+}$

  4. (4)

if $t\equiv t_{1}(c\mapsto u)$, then by induction hypothesis,
$t_{1}\Rrightarrow t_{1}^{+}$, and $u\Rrightarrow u^{+}$, and

    1. (a)

if $t^{+}\equiv\llbracket\ldots,\varphi\mapsto t_{\varphi},\ldots\rrbracket$,
then by APP${}_{c}^{\Rrightarrow}$, $t\Rrightarrow\llbracket\ldots,c\mapsto
u^{+}\uparrow,\ldots\rrbracket$

    2. (b)

otherwise, by cong${}_{APP}^{\Rrightarrow}$, $t\Rrightarrow t_{1}^{+}(c\mapsto
u^{+})\equiv t^{+}$

∎

###### Lemma A.12 (Main Lemma, Lemma 3.16).

$t\Rrightarrow s$ implies
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s$
for some $r$.

###### Proof.

By induction on $\Rrightarrow$,

  1. (1)

cong${}_{\text{OBJ}}^{\Rrightarrow}$: If $t\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket\Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{n}\mapsto t_{n}^{\prime}\rrbracket\equiv s$, where
$t_{i}\Rrightarrow t_{i}^{\prime}$ for all $i\in\\{1,\ldots,n\\}$, then let
$r\equiv t$, and from the definition of
$\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}$,
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s$.

  2. (2)

cong${}_{\rho}^{\Rrightarrow}$: If $t\equiv\rho^{i}\Rrightarrow\rho^{i}\equiv
s$, let $r\equiv t$.

  3. (3)

cong${}_{\text{DOT}}^{\Rrightarrow}$: If $t\equiv t^{\prime}.c\Rrightarrow
s^{\prime}.c\equiv s$ where $t^{\prime}\Rrightarrow s^{\prime}$, then by
induction hypothesis, there exists $r^{\prime}$, such that
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}$.
Hence,
$t^{\prime}.c\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}.c\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}.c$,
from the definition of
$\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}$ and
$\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}$.

  4. (4)

cong${}_{\text{APP}}^{\Rrightarrow}$: If $t\equiv t^{\prime}(c\mapsto
u)\Rrightarrow s^{\prime}(c\mapsto u^{\prime})\equiv s$, where
$t^{\prime}\Rrightarrow s^{\prime}$ and $u\Rrightarrow u^{\prime}$, then by
induction hypothesis, there exists $r^{\prime}$, such that
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}$.
Hence, $t^{\prime}(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}(c\mapsto
u^{\prime})$, from the definition of
$\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}$ and
$\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}$.

  5. (5)

DOT${}_{c}^{\Rrightarrow}$: If $t\equiv t^{\prime}.c\Rrightarrow
t_{c}[\rho^{0}\mapsto t^{\prime\prime}]\equiv s$, where
$t^{\prime}\Rrightarrow t^{\prime\prime}\equiv\llbracket\ldots,c\mapsto
t_{c},\ldots\rrbracket$, then, by induction hypothesis, there exists $q$, such
that
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}q\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}t^{\prime\prime}$.
Since
$q\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}t^{\prime\prime}$
and $t^{\prime\prime}\equiv\llbracket\ldots,c\mapsto t_{c},\ldots\rrbracket$,
$q\equiv\llbracket\ldots,c\mapsto t_{c}^{\prime},\ldots\rrbracket$ with
$t_{c}^{\prime}\Rrightarrow t_{c}$. Then
$q.c\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t_{c}^{\prime}[\rho^{0}\mapsto
q]$. Moreover, we have $t_{c}^{\prime}\Rrightarrow t_{c}$, and by induction
hypothesis, there exists $r^{\prime}$, such that
$t_{c}^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}t_{c}$.
Finally, with substitution lemmas for
$\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}$ and
$\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}$, we
have $t\equiv
t^{\prime}.c\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}q.c\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t_{c}^{\prime}[\rho^{0}\mapsto
q]\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}[\rho^{0}\mapsto
q]\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}t_{c}[\rho^{0}\mapsto
t^{\prime\prime}]\equiv s$, so we can take $r^{\prime}[\rho^{0}\mapsto q]$ for
$r$.

  6. (6)

DOT${}_{c}^{\varphi\Rrightarrow}$: If $t\equiv t^{\prime}.c\Rrightarrow
s^{\prime}.\varphi.c\equiv s$, where $t^{\prime}\Rrightarrow
s^{\prime}\equiv\llbracket\ldots\rrbracket$, and
$c\notin\operatorname{\mathsf{attr}}(s^{\prime})$ and
$\varphi\in\operatorname{\mathsf{attr}}(s^{\prime})$, then, by induction
hypothesis, there exists $r^{\prime}$, such that
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}$.
As
$r^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}$,
$r^{\prime}\equiv\llbracket\ldots\rrbracket$ with
$c\notin\operatorname{\mathsf{attr}}(r^{\prime})$ and
$\varphi\in\operatorname{\mathsf{attr}}(r^{\prime})$. Hence
$r^{\prime}.c\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}r^{\prime}.\varphi.c$.
Secondly,
$r^{\prime}.\varphi.c\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}.\varphi.c$.
So, for $r\equiv r^{\prime}.\varphi.c$,
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s$.

  7. (7)

APP${}_{c}^{\Rrightarrow}$: If $t\equiv t^{\prime}(c\mapsto
u)\Rrightarrow\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
u^{\prime}\uparrow,b_{1}\mapsto t_{1},\ldots,b_{n}\mapsto
t_{n}\rrbracket\equiv s$, where $t^{\prime}\Rrightarrow
s^{\prime}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto\varnothing,b_{1}\mapsto
t_{1},\ldots,b_{n}\mapsto t_{n}\rrbracket$ and $u\Rrightarrow u^{\prime}$,
then, by induction hypothesis, there exists $r^{\prime}$, such that
$t^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}$.
As
$r^{\prime}\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s^{\prime}$,
$r^{\prime}\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto\varnothing,b_{1}\mapsto
t_{1}^{\prime},\ldots,b_{n}\mapsto t_{n}^{\prime}\rrbracket$ with
$t_{i}^{\prime}\Rrightarrow t_{i}$. Hence $r^{\prime}(c\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
u\uparrow,b_{1}\mapsto t_{1}^{\prime},\ldots,b_{n}\mapsto
t_{n}^{\prime}\rrbracket$. Let $r\equiv\llbracket
a_{1}\mapsto\varnothing,\ldots,a_{k}\mapsto\varnothing,c\mapsto
u\uparrow,b_{1}\mapsto t_{1}^{\prime},\ldots,b_{n}\mapsto
t_{n}^{\prime}\rrbracket$. By
cong${}_{\text{OBJ}}^{\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}}$,
$r\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s$, so,
$t\operatorname{\stackrel{{\scriptstyle\textit{h}^{\ast}}}{{\rightsquigarrow}}}r\operatorname{\stackrel{{\scriptstyle\textit{i}}}{{\Rrightarrow}}}s$.

∎

###### Lemma A.13 (Substitution Lemma for
$\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}$,
Lemma 3.17).

If $t\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}s$,
then $t[\rho^{n}\mapsto
q]\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}s[\rho^{n}\mapsto
q]$.

###### Proof.

By induction on
$\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}$:

  1. (1)

cong${}_{\text{DOT}}^{h}$: If
$t.a\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}.a$
and
$t\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}$,
then by induction hypothesis $t[\rho^{n}\mapsto
q]\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}[\rho^{n}\mapsto
q]$, so $t.a[\rho^{n}\mapsto
q]\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}.a[\rho^{n}\mapsto
q]$

  2. (2)

cong${}_{\text{APP}}^{h}$: If $t(a\mapsto
u)\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}(a\mapsto
u)$ and
$t\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}$,
then by induction hypothesis $t[\rho^{n}\mapsto
q]\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}[\rho^{n}\mapsto
q]$, so $t[\rho^{n}\mapsto q](a\mapsto u[\rho^{n}\mapsto
q])\operatorname{\stackrel{{\scriptstyle\textit{h}}}{{\rightsquigarrow}}}t^{\prime}[\rho^{n}\mapsto
q](a\mapsto u[\rho^{n}\mapsto q])$, and $t(a\mapsto u)[\rho^{n}\mapsto