Abstract
Inspired by a recent graphical formalism for λ-calculus based on Linear Logic technology, we introduce an untyped structural λ-calculus, called λj, which combines action at a distance with exponential rules decomposing the substitution by means of weakening, contraction and dereliction. Firstly, we prove fundamental properties such as confluence and preservation of β-strong normalisation. Secondly, we use λj to describe known notions of developments and superdevelopments, and introduce a more general one called XL-development. Then we show how to reformulate Regnier’s σ-equivalence in λj so that it becomes a strong bisimulation. Finally, we prove that explicit composition or de-composition of substitutions can be added to λj while still preserving β-strong normalisation.
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
Accattoli, B., Guerrini, S.: Jumping boxes. representing lambda-calculus boxes by jumps. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 55–70. Springer, Heidelberg (2009)
Accattoli, B., Kesner, D.: The structural calculus λj. Technical report, PPS, CNRS and University Paris-Diderot (2010)
Ó Conchúir, S.: Proving PSN by simulating non-local substitutions with local substitution. In: Proceedings of the 3rd HOR, August 2006, pp. 37–42 (2006)
Danos, V., Regnier, L.: Reversible, irreversible and optimal lambda-machines. TCS 227(1), 79–97 (1999)
David, R., Guillaume, B.: A λ-calculus with explicit weakening and explicit substitution. MSCS 11, 169–206 (2001)
de Bruijn, N.G.: Generalizing Automath by Means of a Lambda-Typed Lambda Calculus. In: Mathematical Logic and Theoretical Computer Science. Lecture Notes in Pure and Applied Mathematics, vol. 106, pp. 71–92. Marcel Dekker, New York (1987)
de Moor, O., Sittampalam, G.: Higher-order matching for program transformation. TCS 269(1-2), 135–162 (2001)
Di Cosmo, R., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. MSCS 13(3), 409–450 (2003)
Faure, G.: Matching modulo superdevelopments application to second-order matching. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 60–74. Springer, Heidelberg (2006)
Girard, J.-Y.: Linear logic. TCS 50 (1987)
Girard, J.-Y.: Geometry of interaction i: an interpretation of system f. In: Proc. of the Logic Colloquim, vol. 88, pp. 221–260 (1989)
Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical lambda-calculus in ”natural deduction” form. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 142–156. Springer, Heidelberg (2009)
Hindley, J.R.: Reductions of residuals are finite. Transactions of the American Mathematical Society 240, 345–361 (1978)
Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 238–252. Springer, Heidelberg (2007)
Kesner, D.: A theory of explicit substitutions with safe and full composition. LMCS 5(3:1), 1–29 (2009)
Kesner, D., Lengrand, S.: Resource operators for lambda-calculus. I & C 205(4), 419–473 (2007)
Kesner, D., Renaud, F.: The prismoid of resources. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 464–476. Springer, Heidelberg (2009)
Klop, J.-W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. TCS 121(1/2), 279–308 (1993)
Lévy, J.-J.: Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Univ. Paris VII, France (1978)
Lévy, J.-J., Maranget, L.: Explicit substitutions and programming languages. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 181–200. Springer, Heidelberg (1999)
Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. TCS 228(1-2), 175–210 (1999)
Milner, R.: Local bigraphs and confluence: two conjectures. In: Proc. of 13th EXPRESS. ENTCS, vol. 175. Elsevier, Amsterdam (2006)
Nederpelt, R.P.: The fine-structure of lambda calculus. Technical Report CSN 92/07, Eindhoven Univ. of Technology (1992)
Ohta, Y., Hasegawa, M.: A terminating and confluent linear lambda calculus. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 166–180. Springer, Heidelberg (2006)
Regnier, L.: Lambda-calcul et réseaux. Thèse de doctorat, Univ. Paris VII (1992)
Regnier, L.: Une équivalence sur les lambda-termes. TCS 2(126), 281–292 (1994)
Schwichtenberg, H.: Termination of permutative conversions in intuitionistic Gentzen calculi. TCS 212(1-2), 247–260 (1999)
Severi, P., Poll, E.: Pure type systems with definitions. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol. 813, pp. 316–328. Springer, Heidelberg (1994)
van Raamsdonk, F.: Confluence and Normalization for Higher-Order Rewriting. PhD thesis, Amsterdam Univ., Netherlands (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Accattoli, B., Kesner, D. (2010). The Structural λ-Calculus. In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-15205-4_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15204-7
Online ISBN: 978-3-642-15205-4
eBook Packages: Computer ScienceComputer Science (R0)