Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-18T04:39:36.407Z Has data issue: false hasContentIssue false
  • English
  • Français

The conservation theorem for differential nets

Published online by Cambridge University Press:  29 October 2015

MICHELE PAGANI  and
PAOLO TRANQUILLI
MICHELE PAGANI
Affiliation:
PPS, Université Paris Diderot, Sorbonne Paris Cité (UMR 7126 CNRS F-75205, Paris, France)
PAOLO TRANQUILLI
Affiliation:
LIP, ENS Lyon, Université de Lyon (UMR 5668 CNRS ENS Lyon UCBL INRIA, France)
Get access Rights & Permissions [Opens in a new window]

Abstract

We prove the conservation theorem for differential nets – the graph-theoretical syntax of the differential extension of Linear Logic (Ehrhard and Regnier's DiLL). The conservation theorem states that the property of having infinite reductions (here infinite chains of cut elimination steps) is preserved by non-erasing steps. This turns the quest for strong normalisation (SN) into one for non-erasing weak normalisation (WN), and indeed we use this result to prove SN of simply typed DiLL (with promotion). Along the way to the theorem we achieve a number of additional results having their own interest, such as a standardisation theorem and a slightly modified system of nets, DiLL∂ϱ.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 27 , Issue 6 , September 2017 , pp. 939 - 992
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Barendregt, H. (1981). The Lambda Calculus, Its Syntax and Semantics. Number 103 in Studies in Logic and the Foundations of Mathematics, 1st edition, North-Holland.Google Scholar
Bonelli, E.A. (2001). Substitutions explicites et réécriture de termes. Thèse de doctorat, Université Paris XI.Google Scholar
Danos, V. (1990). La Logique Linéaire appliquée à l'étude de divers processus de normalisation (principalement du λ-calcul). Thèse de doctorat, Université Paris VII.Google Scholar
Danos, V. and Regnier, L. (1989). The structure of multiplicatives. Archive for Mathematical Logic 28 (3) 181–203.CrossRefGoogle Scholar
de Falco, M. (2009). An explicit framework for interaction nets. In: Treinen, R. (ed.) RTA. Springer Lecture Notes in Computer Science 5595 209–223.CrossRefGoogle Scholar
Di Cosmo, R. and Guerrini, S. (1999). Strong normalization of proof nets modulo structural congruences. In: Narendran, P. and Rusinowitch, M. (eds.) Proceedings Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2–4. Springer Lecture Notes in Computer Science 1631 75–89.CrossRefGoogle Scholar
Di Cosmo, R. and Kesner, D. (1997). Strong normalization of explicit substitutions via cut elimination in proof nets (extended abstract). In: Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29–July 2, 1997, IEEE Computer Society 35–46.Google Scholar
Di Cosmo, R., Kesner, D. and Polonovski, E. (2003). Proof nets and explicit substitutions. Mathematical Structures in Computer Science 13 (3) 409–450.CrossRefGoogle Scholar
Ehrhard, T. (2005). Finiteness spaces. Mathematical Structures in Computer Science 15 (4) 615–646.Google Scholar
Ehrhard, T. and Laurent, O. (2007). Interpreting a finitary pi-calculus in differential interaction nets. In: CONCUR 2007 - Concurrency Theory, Proceedings of the 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3–8, 2007, Springer Lecture Notes in Computer Science 4703 333–348.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science 309 (1) 1–41.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2006). Differential interaction nets. Theoretical Computer Science 364 (2) 166–195.Google Scholar
Fiore, M.P. (2007). Differential structure in models of multiplicative biadditive intuitionistic linear logic. In: Ronchi Della Rocca, S. (eds.) TLCA. Springer Lecture Notes in Computer Science 4583 163–177.CrossRefGoogle Scholar
Gandy, R.O. (1980). Proofs of strong normalization. In: Seldin, J.P. and Hindley, J.R. (eds.)To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press Limited 457–477.Google Scholar
Gimenez, S. (2011). Realizability proof for normalization of full differential linear logic. In: Luke Ong, C.-H. (eds.) Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1–3. Springer Lecture Notes in Computer Science 6690 107–122.CrossRefGoogle Scholar
Girard, J.-Y. (1972). Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique d'Ordre Supérieur. Thèse de doctorat d'etat, Université Paris VII.Google Scholar
Girard, J.-Y. (1987a). Linear Logic. Theoretical Computer Science 50 1–102.Google Scholar
Girard, J.-Y. (1987b). Proof Theory and Logical Complexity. Studies in Proof-theory. Bibliopolis, Napoli.Google Scholar
Girard, J.-Y., Lafont, Y. and Taylor, P. (1989). Proofs and Types, Cambridge Tracts in Theoretical Computer Science volume 7, Cambridge University Press.Google Scholar
Hindley, J.R. (1964). The Church-Rosser Property and a Result in Combinatory Logic, Ph.D. thesis, University of Newcastle-upon-Tyne.Google Scholar
Huet, G.P. (1980). Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM 27 (4) 797–821.Google Scholar
Lafont, Y. (1990). Interaction nets. In: POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA. ACM 95–108.Google Scholar
Nederpelt, R.P. (1973). Strong Normalization for a Typed Lambda Calculus with Lambda Structured Types, Ph.D. thesis, Technische Hogeschool Eindhoven.Google Scholar
Pagani, M. (2009). The cut-elimination theorem for differential nets with promotion. In: Curien, P.-L. (eds.) TLCA. Springer Lecture Notes in Computer Science 5608 219–233.Google Scholar
Pagani, M. and Tortora de Falco, L. (2010). Strong normalization property for second order linear logic. Theoretical Computer Science 411 (2) 410–444.Google Scholar
Sørensen, M.H. (1997). Strong normalization from weak normalization in typed λ-calculi. Information and Computation 133 (1) 35–71.Google Scholar
Tait, W.W. (1967). Intensional interpretation of functionals of finite type. Journal of Symbolic Logic 32 (2) 187–199.Google Scholar
Terese. (2003). Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science volume 55, Cambridge University Press.Google Scholar
Tortora de Falco, L. (2003). Additives of linear logic and normalization- part I: a (restricted) Church-Rosser property. Theoretical Computer Science 294 (3) 489–524.Google Scholar
Tranquilli, P. (2009a). Confluence of pure differential nets with promotion. In: Grädel, E. and Kahle, R. (eds.) CSL. Springer Lecture Notes in Computer Science 5771 500–514.Google Scholar
Tranquilli, P. (2009b). Nets Between Determinism and Nondeterminism Ph.D. thesis, Università Roma Tre/Université Paris Diderot (Paris 7).Google Scholar
Tranquilli, P. (2011). Intuitionistic differential nets and lambda-calculus. Theoretical Computer Science 412 (20) 1979–1997.Google Scholar
Vaux, L. (2007). λ-calcul différentiel et logique classique : interactions calculatoires. Thèse de doctorat, Université de la Méditerranée.Google Scholar