[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Structural Proof Theory as Rewriting

  • Conference paper
Term Rewriting and Applications (RTA 2006)

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

Included in the following conference series:

Abstract

The multiary version of the λ-calculus with generalized applications integrates smoothly both a fragment of sequent calculus and the system of natural deduction of von Plato. It is equipped with reduction rules (corresponding to cut-elimination/normalisation rules) and permutation rules, typical of sequent calculus and of natural deduction with generalised elimination rules. We argue that this system is a suitable tool for doing structural proof theory as rewriting. As an illustration, we investigate combinations of reduction and permutation rules and whether these combinations induce rewriting systems which are confluent and terminating. In some cases, the combination allows the simulation of non-terminating reduction sequences known from explicit substitution calculi. In other cases, we succeed in capturing interesting classes of derivations as the normal forms w.r.t. well-behaved combinations of rules. We identify six of these “combined” normal forms, among which are two classes, due to Herbelin and Mints, in bijection with normal, ordinary natural deductions. A computational explanation for the variety of “combined” normal forms is the existence of three ways of expressing multiple application in the calculus.

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

Access this chapter

Log in via an institution

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. Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Studia Logica 60, 107–118 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  2. Dyckhoff, R., Pinto, L.: Permutability of proofs in intuitionistic sequent calculi. Theoretical Computer Science 212, 141–155 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  3. Espírito Santo, J.: Conservative extensions of the λ-calculus for the computational interpretation of sequent calculus. PhD thesis, University of Edinburgh (2002), available at: http://www.lfcs.informatics.ed.ac.uk/reports/

  4. Espírito Santo, J.: An isomorphism between a fragment of sequent calculus and an extension of natural deduction. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 354–366. Springer, Heidelberg (2002)

    Google Scholar 

  5. Santo, J.E., Pinto, L.: Permutative conversions in intuitionistic multiary sequent calculus with cuts. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 286–300. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Santo, J.E., Pinto, L.: Confluence and strong normalisation of the generalised multiary λ-calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 194–209. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Herbelin, H.: A λ-calculus structure isomorphic to a Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61–75. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  8. Joachimski, F., Matthes, R.: Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel’s T. Archive for Mathematical Logic 42, 59–87 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  9. Mints, G.: Normal forms for sequent derivations. In: Odifreddi, P. (ed.) Kreiseliana, pp. 469–492. A. K. Peters, Wellesley, Massachusetts (1996)

    Google Scholar 

  10. Negri, S., von Plato, J.: Structural Proof Theory, Cambridge (2001)

    Google Scholar 

  11. Rose, K.: Explicit substitutions: Tutorial & survey. Technical Report LS-96-3, BRICS (1996)

    Google Scholar 

  12. Schwichtenberg, H.: Termination of permutative conversions in intuitionistic gentzen calculi. Theoretical Computer Science 212 (1999)

    Google Scholar 

  13. von Plato, J.: Natural deduction with general elimination rules. Annals of Mathematical Logic 40(7), 541–567 (2001)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Matemática, Universidade do Minho, Braga, Portugal

    J. Espírito Santo & L. Pinto

  2. Departamento de Informática, Universidade do Minho, Braga, Portugal

    M. J. Frade

Authors
  1. J. Espírito Santo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. J. Frade
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. L. Pinto
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University,  

    Frank Pfenning

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Santo, J.E., Frade, M.J., Pinto, L. (2006). Structural Proof Theory as Rewriting. In: Pfenning, F. (eds) Term Rewriting and Applications. RTA 2006. Lecture Notes in Computer Science, vol 4098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11805618_15

Download citation

  • DOI: https://doi.org/10.1007/11805618_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36834-2

  • Online ISBN: 978-3-540-36835-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation