Computing in Cantor’s Paradise with λ _ZFC

Abstract

Applied mathematicians increasingly use computers to answer mathematical questions. We want to provide them domain-specific languages. 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 a conservative 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, and using standard topological theorems to derive a computable replacement.