[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #78 (Solved !)

Originator: Pierre Lescanne
Date: April 1995

Summary: Is there a calculus of explicit substitution that is both confluent and preserves termination?

There are confluent calculi of explicit substitutions, but these do not preserve termination (strong normalization) [CHL92, Mel95], and there are calculi that are not confluent on open terms, but which do preserve termination [LRD94]. Is there a calculus of explicit substitution that is both confluent and preserves termination?

Remark

The calculus presented in [Mu n96] enjoys both properties. This has led to Problem #88.

References

[CHL92]

Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. RR 1617, Institut National de Rechereche en Informatique et en Automatique, Rocquencourt, France, February 1992.

[LRD94]

Pierre Lescanne and J. Rouyer-Degli. The calculus of explicit substitutions λυ. Technical Report RR-2222, INRIA-Lorraine, January 1994.

[Mel95]

Paul-André Melliès. Typed λ-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, 1995.

[Mu n96]

César Mu noz. Confluence and preservation of strong normalisation in an explicit substitutions calculus (extended abstract). In Edmund C. Clarke, editor, Eleventh Symposium on Logic in Computer Science, pages 440–447, New Brunswick, NJ, July 1996. IEEE.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]