Abstract
Calculi with explicit substitutions (ES) are widely used in different areas of computer science. Complex systems with ES were developed these last 15 years to capture the good computational behaviour of the original systems (with meta-level substitutions) they were implementing.
In this paper we first survey previous work in the domain by pointing out the motivations and challenges that guided the development of such calculi. Then we use very simple technology to establish a general theory of explicit substitutions for the lambda-calculus which enjoys fundamental properties such as simulation of one-step beta-reduction, confluence on metaterms, preservation of beta-strong normalisation, strong normalisation of typed terms and full composition. The calculus also admits a natural translation into Linear Logic’s proof-nets.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arbiser, A., Bonelli, E., Ríos, A.: Perpetuality in a lambda calculus with explicit substitutions and composition. In: WAIT (2000)
Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.-J.: Explicit substitutions. JFP 4(1), 375–416 (1991)
Arbiser, A.: Explicit Substitution Systems and Subsystems. PhD thesis, Universidad Buenos Aires (2006)
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1984)
Barendregt, H.: Lambda calculus with types. Handbook of Logic in Computer Science 2 (1992)
Benaissa, Z.-E.-A., Briaud, D., Lescanne, P., Rouyer-Degli, J.: λυ, a calculus of explicit substitutions which preserves strong normalisation. JFP (1996)
Bloo, R., Geuvers, H.: Explicit substitution: on the edge of strong normalization. TCS 6(5), 699–722 (1999)
Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University of Technology (1997)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bloo, R., Rose, K.: Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In: Computer Science in the Netherlands (1995)
de Bruijn, N.: Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indag. Mat. 5(35), 381–392 (1972)
de Bruijn, N.: Lambda-calculus notation with namefree formulas involving symbols that represent reference transforming mappings. Indag. Mat. 40, 356–384 (1978)
Di Cosmo, R., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. In: Tiuryn, J. (ed.) ETAPS 2000 and FOSSACS 2000. LNCS, vol. 1784, Springer, Heidelberg (2000)
David, R., Guillaume, B.: A λ-calculus with explicit weakening and explicit substitution. MSCS 11, 169–206 (2001)
Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. I&C 157, 183–235 (2000)
Dyckhoff, R., Urban, C.: Strong normalisation of Herbelin’s explicit substitution calculus with substitution propagation. In: WESTAPP 2001 (2001)
de Flavio Moura, M.A.-R., Kamareddine, F.: Higher order unification: A structural relation between Huet’s method and the one based on explicit substitution. Available from http://www.macs.hw.ac.uk/~fairouz/papers/
Forest, J.: A weak calculus with explicit operators for pattern matching and substitution. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, Springer, Heidelberg (2002)
Girard, J.-Y.: Linear logic. TCS 50(1), 1–101 (1987)
Goubault-Larrecq, J.: Conjunctive types and SKInT. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, Springer, Heidelberg (1999)
Hardin, T.: Résultats de confluence pour les règles fortes de la logique combinatoire catégorique et liens avec les lambda-calculs. Thèse de doctorat, Université de Paris VII (1987)
Herbelin, H.: A ł-calculus structure isomorphic to sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, Springer, Heidelberg (1995)
Hardin, T., Lévy, J.-J.: A confluent calculus of substitutions. In: France-Japan Artificial Intelligence and Computer Science Symposium (1989)
Hardin, T., Maranget, L., Pagano, B.: Functional back-ends within the lambda-sigma calculus. In: ICFP (1996)
Huet, G.: Résolution d’équations dans les langages d’ordre 1,2, ..., ω. Thèse de doctorat d’état, Université Paris VII (1976)
Khasidashvili, Z.: Expression reduction systems. In: Proceedings of IN Vekua Institute of Applied Mathematics, Tbilisi, vol. 36 (1990)
Kesner, D.: Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions. In: Ganzinger, H. (ed.) Rewriting Techniques and Applications. LNCS, vol. 1103, Springer, Heidelberg (1996)
Kesner, D.: The theory of calculi with explicit substitutions revisited (2006), Available as http://hal.archives-ouvertes.fr/hal-00111285/
Kesner, D., Lengrand, S.: Extending the explicit substitution paradigm. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, Springer, Heidelberg (2005)
Klop, J.-W.: Combinatory Reduction Systems. PhD thesis, Mathematical Centre Tracts 127, CWI, Amsterdam (1980)
Khasidashvili, Z., Ogawa, M., van Oostrom, V.: Uniform Normalization Beyond Orthogonality. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, Springer, Heidelberg (2001)
Kamareddine, F.: A λ-calculus à la de Bruijn with explicit substitutions. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol. 982, Springer, Heidelberg (1995)
Lengrand, S., Dyckhoff, R., McKinna, J.: A sequent calculus for type theory. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, Springer, Heidelberg (2006)
Lengrand, S.: Normalisation and Equivalence in Proof Theory and Type Theory. PhD thesis, University Paris 7 and University of St Andrews (2006)
Lescanne, P.: From λ σ to λ υ , a journey through calculi of explicit substitutions. In: POPL (1994)
Lins, R.: A new formula for the execution of categorical combinators. In: Siekmann, J.H. (ed.) 8th International Conference on Automated Deduction. LNCS, vol. 230, Springer, Heidelberg (1986)
Lins, R.: Partial categorical multi-combinators and Church Rosser theorems. Technical Report 7/92, Computing Laboratory, University of Kent at Canterbury (1992)
Lévy, J.-J., Maranget, L.: Explicit substitutions and programming languages. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 1738, Springer, Heidelberg (1999)
Lescanne, P., Rouyer-Degli, J.: Explicit substitutions with de Bruijn levels. In: Hsiang, J. (ed.) Rewriting Techniques and Applications. LNCS, vol. 914, Springer, Heidelberg (1995)
Melliès, P.-A.: Typed λ-calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, Springer, Heidelberg (1995)
Muñoz, C.: Un calcul de substitutions pour la représentation de preuves partielles en théorie de types. PhD thesis, Université Paris 7 (1997)
Nederpelt, R.: Strong Normalization in a Typed Lambda Calculus with Lambda Structured Types. PhD thesis, Eindhoven University of Technology (1973)
Polonovski, E.: Substitutions explicites, logique et normalisation. Thèse de doctorat, Université Paris 7 (2004)
Rose, K.: Explicit cyclic substitutions. In: Rusinowitch, M., Remy, J.-L. (eds.) Conditional Term Rewriting Systems. LNCS, vol. 656, Springer, Heidelberg (1993)
Sakurai, T.: Strong normalizability of calculus of explicit substitutions with composition. Available on http://www.math.s.chiba-u.ac.jp/~sakurai/papers.html
Sinot, F.-R., Fernández, M., Mackie, I.: Efficient reductions with director strings. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, Springer, Heidelberg (2003)
Terese.: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kesner, D. (2007). The Theory of Calculi with Explicit Substitutions Revisited. In: Duparc, J., Henzinger, T.A. (eds) Computer Science Logic. CSL 2007. Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74915-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-74915-8_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74914-1
Online ISBN: 978-3-540-74915-8
eBook Packages: Computer ScienceComputer Science (R0)