Computing in Cantor's Paradise With λZFC
or
How to Make an Infinitary λ-Calculus in κ Easy Steps(and Why)FLOPS 2012
Neil Toronto and Jay McCarthy
PLT @ Brigham Young University

Living in Cantor’s Paradise“No one shall expel us from the Paradise that
Cantor has created.”David Hilbert1Living in Cantor’s Paradise“No one shall expel us from the Paradise that
Cantor has created.”David Hilbert

Cantor’s Paradise (set theory) is characterized by mind-bogglingorders of ever-increasing infinities...

1Living in Cantor’s Paradise“No one shall expel us from the Paradise that
Cantor has created.”David Hilbert

Cantor’s Paradise (set theory) is characterized by mind-bogglingorders of ever-increasing infinities...
... but mathematicians still want to use computers to answer
questions!

1

Living in Cantor’s Paradise“No one shall expel us from the Paradise that
Cantor has created.”David Hilbert

Cantor’s Paradise (set theory) is characterized by mind-bogglingorders of ever-increasing infinities...
... but mathematicians still want to use computers to answer
questions!
• Simple example:
1

Options for Domain Specific Languages• Option 1: Write theorems and proofs in a proof assistant, extract
programs
Problem: Re-proving theorems takes a long time!
Hurd 2002: Dissertation half comprised of convincing HOL oftheorems from early-1900s measure theory
O’Connor 2008: Five months to convince Coq of his own
theorems (which had detailed, published proofs)

2

Options for Domain Specific Languages• Option 1: Write theorems and proofs in a proof assistant, extract
programs
Problem: Re-proving theorems takes a long time!
Hurd 2002: Dissertation half comprised of convincing HOL oftheorems from early-1900s measure theory
O’Connor 2008: Five months to convince Coq of his own
theorems (which had detailed, published proofs)• Option 2: Write semantics in contemporary math
Problem: Higher-order anything is difficult
Problem: No connection to implementation
2

Options for Domain Specific Languages• Option 1: Write theorems and proofs in a proof assistant, extract
programs
Problem: Re-proving theorems takes a long time!
Hurd 2002: Dissertation half comprised of convincing HOL oftheorems from early-1900s measure theory
O’Connor 2008: Five months to convince Coq of his own
theorems (which had detailed, published proofs)• Option 2: Write semantics in contemporary math
Problem: Higher-order anything is difficult
Problem: No connection to implementation• ∃n. Option n is a middle ground?

2

Example: Beautiful Differentiation• Elliot 2010: Derives an automatic differentiation implementationfrom this exact specification:3

Example: Beautiful Differentiation• Elliot 2010: Derives an automatic differentiation implementationfrom this exact specification:• Unimplementable because of3

Example: Beautiful Differentiation• Elliot 2010: Derives an automatic differentiation implementationfrom this exact specification:• Unimplementable because of• How Elliot does it:
1. Reformulates differentiation in terms of toD to hide use of d
2. Uses differentiation theorems and Functor and Applicative
instance definitions to derive d-free functions
3. Implements using floating-point to approximate reals
3Beautiful Derivations

4Beautiful Derivations• Problem: To elegantly derive the implementation, the derivations
have to be done in a language that doesn’t exist!

4Apologies“We have no implementation of d, so this definition of toD willserve as a specification, not an implementation.”“This definition is not executable, however, since d is not.”“Every remaining use of d is applied to a function whose
derivative is known, so we can replace each use.... Now we havean executable implementation again.”“Again, this definition can be refactored, followed by replacing thenon-effective [unimplementable] applications of d with known
derivatives.”

5

Example: From Bayesian Notation to Pure Racket• Toronto and McCarthy 2010: Derive implementation of Bayesianmodeling language from an exact specification using

6

Example: From Bayesian Notation to Pure Racket• Toronto and McCarthy 2010: Derive implementation of Bayesianmodeling language from an exact specification using• Unimplementable because

may be a countable set

6

Example: From Bayesian Notation to Pure Racket• Toronto and McCarthy 2010: Derive implementation of Bayesianmodeling language from an exact specification using• Unimplementable because

may be a countable set• How we did it:
1. Assume a very powerful lambda calculus (λZFC) exists
2. Define exact meaning of Bayesian notation in this language
3. Derive implementable approximation, prove convergence6

Apologies“[Sketch of λZFC features.] We intend λZFC to be contemporary
mathematics with well-defined lambdas, or a practical lambda
calculus with infinite sets.”7Apologies“[Sketch of λZFC features.] We intend λZFC to be contemporary
mathematics with well-defined lambdas, or a practical lambda
calculus with infinite sets.”

Our Vision:

λ calculus

7Apologies“[Sketch of λZFC features.] We intend λZFC to be contemporary
mathematics with well-defined lambdas, or a practical lambda
calculus with infinite sets.”

Our Vision:+

λ calculus

Inﬁnite Sets and Set Operations

7

Apologies“[Sketch of λZFC features.] We intend λZFC to be contemporary
mathematics with well-defined lambdas, or a practical lambda
calculus with infinite sets.”

Our Vision:+

λ calculus=

Inﬁnite Sets and Set Operations

λZFC

7

Apologies“[Sketch of λZFC features.] We intend λZFC to be contemporary
mathematics with well-defined lambdas, or a practical lambda
calculus with infinite sets.”

Our Vision:+

λ calculus=

Inﬁnite Sets and Set Operations

λZFC• “Computing in Cantor’s Paradise With λZFC” realizes this vision7

Lambda-ZFC Requirements• Must be similar to implementation language
Higher-order functions and lambdas
Computable sublanguage
Call-by-value reduction semantics

8

Lambda-ZFC Requirements• Must be similar to implementation language
Higher-order functions and lambdas
Computable sublanguage
Call-by-value reduction semantics• Must have infinite sets
Operations expressive enough to do measure theory
Apply well-known theorems with only trivial translation8

Lambda-ZFC Requirements• Must be similar to implementation language
Higher-order functions and lambdas
Computable sublanguage
Call-by-value reduction semantics• Must have infinite sets
Operations expressive enough to do measure theory
Apply well-known theorems with only trivial translation• Should treat values uniformly (all values first-class)Specifically allow lambdas in sets:
For minimalism: want to use

8Building Lambda-ZFC- From the ZFC Axioms (1)Axiom
Empty set. There is a set
elements.

λ–ZFCwith no(value symbol)

9Building Lambda-ZFC- From the ZFC Axioms (1)Axiom
Empty set. There is a set
elements.

λ–ZFCwith no(value symbol)

Powerset. The subsets of a set
comprise a set.

9Building Lambda-ZFC- From the ZFC Axioms (1)Axiom
Empty set. There is a set
elements.

λ–ZFCwith no(value symbol)

Powerset. The subsets of a set
comprise a set.
Union. The union of a set of sets is a set.

9

Building Lambda-ZFC- From the ZFC Axioms (1)Axiom
Empty set. There is a set
elements.

λ–ZFCwith no(value symbol)

Powerset. The subsets of a set
comprise a set.
Union. The union of a set of sets is a set.
Example:9Building Lambda-ZFC- From the ZFC Axioms (1)Axiom
Empty set. There is a set
elements.

λ–ZFCwith no(value symbol)

Powerset. The subsets of a set
comprise a set.
Union. The union of a set of sets is a set.
Example:Example:9Building Lambda-ZFC- From the ZFC Axioms (1)
Axiom

λ–ZFC

Empty set. There is a set
elements.

with no(value symbol)

Powerset. The subsets of a set
comprise a set.
Union. The union of a set of sets is a set.
Example:Example:Cardinality. Every set.
cardinality

has a unique

9Building Lambda-ZFC- From the ZFC Axioms (2)
Axiom

λ–ZFC

Replacement. The image of a set
under a binary predicate is a set.

10

Building Lambda-ZFC- From the ZFC Axioms (2)
Axiom

λ–ZFC

Replacement. The image of a set
under a binary predicate is a set.
Ex.: let
then

;

10

Building Lambda-ZFC- From the ZFC Axioms (2)
Axiom

λ–ZFC

Replacement. The image of a set
under a binary predicate is a set.
Ex.: let
then

;
Ex.:

10

Building Lambda-ZFC- From the ZFC Axioms (2)
Axiom

λ–ZFC

Replacement. The image of a set
under a binary predicate is a set.
;Ex.: letthenEx.: letunique set

Ex.:such that; then theis10Building Lambda-ZFC- From the ZFC Axioms (2)
Axiom

λ–ZFC

Replacement. The image of a set
under a binary predicate is a set.
;Ex.: letthenEx.: letunique set

Ex.:such that; then theisnone(hasn't been a problem)

10Building Lambda-ZFC- From the ZFC Axioms (2)
Axiom

λ–ZFC

Replacement. The image of a set
under a binary predicate is a set.
;Ex.: letthenEx.: letunique set

Ex.:such that; then theisnone(hasn't been a problem)of
Infinity. The language
is a set, where
and
.
10

Building Lambda-ZFC- From the ZFC Axioms (2)
Axiom

λ–ZFC

Replacement. The image of a set
under a binary predicate is a set.
;Ex.: letthenEx.: letunique set

Ex.:such that; then theisofInfinity. The language
is a set, where
and
.

none
(hasn't been a problem)(value symbol)

10Grammar of Finite Terms• Final λ–ZFC grammar:

11

Grammar of Finite Terms• Final λ–ZFC grammar:

11

Grammar of Finite Terms• Final λ–ZFC grammar:

11

Grammar of Finite Terms• Final λ–ZFC grammar:

11

Grammar of Finite Terms• Final λ–ZFC grammar:• Computable sublanguage: Remove

11Grammar of Finite Terms• Final λ–ZFC grammar:• Computable sublanguage: Remove• Problem: What should

reduce to?

isn’t a value...

11

An Easy (???) Solution
Solution: Include all the sets as values!

12

An Easy (???) Solution
Solution: Include all the sets as values!
• Problem 1: Set theory (the metalanguage) is single-sorted• Solution 1: Recursively encode expressions as sets using tags
(i.e. SICP-style records)(equivalently) is a lambda with body

is a set containing the members of
encoding ofis)(e.g. the12

An Easy (???) Solution
Solution: Include all the sets as values!
• Problem 1: Set theory (the metalanguage) is single-sorted• Solution 1: Recursively encode expressions as sets using tags
(i.e. SICP-style records)(equivalently) is a lambda with body

is a set containing the members of
encoding ofis)(e.g. the• Problem 2: “All the sets” is not a set• Solution 2: Find a set that acts enough like “all the sets”

12All the Sets (1)• Curious fact: unfolding

generates the hereditarily finite sets13

All the Sets (1)• Curious fact: unfolding

generates the hereditarily finite sets13

All the Sets (1)• Curious fact: unfolding• Curious fact:

generates the hereditarily finite sets

is also a number: the first countable ordinal

13

All the Sets (1)• Curious fact: unfolding• Curious fact:

generates the hereditarily finite sets

is also a number: the first countable ordinal• Can define more limit ordinals

,

,

13

All the Sets (2)• Curious fact: unfolding

actually generates all the sets

Every set first appears in some; e.g.

14

All the Sets (2)• Curious fact: unfolding

actually generates all the sets

Every set first appears in some; e.g.

• Can we stop unfolding at some ordinal and have a set of setsthat is closed under set primitives?
Yes:
is closed under set primitives; it’s called aGrothendieck universe
14All the Sets (2)• Curious fact: unfolding

actually generates all the sets

Every set first appears in some; e.g.

• Can we stop unfolding at some ordinal and have a set of setsthat is closed under set primitives?
Yes:
is closed under set primitives; it’s called aGrothendieck universe• Is there a Grothendieck universe that contains ? Undecidable.
14

Inaccessible Cardinal Axiom

Axiom (inaccessible cardinal). There exists an ordinal suchcontains and is closed under , , and replacement.
that• Call sets inhereditarily accessible sets15

Inaccessible Cardinal Axiom

Axiom (inaccessible cardinal). There exists an ordinal suchcontains and is closed under , , and replacement.
that• Call sets inhereditarily accessible sets

• Uncontroversial extension to ZFC, relatively mild (c.f. HOL, Coq)

15

Inaccessible Cardinal Axiom

Axiom (inaccessible cardinal). There exists an ordinal suchcontains and is closed under , , and replacement.
that• Call sets inhereditarily accessible sets

• Uncontroversial extension to ZFC, relatively mild (c.f. HOL, Coq)
• No corresponding λ–ZFC or λZFC expression

15

The Hierarchy of Sets

16

An Infinite Set Rule For Finite Grammars
New BNF rule:means “sets ofwith less thanelements”

17

An Infinite Set Rule For Finite Grammars
New BNF rule:means “sets ofwith less thanelements”• Example:
Equivalent toLanguage is(the hereditarily finite sets)17

An Infinite Set Rule For Finite Grammars
New BNF rule:means “sets ofwith less thanelements”• Example:
Equivalent toLanguage is(the hereditarily finite sets)• Example:
Language is(the hereditarily accessible sets)17

An Infinite Set Rule For Finite Grammars
New BNF rule:means “sets ofwith less thanelements”• Example:
Equivalent toLanguage is(the hereditarily finite sets)• Example:
Language is(the hereditarily accessible sets)• Example:
Language is every set in, recursively tagged

17

Finite Grammar of Infinite Terms• Final λZFC grammar:

18

Finite Grammar of Infinite Terms• Final λZFC grammar:• Contains encodings of all the sets in18

Finite Grammar of Infinite Terms• Final λZFC grammar:• Contains encodings of all the sets in• Computable sublanguage: replace

with

18

Finite Grammar of Infinite Terms• Final λZFC grammar:• Contains encodings of all the sets in• Computable sublanguage: replacewith• Ugly! Write in λ–ZFC with heaps of syntactic sugar; assumetransformation to λZFC before reduction18

Lambda-ZFC’s Reduction Semantics
Defines a -sized, big-step reduction relation:19

Lambda-ZFC’s Reduction Semantics
Defines a -sized, big-step reduction relation

Theorem. λZFC’s set values and(i.e. theorems that don’t depend on:

are a model of ZFC- .
are true of λZFC’s sets)

19

Expressive Enough?

• Implementable in λZFC:
Bounded logic, pairs, naturals, integers, rationals, arithmetic

20

Expressive Enough?

• Implementable in λZFC:
Bounded logic, pairs, naturals, integers, rationals, arithmetic
Reals and real limits (in the paper)

20

Expressive Enough?

• Implementable in λZFC:
Bounded logic, pairs, naturals, integers, rationals, arithmetic
Reals and real limits (in the paper)
Set-theoretic, general closure operators, metricuniverses, limits on metric spaces

20Expressive Enough?

• Implementable in λZFC:
Bounded logic, pairs, naturals, integers, rationals, arithmetic
Reals and real limits (in the paper)
Set-theoretic, general closure operators, metricuniverses, limits on metric spaces
Measure theory: Borel σ-algebras, arbitrary products of
σ-algebras, product measures, Lebesgue measure,Lebesgue integration, conditional probability measures

20

Example Application: Limit Monad• Values: languageof21

Example Application: Limit Monad• Values: language• Computations:of(converging sequences of values)

21

Example Application: Limit Monad• Values: language• Computations:of(converging sequences of values)• Run function:

21

Example Application: Limit Monad• Values: language• Computations:of(converging sequences of values)• Run function:

Example:21

Example Application: Limit Monad• Values: language• Computations:of(converging sequences of values)• Run function:

Example:Example:21

Uncomputable Limit Monad• Defining functions:22Uncomputable Limit Monad• Defining functions:• Example:

22

Uncomputable Limit Monad• Defining functions:• Example:• Wish for: limit-free, drop-in replacement forReality says: Sorry Bucko, only under limited conditions

22Uncomputable Limit Monad• Defining functions:• Example:• Wish for: limit-free, drop-in replacement forReality says: Sorry Bucko, only under limited conditions• Step 1: Factor using monad identities and topological theorems

22Computable Limit Monad• Step 2: Collapse limits using topological theorems
Identity

Condition (per-instance)Continuity

23

Computable Limit Monad• Step 2: Collapse limits using topological theorems
Identity

Condition (per-instance)Continuity
Uniform Convergence23Computable Limit Monad• Step 2: Collapse limits using topological theorems
Identity

Condition (per-instance)Continuity
Uniform Convergence• Limit-free replacement for:

23

Computable Limit Monad• Step 2: Collapse limits using topological theorems
Identity

Condition (per-instance)Continuity
Uniform Convergence• Limit-free replacement for• Prove conditions for use of:in; then redefine23Limit Monad Example: Computing πMachin’s formula (1706):24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Proof

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

Continuity
Unif. conv.

24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Proof

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

Continuity
Unif. conv.

24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Proof

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

Continuity
Unif. conv.
(define (atan-lim ys)(bind ys atan-seq))24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Proof

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

Continuity
Unif. conv.
(define (atan-lim ys)(bind ys atan-seq))24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Proof

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

Continuity
Unif. conv.
(define (atan-lim ys)(bind ys atan-seq))

None

24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Proof

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

Continuity
Unif. conv.
(define (atan-lim ys)(bind ys atan-seq))None(define pi-lim(-lim (*lim (r 16) (atan-lim (r 1/5)))(*lim (r 4) (atan-lim (r 1/239)))))

24

Limit Monad Example: Computing πMachin’s formula (1706):
λZFC

Proof

Racket(define (atan-seq y)(sums (λ (n) (/ (* (expt -1 n)(expt y (+ (* n 2) 1)))(+ (* n 2) 1)))))

Continuity
Unif. conv.
(define (atan-lim ys)(bind ys atan-seq))None(define pi-lim(-lim (*lim (r 16) (atan-lim (r 1/5)))(*lim (r 4) (atan-lim (r 1/239)))))> (real->decimal-string (time (pi-lim 141)) 200)
cpu time: 10 real time: 18 gc time: 0"3.1415926535897932384626433832795028841971693993751058[...]"
24

Conclusions and Future Work• We did awesome things
Defined λZFC, which can express anything “constructive”;
proved almost all theorems apply directly to λZFC terms
Defined the limit monad, defined π in it, derived an
implementation, transliterated it into Racket

25Conclusions and Future Work• We did awesome things
Defined λZFC, which can express anything “constructive”;
proved almost all theorems apply directly to λZFC terms
Defined the limit monad, defined π in it, derived an
implementation, transliterated it into Racket• We will do more awesome things

25Conclusions and Future Work• We did awesome things
Defined λZFC, which can express anything “constructive”;
proved almost all theorems apply directly to λZFC terms
Defined the limit monad, defined π in it, derived an
implementation, transliterated it into Racket• We will do more awesome things• Bonus Questions!
How much deep set theory do I need to know to use λZFC?
Can proofs about λZFC terms be used in contemporary math?
How would one make a call-by-name version of λZFC?
Why is?

25