Abstract
When defined with general elimination/application rules, natural deduction and λ-calculus become closer to sequent calculus. In order to get real isomorphism, normalisation has to be defined in a “multiary” variant, in which reduction rules are necessarily non-local (reason: nomalisation, like cut-elimination, acts at the head of applicative terms, but natural deduction focuses at the tail of such terms). Non-local rules are bad, for instance, for the mechanization of the system. A solution is to extend natural deduction even further to a unified calculus based on the unification of cut and general elimination. In the unified calculus, a sequent term behaves like in the sequent calculus, whereas the reduction steps of a natural deduction term are interleaved with explicit steps for bringing heads to focus. A variant of the calculus has the symmetric role of improving sequent calculus in dealing with tail-active permutative conversions.
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
Dyckhoff, R., Pinto, L.: Permutability of proofs in intuitionistic sequent calculi. Theoretical Computer Science 212, 141–155 (1999)
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/ .
Espírito Santo, J., Pinto, L.: Permutative conversions in intuitionistic multiary sequent calculus with cuts. In: Hoffman, M. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 286–300. Springer, Heidelberg (2003)
Espírito Santo, J., Pinto, L.: Confluence and strong normalisation of the generalised multiary λ-calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, Springer, Heidelberg (2004)
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)
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)
Mints, G.: Normal forms for sequent derivations. In: Odifreddi, P., Peters, A.K. (eds.) Kreiseliana, pp. 469–492. Wellesley, Massachusetts (1996)
Negri, S., von Plato, J.: Structural Proof Theory. Cambridge (2001)
Schwichtenberg, H.: Termination of permutative conversions in intuitionistic gentzen calculi. Theoretical Computer Science, 212 (1999)
von Plato, J.: Natural deduction with general elimination rules. Annals of Mathematical Logic 40(7), 541–567 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Espírito Santo, J. (2007). Refocusing Generalised Normalisation. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds) Computation and Logic in the Real World. CiE 2007. Lecture Notes in Computer Science, vol 4497. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73001-9_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-73001-9_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73000-2
Online ISBN: 978-3-540-73001-9
eBook Packages: Computer ScienceComputer Science (R0)