Nothing Special   »   [go: up one dir, main page]

Skip to main content

Alpha-Structural Recursion and Induction

(Extended Abstract)

  • Conference paper
Theorem Proving in Higher Order Logics (TPHOLs 2005)

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

Included in the following conference series:

Abstract

There is growing evidence for the usefulness of name permutations when dealing with syntax involving names and name-binding. In particular they facilitate an attractively simple formalisation of common, but often technically incorrect uses of structural recursion and induction for abstract syntax trees modulo α-equivalence. At the heart of this formalisation is the notion of finitely supported mathematical objects. This paper explains the idea in as concrete a way as possible and gives a new derivation within higher-order logic of principles of α-structural recursion and induction for α-equivalence classes from the ordinary versions of these principles for abstract syntax trees.

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

Access this chapter

Subscribe and save

Springer+ Basic
$34.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
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping 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. Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1984) (revised edition)

    MATH  Google Scholar 

  2. Cheney, J.: Nominal Logic Programming. PhD thesis, Cornell University (August 2004)

    Google Scholar 

  3. Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)

    Article  MATH  MathSciNet  Google Scholar 

  4. de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math. 34, 381–392 (1972)

    Google Scholar 

  5. Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proc. LICS 1999, pp. 193–202. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  6. Gabbay, M.J.: A Theory of Inductive Definitions with α-Equivalence: Semantics, Implementation, Programming Language. PhD thesis, University of Cambridge (2000)

    Google Scholar 

  7. Gabbay, M.J.: FM-HOL, a higher-order theory of names. In: Kamareddine, F. (ed.) Workshop on Thirty Five years of Automath, Informal Proceedings, April 2002, Heriot-Watt University, Edinburgh (2002)

    Google Scholar 

  8. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2002)

    Article  MATH  Google Scholar 

  9. Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 173–191. Springer, Heidelberg (1996)

    Google Scholar 

  10. Griffin, T.G.: Notational definition — a formal account. In: Proc. LICS 1988, pp. 372–383. IEEE Computer Society Press, Los Alamitos (1988)

    Google Scholar 

  11. Gunter, C.A.: Semantics of Programming Languages: Structures and Techniques. MIT Press, Cambridge (1992)

    MATH  Google Scholar 

  12. Honsell, F., Miculan, M., Scagnetto, I.: An axiomatic approach to metareasoning on nominal algebras in HOAS. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 963–978. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge (1986)

    MATH  Google Scholar 

  14. Norrish, M.: Recursive function definition for types with binders. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 241–256. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proc. PLDI 1988, pp. 199–208. ACM Press, New York (1988)

    Google Scholar 

  16. Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  17. Plotkin, G.D.: An illative theory of relations. In: Cooper, R., Mukai, K., Perry, J. (eds.) Situation Theory and its Applications. CSLI Lecture Notes, vol. 1, 22, pp. 133–146. Stanford University (1990)

    Google Scholar 

  18. Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004)

    Google Scholar 

  19. Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    Google Scholar 

  20. Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. Theoretical Computer Science (2005) (To appear)

    Google Scholar 

  21. Stoughton, A.: Substitution revisited. Theoretical Computer Science 59, 317–325 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  22. Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoretical Computer Science 323, 473–497 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  23. Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: Proc. CADE-20. LNCS. Springer, Heidelberg (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pitts, A.M. (2005). Alpha-Structural Recursion and Induction. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_2

Download citation

  • DOI: https://doi.org/10.1007/11541868_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28372-0

  • Online ISBN: 978-3-540-31820-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics