1

# A metalanguage for cost-aware denotational semantics

Yue Niu  0000-0003-4888-6042<EMAIL_ADDRESS>and  Robert Harper
<EMAIL_ADDRESS>0000-0002-9400-2941 Carnegie Mellon University5000 Forbes
Ave.PittsburghPA15213USA

###### Abstract.

We present two metalanguages for developing _synthetic cost-aware denotational
semantics_ of programming languages. Extending the recent work of Niu et al.
on calf, a dependent type theory for both cost and behavioral verification, we
define two metalanguages, $\textbf{calf}^{\star}$ and
$\textbf{calf}^{\omega}$, for studying cost-aware metatheory.
$\textbf{calf}^{\star}$ is an extension of calf with universes and inductive
types, and $\textbf{calf}^{\omega}$ is a an extension of
$\textbf{calf}^{\star}$ with unbounded iteration. We construct denotational
models of the simply-typed lambda calculus and Modernized Algol, a language
with first-order store and while loops, and show that they satisfy a _cost-
aware_ generalization of the classic Plotkin-type computational adequacy
theorem. Moreover, by developing our proofs in a synthetic language of _phase-
separated_ constructions of intension and extension, our results easily
_restrict_ to the corresponding extensional theorems. Consequently, our work
provides a positive answer to the conjecture raised in Niu et al. (2022) and
in light of _op. cit_.’s work on algorithm analysis, contributes a
metalanguage for doing both cost-aware programming and verification and cost-
aware metatheory of programming languages.

types, semantics, cost analysis

††journal: PACMPL††journalvolume: 1††journalnumber: CONF††article:
1††journalyear: 2018††publicationmonth: 1††copyright: none

##  1\. Introduction

Denotational semantics is a well-established method for obtaining an
_equational theory_ for program verification. Whereas the operational
semantics of a programming language gives meaning to programs via closed,
whole program computation, denotational semantics aims to assign a
_compositional_ theory to _open_ programs amenable to equational/algebraic
reasoning. A well-behaved denotational semantics respects the operational
meaning of programs in the sense that the denotation of a program is invariant
under evaluation. This property is known as _soundness_. Conversely, for a
denotational model to be useful, it must be conservative enough as an
equational theory so that “computations” in the denotational model can be
reflected in the operational semantics. This is known as _computational
adequacy_.111In the literature, the computational adequacy sometimes refer to
the conjunction of soundness and adequacy as we have defined here.
Denotational semantics satisfying these properties have been studied for a
long time, starting with Plotkin’s work on the investigation of LCF as a
programming language (PCF) (Plotkin, 1977).

Although the question of computational adequacy has been traditionally studied
in the context of denotational semantics, recent work on program cost analysis
in type theory has broached the possibility of viewing adequacy in the more
general context of equational theories. In particular, Niu et al. proposed a
dependent type theory calf (cost-aware logical framework) that provides a rich
specification language supporting both behavioral and cost verification of
functional programs. That work formalizes a myriad of case studies of the cost
analysis of algorithms in the framework and proves the consistency of calf via
a model construction. As a type theory, calf can be thought of as the semantic
domain of a denotational semantics in the sense that it furnishes an
equational theory for program analysis. Moreover, as a cost analysis
framework, calf does not stipulate a cost semantics for programs; instead, the
users of the framework is responsible for specifying the cost model of the
algorithms they define. This raises a natural question: how does one know if a
cost model is reasonable relative to a given programming language? In the
concluding remarks, the authors expressed the idea that the choice of a cost
model with respect to an operational semantics may be justified by an
_internal_ computational adequacy theorem in the style of Plotkin.

In this paper, we substantiate this idea and develop extensions of calf that
promote it to a metalanguage for _synthetic cost-aware denotational
semantics_. To illustrate our approach, we first define
$\textbf{calf}{}^{\star}$, an extension of calf with universes and inductive
types, which we use to define a computationally adequate denotational
semantics for the simply-typed lambda calculus (STLC). To ramp up to a richer
programming language, we define $\textbf{calf}{}^{\omega}$, an extension of
$\textbf{calf}{}^{\star}$ with _unbounded iteration_ , in which we define a
computationally adequate semantics for Modernized Algol (MA), a dialect of
Algol (Harper, 2012).

##### Cost-aware computational adequacy

In both of the case studies we prove a generalization of the classic,
_extensional_ Plotkin adequacy that we refer to as _cost-aware computational
adequacy_. Roughly, whereas the classic adequacy theorem speaks about the
extensional content in both the operational and denotational semantics, cost-
aware adequacy relates the operational cost with the denotational cost in
addition to the extensional behavior of programs. An important contribution of
our work is the fact that ordinary adequacy follows immediately from the cost-
aware adequacy theorem, which is an instance of a more general principle of
calf as a _synthetic language_ for mediating the interaction of the cost
(intension) and behavior (extension) of programs, a point that we shall expand
on in Sections 1.1.3 and 1.1.4.

##### Synthetic denotational semantics

The denotational models we define are also synthetic in a more traditional
sense: type structure of the object language is implemented as simple
compositions of the corresponding type structures in the metalanguage that do
not involve complex analytic constructions typical of classic domain theory.
This analytic-synthetic dichotomy is perhaps most well-studied in the context
of classical (Euclidean) geometry. Euclid’s _Elements_ makes use of the
prototypical example of a _synthetic_ theory: the mathematical objects
involved in the study of geometry such as points and lines are postulated to
exist and satisfy certain axioms with no further ado, and the subject is
developed with reference to only these assumptions. On the other hand,
analytic geometry in the sense of Descartes _constructs_ geometrical objects
from a more primitive notion of space (_i.e_. cartesian coordinates), from
which the axioms of Euclid may be verified to hold.

The benefit of synthetic theories are both theoretical and practical. The
axioms of a synthetic theory are useful _abstractions_ that reveal the
fundemantal structures and seal away irrelevant details of the mathematical
objects at hand. This has a tangible impact on users of the theory; although a
programming languages researcher may not care about how a fixed-point operator
is implemented, they will certainly need to use the universal property of the
fixed-point to prove theorems about programs. In the context using calf as a
metalanguage for cost-aware denotational semantics, the synthetic nature of
the theory is reflected in both the interpretation of the type structures and
the treatment of the interaction of intension/extension.

###  1.1. calf: a cost-aware logical framework

In this section, we recall the key components of calf as a type theory and
framework for cost analysis; we defer to Niu et al. (2022) for more details.
We present a fragment of the signature of calf in Fig. 1.

$\displaystyle\mathsf{step}$
$\displaystyle:\,\mathrel{\\{X:\mathsf{tp}^{\ominus}\\}}\mathbb{C}\to\mathsf{tm}^{\ominus}(X)\to\mathsf{tm}^{\ominus}(X)$
$\displaystyle\mathsf{step}_{0}$
$\displaystyle:\,\mathrel{\\{X,e\\}}\mathsf{step}^{0}(e)=e$
$\displaystyle\mathsf{step}_{+}$
$\displaystyle:\,\mathrel{\\{X,e,c_{1},c_{2}\\}}$
$\displaystyle\mathsf{step}^{c_{1}}(\mathsf{step}^{c_{2}}(e))=\mathsf{step}^{c_{1}+c_{2}}(e)$
$\displaystyle\mathsf{tp}^{+}$ $\displaystyle:\bf{Jdg}$
$\displaystyle\mathsf{tm}^{+}$ $\displaystyle:\mathsf{tp}^{+}\to\bf{Jdg}$
$\displaystyle\mathsf{U}$
$\displaystyle:\mathsf{tp}^{\ominus}\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{F}$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{\ominus}$
$\displaystyle\mathsf{tm}^{\ominus}(X)$
$\displaystyle\coloneqq\mathsf{tm}^{+}(\mathsf{U}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
X$}\mathclose{}{)}})$ $\displaystyle\mathsf{ret}$
$\displaystyle:(A:\mathsf{tp}^{+},a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})$ $\displaystyle\mathsf{bind}$
$\displaystyle:\,\mathrel{\\{A:\mathsf{tp}^{+},X:\mathsf{tp}^{\ominus}\\}}\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})\to$
$\displaystyle(\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(X))\to\mathsf{tm}^{\ominus}(X)$
$\displaystyle\P_{\mathsf{E}}$ $\displaystyle:\bf{Jdg}$
$\displaystyle\P_{\mathsf{E}}/{\mathsf{uni}}$
$\displaystyle:\,\mathrel{\\{u,v:\P_{\mathsf{E}}\\}}u=v$
$\displaystyle\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}\mathcal{J}$
$\displaystyle\coloneqq\P_{\mathsf{E}}\to\mathcal{J}$
$\displaystyle\mathsf{step}/{\P_{\mathsf{E}}}$
$\displaystyle:\,\mathrel{\\{X,e,c\\}}\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}(\mathsf{step}^{c}(e)=e)$
$\displaystyle\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}^{+}$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{+}$ $\displaystyle\\_$
$\displaystyle:\,\mathrel{\\{A\\}}\mathsf{tm}^{+}(\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}^{+}{A})\cong\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}(\mathsf{tm}^{+}(A))$
$\displaystyle\Pi$
$\displaystyle:(A:\mathsf{tp}^{+},X:\mathsf{tm}^{+}(A)\to\mathsf{tp}^{\ominus})\to\mathsf{tp}^{\ominus}$
$\displaystyle(\mathsf{ap},\mathsf{lam})$
$\displaystyle:\,\mathrel{\\{A,X\\}}\mathsf{tm}^{\ominus}(\Pi(A;X))\cong(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(a))$
$\displaystyle\mathsf{lam}_{\mathsf{step}}$
$\displaystyle:\,\mathrel{\\{A,X,f,c\\}}\mathsf{lam}(\mathsf{step}^{c}(f))=\mathsf{step}^{c}(\mathsf{lam}(f))$
$\displaystyle\mathsf{bind}_{\mathsf{step}}$
$\displaystyle:\,\mathrel{\\{A,X,e,f,c\\}}\mathsf{bind}(\mathsf{step}^{c}(e);f)=\mathsf{step}^{c}(\mathsf{bind}(e;f))$
Figure 1. A fragment of the signature of calf.

####  1.1.1. Dependent call-by-push-value

calf is defined as an extension of the dependent call-by-push-value calculus
of Pédrot and Tabareau (2019). Recall that the theory of call-by-push-value
(CBPV) can be extracted from the Eilenberg-Moore category arising from a monad
that encodes the computational effect. More concretely, there are two classes
of types in CBPV: the _value_ /_positive_ types classifying values, and the
_computation_ /_negative_ types classifying computations. Semantically, value
types correspond to plain sets while computation types correspond to
_algebras_ for the given monad. The type constructors $\mathsf{U},\mathsf{F}$
bridge this stratification of values and computations and corresponds to a
free-forgetful adjunction in the semantics. A computation of the type
$\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}$ is called a _free computation_ , and $\mathsf{ret}$ and
$\mathsf{bind}$ are the introduction and elimination forms of the free
computations.

####  1.1.2. Cost as a computational effect

As a theory, calf is paramterized by an (ordered) monoid
$(\mathbb{C},+,\leq,0)$. The cost structure of programs is generated from a
single computational effect
$\mathsf{step}:\,\mathrel{\\{X\\}}\mathbb{C}\to\mathsf{tm}^{\ominus}(X)\to\mathsf{tm}^{\ominus}(X)$,
which one may think operationally as incurring the given cost onto a
computation.

As a dependent CBPV calculus, calf supports a simple equational theory for
reasoning about the cost of computations. For instance, Niu et al. (2022)
defines an internal predicate $\mathsf{hasCost}_{A}(e,c)\coloneqq\Sigma
a\mathbin{:}A.\;e=\mathsf{step}^{c}(\mathsf{ret}(a))$ that defines when a
computation has a given cost.

####  1.1.3. The interaction intension and extension

A key innovation of calf as a cost analysis framework is a solution to the
problem of _exotic programs_. Traditional accounts of cost structure in type
theory employs the cost monad/writer monad $\mathbb{C}\times-$, so that a
cost-aware/effectful program of type $A$ is rendered as a term of type
$\mathbb{C}\times A$. One thinks of an effectful program in this setting as a
program instrumented with a counter that returns the incurred cost. However,
this encoding is transparent enough so that the counter is allowed to
interfere with the _behavior_ of the program; such programs are called
_exotic_ by Niu et al. (2022) because one cannot extract from it an ordinary,
cost-unaware program.

Because the free computations and the cost effect $\mathsf{step}$ are
_abstract_ , there is no way to define such exotic programs, which is an
internal theorem one may specify and prove in calf. Semantically, the free
computations may be implemented using the writer monad on an appropriate cost
monoid, but it is important that this fact is not exposed in the theory. In
order to work with cost effects in the abstract, calf introduced a pair of
_modalities_ for the interaction of intension and extension.

####  1.1.4. Modalities for intension and extension

The first problem one encounters working in a cost-sensitive/intensional
setting where the cost effect is abstract is function extensionality. For
example, consider the merge sort and insertion sort algorithms. Under the
usual cost model, these algorithms are most definitely distinct as far as cost
is concerned. However, because they are both sorting algorithms, they are
equal in extension/behavior, and by functional extensionality, they are equal!
In calf this contradiction may be resolved by the following observation:
equality of extension/behavior may be analyzed in a special phase called the
_extensional phase_ in which the cost effect is trivial. Technically, the
extensional phase is generated by a distinguished proposition
$\P_{\mathsf{E}}$ along with the axiom $\mathsf{step}/\P_{\mathsf{E}}$ (see
Fig. 1); whenever we are in a context in which $\P_{\mathsf{E}}$ is derivable,
$\mathsf{step}/\P_{\mathsf{E}}$ stipulates that $\mathsf{step}$ is trivial,
and therefore we require ordinary extensional reasoning. Of course there are
no closed terms of $\P_{\mathsf{E}}$, but no other structures are assumed
aside from the fact it is a proposition.

The extensional phase generates a pair of modalities for intension and
extension. The extensional modality is defined as
$\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}(A)\coloneqq\P_{\mathsf{E}}\to
A$, which simply internalizes the derivability of $\P_{\mathsf{E}}$. Given a
type $A$, one can think of
$\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}A$
as the extensional part of $A$; in terms of the cost monad the unit of the
extensional modality is the projection map $\mathbb{C}\times A\to A$.
Complementary to the extensional modality is the intensional modality, which
is defined as a pushout of the projections of $A\times\P_{\mathsf{E}}$. It is
a bit more difficult to visualize the meaning of the intensional modality, but
one can imagine
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}A$
as identical to $A$ except that it is trivial inside the extensional phase,
_i.e_.
$\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}A\cong
1$. A useful way to internalize this fact is the phrase “the extension part of
the intensional part is trivial”.

In calf one can use these modalities to manage the interaction of the
intension and extension. For instance, although it is not the case that merge
sort and insertion sort are equal in the _empty_ context, one can derive their
equality in the extensional phase, _i.e_. one has
$\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}(\mathsf{mergeSort}=\mathsf{insSort})$.
On the other hand, one may use the intensional modality to _seal away_ cost
structures, which is useful in applications such as program optimization and
noninterference.

##### The phase distinction of intension and extension

The interaction of the intension and extension in calf is an instance of a
more general phenomenon of _phase distinctions_ in the sense of the theory of
ML modules; as explained in Sterling and Harper (2021); Niu et al. (2022), the
(non)interaction of intensional structure with the extensional behavior of a
cost-aware function is formally identical to the (non)interaction of dynamic
components with static components in a module functor. Consequently, one can
think of calf as a synthetic language for _phase distinct programming_ of
intension and extension, and a calf program is said to be phase-separated if
it exploits the interaction of the intensional and extensional modalities.

###  1.2. Cost-aware computational adequacy

Niu et al. deployed these ideas on several case studies, including Euclid’s
algorithm for the greatest common divisor, amortized analysis batched queues,
and sequential and parallel sorting algorithms. An important feature of these
analyses is that they all employed their own cost models, which follows the
prevailing convention of algorithms research community. Although all the cost
models of _op. cit_. are intuitively reasonable, the authors did not provide a
formal theory for _why_ certain cost models _are_ reasonable; however, it was
conjectured that this may be achieved via a cost-aware version of Plotkin’s
adequacy theorem.

We provide a positive answer to this conjecture. For the following, suppose
that we have defined inside calf a programming language P along with an
evaluation relation
$\Downarrow:\textbf{P}\to\mathbb{N}\to\textbf{P}\to\mathsf{tp}^{+}$. A
denotational semantics $\llbracket-\rrbracket$ of P satisfies cost-aware
computational adequacy when the following holds:

> For all closed programs of base type
> $\vdash_{\textbf{P}}e:{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$,
> if $\llbracket e\rrbracket=\mathsf{step}^{c}(\mathsf{ret}(b))$ for some
> $b:\mathsf{bool}$ and $c:\mathbb{N}$, then
> $e\Downarrow_{\P_{\mathsf{E}}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c}\overline{b}$.

In the above,
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$
is the boolean type in P, and $\overline{a}$ sends a calf boolean to its
numeral in
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$.
We write
$\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}:A\to\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}A$
for the unit of the intensional modality, and the relation
$\Downarrow_{\P_{\mathsf{E}}}$ is a _phase-separated_ version of the
evaluation relation whose meaning we will explain shortly. Roughly, cost-aware
computational adequacy states that if the denotation of a boolean program is
equal to a value incurring some cost, then operationally the program must also
evaluate to the same value with the same cost.

##### Phase-separated evaluation

In order to explain phase-separated evaluation, let us consider a statement of
cost-aware adequacy using the usual operational cost semantics $\Downarrow$
and observe what goes wrong. Suppose we have a proof of the extensional phase
$u:\P_{\mathsf{E}}$, and consider a closed program
$e:{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$
such that $e=\mathsf{step}^{c}(\mathsf{ret}(\Set{\mathsf{tt},\mathsf{ff}}))$.
We have to show that
$e\Downarrow^{c}\Set{{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}},{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}}$.
But because we are in the extensional phase, we also have
$\mathsf{step}^{c}(\mathsf{ret}(\Set{\mathsf{tt},\mathsf{ff}}))=\mathsf{step}^{0}(\mathsf{ret}(\Set{\mathsf{tt},\mathsf{ff}}))$.
Therefore, we also have to show that
$e\Downarrow^{0}\Set{{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}},{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}}$!
Now, if $c\neq 0$, we have a contradiction if adequacy holds, because the
evaluation relation is deterministic: if $e\Downarrow^{c}v$ holds, then it
holds for unique $c$ and $v$.

So we would like the relation $\Downarrow$ to _restrict_ to a cost-unaware
evaluation relation in the extensional phase. This is the purpose of the
phase-separated evaluation relation: we define a relation
$\Downarrow_{\P_{\mathsf{E}}}:\textbf{P}\to\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}\mathbb{N}\to\textbf{P}\to\mathsf{tp}^{+}$
whose cost component is _sealed_ by the intensional modality. We can define
such a relation $\Downarrow_{\P_{\mathsf{E}}}$ and prove that it becomes
equivalent to the cost-unaware evaluation relation $e\Downarrow v$ in the
extensional phase. Consequently, the problem above is resolved because the
contradictory evaluation costs are sealed away by the intensional modality and
invisible in the extensional phase.

####  1.2.1. Synthetic cost-aware denotational semantics

The contribution of our work is the development of the proceeding idea with
two concrete programming languages: the simply-typed lambda calculus (STLC)
and Modernized Algol (MA). First, we axiomatize an extension of calf with
universes and inductive types dubbed $\textbf{calf}{}^{\star}$. We define the
syntax and operational semantics of STLC in $\textbf{calf}{}^{\star}$,
construct a cost-aware denotational semantics of STLC, and prove the model to
be computationally adequate in the sense describe above. Next, we axiomatize
an extension of $\textbf{calf}{}^{\star}$ with unbounded iteration dubbed
$\textbf{calf}{}^{\omega}$ and carry out a similar construction for MA, a
language with first-order stores and while loops.

In both case studies we will rely on the respective metalanguages to define
conceptually simple and _synthetic_ models of the object programming
languages. Here we emphasize that our models are synthetic in two orthogonal
senses. First, as we discussed in Section 1.1.4, calf is a theory for phase-
separated constructions. In more geometric language, one can think of calf
types as families of cost/intensional structures indexed by
behavioral/extensional specifications. The benefit of working in a language
for such indexed constructions is that one may always _project_ the index of
the family to obtain the ordinary, extensional content of an object. This is
exemplified in our account of cost-aware computational adequacy: the classic
extensional Plotkin-type adequacy theorem follows immediately as a corollary
of cost-aware computational adequacy, a property that is _not_ enjoyed by
prior work on sythetic denotational semantics, which we discuss more in
Section 1.4.

Our work is also synthetic in a more traditional sense: types and computations
of the object language is defined via simple constructions using the
corresponding structures in the metalanguage. For instance, while loops of MA
may be interpreted straightforwardly as an _iteration_ primitive of
$\textbf{calf}{}^{\omega}$ satisfying the expected unfolding law and
compactness property. By isolating the essential properties necessary to
develop the computational adequacy proof, we refine and provide a way to
interpret classic accounts of adequacy in multiple metatheories.

###  1.3. Models of $\textbf{calf}{}^{\star}$ and $\textbf{calf}{}^{\omega}$

To show that a synthetic theory is sensible, one must exhibit an
interpretation or model of the theory in terms of previously understood
concepts. Following the work of Niu et al. (2022), we prove the consistency of
$\textbf{calf}{}^{\star}$ and $\textbf{calf}{}^{\omega}$ by means of a model
construction. Similar to authors of _op. cit_., we define
$\textbf{calf}{}^{\star}$ and $\textbf{calf}{}^{\omega}$ as signatures of the
_logical framework_ of locally cartesian closed categories (lccc’s). One can
think of the language of this logical framework as an extensional dependent
type theory with a universe of judgments closed under dependent products,
dependent sums, and extensional equality. A model of a theory (_e.g_. calf)
associated to a signature is given by an implementation of the constants in
the signature in any other lccc.

The authors of _op. cit_. defines a model of calf called the _counting model_
in an arbitrary presheaf topos equipped with a proposition representing the
semantic extensional phase. The counting model is itself an extension of the
Eilgenberg-Moore model of CBPV associated to the cost monad. We first extend
the counting model of calf with an interpretation of inductive types and
universes based on the _weaning models_ of dependent CBPV (Pédrot and
Tabareau, 2019) to obtain a model of $\textbf{calf}{}^{\star}$. We then modify
this model to account for partiality, resulting in a model for
$\textbf{calf}{}^{\omega}$.

###  1.4. Related work

####  1.4.1. Cost-aware denotational semantics

Notions of cost-sensitive version of classic extensional denotational
semantics has been studied in the context of formalization of recurrence
extraction (Danner et al., 2015; Kavvos et al., 2019). The idea of this series
of works is to develop a formal framework for the well-known and used method
of recurrence relations and extend it to work with higher-order functional
programs. Here we give a brief summary of the approach of Kavvos et al.
(2019), which is divided into several stages across two different languages:
the programming language (CBPV) and the syntactic recurrence language. A
_syntactic recurrence_ is extracted from a given program, which is then turn
into a semantic recurrence suitable for mathematical manipulation in using a
denotational semantics based on _sized domains_. _op. cit_. prove a bounding
theorem about the extraction procedure, which roughly states that the
extracted recurrence program produces an upperbound on the evaluation of the
source program; _op. cit_. then prove a traditional adequacy theorem for the
denotational semantics with respect to the syntactic recurrence language,
which in conjunction with the bounding theorem produces a sound mathematical
domain for doing algorithm analysis à la recurrence relations.

The work of Kavvos et al. (2019) is different from ours in several aspects.
First, _op. cit_. define a denotational semantics for a variant of PCF, while
we define the denotational semantics of MA, an imperative language with first-
order store and while loops (and consequently no mechanism for defining
arbitrary fixed-points). Second, the adequacy theorem of _op. cit_. only
speaks about cost indirectly through the recurrence extraction, whereas we
prove a direct cost-aware adequacy theorem that allows one to directly reason
about cost of the source program. Lastly, the most important difference stems
from the fact that we work in a formalized metatheory (calf) that allows for
synthetic constructions as discussed in Sections 1.1.4 and 1.2.1. Whereas
Kavvos et al. (2019) work in a classical set-theoretic metatheory and use
classic domain-theoretic constructions, we promote a more abstract approach
based on an axiomatization of the necessary domain structures and the
interaction of intension and extension. Moreover, because calf (and its
extensions) is a dependent type theory, one may also use it as programming
language, which Niu et al. (2022) has shown to be a fruitful endeavor in the
context of both the cost analysis and behavioral verification of programs.

####  1.4.2. Denotational semantics of Algol

Denotational semantics of procedural languages with first-order store traces
back to at least the early seminal works of Scott (1970); Scott and Strachey
(1971). Algol and Algol-like languages in particular were widely-studied in
terms of both denotational and operational semantics, and we do not recall the
specifics of the language here; for more details we defer to the definitive
sources on the subject (O’Hearn and Tennent, 1997a, b; Reynolds, 1981). We
present a denotational model for Modernized Algol (MA), a version Algol
presented in Harper (2012). MA is an imperative programming language with
first-order store and unbounded iteration, a call-by-value operational
semantics, and a categorical separation of expressions and commands. The
denotational semantics we define for MA is based on the a Kripke-world
interpretation of store and in some sense not substantially different from the
standard models of Algol-like languages.

The main improvement of our work is the cost-aware aspect of the denotational
semantics and an axiomatization of the properties in
$\textbf{calf}{}^{\omega}$ that are necessary to prove computational adequacy.
Moreover, as mentioned in Section 1.2, our results easily restricts to the
classic adequacy theorem for denotational models of MA extensionally.

####  1.4.3. Synthetic domain theory

Ever since the pioneering work of Scott on the domain-theoretic semantics for
programming languages, there has been much interest (Hyland, 1991; Fiore and
Rosolini, 1997; Fiore and Plotkin, 1996; Reus and Streicher, 1999) in finding
set-theoretic universes (in other words, topoi) that embed concrete categories
of domains, which would furnish a rich intuitionistic/type-theoretic framework
for defining reasoning about domain-theoretic constructions.

Synthetic domain theory (SDT) is an elegant and powerful approach for modeling
programming languages, but does not immediately provide a synthetic language
for talking about cost-aware computation. From our perspective, a good way to
situate our work with respect to SDT is to view categories (topoi to be
precise) with an SDT theory as _models_ for the kind of metalanguages we
promote in this paper. In fact, we hope that by constructing models of calf in
categories with SDT structure, we can extend our results to Plotkin’s PCF,
thereby truly generalizing Plotkin’s original adequacy result to a cost-
sensitive setting; we shall come back to this point in Section 9.

####  1.4.4. Denotational semantics in guarded type theory

More recently, Møgelberg and Paviotti (2016); Paviotti et al. (2015) promoted
the use of _guarded dependent type theory_ (gDTT) for doing synthetic
denotational semantics. Similar to our approach of using a type-theoretic
metalanguage, Møgelberg and Paviotti (2016) defines a denotational semantics
for FPC in gDTT and prove it to be computationally adequate in the traditional
sense. Interestingly, _op. cit_. defines an intensional denotational model of
FPC: because recursive types of FPC are defined using guarded recursive types
in gDTT, the interpretation of terms of recursive types naturally contains
“steps” engenered by the use of guarded recursion. As a result, _op. cit_.
works with a slightly nonstandard operational cost semantics that is defined
to compute in “lock-step” with the unfolding of guarded recursive types in the
denotational semantics. _op. cit_. proves an intensional adequacy theorem that
relates the steps taken by the operational semantics and the denotational
semantics.

There is a subtle difference between _op. cit_. and our notion of intensional
adequacy. Because the operational semantics of _op. cit_. _only_ tracks the
unfolding of recursive types, it does not correspond to the natural cost
semantics one obtains from the reflexive-transitive closure of the one step
transition relation. We do not perceive this to be a fundamental limitation of
guarded type theory, since one may insert artificial delays in both the
operational and denotational semantics to obtain an adequacy theorem about an
ordinary cost semantics. However, because guarded type theory does not have
the general facilities of calf for reasoning about cost-aware programs (see
Section 1.1), it is not clear if this kind of result would be useful in that
setting.

A more significant difference also stems from the fact that gDTT is not
equipped with a synthetic language for phase-separated constructions. To
obtain the ordinary extensional adequacy theorem, Møgelberg and Paviotti
(2016) employ an additional logical relation over the interpretation of FPC
types, a construction that involves defining a guarded version of the
coninductive delay monad and an analogue of the weak bisimilarity relation. In
contrast, the extensional adequacy theorem in our setting follows
_immediately_ from the cost-aware adequacy theorem, a consequence of working
in a framework suitable for cost-aware metatheory. Note that the work did not
disappear — by isolating the theory of the interaction of intension and
extension and verifying the resulting axioms via a model construction once and
for all, we package up the work into a mechanism that may be applied more
generally than the concrete analytic construction used by _op. cit_.

####  1.4.5. Compiler correctness

Lastly, we outline some connections of our work to the area of compiler
correctness Patterson and Ahmed (2019); Perconti and Ahmed (2014); Ahmed
(2015); Mates et al. (2019); Benton and Hur (2010). In the early days of the
mathematization of the study of programming languages, the primary purpose of
denotational semantics is to explain the meaning of programs in terms of
previously established and undertood mathematical structures. However, as the
field and synthetic methods developed, denotational semantics took on more of
a logical character: models look more like _translations_ between different
_languages_ , a view point that is expressed in Jung et al. (1996).
Consequently, one may view denotational semantics as a sort of “compiler” from
the object language into the semantic domain and computational adequacy as a
sort of compiler correctness argument. Traditionally, compiler verification is
concerned with the _functional_ or _extensional_ correctness of the
compilation process. We are naturally led to ask whether working in a rich,
_cost-aware_ metalanguage for denotational semantics could prove useful in
studying the _intensional_ aspects of compilation. We have broached the idea
in this paper by way of proving a cost-aware adequacy theorem, and there are
ample opportunities to apply the ideas we developed to both new and old
problems in compiler verification.

##  2\. $\textbf{calf}{}^{\star}$: extending calf with universes and inductive
types

In this section, we present an extension of calf with universes and general
inductive types.

$\displaystyle\mathsf{Univ}^{+}$ $\displaystyle:\mathsf{tp}^{+}$
$\displaystyle\mathsf{El}^{+}$
$\displaystyle:\mathsf{tm}^{+}(\mathsf{Univ}^{+})\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{Univ}^{\ominus}$ $\displaystyle:\mathsf{tp}^{\ominus}$
$\displaystyle\mathsf{El}^{\ominus}$
$\displaystyle:\mathsf{tm}^{+}(\mathsf{Univ}^{\ominus})\to\mathsf{tp}^{\ominus}$
$\displaystyle W$
$\displaystyle:(A:\mathsf{tp}^{+},B:\mathsf{tm}^{+}(A)\to\mathsf{tp}^{+})\to\mathsf{tp}^{+}$
$\displaystyle W/\mathsf{intro}$
$\displaystyle:\,\mathrel{\\{A,B\\}}(a:\mathsf{tm}^{+}(A))\to(\mathsf{tm}^{+}(B(a))\to\mathsf{tm}^{+}(W(A,B)))\to\mathsf{tm}^{+}(W(A,B))$
$\displaystyle W/\mathsf{rec}$
$\displaystyle:\,\mathrel{\\{A,B,(C:\mathsf{tm}^{+}(W(A,B))\to\mathsf{tp}^{+})\\}}$
$\displaystyle((a:\mathsf{tm}^{+}(A))\to(f:\mathsf{tm}^{+}(B(a))\to\mathsf{tm}^{+}(W(A,B)))\to$
$\displaystyle\quad((b:\mathsf{tm}^{+}(B(a)))\to\mathsf{tm}^{+}(C(fb)))\to\mathsf{tm}^{+}(C(W/\mathsf{intro}(a,f))))\to$
$\displaystyle(w:\mathsf{tm}^{+}(W(A,B)))\to\mathsf{tm}^{+}(C(w))$
$\displaystyle W/\mathsf{comp}$
$\displaystyle:\,\mathrel{\\{A,B,C,h,a,f\\}}W/\mathsf{rec}(W/\mathsf{intro}(a,f),h)=h(a,f,(\lambda
b.\;W/\mathsf{rec}(h,f(b))))$

###  2.1. Universes

Following Pédrot and Tabareau (2019), we axiomatize a _pair_ of universes
$\mathsf{Univ}^{+},\mathsf{Univ}^{\ominus}$ classifying value types and
computation types respectively. We do not explicitly write down the type codes
and their decodings (which are completely standard); as an example, the
following signature axiomatizes closure under dependent products:

$\displaystyle\widehat{\Pi}$
$\displaystyle:(A:\mathsf{Univ}^{+})\to(\mathsf{El}^{+}(A)\to\mathsf{Univ}^{\ominus})\to\mathsf{Univ}^{\ominus}$
$\displaystyle\widehat{\Pi}/\mathsf{decode}$
$\displaystyle:\,\mathrel{\\{A,X\\}}\mathsf{El}^{\ominus}(\widehat{\Pi}(A,X))=\Pi(\mathsf{El}^{+}(A),\lambda
a.\;\mathsf{El}^{\ominus}(X(a)))$

##### Convention

In this paper we define type families (_i.e_. functions whose codomain is
$\mathsf{tp}^{+}$) in a style akin to large elimination that can be unfolded
to defining a family of type _codes_ (_i.e_. functions whose codomain is
$\mathsf{Univ}^{+}$) and decoding using $\mathsf{El}^{+}$.

###  2.2. Inductive types

Because calf is an extensional type theory, general inductive types may be
encoded by $W$-types. However, in practice we will use a more natural
presentation like the following:

(1) Inductive $\displaystyle\;\mathbb{N}:\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle\mathsf{zero}$ $\displaystyle:\mathbb{N}$
$\displaystyle\mathsf{suc}$ $\displaystyle:\mathbb{N}\to\mathbb{N}$

The definition above may be elaborated into the following $W$-type:

$\displaystyle\mathbb{N}$
$\displaystyle=\mathsf{El}^{+}(\widehat{\mathbb{N}})$
$\displaystyle\widehat{\mathbb{N}}$ $\displaystyle:\mathsf{Univ}^{+}$
$\displaystyle\widehat{\mathbb{N}}$
$\displaystyle=\widehat{W}(\widehat{2},\widehat{B})$
$\displaystyle\widehat{B}$
$\displaystyle:\mathsf{tm}^{+}(2)\to\mathsf{Univ}^{+}$ $\displaystyle B(b)$
$\displaystyle=\mathsf{if}(b,\widehat{0},\widehat{1})$

In general a declaration like Eq. 1 should be thought of defining the _code_
of an inductive type. Moreover, because inductive _families_ can be defined
using _indexed containers_ (Altenkirch et al., 2015), which in turn can be
defined using $W$-types, we will also use a similar notation for defining
inductive families; the precise schema of inductive families and elaboration
procedure is beyond the scope of our work, and we defer to the relevant
literature for details.

###  2.3. Uniqueness of cost bounds

The theory of cost effects introduced in Niu et al. (2022) is sufficient to
define and _compose_ cost bounds of programs (see Section 1.1.2). However, in
order to prove adequacy, we have to be able to go the other way: it needs to
be the case that a given cost bound may be shown to be _unique_. We axiomatize
uniqueness as follows:

$\displaystyle\mathsf{step}/\mathsf{inj}$
$\displaystyle:\,\mathrel{\\{A,(a,a^{\prime}:A)(c,c^{\prime}:\mathbb{C})\\}}\mathsf{step}^{c}(\mathsf{ret}(a))=\mathsf{step}^{c^{\prime}}(\mathsf{ret}(a^{\prime}))\to
a=a^{\prime}\times\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=c^{\prime})$

Note that because the premise of $\mathsf{step}/\mathsf{inj}$ could have been
derived using a proof of the extensional phase, we must seal the equation
$c=c^{\prime}$ by the intensional modality. We will show that
$\mathsf{step}/\mathsf{inj}$ holds in an extension of the counting model of
calf in Section 7.

##  3\. Warm-up: STLC

In this section, we define and study a cost-aware denotational semantics for
the STLC. In the following, we suppress some notation from meta-level terms,
_i.e_. we write $e:A$ for $e:\mathsf{tm}^{+}(A)$.

###  3.1. Representing object languages in $\textbf{calf}{}^{\star}$

The exact mechanism by which object-level syntax is defined is immaterial for
our purposes; we may choose from a variety of first-order encodings definable
using inductive types/families. As an example, we will present an
intrinsically-typed nameless representation for STLC based on Benton et al.
(2012).

##### Notation

In this paper we write _e.g_.
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$
for object-level syntactic phrases.

###  3.2. Syntax of the STLC

We consider a version of STLC with a base type of observations
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$
with two points
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}},{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}:{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$:

Inductive $\displaystyle\mathsf{Ty}:\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$
$\displaystyle:\mathsf{Ty}$ $\displaystyle\Rightarrow$
$\displaystyle:\mathsf{Ty}\to\mathsf{Ty}$

Because we work with an intrinsic encoding, the type of terms is indexed by an
object-level context $\mathsf{Con}\coloneqq\mathsf{list}(\mathsf{Ty})$ and
type:

Inductive
$\displaystyle\mathsf{Tm}:\mathsf{Con}\to\mathsf{Ty}\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{var}}}$
$\displaystyle:\,\mathrel{\\{\Gamma,A\\}}\mathsf{Var}(\Gamma,A)\to\mathsf{Tm}(\Gamma,A)$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{lam}}}$
$\displaystyle:\,\mathrel{\\{\Gamma,A_{1},A_{2}\\}}\mathsf{Tm}(A_{1}::\Gamma,A_{2})\to\mathsf{Tm}(\Gamma,A_{1}\Rightarrow
A_{2})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}$
$\displaystyle:\,\mathrel{\\{\Gamma,A_{1},A_{2}\\}}\mathsf{Tm}(\Gamma,A_{1}\Rightarrow
A_{2})\to\mathsf{Tm}(\Gamma,A_{1})\to\mathsf{Tm}(\Gamma,A_{2})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}}$
$\displaystyle:\,\mathrel{\\{\Gamma\\}}\mathsf{Tm}(\Gamma,{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}$
$\displaystyle:\,\mathrel{\\{\Gamma\\}}\mathsf{Tm}(\Gamma,{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}})$

In the above, elements of the family $\mathsf{Var}$ represents proofs for
variable indexing:

Inductive
$\displaystyle\mathsf{Var}:\mathsf{Con}\to\mathsf{Ty}\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{here}}}$
$\displaystyle:\,\mathrel{\\{\Gamma,A\\}}\mathsf{Var}(A::\Gamma,A)$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{next}}}$
$\displaystyle:\,\mathrel{\\{\Gamma,A,A_{1}\\}}\mathsf{Var}(\Gamma,A_{1})\to\mathsf{Var}(A::\Gamma,A_{1})$

###### Definition 3.1 (Substitution).

A substitution from $\Gamma$ to $\Gamma^{\prime}$ is defined as
$\mathsf{Sub}(\Gamma,\Gamma^{\prime})\coloneqq(A:\mathsf{Ty})\to\mathsf{Var}(\Gamma,A)\to\mathsf{Tm}(\Gamma^{\prime},A)$.

##### Notation

Given a substitution $\sigma:\mathsf{Sub}(\Gamma,\Gamma^{\prime})$ and term
$e:\mathsf{Tm}(\Gamma,A)$, we write $e[\sigma]:\mathsf{Tm}(\Gamma^{\prime},A)$
for the result of the substitution. Given $e:\mathsf{Tm}(A_{1}::\Gamma,A_{2})$
and $e^{\prime}:\mathsf{Tm}(\Gamma,A_{1})$ we also write
$e[e^{\prime}]:\mathsf{Tm}(\Gamma,A_{2})$ for the result of substituting the
first free variable of $e$ for $e^{\prime}$.

####  3.2.1. Operations on substitutions

One can extend a substitution $\sigma:\mathsf{Sub}(\Gamma,\Gamma^{\prime})$ by
a term $e:\mathsf{Tm}(\Gamma^{\prime},A)$:

$\displaystyle\mathsf{cons}$
$\displaystyle:\,\mathrel{\\{\Gamma,\Gamma^{\prime},A\\}}\mathsf{Tm}(\Gamma^{\prime},A)\to\mathsf{Sub}(\Gamma,\Gamma^{\prime})\to\mathsf{Sub}(A::\Gamma,\Gamma^{\prime})$
$\displaystyle\mathsf{cons}(e,\sigma,A^{\prime},\mathsf{now})$
$\displaystyle=e$
$\displaystyle\mathsf{cons}(e,\sigma,A^{\prime},\mathsf{next}(v))$
$\displaystyle=\sigma(v)$

One can also shift substitution $\sigma:\mathsf{Sub}(\Gamma,\Gamma^{\prime})$
to account for context extensions, written as
$\uparrow^{A}\sigma:\mathsf{Sub}(A::\Gamma,A::\Gamma^{\prime})$. We will use
the following property about substitution:

###### Proposition 3.2.

Given $e:\mathsf{Tm}(A::\Gamma,A^{\prime})$,
$\sigma:\mathsf{Sub}(\Gamma,\mathsf{nil})$, and
$e^{\prime}:\mathsf{Tm}(\mathsf{nil},A)$, we have that
$e[\uparrow^{A}\sigma][e^{\prime}]=e[\mathsf{cons}(e^{\prime},\sigma)]$.

###  3.3. Operational semantics

We work with a call-by-value operational semantics for STLC:

Inductive
$\displaystyle\mathsf{Val}:\,\mathrel{\\{A\\}}\mathsf{Pg}(A)\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}}/\mathsf{val}$
$\displaystyle:\mathsf{Val}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}}/\mathsf{val}$
$\displaystyle:\mathsf{Val}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{lam}}}/\mathsf{val}$
$\displaystyle:\,\mathrel{\\{e\\}}\mathsf{Val}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{lam}}}(e))$
Inductive
$\displaystyle{\mapsto}:\,\mathrel{\\{A\\}}\mathsf{Pg}(A)\to\mathsf{Pg}(A)\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle\beta$
$\displaystyle:\,\mathrel{\\{A_{1},A_{2},e,e_{1}\\}}{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{lam}}}(e),e_{1})\mapsto
e[e_{1}]$ $\displaystyle\mathsf{ap}/\mathsf{l}$
$\displaystyle:\,\mathrel{\\{A_{1},A_{2},e,e^{\prime},e_{1}\\}}e\mapsto
e^{\prime}\to{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}(e,e_{1})\mapsto{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}(e^{\prime},e_{1})$
$\displaystyle\mathsf{ap}/\mathsf{l}$
$\displaystyle:\,\mathrel{\\{A_{1},A_{2},e,e^{\prime},e_{1}\\}}\mathsf{Val}(e)\to
e_{1}\mapsto
e_{1}^{\prime}\to{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}(e,e_{1})\mapsto{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}(e,e_{1}^{\prime})$

In the above, we write $\mathsf{Pg}(A)\coloneqq\mathsf{Tm}([],A)$ for the type
of closed STLC terms. Evaluation may be defined as the reflexive-transitive
closure of $\mapsto$:

Inductive
$\displaystyle\mapsto^{*}:\,\mathrel{\\{A\\}}\mathsf{Pg}(A)\to\mathsf{Pg}(A)\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle\mathsf{refl}$ $\displaystyle:\,\mathrel{\\{e\\}}e\mapsto^{*}e$
$\displaystyle\mathsf{trans}$ $\displaystyle:\,\mathrel{\\{e\\}}e\mapsto
e_{1}\to e_{1}\mapsto^{*}e_{2}\to e\mapsto^{*}e_{2}$

We then define evaluation: $e\Downarrow v\coloneqq
e\mapsto^{*}v\times\mathsf{Val}(v)$. In a similar fashion, we may define the
cost-aware evaluation relation by using a $\mathbb{N}$-indexed version of the
reflexive-transitive closure of $\mapsto$: $e\Downarrow^{c}v\coloneqq
e\mapsto^{(c)}v\times\mathsf{Val}(v)$.

####  3.3.1. Phase-separated cost semantics

As discussed in Section 1.2, we cannot directly use the cost-aware evaluation
relation defined above in the statement of the cost-aware adequacy theorem.
Instead, we define a more refined version of the cost-aware evaluation
relation that _restricts_ to the ordinary evaluation relation in the
extensional phase. To this end, we may define a _phase-separated_ version of
the cost-aware reflexive transitive closure:

Inductive
$\displaystyle{\mapsto_{\P_{\mathsf{E}}}}:\,\mathrel{\\{A\\}}\mathsf{Pg}(A)\to\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}\mathbb{N}\to\mathsf{Pg}(A)\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle\mathsf{refl}$
$\displaystyle:\,\mathrel{\\{e\\}}e\mapsto_{\P_{\mathsf{E}}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}0}e$
$\displaystyle\mathsf{trans}$ $\displaystyle:\,\mathrel{\\{c,e\\}}e\mapsto
e_{1}\to e_{1}\mapsto_{\P_{\mathsf{E}}}^{c}e_{2}\to
e\mapsto_{\P_{\mathsf{E}}}^{c\mathrel{(\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}+)}\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}1}e_{2}$

Cruically, this relation becomes equivalent to the ordinary reflexive
transitive closure under the extensional phase:

###### Proposition 3.3.

Given $u:\P_{\mathsf{E}}$, we have that
$e\mapsto_{\P_{\mathsf{E}}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c}v$
if and only if $e\mapsto^{*}v$ for all $c:\mathbb{N}$.

Consequently, we may define phase-separated evaluation as
$e\Downarrow_{\P_{\mathsf{E}}}^{c}v\coloneqq
e\mapsto^{(c)}v\times\mathsf{Val}(v)$, which satisfies a similar restriction
property:

###### Proposition 3.4.

Given $u:\P_{\mathsf{E}}$, we have that
$e\Downarrow_{\P_{\mathsf{E}}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c}v$
if and only if $e\Downarrow v$ for all $c:\mathbb{N}$.

###  3.4. A cost-aware denotational semantics for STLC

We now define a denotational semantics for STLC in $\textbf{calf}{}^{\star}$
based on the standard polarized decomposition of call-by-value. Types are
interpreted as follows:

$\displaystyle\llbracket-\rrbracket_{\mathsf{Ty}}$
$\displaystyle:\mathsf{Ty}\to\mathsf{tp}^{+}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}\rrbracket_{\mathsf{Ty}}$
$\displaystyle=\mathsf{bool}$ $\displaystyle\llbracket A_{1}\Rightarrow
A_{2}\rrbracket_{\mathsf{Ty}}$
$\displaystyle=\mathsf{U}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{1}\rrbracket_{\mathsf{Ty}}\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{1}\rrbracket_{\mathsf{Ty}}\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{1}\rrbracket_{\mathsf{Ty}}\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{1}\rrbracket_{\mathsf{Ty}}\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{2}\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}$}\mathclose{}{)}}$

The interpretation for types is extended to contexts in the obvious way:

$\displaystyle\llbracket-\rrbracket_{\mathsf{Con}}$
$\displaystyle:\mathsf{Con}\to\mathsf{tp}^{+}$
$\displaystyle\llbracket\mathsf{nil}\rrbracket_{\mathsf{Con}}$
$\displaystyle=1$ $\displaystyle\llbracket A::\Gamma\rrbracket_{\mathsf{Con}}$
$\displaystyle=\llbracket
A\rrbracket_{\mathsf{Ty}}\times\llbracket\Gamma\rrbracket_{\mathsf{Con}}$

For the interpretation of terms, we insert cost effects for elimination forms
to account for steps in the operational semantics:

$\displaystyle\llbracket-\rrbracket_{\mathsf{Var}}$
$\displaystyle:\,\mathrel{\\{\Gamma,A\\}}\mathsf{Var}(\Gamma,A)\to\llbracket\Gamma\rrbracket_{\mathsf{Con}}\to\llbracket
A\rrbracket_{\mathsf{Ty}}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{here}}}\rrbracket_{\mathsf{Var}}$
$\displaystyle=\pi_{1}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{next}}}(v)\rrbracket_{\mathsf{Var}}$
$\displaystyle=\llbracket v\rrbracket_{\mathsf{Tm}}\circ\pi_{2}$
$\displaystyle\llbracket-\rrbracket_{\mathsf{Tm}}$
$\displaystyle:\,\mathrel{\\{\Gamma,A\\}}\mathsf{Tm}(\Gamma,A)\to\llbracket\Gamma\rrbracket_{\mathsf{Con}}\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{var}}}(v)\rrbracket_{\mathsf{Tm}}$
$\displaystyle=\mathsf{ret}\circ\llbracket v\rrbracket_{\mathsf{Var}}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}}\rrbracket_{\mathsf{Tm}}$
$\displaystyle=\lambda\\_.\;\mathsf{ret}(\mathsf{tt})$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}\rrbracket_{\mathsf{Tm}}$
$\displaystyle=\lambda\\_.\;\mathsf{ret}(\mathsf{ff})$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{lam}}}(e)\rrbracket_{\mathsf{Tm}}$
$\displaystyle=\lambda\gamma:\llbracket\Gamma\rrbracket_{\mathsf{Con}}.\;\lambda
a:\llbracket A_{1}\rrbracket_{\mathsf{Ty}}.\;\llbracket
e\rrbracket_{\mathsf{Tm}}(a,\gamma)$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}(e,e_{1})\rrbracket_{\mathsf{Tm}}$
$\displaystyle=\lambda\gamma:\llbracket\Gamma\rrbracket_{\mathsf{Con}}.\;\mathsf{bind}(\llbracket
e\rrbracket_{\mathsf{Tm}}(\gamma);\lambda f.\;\mathsf{bind}(\llbracket
e_{1}\rrbracket_{\mathsf{Tm}}(\gamma);\lambda a.\;\mathsf{step}^{1}(f(a))))$

###  3.5. Computational adequacy

####  3.5.1. Logical relation for adequacy

Following the classic adequacy proof of Plotkin, we prove our cost-aware
adequacy theorem by means of a logical relations construction. First, we
define a binary logical relation relating the values of STLC of type
$A:\mathsf{Ty}^{\lambda}{}$ with values in the semantic domain $\llbracket
A\rrbracket^{\textbf{STLC}{}}_{\mathsf{Ty}}$ by induction on $A$:

$\displaystyle{\approx}$
$\displaystyle:\,\mathrel{\\{A\\}}\mathsf{Pg}(A)\to\llbracket
A\rrbracket_{\mathsf{Ty}}\to\mathsf{tp}^{+}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{b}}}\approx_{{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}}b$
$\displaystyle=({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{b}}}=\overline{b})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e}}}\approx_{A_{1}\Rightarrow
A_{2}}e$
$\displaystyle=(\Sigma{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e_{2}}}}:\mathsf{Tm}^{\lambda}(A_{1},A_{2}).\;{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e}}}={\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{lam}}}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e_{2}}}})$
$\displaystyle\times\mathsf{U}((({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e_{1}}}}:\mathsf{Pg}(A_{1}),e_{1}:\llbracket
A_{1}\rrbracket_{\mathsf{Ty}})\to{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e_{1}}}}\approx_{A_{1}}e_{1}\to{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e_{2}}}}[{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e_{1}}}}]\approx^{\Downarrow}_{A_{2}}e(e_{1}))))$

In the above $\overline{-}$ sends $\mathsf{tt}$ to
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}}$
and $\mathsf{ff}$ to
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}$,
and $-^{\Downarrow}$ lifts a relation on values to computations using the
phase-separated evaluation relation defined in Section 3.3.1:

$\displaystyle-^{\Downarrow}$
$\displaystyle:\,\mathrel{\\{A\\}}(\mathsf{Pg}(A)\to\llbracket
A\rrbracket_{\mathsf{Ty}}\to\mathsf{tp}^{+})\to(\mathsf{Pg}(A)\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket_{\mathsf{Ty}}$}\mathclose{}{)}}\to\mathsf{tp}^{+})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e}}}\mathrel{R^{\Downarrow}}e$
$\displaystyle=\Sigma{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{v}}}:\mathsf{Pg}(A).\;\Sigma
v:\llbracket
A\rrbracket_{\mathsf{Ty}}.\;({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{e}}}\Downarrow_{\P_{\mathsf{E}}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c}{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{v}}})\times
e=\mathsf{step}^{c}(\mathsf{ret}(v))\times{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{v}}}\mathrel{R}v$

The relation is readily lifted to contexts:

Inductive
$\displaystyle{\approx}:\,\mathrel{\\{\Gamma\\}}\mathsf{Inst}(\Gamma)\to\llbracket\Gamma\rrbracket_{\mathsf{Con}}\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle\mathsf{emp}$
$\displaystyle:\mathsf{nil}\approx_{\cdot}\mathsf{\star}$
$\displaystyle\mathsf{cons}$
$\displaystyle:\,\mathrel{\\{\Gamma,{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{\gamma}}},\gamma,A,{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{a}}},a\\}}{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{a}}}\approx_{A}a\to{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{\gamma}}}\approx_{\Gamma}\gamma\to\mathsf{cons}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{a}}},{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{\gamma}}})\approx_{A::\Gamma}(a,\gamma)$

####  3.5.2. Fundamental theorem

As usual, we may prove the fundamental theorem of the logical relation by
induction on terms. The details of the proof can be found in Appendix A.

###### Theorem 3.5 (FTLR).

Given a STLC term $e:\mathsf{Tm}^{\lambda}(\Gamma,A)$, if
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{\gamma}}}\approx_{\Gamma}\gamma$,
then
$e[{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{\gamma}}}]\approx^{\Downarrow}_{A}\llbracket
e\rrbracket_{\mathsf{Tm}}(\gamma)$.

###### Corollary 3.6 (Computational adequacy).

Given a closed term
$e:\mathsf{Pg}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}})$,
if $e=\mathsf{step}^{c}(\mathsf{ret}(b))$ for some $c:\mathbb{N}$ and
$b:\mathsf{bool}$, then
$e\Downarrow^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c}\overline{b}$.

###### Proof.

Suppose that
$e:\mathsf{Pg}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}})$
and $e=\mathsf{step}^{c}(\mathsf{ret}(b))$. By Theorem 3.5, we know that
$e\approx^{\Downarrow}_{{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}}\llbracket
e\rrbracket^{\textbf{STLC}{}}_{\mathsf{Tm}}$, which means that there exists
$c^{\prime}$,
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{b}}}$,
and $b^{\prime}$ such that
$e\Downarrow_{\P_{\mathsf{E}}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c^{\prime}}{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{b}}}$,
$e=\mathsf{step}^{c^{\prime}}(\mathsf{ret}(b^{\prime}))$, and
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{b}}}\approx_{{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}}b^{\prime}$.
By $\mathsf{step}/\mathsf{inj}$, we have that $b=b^{\prime}$ and
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=c^{\prime})$.
By the definition of the logical relation at
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$,
we have that
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{b}}}=\overline{b^{\prime}}=\overline{b}$.
The result then holds because
$\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c^{\prime}=\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c$
since 🌑 is a lex monad. ∎

###### Corollary 3.7 (Extensional adequacy).

Suppose that $u:\P_{\mathsf{E}}$. Given a closed term
$e:\mathsf{Pg}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}})$,
if $e=\mathsf{ret}(b)$ for some $b:\mathsf{bool}$, then
$e\Downarrow\overline{b}$.

###### Proof.

Because $e=\mathsf{ret}(b)=\mathsf{step}^{0}(\mathsf{ret}(b))$, we may apply
Corollary 3.6 to obtain
$e\Downarrow_{\P_{\mathsf{E}}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}0}\overline{b}$.
But since we have $u:\P_{\mathsf{E}}$, we have $e\Downarrow\overline{b}$ by
Proposition 3.4. ∎

##  4\. $\textbf{calf}{}^{\omega}$: unbounded iteration

In order to define a model of Modernized Algol (see Section 5), we will need
to extend $\textbf{calf}{}^{\star}$ with facilities for modeling while loops.
In this section, we present $\textbf{calf}{}^{\omega}$, a metalanguage for
_unbounded iteration_. An intuitive way to think about iteration is as a
coinductive system. If we are given a “one step” computation $f:A\to B+A$ in
which the left summand represents the terminal state and the right summand
represents the nonterminal state, an iterative computation of $f$ can be
thought of as running $f$ until the terminal state is reached. In terms of
equations this is expressed as an unfolding rule:
$\mathsf{iter}(f,a)=[\mathsf{ret};\mathsf{iter}(f)]\circ f(a)$ (here
$[f;g]:A+B\to C$ is the sum of $f:A\to C$ and $g:B\to C$).

##### Lifted computations

Although it might be tempting to combine the computational effects of _cost_
and _partiality_ , doing so will complicate our model construction for
$\textbf{calf}{}^{\omega}$. In particular, it is not immediately clear how to
assign meaning to a potential divergent _type_ computation in the usual
adjunction models of CBPV we consider in this paper. Fortunately, we may
sidestep this problem by axiomatizing a more general class of _lifted
computations_ $\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}$ that supports possibly divergent computations and isolate
among these the previously cost-sensitive (but total) computations
$FA\hookrightarrow LA$:

$\displaystyle\mathsf{L}$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{\ominus}$
$\displaystyle\mathsf{lift}$
$\displaystyle:\,\mathrel{\\{A\\}}\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}\to\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}$ $\displaystyle\mathsf{lift}/\mathsf{inj}$
$\displaystyle:\,\mathrel{\\{A\\}}\mathsf{lift}(e)=\mathsf{lift}(e^{\prime})\to
e=e^{\prime}$

Similar to free computations, we may sequence lifted computations:

$\displaystyle\mathsf{bind}_{\mathsf{L}}$
$\displaystyle:\,\mathrel{\\{A,B\\}}\mathsf{tm}^{\ominus}(\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})\to(\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B$}\mathclose{}{)}}))\to\mathsf{tm}^{\ominus}(\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B$}\mathclose{}{)}})$

Note that in contrast to free computations one may only sequence a lifted
computation with another lifted computation. The sequencing satisfies the
expected equational laws with respect to the unit of lifting, defined as
$\mathsf{ret}_{\mathsf{L}}\coloneqq\mathsf{lift}\circ\mathsf{ret}$. Moreover,
the lifting of free computations commutes with sequencing and the cost effect:

$\displaystyle\mathsf{lift}/\mathsf{bind}$
$\displaystyle:\,\mathrel{\\{A,B,e,f\\}}\mathsf{lift}(\mathsf{bind}(e;f))=\mathsf{bind}_{\mathsf{L}}(\mathsf{lift}(e);\mathsf{lift}\circ
f)$ $\displaystyle\mathsf{lift}/\mathsf{step}$
$\displaystyle:\,\mathrel{\\{A,e,c\\}}\mathsf{lift}(\mathsf{step}^{c}(e))=\mathsf{step}^{c}(\mathsf{lift}(e))$

##### Notation

We write $a\leftarrow e;f(a)$ for $\mathsf{bind}(e;f)$ and
$a\leftarrow_{\mathsf{L}}e;f(a)$ for $\mathsf{bind}_{\mathsf{L}}(e;f)$.

##### Propositional truncation

In order to state the axioms governing cost decomposition for
$\textbf{calf}{}^{\omega}$, we will need to work with the _propositional
truncation_ of a type Univalent Foundations Program (2013). Following standard
notation, we write $\lVert A\rVert$ for the propositional truncation of a
given type $A$. As usual we define _mere existence_ as the propositional
truncation of a dependent sum: $\exists a:A.\;B(a)\coloneqq\lVert\Sigma
a:A.\;B(a)\rVert$. Given an assumption of the form $\exists a:A.\;B(a)$, we
say that “there merely exists $a:A$ such that $B(a)$”. The universal property
of propositional truncation allows one to extract the witness $a$ and
associated data $B(a)$ when one is proving a proposition.

##### Higher-order recursion

Given that we have indulged in unbounded iteration, it is natural to ask why
not also assume arbitrary fixed-points, from which iteration may be derived as
a special case? As we will show in Section 8, we model _lifted_ computations
of $\textbf{calf}{}^{\omega}$ as terms of a certain partiality monad $\bot$.
However, $\bot$ only supports recursion for _continuous_ functions, and it is
not possible to enforce this property in the kind of model we use to interpret
$\textbf{calf}{}^{\star}$ and $\textbf{calf}{}^{\omega}$. A possibility for
adding _all_ fixed-points on a computation domain is to use _synthetic domain
theory_ , which we discuss in Section 9.

###  4.1. Axioms for iteration

Equipped with this intuition, we may axiomatize iteration in
$\textbf{calf}{}^{\omega}$ as follows; note that iteration is only available
for lifted computations:

$\displaystyle\mathsf{iter}$
$\displaystyle:\,\mathrel{\\{A,B\\}}(\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B+A$}\mathclose{}{)}}))\to
A\to\mathsf{tm}^{\ominus}(\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B$}\mathclose{}{)}})$ $\displaystyle\mathsf{iter}/\mathsf{unfold}$
$\displaystyle:\,\mathrel{\\{A,B,f,a,a^{\prime}\\}}\mathsf{iter}(f)(a)=\mathsf{bind}_{\mathsf{L}}(f(a);[\mathsf{ret}_{\mathsf{L}}(b);\mathsf{iter}(f)])$

As we will see in Section 5.5, we need iterative computations to satisfy a
certain compactness property, in the sense that whenever an iterative
computation $\mathsf{iter}(f,a)$ has a cost bound, there is a finite prefix
$\mathsf{seq}(f,k,a)$ that suffices for obtaining that cost bound:

$\displaystyle\mathsf{seq}$
$\displaystyle:\,\mathrel{\\{A,B\\}}(\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B+A$}\mathclose{}{)}}))\to\mathbb{N}\to\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B+A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B+A$}\mathclose{}{)}})$ $\displaystyle\mathsf{seq}(f,0)(a)$
$\displaystyle=\mathsf{ret}_{\mathsf{L}}(\mathsf{inr}(a))$
$\displaystyle\mathsf{seq}(f,k+1)(a)$
$\displaystyle=\mathsf{bind}_{\mathsf{L}}(f(a);[\mathsf{ret}_{\mathsf{L}}\circ\mathsf{inl};\mathsf{seq}(f,k)])$
$\displaystyle\mathsf{iter}/\mathsf{trunc}$
$\displaystyle:\,\mathrel{\\{A,B,f,a,b,c\\}}\mathsf{iter}(f,a)=\mathsf{step}^{c}(\mathsf{ret}_{\mathsf{L}}(b))\to$
$\displaystyle\lVert\Sigma
k:\mathbb{N}.\;\mathsf{seq}(g,k)(a)=\mathsf{step}^{c}(\mathsf{ret}_{\mathsf{L}}(\mathsf{inl}(b)))\rVert$

Similar to the uniqueness axioms we introduced in Section 3, we require that
cost bounds for lifted computations are unique:

$\displaystyle\mathsf{step}_{\mathsf{L}}/\mathsf{inj}$
$\displaystyle:\,\mathrel{\\{A,(a,a^{\prime}:A)(c,c^{\prime}:\mathbb{C})\\}}\mathsf{step}^{c}(\mathsf{ret}_{\mathsf{L}}(a))=\mathsf{step}^{c^{\prime}}(\mathsf{ret}_{\mathsf{L}}(a^{\prime}))\to(a=a^{\prime})\times\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=c^{\prime})$

we will also postulate that cost bounds on lifted computations may be
decomposed:

$\displaystyle\mathsf{bind}_{\mathsf{L}}^{-1}$
$\displaystyle:\,\mathrel{\\{A,B,e,f,c,b\\}}\mathsf{bind}_{\mathsf{L}}(e;f)=\mathsf{step}^{c}(\mathsf{ret}_{\mathsf{L}}(b))\to\lVert\Sigma
c_{1},c_{2}:\mathbb{C}.\;\Sigma
a:A.\;e=\mathsf{step}^{c_{1}}(\mathsf{ret}_{\mathsf{L}}(a))\times$
$\displaystyle
f(a)=\mathsf{step}^{c_{2}}(\mathsf{ret}_{\mathsf{L}}(b))\times\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=c_{1}+c_{2})\rVert$
$\displaystyle\mathsf{step}_{\mathsf{L}}^{-1}$
$\displaystyle:\,\mathrel{\\{A,c,c_{1},a\\}}\mathsf{step}^{c_{1}}(e)=\mathsf{step}^{c}(\mathsf{ret}_{\mathsf{L}}(a))\to\lVert\Sigma
c_{2}:\mathbb{C}.\;e=\mathsf{step}^{c_{2}}(\mathsf{ret}_{\mathsf{L}}(a))\times\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=c_{1}+c_{2})\rVert$

Note that the corresponding laws for free computations may be derived using
the properties of the lifting operation $\mathsf{lift}$:

###### Proposition 4.1.

There are terms of the following types:

$\displaystyle\mathsf{step}/\mathsf{inj}$
$\displaystyle:\,\mathrel{\\{A,(a,a^{\prime}:A)(c,c^{\prime}:\mathbb{C})\\}}\mathsf{step}^{c}(\mathsf{ret}(a))=\mathsf{step}^{c^{\prime}}(\mathsf{ret}(a^{\prime}))\to(a=a^{\prime})\times\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=c^{\prime})$
$\displaystyle\mathsf{bind}^{-1}$
$\displaystyle:\,\mathrel{\\{A,X,e,f,c,b\\}}\mathsf{bind}(e;f)=\mathsf{step}^{c}(\mathsf{ret}(b))\to\lVert\Sigma
c_{1},c_{2}:\mathbb{C}.\;\Sigma
a:A.\;e=\mathsf{step}^{c_{1}}(\mathsf{ret}(a))\times$ $\displaystyle
f(a)=\mathsf{step}^{c_{2}}(\mathsf{ret}(b))\times\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=c_{1}+c_{2})\rVert$
$\displaystyle\mathsf{step}^{-1}$
$\displaystyle:\,\mathrel{\\{A,c,c_{1},e,a\\}}\mathsf{step}^{c_{1}}(e)=\mathsf{step}^{c}(\mathsf{ret}(a))\to\lVert\Sigma
c_{2}:\mathbb{C}.\;e=\mathsf{step}^{c_{2}}(\mathsf{ret}(a))\times\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=c_{1}+c_{2})\rVert$

From these axioms, we may derive some useful reasoning principles regarding
cost bounds:

###### Proposition 4.2.

There is a term of type
$\mathsf{step}^{c}(\mathsf{ret}_{\mathsf{L}}(a))=\mathsf{ret}_{\mathsf{L}}(a^{\prime})\to\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=0)$.

###### Proof.

By $\mathsf{step}_{\mathsf{L}}^{-1}$, we have that there merely exists
$c^{\prime}$ such that
$\mathsf{ret}_{\mathsf{L}}(a)=\mathsf{step}^{c^{\prime}}(\mathsf{ret}_{\mathsf{L}}(a^{\prime}))$
and
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(0=c+c^{\prime})$.
Because
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=0)$
is a proposition, we may project the underlying witness and data. Lifting
using the functorial action of 🌑, it suffices to show that there is a term
$0=c+c^{\prime}\to c=0$, which clearly holds for a cancellative monoid. ∎

###### Proposition 4.3.

There is a term of type
$\mathsf{step}^{c}(\mathsf{ret}_{\mathsf{L}}(a))=\mathsf{ret}_{\mathsf{L}}(a^{\prime})\to(a=a^{\prime})$.

###### Proof.

By Proposition 4.2, we have that
$\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}(c=0)$.
By induction principle of the closed modality, we have to consider two cases.
First, if $u:\P_{\mathsf{E}}$, then we have
$\mathsf{step}^{c}(\mathsf{ret}_{\mathsf{L}}(a))=\mathsf{ret}_{\mathsf{L}}(a)=\mathsf{ret}_{\mathsf{L}}(a^{\prime})$,
from which the result follows from $\mathsf{ret}/\mathsf{inj}$ and
$\mathsf{in}/\mathsf{inj}$. Otherwise, we have $c=0$, and the result holds
from the same argument. ∎

##  5\. Modernized Algol

We define and study a denotational semantics for a variant of Modernized Algol
(MA) as formulated in Harper (2012). MA is a procedural programming language
with first-order store and unbounded iteration and obeys a stack discipline in
the sense that store assignables are deallocated when they go out of scope. A
characteristic feature of MA is the distinction between expressions and
commmands that reflects the separation of mathematical and effectful
computation. Unlike _op. cit_., we restrict our expression language to a total
language (a mild extension of STLC as presented in Section 3) and extend the
command language with a primitive iteration command.

The version of MA that we present is not as bare-bones as the STLC from
Section 3, but it is still somewhat austere in terms of type structures, with
natural numbers being the only (non trivial) inductive data type. Because our
intention is to illustrate the construction and adequacy proof of a cost-aware
denotational semantics, we have delibrately kept the language in question
simple to isolate the core ideas. The methods we develop here may be extended
to include richer data structures so that one may program the algorithms
studied in Niu et al. (2022) (in fact we can already define Euclid’s algorithm
in this modest version of MA).

###  5.1. Syntax of MA

MA is equipped with a small class of inductive types, functions types, and a
type
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{cmd}}}(A)$
of reified commands that compute expressions of type $A$ (see Fig. 2). We also
outline a class of _strictly positive types_ that may be used as assignables,
which restricts MA to _first-order stores_. We define the type of strictly
positive types as $\mathsf{Pos}\coloneqq\Sigma
A:\mathsf{Ty}^{\textbf{MA}{}}{}.\;\mathsf{pos}(A)$.

##### Convention

In order to faciliate readbility, we will not write the proof of strict
positivity, _i.e_. we write
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}:\mathsf{Pos}$
for
$({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}},{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}/\mathsf{pos}):\mathsf{Pos}$.

Inductive $\displaystyle\mathsf{Ty}^{\textbf{MA}{}}{}\;\textbf{where}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}}$
$\displaystyle:\mathsf{Ty}^{\textbf{MA}{}}{}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$
$\displaystyle:\mathsf{Ty}^{\textbf{MA}{}}{}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}$
$\displaystyle:\mathsf{Ty}^{\textbf{MA}{}}{}$ $\displaystyle\Rightarrow$
$\displaystyle:\mathsf{Ty}^{\textbf{MA}{}}{}\to\mathsf{Ty}^{\textbf{MA}{}}{}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{cmd}}}$
$\displaystyle:\mathsf{Ty}^{\textbf{MA}{}}{}\to\mathsf{Ty}^{\textbf{MA}{}}{}$

Inductive
$\displaystyle\mathsf{pos}:\mathsf{Ty}^{\textbf{MA}{}}{}\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}}/\mathsf{pos}$
$\displaystyle:\mathsf{pos}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}/\mathsf{pos}$
$\displaystyle:\mathsf{pos}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}})$
$\displaystyle{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}/\mathsf{pos}$
$\displaystyle:\mathsf{pos}({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}})$

Figure 2. Left: types of MA; right: strictly positive types.

As for the STLC, we work with an instrinsic encoding of MA; the terms of MA
are presented in Fig. 3. Both the judgment for well-typed commands
$\mathsf{Cmd}^{\textbf{MA}{}}$ and expressions $\mathsf{Tm}^{\textbf{MA}{}}$
are indexed by a _signature_
$\mathsf{Sig}\coloneqq\mathsf{list}(\mathsf{Pos})$ of strictly positive types.
Well-typed expressions $e:\mathsf{Tm}^{\textbf{MA}{}}(\Sigma,\Gamma,A)$ are
written as $\Gamma\vdash_{\Sigma}e:A$ and well-typed commands
$m:\mathsf{Cmd}^{\textbf{MA}{}}(\Sigma,\Gamma,A)$ are written as
$\Gamma\vdash_{\Sigma}m\div A$; note that we make use of a mutual inductive
definition because well-typed expressions and commands must be defined
simultaneously.

Inductive
$\displaystyle\mathsf{Var}:\mathsf{Ctx}\to\mathsf{Ty}^{\textbf{MA}{}}\to\mathsf{tp}^{+}\;\textbf{where}$
Inductive
$\displaystyle\mathsf{Cmd}^{\textbf{MA}{}}:\mathsf{Sig}\to\mathsf{Ctx}\to\mathsf{Ty}^{\textbf{MA}{}}{}\to\mathsf{tp}^{+}\;\textbf{where}$
mutual
$\displaystyle\mathsf{Tm}^{\textbf{MA}{}}:\mathsf{Sig}\to\mathsf{Ctx}\to\mathsf{Ty}^{\textbf{MA}{}}{}\to\mathsf{tp}^{+}\;\textbf{where}$

v : $\mathsf{Var}$(Γ, A)
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{var}}}$(v)
: A

Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{\star}}}$
:
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}}$

Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{zero}}}$
:
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}$

Γ⊢_Σe :
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}$
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{suc}}}$(e)
:
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}$

Γ⊢_Σe :
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}$
Γ⊢_Σe_1 : A
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}$::Γ⊢_Σe_2
: A
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ifz}}}$(e,
e_1, e_2) : A

Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}}$,
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}$
:
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$

A_1::Γ⊢_Σe : A_2
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{lam}}}$(e)
: A_1 ⇒A_2

Γ⊢_Σe : A_1 ⇒A_2
Γ⊢_Σe_1 : A_1
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}$(e,
e_1) : A_2

Γ⊢_Σ m ÷A Γ⊢_Σ
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{cmd}}}$(m)
:
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{cmd}}}$(A)

Γ⊢_Σa : A
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ret}}}$(a)
:
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{cmd}}}$(A)

Γ⊢_Σe :
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{cmd}}}$(A)
A::Γ⊢_Σm ÷B
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bnd}}}$(e,
m) ÷B

Σ[n] =
(${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$
, -)
Γ⊢_Σm
÷${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}}$
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{while}}}$[n](m)
÷${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}}$

Σ[n] = (A , -) Γ⊢_Σ
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{get}}}$[n]
÷A

Σ[n] = (A , -)
Γ⊢_Σe : A Γ⊢_Σ
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{set}}}$[n](e)
÷${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$

A_$\mathsf{pos}$ : $\mathsf{pos}$(A)
Γ⊢_Σ e : A
Γ⊢_(A, A_$\mathsf{pos}$)::Σ m
÷${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$
Γ⊢_Σ${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{dcl}}}$(e,
m) :
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}$

Figure 3. Expressions and commands of MA.

###  5.2. Preorder of signatures

In the possible worlds semantics/Kripke models of mutable store, the
interpretation of signature-indexed commands and expressions can be thought of
as a family of models linked by a contravariant action on the _preorder
relation_ on the signatures, which represents the stability of the
interpretation with respect to allocation of new assignables. We may define
the preorder on signatures as follows:

Inductive
$\displaystyle\geq:\mathsf{Con}\to\mathsf{Con}\to\mathsf{tp}^{+}\;\textbf{where}$
$\displaystyle\mathsf{refl}$
$\displaystyle:\,\mathrel{\\{\Sigma\\}}\Sigma\geq\Sigma$
$\displaystyle\mathsf{mono}$
$\displaystyle:\,\mathrel{\\{\Sigma,\Sigma^{\prime},A\\}}\Sigma^{\prime}\geq\Sigma\to
A::\Sigma^{\prime}\geq A::\Sigma$ $\displaystyle\mathsf{extend}$
$\displaystyle:\,\mathrel{\\{\Sigma,\Sigma^{\prime},A\\}}\Sigma^{\prime}\geq\Sigma\to
A::\Sigma^{\prime}\geq\Sigma$

In other words, we have a proof of $\Sigma^{\prime}\geq\Sigma$ whenever
$\Sigma$ occurs as a _subsequence_ of $\Sigma^{\prime}$.

###### Proposition 5.1.

The relation $\geq$ is reflexive and transitive. We write
$\mathsf{tr}:\,\mathrel{\\{\Sigma^{\prime\prime},\Sigma^{\prime},\Sigma:\mathsf{Sig}\\}}\Sigma^{\prime\prime}\geq\Sigma^{\prime}\to\Sigma^{\prime}\geq\Sigma\to\Sigma^{\prime\prime}\geq\Sigma$
for the proof of transitivity.

##### Action of the preorder of signatures

First, we show that one may shift assignables along a signature extension:

###### Proposition 5.2.

There is a map
$\mathsf{sh}:\,\mathrel{\\{\Sigma,\Sigma^{\prime}\\}}\Sigma^{\prime}\geq\Sigma\to\mathbb{N}\to\mathbb{N}$

###### Proposition 5.3.

There is a map
$\Uparrow:\,\mathrel{\\{\Sigma,\Sigma^{\prime},\Gamma,A\\}}\Sigma^{\prime}\geq\Sigma\to\mathsf{Tm}^{\textbf{MA}{}}(\Sigma,\Gamma,A)\to\mathsf{Tm}^{\textbf{MA}{}}(\Sigma^{\prime},\Gamma,A)$.

###### Proposition 5.4.

There is a map
$\Uparrow:\,\mathrel{\\{\Sigma,\Sigma^{\prime},\Gamma,A\\}}\Sigma^{\prime}\geq\Sigma\to\mathsf{Cmd}^{\textbf{MA}{}}(\Sigma,\Gamma,A)\to\mathsf{Cmd}^{\textbf{MA}{}}(\Sigma^{\prime},\Gamma,A)$.

####  5.2.1. Substitution

###### Definition 5.5 (Substitution).

Given a signature $\Sigma$, a substitution from $\Gamma$ to $\Gamma^{\prime}$
is defined as
$\mathsf{Sub}_{\Sigma}(\Gamma,\Gamma^{\prime})\coloneqq(A:\mathsf{Ty})\to\mathsf{Var}(\Gamma,A)\to\mathsf{Tm}(\Sigma,\Gamma^{\prime},A)$.

The action of the preorder of signatures extends to substitions:

###### Proposition 5.6.

There is a map
${\Uparrow}:\,\mathrel{\\{\Sigma,\Sigma^{\prime},\Gamma,\Gamma^{\prime}\\}}\Sigma^{\prime}\geq\Sigma\to\mathsf{Sub}_{\Sigma}(\Gamma,\Gamma^{\prime})\to\mathsf{Sub}_{\Sigma^{\prime}}(\Gamma,\Gamma^{\prime})$.

We write the following for the application of a subsititution to an expression
and a command:

$\displaystyle-[-]$
$\displaystyle:\,\mathrel{\\{\Sigma,\Gamma,A\\}}\mathsf{Tm}^{\textbf{MA}{}}(\Sigma,\Gamma,A)\to\mathsf{Sub}_{\Sigma}(\Gamma,\Gamma^{\prime})\to\mathsf{Tm}^{\textbf{MA}{}}(\Sigma,\Gamma^{\prime},A)$
$\displaystyle-[-]$
$\displaystyle:\,\mathrel{\\{\Sigma,\Gamma,A\\}}\mathsf{Cmd}^{\textbf{MA}{}}(\Sigma,\Gamma,A)\to\mathsf{Sub}_{\Sigma}(\Gamma,\Gamma^{\prime})\to\mathsf{Cmd}^{\textbf{MA}{}}(\Sigma,\Gamma^{\prime},A)$

###  5.3. Operational semantics of MA

The operational semantics of MA is defined separately for expressions and
commands. Expressions execute via substitution as in STLC:

$\displaystyle\mathsf{val}$
$\displaystyle:\,\mathrel{\\{\Sigma,A\\}}\mathsf{Pg}(\Sigma,A)\to\mathsf{tp}^{+}$
$\displaystyle{\mapsto}$
$\displaystyle:\,\mathrel{\\{\Sigma,A\\}}\mathsf{Pg}(\Sigma,A)\to\mathsf{Pg}(\Sigma,A)\to\mathsf{tp}^{+}$

In the above, we defined closed expressions as
$\mathsf{Pg}(A)\coloneqq\mathsf{Tm}^{\textbf{MA}{}}(\Sigma,\mathsf{nil},A)$.
Define $\mathsf{Val}(\Sigma,A)\coloneqq\Sigma
e:\mathsf{Pg}(\Sigma,A).\;\mathsf{val}(e)$. In contrast to expressions,
commands execute in conjunction with a _store_ that contains values associated
to the declared assignables. More explicitly, we may define a store as the
following family indexed in a signature:

$\displaystyle\mathsf{store}$ $\displaystyle:\mathsf{Sig}\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{emp}$ $\displaystyle:\mathsf{Store}(\mathsf{nil})$
$\displaystyle\mathsf{extend}$
$\displaystyle:\,\mathrel{\\{\Sigma,A\\}}(p:\mathsf{pos}(A))\to\mathsf{Val}(\mathsf{nil},A)\to\mathsf{Store}(\Sigma)\to\mathsf{Store}((A,p)::\Sigma)$

A _state_ is composed of a store and command, defined as
$\mathsf{State}(\Sigma,A)\coloneqq\mathsf{Store}(\Sigma)\times\mathsf{Cmd}(\Sigma,A)$,
and we have the following judgments governing the dynamics of states:

$\displaystyle\mathsf{final}$
$\displaystyle:\,\mathrel{\\{\Sigma,A\\}}\mathsf{State}(\Sigma,A)\to\mathsf{tp}^{+}$
$\displaystyle{\Mapsto}$
$\displaystyle:\,\mathrel{\\{\Sigma,A\\}}\mathsf{State}(\Sigma,A)\to\mathsf{State}(\Sigma,A)\to\mathsf{tp}^{+}$

μ[n] =
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}$
(μ,
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{while}}}$[n](m))
⤇(μ,
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ret}}}$${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{\star}}}$)

μ[n] =
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}}$
(μ,
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{while}}}$[n](m))
⤇(μ,
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bnd}}}$(${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{cmd}}}$(m),
$\mathsf{wk}$(${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{while}}}$[n](m))))

Figure 4. Selected rules for the one-step transition of commands of MA; here
$\mathsf{wk}$ denotes weakening of a term.

As an example, we give the rules for
${\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{while}}}$
in Fig. 4. For brevity we have suppressed the definitions of the other
commands; the complete definition may be found in Harper (2012). As usual we
define evaluation of expressions as $e\Downarrow_{\mathsf{exp}}v\coloneqq
e\mapsto^{*}v\times\mathsf{val}(v)$ and evaluation of commands as
$(\mu,m)\Downarrow_{\mathsf{cmd}}(\mu^{\prime},m^{\prime})\coloneqq(\mu,m)\Mapsto^{*}(\mu^{\prime},m^{\prime})\times\mathsf{final}(m^{\prime})$.

####  5.3.1. Phase-separated operational semantics

Similar to the case for STLC, in order to state and prove adequacy, we will
need a phase-separated version of the transition relation for both expressions
and commands where the evaluation cost is _sealed_ by the closed modality:

$\displaystyle{\mapsto_{\P_{\mathsf{E}}}}$
$\displaystyle:\,\mathrel{\\{\Sigma,A\\}}\mathsf{Pg}(\Sigma,A)\to\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}\mathbb{N}\to\mathsf{Pg}(\Sigma,A)\to\mathsf{tp}^{+}$
$\displaystyle{\Mapsto_{\P_{\mathsf{E}}}}$
$\displaystyle:\,\mathrel{\\{\Sigma,A\\}}\mathsf{State}(\Sigma,A)\to\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}\mathbb{N}\to\mathsf{State}(\Sigma,A)\to\mathsf{tp}^{+}$

Using these phase-separated relations we may define phase-separated evaluation
for both expressions and commands as
$e\Downarrow_{\P_{\mathsf{E}}}^{c}v\coloneqq
e\mapsto_{\P_{\mathsf{E}}{}}^{c}v\times\mathsf{val}(v)$ and
$(\mu,m)\Downarrow_{\P_{\mathsf{E}}/\mathsf{cmd}}^{c}(\mu^{\prime},m^{\prime})\coloneqq(\mu,m)\Mapsto_{\P_{\mathsf{E}}}^{c}(\mu^{\prime},m^{\prime})\times\mathsf{final}(m^{\prime})$
respectively. As before, phase-separated evaluation restricts to ordinary
evaluation in the extensional phase:

###### Proposition 5.7.

Given $u:\P_{\mathsf{E}}$ and $c:\mathbb{N}$, we have that
$e\Downarrow_{\P_{\mathsf{E}}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c}v$
is equivalent to $e\Downarrow v$ and that
$(\mu,m)\Downarrow_{\P_{\mathsf{E}}/\mathsf{cmd}}^{\eta_{\mathchoice{\mbox{\normalshape\newmoon}}{\mbox{\normalshape\newmoon}}{\scalebox{0.8}{\normalshape\newmoon}}{\scalebox{0.6}{\normalshape\newmoon}}}c}(\mu^{\prime},m^{\prime})$
is equivalent to $(\mu,m)\Downarrow_{\mathsf{cmd}}(\mu^{\prime},m^{\prime})$.

###  5.4. A denotational model for MA

As mentioned in Section 5.2, our denotational semantics of MA is based on a
possible-worlds model of allocation. Consequently, we interepret (closed)
commands as _families_ of functions that may be executed on any future
semantic store (according the the preorder of signatures). In a language with
higher-order store this definition becomes circular because the interpretation
of signatures depends on _all_ types and so in particular command types;
consequently, more refined techniques such as (abstract) step-indexing
(Birkedal et al., 2011) is required to resolve the circularity of the
definition. Because MA only admits first-order store, we may bootstrap the
definition by first defining the meaning of strictly positive types, which is
independent of the interpretation of signatures (see Fig. 5). The definition
of types is then allowed to reference the meaning of signatures:

$\displaystyle\llbracket-\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}$
$\displaystyle:\mathsf{Ty}^{\textbf{MA}{}}\to\mathsf{Sig}\to\mathsf{tp}^{+}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma)$
$\displaystyle=1$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma)$
$\displaystyle=\mathsf{bool}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma)$
$\displaystyle=\mathbb{N}$ $\displaystyle\llbracket A_{1}\Rightarrow
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma)$
$\displaystyle=\mathsf{U}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle(\Sigma^{\prime}:\mathsf{Con})\to\Sigma^{\prime}\geq\Sigma\to\llbracket
A_{1}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle(\Sigma^{\prime}:\mathsf{Con})\to\Sigma^{\prime}\geq\Sigma\to\llbracket
A_{1}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle(\Sigma^{\prime}:\mathsf{Con})\to\Sigma^{\prime}\geq\Sigma\to\llbracket
A_{1}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle(\Sigma^{\prime}:\mathsf{Con})\to\Sigma^{\prime}\geq\Sigma\to\llbracket
A_{1}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}$}\mathclose{}{)}}$
$\displaystyle\llbracket\mathsf{cmd}(A)\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma)$
$\displaystyle=\mathsf{U}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle(\Sigma^{\prime}:\mathsf{Con})\to\Sigma^{\prime}\geq\Sigma\to\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}\to\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle(\Sigma^{\prime}:\mathsf{Con})\to\Sigma^{\prime}\geq\Sigma\to\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}\to\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle(\Sigma^{\prime}:\mathsf{Con})\to\Sigma^{\prime}\geq\Sigma\to\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}\to\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle(\Sigma^{\prime}:\mathsf{Con})\to\Sigma^{\prime}\geq\Sigma\to\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}\to\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}$}\mathclose{}{)}}$

$\displaystyle\llbracket-\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}^{+}}$
$\displaystyle:\mathsf{Pos}\to\mathsf{tp}^{+}$
$\displaystyle\llbracket({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}},{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{unit}}}/\mathsf{base})\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}^{+}}$
$\displaystyle=1$
$\displaystyle\llbracket({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}},{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bool}}}/\mathsf{base})\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}^{+}}$
$\displaystyle=\mathsf{bool}$
$\displaystyle\llbracket({\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}},{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{nat}}}/\mathsf{base})\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}^{+}}$
$\displaystyle=\mathbb{N}$

$\displaystyle\llbracket-\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$
$\displaystyle:\mathsf{Sig}\to\mathsf{tp}^{+}$
$\displaystyle\llbracket\cdot\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$
$\displaystyle=1$ $\displaystyle\llbracket
A::\Sigma\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$ $\displaystyle=\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}^{+}}\times\llbracket\Sigma\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$

$\displaystyle\llbracket-\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}$
$\displaystyle:\mathsf{Con}\to\mathsf{Sig}\to\mathsf{tp}^{+}$
$\displaystyle\llbracket\cdot\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}(\Sigma)$
$\displaystyle=1$ $\displaystyle\llbracket
A::\Gamma\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}(\Sigma)$
$\displaystyle=\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma)\times\llbracket\Sigma\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}$

Figure 5. Top left: the interpretation of strictly positive types; top right:
interpretation of signatures; bottom: interpretation of contexts.

Similar to the action of preorders at the syntactic level, we may define an
analogous action on the interpretation of types:

###### Proposition 5.8.

There is a map
$\mathsf{up}:\,\mathrel{\\{A,\Sigma^{\prime},\Sigma\\}}\Sigma^{\prime}\geq\Sigma\to\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma)\to\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$.

###### Corollary 5.9.

There is a map
$\mathsf{up}:\,\mathrel{\\{\Gamma,\Sigma^{\prime},\Sigma\\}}\Sigma^{\prime}\geq\Sigma\to\llbracket\Gamma\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}(\Sigma)\to\llbracket\Gamma\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}(\Sigma^{\prime})$.

####  5.4.1. The model

In Figs. 6 and 7 we present the denotational semantics of expression and
commands of MA. The expression-level denotational semantics for MA is defined
in a similar style to Section 3; reified commands are defined using the
mutually recursive interpretation of commands. Commands are defined using a
possible-worlds semantics of first-order store. Observe that both the
interpretation of expressions and commands at a world (_i.e_. signature)
$\Sigma$ are paramterized by a _future world_ $\Sigma^{\prime}\geq\Sigma$.
Consequently commands of a type $A$ are _families_ of _lifted_ transformations
$\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\to\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}$
of semantic stores that also produces a value of type $A$ (at the extended
signature). In contrast, because expressions are total and cannot modify the
store, they are simply interpreted as _free_ computations of the given type.
As in the case for the STLC, we must insert $\mathsf{step}$’s in both the
interpretation of expressions and commands when $\beta$-reductions occur in
the operational semantics.

Here, we highlight the the fact that the while loop of MA is interpreted as a
“while loop” in $\textbf{calf}{}^{\omega}$, a feature typical of synthetic
denotational semantics. As we shall see in Section 5.5, this synthetic
interpretation allows for a somewhat involved but elementary proof of
computational adequacy.

$\displaystyle\llbracket-\rrbracket_{\mathsf{Var}}$
$\displaystyle:\,\mathrel{\\{\Sigma,\Gamma,A\\}}\mathsf{Var}(\Gamma,A)\to\to(\Sigma^{\prime}:\mathsf{Sig})\to\Sigma^{\prime}\geq\Sigma\to\llbracket\Gamma\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}(\Sigma^{\prime})\to\llbracket
A\rrbracket_{\mathsf{Ty}}(\Sigma^{\prime})$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{here}}}\rrbracket_{\mathsf{Var}}(\Sigma^{\prime},p,\gamma^{\prime})$
$\displaystyle=\pi_{1}(\gamma^{\prime})$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{next}}}(v)\rrbracket_{\mathsf{Var}}(\Sigma^{\prime},p,\gamma^{\prime})$
$\displaystyle=(\llbracket
v\rrbracket_{\mathsf{Tm}}(\Sigma^{\prime},p)\circ\pi_{2})\gamma^{\prime}$
$\displaystyle\llbracket-\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}$
$\displaystyle:\,\mathrel{\\{\Sigma,\Gamma,A\\}}\mathsf{Tm}^{\textbf{MA}{}}(\Sigma,\Gamma,A)\to(\Sigma^{\prime}:\mathsf{Sig})\to\Sigma^{\prime}\geq\Sigma\to\llbracket\Gamma\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}(\Sigma^{\prime})\to\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})$}\mathclose{}{)}}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{var}}}(v)\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}$
$\displaystyle=\mathsf{ret}\circ\llbracket v\rrbracket_{\mathsf{Var}}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{tt}}}\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,-)$
$\displaystyle=\mathsf{ret}(\mathsf{tt})$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ff}}}\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,-)$
$\displaystyle=\mathsf{ret}(\mathsf{ff})$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{zero}}}\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,-)$
$\displaystyle=\mathsf{ret}(0)$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{suc}}}\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime})$
$\displaystyle=\mathsf{bind}(\llbracket
e\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime});\lambda
n:\mathbb{N}.\;\mathsf{ret}(n+1))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ifz}}}(e,e_{1},e_{2})\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime})$
$\displaystyle=n\leftarrow\llbracket
e\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime});$
$\displaystyle\mathsf{if}(n,{\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{1}(\llbracket
e_{1}\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime})),\lambda
n^{\prime}.\;{\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{1}(\llbracket
e_{2}\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,(n^{\prime},\gamma^{\prime}))))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{lam}}}(e)\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime})$
$\displaystyle=\mathsf{ret}(\lambda\Sigma^{\prime\prime},p^{\prime},\lambda
a:\llbracket
A_{1}\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime\prime}).\;\llbracket
e\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime\prime},\mathsf{tr}(p^{\prime},p),(a,\mathsf{up}(p^{\prime},\gamma^{\prime}))))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ap}}}(e,e_{1})\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime})$
$\displaystyle=f\leftarrow\llbracket
e\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime});a\leftarrow\llbracket
e_{1}\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma);{\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{1}(f(\Sigma^{\prime},\mathsf{refl},a))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{cmd}}}(m)\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime})$
$\displaystyle=\mathsf{ret}(\lambda\Sigma^{\prime\prime},p^{\prime},(\sigma^{\prime\prime}:\llbracket\Sigma^{\prime\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}).\;\llbracket
m\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(\Sigma^{\prime\prime},\mathsf{tr}(p^{\prime},p),\mathsf{up}(p^{\prime},\gamma^{\prime}),\sigma^{\prime\prime}))$
Figure 6. The interpretation of expressions of MA.
$\displaystyle\llbracket-\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}$
$\displaystyle:\,\mathrel{\\{\Sigma,\Gamma,A\\}}\mathsf{Tm}^{\textbf{MA}{}}(\Sigma,\Gamma,A)\to(\Sigma^{\prime}:\mathsf{Sig})\to\Sigma^{\prime}\geq\Sigma\to$
$\displaystyle\llbracket\Gamma\rrbracket^{\textbf{MA}{}}_{\mathsf{Con}}(\Sigma^{\prime})\to\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}\to\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\llbracket
A\rrbracket^{\textbf{MA}{}}_{\mathsf{Ty}}(\Sigma^{\prime})\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{ret}}}(a)\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(\Sigma^{\prime},p,\gamma^{\prime},\sigma^{\prime})$
$\displaystyle=\mathsf{bind}(\llbracket
a\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime});\lambda
a:\llbracket
A\rrbracket_{\mathsf{Ty}}(\Sigma^{\prime}).\;\mathsf{ret}_{\mathsf{L}}(a,\sigma^{\prime}))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{bnd}}}(e,m)\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(\Sigma^{\prime},p,\gamma^{\prime},\sigma^{\prime})$
$\displaystyle=m_{1}\leftarrow_{\mathsf{L}}\mathsf{lift}(\llbracket
e\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime}));(a,\sigma_{1})\leftarrow_{\mathsf{L}}m_{1}(\Sigma^{\prime},\mathsf{refl},\sigma^{\prime});$
$\displaystyle{\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{1}(\llbracket
m\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(\Sigma^{\prime},p,(a,\gamma^{\prime}),\sigma_{1}))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{while}}}[n](m)\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(\Sigma^{\prime},p,\gamma^{\prime},\sigma^{\prime})$
$\displaystyle=\mathsf{iter}(g)(\sigma^{\prime})\;\textbf{where}$
$\displaystyle g$
$\displaystyle:\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}\to\mathsf{L}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle(1\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}})+\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle(1\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}})+\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle(1\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}})+\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle(1\times\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}})+\llbracket\Sigma^{\prime}\rrbracket^{\textbf{MA}{}}_{\mathsf{Sig}}$}\mathclose{}{)}}$
$\displaystyle g(\sigma)\textbf{ with }\sigma[n]$
$\displaystyle\dots\mid\mathsf{ff}$
$\displaystyle={\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{1}(\mathsf{ret}_{\mathsf{L}}(\mathsf{inl}(\star,\sigma)))$
$\displaystyle\dots\mid\mathsf{tt}$
$\displaystyle=(-,\sigma^{\prime})\leftarrow_{\mathsf{L}}\llbracket
m\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(\Sigma^{\prime},p,\gamma^{\prime},\sigma);{\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{2}(\mathsf{ret}(\mathsf{inr}(\sigma^{\prime})))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{dcl}}}(e,m)\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}\,\mathrel{\\{A=A\\}}(\Sigma^{\prime},p,\gamma^{\prime},\sigma^{\prime})$
$\displaystyle=a\leftarrow_{\mathsf{L}}\mathsf{lift}(\llbracket
e\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime}));$
$\displaystyle(b,(-,\sigma_{1}))$
$\displaystyle\leftarrow_{\mathsf{L}}\llbracket
m\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(A::\Sigma^{\prime},\mathsf{mono}(p),\mathsf{up}(\mathsf{extend}(p),\gamma^{\prime}),(a,\sigma^{\prime}));{\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{1}(\mathsf{ret}_{\mathsf{L}}(b,\sigma_{1}))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{get}}}[n]\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(\Sigma^{\prime},p,\gamma^{\prime},\sigma^{\prime})$
$\displaystyle={\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{1}(\mathsf{ret}_{\mathsf{L}}(\sigma^{\prime}[n],\sigma^{\prime}))$
$\displaystyle\llbracket{\color[rgb]{0.015625,0.4609375,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.015625,0.4609375,0.81640625}{\mathsf{set}}}[n](e)\rrbracket^{\textbf{MA}{}}_{\mathsf{Cmd}}(\gamma,\sigma^{\prime})$
$\displaystyle=a\leftarrow_{\mathsf{lift}}\mathsf{lift}(\llbracket
e\rrbracket^{\textbf{MA}{}}_{\mathsf{Exp}}(\Sigma^{\prime},p,\gamma^{\prime},\sigma^{\prime}));{\color[rgb]{0.0546875,0.33984375,0.2109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.33984375,0.2109375}\mathsf{step}}^{1}(\mathsf{ret}_{\mathsf{L}}(\sigma^{\prime}[n],\sigma^{\prime}[n\mapsto
a]))$ Figure 7. The interpretation of commands of MA.

###  5.5. Computational adequacy

In this section we prove that the denotational semantics of MA defined in