Deciding equivalence with sums and the empty type
Gabriel Scherer
Northeastern University, USA
gabriel.scherer@gmail.com

arXiv:1610.01213v3 [] 8 Nov 2016

Abstract
The logical technique of focusing can be applied to the λ-calculus;
in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide
with βη-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types
and the empty type). This rich structure let us prove the decidability of βη-equivalence in presence of the empty type, the fact that it
coincides with contextual equivalence, and a finite model property.

1.

Introduction

1.1

Notion of equivalences

For a given type system, there may be several notions of program equivalence of interest. One may define a notion of syntactic
equivalence by a system of equations between terms, such as βequivalence and η-equivalence, or their union βη-equivalence. A
more extensional notion of equivalence is contextual or observational equivalence, which checks that the two terms behave in the
same way under all contexts. Finally, a semantic notion of equivalence is given by interpreting terms in a certain mathematical space,
typically morphisms in categories with a certain structure, and considering two terms equivalent if they are equal under all interpretations. One can generally prove that considering all interpretations
in the category of sets suffices to distinguish two observably distinct terms, and certain type systems have the stronger finite model
property that considering all interpretations in finite sets suffices to
distinguish observably distinct terms.
Contextual equivalence has a clear, compact definition, it is the
notion of equivalence that corresponds to programmers’ intuition,
but it is difficult to prove and reason about. Syntactic equivalence
can be used as part of syntactic typing judgments, and may be easier
to prove decidable. Semantic models provide a more abstract point
of view on the identity of programs, and may enable the powerful
method of normalization-by-evaluation.
For the untyped λ-calculus, Böhm (1968) proved that βηequivalence and observational equivalence coincide. Untyped βreduction is not normalizing, so equivalence is undecidable.
For the simply-typed λ-calculus with atomic types, functions
and pairs – what we call the negative fragment – we also know that
these notions of equivalence coincide. Furthermore, typed equivalence is decidable: we can define and compute β-short η-long
normal forms, and two terms are βη-equivalent exactly when they
have the same normal form. Friedman (1975) proved that two terms
equal in all set-theoretic models are equivalent, and Statman (1982)
sharpened the result by proving that finite sets suffice to distinguish
inequivalent terms – the finite model property.
This pleasant setting is quickly eroded by moving to richer
programming languages and type systems. Adding notions of
side-effects, for example, makes the general βη-equivalence unsound. Even in the realm of pure, total programming languages,

adding parametric polymorphism (System F and beyond) makes
βη-equivalence strictly weaker than contextual equivalence.
1.2

Sums and empty type

An interesting middle-ground is the full simply-typed λ-calculus,
with not only atomic types, functions, pairs and the unit type 1 but
also sum types and the empty type 0. There, results on program
equivalence have been surprisingly long to come, because of deep
difficulties caused by mixing functions (negative connectives) and
sums (positive connectives), and the strong behavior of the empty
type: in an inconsistent context, all terms are equal.
The first decidability result for the system with non-empty sums
was Ghani (1995), using advanced rewriting techniques later simplified by Lindley (2007). It was followed by normalization-byevaluation results (Altenkirch, Dybjer, Hofmann, and Scott 2001;
Balat, Di Cosmo, and Fiore 2004) that also established decidability
of equivalence in the non-empty case using the categorical structure introduced in Fiore and Simpson (1999). Decidability in the
presence of the empty type is still open – we propose a proof.
Finally, the only known completeness result for set-theoretic
models is Dougherty and Subrahmanyam (2000); it only holds for
non-empty sums, and relies in an essential way on infinite sets. The
finite model property is only conjectured – we propose a proof,
including in presence of the empty type.
1.3

Focusing

Focusing (Andreoli 1992) is a general technique that uses the notion of invertibility of inference rules to define a focused subset of
any logic that is complete but removes some redundant proofs.
A recent branch of work on maximal multi-focusing (Chaudhuri,
Miller, and Saurin 2008a; Chaudhuri, Hetzl, and Miller 2012) has
demonstrated that focused proofs can be further restricted to become even more canonical: in each application to a specific logic,
the resulting representations are equivalent to existing representations capturing the identity of proofs – proof nets for linear logic,
expansion proofs for classical logic.
Scherer and Rémy (2015) applied focusing to the λ-calculus
with non-empty sums. Completeness of focusing there means that
any term has a βη-equivalent focused term. Their counterpart of
maximal multi-focusing is saturation: saturated terms of the focused λ-calculus introduce and deconstruct neutral terms of sum
type as early as possible – when they are new, they were not derivable in the previous saturation phase. Canonicity of this representation gives yet another decision procedure for βη-equivalence of
λ-terms with non-empty sums.
The present work extends saturated focusing to the full simplytyped lambda calculus, with units and in particular the empty type.
The suitably extended notion of saturated form retains its canonicity properties in the full system. This means that βη-equivalence
with empty types is decidable – by converting terms to their saturated focused form. From two distinct saturated forms, one can
furthermore build a well-typed context that distinguishes them.

This proves that contextual equivalence implies equality of normal forms, and thus βη-equivalence: any term is βη-equivalent
to its normal form, so two terms with the same normal form are
βη-equivalent. Our distinguishing context needs only instantiate
atomic types with finite sets, giving a finite model property.
Extending saturated focusing to the empty type requires adding
a requirement that saturation phases be complete for provability:
not only must they introduce all new neutrals of positive type for
use in the rest of the term, but they must at least introduce one
such neutral for each type deducible in the current context. As
a consequence, we can prove a Saturation Consistency theorem
which is key to our canonicity: if two saturated terms are distinct,
then their context must be consistent.
1.4

Sections 1 to 5, in particular the presentations of focusing and saturated normal forms, correspond to content that
was presented in the thesis manuscript Scherer (2016). In
the present article, definitions and proofs in these sections
are given with minimal amount of details for economy of
space; they are presented in full in the manuscript. In contrast, Section 6, which presents the key canonicity result enabling the contributions of this article, is entirely new, and
presented in more detail.

Contributions

We establish the following results in the simply-typed λ-calculus
with atoms, functions, pairs, the unit type, sums and the empty type
ΛC(X, →, ×, 1, +, 0):
• Saturated terms provide a notion of quasi-normal form; equiva-

lent quasi-normal forms are not necessarily α-equivalent, but
are related by a local, easily decidable relation of invertible
commutation conversions (≈icc ).
• βη-equivalence is decidable.
• βη-equivalence and contextual equivalence coincide, along

with set-theoretic equivalence in all models where atomic types
are interpreted by closed types.
• The finite model property holds – as closed types in this system

have finitely many inhabitants.
Our notion of βη-equivalence is the strong equivalence on sums.
It corresponds to equality of morphisms in the free bi-cartesian
closed category – see Scherer (2016), Section 3.2.2.
1.5

one of them equal to true and the other to false. By contraposition, this proves that two terms contextually equivalent in all models have the same saturated normal forms – giving decidability –
and in particular are βη-equivalent.
For lack of space, our statements do not come with their proofs,
but proof outlines are given in Appendix B (Proof outlines).

Plan

Section 2 (Equivalences in the full λ-calculus) introduces the full
λ-calculus we shall consider in this work, along with the various
notions of equivalence (βη, contextual, set-theoretic) we will discuss. We prove some elementary results: βη-equivalence implies
contextual equivalence in all closed models, which coincides with
set-theoretic equivalence in all closed models.
Section 3 (Focusing) presents focusing, before detailing the
focused λ-calculus extended with the unit type and empty type.
We formulate the computational counterpart of the completeness
theorem: any λ-term has a βη-equivalent focused term.
Section 4 (Saturated focused λ-calculus) presents the saturated
subset of the focused λ-calculus as defined by a different system
of inference rules. Compared to the simpler system of Scherer and
Rémy (2015), this saturated system is parametrized over a selection
function that selects the neutrals to split over during saturation. The
saturated system is, again, computationally complete with respect
to focused terms.
Section 5 (Saturation consistency) establishes the main metatheoretic property of saturated terms in presence of the empty
type, namely that saturating an inconsistent context will always
find a proof of 0. In other words, if two saturated terms differ
after a saturation phase instead of both ending on an absurdity
elimination, we know that they differ in consistent contexts. This
result is key to extending the distinguishability result of Dougherty
and Subrahmanyam (2000) to a system with empty types.
Finally, Section 6 (Canonicity) establishes the central result of
this work: if two saturated λ-terms t 
≈icc u are syntactically distinct (modulo invertible commuting conversions), then there exists
a closed type model M in which we have a distinguishing context C [] such C [M(t)], C [M(u)] are closed booleans (1 + 1),

2.

Equivalences in the full λ-calculus

2.1

Typing rules and βη-equivalence

Figure 1. Full simply-typed lambda-calculus ΛC(X, →, ×, 1, +, 0)
A, B, C ::= X, Y , Z | A → B | A1 × A2 | 1 | A1 + A2 | 0
t, u, r ::=

x, y, z | λx. t | t u | (t1 , t2 ) | πi t | ()
| σi t | match t with (σi xi → ui )i | absurd(t)
Γ`t:A→B
Γ`u:A
Γ`tu:B

Γ, x : A ` t : B
Γ ` λx. t : A → B

Γ ` t : A1 × A2
Γ ` πi t : Ai

Γ`t:A
Γ`u:B
Γ ` (t, u) : A × B
Γ ` t : Ai
Γ ` σ i t : A1 + A2

Γ ` () : 1

Γ ` t : A1 + A2

(Γ, xi : Ai ` ui : C)i

Γ ` match t with (σi xi → ui )i : C

Γ, x : A ` x : A

Γ`t:0
Γ ` absurd(t) : A

Figure 2. βη-equivalence for ΛC(X, →, ×, 1, +, 0)
(λx. t) u .β t[u/x]
πi (t1 , t2 ) .β ti

(t : A → B) .η λ(x : A). t x
(t : A1 × A2 ) .η (π1 t, π2 t)

match σj t with (σi xi → ui )i .β uj [t/xj ]
t[u : A1 + A2 /x] .η match u with (σi y i → t[σi y i /x])i
Γ`t:1
Γ ` t .η () : 1
Derived rules:

Γ`u:0
Γ, x : 0 ` t : A
Γ ` t[u/x] .η absurd(u) : A

Γ ` t1 ≈η t2 : 1

Γ`u:0
Γ ` t1 ≈η t2 : A

Figure 1 gives the grammar and typing rules for the full simplytyped λ-calculus ΛC(X, →, ×, 1, +, 0). By symmetry with the
pair projections πi t, we use σi t for sum injection. We use
(. . . )i∈I for a family of objects indexed by i ∈ I. The common
indexing family, when dealing with syntactic binary operations,
is {1, 2}, and we will most of the time leave it implicit. Finally,
match t with (σi xi → ui )i is a compact syntax for our full sumelimination syntax, (match t with | σ1 x1 → u1 | σ2 x2 → u2 ).

Definition 1. A closed type does not contain atomic types.1
Definition 2. We write Γ ` A when t exists such that Γ ` t : A.
We define βη-equivalence as the smallest congruent relation
(≈βη ) closed by the union of the β-reduction relation (.β ) and
the η-expansion relation (.η ) of Figure 2. We have not explicited
the full typing assumptions, but only type-preserving rewrites are
considered. The derived rules are not primitives, they are derivable
from η-expansion at unit and empty type.
If t1 , t2 are of type 1, then they both rewrite to () and are thus
equal. The derivation for equality under absurdity is less direct:
if the current typing context Γ is inconsistent, that is there is a
derivation (u : 0), then any term of any type (t : A) can be seen
as the result of the substitution t[u/x] for a variable x that does not
appear in t, and is thus equal to absurd(u); in particular, any two
terms of the same type are equal.
Theorem 1 (Strong normalization). β-reduction is strongly normalizing in the full simply-typed λ-calculus ΛC(X, →, ×, 1, +, 0).
Theorem 2 (Confluence). β-reduction is confluent for the full
simply-typed λ-calculus ΛC(X, →, ×, 1, +, 0): each term has a
unique β-short normal form.
Lemma 1 (Inversion). A closed β-normal form (in an empty context) starts with an introduction form.
2.2

Contextual equivalence

A common definition of contextual equivalence, for System F for
example, is that two terms Γ ` t, u : A are contextually equivalent if there exists no separating context ∅ ` C [Γ `  : A] : 1 + 1
such that C [t] ≈β σ1 () and C [u] ≈β σ2 (). For a trivdef
def
ial example, if Γ = (x : 1 + 1, y : 1 + 1) , then C [] =
(λx. λy. ) (σ1 ()) (σ2 ()) separates x and y.
This definition is too weak in presence of atomic types. Condef
sider the context Γ = (x : X, y : X) and the terms Γ ` x, y : X.
We want a definition of contextual equivalence that declares these
terms inequivalent, but there is no distinguishing context in the
sense above as we have no information on X, and thus no way
to provide distinct values for x and y. The variables x and y could
be distinct depending on what is the unknown type represented by
the abstract type X.
Definition 3. A model M is a mapping from atomic types to closed
types.
If x is some syntactic object containing types, we write M(x)
for the result of replacing each atomic type in x by its image
in the model M. If Γ ` t : A holds, then it is also the case that
M(Γ) ` t : M(A) holds; we may write the term M(t) as well, to
emphasize that we look at its typing in the model.
Definition 4. If Γ ` t, u : A and for a given model M, we say that
t and u are contextually equivalent in M, written t ≈ctx(M) u, if
∀C, ∅ ` C [M(Γ) `  : M(A)] : 1 + 1 ⇒ C [M(t)] ≈β C [M(u)]

We say that t and u are contextually equivalent, written t ≈ctx u,
if they are contextually equivalent in all models.
2.3

Semantic equivalence

Definition 5 (Semantics of types). For a closed type A we define
the set of semantic values of A, written JA K, by induction on A as
1A

reviewer remarks that the terminology “atomic type” is awkward; if
“atom” means “indecomposable”, then unit types 1, 0 could arguably be
considered atomic. In retrospect, we agree that “type variable”, as naturally
used in polymorphic type systems, would be a better terminology, and plan
to use it in the future.

follows:
JA → B K
JA × B K
J1 K
JA + B K
J0 K

def

=
=
def
=
def
=
def
=
def

total functions from JA K to JB K
{(v, w) | v ∈ JA K, w ∈ JB K}
{?}
{(1, v) | v ∈ JA K} ] {(2, w) | w ∈ JB K}
∅

For an arbitrary type A we write JA KM for JM(A) K.

We remark that JA KM is always a finite type, whose elements
can be enumerated. It is thus decidable whether two elements of
JA KM are equal as mathematical objects; at function types, one
compares two functions pointwise on their finite domain.
Definition 6 (Semantics of environments). For a closed typing environment Γ, we define the set JΓ K of semantic valuations, functions from the domain of Γ to semantic values such that:
def

JΓ K

=

{G | ∀x : A ∈ Γ,

We write JΓ KM for JM(Γ) K.

G(x) ∈ JA K}

Definition 7 (Semantics of typing judgments). We write JΓ ` A K
for the set of functions from semantic valuations of Γ to semantic
def
values in A: JΓ ` A K = JΓ K → JA K . We write JΓ ` A KM for
JM(Γ) ` M(A) K.

Definition 8 (Semantics of terms). For a term Γ ` t : A in a judgment with closed types, we write Jt K for the set-theoretic semantics
of t, as an object of JΓ ` A K. The (natural) definition is given in
full in Appendix A (Semantics of terms), but for example
def

Jλx. t K(G) = (v 7→ Jt K(G, x 7→ v))

We write Jt KM for JM(t) K.

Definition 9 (Semantic equivalence). For any terms Γ ` t, u : A
and model M, we say that t and u are semantically equivalent in
M, written t ≈sem(M) u, if their semantics are (pointwise) equal.
def

t ≈sem(M) u = (∀G ∈ JΓ KM , Jt KM (G) = Ju KM (G) ∈ JA KM )

We say that t and u are semantically equivalent, written t ≈sem u,
if they are semantically equivalent in all models M.
2.4

Easy relations between equivalences

Theorem 3 (βη is semantically sound). If t ≈βη u then t ≈sem u.
Theorem 4 (Semantic equivalence implies contextual equivalence). If t ≈sem u then t ≈ctx u.
On models using closed types (Long version) Our definition of a
model M allows to instantiate atomic types with any closed type;
this instantiation happens in the world of syntax, before we interpret types as sets. It is more common, when giving set-theoretic semantics, to instantiate atoms only in the semantics, defining models
as mapping from atomic types to arbitrary sets.
We are fortunate that our grammar of closed types is expressive
enough to describe any finite set; if we did not have units (1 and
0), for example, we could not do this. Our more syntactic notion of
model can be shared by our definition of contextual and semantic
equivalence, which is very pleasing.
Note that, as a consequence, the finite model property is sort
of built into our definition of the semantic and contextual equivalences: we may only distinguish atoms by instantiating them with
finite sets, not arbitrary sets. One may wonder, then, whether a notion of semantic equivalence that allows to instantiate atoms with
infinite sets would behave differently – did we really prove the finite
model property, or just enforce it by stifling our notion of equivalence?

The coincidence of the finite and infinite interpretations is a
consequence of the later results of this work on the coincidence
of semantic and β-equivalence. If we added the ability to instantiate atoms by infinite sets, we would distinguish more: we could
not prove more terms equal, but would only prove more terms different. But any pair of terms equal in the finite-set semantics is
βη-equivalent, and Theorem 3 (βη is semantically sound) seamlessly extends to infinite sets – those terms must still be equal in an
infinite-set semantics.

Theorem 5 (Reification). For each semantic value v in JA K we
can define a closed term reify(v) such that Jreify(v) K = v.

2.5 Fun-less types and reification
To prove that contextual equivalence implies semantic equivalence,
we build a reification procedure reifyM (v) that goes from JA KM
to closed terms in M(A) and satisfies the following properties:

Theorem 6 (Contextual equivalence implies semantic equivalence). If t ≈ctx u then t ≈sem u.

∀v, JreifyM (v) KM = v

∀(∅ ` t : A), reifyM (Jt KM ) ≈βη t

This is difficult in the general case, as it corresponds to a
normalization-by-evaluation procedure – when you can furthermore prove that reifyM (v) is always a normal term. The reification of finite sums and products is straightforward, but function
types are delicate; intuitively, to reify a function one builds a decision tree on its input, which requires an enumeration procedure for
the input type (Altenkirch and Uustalu 2004) which may itself be a
function, etc.
In the present case, however, the fact that we work with closed
types (no atoms) enables a useful hack: we can eliminate function types by rewriting them in isomorphic types expressed in
ΛC(×, 1, +, 0) only. This was inspired by an idea of Danko Ilik
(see for example Ilik (2015)), which removes sum types rather than
function types. In presence of atomic or infinite types, neither sum
nor function types can be fully removed. In absence of atoms, function types can be fully removed, but sum types cannot – there is no
type isomorphic to 1 + 1 in ΛC(→, ×, 1).
Figure 3 (Fun-less data types) defines the fun-less bAc for each
closed type A. Its definition is structurally recursive, and uses an
auxiliary definition TA → BU that takes a function type whose
left-hand side A is fun-less, and is structurally recursive on this
left-hand side. We also define pair of transformations b cA from
A to bAc and d eA from bAc to A, on both terms and semantic
values. On semantic values they are inverse; on terms they are
inverse modulo βη-equivalence. The (natural) definitions are given
in full in Appendix A (Fun-less types and reification). It uses
auxiliary definitions T UA→B and V WA→B , and has for example
def
def
bvcA→B = Tw 7→ bv(dweA )cB UA→B and TtUA1 ×A2 →B =
Tλx1 . Tλx2 . t (x1 , x2 )UA2 →B UA1 →(A2 →B) .
Finally, we also have that the isomorphisms on semantic values
and ground terms commute.
Figure 3. Fun-less data types
def

def

bA → Bc = TbAc → bBcU
def

bA1 × A2 c = bA1 c × bA2 c
def

b1c = 1

bA1 + A2 c = bA1 c + bA2 c
def

T(A1 × A2 ) → CU
T1 → BU

def

T(A1 + A2 ) → BU
T0 → BU

def

∀v, dbvcA eA = v
∀t,

=

=

def

=

=

def

b0c = 0

TA1 → TA2 → CUU

B

TA1 → BU × TA2 → BU

1

∀t, dbtcA eA ≈βη t

bJt KcA = JbtcA K ∧ dJt KeA = JdteA K

Theorem 5 (Reification) establishes that semantic inhabitation
and provability coincide at closed types.

Corollary 1 (Inhabited or inconsistent). For Γ, A closed, if Γ ` A
then either ∅ ` A or Γ ` 0.
Lemma 2. For any closed term of closed type ∅ ` t : A we have
reify(Jt K) ≈βη t.

3.

Focusing

Consider the usual description of β-normal forms in the purely negative fragment of the simply-typed λ-calculus, ΛC(X, →, ×, 1).
values
neutrals

t
n

::=
::=

λx. t | (t1 , t2 ) | () | n
n t | πi n | x

Values, the story goes, are a sequence of constructors applied to a
neutral, which is a sequence of destructors applied to a variable. It
is even possible and easy to capture the set of β-short η-long normal
forms by adding a typing restriction to this grammar, asking for the
first neutral term n found in a value to be of atomic type (n : X).
Unfortunately, adding sum types to this picture shatters it irreparably. If σi is a constructor, it should go in values, and
match with . . . is a destructor, it should be a neutral term former. Adding σi t to the grammar of values seems innocuous, but
adding match to neutrals raises a question: should we ask the
branches to be neutrals match n with (σi xi → ni )i or values
match n with (σi xi → ti )i ? Neither choices work very well.
Asking branches to be neutrals means that the term
x : X + Y ` (match x with | σ1 y → σ2 y | σ2 y → σ1 y) : Y + X

is not a valid normal form, and in fact has no valid normal form!
We cannot force all constructors to occur outside branches, as in
this example we fundamentally need to choose a different constructor in each branch – committing to either σ1 or σ2 before matching on x would make us stuck, unable to complete our
attempt with a well-formed term.
On the other hand, letting branches be any value introduces
normal forms that really should not be normal forms, such as
π1 (match x with (σi y i → (n, y i ))i ), clearly equivalent, for any
value of x, to the neutral n.
The solution to this problem comes from logic. Logicians remark that some inference rules are invertible and some are noninvertible. A rule is invertible when, used during goal-directed
proof search, it preserves provability: if the conclusion was provable (maybe using another rule), then applying this rule results in
premises that are also provable. For example, consider the implication and disjunction introduction rules:
Γ, A ` B
Γ`A→B

Γ ` Ai
Γ ` A1 + A2

Implication introduction is invertible – this can be proved by inverting the rule, showing a derivation of Γ, A ` B with open
premise Γ ` A → B. Disjunction introduction is not: if one decides to prove, say, A1 , one may get stuck while having chosen to
prove A2 would have worked. Or maybe one needs to delay this
choice until some hypothesis of the contexts is explored – which is
the heart of our X + Y ` Y + X example.
Andreoli’s focusing (Andreoli 1992) is a technique to restrict a
logic, make its proof term more canonical, by imposing additional
restrictions based on the invertibility of rules. One easy restriction
is that invertible rules, when they can be applied to a judgment,
should be applied as early as possible. The more interesting restriction is that when one starts applying non-invertible rules, focusing

forces us to apply them as long as possible, as long as the formula
introduced in premises remain at a type where a non-invertible rule
exists. For a complete reference on focusing in intuitionistic logic,
see Liang and Miller (2007).
In programming terms, the fact that the right implication rule is
invertible corresponds to an inversion principle on values: without
loss of generality, one can consider that any value of type A → B
is of the form λx. t. Any value of type A1 × A2 is of the form
(t1 , t2 ). This is strictly true for closed values in the empty context,
but it is true modulo equivalence even in non-empty contexts, as is
witnessed by the η-expansion principles. If a value (t : A → B) is
not a λ-abstraction, we can consider the equivalent term λx. t x.
But it is not the case that any value of type A + B is of the form
σi t, as our example X + Y ` Y + X demonstrated. Inspired by
focusing we look back at our grammar of βη-normal forms: it is
not about constructors and destructors, it is about term-formers that
correspond to invertible rules and those that do not. To gracefully
insert sums into this picture, the non-invertible σi should go
into the neutrals, and case-splitting should be a value. Scherer and
Rémy (2015) introduce focusing in more details, and present a
grammar of focused normal forms is, lightly rephrased, as follows:
values

t

choice terms
negative neutrals
positive neutrals

f
n
p

::= λx. t | (t1 , t2 ) | () | f
| match x with (σi y i → ti )i
::= (n : X) | let x : A + B = n in t | p
::= n p | πi n | x
::= σi p | (t : N )

The type N on the last line denotes a negative type, defined as
a type whose head connective has an invertible right-introduction
rule: A → B or A × B or 1. This means that if the argument of an
injection σi is itself of sum type, it must be of the form σj as
well; this enforces the focusing restriction that non-invertible rules
are applied as long as the type allows.
It is interesting to compare this grammar to bidirectional type
systems – when used to understand canonical forms rather than
for type inference. Focusing generalizes the idea that some parts
of the term structure (constructors) are canonically determined by
type information, while some parts (neutrals) are not. It generalizes
bidirectional typing by taking the typing environment into account
as well as the goal type (variables of sum type are split during
the inversion phase), and refines the application syntax n t into the
sharper n p where both sub-terms have a neutral spine.
Our work builds on this focused representation, easily extended
with an empty type 0. Our presentation of the type system is different, farther away from the standard λ-calculi and closer to recent presentation of focused systems, by using polarized syntax for
types with explicit shifts – it clarifies the structure of focused systems. Instead of distinguishing positive and negative types based on
their head connectives, we define two disjoint syntactic categories
P and N , with explicit embeddings hN i+ , hP i− to go from one
to the other. In particular, atoms are split in two groups, the positive atoms of the form X + and the negative atoms X − – there is a
global mapping from atoms X to polarities, a given atom is either
always positive or always negative. Sometimes we need to consider
either types of a given polarity or atoms of any polarity; we use P a
for positive types or negative atoms, and N a for negative types of
positive atoms.
We present this focused λ-calculus in Figure 4 (Cut-free focused λ-terms). The focusing discipline is enforced by the inference rules which alternate between four different judgments:
• The invertible judgment Γna ; Σp `inv t : N | Qa corresponds

to invertible phases in focused proof search. Γna is a typing
environment mapping variables to negative types N or positive
atoms X + . Σp contains only positive types; it is the part of the
context that must be decomposed by invertible rules before the
end of the phase. The two positions N | Qa in the goal are either
formulas or empty (∅), and exactly one of them is non-empty in

any valid judgment. If the goal is a negative formula N , it has
yet to be introduced by invertible rules during this phase; once
it becomes atomic or positive it moves to the other position Qa .
• The negative focus judgment Γna ` n ⇓ N corresponds to

a non-invertible phase focused on a (negative) formula in the
context.
• The positive focus judgment Γna ` p ⇑ P corresponds to a non-

invertible phase focused on a (positive) formula in the goal.
• The choice-of-focusing judgment Γna `foc f : P a corre-

sponds to the moment of the proof search (reading from the
conclusion to the premises) where the invertible phase is finished, but no choice of focus has been made yet. Focusing on
the goal on the right uses a positive neutral to prove a positive type – FOCLC - CONCL - POS. Focusing on the left uses a
negative neutral. If the neutral has a positive type, it is letbound to a variable and the proof continue with an invertible phase – FOCLC - LET- POS. If it has a negative atomic type,
then it must be equal to the goal type and the proof is done –
FOCLC - CONCL - NEG .
The notation h i+
a takes a negative-or-atomic type N a and returns a positive type. It is used in the rule FOCLC - INV- FOC that concludes an invertible phase and starts the choice-of-focusing phase.
It may only be applied when the positive context Σp is of the form
+
hΓ0na ia for some Γ0na , that is, when it only contains negative or
atomic formulas – it has been fully decomposed.
Notice that the sum-elimination rule in the invertible judgment
eliminates a variable x, and not an arbitrary term, and re-introduces
variables with the same name x, shadowing the previous hypothesis
of sum type: there is no need to refer to it anymore as we learned
its value. This cute trick is not fundamental for a focused calculus,
but it corresponds to the intuition of the corresponding sequentcalculus rule, and let us actually remove positive types from the
context to have a negative-or-atomic context at the end of the phase.
For any judgment, for example Γna ` p ⇑ P , we use the version
without a term position, for example Γna ⇑ P , as the proposition
that there exists a well-typed term: ∃p, Γna ` p ⇑ P . This is also
an invitation to think of the derivation as a logic proof rather than a
typed program.
Our focused terms are cut-free in the sense that they contain no β-redexes, even modulo commuting conversions. The rule
FOCLC - LET- POS does look like a cut, proving Γna `foc Qa from
Γna ` n ⇓ hP i− and Γna ; x : P `inv t : ∅ | Qa , but notice
that substituting the negative neutral n inside the invertible proof
t would not create a β-redex: we know that x is matched over
during the invertible phase, but n cannot start with a constructor so match n with . . . cannot reduce. If you are interested in
focused systems that do have cuts and interesting dynamic semantics, then the abstract machine calculi of Curien, Fiore, and
Munch-Maccagnoni (2016) are a better starting point.
3.1

(Non-)canonicity

When we look at the purely negative fragment of our calculus
ΛC(X − , →, ×, 1), we can prove that the focused λ-terms correspond exactly to the usual notion of β-short η-long normal
forms. For example, consider the valid terms for the judgment
−
−
+
x : Y + → Z−
→ Z−
1 × Z 2 ; ∅ `inv ? : Y
1 × Z 2 | ∅ . Neither x nor λy. x y, that would be well-typed for the corresponding
un-focused judgment, are valid according to our inference rules.
There is exactly one valid derivation in our system, for the term
λy. (π1 (x y), π2 (x y)) which is the η-long normal form of x at
this type.
A consequence of this result is that the focused λ-calculus is
canonical for the purely negative fragment (or, in fact, the purely

Figure 4. Cut-free focused λ-terms
N , M ::= X − , Y − , Z − | P → N | N 1 × N 2 | 1 | hP i−
P , Q ::= X + , Y + , Z + | P 1 + P 2 | 0 | hN i+

negative types
positive types

P a , Qa ::= P , Q | X − , Y −

N a , M a ::= N , M | X + , Y +

t, u, r ::= λx. t | () | (t1 , t2 ) | (f : P )
| absurd(x) | match x with (σi x → ti )i
f , g ::= let (x : P ) = n in t | (n : X − ) | p
n, m ::= (x : N ) | n p | πi n
p, q ::= σi p | (x : X + )

invertible terms
focusing terms
negative neutrals
positive neutrals

Γna ; Σp , x : P `inv t : N | ∅
Γna ; Σp `inv λx. t : P → N | ∅

proximation of the idea of normal form, as it is easily decidable.
Indeed, while in general commuting conversions may relate very
different terms, they can be easily decided inside a single invertible
phase, for example by imposing a fixed ordering on invertible rules.
By definition of invertibility, any ordering preserves completeness.
The other more fundamental source of non-canonicity is that
two non-invertible phases may be independent from each other, and
thus be ordered in several possible ways, giving distinct but equivalent terms. For example, let x1 = n1 in let x2 = n2 in (x1 , x2 )
and let x2 = n2 in let x1 = n1 in (x1 , x2 ) are equivalent at
type X − × Y − if x1 ∈
/ n2 , x2 ∈
/ n1 . This source of redundancy is
non-local – the permutable let-bindings may be miles away inside
the term. It requires a global approach to recover canonicity, which
we discuss in Section 4 (Saturated focused λ-calculus).
3.2

(Γna ; Σp `inv ti : N i | ∅)i
Γna ; Σp `inv (t1 , t2 ) : N 1 × N 2 | ∅
(Γna ; Σp , x : Qi `inv ti : N | P a )i
Γna ; Σp , x : Q1 + Q2 `inv match x with (σi x → ti )i : N | P a
Γna ; Σp , x : 0 `inv absurd(x) : N | P a
FOCLC - INV- FOC

FOCLC - CONCL - POS

Γna , Γ0na `foc f : (P a | Qa )

Γna ;

+
Γ0na a

`inv f :

FOCLC - CONCL - NEG

Γna ` n ⇓ X −

Γna `foc n : X

−

hP a i−
a

Γna ; Σp `inv () : 1 | ∅
Γna ` p ⇑ P
Γna `foc p : P

| Qa

We can define a depolarization operation b c± that takes polarized
types and erases polarity information. The definition is given in
full in Appendix A (Depolarization), but for example we have
 −  def

 def
def
X ± = X, bP → N c± = bP c± → bN c± , and hN i+ ± =
bN c± .
This erasure operation can be extended to a defocusing operation b cfoc on focused terms that preserves typing modulo depolarization. For example, if Γna ; Σp `inv t : N | Qa holds, then in the
un-focused system bΓna c± , bΣp c± ` btcfoc : (bN c± | bQa c± )
def

FOCLC - LET- POS

Γna ` n ⇓ hP i−
Γna ; x : P `inv t : ∅ | Qa
Γna `foc let x = n in t : Qa
Γna , x : X + ` x ⇑ X +

Γna , x : N ` x ⇓ N

Computational completeness

holds – with (A | ∅) = A and conversely. This operation is defined
on terms as a direct mapping on all λ-term formers, except the letdefinition form which does not exist in the unfocused calculus and
def
is substituted away: blet x = n in tcfoc = btcfoc [bncfoc /x].
Going from a focused system to a system with less restrictions
is easy. The more interesting statement is the converse, that for any
un-focused term t there exists an equivalent focused term t0 .
Theorem 7 (Completeness of focusing).

Γna ; ∅ `inv t : N | ∅

Γna ` n ⇓ N 1 × N 2
Γna ` πi n ⇓ N i

bΓna c± , bΣp c± ` t : (bN c± | bQa c± )

Γna ` t ⇑ hN i+
=⇒

Γna ` n ⇓ P → N
Γna ` p ⇑ P
Γna ` n p ⇓ N

Γna
def

shift-or-atom notations

+
hN i+
a = hN i
def
hP i−
a =

hP i−

Γna ` p ⇑ P i
` σi p ⇑ P 1 + P 2
+ def
=
a
− def
X− a =

X+

X+
X−

Definition 10. We define the equivalence relation (≈icc ) as allowing well-typed permutations of two adjacent invertible rules. For
example we have absurd(x) ≈icc λy. absurd(x).
From now on any notion of normal form being discussed should
be understood as a quasi-normal form, a normal form modulo invertible commuting conversions (≈icc ). This is a reasonable ap-

 0
t foc ≈βη t

∧

Γna ; Σp `inv t0 : N | Qa

Proof. Completeness of focusing is a non-trivial result, but it is independent to the contributions of the current work, and in particular
extends gracefully to the presence of an empty type. See for example proofs in Liang and Miller (2007); Ahmad, Licata, and Harper
(2010); Simmons (2011).
3.3

positive fragment): if we have Γn ; ∅ `inv t, u : N | X − with
t 6=α u, then t 
≈βη u and t 
≈ctx u – these are known to be
equivalent in the negative fragment.
Focusing is not canonical anymore in mixed-polarity settings.
The first source of non-canonicity is that there may a free choice
of ordering of invertible rules in a phase; consider the judgment
Γna ; x : P 1 + P 2 `inv ? : Q → N | ∅ for example, one may
either do a case-split on P 1 + P 2 or introduce a λ-abstraction
for the function type Q → N : match x with (σi x → λy. ?i )i or
λy. match x with (σi x → ?i )i are both valid term prefixes. This
is solved by declaring that we do not care about the ordering of
invertible rules within a single phase.

∃t0 ,

Choices of polarization

We mentioned that a given un-polarized atom X must either appear
always positively X + or always negatively X − in our judgments.
Violating this restriction would break completeness, as for example
X + ` X − is not provable – they are considered distinct atoms. But
the global choice of polarization of each atom is completely free:
completeness holds whatever choice is made. Those choices influence the operational behavior of proof search: Chaudhuri, Pfenning, and Price (2008b) shows that using the negative polarization
for all atoms corresponds to backward proof search, whereas using
the positive polarization corresponds to forward proof search.
Similarly, there is some leeway in insertion of the
D polarity
E shifts
−

+

h i+ and h i− ; for example, 0 + X + and 0 + X +
depolarize to the same formula, but admit fairly different terms –
the double-shifting allows an invertible phase to start right after
(σ2 ). When transforming a non-polarized type into a polarized
type, two strategies for inserting shifts are notable. One is to insert
as few shifts as possible; the terms inhabiting the minimally-shifted
judgment are in one-to-one correspondence with terms of the unfocused system that “respect the focusing restriction”. The other is

to insert double-shifts under each connective; the terms inhabiting
these double-shifted judgments are in one-to-one correspondence
with unfocused sequent terms – Zeilberger (2013) relates this to
double-negation translations from classical to intuitionistic logic.

4.

Saturated focused λ-calculus

In Section 3.1 ((Non-)canonicity) we explained that the essential
source of non-canonicity in focused term systems is that distinct
non-invertible phases may be independent from each other: reordering them gives syntactically distinct terms that are observably
equivalent in a pure calculus. Being such a reordering of another
term is a highly global property, that cannot be decided locally like
invertible commuting conversions.
Logicians introduced maximal multi-focusing (Chaudhuri, Miller,
and Saurin 2008a) to quotient over those reorderings, and Scherer
and Rémy (2015) expressed this in a programming setting as saturation. The idea of maximal multi-focusing is to force each noninvertible phase to happen as early as possible in a term, in parallel,
removing the potential for reordering them. However, in general
there is no goal-directed proof search (or term enumeration) procedure that generates only maximally multi-focused derivations,
as one cannot guess in advance what non-invertible phases will be
useful in the rest of the term – to introduce them as early as possible. Saturation is a technique specific to intuitionistic logic: when
a non-invertible phase starts, instead of trying to guess which noninvertible phases would be useful later, one saturates the context
by performing all the possible left-focused phases, let-binding all
the neutrals that might be used in the rest of the term. One can
think of a neutral of positive type (n : P ) as an observation of the
current environment: we are saturating by performing all possible observations before making a choice – a right focusing phase.
Note this strategy would be invalid in an effectful language, or
a resource-aware logic where introducing unused sub-derivations
can consume necessary resources and get you stuck.
In general there may be infinitely many distinct observations
that can be made in a saturation phase – consider the context
−
(z : X + , s : X + → X + ), and a type system that would enforce complete saturation would then have to admit infinite terms.
Instead, Scherer and Rémy (2015) relax the definition of saturation
by allowing saturation phases to introduce only a finite subset of
deducible neutrals (n : P ). They prove that canonicity holds (in a
system without the empty type) in the following sense: if two saturated terms made the same saturation choices, then they are equivalent if and only if they are syntactically the same – modulo (≈icc ).
In their work, the notion of equivalence is βη-equivalence of the
defocused forms.
4.1

Figure 5. Cut-free saturated focused type system
Γna ; Σp , x : P `sinv t : N | ∅
Γna ; Σp `sinv λx. t : P → N | ∅
Γna ; Σp `sinv () : 1 | ∅

(Γna ; Σp `sinv ti : N i | ∅)i
Γna ; Σp `sinv (t1 , t2 ) : N 1 × N 2 | ∅

Γna ; Σp , x : 0 `sinv absurd(x) : N | Qa

(Γna ; Σp , x : P i `sinv ti : N | Qa )i
Γna ; Σp , x : P 1 + P 2 `sinv match x with (σi x → ti )i : N | Qa
SINV- SAT

Γna ; Γ0na `sat f : (P a | Qa )

Γna ; Γ0na

+
a

`sinv f : hP a i−
a | Qa

SAT



def
(Γna , Γ0na `s n ⇓ hP i− )
)
(n̄, P̄ ) = SelectΓna ,Γ0na ( (n, P ) |
0
∧ ∃x ∈ Γna , x ∈ n
Γna , Γ0na ; x̄ : P̄ `sinv t : ∅ | Qa
Γna ; Γ0na `sat let x̄ = n̄ in t : Qa
SAT- UP

SAT- DOWN

Γna `s p ⇑ P
Γna ; ∅ `sat p : P

Γna ; ∅ `sat n : X −

Γna `s n ⇓ X −

Γna ; ∅ `sinv t : N | ∅
Γna `s t ⇑ hN i+

Γna , x : X + `s x ⇑ X +

Γna `s n ⇓ N 1 × N 2
Γna `s πi n ⇓ N i

Γna , x : N `s x ⇓ N

Γna `s p ⇑ P i
Γna `s σi p ⇑ P 1 + P 2

Γna `s n ⇓ P → N
Γna `s p ⇑ P
Γna `s n p ⇓ N

context ∅, allowing saturation to proceed to prove the goal with one
of the two other choice-of-focusing rules.
This aspect of the saturation judgment is reused, unchanged,
from Scherer and Rémy (2015). On the other hand, the formulation of the saturation rule SAT is different. We pass the (potentially
infinite) set S of new introducible neutrals to a selection function
SelectΓna (S), which returns a finite subset of neutrals to introduce in a given context. SelectΓna (S) may not return any subset,
we give the requirement for a selection function to be valid in Section 4.3 (Selection function).
The notation let x̄ = n̄ in t denotes simultaneous binding of a
(finite) set of neutral terms – our notion of syntactic α-equivalence
is considered to test the (decidable) set equality.

The saturated type system

The saturated type system is given in Figure 5 (Cut-free saturated
focused type system). The neutral judgments are identical to the
focused type system of Figure 4 (Cut-free focused λ-terms), and
most of the invertible rules are also identical. The only change
is that the rule SINV- SAT moving from the invertible phase to the
focused phase, instead of merging the two contexts Γna ; Γ0na in a
single context position as FOCLC - INV- FOC, now keeps them separate.
This second position Γ0na represents the fragment of the context
that is new during the following saturation phase. The saturation
rule SAT requires that any introduced neutral n use at least one
variable of this new context (∃x ∈ Γ0na , x ∈ n). This guarantees
that a single neutral term cannot be introduced twice by distinct
saturation phases: the second time it will not be new anymore.
This new context is also used to know when saturation stops: if
an instance of the SAT rule does not introduce any new neutral, then
on the next saturation phase the new context Γ0na will be the empty

4.2

Strong positive neutrals

To understand and formalize saturation it is interesting to compare
and contrast the various notions of deductions (seeing our type
systems as logics) at play; how to prove A in a context Γ?
• The more general notion of deduction is the unfocused notion

of proof Γ ` A – proof terms have no restriction. In the focused
system, it would correspond to looking for a proof of an invertible judgment ∅; Γ `inv A | ∅.
• The neutral judgments Γ ` n ⇓ N and Γ ` p ⇑ P correspond

to a less expressive notion of “simple deduction step”, which are
iterated by saturation. For example, hX + Y i− ⇑ Y + X does
not hold, it requires more complex reasoning than a chain of
eliminations from the context variables. Focusing decomposes
a non-focused reasoning into a sequence of such simple deduction steps, separated by invertible phases of blind proof search.

V

Γna , x : X + ` x

X+

V

V

Γna ` p P i
Γna ` σi p P 1 + P 2

saturation to find it. One could cheat, knowing that provability of
any formula is decidable in propositional logic, and test explicitly
for the absence of proof of 0; but saturation is already doing proof
search2 , and we can extend it gracefully to have this property.
We define our requirement on the selection function in Figure 7
(Specification of saturation selection functions). We require that,
for any type P that is part of the deducible observations S (by a
neutral (n : hP i− )), either P is already retrievable from the context
Γna (no need to introduce it then) or it is the type of a neutral n0
selected by the function. We do not require the same neutral n to be
selected: there may be infinitely many different neutrals deducible
at P , but just having one of them in the returned set suffices. This
definition is not natural, it will be validated by the results from
Section 5 (Saturation consistency).
Note that the types P that can be simply deduced from the context Γna ⇓ P are subformulas of Γna . We know by the subformula
property that they are also subformulas of the root judgment of the
global derivation. In particular, there is only a finite number of such
deducible types P – this would not hold in a second-order type system. Valid selection functions exist thanks to this finiteness.
Figure 7. Specification of saturation selection functions

Strong positive neutrals correspond to the positive patterns of
Zeilberger (2009). Those patterns describe the spine of a noninvertible phase, but they can also characterize invertible phases:
an invertible phase, presented in a higher-order style, provides a
derivation of the goal for any possible positive pattern passed by
the environment. The two following results witness this relation.

∀k, Γ0nak

∀P ∈ Σp ,

V

Lemma 3 (Strong decomposition of invertible phases). Consider
an invertible derivation Γna ; Σp `sinv t : N | Qa : it starts
with invertible rules, until we reach a (possibly empty) “frontier”
of saturated subterms f to which the rule SINV- SAV is applied.
k∈K
be the family of such subterms.
Let Γna ; Γ0nak `sat f k : Q0ak
0
Then the Γnak are exactly the contexts such that

SELECT- SPECIF

n : hP i− ∈ S

Note that two valid selection functions can be merged into a
valid selection function, by taking the union of their outputs.
4.4 Completeness of saturation
Completeness of saturation is relative to a specific choice of selection function. Indeed, consider the context
Γna

P

V

Lemma 4 (Strong positive cut).
If both Γna ` p P and Γna ; P `sinv t : ∅ | Qa hold, then there
exists a subterm f of t such that Γna `foc f : Qa holds.

V

This result would not be provable for the more expressive judgment Γna ` p ⇑ P : there is no obvious way to substitute a general
u : N through t that would respect the focusing structure – and
return a strict subterm. Γna P =⇒ Γna ⇑ P is true but nontrivial, it relies on the compleness result – identity expansion.
4.3 Selection function
Contrarily to the simpler setting with sums but no empty type,
not all ways to select neutrals for saturation preserve canonicity
in presence of the empty type. Consider for example the focused
terms
let x = f () in match x with (σi x → σ1 ())i
let x = f () in match x with (σi x → σ2 ())i

at the typing f : h1i+ → h1 + 1i− , g : h1i+ → h0i− ` 1 + 1.
The set of potential observations is {f (), g ()}, and both terms
made the same choice of observing only f (). The first term always returns σ1 () and the second σ2 (), so they are syntactically
distinct even modulo (≈icc ). Yet they are βη-equivalent as the
context is inconsistent. Note that if let y = g () in had been
introduced during saturation, the immediately following invertible
phase would necessarily have been absurd(y), and the two terms
would thus be syntactially equal.
To make saturation canonical again, we need a provability completeness requirement: if there is a possible proof of 0, we want

∀Γna , S, P ,
=⇒
Γna P ∨ ∃(n0 : hP i− ), n0 ∈ SelectΓna (S)
Select ( ) is a valid selection function
V

hN i+

P

V

Γna , x : N ` x

V

Figure 6. Strong positive judgment Γna ` p

V

V

One notion that is missing is the notion of what is “already
known by the context”. With the usual non-focused logic, to know
if a positive formula P has been introduced before, we simply
check if P is in the context. But the focusing discipline decomposes
positive formulas and removes them from the context.
One could use the judgment Γna ⇑ P instead – X + , Y + ⇑
X + + Y + as intended. But Γna ⇑ P is too strong for the purpose of
just retrieving information from the context, as it calls the general
invertible judgment at the end of the focused phase. Γna ⇑ hN i+
holds whenever N is provable from Γna , not only when N is an
hypothesis in Γna .
To capture this idea of what can be “retrieved” from the context
without any reasoning, we introduce in Figure 6 (Strong positive
judgment Γna ` p P ) the strong positive judgment Γna P .

def

=

(x : X + , y : h1i+ → X +

−

)

+

In this context, the only deducible positive formula is X , and it is
already retrievable from Γna . This means that a selection function
that would satisfy SelectΓna (S) = ∅ would be a valid selection
function. However, saturating with such a selection function is
not computationally complete: the saturated term x : X + has a
valid derivation, but let z = y () in z does not – nor does any
equivalent term.
We can order selection functions by pointwise subset ordering:
a function f is above g if it selects at least all of g’s neutrals for
each context. A set of saturation functions is upward-closed if, for
any saturation function in the set, any function above it is in the set.
Theorem 8 (Completeness of saturation). For any focused term
Γna ; Σp `inv t : N | P a , there exists an upward-closed set of
selections functions such that Γna ; Σp `sinv t0 : N | P a holds, for
a (computable) saturated term t0 such that btcfoc ≈βη bt0 cfoc .
Note that, given two focused term t1 , t2 , we can merge the selection functions used in the theorem above to get a single selection
function for which there exists saturated terms for both t1 and t2 .

5.

Saturation consistency

In this section, we prove the main result of this extension of saturation to the empty type: if a context is inconsistent, then the saturation phase will eventually introduce a variable of the empty type 0
2 Saturation

synthetizes new sub-terms and can thus decide equivalence
with 0, unlike previous methods that would only reorder the subterms of the
compared terms.

in the context. This is key to obtaining a canonicity result – if saturation sometimes missed proofs of 0, it could continue with distinct
neutral terms and result in distinct but equivalent saturated terms.
The informal view of the different ways to deduce a positive
formula presented in Section 4.2 (Strong positive neutrals) (general proof, simple deduction, retrieval from context) gives a specification of what saturation is doing. From a high-level or big-step
point of view, saturation is trying all possible new simple deductions iteratively, until all the positives deducible from the context
have been added to it. The following characterization is more finegrained, as it describes the state of an intermediary saturation judgment Γna ; Γ0na `sat f : P a .
The characterization is as follows: any formula that can be
“simply deduced” from the old context Γna becomes “retrievable”
in the larger context Γna , Γ0na . This gives a precise meaning to the
intuition that Γna is “old”. What we mean when saying that Γ0na is
“new” can be deduced negatively: it is the part of the context that is
still fresh, its deductions are not stored in the knowledge base yet.

∀P ,

Γna ⇓ hP i−

Γna , Γ0na

=⇒
−

Definition 11. Γna is saturated if Γna ⇓ hP i implies Γna

V V

Theorem 9 (Saturation). If a saturated proof starts from a judgment of the form ∅; Γna0 `sat f : Qa or ∅; Σp 0 `sinv t : N | Qa
then for any sub-derivation of the form Γna ; Γ0na `sat f : Qa we
have the following property:
P
P.

Corollary 2 (Saturation). If a saturated proof starts from a judgment of the form ∅; Γna0 `sat f : Qa or ∅; Σp 0 `sinv t : N | Qa
then for any sub-derivation of the form Γna ; ∅ `sat f : Qa the environment Γna is saturated.
Lemma 5 (Saturated consistency). If Γna is saturated, then Γna 0 0.
Theorem 10 (Inconsistent canonicity). If Γna ` 0, then for any
f , f 0 such that ∅; Γna `sat f , f 0 : P a we have f ≈icc f 0 .

6.

Canonicity

In this section we establish the main result of this article. If two
saturated terms Γna ; Σp `sinv t, t0 : N | Qa are not syntactically
equivalent (t 
≈icc t0 ), then there exists a model M in which a
context distinguishes t from t0 : they are not contextually equivalent.
(We build distinguishing contexts in the un-focused λ-calculus,
so technically we are distinguishing the defocused forms btcfoc , bt0 cfoc ;
the proof crucially relies on the saturated structure of its inputs, but
the code we generate for computation and separation is more easily
expressed unfocused.)
6.1

Sketch of the proof

Intuition It is helpful to first get some intuition of what a pair
of syntactically distinct normal forms looks like, and what the
corresponding distinguishing context will look like. Suppose we
have Γna ; Σp `sinv t 
≈icc t0 : N | Qa . We can explore t and t0
simultaneously, until we find the source of their inequality.
The source of inequality cannot be in an invertible phase, given
that the term formers in invertible phase are completely determined
by the typing (modulo invertible commuting conversions); for example, if N is N 1 × N 2 , we know that t is of the form (t1 , t2 ),
and t0 of the form (t0 1 , t0 2 ), with ti 
≈icc t0 i for some i – so we
can continue exploring ti 
≈icc t0 i . Same thing if the term starts
with a sum elimination (modulo (≈icc ) one can assume that they
eliminate the same variable), match x with (σi x → ti )i 
≈icc
match x with (σi x → t0 i )i : the subterms ti , t0 i in at least one
of the two branches differ.
Similarly, the source of inequality cannot be in the saturation
phase, where both terms saturate on neutrals that are completely

determined by the typing context – and the saturation selection
function – they are both of the form let x̄ = n̄ in for the same
set of neutrals on each side. The end of this saturation phase is
also type-directed, so both terms stop saturating (they get an empty
Γ0na context) at the same time. The difference must then be in
the neutrals used in the SAT- UP or SAT- DOWN rules, n 
≈icc n0
or p 
≈icc p0 . Note that we cannot get a positive neutral on one
side and a negative neutral on the other, as usage of those rules
is directed by whether the goal type is a negative atom X − or a
positive type P .
Now, two neutrals n 
≈icc n0 or p 
≈icc p0 may differ because
their spine differ, or because their sub-terms that are outside the
non-invertible phase differ. In the latter case, finding the source of
inequality is a matter of traversing the common structure towards
the sub-terms that differ. The former case is more interesting –
this pair of neutrals with distinct spines is what we call source of
inequality.
In the positive neutral case, we end up on either σi p and σj p0
with i 6= j, or distinct variables x 6= y of atomic type X + . In
the negative neutral case, one may encounter distinct neutrals with
distinct structure, for example n p 6= x 6= πi m at the same type
N ; negative neutrals should be looked “upside down”, as in System
L (Curien, Fiore, and Munch-Maccagnoni 2016): either their head
variables differ, or the same variable is applied a different sequence
of elimination rules.
In the easy case where the source of inequality is a sum con≈icc (σj ), obtaining a distinguishing context
structor (σi ) 
looks relatively easy: we need a context C [] that corresponds to
the term traversal we performed to reach this source of inequality.
≈icc t0 2 ,
For example, if we had (t1 , t2 ) 
≈icc (t0 1 , t0 2 ) because t2 
the context fragment corresponding to this reasoning step would
be π2 . This is trickier in the sum-elimination case: if we have
≈icc match x with (σi x → t0 i )i
match x with (σi x → ti )i 
then we need our context to instantiate the variable x with the
right value σi p so that the branch we want is taken – the one with
≈icc t0 i . This is easy if x is a formal variable introduced by a
ti 
λ-abstraction: at the point where our context needs to distinguish
the two λ-abstraction λx. t 
≈icc λx. t0 , we need to use an application context of the form  (σi p). But x may have been introduced
by a left-focusing step let x = n in t 
≈icc let x = n in t0 ; then
we need to instantiate the variables of the observation n just so that
we get the desired result σi t0 . When the source of inequality is on
negative neutrals with heads x : N , y : M or positive variables
x 6= y : X + , we need the distinguishing context to pass values in
the same way to get to this source of inequality, and also to instantiate the variables x, y to get an inequality. If those variables are
at an atomic type, we must pick a model that replaces this atomic
type by a closed type, to instantiate them by distinguishable values
at this closed type.
Positive simplification In order to simplify the following arguments, we will suppose that the context and types of the two saturated proof to distinguish do not use negative atoms, only positive
atoms. In other words, the results only holds for the focused system
in the fragment ΛC(X + , →, ×, 1, +, 0).
This is a perfectly reasonable simplification in view of our
goal, which is to distinguish inequivalent non-focused term that
have distinct saturated normal forms: we know that any choice of
polarization for the non-focused atoms preserves the existence of
normal forms, so we can make them all positives – see Section 3.3
(Choices of polarization).
In particular, the source of inequality (distinct neutrals whose
spine differs) is always a pair of neutrals p 
≈icc p0 , who contain a
syntactic difference (σi 
≈icc σj with i 6= j, or x 6= y : X + )
before the end of the non-invertible phase. Negative neutrals are
only used during saturation.

outFin (inFin (x)) = x ∈ S ∧ ∅ ` inFin (outFin (t)) ≈βη t : Fin (S)

For any two distinct elements x 6= y ∈ S there exists a distinguishing context for inFin (x) 
≈ctx inFin (y).
Definition 12 (Neutral model). Given two syntactically distinct
≈icc t00 : N | P a (with positive
saturated terms Γna ; Σp `inv t0 
atoms only) with a source of inequality of the form
Γ0na ` p 
≈icc p0 ⇑ P

we define the neutral model N t0 ,t00 (or just N ) by

def
N t0 ,t0 0 (Y + ) = Fin {x | (x : Y + ) ∈ Γ0na }

We say that N (X) contains a code for each atomic variable
bound at the source of inequality.
Distinguishing outline The general idea of our distinguishing
context construction is to instantiate variables just so that each
variable of atomic type (x : X + ) evaluates to its code inFin (x).
Thus, when we end up on distinct neutrals p 
≈icc p0 , we know that
our context will send them to distinguishables values.
There are two moments where building a distinguishing context requires synthesizing a closed value of a type: to instantiate
the open variables in the context of the two terms, and when distinguishing invertible terms at a function type P → N , which we
know to be of the shape λ(x : P ). ( : N ).
Synthesizing a value for a variable of atomic type (x : X + )
is obvious, we just pick inFin (x) – this guarantees that, under
this context, x will reduce to inFin (x) as expected. For a variable
of sum type P + Q, we have to choose the value to make sure
that the correct branch of the two terms (the one containing the
source of inequality) will be explored, as previously explained. For
a variable x of negative type N , we have to make sure that any
observation of x, any neutral term n whose head variable is x (in
the syntax of Curien, Fiore, and Munch-Maccagnoni (2016) they
are the hx | Si), will reduce to the value we need: if we have
let y : P = n in . . ., the neutral n should reduce to inFin (y). In
other words, much in the spirit of higher-order focusing Zeilberger
(2009), we specify the instantiation of (x : N ) by a mapping over
all the observations over x that are made in t0 , t00 .
Example Consider for example:
+

n : (1 + X ) → X

+ −

`

let z = n (σ1 ()) in
let o = n (σ2 z) in z
≈icc

let z = n (σ1 ()) in
let o = n (σ2 z) in o

: X+

The shared context in this example is
let z = n σ1 () in let o = n (σ2 z) in 

and the source of inequality is z 
≈icc o. The atomic variables in
the context at this point are z and o, so we have N (X + ) =
Fin ({z, o}). We have to provide a value for the negative variable
n; its “observations”, the arguments it is called with, are σ1 () and
σ2 z, so we define it on these inputs following the general scheme:
def

n̂ =



σ1 ()
σ2 inFin (z)

7→
7→

inFin (z)
inFin (o)

The value of n̂ on the last element of N (1 + X + ), namely
σ2 (inFin (o)), is not specified; the return type is inhabited so a
value can be chosen, and the specific choice does not matter.
def
It is easy to check that the context C [] = (λn. ) n̂ is such
that plugging both terms will result in distinct closed values of
N (X + ), namely inFin (z) and inFin (o). From there, building a
distinguishing context returning a boolean is trivial.

Technical challenge We outlined the general argument and
demonstrated it on an example. Unfortunately, we found that scaling it to a rigorous, general proof is very challenging.
When we define instantiation choices for negative types as mappings from observations to their results, we implicitly rely on the
fact that the observations are distinct from each other. This is obvious when the domain of these observations is made of firstorder datatypes (no functions), but delicate when some of those
observations have function types – consider observations against
−
(x : hP → N i+ → X + ).
The natural idea is to inductively invoke the distinguishability
result: if x (λy. t) 
≈icc x (λy. t0 ), then t 
≈icc t0 are distinguishable and x̂ can distinguish those two arguments by passing the right
instantiation for y. However, making this intuition precise gets us
into a quagmire of self-references: to define instantiation of the
variable x, we may need to instantiate any such variable y whose
scope it dominates, but the argument for distinguishability is really
on the values that λy. t, λy. t0 have reduced to by the time they are
passed to x̂; but the natural way to denote those values makes a reference to the instances passed for all the variables in their scope, x
included...
We are convinced that there is a general inductive argument to
be found that would play in a beautiful way with general polarized
type structure. We have not found it yet, and shall for now use
(a focused version of) the function-removal hack from Section 2.5
(Fun-less types and reification).
6.2

Saturated inequivalence

We argued that if we have t 
≈icc t0 , then those terms must
be of the form D [n], D [n0 ] or D [p], D [p0 ] where the neutrals
n
≈icc n0 : X − or p 
≈icc p0 : P have distinct spines (invertible
phases), that is, they differ even when ignoring their invertible subterms. With the simplifying assumption that all atoms are positively
polarized, only the case p 
≈icc p0 may arise.
This structure is crucial in the proof of canonicity, so we introduce in Figure 8 (Saturated inequivalence judgment) a precise
inductive definition of this decomposition as a saturated inequivalence judgment


Γ | Ξ `inv D Γ0 | Ξ0 `ne p 6= p0 : P : N | P a

which represents constructive evidence of the fact that D [p] 
≈icc
D [p0 ], where p, p0 are the source of inequality as witnessed by the
new judgment Γ0 `ne p 6= p0 ⇑ P .
The new structure Ξ is a constraint environment, a list of equalities of the form p = x : P or x = n : P that correspond to
knowledge that was accumulated during the traversal of D: under
a binding let x = n in t we remember x = n, and when doing a case-split on a variable x : P 1 + P 2 we remember which
branch leads to the source of inequality by σi x0 = x. Together,
Γ0 | Ξ0 form a constrained environment as used in Fiore and Simpson (1999). Note that when decomposing the variable x : P 1 + P 2
we mention it in the constraint environment, so we also keep it in
Γ0 for scoping purposes: we use general contexts with types of any
polarity, not just negative or atomic contexts Γna .
Two side-conditions in this judgment capture the essential properties of saturated terms required to obtain canonicity. In the saturation case, the condition ∀n ∈ n̄, n ∈
/ Ξ enforces that let-bindings
in the constraint environment Ξ all bind distinct neutrals. At the
source of inequality, the condition Γ 0 0 enforces that the context
is consistent.
Definition 13. A constrained environment Γ | Ξ is valid if
n ∈ Ξ =⇒ Γ ` n ⇓ Ξ

p ∈ Ξ =⇒ Γ ` p

V

Neutral model If S is a finite set, let us write Fin (S) for the
type 1 + . . . + 1 that is in bijection with S (same number of elements), witnessed by embeddings inFin ( ) : S → Fin (S) and
outFin ( ) : Fin (S) → S such that

(p = x) ∈ Ξ, (p0 = y) ∈ Ξ, x =α y =⇒ p =α p0
(x = n) ∈ Ξ, (y = n0 ) ∈ Ξ, n =α n0 =⇒ x =α y

Ξ

Figure 8. Saturated inequivalence judgment
Ξ ::= ∅ | Ξ, p = x | Ξ, x = n

constraint environment

Γ | Ξ `inv D [Γ0 | Ξ0 `ne p 6= p0 : P 0 ] : N | Qa
Γ, x : P 1 + P 2 , xi : P i | Ξ, σi xi = x `inv
D Γ0 | Ξ0 `ne p 6= p0 : P 0 : N | Qa
Γ, 
x : P 1 + P 2 | Ξ `inv
match x with



σi xi → D  Γ0 | Ξ0 `ne p 6= p0 : P 0 : N | Qa
σj xj6=i → t
(other cases omitted for space)
Γ | Ξ `foc D [Γ0 | Ξ0 `ne p 6= p0 : P 0 ] : Qa
∀n ∈ n̄, n ∈
/Ξ

Γ, x̄ : P̄ | Ξ, x̄ = n̄ `inv D Γ0 | Ξ0 `ne p 6= p0 : P 0 : ∅ | Qa
 0

Γ | Ξ `foc let (x̄ : P̄ ) = n̄ in D (Γ | Ξ0 `ne p 6= p0 : P 0 ) : Qa
Γ `ne p 6= p0 ⇑ P
Γ00


Γ | Ξ `foc  Γ | Ξ `ne p 6= p0 : P : P

(other cases omitted for space)

Γ `ne p 6= p0 ⇑ P
(i 6= j) ∨ Γ `ne p 6= p0 ⇑ P i=j
Γ `ne σi p 6= σj p0 ⇑ P 1 + P 2

x 6= y
+

Γ, x : X , y : X

+

`ne x 6= y ⇑ X

+

no case for Γ `ne t 6= t0 ⇑ hN i+

Lemma 6 (Saturated inequivalence).
If ∅; Σp `inv t 
≈icc t0 : N | Qa with positive atoms only, then there
exists D [], p, p0 and a valid Ξ such that
Σp | ∅ `inv D Γ0na | Ξ `ne p 6= p0 : P : N | Qa




0

t ≈icc D [p]
0

Let us write (t 
≈icc t )
6.3

t ≈icc
0

D [p 6= p ] when this relation holds.

Focused fun removal

In this section, we describe how to transform any pair of distinct saturated terms t0 
≈icc t00 in ΛC(X + , →, ×, 1, +, 0) into
a pair of distinct saturated terms in the restricted type system
ΛC(×, 1, +, 0). We know that we can apply the neutral model
N t0 ,t00 to get a pair of terms without atoms – ΛC(→, ×, 1, +, 0)
– and then the bijections of Section 2.5 (Fun-less types and
reification) give us terms in ΛC(×, 1, +, 0). But the impact of these
transformations on the focused and saturated term structure must
be studied carefully.
Reduction to closed types When applying the neutral model
N t0 ,t00 , we turn atomic types X + into strictly positive types
N (X + ) of the form 1 + . . . + 1. Consider a binding site of the
form (λ(x : X + ). t), which becomes λ(x : 1 + . . . + 1). N (t) after transformation. To recover a valid focused term, we need to
insert a big sum elimination to remove the positive variable x from
the context:
+

Theorem 11 (Inequivalence in the model). Suppose we have satdef
urated forms t0 , t00 with positive atoms only. Let us define t1 =
0
0 def
N t0 ,t00 (t0 ) and t1 = N t0 ,t00 (t0 ).
If (t0 
≈icc t00 )
D0 [p0 6= p0 0 ], then there exists D1 , p1 , p0 1
0
≈icc t1 )
D1 [p1 6= p0 1 ]
such that (t1 
Function elimination To turn t1 
≈icc t01 into terms at functionless types, we use the transformations presented in Figure 9 (Funless focused forms). They correspond to focused versions of the
term transformation b cA and T UA of Figure 3 (Fun-less data
types), in two interdependent ways: their definition assumes the
transformed terms respect the focused structures, which gives us
rich information on term shapes, and their result remain in focused
form. The specification of these transformations is as follows:
Γna ; Σp `inv t : N | P a ⇒ bΓna c; bΣp c `inv btc(N |P a ) : bN c | bP a c
Γna ; Σp `inv t : N | P a ⇒ TtU(N |P a ) TN UTP a U

 
D p0

λx. match x with (σi x → t[σi ()/x])i∈N (X

The substitution of σi () for (x : X + ) in t may not create βredexes, as a variable x of atomic type may not occur in eliminatedsum position. By inspection of the typing rules of our focused
system, such a variable can only appear in a judgment of the form
Γna ` x ⇑ X + ; the focused structure is preserved by replacing it
by the derivation Γna ` σi () ⇑ 1 + . . . + 1.
For a focused term t, let us simply write N (t) for this transformed focused term, splitting over each variable of type N (X + ).
The saturated structure, however, is not preserved by this
change. The problem is that replacing a new variable x by a closed
term σi () may break the condition that only “new” neutrals are
introduced during a saturation phase: any neutral that would only
use x as the new variable introduced by the last invertible phase is
not new anymore.
However, we can show that the saturated inequivalence structure is preserved by this transformation. There is a shared context
to a source of inequality in the transformed terms, where the letbindings might not be new at introduction time, but they are not
redundant, as requested by the inequivalence structure. This is the
property of saturated proofs (besides saturation consistency) that
our distinguishability result relies on.

)

(the family notation here denotes a cascade of sum-eliminations,
with as many cases in total as elements in N (X + )). We also
perform such an elimination on each variable in context at the root.

Γna ` n ⇓ N
...
TΓna U ` TnUN ⇓ TN U
⇒ ∃m0 ,
Γna ` m ⇓ N 0
TΓna U ` m0 ⇓ N 0

...

The transformation of negative neutrals is more elegantly expressed in the sequent-calculus syntax of Curien, Fiore, and
Munch-Maccagnoni (2016): we transform a command hn |N Si :
Γna ` M cutting on a type N into a command Thn |N SiUN :
TΓna U ` M cutting on TN U. We will write m [n] when the neutral
m has head n – it is of the form hn | Si.
The definition strongly relies on the inversion of term structure
of focused terms modulo (≈icc ). For example, when we define
Tλx. tU(P 1 +P 2 )→N , we know that x : P 1 + P 2 and can thus assume modulo (≈icc ) that t is of the form match x with (σi x → ti )i .
Similarly in the neutral case, we know that any neutral Γna ` n ⇓
(P 1 + P 2 ) → N can only appear in a term applied to an argument
Γna ` p ⇑ (P 1 + P 2 ) – non-invertible phases are as long as possible, so they cannot stop on a negative function type – and we know
that such an p must be of the form σi p0 .
The way the focused structure conspires to make this transformation possible is, in fact, rather miraculous – is it more than just
a hack? In the λx. t case of hN 1 × N 2 i+ → M , we know that a
derivation of the form Γna ` x ⇓ N 1 × N 2 can only appear inside a larger derivation Γna ` πi x ⇓ N i , which we can replace by
TΓna U ` xi ⇓ N i . In the neutral case, a (n : hN 1 × N 2 i+ → )
can only appear applied to an argument Γna ` p ⇑ hN 1 × N 2 i+ ,
but as this is a shifted negative type we know that p is in fact an
invertible form Γna ; ∅ `inv t : N 1 × N 2 | ∅, and this must be a pair

Figure 9. Fun-less focused forms
btcA

Tλx.

match x with
σ1 x → t1
σ2 x → t2

applies T UA on all subterms


Tλx. t1 UP 1 →N
def 

,
U(P 1 +P 2 )→N =
Tλx. t2 UP 2 →N
def

TnU(P 1 +P 2 )→N (σi p) = Tπi nUP i →N p
def

Tλx. absurd(x)U0→N = ()

TnU0→N p impossible

def

def

Tλx. tUh1i+ →N = t
def

def

TnUhN 1 ×N 2 i+ →M (t1 , t2 ) = TTnUN 1 → t1 UN 2 → t2
def

hhP i− i+ →N

= Tλx. tUP →N
def

TnU hP i− + →N (Γna ; ∅ `inv p : hP i− | ∅) = TnUP →N p
h
i
def

TxUN = (x : TN U)

(t1 , t2 ), exactly what we needed to define the transformation. The
+
same phenomenon occurs on the argument Γ0na ` p ⇑ hP i− of
the double-shifted case.
Lemma 7 (Function elimination preserves inequivalence).
(∃D, p, p0 , (t 
≈icc t0 )



D p 6= p0 )

=⇒ (∃D, p, p0 , (btc 
≈icc bt0 c)



D p 6= p0 )

(The converse implication also holds, but we don’t need it.)
Lemma 8.
r
z
r
z
q
y
q
y
bbtcA cfoc = bbtcfoc cbAc± = b btcfoc cbbAc± c ∈ bAc±

Corollary 3 (Fun-elimination preserves semantic equivalence).
q y
Jt K = t0

6.4

⇐⇒

q
y
JbtcA K = bt0 cA

Canonicity

Definition 14. Let a closed substitution ρ be a mapping from
variables to closed terms of closed types (types without atoms).
We write ρ : Γ when Γ is a closed context and, for any (x : A) ∈
Γ we have ∅ ` x[ρ] : A.
If Ξ is a constraint environment, we say that Ξ[ρ] holds when,
for any equation t = u in Ξ, we have t[ρ] ≈sem u[ρ].
We write ρ : (Γ | Ξ) if ρ : Γ and Ξ[ρ] hold.
Theorem 12 (Canonicity). Assume Γ is consistent, Ξ is valid, and


Γ0 | ∅ `inv D Γ | Ξ `ne p 6= p0 : P : N | P a

is a judgment of closed function-less types. Then there exists a
closed substitution ρ : (Γ | Ξ) such that p[ρ] 
≈sem p0 [ρ].
Corollary 4 (Canonicity). In the sub-system ΛC(×, 1, +, 0):


 
Γ | ∅ `inv D Γ0 | Ξ0 `ne p 6= p0 : P : N | P a ⇒ D [p] 
≈ctx D p0

6.5

Corollary 6. Contextual and βη-equivalence coincide
Corollary 7. Equivalence in the full simply-typed λ-calculus with
sums and the empty type is decidable.
Corollary 8. The full simply-typed λ-calculus with sums and the
empty type has the finite model property.

TnUh1i+ →N () = n

Tλx. tUhN 1 ×N 2 i+ →M = Tλx1 . Tλx2 . t[xi /πi x]i UN 2 → UN 1 →

Tλx. tU

Corollary 5 (Contextual equivalence implies equality of saturated
forms). If Γ ` t, t0 : A are (non-focused) terms of the full simplytyped lambda-calculus ΛC(X, →, ×, 1, +, 0) with t ≈ctx t0 , then
for any Σp , N with no positive atoms and bΣp c± = Γ, bN c± = A
and any saturated terms ∅; Σp `sinv u, u0 : N | ∅ such that
t ≈βη bucfoc and t0 ≈βη bu0 cfoc we have u ≈icc u0 .

Results

Theorem 13 (Saturated terms are canonical). In the system with
only positive atoms, if ∅; Σp `sinv t 
≈icc t0 : N | P a then
t
≈ctx t0 .

7.

Conclusion

7.1

Other Related Work

Background material For the reader looking for more historical
perspective Dougherty and Subrahmanyam (2000) gives an interesting, detailed presentation of the state of the art in separation theorems in absence of sum types, and of why their approach are difficult to extend to sums. Simpson (1995) gives an enjoyable, accessible exposition of what “completeness” exactly means in the setting
of categorical semantics; in particular, while we can prove that two
inequivalent terms can be distinguished by a choice of finite sets,
there is no fixed choice of finite sets that could separate all pairs of
terms. It also discusses the notion of “typical ambiguity”, and the
idea that βη-equality is shown to be the maximal consistent relation. At the time of writing, Simpson’s statement of the 15th TLCA
open problem is also one of the clearest expositions of the relation
between these questions.
Focusing The main field of application of focusing to programming is the area of logic programming, where operational semantics correspond to search strategies, which can often be described
as specific choices of polarization in a focused logic (Chaudhuri,
Pfenning, and Price 2008b). Focusing has been used to study programming language principles in Zeilberger (2009); when considering non-normal forms (logics with a strong cut rule) it let us reason finely about evaluation order.
This suggests the general notion of polarization, an approach of
programming calculi where compositions (cuts) are non-associative
(Curien, Fiore, and Munch-Maccagnoni 2016), modeling effects
and resources. In the present work we consider only focused normal forms (except for stating the completeness of focusing), which
only captures the pure, strongly normalizing fragment, and thus
corresponds to a depolarized system.
Guillaume Munch-Maccagnoni’s work on polarized abstract
machine calculi harps on many ideas close to the present work, in
particular Munch-Maccagnoni and Scherer (2015). It is conducted
in a syntax that is inspired by the sequent calculus rather than the
λ-calculus; this choice gives a beautiful dynamic semantics to polarized systems. In contrast, the focused λ-calculus as presented
is a system of normal forms, and defining an internal reduction
for it would be awkward. While there is no direct correspondence
between sequent proofs and natural deduction proofs in general,
their normal forms are in one-to-one mapping, so in our context the
choice of abstract machine or λ-terms-inspired syntax matters less.
Atom-less systems The structure of normal forms has been studied in Altenkirch and Uustalu (2004) in the special case of the
type system ΛC(→, +, 2), with boolean types instead of general
sums, and no atoms. While conceptually easier to follow than the
Grothendieck logical relations of the more general normalizationby-evaluation work on sums, they remain challenging in presence
of higher-order functions.

In unpublished work, Ahmad, Licata, and Harper (2010) work
with the type system ΛC(→, ×, 1, +, 0): no atoms, but everything
else. They use focusing as a guiding principle to generalize the normal forms of ΛC(→, +, 2) to everything else – to our knowledge
this is the first work to use focusing to approach sum types. The
result obtained, namely decidability of observational equivalence
in this system, is not striking on its own: in absence of atoms, all
types are finitely inhabited, so two functions can be compared by
testing them on all their input domain. But it is conducted in a rigorous, inspiring way that shows the promises of the focused structure. Our own proof of distinguishability of distinct normal forms is
not as elegant as this development, as it uses the inelegant shortcut
of function type elimination. We are convinced that there exists a
beautiful proof that weaves the distinguishability structure through
higher-order abstractions in their style, but have yet to find it.
7.2

Future Work

Direct distinguishability proof The use of the positive atoms
simplification and the detour through types without functions are
a bit disappointing. There should be a proof in which all steps are
as general and general as possible: completeness of focusing in the
explicitly polarized system, completeness of saturated forms, and
then canonicity of saturated forms at all types.
Categorical semantics We wonder what is the relation between
the saturated structure and the existing work on categorical semantics of the λ-calculus with finite sums.
Direct comparison algorithm We prove decidability by reducing
equivalence of arbitrary λ-terms to equivalence of saturated forms.
This algorithm can be implemented, but we would rather use an algorithm that does not need to compute full saturated normal forms
before returning a result – in particular on inequivalent inputs.
It is reasonably easy to formulate an equivalence algorithm on
the focused forms directly, that would perform the saturation “on
the fly”: at the beginning of each saturation phase, look for all the
neutrals that can be defined in the current context, recursively compute their equivalence classes, and replace each class by a distinct
free variable – then continue on the neutral structure. Proving this
algorithm correct, however, turns out to be challenging.
Finally, it would be interesting to have an algorithm expressed
directly on the non-focused terms, that would perform a focusing
transformation on the fly, as much as each step of equivalence
requires. The difficulty then is that neutral subterms are not as long
as possible (they may be interrupted by commuting conversions),
so it is possible to look for neutrals sub-terms definable in the
current context and miss some of them – future reasoning stages
may un-stuck sum-eliminations that in turn un-block neutrals that
should have been bound now. For the type system with non-empty
sums, control operators have been used (Balat, Di Cosmo, and
Fiore 2004) to solve that issue; can the technique be extended?

Acknowledgments
Amal Ahmed made this work possible by giving the time, motivation and advice that let it foster. Andrew Pitts gave warm encouragements to look at the specific question of the empty type, and
Alex Simpson enthusiastically sat through an intense whiteboard
session at Schloss Dagstuhl and provided the final motivation to
get it done. Max New, Didier Rémy and the anonymous referees
provided very useful feedback on the article.
This research was supported in part by the National Science
Foundation (grant CCF-1422133).

References
Arbob Ahmad, Daniel R. Licata, and Robert Harper. Deciding coproduct
equality with focusing. Online draft, 2010. 6, 13
Thorsten Altenkirch and Tarmo Uustalu. Normalization by evaluation for
lambda-2 . In FLOPS, 2004. 4, 12
Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott.
Normalization by evaluation for typed lambda calculus with coproducts.
In LICS, 2001. 1
Jean-Marc Andreoli. Logic Programming with Focusing Proof in Linear
Logic. Journal of Logic and Computation, 2(3), 1992. 1, 4
Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus
with sums. In POPL, 2004. 1, 13
Corrado Böhm. Alcune proprieta delle forme normali nel k-calcolo. IAC
Pubbl, 696119, 1968. 1
Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent
proofs via multi-focusing. In IFIP TCS, 2008a. 1, 7
Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. J.
Autom. Reasoning, 40(2-3), 2008b. 6, 12
Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A Systematic Approach
to Canonicity in the Classical Sequent Calculus. In CSL, 2012. 1
Pierre-Louis Curien, Marcelo Fiore, and Guillaume Munch-Maccagnoni.
A Theory of Effects and Resources: Adjunction Models and Polarised
Calculi. In Proc. POPL, 2016. doi: 10.1145/2837614.2837652. 5, 9, 10,
11, 12
Daniel J Dougherty and Ramesh Subrahmanyam. Equality between functionals in the presence of coproducts. Information and Computation, 157
(1), 2000. 1, 2, 12
Marcelo Fiore and Alex Simpson. Lambda definability with sums via
grothendieck logical relations. In TLCA, 1999. 1, 10
Harvey Friedman. Equality between functionals. In Logic Colloquium,
1975. 1
Neil Ghani. Beta-Eta Equality for Coproducts. In TLCA, 1995. 1
Danko Ilik. The exp-log normal form of types and canonical terms for
lambda calculus with sums. CoRR, arxiv:1502.04634, 2015. URL
http://arxiv.org/abs/1502.04634. 4
Chuck Liang and Dale Miller. Focusing and polarization in intuitionistic
logic. CoRR, arxiv:0708.2252, 2007. URL http://arxiv.org/
abs/0708.2252. 5, 6
Sam Lindley. Extensional rewriting with sums. In TLCA, 2007. 1
Guillaume Munch-Maccagnoni and Gabriel Scherer. Polarised Intermediate
Representation of Lambda Calculus with Sums. In LICS, 2015. 12
Gabriel Scherer. Which types have a unique inhabitant? Focusing on pure
program equivalence. PhD thesis, Université Paris-Diderot, 2016. 2
Gabriel Scherer and Didier Rémy. Which simple types have a unique
inhabitant? In ICFP, 2015. 1, 2, 5, 7, 15
Robert J. Simmons. Structural focalization. CoRR, arxiv:1109.6273,
2011. URL http://arxiv.org/abs/1109.6273. 6
Alex Simpson. Categorical completeness results for the simply-typed
lambda-calculus. In TLCA, 1995. 12
Richard Statman. Completeness, equivalence and lambda-definability.
Journal of Symbolic Logic, 47(1), 1982. 1
Noam Zeilberger. The Logical Basis of Evaluation Order and PatternMatching. PhD thesis, Carnegie Mellon University, 2009. 8, 10, 12
Noam Zeilberger. Polarity in proof theory and programming, 2013. URL
http://noamz.org/talks/logpolpro.pdf. Lecture Notes for the
Summer School on Linear Logic and Geometry of Interaction in Torino,
Italy. 7

A.

Full definitions

Definition (Semantics of terms). We define the following naive
semantics for term formers:

def

TtUA1 ×A2 →B = Tλx1 . Tλx2 . t (x1 , x2 )UA2 →B UA1 →TA2 →BU
def

TtU1→B = t ()

def

varx : JΓ, x : A ` A KM

TtUA1 +A2 →B = Tλx. t (σ1 t)UA1 →B , Tλx. t (σ2 t)UA2 →B

def



def

varx (G) = G(x)

pair : JΓ ` A1 KM × JΓ ` A2 KM → JΓ ` A1 × A2 KM

TtU0→B = ()

def

pair(f1 , f2 )(G) = (f1 (G), f2 (G))

VtWA1 ×A2 →B = λx. VVtWA1 →TA2 →BU (π1 x)WA2 →B (π2 x)

proji : JΓ ` A1 × A2 KM → JΓ ` Ai KM

VtWA1 +A2 →B = λx. match x with

def

def

VtW1→B = λx. t

σ1 x1 → Vπ1 tWA1 →B x1
σ2 x2 → Vπ2 tWA2 →B x2

def

def

proji (f )(G) = vi
where f (G) = (v1 , v2 )

def

VtW0→B = λx. absurd(x)

lam : JΓ, x : A ` B KM → JΓ ` A → B KM

def

def

TvUA1 ×A2 →B = Tw1 7→ Tw2 7→ v((w1 , w2 ))UA2 →B UA1 →TA2 →BU

lam(f )(G) = (v ∈ JA KM ) 7→ f (G, x 7→ v)

def

TvU1→B = v(?)

app : JΓ ` A → B KM × JΓ ` A KM → JΓ ` B KM

def

TvUA1 +A2 →B = Tw 7→ v(((1, v)))UA1 →B , Tw 7→ v(((2, v)))UA2 →B

def

app(f, g)(G) = f (G)(g(G))

def

TvU0→B = ?

unit : JΓ ` 1 KM

def

unit(G) = ?

VvWA1 ×A2 →B = (w1 , w2 ) 7→ VVvWA1 →TA2 →BU (w1 )WA2 →B (w2 )

inji : JΓ ` Ai KM → JΓ ` A1 + A2 KM

V(v1 , v2 )WA1 +A2 →B = (i, w) 7→ Vvi WAi →B (w)

def

def

VvW1→B = ? 7→ v

def

inji (f )(G) = (i, f (G))

match : JΓ ` A1 + A2 KM × JΓ, x : A1 ` B KM × JΓ, x : A2 ` B KM
→ JΓ ` B KM
def

match(f, g1 , g2 )(G) = gi (G, x 7→ v)
where f (G) = (i, v)
absurd : JΓ ` ∅ KM → JΓ ` A KM
def

absurd = ∅

VvW0→B = ∅

Definition (Depolarization).


X+

def



=

±

bP + Qc±

def

b0c±
j
k
hN i+

def

±

By composing together the semantics of the term formers in the
obvious way, we obtain semantics for terms t and one-hole contexts
C:
JΓ ` t : A KM ∈ JΓ ` A KM
q



y
q
y
Γ ` C Γ0 `  : A0 : A0 M ∈ Γ, Γ0 ` A0 M → JΓ ` A KM

For example we have J(t1 , t2 ) KM = pair(Jt1 KM , Jt2 KM ) and
J(t, ) KM (f ) = pair(Jt1 KM , f ). In particular, J KM is the
identity function.
Definition (Fun-less types and reification).
(The definitions of bAc and TAU were given in Figure 3 (Funless data types).)
b cA

A → bAc

:

def

b(t1 , t2 )c = (bt1 c, bt2 c)
def

bσi tc = σi btc
btcA→B = Tλx. bt dxeA cB UA→B
:

JA K → JbAc K

def

b(v1 , v2 )c = (bv1 c, bv2 c)
def

b(i, v)c = (i, bvc)
def

b?c = ?
bvcA→B
def

bAc → A

:

= Tw 7→ bv(dweA )cB UA→B

B.

=


X
bP c± + bQc±

=

0

def

bN c±

=

Y−

def



=

Y

bP → N c±

def

=

bP c± → bN c±

bN × M c±

def

bN c± × bM c±

b1c±
j
k
hP i−

def

±

=

=

1

def

bP c±

=

±

Proof outlines

Theorem 3 (βη is semantically sound). This is proved by direct induction on the evidence that t ≈βη u; semantic equivalence is a
congruence, and β-reduction and η-expansions are identities in the
semantic domain.
Theorem 4 (Semantic equivalence implies contextual equivalence).
For any model M and context ∅ ` C [] : 1 + 1, the closed term
C [M(t)] must have a normal form σi () by Lemma 1 (Inversion),
and C [M(u)] a normal form σj (). The semantic interpretation of
C [t] (technically, JC K(Jt KM ) for the natural semantics of contexts
with a hole) and of C [u] are equal by our assumption t ≈sem u and
the fact that semantic equality is a congruence. They are also are
respectively equal to (i, ?) and (j, ?) by Theorem 3 (βη is semantically sound), so we must have i = j. C [] is not separating.

def

d(t1 , t2 )e = (dt1 e, dt2 e)
def

def

Theorem 5 (Reification). We define reify(v) = dreify0 (bvcA )eA
using an (obvious) auxiliary function reify0 (v) on values at funless types, on which the inversion property is immediate; for
def
= Vλx. dt bxcA eB W reify( ) it is then proved using the fact that J K and b cA , d eA
commute.

dσi te = σi dte
d()e = ()

def

b cA

d eA

def

def

b()c = ()

def

def

dtebAc→bBc

d eA

:

JbAc K → JA K

def

d(v1 , v2 )e = (dv1 e, dv2 e)
def

d(i, v)e = (i, dve)
def

d?e = ?
dveA→B
def

= Vw 7→ dv(bwcA )eB WA→B

Lemma 2. By Theorem 3 (βη is semantically sound), we can
without loss of generality consider β-normal forms only. For the
fun-less reify0 ( ), direct induction proves reify0 (Jt K) = t on
normal-forms t – note that the fact that our types have no functions
is key to preserve the inductive invariant that our terms are closed,
necessary to use the inversion lemma to reason on the shape of t.
The result for reify( ) holds by commutation of J K and b cA ,
d eA .



Lemma 4 (Strong positive cut). By simultaneous induction on p
and t. In the variable case, it’s just a variable/variable substitution.
Theorem 8 (Completeness of saturation). The proof of Scherer and
Rémy (2015) can be reused almost as-is. It defines a rewriting relation from focused terms to saturated terms, that proceeds by moving let-bindings around: at any saturation point in some context
Γna ; Γ0na , it looks for all the negative neutral terms in t that would
be well-typed in Γna , Γ0na , and saturates over exactly those neutral
terms.
However, just selecting the neutral sub-terms of t does not make
a valid selection function. We also have to add enough neutrals
at each saturation step to respect the validity criterion; by the
subformula property, a finite number of neutrals always suffices,
so there exists a valid selection function with the neutral sub-terms
of t.
Finally, any selection function above this one also satisfies completeness. Introducing more neutrals either does not change the
term shape (after the next invertible phase) or exposes a neutral
proof of inconsistency (n : 0); in the latter case, more terms become βη-equivalent, which helps us proving our goal btcfoc ≈βη
bt0 cfoc .

V

Theorem 9 (Saturation). By induction on the derivation. In the base
case, the old context is empty so the result is trivial – there is no P
such that ∅ ⇓ hP i− . The induction case considers the application of
the SAT rule to deduce Γna ; Γ0na `sat let x̄ = n̄ in t : Qa . We have
to prove that any sub-derivation of t of the form Γna , Γ0na ; Γ00nak `sat
f k : Qak satisfies the expected property for any P .
If Γna ⇓ P , this is immediate by induction hypothesis. If we
have Γna , Γ0na ⇓ P but not Γna ⇓ P , then P is only provable
by a “new” neutral n using variables from Γ0na , so it is passed
to the selection function. By validity of the selection function
(Figure 7 (Specification of saturation selection functions)) we know
that some neutral n0 : P must then selected, so P occurs in the
positive context of the invertible term t. By Lemma 3 (Strong
decomposition of invertible phases) we thus have Γ00nak P as
required.
Lemma 5 (Saturated consistency). By (logical) completeness of
focusing it suffices to prove that there is no focused proof of
Γna ; ∅ `inv t : ∅ | 0.
By inversion on the possible derivations, we see that the invertible phase must be empty, and FOCLC - LET- POS is the only possible
choice of focusing: t is of the form let x = n in u with
Γna ` n ⇓ hQi−
Γna ; Q `inv u : ∅ | 0
Γna `foc let x = n in u : 0

Γna is saturated so Γna ⇓ hQi− implies Γna Q. But then, by
Lemma 4 (Strong positive cut), we know that u has a subterm
Γna `foc f : 0.
We have proved that any term in the judgment Γna `foc 0 has a
strictly smaller subterm itself in the judgment Γna `foc 0. There is
no such proof term.
V

Theorem 6 (Contextual equivalence implies semantic equivalence).
We prove the contrapositive: if Jt KM 6= Jt0 KM in some model
M, we build a discriminating context C [] in M. Our induction on a type A has a slightly stronger hypothesis. We assume
M(Γ) ` t, t0 : A(M) and Jt K 6= Jt0 K: the semantically distinct
terms are well-typed at the closed typing M(Γ) ` : Γ(A), but
need not be well-typed at Γ ` : A.
In the function case A → B we have an input w ∈ JA KM
where the two semantics differ, we build the discriminating context
C [( (reifyA (w)))], where C distinguishes at B by induction
hypothesis.
In the sum case, Jt KM is of the form (i, v) and Jt0 KM of
the form (j, v 0 ) and we have either i 6= j or v 6= v 0 . In the
second case, suppose for example i = j = 1, we use a context (match  with | σ1 x1 → C [x1 ] | σ2 x2 → σk ()), using
the fact that the return type 1 + 1 is inhabited to build a dummy
value for the unused branch (k ∈ {1, 2} is arbitrary).

Theorem 10 (Inconsistent canonicity). The inversible and saturation phase are purely type-directed, so f and f 0 necessarily use
the same term-formers during those phases. They could only differ on a neutral term, but they cannot contain a derivation of
the form Γna , Γ0na `s n ⇓ X − or Γna , Γ0na `s p ⇑ P as, by
Corollary 2 (Saturation), Γna , Γ0na would be saturated, which is incompatible with our assumption Γna ` 0 and Lemma 5 (Saturated
consistency).
Lemma 6 (Saturated inequivalence). By direct induction on t 
≈icc
t0 . In particular, the two side-conditions we mentioned are direct
consequences of the saturated term structure.
The fact that the x = n bindings are never redundant is a direct
consequence of the “new”-ness condition on saturated neutrals: n
cannot be added in Ξ in a future phase as it would not be new
anymore.
The fact that the context is consistent at the source of inequality is a consequence of Corollary 2 and Lemma 5 (Saturated
consistency).
Theorem 11 (Inequivalence in the model). We prove this by simultaneous induction on the inequivalence evidence for t0 
≈icc t00 ,
Γna | Σp `inv D0 [Γ0na | Ξ `ne p0 6= p0 0 : P ] : N | Qa and the
sub-terms of the two terms t1 , t01 , building inequivalence evidence
for t1 
≈icc t01 . There are three interesting cases: when the current term-former introduces a variable (x : X + ) in context (or at
the root for the variables of Γna , Σp ), the saturation step (where
non-redundancy is checked), and when the source of inequality
Γ0na | Ξ `ne p 6= p0 : P is finally encountered.
When we enter a binding x : X + , the corresponding subterms
of t1 , t01 start with a large pattern-matching on the possible values
of x : N (X + ). We decide to take the branch corresponding to
the case inFin (x), maintaining the inductive invariant that the subterms of t1 , t01 are equal to the sub-terms of t0 , t00 under the family
of substitutions ([inFin (x)/x])x , for all variables x of atomic type
introduced so far.
In a saturation step, we must check that the newly added
bindings are not already present in the constrained environment
Γna | Ξ. The neutrals introduced in t1 
≈icc t01 are of the form
n[inFin (x)/x]x , and this substitution preserves α-inequivalence,
as it replaces distinct variables by distinct values.
When we reach the source of inequality Γ0na | Ξ `ne p 6= p0 : P ,
the derivation of spine inequivalence Γ0na `ne p 6= p0 ⇑ P either
ends up on a Γ0na `ne σi p 6= σj p0 ⇑ P with i 6= j, in which case
the corresponding neutral subterms of t1 , t01 are also of this form,
or Γ0na `ne x 6= y ⇑ X + . In this case the subterms of t1 , t01 are
inFin (x), inFin (y), by our inductive invariant: they are also distinct
positive neutrals, and form a source of inequality.
At the source of inequality, we also have to prove that N t0 ,t00 (Γ0 ) 0 0
from the hypothesis Γ0 0 0. Note that this could be wrong if we applied some other model M; for example, the context (x : X + , y : Y + → 0)
is consistent, but applying the model {X + 7→ 1, Y + 7→ 1} results
in an inconsistent context.
Fortunately, the definition of the neutral model Definition 12
(Neutral model) is such that the positive atoms that become inhabited are exactly those that have bound variables in the context at the
source of inequality Γ0na ` p 
≈icc p0 P . And, by saturated consistency (Corollary 2 (Saturation)), we know that those positive atoms
are exactly those that are provable in Γ0na .

We can thus can prove N (Γ0na ) 0 0 by contradiction as follows.
Suppose we have a proof of N (Γ0na ) ` 0. Any subproof of the
form N (Γ0na ) ` N (X + ), for one of the X + inhabited in N , can
be replaced by a subproof of the form N (Γ0na ` X + ), as we know
that all such X + are derivable in Γ0na . The transformed proof does
not rely on the definition of the X + , so it is also a valid proof of
Γ0na ` 0, which is impossible.
Corollary 3 (Fun-elimination preserves semantic equivalence). This
is immediate from Lemma 8 and the fact that the functionelimination transformation is a bijection on semantics value – Figure 3 (Fun-less data types).
0

Theorem 12 (Canonicity). We remark that p[ρ] 
≈sem p [ρ] is a trivial property if P is a closed type (no atoms X + ): by inspecting the
Γ `ne p 6= p0 ⇑ P judgment (or the strong positive neutral structure), we know that p and p0 differ on a constructor, and this property is preserved by any substitution.
From Γ 0 ∅ we know that for any A ∈ Γ, A is inhabited by
some closed values – Corollary 1 (Inhabited or inconsistent). We
can always pick an arbitrary closed value of type A.
We build ρ by peeling off the variables of the environment Γ,
from the most recently introduced to the first introduced. At any
point during our induction, we have processed a fragment ∆0 of
the context, and ∆ remains unprocessed, with Γ = (∆, ∆0 ), and
we have a substitution ρ that binds the variables of ∆0 to closed
terms, such that Ξ[ρ] contains no inconsistent equation. Initially
def
def
def
we have ∆ = Γ, ∆0 = ∅, ρ = ∅.
0
When Γ is of the form Γ , x : A1 + A2 , we look for equations
of the form σi xi = x in Ξ; by validity of Ξ (Definition 13), there
is at most one. If there is none, we choose an arbitrary value for x
in ρ; if there is one, we choose xi [ρ]; this is a closed term as xi
must be defined after x in the context.
When Γ is of the form Γ0 , x : N , we look for equations the
family of equations (y i = ni [x])i∈I – remember that we write
n [x] when the neutral n has head x. Let us write Ξ [x] for this
set of equations about x.
We define the value for x in ρ as Val(x : N | (y i = ni )i∈I )
where Val(n : N | Ξ), defined below, is such that Ξ[Val(n : N | Ξ)/n]
always holds, if all equations in Ξ are of the form y = m [n].
def

Val(n : 1 | Ξ) = ()


Val(π1 n : N 1 | {(x = m [π1 n]) ∈ Ξ})
def 

,
Val(n : N 1 × N 2 | Ξ) =
Val(π2 n : N 2 | {(x = m [π2 n]) ∈ Ξ})
def

Val(n : hP i− | {y = n}) = y

def

Val(n : hP i− | ∅) = arbitrary

From the validity of Ξ, we know that Ξ [x] contains at most
one equation of the form (y : P ) = n for each possible neutral
` n ⇓ hP i− , which justifies the only two cases in the definition of
Val(n : hP i− | Ξ) above.
Corollary 4 (Canonicity). We use a stronger induction hypothesis
on the inequivalence judgment: if


Γ | Ξ `inv D Γ0 | Ξ0 `ne p 6= p0 : P : N | P a

then there is a substitution ρ : (Γ | Ξ) and a context C [] such as


∅ ` C [t[ρ]] 
≈β C t0 [ρ] : 1 + 1
def

def

where t = D [p] and t0 = D [p0 ].
def
In the base case D = , we get a substitution ρ : (Γ0 | Ξ0 )
from Theorem 12 (Canonicity); the theorem also gives us p[ρ] 
≈sem
p0 [ρ], so there is a distinguishing context C as required as contextual and semantic equivalence coincide.

In the sum-elimination case


Γ, x : P 1 + P 2 , xi : P i | Ξ, σi xi = x `inv D Γ0 | Ξ0 `ne p 6= p0 : P 0 : N | Qa


match x with


 Γ0 | Ξ0 `ne p 6= p0 : P 0 : N | Qa
σi xi → 
Γ, x : P 1 + P 2 | Ξ `inv 
σj xj6=i → t

the substitution ρ verifies, by inductive hypothesis, that σi xi [ρ] =
x[ρ], so in particular the sum-elimination term, once applied ρ, will
reduce to (D [p][ρ] and (D [p0 ])[ρ] respectively, as desired: this
means that the distinguishing context D for the premise is also a
distinguishing context for the sum-elimination terms.
In the (left) pair case


Γ | Ξ `inv D Γ0 | Ξ0 `ne p 6= p0 : P : N 1 | ∅
 0

Γ | Ξ `inv (D, u) Γ | Ξ0 `ne p 6= p0 : P : N 1 × N 2 | ∅

We can obviously keep the same ρ, and build the distinguishing
context C [π1 ], where C is the distinguishing context for the
inductive premise.
From this stronger inductive hypothesis (ρ, C), we can build a
distinguishing context for D [p] 
≈ctx D [p0 ] as
C [(λ(x1 . . . xn ∈ Γ). ) (x1 [ρ]) . . . (xn [ρ])]

def

def

Theorem 13 (Saturated terms are canonical). Let t0 = t and t00 =
t0 .
By Lemma 6 (Saturated inequivalence) we have Σp | ∅ `inv
D0 [Γ0na | Ξ `ne p0 6= p0 0 : P ] : N | Qa with t0 ≈icc D0 [p0 ]
≈icc t00 )
D0 [p0 6= p0 0 ].
and t00 ≈icc D0 [p0 0 ], that is, (t0 
0
We consider the neutral model N t0 ,t0 defined in Definition 12
def

def

(Neutral model). Let t1 = N (t0 ) and t01 = N (t00 ).
By Theorem 11 (Inequivalence in the model) we have (t0 
≈icc
t00 )
D1 [p1 6= p0 1 ], that is a inequivalence of terms at the atom≈icc t00 : N (N ) | N (Qa ) .
less judgments ∅; N (Σp ) `inv t0 
Using the focused function-elimination transformation of Figdef
def
ure 9 (Fun-less focused forms), let us define t2 = bt1 c and t02 =
0
bt1 c. By Lemma 7 (Function elimination preserves inequivalence)
≈icc t02 )
D2 [p2 6= p0 2 ], that is a saturated inequivawe get (t2 
lence at closed types without functions.
From Corollary 4 (Canonicity), we finally get D2 [p2 ] 
≈ctx
≈ctx t02 , a contextual inequivalence at closed
D2 [p0 2 ], that is t2 
types without functions. As contextual and semantic equivalence
coincide at closed types, this is equivalent to Jt2 K 6= Jt02 K, that is,
Jbt1 c K 6= Jbt01 c K.
By Corollary 3 (Fun-elimination preserves semantic equivalence),
we thus have that Jt1 K 6= Jt01 K at closed types, that is, Jt0 KN 6=
Jt00 KN , that is, t0 
≈sem(N ) t00 , that is, t0 
≈sem t0 , or equivalently
t0 
≈ctx t0 .
Corollary 5 (Contextual equivalence implies equality of saturated forms).
By contrapositive, we show that u 
≈icc u0 implies t 
≈ctx t0 . If we
0
0
had u 
≈icc u we would have bucfoc 
≈ctx bu cfoc by Theorem 13
(Saturated terms are canonical). As βη-equivalence implies contextual equivalence, we have t ≈ctx bucfoc and t0 ≈ctx bu0 cfoc , so
t
≈ctx t0 by transitivity.
Corollary 6 (). We know from Section 2 (Equivalences in the full
λ-calculus) that βη-equivalence implies contextual equivalence.
Conversely, we suppose t ≈ctx t0 and prove t ≈βη t0 .
By Theorem 7 (Completeness of focusing), there exists focused
forms u, u0 that erase to t, t0 (respectively) modulo βη; we can even
pick them in the subset with positive atoms only.
By Theorem 8 (Completeness of saturation), there exists saturated forms r, r0 that have the same erasures as u, u0 (respectively)
modulo βη, that is they erase to t, t0 modulo βη.

By Corollary 5 (Contextual equivalence implies equality of saturated forms), we have r ≈icc r0 . As the invertible commuting conversions are sound with respect with βη-equality, we have
brcfoc ≈βη br0 cfoc , that is, t ≈βη t0 .
Corollary 7 (). To test if two terms are equivalent, we invoke the focusing completeness result then the saturated completeness result,
and check if the normal form coincide modulo (≈icc ). Those two
transformations are computable and (≈icc ) is decidable, so equivalence is decidable.
Corollary 8 (). Our notion of semantic equivalence coincides with
βη and contextual equivalence, and only distinguishes terms using
sets isomorphic to closed types, which are all finitely inhabited.

