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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abbott, S.: Understanding Analysis. Springer (2001)
Aczel, P.: An introduction to inductive definitions. Studies in Logic and the Foundations of Mathematics 90, 739–782 (1977)
Barras, B.: Sets in Coq, Coq in sets. Journal of Formalized Reasoning 3(1) (2010)
Berline, C., Grue, K.: A κ-denotational semantics for Map Theory in ZFC+SI. Theoretical Computer Science 179(1-2), 137–202 (1997)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004), http://www.labri.fr/publications/l3a/2004/BC04
Flagg, R.C., Myhill, J.: A type-free system extending ZFC. Annals of Pure and Applied Logic 43, 79–97 (1989)
Flatt, M.: PLT: Reference: Racket. Tech. Rep. PLT-TR-2010-1, PLT Inc. (2010), http://racket-lang.org/tr1/
Hrbacek, K., Jech, T.J.: Introduction to set theory. Pure and Applied Mathematics. M. Dekker (1999)
Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D. thesis, University of Cambridge (2002)
Kennaway, R., Klop, J.W., Sleep, M.R., Jan De Vries, F.: Infinitary lambda calculus. Theoretical Computer Science 175, 93–125 (1997)
Leivant, D.: Higher order logic. In: Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 229–321. Clarendon Press (1994)
Munkres, J.R.: Topology, 2nd edn. Prentice Hall (2000)
O’Connor, R.: Certified Exact Transcendental Real Number Computation in Coq. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 246–261. Springer, Heidelberg (2008)
Ord, T.: The many forms of hypercomputation. Applied Mathematics and Computation 178, 143–153 (2006)
Paulson, L.C.: Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning 15, 167–215 (1995)
Paulson, L.C.: Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning 11, 353–389 (1993)
Toronto, N., McCarthy, J.: From Bayesian Notation to Pure Racket, via Measure-Theoretic Probability in λ ZFC. In: Hage, J., Morazán, M.T. (eds.) IFL 2010. LNCS, vol. 6647, pp. 89–104. Springer, Heidelberg (2011)
Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society 42, 230–265 (1936)
Tzouvaras, A.: Cardinality without enumeration. Studia Logica: An International Journal for Symbolic Logic 80(1), 121–141 (2005)
Uzquiano, G.: Models of second-order Zermelo set theory. The Bulletin of Symbolic Logic 5(3), 289–302 (1999)
Werner, B.: Sets in Types, Types in Sets. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 530–546. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Toronto, N., McCarthy, J. (2012). Computing in Cantor’s Paradise with λ ZFC . In: Schrijvers, T., Thiemann, P. (eds) Functional and Logic Programming. FLOPS 2012. Lecture Notes in Computer Science, vol 7294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29822-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-29822-6_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29821-9
Online ISBN: 978-3-642-29822-6
eBook Packages: Computer ScienceComputer Science (R0)