Document Open Access Logo

Metaconfluence of Calculi with Explicit Substitutions at a Distance

Authors Flávio L. C. de Moura, Delia Kesner, Mauricio Ayala-Rincón

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.391.pdf
  • Filesize: 461 kB
  • 12 pages

Document Identifiers

Author Details

Flávio L. C. de Moura
Delia Kesner
Mauricio Ayala-Rincón

Cite As Get BibTex

Flávio L. C. de Moura, Delia Kesner, and Mauricio Ayala-Rincón. Metaconfluence of Calculi with Explicit Substitutions at a Distance. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 391-402, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.FSTTCS.2014.391

Abstract

Confluence is a key property of rewriting calculi that guarantees uniqueness of normal-forms when they exist. Metaconfluence is even more general, and guarantees confluence on open/meta terms, i.e. terms with holes, called metavariables that can be filled up with other (open/meta) terms. The difficulty to deal with open terms comes from the fact that the structure of metaterms is only partially known, so that some reduction rules became blocked by the metavariables. In this work, we establish metaconfluence for a family of calculi with explicit substitutions (ES) that enjoy preservation of strong-normalization (PSN) and that act at a distance. For that, we first extend the notion of reduction on metaterms in such a way that explicit substitutions are never structurally moved, i.e. they also act at a distance on metaterms.  The resulting reduction relations are still rewriting systems, i.e. they do not include equational axioms, thus providing for the first time an interesting family of lambda-calculi with explicit substitutions that enjoy both PSN and metaconfluence without requiring sophisticated notions of reduction modulo a set of equations.

Subject Classification

Keywords
  • Confluence
  • Explicit Substitutions
  • Lambda Calculi

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit Substitutions. Journal of Functional Programming, 1(4):375-416, 1991. Google Scholar
  2. B. Accattoli, P. Barenbaum, and D. Mazza. Distilling abstract machines. Available at https://sites.google.com/site/beniaminoaccattoli/, 2014. Google Scholar
  3. B. Accattoli, E. Bonelli, D. Kesner, and C. Lombardi. A nonstandard standardization theorem. In 41st Symposium on Principles of Programming Languages (POPL), editor, ACM SIGPLAN-SIGACT, pages 659-670, 2014. Google Scholar
  4. B. Accattoli and D. Kesner. The structural lambda-calculus. In 19th EACSL Annual Conference on Computer Science and Logic (CSL), volume 6247 of LNCS, pages 381-395. Springer-Verlag, 2010. Google Scholar
  5. B. Accattoli and D. Kesner. The permutative lambda calculus. In LPAR, pages 23-36, 2012. Google Scholar
  6. B. Accattoli and D. Kesner. Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  7. B. Accattoli and U. Dal Lago. Beta reduction is invariant, indeed. Accepted to LICS/CSL 2014. Google Scholar
  8. M. Ayala-Rincón and F. Kamareddine. Unification via the λ s \_e-Style of Explicit Substitution. The Logical Journal of the IGPL, 9(4):489-523, 2001. Google Scholar
  9. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  10. H. Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. Google Scholar
  11. M. Bezem, J. W. Klop, and R. de Vrijer, editors. Term Rewriting Seminar - Terese. Cambridge University Press, 2003. Google Scholar
  12. P.-L. Curien, T. Hardin, and J.-J. Levy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43:43-2, 1996. Google Scholar
  13. R. David and B. Guillaume. A lambda-calculus with explicit weakening and explicit substitution. Mathematical Structures in Computer Science, 11(1):169-206, 2001. Google Scholar
  14. F. L. C. de Moura, M. Ayala-Rincón, and F. Kamareddine. Higher-Order Unification: A structural relation between Huet’s method and the one based on explicit substitutions. Journal of Applied Logic, 6(1):72-108, 2008. Google Scholar
  15. G. Dowek, T. Hardin, and C. Kirchner. Higher order unification via explicit substitutions. Inf. Comput., 157(1-2):183-235, 2000. Google Scholar
  16. G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In JICSLP, pages 259-273, 1996. Google Scholar
  17. Z. el A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λυ, a Calculus of Explicit Substitutions which Preserves Strong Normalization. JFP, 6(5):699-722, 1996. Google Scholar
  18. B. Guillaume. The λ s \_e-calculus Does Not Preserve Strong Normalization. J. of Func. Programming, 10(4):321-325, 2000. Google Scholar
  19. F. Kamareddine and A. Ríos. A λ-calculus à la de Bruijn with Explicit Substitutions. In Proc. of PLILP'95, volume 982 of LNCS, pages 45-62. Springer, 1995. Google Scholar
  20. F. Kamareddine and A. Ríos. Extending a λ-calculus with Explicit Substitution which Preserves Strong Normalisation into a Confluent Calculus on Open Terms. Journal of Functional Programming, 7:395-420, 1997. Google Scholar
  21. D. Kesner. The theory of calculi with explicit substitutions revisited. In CSL, pages 238-252, 2007. Google Scholar
  22. D. Kesner. Perpetuality for full and safe composition (in a constructive setting). In To appear in Proceedings of the 35th International Colloquium on Automata, Languages and Programming (ICALP 2008), Track B, Reykjavik, Iceland,, 2008. Google Scholar
  23. D. Kesner. A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science, 5(3:1):1-29, 2009. Google Scholar
  24. D. Kesner and S. Ó Conchúir. Milner’s Lambda Calculus with Partial Substitutions. Technical Report, Université Paris Diderot, 2008. Google Scholar
  25. P.-A. Melliès. Typed λ-calculi with explicit substitutions may not terminate. In Proceedings of TLCA'95, volume 902 of LNCS. Springer-Verlag, 1995. Google Scholar
  26. R. Milner. Local bigraphs and confluence: Two conjectures: (extended abstract). ENTCS, 175(3):65-73, 2007. Google Scholar
  27. F. Renaud. Les Ressources Explicites vues par la Théorie de la Réécriture. PhD thesis, Université Paris Diderot - Paris 7, 2011. Available at www.lix.polytechnique.fr/∼renaud/these.pdf. Google Scholar
  28. Jean yves Girard. Proof-nets: The parallel syntax for proof-theory. In Logic and Algebra, pages 97-124. Marcel Dekker, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact