# From Semantics to Types: the Case of the Imperative $\lambda$-Calculus

Ugo de’Liguoro Department of Computer Science
Università di Torino
Torino, Italy<EMAIL_ADDRESS>Department of Computer Science
Università di Torino
Torino, Italy Riccardo Treglia Department of Computer Science
Università di Torino
Torino, Italy<EMAIL_ADDRESS>
###### Abstract

We propose an intersection type system for an imperative $\lambda$-calculus
based on a state monad and equipped with algebraic operations to read and
write to the store. The system is derived by solving a suitable domain
equation in the category of $\omega$-algebraic lattices; the solution consists
of a filter-model generalizing the well known construction for ordinary
$\lambda$-calculus. Then the type system is obtained out of the term
interpretations into the filter-model itself. The so obtained type system
satisfies the “type-semantics” property, and it is sound and complete by
construction.

##  1 Introduction

Since Strachey and Scott’s work in the 60’s, $\lambda$-calculus and
denotational semantics, together with logic and type theory, have been
recognized as the mathematical foundations of programming languages.
Nonetheless, there are aspects of actual programming languages that have shown
to be quite hard to treat, at least with the same elegance as the theory of
recursive functions and of algebraic data structures; a prominent case is
surely side-effects.

The introduction of notions of computation as monads by Moggi in [23] greatly
improved the understanding of “impure”, namely non functional features in the
semantics of programming languages, by providing a unified framework for
treating computational effects: see [27, 28], the introductory [9], and the
large body of bibliography thereafter; a gentle introduction and references
can be found e.g. in [18].

Starting with [15], we have considered an untyped variant of Moggi’s
computational $\lambda$-calculus, with two sorts of terms: values denoting
points of some domain $D$, and computations denoting points of $TD$, where $T$
is some generic monad and $D\cong D\xrightarrow{}TD$. The goal was to show how
such a calculus can be equipped with an operational semantics and an
intersection type system, such that types are invariant under reduction and
expansion of computation terms, and convergent computations are characterized
by having non-trivial types in the system.

Our approach was limited to a pure calculus without constants, where the unit
and bind operations are axiomatized by the monadic laws from [28]. On the
other hand, such operations may model how morphisms from values to
computations compose, but do not tell anything about how the computational
effects are produced. In the theory of algebraic effects [24, 25, 26], Plotkin
and Power have shown under which conditions effect operators live in the
category of algebras of a computational monad, which is isomorphic to the
category of models of certain equational specifications, namely varieties in
the sense of universal algebra [20].

Toward a general theory of intersection type systems for (untyped)
computational $\lambda$-calculi with algebraic effects, we have studied in the
draft [16] the case of the imperative $\lambda$-calculus $\lambda_{imp}$, both
because the modeling of a functional calculus with (implicitly higher-order)
side-effects is of interest per se, and because it is a case study to test our
claim that an intersection types assignment system can be defined and that it
is useful to formalize reasoning about the calculus itself.

Indeed the type system, which we present in the very last section of this
work, has not been invented from scratch; on the contrary, it has been
constructed moving from the domain equation $D=D\xrightarrow{}\mathbb{S}D$,
where $\mathbb{S}$ is (a variant of) the state monad. The method we follow is
to solve such equation in the category of $\omega$-algebraic lattices, whose
objects and morphisms can be described via intersection type theories, that
are the “logic” of such domains in the sense of [2]: see also [4]. The
solution is constructed via the description of compact points of such a $D$,
implicitly mirroring the inverse limit construction, but in a conceptually
simpler way, consisting of an inductive definition of types and of their
preorders. Once this has been obtained, subtyping and typing rules are derived
in a uniform way, leading to a type assignment system which enjoys the “type-
semantics” property, namely that denotational semantics of terms is fully
characterized by their typings in the system. Soundness and completeness of
the type system now follow straightforwardly.

Summary and results. In section 2 we outline the syntax of the untyped
imperative $\lambda$-calculus $\lambda_{imp}$, and stress the difference with
other calculi in literature. In section 3 we deal with solving the domain
equation thoroughly. To do this we recall the concept of computational monad,
then we consider the state and partiality monad $\mathbb{S}$. In the same
section, we tackle the solution of the domain equation by breaking the
circularity that arises out of the definition of the monad $\mathbb{S}$
itself. We conclude the section by modelling algebraic operators over the
monad $\mathbb{S}$ and formalizing the model of $\lambda_{imp}$. In section 4,
we solve the domain equation by inductively constructing type theories that
induce a filter model.

Section 5 explains how to derive the type assignment system from the filter-
model construction. We conclude establishing the type semantics theorem for
our calculus. Finally, section 6 is devoted to the discussion of our results
and to related works.

We assume familiarity with $\lambda$-calculus and intersection types; a
comprehensive reference is [8] Part III. Some previous knowledge about
computational monads and algebraic effects is useful: see e.g. [9] and [18]
chap. 3.

##  2 An untyped imperative $\lambda$-calculus: $\lambda_{imp}$

Imperative extensions of the $\lambda$-calculus, both typed and type-free, are
usually based on the call-by-value $\lambda$-calculus, and enriched with
constructs for reading and writing to the store. Aiming at exploring the
semantics of side effects in computational calculi, where “impure” functions
are modeled by pure ones sending values to computations in the sense of [23],
we consider the calculus introduced in [15], to which we add syntax denoting
algebraic effect operations à la Plotkin and Power [24, 25, 26] over a
suitable state monad.

Let $\mathbb{L}=\\{\ell_{0},\ell_{1},\ldots\\}$ be a denumerable set of
abstract locations. Borrowing notation from [18], chap. 3, we consider
denumerably many operator symbols $\textit{get}_{\ell}$ and
$\textit{set}_{\ell}$, obtaining:

######  Definition 2.1.

The syntax of the untyped imperative $\lambda$-calculus $\lambda_{imp}$ has
two sorts of terms, which are defined by mutual induction as follows:

$\begin{array}[]{rrcl@{\hspace{1cm}}l}\textit{Val}:&V,W&::=&x\mid\lambda
x.M\hfil\hskip 28.45274pt\\\ \textit{Com}:&M,N&::=&[V]\mid M\star
V\mid\textit{get}_{\ell}(\lambda x.M)\mid\textit{set}_{\ell}(V,M)\hfil\hskip
28.45274pt&(\ell\in\mathbb{L})\\\ \end{array}$

Terms are of either sorts Val and Com, representing values and computations,
respectively. The variable $x$ is bound in $\lambda x.M$ and
$\textit{get}_{\ell}(\lambda x.M)$; terms are identified up to renaming of
bound variables so that the capture avoiding substitution $M[V/x]$ is always
well defined; $FV(M)$ denotes the set of free variables in $M$. We call
$\textit{Val}^{\,0}$ the subset of closed $V\in\textit{Val}$; similarly for
$\textit{Com}^{0}$.

Terms of the shape $[V]$ and $M\star V$ are written $\texttt{return }V$ and
$M\texttt{ >>= }V$ in Haskell-like syntax, respectively. With respect to [15]
we write $[V]$ instead of $\mbox{\it unit}\;V$. With respect to the syntax of
the “imperative $\lambda$-calculus” in [18], we do not have the let construct,
nor the application $VW$ among values. These constructs are indeed definable:
$\mbox{{let} $x=M$ {in} $N$}\;\equiv\;M\star(\lambda x.N)$ and
$VW\;\equiv\;[W]\star V$ (where $\equiv$ is syntactic identity). In general,
application among computations can be encoded by $MN\equiv M\star(\lambda z.\
N\star z)$, where $z$ is fresh.

In a sugared notation from functional programming languages, we could have
written location dereferentiation and assignment, respectively, as follows:

$\mbox{{let} $x=\;!\ell$ {in} $M$}~{}\equiv~{}\textit{get}_{\ell}(\lambda
x.M)\qquad\ell:=V;M~{}\equiv~{}\textit{set}_{\ell}(V,M)$

Observe that we do not consider locations as values; consequently they cannot
be dynamically created like with the ref operator from ML, nor is it possible
to model aliasing. On the other hand, since the calculus is untyped, “strong
updates” are allowed (differently than [10]). By this, we mean that when
evaluating $\textit{set}_{\ell}(V,M)$, the value $V$ to which the location
$\ell$ is updated bears no relation to the previous value, say $W$, of $\ell$
in the store: indeed, in our type assignment system $W$ and $V$ may well have
completely different types.

##  3 Denotational semantics

We illustrate a denotational semantics of the calculus in the category of
domains. The model is based on the solution of the domain equation:

$D=[D\xrightarrow{}[S\xrightarrow{}(D\times S)_{\bot}]]$ (1)

where $S$ is a suitable space of stores over $D$, and
$\mathbb{S}\,D=[S\xrightarrow{}(D\times S)_{\bot}]$ is a variant of the state
monad in [23], which is called the partiality and state monad in [14].

Before embarking on solving the equation (1), let us recall definitions of
monads, of $\mathbb{S}$, and algebraic operators, and fix notations.

The partiality and state monad. We recall Wadler’s type-theoretic definition
of monads [27, 28], that is at the basis of their successful implementation in
Haskell language, a natural interpretation of the calculus is into a cartesian
closed category (ccc), such that two families of combinators, or a pair of
polymorphic operators called the “unit” and the “bind”, exist satisfying the
monad laws. In what follows, $\mathcal{C}$ will be a concrete ccc. Examples
are the category Dom of Scott domains with continuous functions, and its full
subcategory $\omega\text{-}\textrm{\bf ALG}$ of algebraic lattices with a
countable basis.

######  Definition 3.1.

(Computational Monad [28] §3) Let $\mathcal{C}$ be a concrete ccc. A
functional computational monad, henceforth just monad over $\mathcal{C}$ is a
triple $(T,\mbox{\it unit}\;\\!,\star)$ where $T$ is a map over the objects of
$\mathcal{C}$, and unit and $\star$ are families of morphisms

$\begin{array}[]{c@{\hspace{2cm}}c}\mbox{\it
unit}_{A}:A\xrightarrow{}TA\hfil\hskip
56.9055pt&\star_{A,B}:TA\times(TB)^{A}\xrightarrow{}TB\end{array}$

such that, writing $\star_{A,B}$ as an infix operator and omitting subscripts:

$\begin{array}[]{l<EMAIL_ADDRESS>unit}:\hfil\hskip 14.22636pt&\mbox{\it unit}\;a\star f&=&f\,a\hfil\hskip
14.22636pt\\\ \textit{Right unit}:\hfil\hskip 14.22636pt&m\star\mbox{\it
unit}&=&m\hfil\hskip 14.22636pt\\\ \textit{Assoc}:\hfil\hskip
14.22636pt&(m\star f)\star g&=&m\star\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern 2.0mu\raisebox{1.18399pt}{$\lambda$}}d.(f\,d\star
g)\hfil\hskip 14.22636pt\end{array}$

where $\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}d.(f\,d\star g)$ is the lambda notation
for $d\mapsto f\,d\star g$.

######  Remark 3.2.

In case of concrete ccc, Def. 3.1 coincides with the notion of Kleisli triple
$(T,\eta,\\_^{\dagger})$ (see e.g. [23], Def. 1.2). The equivalence is
obtained by relating maps $\eta$ and $\\_^{\dagger}$ to unit and $\star$
operators, as follows:

$\mbox{\it unit}_{X}=\eta_{X}\qquad\qquad a\star f=f^{\dagger}(a)$

The first equality is just a notational variation of the coercion of values
into computations. The latter, instead, establishes the connection between the
$\star$ operator with the map $\\_^{\dagger}$, also called extension operator:
if $f:X\xrightarrow{}TY$ then $f^{\dagger}:TX\xrightarrow{}TY$ is the unique
map such that $f=f^{\dagger}\circ\eta_{X}$.

Now, let us look closer how monads model effectful computations. We focus on
Dom, a full subcategory of pointed Dcpo’s with Scott continuous functions as
morphisms. Then $TX$ is the domain, or the type, of computations with values
in $X$. In general $TX$ has a richer structure than $X$ itself, modeling
partial computations, exceptions, non-determinism etcetera, including side
effects. The mapping $\mbox{\it unit}_{X}:X\xrightarrow{}TX$ is interpreted as
the trivial computation $\mbox{\it unit}_{X}(x)$ just returning the value $x$,
and it is an embedding if $T$ satisfies the requirement that all the
$\mbox{\it unit}_{X}$ are monos. Now a function $f:X\xrightarrow{}TY$ models
an “impure” program $P$ with input in $X$ and output in $Y$ via a pure
function returning the computation $f(x)\in TY$.

To relate equation (1) to the monad $\mathbb{S}$ we have to be more precise
about the domain $S$. We consider $FX=X^{\mathbb{L}}$ the domain of stores
over $X$ with locations in $\mathbb{L}$, namely the set $X^{\mathbb{L}}$,
ranged over by $\varsigma$, of maps from locations to points of $X$; $FX$ is a
domain with the order inherited from $X$. The map $FX$ obviously extends to a
locally continuous functor by setting
$F(g)=g^{\mathbb{L}}=g\circ\\_:X^{\mathbb{L}}\xrightarrow{}Y^{\mathbb{L}}$ for
any $g:X\xrightarrow{}Y$.

We are now in place to properly define the partiality and state monad
$\mathbb{S}$ in terms of Def. 3.1.

######  Definition 3.3.

(Partiality and state monad) Given the domain $S=X^{\mathbb{L}}$ representing
a notion of state, we define the partiality and state monad
$(\mathbb{S},\mbox{\it unit}\;,\star)$, as the mapping

$\mathbb{S}\,X=[S\xrightarrow{}(X\times S)_{\bot}]$

where $(X\times S)_{\bot}$ is the lifting of the cartesian product $X\times
S$, equipped with two (families of) operators unit and $\star$ defined as
follows:

$\begin{array}[]{l<EMAIL_ADDRESS>unit}\;x::=\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}\varsigma.(x,\varsigma)\hfil\hskip
14.22636pt\\\ (c\star
f)\varsigma=f^{\dagger}(c)(\varsigma)::=\left\\{\begin{array}[]{lll}f\,(x)(\varsigma^{\prime})&\mbox{if
$c(\varsigma)=(x,\varsigma^{\prime})\neq\bot$}\\\ \bot&\mbox{if
$c(\varsigma)=\bot$}\end{array}\right.\hfil\hskip 14.22636pt\end{array}$

where we omit subscripts.

######  Remark 3.4.

A function $f:X\xrightarrow{}\mathbb{S}\,Y$ has type
$X\xrightarrow{}S\xrightarrow{}(Y\times S)_{\bot}$, which is isomorphic to
$(X\times S)\xrightarrow{}(Y\times S)_{\bot}$; if $f$ is the interpretation of
an “imperative program” $P$, and it is the currying of $f^{\prime}$, then we
expect that $f\,x\,\varsigma=f^{\prime}(x,\varsigma)=(y,\varsigma^{\prime})$
if $y$ and $\varsigma^{\prime}$ are respectively the value and the final store
obtained from the evaluation of $P(x)$ starting in $\varsigma$, if it
terminates; $f\,x\,\varsigma=f^{\prime}(x,\varsigma)=\bot$ otherwise. Clearly
$f^{\prime}$ is the familiar interpretation of the imperative program $P$ as a
state transformation mapping.

A domain equation. Evidently, the domain $FX$ depends on $X$ itself; in
contrast, while defining $\mathbb{S}\,X$ the domain $S$ has to be fixed, since
otherwise the definition of the $\star$ operator does not make sense, and
$\mathbb{S}$ is not even a functor. A solution would be to take $S=FD$, where
$D\cong[D\xrightarrow{}\mathbb{S}\,D]$, but this is clearly circular.

To break the circularity, we define the mixed-variant bi-functor
$G:\textbf{Dom}^{\textit{op}}\times\textbf{Dom}\xrightarrow{}\textbf{Dom}$ by

$G(X,Y)=[FX\xrightarrow{}(Y\times FY)_{\bot}]$

whose action on morphisms is illustrated by the diagram:

$\begin{diagram}$

where $f:X^{\prime}\xrightarrow{}X$, $g:Y\xrightarrow{}Y^{\prime}$ and
$\alpha\in G(X,Y)$. Now it is routine to prove that $G$ is locally continuous
so that, by the inverse limit technique, we can find the initial solution to
the domain equation (which is the same as Equation 1):

$D=[D\xrightarrow{}G(D,D)]$ (2)

In summary we have:

######  Theorem 3.5.

There exists a domain $D$ such that the state monad $\mathbb{S}_{D}$ with
state domain $S=[\mathbb{L}\xrightarrow{}D]$ is a solution in Dom to the
domain equation:

$D=[D\xrightarrow{}\mathbb{S}_{D}\,D]$

Moreover, it is initial among all solutions to such equation.

###### Proof.

Take $D$ to be the (initial) solution to Equation 2; now if
$S=FD=D^{\mathbb{L}}$ then $\mathbb{S}_{D}\,D=G(D,D)$. ∎

Algebraic operations over $\mathbb{S}$. Monads are about composition of
morphisms of some special kind. However, thinking of
$f:X\xrightarrow{}\mathbb{S}X$ as the meaning of a program with side effects
doesn’t tell anything about side effects themselves, that are produced by
reading and writing values from and to stores in $S$.

To model effects associated to a monad, Plotkin and Power have proposed in
[24, 25, 26] a theory of algebraic operations. A gentle introduction to the
theory can be found in [18], chap. 3, from which we borrow the notation.

Suppose that $T$ is a monad over a category $\mathcal{C}$ with terminal object
1 and all finite products; then an algebraic operation op with arity $n$ is a
family of morphisms $\textbf{op}_{X}:(TX)^{n}\xrightarrow{}TX$, where
$(TX)^{n}=TX\times\cdots\times TX$ is the $n$-times product of $TX$ with
itself, such that

$\textbf{op}_{X}\circ\Pi_{n}f^{\dagger}=f^{\dagger}\circ\textbf{op}_{X}$ (3)

where $f:X\xrightarrow{}TX$ and
$\Pi_{n}f^{\dagger}=f^{\dagger}\times\cdots\times
f^{\dagger}:(TX)^{n}\xrightarrow{}(TX)^{n}$. In case of the concrete category
Dom, 1 is a singleton and products are sets of tuples. Then $\textbf{op}_{X}$
is an operation of arity $n$ of an algebra with carrier $TX$; since
$f^{\dagger}:TX\xrightarrow{}TX$, we have that $(\Pi_{n}f^{\dagger})\langle
x_{1},\ldots,x_{n}\rangle=\langle
f^{\dagger}(x_{1}),\ldots,f^{\dagger}(x_{n})\rangle$, and Equation 3 reads as:

$\textbf{op}_{X}(f^{\dagger}(x_{1}),\ldots,f^{\dagger}(x_{n}))=f^{\dagger}(\textbf{op}_{X}(x_{1},\ldots,x_{n}))$

namely the functions $f^{\dagger}$ are homomorphisms w.r.t. $\textbf{op}_{X}$.

Algebraic operations $\textbf{op}_{X}:(TX)^{n}\xrightarrow{}TX$ do suffice in
case $T$ is, say, the nondeterminism or the output monad, but cannot model
side effects operations in case of the store monad. This is because read and
write operations implement a bidirectional action of stores to programs and of
programs to stores. What is needed instead is the generalized notion of
operation proposed in [24] (and further studied in [19]); such construction,
that is carried out in a suitable enriched category, can be instantiated to
the case of Dom as follows:

$\textbf{op}:P\times(TX)^{A}\xrightarrow{}TX\cong(TX)^{A}\xrightarrow{}(TX)^{P}$

where $P$ is the domain of parameters and $A$ of generalized arities, and the
rightmost “type” is the interpretation in Dom of Def. 1 in [24]. For such
operations Equation 3 is generalized as follows (see [18], Def. 13):

$\textbf{op}(p,k)\star
f=f^{\dagger}(\textbf{op}(p,k))=\textbf{op}(p,f^{\dagger}\circ
k)=\textbf{op}(p,\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}x.(k(x)\star f))$ (4)

where $f:X\xrightarrow{}TX$, $p\in P$ and $k:A\xrightarrow{}TX$.

Denotational semantics of terms. Given the monad
$(\mathbb{S},\eta,\\_^{\dagger})$ and the domain $D$ from Theorem 3.5, we
first interpret the constants $\textit{get}_{\ell}$ and $\textit{set}_{\ell}$
as generalized operations over $\mathbb{S}$. By taking $P=\textbf{1}$ and
$A=D$ we define:

$\llbracket\textit{get}_{\ell}\rrbracket:\textbf{1}\times(\mathbb{S}D)^{D}\xrightarrow{}\mathbb{S}D\simeq(\mathbb{S}D)^{D}\xrightarrow{}\mathbb{S}D\quad\mbox{
by
}\quad\llbracket\textit{get}_{\ell}\rrbracket\,d\,\varsigma=d\,(\varsigma\,(\ell))\,\varsigma$

where $d\in D$ is identified with its image in $D\xrightarrow{}\mathbb{S}\,D$,
and $\varsigma\in S=[\mathbb{L}\xrightarrow{}D]$. On the other hand, taking
$P=D$ and $A=\textbf{1}$, we define:

$\llbracket\textit{set}_{\ell}\rrbracket:D\times(\mathbb{S}D)^{\textbf{1}}\xrightarrow{}\mathbb{S}D\simeq
D\times\mathbb{S}D\xrightarrow{}\mathbb{S}D\quad\mbox{ by
}\llbracket\textit{set}_{\ell}\rrbracket(d,c)\,\varsigma=c(\varsigma[\ell\mapsto
d])$

where $c\in\mathbb{S}D=S\xrightarrow{}(D\times S)_{\bot}$ and
$\varsigma[\ell\mapsto d]$ is the store sending $\ell$ to $d$ and it is equal
to $\varsigma$ otherwise.

Then we interpret values from Val in $D$ and computations from Com in
$\mathbb{S}\,D$. More precisely we define the maps
$\llbracket\cdot\rrbracket^{D}:\textit{Val}\xrightarrow{}\mbox{\it
Env}\xrightarrow{}D$ and
$\llbracket\cdot\rrbracket^{\mathbb{S}D}:\textit{Com}\xrightarrow{}\mbox{\it
Env}\xrightarrow{}\mathbb{S}\,D$, where $\mbox{\it
Env}=\textit{Var}\xrightarrow{}D$ is the set of environments interpreting term
variables in Var:

######  Definition 3.6.

A $\lambda_{imp}$-model is a structure ${\cal
D}=(D,\mathbb{S},\llbracket\cdot\rrbracket^{D},\llbracket\cdot\rrbracket^{\mathbb{S}D})$
such that:

  1. 1.

$D$ is a domain s.t. $D\cong D\xrightarrow{}\mathbb{S}D$ via $(\Phi,\Psi)$,
where $\mathbb{S}$ is the partiality and state monad of stores over $D$;

  2. 2.

for all $e\in\mbox{\it Env}$, $V\in\textit{Val}$ and $M\in\textit{Com}$:

$\begin{array}[]{ll}\llbracket x\rrbracket^{D}e=e(x)&\quad\llbracket\lambda
x.M\rrbracket^{D}e=\Psi(\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}d\in D.\,\llbracket
M\rrbracket^{\mathbb{S}D}{e[x\mapsto d]})\\\\[2.84526pt]
\llbracket\,[V]\,\rrbracket^{\mathbb{S}D}e=\mbox{\it unit}\;\,(\llbracket
V\rrbracket^{D}e)&\quad\llbracket M\star
V\rrbracket^{\mathbb{S}D}e=(\llbracket
M\rrbracket^{\mathbb{S}D}e)\star\Phi(\llbracket
V\rrbracket^{D}e)\\\\[2.84526pt] \llbracket\textit{get}_{\ell}(\lambda
x.M)\rrbracket^{\mathbb{S}D}e=\llbracket\textit{get}_{\ell}\rrbracket\,\Phi(\llbracket\lambda
x.M\rrbracket^{D}e)&\quad\llbracket\textit{set}_{\ell}(V,M)\rrbracket^{\mathbb{S}D}e=\llbracket\textit{set}_{\ell}\rrbracket(\llbracket
V\rrbracket^{D}e,\llbracket M\rrbracket^{\mathbb{S}D}e)\end{array}$

By unravelling definitions and applying to an arbitrary store $\varsigma\in
S$, the last two clauses can be written:

$\begin{array}[]{rcl}\llbracket\textit{get}_{\ell}(\lambda
x.M)\rrbracket^{\mathbb{S}D}e\,\varsigma&=&\llbracket
M\rrbracket^{\mathbb{S}D}(e[x\mapsto\varsigma(\ell)])\,\varsigma\\\\[2.84526pt]
\llbracket\textit{set}_{\ell}(V,M)\rrbracket^{\mathbb{S}D}e\,\varsigma&=&\llbracket
M\rrbracket^{\mathbb{S}D}e\,(\varsigma[\ell\mapsto\llbracket
V\rrbracket^{D}e])\end{array}$

We say that the equation $M=N$ is true in ${\cal D}$, written ${\cal D}\models
M=N$, if $\llbracket M\rrbracket^{\mathbb{S}D}e=\llbracket
N\rrbracket^{\mathbb{S}D}e$ for all $e\in\mbox{\it Env}$.

######  Proposition 3.7.

The following equations are true in ${\cal D}$:

  1. 1.

$[V]\star(\lambda x.M)=M[V/x]$

  2. 2.

$M\star\lambda x.[x]=M$

  3. 3.

$(L\star\lambda x.M)\star\lambda y.N=L\star\lambda x.(M\star\lambda y.N)$

  4. 4.

$\textit{get}_{\ell}(\lambda x.M)\star W=\textit{get}_{\ell}(\lambda x.(M\star
W))$

  5. 5.

$\textit{set}_{\ell}(V,M)\star W=\textit{set}_{\ell}(V,M\star W)$

where $x\not\in FV(\lambda y.N)$ in (3) and $x\not\in FV(W)$ in (4).

###### Proof.

By definition and straightforward calculations. For example, to see (4), let
$\varsigma\in S$ be arbitrary and $e^{\prime}=e[x\mapsto\varsigma(\ell)]$;
then, omitting the apices of the interpretation mappings
$\llbracket\cdot\rrbracket$:

$\llbracket\textit{get}_{\ell}(\lambda x.M)\star W\rrbracket
e\,\varsigma=(\llbracket W\rrbracket e)^{\dagger}(\llbracket M\rrbracket
e^{\prime})\,\varsigma$

On the other hand:

$\llbracket\textit{get}_{\ell}(\lambda x.(M\star W))\rrbracket
e\,\varsigma=(\llbracket\lambda x.(M\star W)\rrbracket
e)\,\varsigma(\ell)\,\varsigma=\llbracket M\star W\rrbracket
e^{\prime}\,\varsigma=(\llbracket W\rrbracket e^{\prime})^{\dagger}(\llbracket
M\rrbracket e^{\prime})\,\varsigma$

But $x\not\in FV(W)$ implies $\llbracket W\rrbracket e^{\prime}=\llbracket
W\rrbracket e$, and we are done. ∎

Equations (1)-(3) in Prop. 3.7 are the monadic laws from Def. 3.1, equations
(4)-(5) are instances of Equation 4.

##  4 The filter-model construction

In this section we switch to the category $\omega\text{-}\textrm{\bf ALG}$ of
$\omega$-algebraic lattices. $\omega\text{-}\textrm{\bf ALG}$ is the full
subcategory of Dom of complete lattices $(D,\sqsubseteq_{D})$ such that the
set $K(D)$ of compact points is countable and $d=\bigsqcup\\{e\in K(D)\mid
e\sqsubseteq_{D}d\\}$ is a directed sup for all $d\in D$.

Observe that morphisms in $\omega\text{-}\textrm{\bf ALG}$ are Scott-
continuous maps, hence preserving direct sups, but not necessary arbitrary
ones.

######  Definition 4.1.

An intersection type theory, shortly itt, is a pair
$\textit{Th}_{A}=(\mathcal{L}_{A},\leq_{A})$ where $\mathcal{L}_{A}$, the
language of $\textit{Th}_{A}$, is a countable set of type expressions closed
under $\wedge$, and $\omega_{A}\in\mathcal{L}_{A}$ is a special constant;
$\leq_{A}$ is a pre-order over $\mathcal{L}_{A}$ closed under the following
rules:

$\begin{array}[]{c@{\hspace{1.5cm}}c@{\hspace{1.5cm}}c<EMAIL_ADDRESS>42.67912pt&\alpha\wedge\beta\leq_{A}\alpha\hfil\hskip
42.67912pt&\alpha\wedge\beta\leq_{A}\beta\hfil\hskip
42.67912pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\alpha\leq_{A}\alpha^{\prime}\quad\beta\leq_{A}\beta^{\prime}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=66.69756pt\hbox{}}}\hbox{\kern
2.37782pt\hbox{$\displaystyle\alpha\wedge\beta\leq_{A}\alpha^{\prime}\wedge\beta^{\prime}$}}}}\hfil\hskip
42.67912pt\end{array}$

In the literature, the operator $\wedge$ is called intersection, and
$\omega_{A}$ the universal type. Informally, $\textit{Th}_{A}$ is identified
with the set of inequalities $\alpha\leq_{A}\beta$, so that, abusing
terminology, we shall also say that $\leq_{A}$ is a type theory. Clearly, the
quotient $\mathcal{L}_{A}/_{\leq_{A}}$ is an inf-semilattice, with $\wedge$ as
meet and $\omega_{A}$ as top element.

######  Definition 4.2.

A non empty $F\subseteq\mathcal{L}_{A}$ is a filter of $\textit{Th}_{A}$ if it
is closed under $\wedge$ and upward closed w.r.t. $\leq_{A}$; let ${\cal
F}_{A}$ be the set of filters of $\textit{Th}_{A}$. The principal filter over
$\alpha$ is the filter
$\uparrow_{A}\alpha=\\{\beta\in\mathcal{L}_{A}\mid\alpha\leq_{A}\beta\\}$.

The following proposition is the fundamental fact about intersection types and
$\omega$-algebraic lattices:

######  Proposition 4.3 (Representation theorem).

The partial order $({\cal F}_{A},\subseteq)$ of the filters of an intersection
type theory $\textit{Th}_{A}$ is an $\omega$-algebraic lattice, whose compact
elements are the principal filters. Vice versa, any $\omega$-algebraic lattice
$A$ is isomorphic the poset $({\cal F}_{A},\subseteq)$ of filters of some
intersection type theory $\textit{Th}_{A}$.

###### Proof.

(Sketch). The first part is established via a direct argument. To the second
part, let $\mathcal{L}_{A}=\\{\alpha_{d}\mid d\in K(A)\\}$ (where each
$\alpha_{d}$ is a new type constant) which is countable by hypothesis, and
take $\textit{Th}_{A}=\\{\alpha_{d}\leq_{A}\alpha_{e}\mid e\sqsubseteq d\\}$.
By observing that $\alpha_{d}\wedge_{A}\alpha_{e}=\alpha_{d\sqcup e}$, where
$d\sqcup e\in K(A)$ if $d,e\in K(A)$, and that $\omega_{A}=\alpha_{\top}$, we
have that $\textit{Th}_{A}$ is an intersection type theory and that
$\mathcal{L}_{A}/_{\leq_{A}}$ is isomorphic to $K^{\textit{op}}(A)$ ordered by
the opposite to the ordering of $A$. From this it follows that ${\cal F}_{A}$
is isomorphic to the ideal completion of $K(A)$, which in turn is isomorphic
to $A$ by algebraicity. ∎

The above proposition substantiates the claim that intersection type theories
are the logic of the domains in $\omega\text{-}\textrm{\bf ALG}$. The theory
$\textit{Th}_{A}$ is called the Lindenbaum algebra of $A$ in [2]; Prop. 4.3 is
the object part of the construction establishing that intersection type
theories, together with a suitable notion of morphisms among them, do form a
category that is equivalent to $\omega\text{-}\textrm{\bf ALG}$; such
equivalence is an instance of Stone duality as studied in [2] w.r.t. the
category of 2/3 SFP domains, when $\omega\text{-}\textrm{\bf ALG}$ is viewed
as a subcategory of topological spaces: see e.g. [4].

The second part in the proof of Prop. 4.3 is the most relevant to us: it
provides a recipe to describe a domain via a formal system, deriving
inequalities among type expressions that encode “finite approximations” of
points in a domain, hence of the denotations of terms if the domain is a
$\lambda_{imp}$-model. Therefore, we seek theories $\textit{Th}_{D}$ and
$\textit{Th}_{S}$ such that:

${\cal F}_{D}\cong[{\cal F}_{D}\xrightarrow{}[{\cal F}_{S}\xrightarrow{}({\cal
F}_{D}\times{\cal F}_{S})_{\bot}]]$ (5)

The first step is to show how the functors involved in the equation above,
namely the lifting, the product and the (continuous) function space, of which
$S=[\mathbb{L}\xrightarrow{}D]$ is a special case, can be put in
correspondence with the construction of new theories out of the theories which
determine the domains combined by the functors. As this is known after [2], we
just recall their definitions, and fix the notation.

######  Definition 4.4.

Suppose that the theories $\textit{Th}_{A}$ and $\textit{Th}_{B}$ are given,
then for $\alpha\in\mathcal{L}_{A}$ and $\beta\in\mathcal{L}_{B}$ define:

$\begin{array}[]{llll@{\hspace{1cm}}llll}\mathcal{L}_{A_{\bot}}{}&\psi&::=&\alpha\mid\psi\wedge\psi^{\prime}\mid\omega_{A_{\bot}}\hfil\hskip
28.45274pt&\mathcal{L}_{A\times
B}{}&\pi&::=&\alpha\times\beta\mid\pi\wedge\pi^{\prime}\mid\omega_{A\times
B}\\\
\mathcal{L}_{A\xrightarrow{}B}{}&\phi&::=&\alpha\xrightarrow{}\beta\mid\phi\wedge\phi^{\prime}\mid\omega_{A\xrightarrow{}B}\hfil\hskip
28.45274pt&\mathcal{L}_{stA}{}&\sigma&::=&\langle\ell:\alpha\rangle\mid\sigma\wedge\sigma^{\prime}\mid\omega_{S}\end{array}$

Then, we define the following sets of axioms:

  1. 1.

$\alpha\leq_{A}\alpha^{\prime}\Longrightarrow\alpha\leq_{A_{\bot}}\alpha^{\prime}$.

  2. 2.

$\omega_{A\times B}\leq_{A\times B}\omega_{A}\times\omega_{B}$ and all
instances of
$(\alpha\times\beta)\wedge(\alpha^{\prime}\times\beta^{\prime})\leq_{A\times
B}(\alpha\wedge\alpha^{\prime})\times(\beta\wedge\beta^{\prime})$.

  3. 3.

$\omega_{A\xrightarrow{}B}\leq_{A\xrightarrow{}B}\omega_{A}\xrightarrow{}\omega_{B}$
and all instances of
$(\alpha\xrightarrow{}\beta)\wedge(\alpha\xrightarrow{}\beta^{\prime})\leq_{A\xrightarrow{}B}\alpha\xrightarrow{}(\beta\wedge\beta^{\prime})$.

  4. 4.

$\omega_{S}\leq_{stA}\langle\ell:\omega_{A}\rangle$ and all instances of
$\langle\ell:\alpha\rangle\wedge\langle\ell:\alpha^{\prime}\rangle\leq_{stA}\langle\ell:\alpha\wedge\alpha^{\prime}\rangle$.

Finally, the theories $\textit{Th}_{A\times B}$,
$\textit{Th}_{A\xrightarrow{}B}$ and $\textit{Th}_{stA}$ are respectively
closed under the rules:

$\begin{array}[]{c@{\hspace{1cm}}c@{\hspace{1cm}}c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
3.01108pt\hbox{$\displaystyle\penalty
1\alpha\leq_{A}\alpha^{\prime}\quad\beta\leq_{B}\beta^{\prime}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=73.04831pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\alpha\times\beta\leq_{A\times
B}\alpha^{\prime}\times\beta^{\prime}$}}}}\hfil\hskip
28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\alpha^{\prime}\leq_{A}\alpha\quad\beta\leq_{B}\beta^{\prime}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=64.24844pt\hbox{}}}\hbox{\kern
2.48889pt\hbox{$\displaystyle\alpha\xrightarrow{}\beta\leq_{A\xrightarrow{}B}\alpha^{\prime}\xrightarrow{}\beta^{\prime}$}}}}\hfil\hskip
28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 19.8236pt\hbox{$\displaystyle\penalty
1\alpha\leq_{A}\alpha^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=68.73672pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\langle\ell:\alpha\rangle\leq_{stA}\langle\ell:\alpha^{\prime}\rangle$}}}\par}\end{array}$

If $X\in{\cal F}_{A\xrightarrow{}B}$ and $Y\in{\cal F}_{A}$, where either
$A=D$ and $B=\mathbb{S}\,D$ or $A=S$ and $B=(D\times S)_{\bot}$, we define:

$X\cdot Y=\\{\psi\mid\exists\varphi\in Y.\;\varphi\xrightarrow{}\psi\in X\\}$

We write $\varphi=_{A}\psi$ if $\varphi\leq_{a}\psi\leq_{A}\varphi$. For a map
$f:{\cal F}_{A}\xrightarrow{}{\cal F}_{B}$, define

$\Lambda(f)=\;\uparrow_{A\xrightarrow{}B}\\{\varphi\xrightarrow{}\psi\in\mathcal{L}_{A\xrightarrow{}B}\mid\psi\in
f(\uparrow_{A}\varphi)\\}$

######  Lemma 4.5.

If $X\in{\cal F}_{A\xrightarrow{}B}$ and $Y\in{\cal F}_{A}$ then $X\cdot
Y\in{\cal F}_{B}$. Moreover the map $\\_\,\cdot\,\\_$ is continuous in both
its arguments.

###### Proof.

We have $X\ni\omega_{A\xrightarrow{}B}\leq\omega_{A}\xrightarrow{}\omega_{B}$
and that $\omega_{A}\in Y$, hence $\omega_{B}\in X\cdot Y$. Since
$\xrightarrow{}$ is monotonic in its second argument, $X\cdot Y$ is upward
closed. Finally, if $\psi_{1},\psi_{2}\in X\cdot Y$ then $\varphi_{i}\in Y$
and $\varphi_{i}\xrightarrow{}\psi_{i}\in X$ for $i=1,2$ and some
$\varphi_{1},\varphi_{2}$; then, by antimonotonicity of $\xrightarrow{}$
w.r.t. its first argument,
$\varphi_{i}\xrightarrow{}\psi_{i}\leq\varphi_{1}\wedge\varphi_{2}\xrightarrow{}\psi_{i}\in
X$ being $X$ upward closed, and
$\varphi_{1}\wedge\varphi_{2}\xrightarrow{}\psi_{1}\wedge\psi_{2}=(\varphi_{1}\wedge\varphi_{2}\xrightarrow{}\psi_{1})\wedge(\varphi_{1}\wedge\varphi_{2}\xrightarrow{}\psi_{2})\in
X$ since $X$ is closed under intersections.

Concerning continuity, we have to show that $X\cdot Y=\bigsqcup{\cal Z}$ where
${\cal Z}=\\{\uparrow\varphi\;\cdot\uparrow\psi\mid\varphi\in X\And\psi\in
Y\\}$, and the sup of a family of filters is the least filter including the
union of the family. Inclusion from left to right follows by observing that if
$\chi\in X\cdot Y$ then $\psi\xrightarrow{}\chi\in X$ for some $\psi\in Y$,
and of course $\chi\in\;\uparrow(\psi\xrightarrow{}\chi)\;\cdot\uparrow\psi$.
Viceversa if $\chi\in\bigsqcup{\cal Z}$ then for finitely many
$\psi_{i},\chi_{i}$ we have that $\bigcap_{i}\chi_{i}\leq\chi$, $\psi_{i}\in
Y$ and $\psi_{i}\xrightarrow{}\chi_{i}\in X$. It follows that $\chi_{i}\in
X\cdot Y$ for all $i$, and hence the thesis since $X\cdot Y$ is a filter by
the above. ∎

######  Lemma 4.6.

If $f:{\cal F}_{A}\xrightarrow{}{\cal F}_{B}$ is continuous then
$\Lambda(f)\in{\cal F}_{A\xrightarrow{}B}$. $\Lambda(\cdot)$ is itself
continuous and such that:

$\Lambda(f)\cdot X=f(X)\qquad\Lambda(\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern 2.0mu\raisebox{1.18399pt}{$\lambda$}}Y.(X\cdot
Y))=X$

###### Proof.

Easy by unfolding definitions and by Lemma 4.5. ∎

Now we can establish:

######  Proposition 4.7.

The following are isomorphisms in $\omega\text{-}\textrm{\bf ALG}$:

${\cal F}_{A_{\bot}}\cong({\cal F}_{A})_{\bot},\quad{\cal F}_{A\times
B}\cong{\cal F}_{A}\times{\cal F}_{B},\quad{\cal
F}_{A\xrightarrow{}B}\cong[{\cal F}_{A}\xrightarrow{}{\cal
F}_{B}]\quad\mbox{and}\quad{\cal F}_{stA}\cong\mathbb{L}\xrightarrow{}{\cal
F}_{A}.$

###### Proof.

That ${\cal F}_{A_{\bot}}\cong({\cal F}_{A})_{\bot}$ is a consequence of the
fact that $\omega_{A}<_{A_{\bot}}\omega_{A_{\bot}}$ is strict, hence
$\uparrow\omega_{A_{\bot}}$ is the new bottom added to ${\cal F}_{A}$. ${\cal
F}_{A\times B}\cong{\cal F}_{A}\times{\cal F}_{B}$ is induced by the
continuous extension of the map
$\uparrow(\alpha\times\beta)\mapsto(\uparrow\alpha,\uparrow\beta)$, that is
clearly invertible. Finally, ${\cal F}_{A\xrightarrow{}B}\cong[{\cal
F}_{A}\xrightarrow{}{\cal F}_{B}]$ is Lemma 4.6, and ${\cal
F}_{stA}\cong[\mathbb{L}\xrightarrow{}{\cal F}_{A}]$ can be reduced to a
particular case of the latter by using the continuous extension of the map
$\uparrow\langle\ell:\delta\rangle\mapsto(\ell\mapsto\uparrow\delta)$. ∎

The next step is to apply Prop. 4.7 to describe the compact elements of
$D\cong{\cal F}_{D}$ and of $S\cong{\cal F}_{S}$ and the (inverse of) their
orderings. Alas, this cannot be done directly because of the recursive nature
of the equation (5), but it can be obtained by mirroring the inverse limit
construction, e.g. along the lines of [4, 6]. Although possible in principle,
such a construction requires lots of machinery from the theory of the solution
of domain equations; instead we follow the shorter path to define the involved
type theories below simply by mutual induction:

######  Definition 4.8.

Let us abbreviate $S=D^{\mathbb{L}}$ and $C=(D\times S)_{\bot}$; then define
the following itt languages by mutual induction:

$\begin{array}[]{llll@{\hspace{1cm}}llll}\mathcal{L}_{D}:&\delta&::=&\delta\xrightarrow{}\tau\mid\delta\wedge\delta^{\prime}\mid\omega_{D}\hfil\hskip
28.45274pt&\mathcal{L}_{S}:&\sigma&::=&\langle\ell:\delta\rangle\mid\sigma\wedge\sigma^{\prime}\mid\omega_{S}\\\
\mathcal{L}_{C}:&\kappa&::=&\delta\times\sigma\mid\kappa\wedge\kappa^{\prime}\mid\omega_{C}\hfil\hskip
28.45274pt&\mathcal{L}_{\mathbb{S}D}:&\tau&::=&\sigma\xrightarrow{}\kappa\mid\tau\wedge\tau^{\prime}\mid\omega_{\mathbb{S}D}\end{array}$

We assume that $\wedge$ and $\times$ take precedence over $\xrightarrow{}$ and
that $\xrightarrow{}$ associates to the right so that
$\delta\xrightarrow{}\tau\wedge\tau^{\prime}$ reads as
$\delta\xrightarrow{}(\tau\wedge\tau^{\prime})$ and
$\delta^{\prime}\xrightarrow{}\sigma^{\prime}\xrightarrow{}\delta^{\prime\prime}\times\sigma^{\prime\prime}$
reads as
$\delta^{\prime}\xrightarrow{}(\sigma^{\prime}\xrightarrow{}(\delta^{\prime\prime}\times\sigma^{\prime\prime}))$.

Then the relations $\leq_{D},\leq_{S},\leq_{C}$ and $\leq_{\mathbb{S}D}$ are
the least itt’s over the respective languages satisfying the following axioms:

$\begin{array}[]{c@{\hspace{1cm}}c}(\delta\xrightarrow{}\tau)\wedge(\delta\xrightarrow{}\tau^{\prime})\leq_{D}\delta\xrightarrow{}\tau\wedge\tau^{\prime}\hfil\hskip
28.45274pt&\omega_{D}\leq_{D}\omega_{D}\xrightarrow{}\omega_{\mathbb{S}D}\\\\[5.69054pt]
\langle\ell:\delta\rangle\wedge\langle\ell:\delta^{\prime}\rangle\leq_{S}\langle\ell:\delta\wedge\delta^{\prime}\rangle\hfil\hskip
28.45274pt&\omega_{S}\leq_{S}\langle\ell:\omega_{D}\rangle\\\\[5.69054pt]
\lx<EMAIL_ADDRESS>(\sigma\xrightarrow{}\kappa)\wedge(\sigma\xrightarrow{}\kappa^{\prime})\leq_{\mathbb{S}D}\sigma\xrightarrow{}\kappa\wedge\kappa^{\prime}\hfil\hskip
28.45274pt&\omega_{\mathbb{S}D}\leq_{\mathbb{S}D}\omega_{S}\xrightarrow{}\omega_{C}\end{array}$

and closed under the rules:

$\begin{array}[]{c@{\hspace{8mm}}c@{\hspace{8mm}}c@{\hspace{8mm}}c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\delta^{\prime}\leq_{D}\delta\quad\tau\leq_{\mathbb{S}D}\tau^{\prime}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.74016pt\hbox{}}}\hbox{\kern
7.8404pt\hbox{$\displaystyle\delta\xrightarrow{}\tau\leq_{D}\delta^{\prime}\xrightarrow{}\tau^{\prime}$}}}}\hfil\hskip
22.76219pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 18.37122pt\hbox{$\displaystyle\penalty
1\delta\leq_{D}\delta^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=62.5187pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\langle\ell:\delta\rangle\leq_{S}\langle\ell:\delta^{\prime}\rangle$}}}}\hfil\hskip
22.76219pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\delta\leq_{D}\delta^{\prime}\quad\sigma\leq_{S}\sigma^{\prime}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=63.0567pt\hbox{}}}\hbox{\kern
1.23949pt\hbox{$\displaystyle\delta\times\sigma\leq_{C}\delta^{\prime}\times\sigma^{\prime}$}}}}\hfil\hskip
22.76219pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\sigma^{\prime}\leq_{S}\sigma\quad\kappa\leq_{C}\kappa^{\prime}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=62.52437pt\hbox{}}}\hbox{\kern
4.01721pt\hbox{$\displaystyle\sigma\xrightarrow{}\kappa\leq_{\mathbb{S}D}\sigma^{\prime}\xrightarrow{}\kappa^{\prime}$}}}}\end{array}$

######  Remark 4.9.

Observe that the only constants used in Def. 4.8 are the $\omega$’s; also we
have plenty of equivalences $\varphi=\psi$, namely relations
$\varphi\leq\psi\leq\varphi$, involving these constants, that are induced by
the definition of the itt’s above. For example
$\delta\xrightarrow{}\omega_{\mathbb{S}D}=\omega_{D}$ is derivable since
$\omega_{D}\leq_{D}\delta\xrightarrow{}\omega_{\mathbb{S}D}\leq_{D}\omega_{D}$
are axioms of $\textit{Th}_{D}$; similarly
$\langle\ell:\omega_{D}\rangle=\omega_{S}$ and
$\omega_{S}\xrightarrow{}\omega_{C}=\omega_{\mathbb{S}D}$.

However, none of the theories above is trivial, because
$\omega_{C}\not\leq_{C}\omega_{D}\times\omega_{S}$. This is implied by
$\uparrow\omega_{C}\subset\;\uparrow(\omega_{D}\times\omega_{S})$, that is
$\uparrow\omega_{C}$ corresponds to the new bottom element added to ${\cal
F}_{D\times S}\cong{\cal F}_{D}\times{\cal F}_{S}$ in ${\cal F}_{C}={\cal
F}_{(D\times S)_{\bot}}\cong({\cal F}_{D\times S})_{\bot}$.

The choice of not having atomic types $\alpha$ in $\mathcal{L}_{D}$ is
minimalistic, and parallels the analogous definition 5.2.1 of [3], where the
only constant in the domain logic of a lazy $\lambda$-model
$D\cong[D\xrightarrow{}D]_{\bot}$ is $t$ (true), corresponding to our
$\omega_{D}$, and having $t\not\leq(t\xrightarrow{}t)_{\bot}$ in the theory.

As a more careful description of ${\cal F}_{D}$ would show, by relating its
construction to the solution of eq. (2) in Theorem 3.5, the reason why the
$\omega$’s suffice is that the domain equation has a non trivial initial
solution. Adding atomic types $\alpha$ to $\mathcal{L}_{D}$ also leads to a
filter model ${\cal F}_{D^{\prime}}$ of $\lambda_{imp}$, which is however not
isomorphic to $[{\cal F}_{D^{\prime}}\xrightarrow{}\mathbb{S}({\cal
F}_{D^{\prime}})]$, which is what we show to hold for ${\cal F}_{D}$ in the
next theorem. To restore the desired isomorphism it suffices to add axioms
$\alpha=_{D^{\prime}}\omega_{D^{\prime}}\xrightarrow{}\omega_{S}\xrightarrow{}(\alpha\times\omega_{S})$
for all atomic $\alpha$: these correspond to the axioms
$\alpha=\omega\xrightarrow{}\alpha$ in [7], which are responsible of obtaining
a “natural equated” solution to the equation $D=[D\xrightarrow{}D]$ of Scott’s
model: see [6].

######  Theorem 4.10.

The theories $\textit{Th}_{D}$ and $\textit{Th}_{S}$ induce the filter domains
${\cal F}_{D}$ and ${\cal F}_{S}$ which satisfy equation (5).

###### Proof.

By Prop. 4.7, ${\cal F}_{D\xrightarrow{}\mathbb{S}D}\cong[{\cal
F}_{D}\xrightarrow{}{\cal F}_{\mathbb{S}D}]\cong[{\cal
F}_{D}\xrightarrow{}[{\cal F}_{S}\xrightarrow{}({\cal F}_{D}\times{\cal
F}_{S})_{\bot}]]$; then the thesis follows since ${\cal F}_{D}={\cal
F}_{D\xrightarrow{}\mathbb{S}D}$ by construction. ∎

The $\lambda_{imp}$ filter model. According to Def. 3.6, to show that ${\cal
F}_{D}$ is a $\lambda_{imp}$-model it remains to see that ${\cal
F}_{\mathbb{S}D}\cong\mathbb{S}{\cal F}_{D}$ can be endowed with the structure
of a monad, which amounts to say that the maps $\textit{unit}^{\cal F}:{\cal
F}_{D}\xrightarrow{}{\cal F}_{\mathbb{S}D}$ and $\star^{\cal F}:{\cal
F}_{\mathbb{S}D}\times[{\cal F}_{D}\xrightarrow{}{\cal
F}_{\mathbb{S}D}]\xrightarrow{}{\cal F}_{\mathbb{S}D}$ are definable in such a
way to satisfy the monadic laws. This easily follows by instantiating the
definition of the state monad Def. 3.3 to the subcategory of filter domains:

$\textit{unit}^{\cal F}X=_{\textit{def}}\Lambda(\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern 2.0mu\raisebox{1.18399pt}{$\lambda$}}Y\in{\cal
F}_{S}.(X,Y))=\;{\tt
Filt}\\{\sigma\xrightarrow{}\delta\times\sigma\in\mathcal{L}_{\mathbb{S}D}\mid\delta\in
X\\}$ (6)

where ${\tt Filt}\,U$ is the least filter including the set $U$. On the other
hand, observing that ${\cal F}_{\mathbb{S}D}\times[{\cal
F}_{D}\xrightarrow{}{\cal F}_{\mathbb{S}D}]\xrightarrow{}{\cal
F}_{\mathbb{S}D}\cong{\cal F}_{\mathbb{S}D}\times{\cal
F}_{D}\xrightarrow{}{\cal F}_{\mathbb{S}D}$, for all $X\in{\cal
F}_{\mathbb{S}D}$, $Y\in{\cal F}_{D}$ and $Z\in{\cal F}_{S}$ we expect that:

$(X\star^{\cal F}Y)\cdot Z=\mbox{{let} $(U,V)=X\cdot Z$ {in} $(Y\cdot U)\cdot
V$}=\left\\{\begin{array}[]{ll}(Y\cdot U)\cdot V&\mbox{if $X\cdot Z=U\times
V\neq\;\uparrow_{C}\omega_{C}$}\\\\[2.84526pt]
\uparrow_{C}\omega_{C}&\mbox{otherwise}\end{array}\right.$

Hence we put

$X\star^{\cal F}Y=_{\textit{def}}{\tt
Filt}\\{\sigma\xrightarrow{}\delta^{\prime\prime}\times\sigma^{\prime\prime}\in\mathcal{L}_{\mathbb{S}D}\mid\exists\delta^{\prime},\sigma^{\prime}.\;\sigma\xrightarrow{}\delta^{\prime}\times\sigma^{\prime}\in
X\And\delta^{\prime}\xrightarrow{}\sigma^{\prime}\xrightarrow{}\delta^{\prime\prime}\times\sigma^{\prime\prime}\in
Y\\}\;\cup\;\uparrow_{C}\omega_{C}$ (7)

The final step is to define the interpretations of $\textit{get}_{\ell}:({\cal
F}_{D}\xrightarrow{}{\cal F}_{\mathbb{S}D})\xrightarrow{}{\cal
F}_{\mathbb{S}D}\cong{\cal F}_{D}\xrightarrow{}{\cal F}_{\mathbb{S}D}$ and
$\textit{set}_{\ell}:{\cal F}_{D}\times{\cal
F}_{\mathbb{S}D}\xrightarrow{}{\cal F}_{\mathbb{S}D}$, which also are
derivable from their interpretation into a generic model $\cal D$. Indeed,
according to Def. 3.6, for any $X\in{\cal F}_{D}$ and $Y\in{\cal F}_{S}$ we
must have:

$\textit{get}_{\ell}(X)\cdot Y=X\cdot(Y\cdot\\{\ell\\})\cdot Y$

where we assume that $\\_\,\cdot\,\\_$ associates to the left, and we
abbreviate
$Y\cdot\\{\ell\\}=\\{\delta\in\mathcal{L}_{D}\mid\langle\ell:\delta\rangle\in
Y\\}$ representing the application of the “store” $Y$ to the location $\ell$.
Now, let
$Z=_{\textit{def}}\\{\tau\in\mathcal{L}_{\mathbb{S}D}\mid\exists\delta\in
Y\cdot\\{\ell\\}.\;\delta\xrightarrow{}\tau\in X\\}$ then

$X\cdot(Y\cdot\\{\ell\\})\cdot Y=Z\cdot Y$

If $\tau=\omega_{\mathbb{S}D}$ then $\delta\xrightarrow{}\tau=\omega_{D}$,
which trivially belongs to any filter; if instead
$\tau\neq\omega_{\mathbb{S}D}$ then
$\tau=\bigwedge_{I}\sigma_{i}\xrightarrow{}\kappa_{i}$ and
$\delta\xrightarrow{}\tau\in X$ if and only if
$\delta\xrightarrow{}\sigma_{i}\xrightarrow{}\kappa_{i}\in X$ for all $i\in
I$. From this we conclude that

$Z\cdot Y=\\{\kappa\in\mathcal{L}_{C}\mid\exists\sigma\in
Y\mid\sigma\xrightarrow{}\kappa\in
Z\\}=\\{\kappa\in\mathcal{L}_{C}\mid\exists\langle\ell:\delta\rangle\wedge\sigma\in
Y.\;\delta\xrightarrow{}\sigma\xrightarrow{}\kappa\in X\\}$

and therefore the appropriate definition of $\textit{get}_{\ell}(X)$ is

$\textit{get}_{\ell}(X)=_{\textit{def}}\;{\tt
Filt}\\{(\langle\ell:\delta\rangle\wedge\sigma)\xrightarrow{}\kappa\in\mathcal{L}_{\mathbb{S}D}\mid\delta\xrightarrow{}(\sigma\xrightarrow{}\kappa)\in
X\\}$ (8)

Similarly, again by Def. 3.6, for any $X\in{\cal F}_{D}$, $Y\in{\cal
F}_{\mathbb{S}D}$ and $Z\in{\cal F}_{S}$ we expect:

$\textit{set}^{\cal F}_{\ell}(X,Y)\cdot Z=Y\cdot(Z[\ell\mapsto X])$

where $Z[\ell\mapsto X]$ is supposed to represent the update of $Z$ by
associating $X$ to $\ell$, namely:

$Z[\ell\mapsto X]={\tt Filt}\\{\\{\langle\ell:\delta\rangle\mid\delta\in
X\\}\cup\\{\langle\ell^{\prime}:\delta^{\prime}\rangle\mid\langle\ell^{\prime}:\delta^{\prime}\rangle\in
Z\;\And\;\ell^{\prime}\neq\ell\\}\\}$

Then

$\begin{array}[]{rcl}Y\cdot(Z[\ell\mapsto X])&=&{\tt
Filt}\\{\kappa\mid\exists\sigma\xrightarrow{}\kappa\in Z[\ell\mapsto
X].\;\sigma\xrightarrow{}\kappa\in Y\\}\\\\[2.84526pt] &=&{\tt
Filt}\\{\kappa\mid\exists\sigma^{\prime}\in Z,\delta\in
X.\;\langle\ell:\delta\rangle\wedge\sigma^{\prime}\xrightarrow{}\kappa\in
Y\;\And\;\ell\not\in\textit{dom}(\sigma^{\prime})\\}\end{array}$

and therefore we define:

$\textit{set}^{\cal F}_{\ell}(X,Y)=_{\textit{def}}{\tt
Filt}\\{\sigma^{\prime}\xrightarrow{}\kappa\in\mathcal{L}_{\mathbb{S}D}\mid\exists\delta\in
X.\;\langle\ell:\delta\rangle\wedge\sigma^{\prime}\xrightarrow{}\kappa\in
Y\;\And\;\ell\not\in\textit{dom}(\sigma^{\prime})\\}$ (9)

Eventually, by construction we have:

######  Theorem 4.11.

The structure ${\cal F}=({\cal
F}_{D},\mathbb{S},\llbracket\cdot\rrbracket^{{\cal
F}_{D}},\llbracket\cdot\rrbracket^{{\cal F}_{\mathbb{S}D}})$ is a
$\lambda_{imp}$-model where, for $e:\textit{Var}\xrightarrow{}{\cal F}_{D}$
the interpretations $\llbracket V\rrbracket^{{\cal F}_{D}}e\in{\cal F}_{D}$
and $\llbracket M\rrbracket^{{\cal F}_{\mathbb{S}D}}e\in{\cal
F}_{\mathbb{S}D}$ are defined by:

$\begin{array}[]{rcl@{\hspace{2cm}}rcl}\llbracket x\rrbracket^{{\cal
F}_{D}}e&=&e(x)\hfil\hskip 56.9055pt&\llbracket\lambda x.M\rrbracket^{{\cal
F}_{D}}e&=&\Lambda(\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}X\in{\cal F}_{D}.\;\llbracket
M\rrbracket^{{\cal F}_{\mathbb{S}D}}e[x\mapsto X])\\\\[2.84526pt]
\llbracket[V]\rrbracket^{{\cal F}_{\mathbb{S}D}}e&=&\textit{unit}^{\cal
F}(\llbracket V\rrbracket^{{\cal F}_{D}}e)\hfil\hskip 56.9055pt&\llbracket
M\star V\rrbracket^{{\cal F}_{\mathbb{S}D}}e&=&(\llbracket M\rrbracket^{{\cal
F}_{\mathbb{S}D}}e)\star^{\cal F}(\llbracket V\rrbracket^{{\cal
F}_{D}}e)\\\\[2.84526pt] \llbracket\textit{get}_{\ell}(\lambda
x.M)\rrbracket^{{\cal
F}_{\mathbb{S}D}}e&=&\textit{get}_{\ell}(\llbracket\lambda
x.M\rrbracket^{{\cal F}_{D}}e)\hfil\hskip
56.9055pt&\llbracket\textit{set}_{\ell}(V,M)\rrbracket^{{\cal
F}_{\mathbb{S}D}}e&=&\textit{set}^{\cal F}_{\ell}(\llbracket
V\rrbracket^{{\cal F}_{D}},\llbracket M\rrbracket^{{\cal
F}_{\mathbb{S}D}}e)\end{array}$

###### Proof.

By applying equations (6)-(9) to the clauses of Def. 3.6. ∎

##  5 Deriving the type assignment system

The definition of a type assignment system can be obtained out of the
construction of the filter-model. The system is nothing else than the
description of the denotation of terms in the particular $\lambda_{imp}$-model
${\cal F}$, which is possible because both $\llbracket V\rrbracket^{{\cal
F}_{D}}e\in{\cal F}_{D}$ and $\llbracket M\rrbracket^{{\cal
F}_{\mathbb{S}D}}e\in{\cal F}_{\mathbb{S}D}$, and filters are sets of types.

Types are naturally interpreted as subsets of the domains of term
interpretation, namely ${\cal F}_{D}$ or ${\cal F}_{\mathbb{S}D}$ according to
their kind; by applying to the present case the same construction as in [7]
and [2], which originates from Stone duality for boolean algebras, we set:

######  Definition 5.1.

For $A=D,S,C$ and $\mathbb{S}D$ and $\varphi\in\mathcal{L}_{A}$ define:

$\llbracket\varphi\rrbracket^{{\cal F}}=\\{X\in{\cal F}_{A}\mid\varphi\in
X\\}$

Such interpretation is a generalization of the natural interpretation of
intersection types over an extended type structure [13], which in the present
case yields:

######  Proposition 5.2.

For $A=D,S,C$ and $\mathbb{S}D$ and $\varphi,\psi\in\mathcal{L}_{A}$ we have:

$\llbracket\varphi\wedge\psi\rrbracket^{{\cal
F}}=\llbracket\varphi\rrbracket^{{\cal F}}\cap\llbracket\psi\rrbracket^{{\cal
F}},\qquad\llbracket\omega_{A}\rrbracket^{{\cal F}}={\cal
F}_{A}\quad\mbox{and}\quad\varphi\leq\psi\Longrightarrow\llbracket\varphi\rrbracket^{{\cal
F}}\subseteq\llbracket\psi\rrbracket^{{\cal F}}$

Moreover:

  1. 1.

$\llbracket\delta\xrightarrow{}\tau\rrbracket^{{\cal F}}=\\{X\in{\cal
F}_{D}\mid\forall Y\in\llbracket\delta\rrbracket^{{\cal F}}.\;X\cdot
Y\in\llbracket\tau\rrbracket^{{\cal F}}\\}$

  2. 2.

$\llbracket\langle\ell:\delta\rangle\rrbracket^{{\cal F}}=\\{X\in{\cal
F}_{S}\mid X\cdot\\{\ell\\}\in\llbracket\delta\rrbracket^{{\cal F}}\\}$

  3. 3.

$\llbracket\delta\times\sigma\rrbracket^{{\cal F}}=\\{X\in{\cal
F}_{C}\mid\pi_{1}(X)\in\llbracket\delta\rrbracket^{{\cal
F}}\And\pi_{2}(X)\in\llbracket\sigma\rrbracket^{{\cal F}}\\}$

  4. 4.

$\llbracket\sigma\xrightarrow{}\kappa\rrbracket^{{\cal F}}=\\{X\in{\cal
F}_{\mathbb{S}D}\mid\forall Y\in\llbracket\sigma\rrbracket^{{\cal F}}.\;X\cdot
Y\in\llbracket\kappa\rrbracket^{{\cal F}}\\}$

where, for $X\in{\cal F}_{C}\cong({\cal F}_{D}\times{\cal F}_{S})_{\bot}$,
$\pi_{1}(X)=\\{\delta\in\mathcal{L}_{D}\mid\exists\sigma\in\mathcal{L}_{S}.\;\delta\times\sigma\in
X\\}$ and similarly for $\pi_{2}(X)$.

###### Proof.

The first part is immediate from the definition of type interpretation and of
filters. Concerning the remaining statements, we prove just (1) as the other
ones are similar. First observe that
$\uparrow\varphi\in\llbracket\varphi\rrbracket^{{\cal F}}$. Hence, if
$X\in\llbracket\delta\xrightarrow{}\tau\rrbracket^{{\cal F}}$ then
$\delta\xrightarrow{}\tau\in X$, which implies that
$X\cdot\uparrow\delta=\;\uparrow\tau\in\llbracket\tau\rrbracket^{{\cal F}}$.
Viceversa if $X\cdot Y\in\llbracket\tau\rrbracket^{{\cal F}}$ for all
$Y\in\llbracket\delta\rrbracket^{{\cal F}}$ then in particular
$X\cdot\uparrow\delta=\;\uparrow\tau\in\llbracket\tau\rrbracket^{{\cal F}}$,
which implies that for some $\delta^{\prime}\in\;\uparrow\delta$,
$\delta^{\prime}\xrightarrow{}\tau\in X$; but then
$\delta\leq_{D}\delta^{\prime}$ so that
$\delta^{\prime}\xrightarrow{}\tau\leq_{D}\delta\xrightarrow{}\tau$ and
therefore $\delta\xrightarrow{}\tau\in X$ as $X$ is upward closed. ∎

We can now build the type assignment system as the description, via type
derivations, of the semantics of terms and types in the model ${\cal F}$.
First, type contexts $\Gamma=\\{x_{1}:\delta_{1},\ldots,x_{n}:\delta_{n}\\}$
are put into correspondence with environments
$e_{\Gamma}:\textit{Var}\xrightarrow{}{\cal F}_{D}$ by setting
$e_{\Gamma}(x_{i})=\;\uparrow_{D}\delta_{i}$. Second, typing judgments
translate the statements:

$\Gamma\vdash V:\delta\iff(\llbracket V\rrbracket^{{\cal
F}_{D}}e_{\Gamma})\in\llbracket\delta\rrbracket^{\cal
F}\iff\delta\in\llbracket V\rrbracket^{{\cal F}_{D}}e_{\Gamma}$

and similarly, $\Gamma\vdash M:\tau\iff\tau\in\llbracket M\rrbracket^{{\cal
F}_{\mathbb{S}D}}e_{\Gamma}$.

Third and final step, typing rules of the shape

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma_{1}\vdash
P_{1}:\varphi_{1}\quad\cdots\quad\Gamma_{n}\vdash P_{n}:\varphi_{n}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=116.07407pt\hbox{}}}\hbox{\kern
37.70242pt\hbox{$\displaystyle\Gamma\vdash Q:\psi$}}}}$

are the translations of equations

$\llbracket Q\rrbracket^{\cal F}e_{\Gamma}={\tt
Filt}\\{\psi\mid\varphi_{1}\in\llbracket P_{1}\rrbracket^{\cal
F}e_{\Gamma_{1}}\And\cdots\And\varphi_{n}\in\llbracket P_{n}\rrbracket^{\cal
F}e_{\Gamma_{n}}\\}$ (10)

derived from Prop. 5.2 and Thr. 4.11. We take advantage of the factorization
of the right hand sides of equations (10) into a set of types $U$ and its
closure $\texttt{Filt}(U)$, by adding the rules:

$\begin{array}[]{c@{\hspace{1cm}}c@{\hspace{1cm}}c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
20.14166pt\hbox{$\displaystyle\penalty 1\vspace{3mm}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=40.28333pt\hbox{\kern
3.00003pt$(\omega)$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Gamma\vdash
P:\omega$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
P:\varphi\quad\Gamma\vdash P:\psi$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=88.39548pt\hbox{\kern
3.00003pt$(\wedge)$}}}\hbox{\kern 15.08504pt\hbox{$\displaystyle\Gamma\vdash
P:\varphi\wedge\psi$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash P:\varphi\quad\varphi\leq\psi$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=76.98929pt\hbox{\kern
3.00003pt$(\leq)$}}}\hbox{\kern 18.2083pt\hbox{$\displaystyle\Gamma\vdash
P:\psi$}}}}\end{array}$ (11)

Therefore we are left to translate set inclusions

$\llbracket Q\rrbracket^{\cal
F}e_{\Gamma}\supseteq\\{\psi\mid\varphi_{1}\in\llbracket P_{1}\rrbracket^{\cal
F}e_{\Gamma_{1}}\And\cdots\And\varphi_{n}\in\llbracket P_{n}\rrbracket^{\cal
F}e_{\Gamma_{n}}\\}$ (12)

where $\psi$ is neither an intersection nor an $\omega$:

######  Definition 5.3.

(Intersection type assignement system for $\lambda_{imp}$) The system is
obtained by adding to the rules (11) the following:

<EMAIL_ADDRESS>spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 29.11784pt\hbox{$\displaystyle\penalty
1\vspace{3mm}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=58.23569pt\hbox{\kern
3.00003pt$(\textit{var})$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:\delta\vdash x:\delta$}}}}\hfil\hskip
17.07182pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 0.97232pt\hbox{$\displaystyle\penalty
1\Gamma,\,x:\delta\vdash M:\tau$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=66.85043pt\hbox{\kern
3.00003pt$(\lambda)$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lambda
x.M:\delta\xrightarrow{}\tau$}}}}\\\\[17.07164pt] {tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
17.10298pt\hbox{$\displaystyle\penalty 1\Gamma\vdash V:\delta$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=72.95572pt\hbox{\kern
3.00003pt$(\textit{unit})$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash[V]:\sigma\xrightarrow{}\delta\times\sigma$}}}}\hfil\hskip
17.07182pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
M:\sigma\xrightarrow{}\delta^{\prime}\times\sigma^{\prime}\quad\Gamma\vdash
V:\delta^{\prime}\xrightarrow{}\sigma^{\prime}\xrightarrow{}\delta^{\prime\prime}\times\sigma^{\prime\prime}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=164.8565pt\hbox{\kern
3.00003pt$(\star)$}}}\hbox{\kern 36.64127pt\hbox{$\displaystyle\Gamma\vdash
M\star
V:\sigma\xrightarrow{}\delta^{\prime\prime}\times\sigma^{\prime\prime}$}}}}\\\\[17.07164pt]
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
27.2779pt\hbox{$\displaystyle\penalty 1\Gamma,\,x:\delta\vdash
M:\sigma\xrightarrow{}\kappa$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=131.56577pt\hbox{\kern
3.00003pt$(\textit{get})$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\textit{get}_{\ell}(\lambda
x.M):(\langle\ell:\delta\rangle\wedge\sigma)\xrightarrow{}\kappa$}}}}\hfil\hskip
17.07182pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash V:\delta\quad\Gamma\vdash
M:(\langle\ell:\delta\rangle\wedge\sigma)\xrightarrow{}\kappa\quad\ell\not\in\textit{dom}(\sigma)$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=207.14767pt\hbox{\kern
3.00003pt$(\textit{set})$}}}\hbox{\kern
61.59302pt\hbox{$\displaystyle\Gamma\vdash\textit{set}_{\ell}(V,M):\sigma\xrightarrow{}\kappa$}}}}\end{array}$

The rules in Definition 5.3 are obtained by instantiating the inclusion (12)
to equations (6) - (9). In conclusion, we obtain for our type system the
analogous of the “Type-semantics theorem” for intersection types and the
ordinary $\lambda$-calculus (see [8], Thr. 16.2.7):

######  Theorem 5.4.

Let $e\models^{\cal F}\Gamma$ if and only if
$e(x)\in\llbracket\delta\rrbracket^{\cal F}$ whenever $x:\delta\in\Gamma$;
then

  1. 1.

$\llbracket V\rrbracket^{{\cal
F}_{D}}e=\\{\delta\in\mathcal{L}_{D}\mid\exists\Gamma.\;e\models^{\cal
F}\Gamma\And\Gamma\vdash V:\delta\\}$

  2. 2.

$\llbracket M\rrbracket^{{\cal
F}_{\mathbb{S}D}}e=\\{\tau\in\mathcal{L}_{\mathbb{S}D}\mid\exists\Gamma.\;e\models^{\cal
F}\Gamma\And\Gamma\vdash M:\tau\\}$

###### Proof.

Observe that $e\models^{\cal F}\Gamma$ if and only if
$e_{\Gamma}(x)=\;\uparrow\delta\subseteq e(x)$ if $x:\delta\in\Gamma$; since
any filter $X$ is the union of the principal filters $\uparrow\delta$ with
$\delta\in X$, the proof reduces to establishing that $\llbracket
V\rrbracket^{{\cal
F}_{D}}e_{\Gamma}=\\{\delta\in\mathcal{L}_{D}\mid\Gamma\vdash V:\delta\\}$,
and similarly for $\llbracket M\rrbracket^{{\cal F}_{\mathbb{S}D}}e_{\Gamma}$;
the latter are an easy induction over term interpretations into ${\cal F}$ for
left to right inclusions, and over type derivations for the inclusions from
right to left. ∎

In spite of the complexity of the construction we have been going through in
the last sections, the payoff of our work is a system with just one typing
rule for each syntactical construct in the grammar of the calculus, plus the
“logical” rules (11) which are standard in intersection type systems with
subtyping since [7].

Moreover, by the obvious interpretation $\llbracket\varphi\rrbracket^{\cal D}$
of types in a model $\cal D$, of which Prop. 5.2 is the instance in case of
${\cal F}$, we get soundness and completeness theorems for free. Indeed,
without entering into the details, we claim that:

$\Gamma\models V:\delta~{}\iff~{}\Gamma\vdash
V:\delta\quad\mbox{and}\quad\Gamma\models M:\tau~{}\iff~{}\Gamma\vdash
M:\tau.$

where for a $\lambda_{imp}$-model ${\cal D}$ we write $\Gamma\models^{\cal
D}T:\varphi$ if $\llbracket T\rrbracket^{\cal
D}e\in\llbracket\varphi\rrbracket^{\cal D}$ for all $e\models^{\cal D}\Gamma$,
and write $\Gamma\models T:\varphi$ if $\Gamma\models^{\cal D}T:\varphi$ for
all $\cal D$.

##  6 Discussion and Related works

This work is a development of [15], where we considered a pure untyped
computational $\lambda$-calculus, namely without operations nor constants.
Therefore, the monad $T$ and the respective unit and bind were generic, so
that types cannot convey any specific information about the domain $TD$, nor
about effects represented by the monad.

In the unpublished report [16] we sketched the construction of the type system
for the state monad $\mathbb{S}$. This has been motivated on the ground of an
operational interpretation of terms that we illustrated, culminating in the
characterization of convergence via the type system. This is akin to the lazy
$\lambda$-calculus [3], where convergent terms are characterized by the
formula $(t\xrightarrow{}t)_{\bot}$ of the endogenous logic of the calculus,
in the sense of [2].

While deferring the exposition of the convergence characterization to a
companion paper, here we have focussed on the construction of the type system
itself. Since [7] we know that a $\lambda$-model can be constructed by taking
the filters of types in an intersection type system with subtyping. The
relation among the filter-model and Scott’s $D_{\infty}$ construction has been
subject to extensive studies, starting with [13] and continuing with [17, 4,
5, 6]. In the meantime Abramsky’s theory of domain logic in [2] provided a
generalization of the same ideas to algebraic domains in the category of 2/3
SFP, of which $\omega\text{-}\textrm{\bf ALG}$ is a (full) subcategory, based
on Stone duality.

In the present work, we use the mathematical theories just mentioned, but
reversing the process from semantics to types. Usually, one starts with a
calculus and a type system, looking for a semantics and studying properties of
the model. On the contrary, we move from a domain equation and the definition
of the denotational semantics of the calculus of interest and synthesize a
filter-model and an intersection type system. This synthetic use of domain
logic is, in our view, prototypical w.r.t. the construction of type systems
catching properties of any computational $\lambda$-calculus with operators. We
expect that the study of such systems will be of help in understanding the
operational semantics of such models, a topic that has been addressed in [14,
21], but with different mathematical tools.

A further research direction is to move from $\omega\text{-}\textrm{\bf ALG}$
to other categories such as the category of relations. The latter is deeply
related to non-idempotent intersection types [12, 11] that have been shown to
catch intensional aspects of $\lambda$-calculi involving quantitative
reasoning about computational resources. If the present approach can be
rephrased in the category of relations, then our method could produce non-
idempotent intersection type systems for effectful $\lambda$-calculi.

In the perspective of considering categories other than
$\omega\text{-}\textrm{\bf ALG}$, it is natural to ask whether the synthesis
of an “estrinisic” type system in the sense of Reynolds out of the
denotational semantics of a calculus, either typed or not, can be described in
categorical terms. Intersection type theories and related systems, as we have
been using in this work, are a special case of refinement type systems; a
starting point may be the framing of refinement type systems as functors in
[22].

Acknowledgements. We are grateful to the anonymous referees for their comments
and hints to categorical prospectives of the present work.

## References

  * [1]
  * [2] S. Abramsky (1991): _Domain Theory in Logical Form_.  Ann. Pure Appl. Log. 51(1-2), pp. 1–77, 10.1016/0168-0072(91)90065-T.
  * [3] S. Abramsky & C.-H.L. Ong (1993): _Full abstraction in the lazy lambda calculus_.  Inf. Comput. 105(2), pp. 159–267, 10.1006/inco.1993.1044.
  * [4] F. Alessi, M. Dezani-Ciancaglini & F. Honsell (2004): _Inverse Limit Models as Filter Models_.  In Delia Kesner, Femke van Raamsdonk & Joe Wells, editors: HOR’04, RWTH Aachen, Aachen, pp. 3–25.
  * [5] F. Alessi, F. Barbanera & M. Dezani-Ciancaglini (2006): _Intersection types and lambda models_.  Theor. Comput. Sci. 355(2), pp. 108–126, 10.1016/j.tcs.2006.01.004.
  * [6] F. Alessi & P. Severi (2008): _Recursive Domain Equations of Filter Models_.  In Viliam Geffert, Juhani Karhumäki, Alberto Bertoni, Bart Preneel, Pavol Návrat & Mária Bieliková, editors: SOFSEM 2008: Theory and Practice of Computer Science, 34th Conference on Current Trends in Theory and Practice of Computer Science, Nový Smokovec, Slovakia, January 19-25, 2008, Proceedings, Lecture Notes in Computer Science 4910, Springer, pp. 124–135, 10.1007/978-3-540-77566-9_11.
  * [7] H. P. Barendregt, M. Coppo & M. Dezani-Ciancaglini (1983): _A Filter Lambda Model and the Completeness of Type Assignment_.  J. Symb. Log. 48(4), pp. 931–940, 10.2307/2273659.
  * [8] H. P. Barendregt, W. Dekkers & R. Statman (2013): _Lambda Calculus with Types_.  Perspectives in logic, Cambridge University Press, 10.1017/CBO9781139032636.
  * [9] N. Benton, J. Hughes & E. Moggi (2002): _Monads and Effects_.  In: Applied Semantics, International Summer School, APPSEM 2000, Lecture Notes in Computer Science 2395, Springer, pp. 42–122, 10.1007/3-540-45699-6_2.
  * [10] N. Benton, A. Kennedy, L. Beringer & M. Hofmann (2009): _Relational semantics for effect-based program transformations: higher-order store_.  In António Porto & Francisco Javier López-Fraguas, editors: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, ACM, pp. 301–312, 10.1145/1599410.1599447.
  * [11] A. Bucciarelli, T. Ehrhard & G. Manzonetto (2007): _Not Enough Points Is Enough_.  In Jacques Duparc & Thomas A. Henzinger, editors: Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lecture Notes in Computer Science 4646, Springer, pp. 298–312, 10.1007/978-3-540-74915-8_24.
  * [12] D. de Carvalho (2018): _Execution time of $\lambda$-terms via denotational semantics and intersection types_.  Math. Struct. Comput. Sci. 28(7), pp. 1169–1203, 10.1017/S0960129516000396.
  * [13] M. Coppo, M. Dezani-Ciancaglini, F. Honsell & G. Longo (1984): _Extended type structures and filter lambda models_.  In G. Lolli, G. Longo & A. Marcja, editors: Logic Colloquium 82, North-Holland, Amsterdam, the Netherlands, pp. 241–262, 10.1016/S0049-237X(08)71819-6.
  * [14] U. Dal Lago, F. Gavazzo & P. B. Levy (2017): _Effectful Applicative Bisimilarity: Monads, Relators, and Howe’s Method_.  In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, IEEE Computer Society, pp. 1–12, 10.1109/LICS.2017.8005117.
  * [15] U. de’Liguoro & R. Treglia (2020): _The untyped computational _$\lambda$_ -calculus and its intersection type discipline_.  Theor. Comput. Sci. 846, pp. 141–159, 10.1016/j.tcs.2020.09.029.
  * [16] U. de’Liguoro & R. Treglia (2021): _Intersection Types for a Computational Lambda-Calculus with Global State, https://arxiv.org/abs/2104.01358_.  arXiv:https://arxiv.org/abs/2104.01358.
  * [17] M. Dezani-Ciancaglini, F. Honsell & F. Alessi (2003): _A complete characterization of complete intersection-type preorders_.  ACM Trans. Comput. Log. 4(1), pp. 120–147, 10.1145/601775.601780.
  * [18] F. Gavazzo (2019): _Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects_.  Ph.D. thesis, University of Bologna, Italy.  Available at http://amsdottorato.unibo.it/9075/.
  * [19] M. Hyland & J. Power (2006): _Discrete Lawvere theories and computational effects_.  Theor. Comput. Sci. 366(1-2), pp. 144–162, 10.1016/j.tcs.2006.07.007.
  * [20] M. Hyland & J. Power (2007): _The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads_.  Electron. Notes Theor. Comput. Sci. 172, pp. 437–458, 10.1016/j.entcs.2007.02.019.
  * [21] U. Dal Lago & F. Gavazzo (2019): _Effectful Normal Form Bisimulation_.  In Luís Caires, editor: Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Lecture Notes in Computer Science 11423, Springer, pp. 263–292, 10.1007/978-3-030-17184-1_10.
  * [22] P.-A. Melliès & N. Zeilberger (2015): _Functors are Type Refinement Systems_.  In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, ACM, pp. 3–16, 10.1145/2676726.2676970.
  * [23] E. Moggi (1991): _Notions of Computation and Monads_.  Inf. Comput. 93(1), pp. 55–92, 10.1016/0890-5401(91)90052-4.
  * [24] G. D. Plotkin & J. Power (2002): _Notions of Computation Determine Monads_.  In: FOSSACS 2002, Lecture Notes in Computer Science 2303, Springer, pp. 342–356, 10.1007/3-540-45931-6_24.
  * [25] G. D. Plotkin & J. Power (2003): _Algebraic Operations and Generic Effects_.  Appl. Categorical Struct. 11(1), pp. 69–94, 10.1023/A:1023064908962.
  * [26] J. Power (2006): _Generic models for computational effects_.  Theor. Comput. Sci. 364(2), pp. 254–269, 10.1016/j.tcs.2006.08.006.
  * [27] P. Wadler (1992): _The Essence of Functional Programming_.  In: Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1992, ACM Press, pp. 1–14, 10.1145/143165.143169.
  * [28] P. Wadler (1995): _Monads for Functional Programming_.  In: Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Lecture Notes in Computer Science 925, Springer, pp. 24–52, 10.1007/3-540-59451-5_2.