The exp-log normal form of types
Decomposing extensional equality and representing terms compactly
Danko Ilik

arXiv:1502.04634v4 [cs.LO] 30 Jun 2016

Inria & LIX, Ecole Polytechnique
91128 Palaiseau Cedex, France
danko.ilik@inria.fr

Abstract

1.

Lambda calculi with algebraic data types lie at the core of functional
programming languages and proof assistants, but conceal at least
two fundamental theoretical problems already in the presence of
the simplest non-trivial data type, the sum type. First, we do not
know of an explicit and implemented algorithm for deciding the
beta-eta-equality of terms—and this in spite of the first decidability
results proven two decades ago. Second, it is not clear how to decide
when two types are essentially the same, i.e. isomorphic, in spite of
the meta-theoretic results on decidability of the isomorphism.
In this paper, we present the exp-log normal form of types—
derived from the representation of exponential polynomials via the
unary exponential and logarithmic functions—that any type built
from arrows, products, and sums, can be isomorphically mapped
to. The type normal form can be used as a simple heuristic for
deciding type isomorphism, thanks to the fact that it is a systematic
application of the high-school identities.
We then show that the type normal form allows to reduce the
standard beta-eta equational theory of the lambda calculus to a
specialized version of itself, while preserving the completeness of
equality on terms.
We end by describing an alternative representation of normal
terms of the lambda calculus with sums, together with a Coqimplemented converter into/from our new term calculus. The difference with the only other previously implemented heuristic for
deciding interesting instances of eta-equality by Balat, Di Cosmo,
and Fiore, is that we exploit the type information of terms substantially and this often allows us to obtain a canonical representation
of terms without performing sophisticated term analyses.

The lambda calculus is a notation for writing functions. Be it simplytyped or polymorphic, it is also often presented as the core of modern
functional programming languages. Yet, besides functions as firstclass objects, another essential ingredient of these languages are
algebraic data types that typing systems supporting only the →-type
and polymorphism do not model directly. A natural model for the
core of functional languages should at least include direct support
for a simplest case of variant types, sums, and of records i.e. product
types. But, unlike the theory of the {→}-typed lambda calculus, the
theory of the {→, +, ×}-typed one is not all roses.

Introduction

Canonicity of normal terms and η-equality A first problem is
canonicity of normal forms of terms. Take, for instance, the term
λxy.yx of type τ + σ → (τ + σ → ρ) → ρ, and three of its η-long
representations,
λx.λy.yδ(x, z.ι1 z, z.ι2 z)
λx.λy.δ(x, z.y(ι1 z), z.y(ι2 z))
λx.δ(x, z.λy.y(ι1 z), z.λy.y(ι2 z)),
where δ is a pattern matching construct, i.e. a case-expression
analysing the first argument, with branches of the pattern matching
given via the variable z in the second and third argument.
These three terms are all equal with respect to the standard
equational theory =βη of the lambda calculus (Figure 1), but why
should we prefer any one of them over the others to be a canonical
representative of the class of equal terms?
Or, consider the following two terms of type (τ1 → τ2 ) →
(τ3 → τ1 ) → τ3 → τ4 + τ5 → τ2 (example taken from (Balat et al.
2004)):
λxyzu.x(yz)

Categories and Subject Descriptors Software and its engineering [Language features]: Abstract data types; Software and its
engineering [Formal language definitions]: Syntax; Theory of computation [Program constructs]: Type structures

λxyzu.δ(δ(u, x1 .ι1 z, x2 .ι2 (yz)), y1 .x(yy1 ), y2 .xy2 ).
These terms are βη-equal, but can one easily notice the equality? In
order to do so, since both terms are β-normal, one would need to do
non-trivial β- and η-expansions (see Example 2 in Section 4).
For the lambda calculus over the restricted language of types—
when the sum type is absent—these problems do not exist, since
β-normalization followed by an η-expansion is deterministic and
produces a canonical representative for any class of βη-equal terms.
Deciding =βη for that restricted calculus amounts to comparing
canonical forms up to syntactic identity.
In the presence of sums, we only have a notion of canonical interpretation of terms in the category of sheaves for the Grothendieck
topology over the category of constrained environments (Altenkirch
et al. 2001), as well as the sophisticated normal form of terms due to
Balat, Di Cosmo, and Fiore which is not canonical (unique) syntactically (Balat et al. 2004). Balat et al. also provide an implementation
of a type-directed partial evaluator that normalizes terms to their

Keywords sum type, eta equality, normal type, normal term, type
isomorphism, type-directed partial evaluation

[Copyright notice will appear here once ’preprint’ option is removed.]

1

2016/7/1

2.

normal form, and this represented up to now the only implemented
heuristic for deciding βη-equality—it is not a full decision procedure, because the normal forms are not canonical. We shall discuss
these and the other decidability results some more in Related work
of Section 5.
Treating full βη-equality is hard, even if, in practice, we often
only need to treat special cases of it, such as certain commuting
conversions.

The exp-log normal form of types

The trouble with sums starts already at the level of types. Namely,
when we consider types built from function spaces, products, and
disjoint unions (sums),
τ, σ ::= χi | τ → σ | τ × σ | τ + σ,
where χi are atomic types (or type variables), it is not always clear
when two given types are essentially the same one. More precisely,
it is not known how to decide whether two types are isomorphic (Ilik
2014). Although the notion of isomorphism can be treated abstractly
in Category Theory, in bi-Cartesian closed categories, and without
committing to a specific term calculus inhabiting the types, in the
language of the standard syntax and equational theory of lambda
calculus with sums (Figure 1), the types τ and σ are isomorphic
when there exist coercing lambda terms M : σ → τ and N : τ → σ
such that

Recognizing isomorphic types If we leave aside the problems of
canonicity of and equality between terms, there is a further problem
at the level of types that makes it hard to determine whether two
type signatures are essentially the same one. Namely, although for
each of the type languages {→, ×} and {→, +} there is a very
simple algorithm for deciding type isomorphism, for the whole of
the language {→, +, ×} it is only known that type isomorphism
is decidable when types are to be interpreted as finite structures,
and that without a practically implementable algorithm in sight (Ilik
2014).
The importance of deciding type isomorphism for functional
programming has been recognized early on by Rittri (Rittri 1991),
who proposed to use it as a criterium for searching over a library
of functional subroutines. Two types being isomorphic means that
one can switch programs and data back and forth between the types
without loss of information. Recently, type isomorphisms have also
become popular in the community around homotopy type theory.
It is embarrassing that there are no algorithms for deciding type
isomorphism for such an ubiquitous type system. Finally, even
if finding an implementable decision procedure for the full type
language {→, +, ×} were hard, might we simply be able to cover
fragments that are important in practice?

λx.M (N x) =βη λx.x

and

λy.N (M y) =βη λy.y.

In other words, data/programs can be converted back and forth
between τ and σ without loss of information.
The problem of isomorphism is in fact closely related to the
famous Tarski High School Identities Problem (Burris and Yeats
2004; Fiore et al. 2006). What is important for us here is that types
can be seen as just arithmetic expressions: if the type τ → σ is
denoted by the binary arithmetic exponentiation σ τ , then every
type ρ denotes at the same time an exponential polynomial ρ. The
difference with ordinary polynomials is that the exponent can now
also contain a (type) variable, while exponentiation in ordinary
polynomials is always of the form σ n for a concrete n ∈ N i.e.
σ n = σ × · · · × σ . Moreover, we have that
|
{z
}
n-times

+
τ ∼
= σ implies N  τ = σ,

that is, type isomorphism implies that arithmetic equality holds for
any substitution of variables by positive natural numbers.
This hence provides an procedure for proving non-isomorphism:
given two types, prove they are not equal as exponential polynomials,
and that means they cannot possibly be isomorphic. But, we are
interested in a positive decision procedure. Such a procedure exists
for both the languages of types {→, ×} and {×, +}, since then we
have an equivalence:
∼ σ iff N+  τ = σ.
τ =

Organization of this paper In this paper, we shall be treating
the two kinds of problems explained above simultaneously, not as
completely distinct ones: traditionally, studies of canonical forms
and deciding equality on terms have used very little of the type
information annotating the terms (with the exceptions mentioned in
the concluding Section 5).
We shall start by introducing in Section 2 a normal form for
types—called the exp-log normal form (ENF)—that preserves the
isomorphism between the source and the target type; we shall also
give an implementation, a purely functional one, that can be used as
a heuristic procedure for deciding isomorphism of two types.
Even if reducing a type to its ENF does not present a complete
decision procedure for isomorphism of types, we shall show in
the subsequent Section 3 that it has dramatic effects on the theory
of βη-equality of terms. Namely, one can reduce the problem of
showing equality for the standard =βη relation to the problem of
showing it for a new equality theory =eβη (Figure 2)—this later
being a specialization of =βη . That is, a complete axiomatization
of βη-equality that is a strict subset of the currently standard one is
possible.
In Section 4, we shall go further and describe a minimalist
calculus of terms—compact terms at ENF type—that can be used
as an alternative to the usual lambda calculus with sums. With its
properties of a syntactic simplification of the later (for instance,
there is no lambda abstraction), the new calculus allows a more
canonical representation of terms. We show that, for a number of
interesting examples, converting lambda terms to compact terms
and comparing the obtained terms for syntactic identity provides a
simple heuristic for deciding =βη .
The paper is accompanied by a prototype normalizing converter
between lambda- and compact terms implemented in Coq.

Indeed, in these cases type isomorphism can not only be decided, but
also effectively built. In the case of {×, +}, the procedure amounts
to transforming the type to disjunctive normal form, or the (nonexponential) polynomial to canonical form, while in that of {→, ×},
there is a canonical normal form obtained by type transformation
that follows currying (Rittri 1991).
Given that it is not known whether one can find such a canonical
normal form for the full language of types (Ilik 2014), what we can
hope to do in practice is to find at least a pseudo-canonical normal
form. We shall now define such a type normal form.
The idea is to use the decomposition of the binary exponential
function σ τ through unary exponentiation and logarithm. This is
a well known transformation in Analysis, where for the natural
logarithm and Euler’s number e we would use
σ τ = eτ ×log σ

also written σ τ = exp(τ × log σ).

The systematic study of such normal forms by Du Bois-Reymond
described in the book (Hardy 1910) served us as inspiration.
But how exactly are we to go about using this equality for
types when it uses logarithms i.e. transcendental numbers? Luckily,
we do not have to think of real numbers at all, because what is
described above can be seen through the eyes of abstract Algebra, in

2

2016/7/1

M, N ::= xτ | (M τ →σ N τ )σ | (π1 M τ ×σ )τ | (π2 M τ ×σ )σ | δ(M τ +σ , xτ1 .N1ρ , xσ2 .N2ρ )ρ |
|(λxτ .M σ )τ →σ | hM τ , N σ iτ ×σ | (ι1 M τ )τ +σ | (ι2 M σ )τ +σ
(λx.N )M =β N {M/x}

(β→ )

πi hM1 , M2 i =β Mi

(β× )

δ(ιi M , x1 .N1 , x2 .N2 ) =β Ni {M/xi }

(β+ )
x 6∈ FV(N )

N =η λx.N x
N =η hπ1 N , π2 N i

(η→ )
(η× )

N {M/x} =η δ(M, x1 .N {ι1 x1 /x}, x2 .N {ι2 x2 /x})

x1 , x2 6∈ FV(N )

(η+ )

Figure 1. Terms of the {→, +, ×}-typed lambda calculus and axioms of the equational theory =βη between typed terms.
exponential fields, as a pair of mutually inverse homomorphisms exp
and log between the multiplicative and additive group, satisfying
exp(τ1 + τ2 ) = exp τ1 × exp τ2

exp(log τ ) = τ

log(τ1 × τ2 ) = log τ1 + log τ2

log(exp τ ) = τ.

instance for the second example of Section 1:
(τ1 → τ2 ) → (τ3 → τ1 ) → τ3 → τ4 + τ5 → τ2 =

τ1 τ3 τ2 τ1
τ4 +τ5 τ3
=
τ2
τ
τ
τ 1 τ1 3 τ3 τ4

τ2 2

In other words, exp and log can be considered as macro expansions
rather than unary type constructors. Let us take the type τ + σ →
(τ + σ → ρ) → ρ from Section 1, assuming for simplicity that
τ, σ, ρ are atomic types. It can be normalized in the following way:


τ5 × τ3 × (τ3 → τ1 ) × (τ1 → τ2 ) → τ2 .
Of course, some care needs to be taken when applying the rewrite
rules, in order for the procedure to be deterministic, like giving precedence to the type rewrite rules and normalizing sub-expressions. To
be precise, we provide a purely functional Coq implementation below. This is just one possible implementation of the rewriting rules,
but being purely functional and structurally recursive (i.e. terminating) it allows us to understand the restrictions imposed on types in
normal form, as it proves the following theorem.

= exp((τ + σ) log[exp{exp((τ + σ) log ρ) log ρ}])
exp((τ + σ) log[exp{exp(τ log ρ) exp(σ log ρ) log ρ}])
exp((τ + σ) exp(τ log ρ) exp(σ log ρ) log ρ)

Theorem 1. If τ is a type in exp-log normal form, then τ ∈ ENF,
where

exp τ exp(τ log ρ) exp(σ log ρ) log ρ)

exp(σ exp(τ log ρ) exp(σ log ρ) log ρ =
τ σ

ρ

ENF 3 e ::= c | d,

τ σ

ρσρ

ρ

where

= (τ ×(τ → ρ)×(σ → ρ) → ρ)×(σ×(τ → ρ)×(σ → ρ) → ρ).
As the exp-log transformation of arrow types is at the source
of this type normalization procedure, we call the obtained normal
form the exp-log normal form (ENF). Be believe the link to abstract
algebra is well work keeping in mind, since it may give rise to
further cross-fertilization between mathematics and the theory of
programming languages. However, from the operational point of
view, all this transformation does is that it prioritized and orients
the high-school identities,
(f + g) + h

f + (g + h)

(1)

(f g)h
f (g + h)

f (gh)
fg + fh

(2)
(3)

(f + g)h

f h + gh

(4)

f g+h

f gf h

(5)

h

f h gh

(6)

hg

(7)

(f g)

g h

(f )

=


= τ4 × τ3 × (τ3 → τ1 ) × (τ1 → τ2 ) → τ2 ×

τ + σ → (τ + σ → ρ) → ρ =
 τ +σ τ +σ
= ρρ
=

= ρτ ρ

τ
τ
τ 1 τ1 3 τ3 τ5

τ2 2

f

,

DNF 3 d, di ::= c1 + (c2 + (· · · + n) · · · )

n≥2

CNF 3 c, ci ::= (c1 → b1 ) × (· · · × (cn → bn ) · · · )
Base 3 b, bi ::= p | d,

n≥0

and p denotes atomic types (type variables).
Assuming a given set of atomic types,
Parameter Proposition : Set.
the goal is to map the unrestricted language of types, given by the
inductive definition,1
Inductive Formula : Set :=
| prop : Proposition → Formula
| disj : Formula → Formula → Formula
| conj : Formula → Formula → Formula
| impl : Formula → Formula → Formula.
1 May

the reader to forgive us for the implicit use of the Curry-Howard
correspondence in the Coq code snippets, where we refer to types and type
constructors as formulas and formula constructors.

all of which are valid as type isomorphisms. We can thus also
compute the isomorphic normal form of the type directly, for

3

2016/7/1

into the exp-log normal form which fits in the following inductive
signature.

| two c0 c1 ⇒ dnf (two (ntimes c c0) (ntimes c c1))
| dis c0 d0 ⇒ dnf match distrib0 c d0 with
| cnf c1 ⇒ two (ntimes c c0) c1
| dnf d1 ⇒ dis (ntimes c c0) d1
end
end.

Inductive CNF : Set :=
| top
| con : CNF → Base → CNF → CNF
with DNF : Set :=
| two : CNF → CNF → DNF
| dis : CNF → DNF → DNF
with Base : Set :=
| prp : Proposition → Base
| bd : DNF → Base.

Definition distrib1 (c : CNF)(e : ENF) : ENF :=
match e with
| cnf a ⇒ cnf (ntimes c a)
| dnf b ⇒ distrib0 c b
end.
Fixpoint explog0 (d : Base)(d2 : DNF) {struct d2} : CNF
:=
match d2 with
| two c1 c2 ⇒ ntimes (con c1 d top) (con c2 d top)
| dis c d3 ⇒ ntimes (con c d top) (explog0 d d3)
end.

Inductive ENF : Set :=
| cnf : CNF → ENF
| dnf : DNF → ENF.
The con c1 b c2 constructor corresponds to bc1 c2 or the type
(c1 → b) × c2 from Theorem 1. The normalization function, enf (·),

Definition explog1 (d : Base)(e : ENF) : CNF :=
match e with
| cnf c ⇒ con c d top
| dnf d1 ⇒ explog0 d d1
end.

Fixpoint enf (f : Formula) {struct f } : ENF :=
match f with
| prop p ⇒ cnf (p2c p)
| disj f0 f1 ⇒ dnf (nplus (enf f0) (enf f1))
| conj f0 f1 ⇒ distrib (enf f0) (enf f1)
| impl f0 f1 ⇒ cnf (explogn (enf2cnf (enf f1)) (enf f0))
end.

Fixpoint distribn (d : DNF)(e2 : ENF) {struct d} : ENF
:=
match d with
| two c c0 ⇒ dnf (nplus (distrib1 c e2) (distrib1 c0 e2))
| dis c d0 ⇒ dnf (nplus (distrib1 c e2) (distribn d0 e2))
end.

is defined using the following fixpoints:

Definition distrib (e1 e2 : ENF) : ENF :=
match e1 with
| cnf a ⇒ distrib1 a e2
| dnf b ⇒ distribn b e2
end.

nplus which makes a flattened n-ary sum out of two given n-ary
sums, i.e. implements the +-associativity rewriting (1),
ntimes which is analogous to ‘nplus’, but for products, implementing (2),
distrib which performs the distributivity rewriting, (3) and (4), and

Fixpoint explogn (c:CNF)(e2:ENF) {struct c} : CNF :=
match c with
| top ⇒ top
| con c1 d c2 ⇒
ntimes (explog1 d (distrib1 c1 e2)) (explogn c2 e2)
end.

explogn which performs the rewriting involving exponentiations,
(5), (6), and (7).
Fixpoint nplus1 (d : DNF)(e2 : ENF) {struct d} : DNF :=
match d with
| two c c0 ⇒ match e2 with
| cnf c1 ⇒ dis c (two c0 c1)
| dnf d0 ⇒ dis c (dis c0 d0)
end
| dis c d0 ⇒ dis c (nplus1 d0 e2)
end.

Definition p2c : Proposition → CNF :=
fun p ⇒ con top (prp p) top.
Definition b2c : Base → CNF :=
fun b ⇒
match b with
| prp p ⇒ p2c p
| bd d ⇒ con top (bd d) top
end.

Definition nplus (e1 e2 : ENF) : DNF :=
match e1 with
| cnf a ⇒ match e2 with
| cnf c ⇒ two a c
| dnf d ⇒ dis a d
end
| dnf b ⇒ nplus1 b e2
end.

Fixpoint enf2cnf (e:ENF) {struct e} : CNF :=
match e with
| cnf c ⇒ c
| dnf d ⇒ b2c (bd d)
end.

Fixpoint ntimes (c1 c2 : CNF) {struct c1} : CNF :=
match c1 with
| top ⇒ c2
| con c10 d c13 ⇒ con c10 d (ntimes c13 c2)
end.

From the inductive characterization of the previous theorem, it
is immediate to notice that the exp-log normal form (ENF) is in fact
a combination of disjunctive- (DNF) and conjunctive normal forms
(CNF), and their extension to also cover the function type. We shall
now apply this simple and loss-less transformation of types to the
equational theory of terms of the lambda calculus with sums.

Fixpoint distrib0 (c : CNF)(d : DNF) : ENF :=
match d with

4

2016/7/1

3. βη -Congruence classes at ENF type

to compacting the βη-congruence class to a single point, a canonical
normal term of type enf (τ ).
Assuming τ, σ, τi are base types, the canonical representatives
for the two βη-congruence classes of Section 1 are

The virtue of type isomorphisms is that they preserve the equational
theory of the term calculus: an isomorphism between τ and σ is
witnessed by a pair of lambda terms
T :σ→τ

hλx.(π1 (π2 x))(π1 x), λx.(π2 (π2 x))(π1 x)i

S:τ →σ

and

such that

and

λx.T (Sx) =βη λx.x and λy.S(T y) =βη λy.y.
Therefore, when τ ∼
= σ, and σ happens to be more canonical than τ —
in the sense that to any βη-equivalence class of type τ corresponds
a smaller one of type σ—one can reduce the problem of deciding
βη-equality at τ to deciding it for a smaller subclass of terms.

hλx.(π1 x)((π1 π2 x)(π1 π2 π2 x)), λx.(π1 x)((π1 π2 x)(π1 π2 π2 x))i.
Note that, unlike (Balat et al. 2004), we do not need any sophisticated term analysis to derive a canonical form in this kind of cases.
One may either apply the standard terms witnessing the isomorphisms by hand, or use our normalizer described in Section 4.
The natural place to pick a canonical representative is thus the
βη-congruence class of terms at the normal type, not the class at
the original type! Moreover, beware that even if it may be tempting
to map a canonical representative along isomorphic coercions back
to the original type, the obtained representative may not be truly
canonical since there is generally more than one way to specify the
terms S and T that witness a type isomorphism.
Of course, not always can all sum types be eliminated by type
isomorphism, and hence not always can a class be compacted to a
single point in that way. Nevertheless, even in the case where there
are still sums remaining in the type of a term, the ENF simplifies
the set of applicable =βη -axioms.
We can use it to get a restricted set of equations, =eβη , shown
in Figure 2, which is still complete for proving full βη-equality, as
made precise in the following theorem.

S

τ

σ
T
T
S
In the case when σ = enf (τ ), the equivalence classes at type σ will
not be larger than their original classes at τ , since the main effect of
the reduction to exp-log normal form is to get rid of as many sum
types on the left of an arrow as possible, and it is known that for the
{×, →}-typed lambda calculus one can choose a single canonical
η-long β-normal representative out of a class of βη-equal terms.
Thus, from the perspective of type isomorphisms, we can observe the partition of the set of terms of type τ into =βη -congruence
classes as projected upon different parallel planes in three dimensional space, one plane for each type isomorphic to τ . If we choose
to observe the planes for τ and enf (τ ), we may describe the situation by the following figure.

ype

=β

Theorem 2. Let P, Q be terms of type τ and let S : τ →
enf (τ ) , T : enf (τ ) → τ be a witnessing pair of terms for
the isomorphism τ ∼
= enf (τ ). Then, P =βη Q if and only if
SP =eβη SQ and if and only if T (SP ) =βη T (SQ).

τ

Proof. Since the set of terms of ENF type is a subset of all typable
terms, it suffices to show that all =βη -equations that apply to terms
of ENF type can be derived already by the =eβη -equations.
Notice first that ηλe and ηπe are special cases of η+ , so, in fact,
the only axiom missing from =eβη is η+ itself,

at t
ses
s
a
cl
η-

N {M/x} =eη δ(M, x1 .N {ι1 x1 /x}, x2 .N {ι2 x2 /x})
(x1 , x2 6∈ FV(N )),

ses

=β

as
-cl

at

nf
ee

(τ )

when N is of type c; the case of N of type d is covered directly by
e
the η+
-axiom. We thus show that the η+ -axiom is derivable from
the =eβη -ones by induction on c.

typ

η

Case for N of type (c → b) × c0 .

The dashed circle depicts the compaction, if any, of a congruence
class achieved by coercing to ENF type. The single point depicts
the compaction to a singleton set, the case where a unique canonical
representative of a class of βη-terms exists.
We do not claim that the plane of enf (τ ) is always the best
possible plane to choose for deciding =βη . Indeed, for concrete
base types there may well be further type isomorphisms to apply
(think of the role of the unit type 1 in (1 → τ + σ) → ρ) and hence
a better plane than the one for enf (τ ). However, it is a reasonably
good default choice.
For the cases of types where the sum can be completely eliminated, such as the two examples of Section 1, the projection amounts

N {M/x}
e
=eη hπ1 (N {M/x}), π2 (N {M/x})i by η×
=h(π1 N ){M/x}, (π2 N ){M/x}i
=eη hδ(M, x1 .(π1 N ){ι1 x1 /x}, x2 .(π1 N ){ι2 x2 /x}),
δ(M, x1 .(π2 N ){ι1 x1 /x}, x2 .(π2 N ){ι2 x2 /x})i by IH
=eβη hπ1 (δ(M, x1 .N {ι1 x1 /x}, x2 .N {ι2 x2 /x})),
π2 (δ(M, x1 .N {ι1 x1 /x}, x2 .N {ι2 x2 /x}))i by ηπe
e
=eη δ(M, x1 .N {ι1 x1 /x}, x2 .N {ι2 x2 /x}) by η×

5

2016/7/1

M, N ::= xe | (M c→b N c )b | (π1 M (c→b)×c0 )c→b | (π2 M (c→b)×c0 )c0 | δ(M c+d , xc1 .N1e , xd2 .N2e )e
| (λxc .M b )c→b | hM b→c , N c0 i(b→c)×c0 | (ι1 M c )c+d | (ι2 M d )c+d
(λxc .N b )M =eβ N {M/x}

e
(β→
)

πi hM1b→c , M2c0 i =eβ Mi

e
(β×
)

δ(ιi M , x1 .N1 , x2 .N2 )e =eβ Ni {M/xi }

e
(β+
)

N c→b =eη λx.N x
N

(c→b)×c0

=eη

d

=eη
=eη

b

N {M /x}
πi δ(M, x1 .N1 , x2 .N2 )

x 6∈ FV(N )

e
(η→
)
e
(η×
)

hπ1 N , π2 N i
δ(M, x1 .N {ι1 x1 /x}, x2 .N {ι2 x2 /x})

b

x1 , x2 6∈ FV(N )

δ(M, x1 .πi N1 , x2 .πi N2 )c

e
(η+
)

(ηπe )

λy.δ(M, x1 .N1 , x2 .N2 ) =eη δ(M, x1 .λy.N1 , x2 .λy.N2 )c→b

y 6∈ FV(M )

(ηλe )

Figure 2. Lambda terms of ENF type and the equational theory =eβη .
Case for N of type c → b.
N {M/x}
=eη λy.(N {M/x})y

the two term calculi. First, we represent the usual lambda calculus
with sums.

e
by η→

Inductive ND : list Formula → Formula → Set :=
| hyp : ∀ {Gamma A},
ND (A :: Gamma) A
| wkn : ∀ {Gamma A B},
ND Gamma A → ND (B :: Gamma) A
| lam : ∀ {Gamma A B},
ND (A :: Gamma) B → ND Gamma (impl A B)
| app : ∀ {Gamma A B},
ND Gamma (impl A B) → ND Gamma A → ND Gamma B
| pair : ∀ {Gamma A B},
ND Gamma A → ND Gamma B → ND Gamma (conj A B)
| fst : ∀ {Gamma A B},
ND Gamma (conj A B) → ND Gamma A
| snd : ∀ {Gamma A B},
ND Gamma (conj A B) → ND Gamma B
| inl : ∀ {Gamma A B},
ND Gamma A → ND Gamma (disj A B)
| inr : ∀ {Gamma A B},
ND Gamma B → ND Gamma (disj A B)
| cas : ∀ {Gamma A B C},
ND Gamma (disj A B) →
ND (A :: Gamma) C → ND (B :: Gamma) C →
ND Gamma C.

= λy.(N y){M/x} for y 6∈ FV (N {M/x})
e
=eη λy.δ(M, x1 .(N y){ι1 x1 /x}, x2 .(N y){ι2 x2 /x}) by η+
e
=η δ(M, x1 .(λy.N y){ι1 x1 /x}, x2 .(λy.N y){ι2 x2 /x}) by ηλe
e
=eη δ(M, x1 .N {ι1 x1 /x}, x2 .N {ι2 x2 /x}) by η→

The transformation of terms to ENF type thus allows to simplify
the (up to now) standard axioms of =βη . The new axioms are
complete for =βη in spite of them being only special cases of
the old ones. A notable feature is that we get to disentangle the lefthand side and right-hand side of the equality axioms: for instance,
the right-hand side of β→ -axiom can no longer overlap with the
left-hand side of the η+ -axiom, due to typing restrictions on the
term M .
One could get rid of ηπe and ηλe if one had a version of λcalculus resistant to these permuting conversions. The syntax of
such a lambda calculus would further be simplified if, instead of
binary, one had n-ary sums and products. In that case, there would
be no need for variables of sum type at all (currently they can only
be introduced by the second branch of δ). We would in fact get a
calculus with only variables of type c → b, and that would still
be suitable as a small theoretical core of functional programming
languages.

4.

The constructors are self-explanatory, except for hyp and wkn, which
are in fact used to denote de Bruijn indices: hyp denotes 0, while
wkn is the successor. For instance, the term λxyz.y is represented
as lam (lam (lam (wkn hyp))) i.e. lam (lam (lam 1)).
DeBruijn indices creep in as the simplest way to work with
binders in Coq, and although they may reduce readability, they solve
the problem with α-conversion of terms.
Next is our compact representation of terms, defined by the
following simultaneous inductive definition of terms at base type
(HSb), together with terms at product type (HSc). These later are
simply finite lists of HSb-terms.

A compact representation of terms at ENF type

It is the subject of this section to show that the desiderata for a
more canonical calculus from the previous paragraph can in fact be
achieved. We shall define a new representation of lambda terms, that
we have isolated as the most compact syntax possible during the
formal Coq development of a normalizer of terms at ENF type. The
description of the normalizer itself will be left for the second part
of this section, Subsection 4.1. In the first part of the section, we
shall demonstrate the value of representing terms in our calculus on
a number of examples. Comparing our normal form for syntactical
identity provides a first such heuristic for deciding =βη in the
presence of sums.
Before we continue with the presentation of the new calculus, for
the sake of precision, we give the formal representation of terms of

Inductive HSc : CNF → Set :=
| tt : HSc top
| pair : ∀ {c1 b c2}, HSb c1 b → HSc c2 → HSc (con c1 b c2)

6

2016/7/1

follows:
with HSb : CNF → Base → Set :=
| app : ∀ {p c0 c1 c2},
HSc (explogn c1 (cnf (ntimes c2 (con c1 (prp p) c0)))) →
HSb (ntimes c2 (con c1 (prp p) c0)) (prp p)
| cas : ∀ {d b c0 c1 c2 c3},
HSc (explogn c1 (cnf (ntimes c2 (con c1 (bd d) c0)))) →
HSc (explogn (explog0 b d)
(cnf (ntimes c3 (ntimes c2 (con c1 (bd d) c0))))) →
HSb (ntimes c3 (ntimes c2 (con c1 (bd d) c0))) b
| wkn : ∀ {c0 c1 b1 b},
HSb c0 b → HSb (con c1 b1 c0) b
| inl two : ∀ {c0 c1 c2},
HSc (explogn c1 (cnf c0)) → HSb c0 (bd (two c1 c2))
| inr two : ∀ {c0 c1 c2},
HSc (explogn c2 (cnf c0)) → HSb c0 (bd (two c1 c2))
| inl dis : ∀ {c0 c d},
HSc (explogn c (cnf c0)) → HSb c0 (bd (dis c d))
| inr dis : ∀ {c0 c d},
HSb c0 (bd d) → HSb c0 (bd (dis c d)).

c0 ⇒ (c1 → b1 ) × · · · × (cn → bn ) ≡
(c1 × c0 → b1 ) × · · · × (cn × c0 → bn )
(c1 + · · · + cn ) ⇒ b ≡ (c1 → b) × · · · × (cn → b)
Note that the usage of d ⇒ b in the typing rule for δ allows the
number of premises contained in Q to be determined by the size
of the sum d.
The typing rules also rely on a implicit variable convention, where a
variable xn actually denotes the variable whose deBruijn index is n
(we start counting from 0).
Variables as deBruijn indices: The variable xn in the rules for
xn P and δ(xn P, Q) represent the hypothesis c1 → p and
c1 → d. For concrete c2 , c3 , the subscript n means that the
variable represents the n-th hypothesis of the form c → b,
counting from left to right and starting from 0, in the context of
the term P , or the n + 1-st, in the context of the term Q.
We shall motivate our syntax in comparison to the syntax of the
lambda calculus from Figure 2, by considering in order all term
constructors of the later.

For a more human-readable notation of our calculus, we are
going to use the following one,
P, Q ::= hM1 , . . . , Mn i

xe Since e ∈ ENF, either e = c ∈ CNF or e = d ∈ DNF.
Variables of type d only appear as binders in the second branch
of δ, so if we have n-ary instead of binary δ’s, the only type a
variable x could have will be a c. But, since c is always of the
form (c1 → b1 ) × · · · × (cn → bn ), a variable xc could be
written as a tupple of n variables xi of types ci → bi . Moreover,
as we want our terms to always be η-expanded, and ci → bi is
an arrow type, we will not have a separate syntactic category of
terms for variables xi in the new calculus, but they will rather
be encoded/merged with either the category of applications
xi P (when b is an atomic type p), or the category of case
analysis δ(xi P, Q) (when b ∈ DNF), the two new constructors
explained below.

(n ≥ 0)

M, Mi ::= xn P | δ(xn P, Q) | wM | ι1 P | ι2 P | ι01 P | ι02 M,
with typing rules as follows:
M1 : (c1 ` b1 ) · · · Mn : (cn ` bn )
hM1 , . . . , Mn i : (c1 → b1 ) × · · · × (cn → bn )
P : (c2 × (c1 → p) × c0 ⇒ c1 )
xn P : (c2 × (c1 → p) × c0 ` p)
P : (c2 × (c1 → d) × c0 ⇒ c1 )
Q : (c3 × c2 × (c1 → d) × c0 ⇒ (d ⇒ b))
δ(xn P, Q) : (c3 × c2 × (c1 → d) × c0 ` b)

M c→b N c We shall only need this term constructor at type b = p,
since if b ∈ DNF the term M N would not be η-long (we want it
to be represented by a δ(M N, · · · )). As we realized during our
Coq development, we shall only need the case M = x, as there
will be no other syntactic element of type c → p (there will be
no projections πi left, while the δ will only be necessary at type
b). In particular, the application xhi can be used to represent the
old category of variables, where hi is the empty tupple of unit
type 1 (the nullary product).

M : (c0 ` b)
wM : ((c1 → b1 ) × c0 ` b)
P : (c0 ⇒ c1 )
ι1 P : (c0 ` c1 + c2 )
P : (c0 ⇒ c)
ι01 P : (c0 ` c + d)

P : (c0 ⇒ c2 )
ι1 P : (c0 ` c1 + c2 )

(π1 M (c→b)×c0 )c→b If M is η-expanded, as we want all terms to
be, this term would only create a β-redex, and so will not be a
part of the new syntax, as we are building a syntax for β-normal
and η-long terms.

M : (c0 ` d)
.
ι02 M : (c0 ` c + d)

The typing rules above involve two kinds of typing judgments.

(π2 M (c→b)×c0 )c0 When product types are represented as n-ary,
the same reasoning as for π1 applies, so π2 will not be part of
the new syntax.

Judgments at base type: Denoted M : (c ` b), this is the main
judgment kind, the conclusion of all but the first typing rule.
It says that M is a term of type b (i.e. either an atomic p or a
disjunction type d) in the typing context c. This context c takes
over the place of the usual context Γ and allows only hypotheses
(variables) of type ci → bi to be used inside the term M .

δ(M c+d , xc1 .N1e , xd2 .N2e )e This constructor is only needed at the
e
type e = b, a consequence of the fact that the η+
-axiom is
e
e
specialized to type b: the axioms ηπ and ηλ will not expressible
in the new syntax, since it will not contain πi , as we saw, and it
will not contain λ, as we shall see. We will also only need the
scrutinee M to be of the form xN , like it the case of application;
this additional restriction was not possible to see upfront, but
only once we used Coq to analyze the terms needed for the
normalizer.
The new constructor δ(xn P, Q) is thus like the old δ(xn P, · · · ),
except that Q regroups in the form of an n-ary tupple all the

Judgments at product type: Denoted P : c or Q : c, this kind of
judgment is only the conclusion of the first typing rule, whose
sole purpose is to make a tupple of base type judgments.
However, the judgments at product type are used as hypotheses
in the other typing rules, where their role is to allow n premises
to the typing rule. For this usage, they are disguised as the macroexpansions c1 ⇒ c2 or c ⇒ (d ⇒ b). Implemented by the Coq
fixpoints explogn and explog1, these macro expansions work as

7

2016/7/1

Example 2. This is the second example from the introduction
(Example 6.2.4.2 from (Balat et al. 2004)). The βη-equal terms

possible branches of the pattern matching (sum types will also
be n-ary, not binary like before).
(λxc .M b )c→b This terms constructor is already severely restricted
(for instance only one variable x can be abstracted), thanks to the
restrictions on the left- and right-hand sides of the function type.
But, as we found out during the Coq development, somewhat
to our surprise, there is no need for λ-abstraction in our syntax.
When reverse-normalizing from our calculus to the standard
lambda calculus (see the six examples below), λ’s can be
reconstructed thanks to the typing information.
hM

b→c

λxyzu.x(yz)

(13)

λxyzu.δ(u, x1 .x(yz), x2 .x(yz))

(14)

λxyzu.δ(u, x1 .δ(ι1 z, y1 .x(yy1 ), y2 .xy2 ),
x2 .δ(ι2 yz, y1 .x(yy1 ), y2 .xy2 ))

(15)

λxyzu.δ(δ(u, x1 .ι1 z, x2 .ι2 (yz)), y1 .x(yy1 ), y2 .xy2 )

c0 (b→c)×c0

This constructor will be maintained, corre,N i
sponding to the only typing rule with conclusion a judgment
of product type, but it will become n-ary, hM1 , . . . , Mn i. In
particular, we may have the nullary tupple hi of the null product
type (i.e. unit type 1).

(16)

at type
(a → b) → (c → a) → c → (d + e) → b,
are all normalized to the compact term
hx3 (x2 x1 ), x3 (x2 x1 )i

(ι1 M c )c+d , (ι2 M d )c+d These constructors will be maintained, but
will be duplicated: the new ι1 , ι2 will only be used to construct
a binary sum c1 + c2 (this is the base case of sum constructors
which must be at least binary by construction), while the ι01 , ι02
will be used to construct sums of the form c + d.

(17)

at the ENF type
(d × c × (c → a) × (a → b) → b)×
(e × c × (c → a) × (a → b) → b),
which can then be reverse-normalized to (14), if desired.

We shall now show a number of examples that our compact
term representation manages to represent canonically. We will also
show cases when βη-equality can not be decided using bringing
terms to the compact normal form. For simplicity, all type variables
(a, b, c, d, e, f, g, p, q, r, s, i, j, k, l) are assumed to be of atomic
type, none of them denoting members of Base, CNF, and DNF,
anymore, and for the rest of this subsection.

A reviewer once remarked that the two previous examples can
be handled just by a CPS transformation. While our implementation
will be based on continuations, the reason why these examples are
handled by our method are not continuations, but rather the fact that
all sum types can be eliminated, allowing us to choose a canonical
term in the compact representation of the {→, ×}-typed lambda
calculus.

Convention 1. We shall adopt the convention of writing the type
1 → p as p (1 is the unit type i.e. the nullary product type), writing
the application to a nullary pair xn hi as xn , and writing a singleton
pair hM i as just M . Hence, for instance, an application of some
term M to a singleton pair, containing an application of a term N to
a nullary pair, M hN hii, will be written as the more readable M N
corresponding to the usual λ-calculus intuitions.

Example 3 (Commuting conversions). The left and right hand sides
of the common commuting conversions,
λxyzu.δ(u, v1 .yv1 , v2 .zv2 )x =βη
=βη λxyzu.δ(u, v1 .(yv1 )x, v2 .(zv2 )x),
λxyzuv.δ(δ(x, x1 .yx1 , x2 .zx2 ), w1 .uw1 , w2 .vw2 ) =βη
=βη λxyzuv.δ(x, x1 .δ(yx1 , w1 .uw1 , w2 .vw2 ),
x2 .δ(zx2 , w1 .uw1 , w2 .vw2 ))

Example 1. This is the first example from the introduction, concerning the relative positions of λ’s, δ’s, and applications. The βη-equal
terms
λx.λy.yδ(x, z.ι1 z, z.ι2 z)
λx.λy.δ(x, z.y(ι1 z), z.y(ι2 z))

(8)
(9)

λx.δ(x, z.λy.y(ι1 z), z.λy.y(ι2 z))

(10)

λx.λy.yx

(11)

(18)

(19)

of types
s → (p → s → r) → (q → s → r) → (p + q) → r
and
(p + q) → (p → r + s) → (q → r + s) →
(r → a) → (s → a) → a,

at type

are normalized to the compact terms

(p + q) → ((p + q) → r) → r,

hx2 hx3 , x0 i, x1 hx3 , x0 ii,

are all normalized to the same canonical representation
hx0 x2 , x1 x2 i

(18’)

of ENF type
(12)

(p × (s × q → r) × (s × p → r) × s → r)×
(q × (s × q → r) × (s × p → r) × s → r)

at the ENF type

and

((p → r) × (q → r) × p → r)×
((p → r) × (q → r) × q → r)

hδ(x3 x4 , hx2 x0 , x1 x0 i), δ(x2 x4 , hx2 x0 , x1 x0 i)i,

(19’)

of ENF type

which can be reverse-normalized back to (9). However, the point
is not that (9) is somehow better than the other 3 terms, but that a
canonical representation should be sought at the ENF type, not the
original type! This remark is valid in general, and in particular for
the other examples below.

((s → a) × (r → a) × (q → r + s) × (p → r + s) × p → a)
× ((s → a) × (r → a) × (q → r + s) × (p → r + s) × q → a),
which can be reverse-normalized to the right-hand sides of (18), and
(19), respectively, if desired.

8

2016/7/1

Example 4 (Eta equations). Both the left- and the right-hand sides
of the eta rules (represented as closed terms),
λx.x =βη λxy.xy
λx.x =βη λx.hπ1 x, π2 xi

of type
(f → g) → (h → g) → i → (i → f + h) → g

(20)
(21)

are normalized to two different compact representations:

λxy.xy =βη λxy.δ(y, x1 .x(ι1 x1 ), x2 .x(ι2 x2 ))
(22)
λxyz.δ(z, z1 .λu.xz1 , z2 .λu.yz2 ) =βη λxyzu.δ(z, z1 .xz1 , z2 .yz2 )
(23)

(i → f + h) × i × (h → g) × (f → g) → g

Example 6. The following βη-equal terms,

of types

((p + q) → r) → ((p + q) → r)
(p → s) → (q → s) → (p + q) → r → s

(22)
(23)

(p → s × r) → (q → s × r) → (p + q) → s

(24)

(p → s × r) → (q → s × r) → (p + q) → r

(25)

(27’)

which can then be reverse-normalized to the starting lambda terms
themselves.

λxyz.π2 δ(z, z1 .xz1 , z2 .yz2 ) =βη λxyz.δ(z, z1 .π2 xz1 , z2 .π2 yz2 )
(25)
(20)
(21)

(26’)

of ENF type

λxyz.π1 δ(z, z1 .xz1 , z2 .yz2 ) =βη λxyz.δ(z, z1 .π1 xz1 , z2 .π1 yz2 )
(24)

(p → p) → (p → p)
(p × q) → (p × q)

δ(x0 x1 , hx4 x0 , x3 x0 i)
δ(x0 x1 , hδ(x1 x2 , hx5 x0 , x4 x0 i), x3 x0 i),

λxyzuv.δ(zv, x1 .ι1 x, x2 .δ(uv, y1 .ι2 y, y2 .ι1 x))

(28)

λxyzuv.δ(uv, y1 .δ(zv, x1 .ι1 x, x2 .ι2 y), y2 .ι1 x),

(29)

of type
k → l → (f → g + h) → (f → i + j) → f → k + l
are normalized to two different compact representations:

are mapped to the same compact term

hδ(x2 x0 , hι1 x5 , δ(x3 x1 , hι2 x5 , ι1 x6 i)i)i

(28’)

hδ(x1 x0 , hδ(x2 x1 , hι1 x6 , ι2 x5 i), ι1 x5 i)i,

(29’)

of ENF type

x1 x0

(20’)

hx0 , x1 i

(21’)

f × (f → i + j) × (f → g + h) × l × k → k + l

hx1 x0 , x2 x0 i
hx3 x1 , x2 x1 i

(22’)
(23’)

which can then be reverse-normalized to the starting lambda terms
themselves.

hx3 x0 , x1 x0 i
hx4 x0 , x2 x0 i,

(24’)
(25’)

p × (p → p) → p

(20’)

Comparison to the examples covered by the heuristic of (Balat
et al. 2004) In addition to Example 2 that was borrowed from
(Balat et al. 2004), other examples that can be covered from
that paper are examples 4.2.1– 4.2.4 and Example 4.3.1. In these
examples, not only are the input and the output of their TDPE
represented uniquely, but also, in the cases when there are two
distinct output normal forms according to Balat et al., our normalizer
unifies the two normal forms into one, shown below:

of ENF types
(p × q → p) × (p × q → q)
(p × (p → r) × (q → r) → r)×
(q × (p → r) × (q → r) → r)
(r × p × (q → s) × (p → s) → s)×
(r × q × (q → s) × (p → s) → s)

(21’)

x0
hι1 x0 , ι2 x0 i

(22’)

hι01 hx0 , x1 i, ι02 ι01 hx0 , x1 i, ι02 ι02 ι1 hx0 , x1 i, ι02 ι02 ι2 hx0 , x1 ii
(4.2.3)

(23’)

(p × (q → s) × (q → r) × (p → s) × (p → r) → s)×
(q × (q → s) × (q → r) × (p → s) × (p → r) → s) (24’)

hι01 hx1 , x0 i, ι02 ι02 ι1 hx1 , x0 i, ι02 ι01 hx1 , x0 i, ι02 ι02 ι2 hx1 , x0 ii
(4.2.4)

(p × (q → s) × (q → r) × (p → s) × (p → r) → r)×
(q × (q → s) × (q → r) × (p → s) × (p → r) → r), (25’)

hι02 ι02 ι1 x1 , ι02 ι01 x1 i.

Finally, as we shall see in the following two examples, our conversion to compact form does not guarantee a canonical representation for terms that are equal with respect to the strong forms of
βη-equality used to duplicate subterms (Example 5) or change the
order of case analysis of subterms (Example 6). Although such term
transformations might not be desirable in the setting of real programming languages, for they change the order of evaluation, in a
pure effect-free setting like a proof assistant, such transformation
would be handy to have.
Example 5. The following βη-equal terms,
0

0

0

0

λxyzu.δ(uz, w.δ(uz, w .xw , w .yw ), w.yw),

(4.3.1)

Canonical representations could be obtained in these examples,
because it was possible to represent the input and output terms in
the fragment of the compact calculus which does not include δ’s
(although it still involves sum types).
On the other hand, there are also the examples where the input
and output are not unified by our procedure.2 Examples 4.3.2
and 4.3.3 are not handled because we do not permute the order of
case analyses (as shown by our Example 6); Example 6.2.4.2 is not
handled because we do not analyze if a subterm has been used twice
in a term or not (as shown also by our Example 5); examples 4.3.4
and 4.4 are not even executable in our implementation, because we
do not have a special treatment of the atomic empty type.
Of course, there is nothing stopping us from applying the
program transformations that would allow to handle this kind of

and reverse-normalizing these compact terms produces always the
right-hand side of the corresponding equation involving lambda
terms.

λxyzu.δ(uz, w.xw, w.yw)

(4.2.1)
(4.2.2)

2 We

shall not reproduce the compact representation for these examples in
this paper, but they are available for inspection in the Coq formalization
accompanying it.

(26)
(27)

9

2016/7/1

cases—or nothing stopping Balat et al. from first applying our typedirected normalization procedure before performing their heuristic
to unify the different normal outputs that they sometimes get. The
point is that these two methodologies are orthogonal and they would
ideally be used in combination inside a real-world application; for
more comments about the two approaches, see Section 5.
4.1

(∀ {w’’}, le w’ w’’ → f w’’ x → X w’’ x0) → X w’ x0.
Next, the necessary forcing fixpoints are defined: bforces, cforces,
and dforces, which are used to construct the type of the continuation monad corresponding to Base, CNF, and DNF, respectively;
sforces is used for constructing the type of the continuation monad
corresponding to non-normalized types.

A converter for the compact term representation

In the remaining part of this section, we explain the high-level structure of our prototype normalizer of lambda terms into compact terms
and vice versa. The full Coq implementation of the normalizer, together with the examples considered above, is given as a companion
to this paper. This is only one possible implementation, using continuations, but all the previous material of this paper was written as
generically as possible, so that it is useful if other implementation
techniques are attempted in the future, such as rewriting based on
evaluation contexts (i.e. the first-order reification of continuations),
or abstract machines.
In a nutshell, our implementation is a type-directed partial
evaluator, written in continuation-passing style, with an intermediate
phase between the evaluation and reification phases, that allows to
map a ‘semantic’ representation of a term from a type to its ENF
type, and vice versa. Such partial evaluators can be implemented
very elegantly, and with getting certain correctness properties for
free, using the GADTs from Ocaml’s type system, as shown by
the recent work of Danvy, Keller, and Puech (Danvy et al. 2015).
Nevertheless, we had chosen to carry out our implementation in Coq,
because that allowed us to perform a careful interactive analysis of
the necessary normal forms—hence the compact calculus introduced
in the first part of this section.
Usual type-directed partial evaluation (TDPE), aka normalizationby-evaluation (NBE), proceeds in tho phases. First an evaluator is
defined which takes the input term and obtains its semantic representation, and then a reifier is used to map the semantic representation
into an output syntactic term. Our TDPE uses an intermediate phase
between the two phases, a phase where type isomorphisms are
applied to the semantic domain so that the narrowing down of a
class of equal terms, described in Section 2, is performed on the
semantic annotation of a term.
The semantics that we use is defined by a continuation monad
over a forcing structure, together with forcing fixpoints that map
the type of the input term into a type of the ambient type theory.
The forcing structure is an abstract signature (Coq module type),
requiring a set K of possible worlds, a preorder relation on worlds,
le, an interpretation of atomic types, pforces, and X, the return type
of the continuation monad.

Fixpoint bforces (w:K)(b:Base) {struct b} : Set :=
match b with
| prp p ⇒ pforces w p
| bd d ⇒ dforces w d
end
with cforces (w:K)(c:CNF) {struct c} : Set :=
match c with
| top ⇒ unit
| con c1 b c2 ⇒
(∀ w’, le w w’ → Cont cforces w’ c1 → Cont bforces w’ b)
× (Cont cforces w c2)
end
with dforces (w:K)(d:DNF) {struct d} : Set :=
match d with
| two c1 c2 ⇒ (Cont cforces w c1) + (Cont cforces w c2)
| dis c1 d2 ⇒ (Cont cforces w c1) + (Cont dforces w d2)
end.
Fixpoint eforces (w:K)(e:ENF) {struct e} : Set :=
match e with
| cnf c ⇒ cforces w c
| dnf d ⇒ dforces w d
end.
Fixpoint sforces (w:K)(F:Formula) {struct F} : Set :=
match F with
| prop p ⇒ pforces w p
| disj F G ⇒ (Cont sforces w F) + (Cont sforces w G)
| conj F G ⇒ (Cont sforces w F) × (Cont sforces w G)
| impl F G ⇒ ∀ w’,
le w w’ → (Cont sforces w’ F) → (Cont sforces w’ G)
end.
Given these definitions, we can write an evaluator for compact
terms, actually two simultaneously defined evaluators evalc and
evalb, proceeding by induction on the input term.
Theorem evalc {c} : (HSc c → ∀ {w}, Cont cforces w c)
with evalb {b c0} : (HSb c0 b → ∀ {w},
Cont cforces w c0 → Cont bforces w b).

Module Type ForcingStructure.
Parameter K : Set.
Parameter le : K → K → Set.
Parameter pforces : K → Proposition → Set.
Parameter Answer : Set.
Parameter X : K → Answer → Set.
End ForcingStructure.

An evaluator for usual lambda terms can also be defined, by
induction on the input term. A helper function lforces analogous to
the list map function for sforces is necessary.

The continuation monad is polymorphic and instantiable by
a forcing fixpoint f and a world w. It ensures that the preorder
relation is respected; intuitively, this has to do with preserving the
monotonicity of context free variables: we cannot ‘forget’ a free
variable i.e. contexts cannot decrease.

Fixpoint
lforces (w:K)(Gamma:list Formula) {struct Gamma} :
Set :=
match Gamma with
| nil ⇒ unit
| cons A Gamma0 ⇒
Cont sforces w A × lforces w Gamma0
end.

Definition Cont {class:Set}(f :K→class→Set)(w:K)(x:class)
:= ∀ (x0:Answer), ∀ {w’}, le w w’ →

10

2016/7/1

Inductive le : CNF → CNF → Set :=
| le refl : ∀ {w}, le w w
| le cons : ∀ {w1 w2 c b},
le w1 w2 → le w1 (con c b w2).

Theorem eval {A Gamma} : ND Gamma A → ∀ {w},
lforces w Gamma → Cont sforces w A.
The novelty of our implementation (besides isolating the compact term calculus itself), in comparison to previous type-directed
partial evaluators for the lambda calculus with sums, consists in
showing that one can go back and forth between the semantic annotation at a type F and the semantic annotation of the normal form
enf (F ). The proof of this statement needs a number of auxiliary
lemmas that we do not mention in the paper. We actually prove two
statements simultaneously, f2f and f2f’, declared as follows.

Definition le := le .
Definition le refl : ∀ {w}, le w w.
Definition pforces := fun w p ⇒ HSb w (prp p).
Definition Answer := Base.
Definition X := fun w b ⇒ HSb w b.
End structureHS.

Theorem f2f :
(∀ F, ∀ w, Cont sforces w F → Cont eforces w (enf F))
with f2f’ :
(∀ F, ∀ w, Cont eforces w (enf F) → Cont sforces w F).

Using the instantiated forcing structures, we can provide reification functions for terms of the lambda calculus,
Theorem sreify : (∀ F w, Cont sforces w F → ND w F)
with sreflect : (∀ F w, ND w F → Cont sforces w F).

As one can see from their type signatures, f2f and f2f’ provide a link
between the semantics of the standard lambda calculus for sums
(ND) and the semantics of our compact calculus(HSc/HSb).
We move forward to describing the reification phase. In this
phase, two instantiations of a forcing structure are needed. Unlike
the evaluators, which can work over an abstract forcing structure,
the reifiers need concrete instantiations built from the syntax of the
term calculus in order to produce syntactic normal forms.
The first instantiation is a forcing structure for the standard
lambda calculus with sums. The set of worlds is the set of contexts
(lists of types), the preorder on worlds is defined as the prefix relation
on contexts, the forcing of an atomic type p is the set of terms of type
p in the context w, and the answer type of the continuation monad
is the set of terms of type F in the context w. One could be more
precise, and instantiate the answer type by the set of normal/neutral
terms, like it has been done in most other implementations of TDPE,
and in our own prior works, but for the sake of simplicity, we do not
make that distinction in this paper.

and for our compact terms:
Theorem creify :
(∀ c w, Cont cforces w c → HSc (explogn c (cnf w)))
with creflect : (∀ c w, Cont cforces (ntimes c w) c)
with dreify : (∀ d w, Cont dforces w d → HSb w (bd d))
with dreflect : (∀ d c1 c2 c3,
HSc (explogn c1 (cnf (ntimes c3 (con c1 (bd d) c2)))) →
Cont dforces (ntimes c3 (con c1 (bd d) c2)) d).
The reifier for atomic types, preify, is not listed above, because it is
simply the ‘run’ operation on the continuation monad. As usually in
TDPE, every reification function required its own simultaneously
defined reflection function.
Finally, one can combine the reifiers, the evaluators, and the functions f2f and f2f’, in order to obtain both a normalizing converter of
lambda terms into compact terms (called nbe in the Coq implementation), and a converter of compact terms into lambda terms (called
ebn in the Coq implementation). One can, if one desires, also define
only a partial evaluator of lambda terms and only a partial evaluator
of compact terms.

Module structureND <: ForcingStructure.
Definition K := list Formula.
Inductive le : list Formula → list Formula → Set :=
| le refl : ∀ {w}, le w w
| le cons : ∀ {w1 w2 F},
le w1 w2 → le w1 (cons F w2).

5.

Definition le := le .

Conclusion

Summary of our results We have brought into relation two distinct fundamental problems of the lambda calculi underlying modern
functional programming languages, one concerning identity of types,
and the other concerning identity of terms, and we have shown how
improved understanding of the first problem can lead to improved
understanding of the second problem.
We started by presenting a normal form of types, the explog normal form, that is a systematic ordering of the high-school
identities allowing for a type to be mapped to normal form. This
can be used as a simple heuristic for deciding type isomorphism, a
first such result for the type language {→, +, ×}. We beleive that
the link established to analysis and abstract algebra (the exp-log
decomposition produces a pair of homomorphisms between the
additive and the multiplicative group in an exponential field) may
also be beneficial to programming languages theory in the future.
The typing restrictions imposed to lambda terms in exp-log
normal form allowed us to decompose the standard axioms for =βη
into a proper and simpler subset of themselves, =eβη . As far as we
are aware, this simpler axiomatization has not been isolated before.

Definition le refl : ∀ {w}, le w w.
Definition pforces := fun w p ⇒ ND w (prop p).
Definition Answer := Formula.
Definition X := fun w F ⇒ ND w F.
End structureND.
The second instantiation is a forcing structure for our calculus
of compact terms. The set of worlds is the same as the set of CNFs,
because our context are simply CNFs, the preorder is the prefix
relation on CNFs, the forcing of atomic types are terms of atomic
types, and the answer type of the continuation monad is the set of
terms at base type.
Module structureHS <: ForcingStructure.
Definition K := CNF.

11

2016/7/1

Even more pleasingly, the new axiomatization disentangles the old
one, in the sense that left-hand sides and right-hand sides of the
equality axioms can no longer overlap.
Finally, we ended by giving a compact calculus of terms that
can be used as a more canonical alternative to the lambda calculus
when modeling the core of functional programming languages: the
new syntax does not allow for the η-axioms of Figure 2 even to
e
be stated, with the exception of η+
that is still present, albeit with
a restricted type. As our method exploits type information, it is
orthogonal to the existing approaches that rely on term analysis
(discussed below), and hence could be used in addition to them; we
hope that it may one day help with addressing the part of η-equality
that is still beyond decision procedures. We also implemented and
described a prototype converter from/to standard lambda terms.
In the future, we would like to derive declarative rules to describe
more explicitly the extent of the fragment of =βη decided by our
heuristic, although implicitly that fragment is determined by the
reduction to ENF congruence classes explained in Section 3. It
should be noted that in this respect our heuristic is no less explicitly
described, than the only other published one (Balat et al. 2004)
(reviewed below).

ample 6. For determining if something is a normal form, in addition
to the standard separation of neutral vs normal terms, one uses three
additional criteria: (A) δ-expressions that appear under a lambda
abstraction must only case-analyze terms involving the abstracted
variable; (B) no two terms which are equal modulo ≈ can be case analyzed twice; in particular, no term can be case analyzed twice; (C)
no case analysis can have the two branches which are equal modulo
≈. To enforce condition A, particular powerful control operators,
set/cupto, are needed in the implementation, requiring a patch of the
ocaml toplevel. Using our compact terms instead of lambda terms
should help get rid of condition A (hence set/cupto), since as we
showed keeping a constructor for λ’s in the representation of normal
forms is not necessary. On the other hand, we could profit from implementing checks such as B and C in our implementation; however,
our goal was to see how far we can get in a purely type-directed way
without doing any program analysis.
A final small remark about this line of works: in (Balat 2009),
Balat used the word “canonical” to name his normal forms, but this
does not preserve the usual meaning of that word, as showed in the
previous article (Balat et al. 2004).
Lindley (Lindley 2007) presents another proof of decidability
of βη-equality for the lambda calculus with sums, based on an
original decomposition of the η+ -axiom into four axioms involving
evaluation contexts (the proof of this decomposition, Proposition 1,
is unfortunately only sketched); the proof of decidability uses
rewriting modulo the congruence relation ≈ of Balat et al.
Scherer (Scherer 2015) reinterprets Lindley’s rewriting approach
to decidability in the setting of the structural proof theory of maximal
multi-focusing, where he brings it in relation to the technique of
preemptive rewriting (Chaudhuri et al. 2008). Scherer seems to
derive canonicity of his normal forms for natural deduction from
Lindley’s results, although the later does not seem to show canonical
forms are a result of his rewriting decidability result.
The idea to apply type isomorphism in order to capture equality
of terms has been used before (Ahmad et al. 2010), but only implicitly. Namely, in the focusing approach to sequent calculi (Liang
and Miller 2007), one gets a more canonical representation of
terms (proofs) by grouping all so called asynchronous proof rules
into blocks called asynchronous phases. However, while all asynchronous proof rules are special kinds of type isomorphisms, not all
possible type isomorphisms are accounted for by the asynchronous
blocks: sequent calculi apply asynchronous proof rules superficially,
by looking at the top-most connectives, but normalizing sequents
(formulas) to their exp-log normal form applies proof rules deeply inside the proof tree. Our approach can thus also been seen as moving
focusing proof systems into the direction of so called deep inference
systems.

Related work Dougherty and Subrahmanyam (Dougherty and Subrahmanyam 1995) show that the equational theory of terms (morphisms) for almost bi-Cartesian closed categories is complete with
respect to the set theoretic semantics. This presents a generalization
of Friedman’s completeness theorem for simply typed lambda calculus without sums (Cartesian closed categories) (Friedman 1975).
Ghani (Ghani 1995) proves βη-equality of terms of the lambda
calculus with sum types to be decidable, first proceeding by rewriting and eta-expansion, and then checking equality up to commuting
conversions by interpreting terms as finite sets of quasi-normal
forms; no canonical normal forms are obtained.
When sums are absent, the existence of a confluent and strongly
normalizing rewrite system proves the existence of canonical normal
forms, and then decidability is a simple check of syntactic identity
of canonical forms. Nevertheless, even in the context when sums are
absent, one may be interested in getting term representations that
are canonical modulo type isomorphism, as in the recent works of
Dı́az-Caro, Dowek, and Martı́nez López (Dı́az-Caro and Dowek
2015; Dı́az-Caro and Martı́nez López 2016).
Altenkirch, Dybjer, Hofmann, and Scott (Altenkirch et al. 2001)
give another proof of decidability of βη-equality for the lambda
calculus with sums by carrying out a normalization-by-evaluation
argument in category theory. They provide a canonical interpretation
of the syntax in the category of sheaves for the Grothendieck
topology over the category of constrained environments, and they
claim that one can obtain an algorithm for a decision procedure by
virtue of the whole development being formalizable in extensional
Martin-Löf type theory.
In the absence of η+ (Dougherty 1993), or for the restriction of
η+ to N being a variable (Di Cosmo and Kesner 1993), a confluent
and strongly normalizing rewrite system exists, hence canonicity of
normal forms for such systems follows.
In (Balat et al. 2004), Balat, Di Cosmo, and Fiore, present a
notion of normal form which is a syntactic counterpart to the notion
of normal forms in sheaves of Altenkirch, Dybjer, Hofmann, and
Scott. However, the forms are not canonical, as there may be two
different syntactic normal forms corresponding to a single semantic
one. They also say they believe (without further analysis or proof)
that one can get canonical normal forms if one considers an ordering
of nested δ-expressions.
The normal forms of Balat et al. are sophisticated and determining if something is a normal form relies on comparing sub-terms up
to a congruence relation ≈ on terms; essentially, this congruence
allows to identify terms such as the ones of our Example 5 and Ex-

References
A. Ahmad, D. Licata, and R. Harper. Deciding coproduct equality with
focusing. Manuscript, 2010.
T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott. Normalization by
evaluation for typed lambda calculus with coproducts. In Logic in
Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on,
pages 303–310, 2001.
V. Balat. Keeping sums under control. In Workshop on Normalization by
Evaluation, pages 11–20, Los Angeles, United States, Aug. 2009.
V. Balat, R. Di Cosmo, and M. Fiore. Extensional normalisation and
type-directed partial evaluation for typed lambda calculus with sums.
In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’04, pages 64–76, New
York, NY, USA, 2004. ACM.
S. N. Burris and K. A. Yeats. The saga of the high school identities. Algebra
Universalis, 52:325–342, 2004.

12

2016/7/1

K. Chaudhuri, D. Miller, and A. Saurin. Canonical Sequent Proofs via
Multi-Focusing, pages 383–396. Springer US, Boston, MA, 2008. ISBN
978-0-387-09680-3.
O. Danvy, C. Keller, and M. Puech. Typeful Normalization by Evaluation.
In P. L. Hugo Herbelin and M. Sozeau, editors, 20th International
Conference on Types for Proofs and Programs (TYPES 2014), volume 39
of Leibniz International Proceedings in Informatics (LIPIcs), pages 72–
88, Dagstuhl, Germany, 2015. Schloss Dagstuhl–Leibniz-Zentrum fuer
Informatik. ISBN 978-3-939897-88-0.
R. Di Cosmo and D. Kesner. A confluent reduction for the extensional
typed λ-calculus with pairs, sums, recursion and terminal object. In
A. Lingas, R. Karlsson, and S. Carlsson, editors, Automata, Languages
and Programming, volume 700 of Lecture Notes in Computer Science,
pages 645–656. Springer Berlin Heidelberg, 1993.
A. Dı́az-Caro and G. Dowek. Simply typed lambda-calculus modulo type
isomorphisms. Draft at https://hal.inria.fr/hal-01109104, 2015.
A. Dı́az-Caro and P. E. Martı́nez López. Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an
implementation of λ+ . In IFL 2015: Symposium on the implementation
and application of functional programming languages. ACM, 2016. To
appear. Preprint at arXiv:1511.09324.
D. Dougherty. Some lambda calculi with categorical sums and products. In
Rewriting Techniques and Applications, pages 137–151. Springer, 1993.
D. J. Dougherty and R. Subrahmanyam. Equality between functionals
in the presence of coproducts. In Proceedings of the 10th Annual
IEEE Symposium on Logic in Computer Science, LICS ’95, pages 282–,
Washington, DC, USA, 1995. IEEE Computer Society.
M. Fiore, R. D. Cosmo, and V. Balat. Remarks on isomorphisms in typed
lambda calculi with empty and sum types. Annals of Pure and Applied
Logic, 141:35–50, 2006.
H. Friedman. Equality between functionals. In Logic Colloquium ’73,
volume 453 of Lecture Notes in Mathematics, pages 22–37. Springer,
1975.
N. Ghani. βη-equality for coproducts. In Typed Lambda Calculi and
Applications, pages 171–185. Springer, 1995.
G. H. Hardy. Orders of Infinity. The ‘Infinitärcalcül’ of Paul Du BoisReymond. Cambridge Tracts in Mathematic and Mathematical Physics.
Cambridge University Press, 1910.
D. Ilik. Axioms and decidability for type isomorphism in the presence of
sums. In Proceedings of the Joint Meeting of the Twenty-Third EACSL
Annual Conference on Computer Science Logic (CSL) and the TwentyNinth Annual ACM/IEEE Symposium on Logic in Computer Science
(LICS), CSL-LICS ’14, pages 53:1–53:7, New York, NY, USA, 2014.
ACM.
C. Liang and D. Miller. Focusing and polarization in intuitionistic logic. In
J. Duparc and T. A. Henzinger, editors, Computer Science Logic, volume
4646 of Lecture Notes in Computer Science, pages 451–465. Springer
Berlin Heidelberg, 2007. ISBN 978-3-540-74914-1.
S. Lindley. Extensional rewriting with sums. In S. R. Della Rocca, editor,
Typed Lambda Calculi and Applications, volume 4583 of Lecture Notes
in Computer Science, pages 255–271. Springer Berlin Heidelberg, 2007.
M. Rittri. Using types as search keys in function libraries. J. Funct. Program.,
1(1):71–89, 1991.
G. Scherer. Multi-Focusing on Extensional Rewriting with Sums. In T. Altenkirch, editor, 13th International Conference on Typed Lambda Calculi
and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 317–331, Dagstuhl, Germany,
2015. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. ISBN 978-3939897-87-3.

13

2016/7/1

