Computing in Cantor’s Paradise With λZFC
Neil Toronto and Jay McCarthy
neil.toronto@gmail.com and jay@cs.byu.edu
PLT @ Brigham Young University, Provo, Utah, USA

Abstract. Applied mathematicians increasingly use computers to answer mathematical questions. We want to provide them domain-specificlanguages. The languages should have exact meanings and computational
meanings. Some proof assistants can encode exact mathematics and extract programs, but formalizing the required theorems can take years.
As an alternative, we develop λZFC , a lambda calculus that contains
infinite sets as values, in which to express exact mathematics and gradually change infinite calculations to computable ones. We define it as aconservative extension of set theory, and prove that most contemporary
theorems apply directly to λZFC terms.
We demonstrate λZFC ’s expressiveness by coding up the real numbers,arithmetic and limits. We demonstrate that it makes deriving computational meaning easier by defining a monad in it for expressing limits, andusing standard topological theorems to derive a computable replacement.

Keywords: Lambda Calculus, Set Theory, Semantics
No one shall expel us from the Paradise that Cantor has created.
David Hilbert

1

Introduction

Georg Cantor first proved some of the surprising consequences of assuming infinite sets exist. David Hilbert passionately defended Cantor’s set theory as amathematical foundation, coining the term “Cantor’s Paradise” to describe theuniverse of transfinite sets in which most mathematics now takes place.
The calculations done in Cantor’s Paradise range from computable to unimaginably uncomputable. Still, its inhabitants increasingly use computers to answer
questions. We want to make domain-specific languages (DSLs) for writing thesequestions, with implementations that compute exact and approximate answers.
Such a DSL should have two meanings: an exact mathematical semantics,
and an approximate computational one. A traditional, denotational approach is
to give the exact as a transformation to first-order set theory, and because set
theory is unlike any intended implementation language, the approximate as atransformation to a lambda calculus. However, deriving approximations whileswitching target languages is rife with opportunities to commit errors.
A more certain way is to define the exact semantics in a proof assistant likeHOL [11] or Coq [5], prove theorems, and extract programs. The type systems
confer an advantage: if the right theorems are proved, the programs are correct.

Unfortunately, reformulating and re-proving theorems in such an exacting
way causes significant delays. For example, half of Joe Hurd’s 2002 dissertation
on probabilistic algorithms [9] is devoted to formalizing early-1900s measure
theory in HOL. Our work in Bayesian inference would require at least threetimes as much formalization, even given the work we could build on.
Some middle ground is clearly needed: something between the traditional,
error-prone way and the slow, absolutely certain way.
Instead of using a typed, higher-order logic, suppose we defined, in firstorder set theory, an untyped lambda calculus that contained infinite sets andoperations on them. We could interpret DSL terms exactly as uncomputable
programs in this lambda calculus. But instead of redoing a century of work to
extract programs that compute approximations, we could directly reuse firstorder theorems to derive them from the uncomputable programs.
Conversely, set theory, which lacks lambdas and general recursion, is an awkward target language for a semantics that is intended to be implemented. Suppose we extended set theory with untyped lambdas (as objects, not quantifiers).
We could still interpret DSL terms as operations on infinite objects. But insteadof leaping from infinite sets and operations on them to implementations, we
could replace those operations with computable approximations piece at a time.
If we had a lambda calculus with infinite sets as values, we could approachcomputability from above in a principled way, gradually changing programs for
Cantor’s Paradise until they can be implemented in Church’s Purgatory.
We define that lambda calculus, λZFC , and a call-by-value, big-step reduction
semantics. To show that it is expressive enough, we code up the real numbers,arithmetic and limits, following standard analysis. To show that it simplifies
language design, we define the uncomputable limit monad in λZFC , and derivea computable, directly implementable replacement monad by applying standard
topological theorems. When certain proof obligations are met, the output of programs that use the computable monad converge to the same values as the output
of programs that use the uncomputable monad but are otherwise identical.
1.1

Language Tower and Terminology

λZFC ’s metalanguage is first-order set theory: first-order logic with equality
extended with ZFC, or the Zermelo Fraenkel axioms and Choice (equivalently
well-ordering). We also assume the existence of an inaccessible cardinal. Section 2
reviews the axioms, which λZFC ’s primitives are derived from.
To help ensure λZFC ’s definition conservatively extends set theory, we encode
its terms as sets. For example, htP , Ri is the encoding of “the powerset of thereals” as a pair, where hx, yi = {{x}, {x, y}} for any sets x and y.
λZFC ’s semantics reduces terms to terms; e.g. htP , Ri reduces to the actual
powerset of R. Thus, λZFC contains infinite terms. Infinitary languages are usefuland definable: the infinitary lambda calculus [10] is an example, and Aczel’s
broadly used work [2] on inductive sets treats infinite inference rules explicitly.
For convenience, we define a language λ−ZFC of finite terms and a function
FJ·K from λ−
to
λ
.
We
can
then
write
P R, meaning FJP RK = htP , Ri.
ZFC
ZFC

Semantic functions like FJ·K and the interpretation of BNF grammars aredefined in set theory’s metalanguage, or the meta-metalanguage. Distinguishingmetalanguages helps avoid paradoxes of definition such as Berry’s paradox, which
are particularly easy to stumble onto when dealing with infinities.
We write λ−ZFC terms in sans serif font, and the metalanguage and metametalanguage in math font. We write common keywords in bold and invented
keywords in bold italics. We abbreviate proofs for space.

2

Metalanguage: First-Order Set Theory

We assume readers are familiar with classical first-order logic with equality andits inference rules, but not set theory. Hrbacek and Jech [8] is a fine introduction.
Set theory extends classical first-order logic with equality, which distinguishes
between truth-valued formulas φ and object-valued terms x. Set theory allows
only sets as objects, and quantifiers like ‘∀’ may range only over sets.
We define predicates and functions using ‘:=’; for example, nand(φ1 , φ2 ) :=¬(φ1 ∧φ2 ). They must be nonrecursive so they can be exhaustively applied. They
are therefore conservative extensions: they do not prove more theorems.
To develop set theory, we make proper extensions, which prove more theorems, by adding symbols and axioms to first-order logic. For example, we firstadd ‘∅’ and ‘∈’, and the empty set axiom ∀ x. x 6∈ ∅.
We use ‘:≡’ to define syntax; e.g. ∀ x ∈ A. P (x) :≡ ∀ x. (x ∈ A ⇒ P (x)),
where predicate application P (x) represents a formula that may depend on x.
We allow recursion in meta-metalanguage definitions if substitution terminates,so ∀ x1 x2 ... xn . φ :≡ ∀ x1 . ∀ x2 ... xn . φ can bind any number of names.
We already have Axiom 0 (empty set). Now for the rest.
Axiom 1 (extensionality). Define A ⊆ B := ∀ x ∈ A. x ∈ B and assume∀ A B. (A ⊆ B ∧ B ⊆ A ⇒ A = B); i.e. A = B if they mutually are subsets. tu
The converse follows from substituting A for B or B for A.
Axiom 2 (foundation). Define A 6∩ B := ∀ x. (x ∈ A ⇒ x 6∈ B) (“A and B are
disjoint”) and assume ∀ A. (A = ∅) ∨ ∃ x ∈ A. x 6∩ A.
tuFoundation implies that the following nondeterministic procedure always terminates: If input A = ∅, return A; otherwise restart with any A0 ∈ A.
Thus, sets are roots of trees in which every upward path is unbounded but
finite. Foundation is analogous to “all data constructors are strict.”
Axiom 3 (powerset). Add ‘P’ and assume ∀ A x. (x ∈ P(A) ⇐⇒ x ⊆ A). tu
A hereditarily finite set is finite and has only hereditarily finite members.
Each such set first appears in some P(P(...P(∅)...)). For example, after {x, ...}
(literal set syntax) is defined, {∅} ∈ P(P(∅)). {R} is not hereditarily finite.
S
S
Axiom 4 (union). Add ‘ ’ (“big” union) and assume ∀ A x. (x ∈ A ⇐⇒∃ y. x ∈ y ∧ y ∈ A).
t
u

S
S
After {x, ...} is defined, {{x, y}, {y, z}} = {x,Sy, z}. Also, ‘ ’ can extract theobject in a singleton set: if A = {x}, then x = A.
Axiom 5 (replacement schema). A binary predicate R can act as a function
if ∀ x ∈ A. ∃! y. R(x, y), where ‘∃!’ means unique existence. We cannot quantify
over predicates in first-order logic, but we can assume, for each such definable R,
that ∀ y. (y ∈ {y 0 | x ∈ A ∧ R(x, y 0 )} ⇐⇒ ∃ x ∈ A. R(x, y)). Roughly, treating
R as a function, if R’s domain is a set, its image (range) is also a set.
tu
A schema represents countably many axioms. If R(n, m) ⇐⇒ m = n + 1, forexample, then {m | n ∈ N ∧ R(n, m)} increments the natural numbers.
Define {F (x) | x ∈ A} :≡ {y | x ∈ A ∧ y = F (x)}, analogous to map F A, forfunctional replacement. Now {n + 1 | n ∈ N} increments the naturals.
It seems replacement should be defined functionally, but predicates allow
powerful nonconstructivism.
Suppose Q(y) for exactly one y. The description
S
operator ι y. Q(y) :≡ {y | x ∈ P(∅) ∧ Q(y)} finds “the y such that Q(y).”From the six axioms so far, we can define A ∪ B (binary union), {x, ...} (literal finite sets), hx, y, z, ...i (ordered pairs(bounded
T and lists), {x ∈ A | Q(x)}Sselection), A\B (relative complement), A (“big” intersection), x∈A F (x) (indexed union), A×B (cartesian product), and A → B (total function spaces). For
details, we recommend Paulson’s remarkably lucid development in HOL [16].
2.1

The Gateway to Cantor’s Paradise: Infinity

From the six axioms so far, we cannot construct a set that is closed underunboundedly many operations, such as the language of a recursive grammar.
Example 1 (interpreting a grammar). We want to interpret z ::= ∅ | h∅, zi. It
should mean the least fixpoint of a function Fz , which, given a subset of z’s
language, returns a larger subset. To define Fz , replace ‘|’ with ‘∪’, the terminal∅ with {∅}, and the rule h∅, zi with functional replacement:
Fz (Z) := {∅} ∪ {h∅, zi | z ∈ Z}

(1)

We could define Z(0) := ∅, then Z(1) := Fz (Z(0)) = {∅, h∅, ∅i}, then Z(2) =Fz (Z(1)) = {∅, h∅, ∅i , h∅, ∅, ∅i}, and so on. The language should be the unionof all the Z(n), but we cannot construct it without a set of all n.
♦
We follow Von Neumann, defining 0 := ∅ as the first ordinal number
and s(n) := n ∪ {n} to generate successor ordinals. Then 1 := s(0) = {0},2 := s(1) = {0, 1}, and 3 := s(2) = {0, 1, 2}, and so on. The set of such numbers
is the language of n ::= 0 | s(n), which should be the least fixpoint of Fn (N ) :={0} ∪ {s(n) | n ∈ N }, similar to (1). We must assume some fixpoint exists.
Axiom 6 (infinity). ∃ I. I = Fn (I).

tu

I is a bounding set, so it may contain more than just finite ordinals. But Fn ismonotone in I, so by the Knaster-Tarksi theorem (suitably restricted [15]),\ω :={N ⊆ I | N = Fn (N )}(2)is the least fixpoint of Fn : the finite ordinals, a model of the natural numbers.

Example 2 (interpreting a grammar). We build the language of z recursively:
Z(0) = ∅Z(ω) =

[

Z(n)

n∈ω

Z(s(n)) = Fz (Z(n)), n ∈ ω(3)

By induction, Z(n) exists for every n ∈ ω; therefore Z(ω) exists, so (3) is aconservative extension of set theory. It is not hard to prove (by induction) that
Z(ω) is the set of all finite lists of ∅, and that it is the least fixpoint of Fz . ♦Similarly to building the language Z(ω) of z in (3), we can build the set V(ω)
of all hereditarily finite sets (see Axiom 3) by iterating P instead of Fz :V(0) = ∅V(ω) =

[

V(n)

n∈ω

V(s(n)) = P(V(n)), n ∈ ω(4)The set ω is not just a model of the natural numbers. It is also a number
itself: the first countable ordinal. Indeed, ω is strikingly similar to every finite
ordinal in two ways. First, it is defined as the set of its predecessors. Second,
it has a successor s(ω) = ω ∪ {ω}. (Imagine it as {0, 1, 2, ..., ω}.) Unlike finite,
nonzero ordinals, ω has no immediate predecessor—it is a limit ordinal.
More limit ordinals allow iterating P further. It is not hard to build ω + ω,
ω 2 and ω ω as least fixpoints. The Von Neumann hierarchy generalizes (4):V(0) = ∅V(s(α)) = P(V (α)), ordinal αV(β) =[

V(α), limit ordinal β

α∈β

(5)

It is a theorem of ZFC that every set first appears in V(α) for some ordinal α.
Equations (3,4,5) demonstrate transfinite recursion, set theory’s unfold:defining a function V on ordinals, with V (β) in terms of V (α) for every α ∈ β.
2.2

Every Set Can Be Sequenced: Well-Ordering

A sequence is a total function from an ordinal to a codomain; e.g. f ∈ 3 → A isa length-3 sequence of A’s elements. (An ordinal is comprised of its predecessors,
so 3 = {0, 1, 2}.) A well-order of A is a bijective sequence of A’s elements.
Axiom 7 (well-ordering). Suppose Ord identifies ordinals and B ↔ A is thebijective mappings from B to A. Assume ∀ A. ∃ α f . Ord(α) ∧ f ∈ α ↔ A; i.e.
every set can be well-ordered.
tuBecause f is not unique, a well-ordering primitive could make λZFC ’s semantics
nondeterministic. Fortunately, the existence of a cardinality operator is equivalent to well-ordering [19], so we will give λZFC a cardinality primitive.
The cardinality of a set A is the smallest ordinal thatTcan be put in bijection
with A. Formally, if F contains A’s well-orderings, |A| = {domain(f ) | f ∈ F }.

e ::= n | v | e e | if e e e | e ∈ e |S

v ::= false | true | λ. e | ∅ | ωn ::= 0 | 1 | 2 | · · ·e | take e | P e | image e e | card e

Fig. 1: The definition of λ−ZFC , which represents countably many λZFC terms.

2.3

Infinity’s Infinity: An Inaccessible Cardinal

The set V(ω) of hereditarily finite sets is closed under powerset, union, replacement (with predicates restricted to V(ω)), and cardinality. It is also transitive:
if A ∈ V(ω), then x ∈ V(ω) for all x ∈ A. These closure properties make it aGrothendieck universe: a set that acts like a set of all sets.
λZFC ’s values should contain ω and be closed under its primitives. But a
Grothendieck universe containing ω cannot be proved from the typical axioms.
If it exists, it must be equal to V(κ) for some inaccessible cardinal κ.
Axiom 8 (inaccessible cardinal). Suppose GU (V ) if and only if V is a
Grothendieck universe. Add ‘κ’ and assume Ord(κ) ∧ (κ > ω) ∧ GU (V(κ)). tu
We call the sets in V(κ) hereditarily accessible.
Inaccessible cardinals are not usually assumed but are widely believed consistent. Set theorists regard them as no more dangerous than ω. Interpreting
category theory with small and large categories, second-order set theory, or CIC
in first-order set theory requires at least one inaccessible cardinal [20, 3, 21].
Constructing a set A 6∈ V(κ) requires assuming κ or an equivalent, so V(κ)
easily contains most mathematics. In fact, most can be modeled well within
V(2ω ); e.g. the model of R we define in Sect. 6 is in V(ω + 11). Besides, if λZFC
needed to contain large cardinals, we could always assume even larger ones.

3

λZFC ’s Grammar

We define λZFC ’s terms in three steps. First, we define λ−ZFC , a language of finite
terms with primitives that correspond with the ZFC axioms. Second, we encode
these terms as sets. Third, guided by the first two steps, we define λZFC bydefining its terms, most of which are infinite, as sets in V(κ).
Figure 1 shows λ−
ZFC ’s grammar. Expressions e are typical: variables, values,
application, if, and domain-specific primitives for membership, union, extraction(take), powerset, functional replacement (image), and cardinality. Values v arealso typical: booleansconstants ∅ and ω.
S and lambdas, and the domain-specificS
In set theory, {A} = A holds for
all
A,
so
can
extractthe element fromS
a singleton. In λZFC , the encoding of {A} reduces to A only if A is an encoded
set. Therefore, the primitives must include take, which extracts A from {A}. In
particular, extracting a lambda from an ordered pair requires take.
We use De Bruijn indexes with 0 referring to the innermost binding. Because
we will define λZFC terms as well-founded sets, by Axiom 2, countably manyindexes is sufficient for λZFC as well as λ−ZFC .

Distinct tvar , tapp , tif , t∈ , t∪ , ttake , tP , timage , tcard , tset , tatom , tλ , tfalse , ttrue
FJnK := htvar , ni
FJef ex K := htapp , FJef K , FJex Ki

FJex ∈ eA K := ht∈ , FJex K , FJeA Ki···

FJ∅K := set(∅)

FJωK := set(ω)

FJfalseK := afalse

afalse := htatom , tfalse i

FJtrueK := atrue

atrue := htatom , ttrue iset(A) = htset , {set(x) | x ∈ A}i

Fig. 2: The semantic function FJ·K from λ−ZFC terms to λZFC terms.

Figure 2 shows part of the meta-metalanguage function FJ·K that encodesλ−
ZFC terms as λZFC terms. It distinguishes sorts of terms in the standard way,by pairing them with tags; e.g. if tset is the “set” tag, then htset , ∅i encodes ∅.
To recursively tag sets, we add the axiom set(A) = htset , {set(x) | x ∈ A}i.
The well-founded recursion theorem proves that for all A, set(A) exists, so
this axiom is a conservative extension. The actual proof is tedious, but in short,
set is structurally recursive. Now set(∅) = htset , ∅i and set(ω) encodes ω.
3.1

An Infinite Set Rule For Finite BNF Grammars

There is no sensible reduction relation for λ−
ZFC . (For example, P ∅ cannot correctly reduce to a value because no value in λ−ZFC corresponds to {∅}.) The
easiest way to ensure a reduction relation exists for λZFC is to include encodingsof all the sets in V(κ) as values.
To define λZFC ’s terms, we first extend BNF with a set rule: {y ∗α }, where α
is a cardinal. Roughly, it means sets comprised of no more than α terms fromthe language of y. Formally, it means P< (Y , α) := {x ∈ P(Y ) | |x| < α}, where
Y is a subset of y’s language generated while building a least fixpoint.
Example 3 (finite sets). The grammar h ::= {h∗ω } should represent all hereditarily finite sets, or V(ω). Intuitively, the single rule for h should be equivalent
to countably many rules h ::= {} | {h} | {h, h} | {h, h, h} | · · · .
Its language is the least fixpoint of Fh (H) := P< (H, ω). Further on, we will
prove that Fh ’s least fixpoint is V(ω) using a general theorem.
♦
Example 4 (accessible sets). The language of a ::= {a∗κ } is the least fixpoint of
Fa (A) := P< (A, κ), which should be V(κ).
♦
The following theorem schemas will make it easy to find least fixpoints.
Theorem 1. Let F be a unary function. Define V by transfinite recursion:[
V (0) = ∅V (β) =
V (α), limit ordinal β
V (s(α)) = F (V (α))

α∈β

(6)

Let γ be an ordinal. If F is monotone on V (γ), V is monotone on γ, and V (γ)
is a fixpoint of F , then V (γ) is also the least fixpoint of F .

e ::= n | v | htapp , e, ei | htif , e, e, ei | ht∈ , e, ei | ht∪ , ei | httake , ei | htP , ei |htimage , e, ei | htcard , ei | htset , {e∗κ }iv ::= afalse | atrue | htλ , ei | htset , {v ∗κ }in ::= htvar , 0i | htvar , 1i | · · ·Fig. 3: λZFC ’s grammar. Here, {e∗κ } means sets comprised of no more than κ
terms from the language of e.

Proof. By induction: successor case by monotonicity; limit by property of

S

. t
u

All the F s we define are monotone. In particular, the interpretations of {y ∗α }rules are monotone because P is monotone. Further, all the F s we define giverise to a monotone V . Grammar terminals “seed” every iteration with singletonsets, and {y ∗α } rules seed every iteration with ∅.
From here on, we write F α instead of V (α) to mean α iterations of F .
Theorem 2. Suppose a grammar with {y ∗α } rules and iterating function F .
Then F ’s least fixpoint is F γ , where γ is a regular cardinal not less than any α.
Proof. Fixpoint by Aczel [2, Theorem 1.3.4]; least fixpoint by Theorem 1.

tu

Example 5 (finite sets). Because ω is regular, by Theorem 2, Fh ’s least fixpoint
is Fhω . Further, Fh (H) = P(H) for all hereditarily finite H, and V(ω) is closed
under P, so Fhω = V(ω), the set of all hereditarily finite sets.
♦
Example 6 (accessible sets). By a similar argument, Fa ’s least fixpoint is Faκ =V(κ), the set of all hereditarily accessible sets.
♦
Example 7 (encoded accessible sets). The language of v ::= htset , {v ∗κ }i is comprised of the encodings of all the hereditarily accessible sets.
♦
3.2

The Grammar of Infinite, Encoded Terms

There are three main differences between λZFC ’s grammar in Fig. 3 and λ−
ZFC ’sgrammar in Fig. 1. First, λZFC ’s grammar defines a language of terms that are
already encoded as sets. Second, instead of the symbols ∅ and ω, it includes, asvalues, encoded sets of values. Most of these value terms are infinite, such as theencoding of ω. Third, it includes encoded sets of expressions.
The language of n is N := {htvar , ii | i ∈ ω}. The rules for e and v aremutually recursive. Interpreted, but leaving out some of e’s rules, they are
Fe (E, V ) := N ∪ V ∪ {htapp , ef , ex i | hef , ex i ∈ E × E} ∪ · · · ∪{htset , ei | e ∈ P< (E, κ)}(7)

Fv (E, V ) := {afalse , atrue } ∪ {htλ , ei | e ∈ E} ∪ {htset , vi | v ∈ P< (V , κ)}
To use Theorem 2, we need to iterate a single function. Note that the language
pair hE, V i = h{e, ...}, {v, ...}i is isomorphic to the single set of tagged terms

v⇓v

(val)

ef ⇓ htλ , ey i ex ⇓ vx ey [0\vx ] ⇓ vy
ec ⇓ atrue et ⇓ vt ec ⇓ afalse ef ⇓ vf
(ap)
(if)
htapp , ef , ex i ⇓ vy
htif , ec , et , ef i ⇓ vt htif , ec , et , ef i ⇓ vf(a) Standard call-by-value reduction ruleseA ⇓ vA Vset (vA ) ex ⇓ vx vx ∈ snd(vA )ht∈ , ex , eA i ⇓ atrueeA ⇓ vA Vset (vA ) ex ⇓ vx vx 6∈ snd(vA )(in)ht∈ , ex , eA i ⇓ afalseeA ⇓ vA Vset (vA ) ∀ vx ∈ snd(vA ). Vset (vx )(union)eA ⇓ vA Vset (vA )(pow)b(vA )
htP , eA i ⇓ P

Sht∪ , eA i ⇓ b (vA )eA ⇓ vA Vset (vA ) ef ⇓ htλ , ey i Ib(htλ , ey i , vA ) ⇓ vy
(image)htimage , ef , eA i ⇓ vy
Eset (eA ) ∀ ex ∈ snd(eA ). ∃ vx . ex ⇓ vx
(set)
eA ⇓ htset , {vx | ex ∈ snd(eA ) ∧ ex ⇓ vx }ieA ⇓ vA Vset (vA )(card)b(vA )
htcard , eA i ⇓ C
eA ⇓ htset , {vx }i(take)
httake , eA i ⇓ vx(b) λZFC -specific rules

Fig. 4: Reduction rules defining λZFC ’s big-step, call-by-value semantics.

EV = {h0, ei , ..., h1, vi , ...}. Binary disjoint union, denoted E t V , createssuch sets. We define Fev by Fev (E t V ) = Fe (E, V ) t Fv (E, V ). By Theorem 2,κκ.
, so we define E and V by E t V = Fev
its least fixpoint is Fev
To make well-founded substitution easy, we will use capturing substitution,
which does not capture when used on closed terms. Let Cl(e) indicate whether
a term is closed—this is structurally recursive. Then E 0 := {e ∈ E | Cl(e)} andV 0 := {v ∈ V | Cl(v)} contain only closed terms. Lastly, we define λZFC := E 0 .

4

λZFC ’s Big-Step Reduction Semantics

We distinguish sets from other expressions using Eset and Vset , which merely
check tags. We also lift set constructors to operate on encoded sets. For example,b A ) := set(|snd(vA )|) extracts the tagged set from vA , applies
for cardinality, C(v| · |, and recursively tags the resulting cardinal number. The rest areb A ) := htset , {htset , vx i | vx ∈ P(snd(vA ))}iP(vSb (vA ) := htset , S{snd(vx ) | vx ∈ snd(vA )}i(8)

b f , vA ) := htset , {htapp , vf , vx i | vx ∈ snd(vA )}i
I(v
All but Ib return values. Sets returned by Ib are intended to be reduced further.
We use e[n\v] for De Bruijn substitution. Because e and v are closed, it is easy
to define it using simple structural recursion on terms; it is thus conservative.
Figure 4 shows the reduction rules that define the reduction relation ‘⇓’.
Figure 4a has standard call-by-value rules: values reduce to themselves, andapplications reduce by substitution. Figure 4b has the λZFC -specific rules. Most

simply use Vset to check tags before applying a lifted operator. The (image)rule replaces each value vx in the set vA with an application, generating a set
expression, and the (set) rule reduces all the terms inside a set expression.
To define ‘⇓’ as a least fixpoint, we adapt Aczel’s treatment [2]. We first
define a bounding set for ‘⇓’ using closed terms, or U := E 0 × V 0 , so that ⇓ ⊆ U.
The rules in Fig. 4 can be used to define a predicate D(R, he, vi). This predicate indicates whether some reduction rule, after replacing every ‘⇓’ in its premisewith the approximation R, derives the conclusion e ⇓ v.1 Using D, we define afunction that derives new conclusions from the known conclusions in R:
F⇓ (R) := {c ∈ U | D(R, c)}(9)For example, F⇓ (∅) = {hv, vi | v ∈ V }, by the (val) rule. F⇓ (F⇓ (∅)) includes all
pairs of non-value expressions and the values they reduce to in one derivation, as
well as {hv, vi | v ∈ V }. Generally, (val) ensures that iterating F⇓ is monotone.
For F⇓ itself to be non-monotone, for some R ⊆ R0 ⊆ U, there would haveto be a conclusion c ∈ F⇓ (R) that is not in F⇓ (R0 ). In other words, having more
known conclusions could falsify a premise. None of the rules in Fig. 4 can do so.
Because F⇓ is monotone and iterating it is monotone, we can define ⇓ := F⇓γ
for some ordinal γ. If λZFC had only finite terms, γ = ω iterations would reacha fixpoint. But a simple countable term shows why ‘⇓’ cannot be F⇓ω .
Example 8 (countably infinite term). If s is the successor function in λZFC , theterm t := htset , {0, htapp , s, 0i , htapp , s, htapp , s, 0ii , ...}i should reduce to set(ω).
The (set) rule’s premises require each of t’s subterms to reduce—using at least F⇓ωbecause each subterm requires a finite, unbounded number of (ap) derivations.
s(ω)
Though F⇓
reduces t, for larger terms, we must iterate F⇓ much further. ♦Theorem 3. ⇓ := F⇓κ is the least fixpoint of F⇓ .
Proof. Fixpoint by Aczel [2, Theorem 1.3.4]; least fixpoint by Theorem 1.

tu

Lastly, ZFC theorems that do not depend on κ can be applied to λZFC terms.
Theorem 4. λZFC ’s set values and ht∈ , ·, ·i are a model of ZFC-κ.
Proof. V(κ), a model of ZFC-κ, is isomorphic to v ::= htset , {v ∗κ }i.

5tu

Syntactic Sugar and a Small Set Library

From here on, we write only λ−ZFC terms, assume FJ·K is applied, and no longer
distinguish λ−
ZFC from λZFC .
We use names instead of De Bruijn indexes and assume names are converted.
We get alpha equivalence for free; for example, λ x. x = htλ , htvar , 0ii = λ y. y.
λZFC does not contain terms with free variables. To get around this technicallimitation, we assume free variables are metalanguage names for closed terms.
1

D is definable in first-order logic, but its definition does not aid understanding much.

S
We allow the primitives ‘∈’, , take, P, image and card to be used as if they
were functions. Enclosing infix operators in parenthesis refers to them as functions, as in (∈). We partially apply infix functions using Haskell-like sectioning
rules, so (x ∈) means λ A. x ∈ A and (∈ A) means λ x. x ∈ A.
We define first-order objects using ‘:=’, as in 0 := ∅, and syntax with ‘:≡’, asin λ x1 x2 ... xn . e :≡ λ x1 . λ x2 ... xn . e to automatically curry. Function definitions
expand to lambdas (using fixpoint combinators for recursion); for example, x = y:= x ∈ {y} and (=) := λ x y. x ∈ {y} equivalently define (=) in terms of (∈). We
destructure pairs implicitly in binding patterns, as in λ hx, yi. f x y.
To do anything useful, we need a small set library. The definitions are similar
to the metalanguage definitions we omitted in Section 2, and we similarly elide
most of the λZFC definitions. However, some deserve special mention.
Because λZFC has only functional replacement, we cannot define unbounded∀ and ∃. But S
we can define bounded quantifiers in terms of bounded selection, or
select f A :=(image (λ x. if (f x) {x} ∅) A). We also define a bounded description operator ι x ∈ eA . ef :≡ take (select (λ x. ef ) eA ). Note ι x ∈ eA . ef reduces
only if ef ⇓ true for exactly one x ∈ eA .
Thus, converting a predicate to an object requires both unique existence anda bounding set. For S
example, if he
Sx , ey i :≡ {{ex }, {ex , ey }} defines ordered pairs,
then fst p := ι x ∈ ( p). ∃ y ∈ ( p). p = hx, yi takes the first element.
The set monad simulates nondeterministic choice. We define it byS
returnset a := {a}bindset A f :=(image f A)
(10)
S
Using bind m f = join (lift f m), evidently liftset := image and joinset := . The
proofs of the monad laws follow the proofs for the list monad. We also define{x ∈ eA }. ef :≡ bindset (λ x. ef ) eA , read “choose x in eA , then ef .” For example,
binary cartesian product is A × B := {x ∈ A}. {y ∈ B}. returnset hx, yi.
Every f ∈ A → B is shaped f = {hx1 , y1 i , hx2 , y2 i , ...} and is total on A. To
distinguish these hash tables from lambdas, we call them mappings. They canbe applied by ap f x := ι y ∈ (range f). hx, yi ∈ f , but we write just f x. We define
ef |eA :≡ image (λ x. hx, ef xi) eA to convert a lambda or to restrict a mapping toeA . We usually use λ x ∈ eA . ey :≡ (λ x. ey )|eA to define mappings.
A sequence of A is a mapping xs ∈ α → A for some ordinal α. For example,
ns := λ n ∈ ω. n is a countable sequence in ω → ω of increasing finite ordinals.
We assume useful sequence functions like map, map2 and drop are defined.

6

Example: The Reals From the Rationals

Here, we demonstrate that λZFC is computationally powerful enough to construct
the real numbers. For a clear, well-motivated, rigorous treatment in first-order set
theory without lambdas, we recommend Abbott’s excellent introductory text [1].
Assume we have a model Q, +Q , −Q , ×Q , ÷Q of the rationals and rationalarithmetic.2 To get the reals, we close the rationals under countable limits.
2

Though the λZFC development of Q is short and elegant, it does not fit in this paper.

We represent limits of rationals with sequences in ω → Q. To select only
the converging ones, we must define what convergence means. We start withconvergence to zero and equivalence. Given Q+ , ‘<Q ’ and | · |Q , define
conv-zero?R xs := ∀ ε ∈ Q+ . ∃ N ∈ ω. ∀ n ∈ ω. (N ∈ n ⇒ |xs n|Q <Q ε)
xs =R ys := conv-zero?R (map2 (−Q ) xs ys)(11)

So a sequence xs ∈ ω → Q converges to zero if, for any positive ε, there is someindex N after which all xs are smaller than ε. Two sequences are equivalent (=R )if their pointwise difference converges to zero.
We should be able to drop finitely many elements from a converging sequence
without changing its limit. Therefore, a sequence of rationals converges to something when it is equivalent to all of its suffixes. We thus define an equivalent to
the Cauchy convergence test, and use it to select the converging sequences:conv?R xs := ∀ n ∈ ω. xs =R (drop n xs)
R := select conv?R (ω → Q)

(12)

But R (equipped with the equivalence relation =R ) is not the real numbers as
they are normally defined: converging sequences in R may be equivalent but notequal. To decide real equality using λZFC ’s ‘=’, we partition R into disjoint setsof equivalent sequences—we make a quotient space. Thus,
quotient A (=A ) := image (λ x. select (=A x) A) A
R := quotient R (=R )(13)

defines the reals with extensional equality.
To define real arithmetic, we must lift rational arithmetic to sequences andthen to sets of sequences. The map2 function lifts, say, +Q to sequences, as in(+R ) := map2 (+Q ). To lift +R to sets of sequences, note that sets of sequences
are models of nondeterministic sequences, suggesting the set monad. We define
lift2set f A B := {a ∈ A}. {b ∈ B}. returnset (f a b) to lift two-argument functions
to the set monad. Now (+) := lift2set (+R ), and similarly for the other operators.
Using lift2set is atypical, so we prove that A + B ∈ R when A ∈ R and B ∈ R,
and similarly for the other operators. It follows from the fact that the rational
operators lifted to sequences are surjective morphisms, and this theorem:
Theorem 5. Suppose =X is an equivalence relation on X, and define its quotient X := quotient X (=X ). If op is surjective on X and a binary morphism for=X , then (lift2set op A B) ∈ X for all A ∈ X and B ∈ X.
Proof. Reduce to an equality. Case ‘⊆’ by morphism; case ‘⊇’ by surjection. tu
Now for real limits. If R+ , ‘<’, and | · | are defined, we can define conv-zero?R ,which is like (11) but operates on real sequences xs ∈ ω → R. We then define
limitR xs := ι y ∈ R. conv-zero?R (map (− y) xs) to calculate their limits.
From here, it is not difficult to treat Q and R uniformly by redefining Q ⊂ R.

7

Example: Computable Real Limits

Exact real computation has been around since Turing’s seminal paper [18]. The
novelty here is how we do it. We define the limit monad in λZFC for expressing
calculations involving limits, with bindlim defined in terms of a general limit.
We then derive a limit-free, computable replacement bind0lim . Replacing bindlim
with bind0lim in a λZFC term incurs proof obligations. If they can be met, thecomputable λZFC term has the same limit as the original, uncomputable term.
In other words, entirely in λZFC , we define uncomputable things, and gradually turn them into computable, directly implementable approximations.
The proof obligations are related to topological theorems [12] that we will
import as lemmas. By Theorem 4, we are allowed to use them directly.
At this point, it is helpful to have a simple, informal type system, which we
can easily add to the untyped λZFC . A ⇒ B is a lambda or mapping type. A → B
is the set of total mappings from A to B. A set is a membership proposition.
7.1

The Limit Monad

We first need a universe U of values that is closed under sequencing; i.e. if A ⊂ Uthen so is ω → A. Define U as the language of u ::= R | ω → u. A complete
product metric δ : U ⇒ U ⇒ R exists; therefore, a function limit : (ω → U) ⇒ U
similar to limitR exists that calculates limits. These are all λZFC -definable.
The limit monad’s computations are of type ω → U. The type does not imply
convergence, which must be proved separately. Its run function is limit.
Example 9 (infinite series). Define partial-sums : (ω → R) ⇒ (ω → R) first bypartial-sums0 xs := λ n. if (n = 0) (xs 0) ((xs n) + (partial-sums0 xs (n − 1))). (Thesequence is recursively defined, so we cannot use λ n ∈ ω. e to immediately createit.) ThenP
restrict its output: partial-sums xs := (partial-sums0 xs)|ω .
Now n∈ω e :≡ limit (partial-sums λ n ∈ ω. e), or the limit of partial sums.
1.
♦
Even if xs converges, partial-sums xs may not; e.g. if xs = λ n ∈ ω. n+1
The limit monad’s returnlim : U ⇒ (ω → U) creates constant sequences, andits bindlim : (ω → U) ⇒ (U ⇒ (ω → U)) ⇒ (ω → U) simply takes a limit:
returnlim x := λ n ∈ ω. x

bindlim xs f := f (limit xs)(14)

The left identity and associativity monad laws hold using ‘=’ for equivalence.
However, right identity holds only in the limit, so we define equivalence by
xs =lim ys := limit xs = limit ys.
Example 10 (lifting). Define liftlim f xs := bindlim xs λ x. returnlim (f x), as is typical. Substituting bindlim and reducing reveals that f (limit xs) = limit (liftlim f xs).
That is, using liftlim pulls limit out of f ’s argument.
♦
Example 11 (exponential). The Taylor series expansion of the exponential funcn
tion is exp-seq : R ⇒ (ω → R), defined by exp-seq x := partial-sums λ n ∈ ω. xn! .
PnIt always converges, so limit (exp-seq x) = n∈ω xn! = exp x for x ∈ R. To exponentiate converging sequences, define explim xs := bindlim xs exp-seq.
♦

7.2

The Computable Limit MonadWe derive the computable limit monad in two steps. In the first, longest step,
we replace the limit monad’s defining functions with those that do not use limit.
But computations will still have type ω → U, whose inhabitants are not directly
implementable, so in the second step, we give them a lambda type.
We define return0lim := returnlim . A drop-in, limit-free replacement for bindlim
does not exist, but there is one that incurs three proof obligations. Without
imposing rigid constraints on using bindlim , we cannot meet them automatically.
But we can separate them by factoring bindlim into liftlim and joinlim .
Limit-Free Lift. Substituting to get liftlim f xs = returnlim (f (limit xs)) exposes
the use of limit. Removing it requires continuity and definedness.
Lemma 1 (continuity in metric spaces). Let f : A ⇒ B with A a metricspace. Then f is continuous at x ∈ A if and only if for all xs ∈ ω → A for which
limit xs = x and f is defined on all elements of xs, f (limit xs) = limit (map f xs).
So if f : U ⇒ U is continuous at limit xs, and f is defined on all xs, thenlimit (liftlim f xs) = limit (returnlim (f (limit xs)))= limit (returnlim (limit (map f xs)))= limit (map f xs)(15)

Thus, liftlim f xs =lim map f xs, so lift0lim f xs := map f xs. Using liftlim f xs insteadof lift0lim f xs requires f to be continuous at limit xs and defined on all xs.
Limit-Free Join. Using join m = bind m λ x. x results in joinlim = limit. Removing limit might seem hopeless—until we distribute it pointwise over xss.
Lemma 2 (limits of sequences). Let f ∈ ω → ω → A, where ω → A has a
product topology. Then limit f = λ n ∈ ω. limit (flip f n), where flip f x y := f y x.
A countable product metric defines a product topology, so joinlim xss :=λ n ∈ ω. limit (flip xss n). Now we can remove limit by restricting joinlim ’s input.
Definition 1 (uniform convergence). A sequence f ∈ ω → ω → U converges
uniformly if ∀ ε ∈ R+ . ∃ N ∈ ω. ∀ n, m > N. (δ (f n m) (limit (f n))) < ε.
Lemma 3 (collapsing limits). If f ∈ ω → ω → U converges uniformly, andr, s : ω ⇒ ω increase, then limit λ n ∈ ω. limit (f n) = limit λ n ∈ ω. f (r n) (s n).
So if flip xss converges uniformly, thenlimit (joinlim xss) = limit λ n ∈ ω. limit (flip xss n)= limit λ n ∈ ω. flip xss (r n) (s n)(16)

We define join0lim : (ω → ω → U) ⇒ (ω → U) by join0lim xss := λ n ∈ ω. xss n n.
Replacing joinlim xss with join0lim xss requires that flip xss converge uniformly.

Limit-Free Bind. Define bind0lim xs f := join0lim (lift0lim f xs). It inherits obligations to prove that f is continuous at limit xs and defined on all xs, and to provethat flip (map f xs) converges uniformly.
Example 12 (exponential cont.). Define exp0lim by replacing bindlim by bind0lim in
explim , so exp0lim xs := bind0lim xs exp-seq. We now meet the proof obligations.
Lemma 4. Let f : A ⇒ (ω → B). If ω → B has a product topology, then f iscontinuous if and only if (flip f) n is continuous for every n ∈ ω.
We have a product topology, so for the first obligation, pointwise continuity is enough. Let g := flip exp-seq. Every g n is a finite polynomial, and thus
continuous. The second obligation, that exp-seq is defined on all xs, is obvious.
The third, that flip (map exp-seq xs) converges uniformly, can be proved using
the Weierstrass M test [1, Theorem 6.4.5].
♦
Example 13 (π). The definition of arctanlim is like explim ’s. Defining arctan0lim ,including proving correctness, is like defining exp0lim . To compute π, we use
πlim :=((returnlim 16) ×lim (arctanlim (returnlim 51 ))) −lim1)))((returnlim 4) ×lim (arctanlim (returnlim 239(17)

where (·)lim are lifted arithmetic operators. Because (17) does not directly use
0
imposes no proof obligations.
♦bindlim , defining the limit-free πlim
In general, using functions defined in terms of bind0lim requires little more workthan using functions on finite values. The implicit limits are pulled outward andcollapse on their own, hidden within monadic computations.
Computable Sequences. Lambdas are the simplest model of ω → U. After manipulating some terms, we define the final, computable limit monad by
return0lim x := λ n. x and bind0lim xs f := λ n. f (xs n) n. Computations have typeω ⇒ U0 , where U0 contains countable sequences of rationals.
Implementation. We have transliterated return0lim , bind0lim , exp0lim , arctan0lim and0
πlim
into Racket [7], using its built-in models of ω and Q. Even without optimiza0
tions, πlim
141 yields a rational approximation in a few milliseconds that is cor0
are almost identirect to 200 digits. More importantly, exp0lim , arctan0lim and πlim
cal to their counterparts in the uncomputable limit monad, and meet their proof
obligations. The code is clean, short, correct and reasonably fast, and resides ina directory named flops2012 at https://github.com/ntoronto/plt-stuff/.

8

Related WorkO’Connor’s completion monad [13] is quite similar to the limit monad. Bothoperate on general metric spaces and compute to arbitrary precision. O’Connor

starts with computable approximations and completes them using a monad.
Implementing it in Coq took five months. It is certainly correct.
We start with a monad for exact values and define a computable replacement. It was two weeks from conception to implementation. Between directly
using well-known theorems, and deriving the computable monad from the uncomputable monad without switching languages, we are as certain as we can bewithout mechanically verifying it. We have found our middle ground.
Higher-order logics such as HOL [11], CIC [5], MT [4] (Map Theory) andEFL* [6] continue Church’s programme to found mathematics on the lambda
calculus. Like λZFC , interpreting them in set theory seems to require a slightly
stronger theory than plain ZFC. HOL and CIC ensure consistency using types,
and use the Curry-Howard correspondence to extract programs.
MT and EFL* are more like λZFC in that they are untyped. MT ensuresconsistency partly by making nontermination a truth value, and EFL* partly
by tagging propositions. Both support classical reasoning. MT and EFL* areinterpreted in set theory using a straightforward extension of Scott-style denotational semantics to κ-sized domains, while λZFC is interpreted in set theory
using a straightforward extension of operational semantics to κ-sized relations.
The key difference between λZFC and these higher-order logics is that λZFC
is not a logic. It is a programming language with infinite terms, which by design
includes a transitive model of set theory (Theorem 4). Therefore, ZFC theorems
can be applied to its set-valued terms with only trivial interpretation, whereas
the interpretation it takes to apply ZFC theorems to lambda terms that represent
sets in MT or EFL* can be highly nontrivial. Applying a ZFC theorem in HOL
or CIC requires re-proving it to the satisfaction of a type checker.
The infinitary lambda calculus [10] has “infinitely deep” terms. Although it
exists for investigating laziness, cyclic data, and undefinedness in finitary languages, it is possible to encode uncomputable mathematics in it. In λZFC , such
up-front encodings are unnecessary.
Hypercomputation [14] describes many Turing machine extensions, including
completion of transfinite computations. Much of the research is for discovering
the properties of computation in physically plausible extensions. While λZFC
might offer a civilized way to program such machines, we do not think of ourwork as hypercomputation, but as approaching computability from above.

9

Conclusions and Future WorkWe defined λZFC , which can express essentially anything constructible in contemporary mathematics, in a way that makes it compatible with existing first-ordertheorems. We demonstrated that it makes deriving computational meaning easier by defining the limit monad in it, deriving a computable replacement, andcomputing real numbers to arbitrary accuracy with acceptable speed.
Our main future work is using λZFC to define languages for Bayesian inference, then deriving implementations that compute converging probabilities. Wehave already done this successfully for countable Bayesian models [17]. Having
built our previous work’s foundation, we can now proceed with it.
Overall, we no longer have to hold back when a set-theoretic construction
could be defined elegantly with untyped lambdas or recursion, or generalized precisely with higher-order functions. If we can derive a computable replacement, wemight help someone in Cantor’s Paradise compute the apparently uncomputable.

References
1. Abbott, S.: Understanding Analysis. Springer (2001)
2. Aczel, P.: An introduction to inductive definitions. Studies in Logic and the Foundations of Mathematics 90, 739–782 (1977)
3. Barras, B.: Sets in Coq, Coq in sets. Journal of Formalized Reasoning 3(1) (2010)
4. Berline, C., Grue, K.: A κ-denotational semantics for Map Theory in ZFC+SI.
Theoretical Computer Science 179(1–2), 137–202 (1997)
5. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development.
Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer
Science, Springer Verlag (2004), http://www.labri.fr/publications/l3a/2004/BC04
6. Flagg, R.C., Myhill, J.: A type-free system extending ZFC. Annals of Pure andApplied Logic 43, 79–97 (1989)
7. Flatt, M., PLT: Reference: Racket. Tech. Rep. PLT-TR-2010-1, PLT Inc. (2010),
http://racket-lang.org/tr1/
8. Hrbacek, K., Jech, T.: Introduction to set theory. Pure and Applied Mathematics,
M. Dekker (1999)
9. Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D. thesis, Universityof Cambridge (2002)
10. Kennaway, R., Klop, J.W., Sleep, M.R., jan De Vries, F.: Infinitary lambda calculus. Theoretical Computer Science 175, 93–125 (1997)
11. Leivant, D.: Higher order logic. In: In Handbook of Logic in Artificial Intelligenceand Logic Programming. pp. 229–321. Clarendon Press (1994)
12. Munkres, J.R.: Topology. Prentice Hall, second edn. (2000)
13. O’Connor, R.: Certified exact transcendental real number computation in Coq. In:
TPHOLs’08. pp. 246–261 (2008)
14. Ord, T.: The many forms of hypercomputation. Applied Mathematics and Computation 178, 143–153 (2006)
15. Paulson, L.C.: Set theory for verification: II. Induction and recursion. Journal ofAutomated Reasoning 15, 167–215 (1995)
16. Paulson, L.C.: Set theory for verification: I. From foundations to functions. Journalof Automated Reasoning 11, 353–389 (1993)
17. Toronto, N., McCarthy, J.: From Bayesian notation to pure Racket, via measuretheoretic probability in λZFC . In: Implementation and Application of Functional
Languages (2010)
18. Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. In: Proceedings of the London Mathematical Society. vol. 42, pp.
230–265 (1936)
19. Tzouvaras, A.: Cardinality without enumeration. Studia Logica: An International
Journal for Symbolic Logic 80(1), 121–141 (June 2005)
20. Uzquiano, G.: Models of second-order Zermelo set theory. The Bulletin of Symbolic
Logic 5(3), 289–302 (1999)
21. Werner, B.: Sets in types, types in sets. In: TACS’97. pp. 530–546 (1997)