SpringerLink
Log in

On Arithmetic Computations with Hereditarily Finite Sets, Functions and Types

  • Conference paper
Theoretical Aspects of Computing – ICTAC 2010 (ICTAC 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6255))

Included in the following conference series:

Abstract

Starting from an executable “shared axiomatization” of a number of bi-interpretable theories (Peano arithmetic, hereditarily finite sets and functions) we introduce generic algorithms that can be instantiated to implement the usual arithmetic operations in terms of (purely symbolic) hereditarily finite constructs, as well as the type language of Gödel’s System T. The Haskell code in the paper is available at http://logic.cse.unt.edu/tarau/research/2010/short_shared.hs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 52.74
Price includes VAT (France)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Kaye, R., Wong, T.L.: On Interpretations of Arithmetic and Set Theory. Notre Dame J. Formal Logic 48(4), 497–510 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  2. Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad-hoc. In: POPL, pp. 60–76 (1989)

    Google Scholar 

  3. Jones, S.P., Jones, M., Meijer, E.: Type classes: An exploration of the design space. In: Haskell Workshop (1997)

    Google Scholar 

  4. Ackermann, W.F.: Die Widerspruchsfreiheit der allgemeinen Mengenlhere. Mathematische Annalen (114), 305–315 (1937)

    Google Scholar 

  5. Tarau, P.: A Groupoid of Isomorphic Data Transformations. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) Calculemus 2009. LNCS (LNAI), vol. 5625, pp. 170–185. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Tarau, P.: An Embedded Declarative Data Transformation Language. In: Proceedings of 11th International ACM SIGPLAN Symposium PPDP 2009, Coimbra, Portugal, September 2009, pp. 171–182. ACM, New York (2009)

    Google Scholar 

  7. Misra, J.: Powerlist: a structure for parallel recursion. ACM Transactions on Programming Languages and Systems 16, 1737–1767 (1994)

    Article  Google Scholar 

  8. Li, M., Vitányi, P.: An introduction to Kolmogorov complexity and its applications. Springer, New York (1993)

    MATH  Google Scholar 

  9. Chaitin, G.J.: A theory of program size formally identical to information theory. J. Assoc. Comput. Mach. 22, 329–340 (1975)

    MATH  MathSciNet  Google Scholar 

  10. Calude, C., Salomaa, A.: Algorithmically coding the universe. In: Developments in Language Theory, pp. 472–492. World Scientific, Singapore (1994)

    Google Scholar 

  11. Pettigrew, R.: On Interpretations of Bounded Arithmetic and Bounded Set Theory. Notre Dame J. Formal Logic 50(2), 141–151 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  12. Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12(280-287), 12 (1958)

    Google Scholar 

  13. Sloane, N.J.A.: The On-Line Encyclopedia of Integer Sequences (2010), published electronically at http://www.research.att.com/~njas/sequences

  14. Lagarias, J.C.: The 3x+1 Problem: An Annotated Bibliography (1963-1999) (2008), http://ar**v.org 0309224v11

  15. Tarau, P.: Isomorphisms, Hylomorphisms and Hereditarily Finite Data Types in Haskell. In: Proceedings of ACM SAC 2009, pp. 1898–1903. ACM, New York (2009)

    Chapter  Google Scholar 

  16. Tarau, P.: Declarative Combinatorics: Isomorphisms, Hylomorphisms and Hereditarily Finite Data Types in Haskell, 104 pages (January 2009), (unpublished draft) http://ar**v.org/abs/0808.2953

  17. Takahashi, M.o.: A Foundation of Finite Mathematics. Publ. Res. Inst. Math. Sci. 12(3), 577–708 (1976)

    Article  MathSciNet  Google Scholar 

  18. Kirby, L.: Addition and multiplication of sets. Math. Log. Q. 53(1), 52–65 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  19. Kiselyov, O., Byrd, W.E., Friedman, D.P., Shan, C.-c.: Pure, declarative, and constructive arithmetic relations (declarative pearl). In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 64–80. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2/3), 95–120 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  21. The Coq development team: The Coq proof assistant reference manual. LogiCal Project. Version 8.0 (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, University of North Texas,  

    Paul Tarau

Authors
  1. Paul Tarau
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of York, YO10 5DD, York, United Kingdom

    Ana Cavalcanti  & Jim Woodcock  & 

  2. Departamento de Informática e Matemática Aplicaty, Universidade Federal do Rio Grande do Norte, Lagoa Nova, 59072-970, Natal-RN, Brazil

    David Deharbe

  3. Université de Paris-Sud, LRI, 91405, Orsay cedex, France

    Marie-Claude Gaudel

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tarau, P. (2010). On Arithmetic Computations with Hereditarily Finite Sets, Functions and Types. In: Cavalcanti, A., Deharbe, D., Gaudel, MC., Woodcock, J. (eds) Theoretical Aspects of Computing – ICTAC 2010. ICTAC 2010. Lecture Notes in Computer Science, vol 6255. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14808-8_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14808-8_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14807-1

  • Online ISBN: 978-3-642-14808-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation