[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #88

Originator: Delia Kesner
Date: January 1998

Summary: Is there a calculus of explicit substitution that is confluent on open terms, simulates one-step beta-reduction and preserves beta-strong normalization?

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]. César Muñoz presented in [Mu n96] a calculus enjoying both properties (answering Problem #78), however, the calculus is not able to simulate one-step of beta-reduction: if a beta-reduces to b in the lambda-calculus then a does not necessarily reduce to b in the calculus of Muñoz. Is there a calculus of explicit substitution that is confluent on open terms, simulates one-step beta-reduction and preserves beta-strong normalization?

Comment sent by Jean Goubault-Larrecq

Date: Mon Nov 27 16:37:43 MET 2000

This problem was solved positively in [GL99]. The calculus SKInT, introduced in [GGL00], is confluent on open terms and simulates one-step beta-reduction (although in a slightly contorted way, see [GGL00]; the obvious translation only simulates a bit more that one-step call-by-value beta-reduction). The paper [GL99] characterizes strongly normalizing, weakly normalizing and solvable terms through intersection types, and preservation of strong normalization follows. SKInT is also standardizing, has a terminating subcalculus of substitutions Σ T, but is based on an infinite signature and finitely many rule schemes parameterized by integers. Can we lift the latter restriction?

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.
[GGL00]
Healfdene Goguen and Jean Goubault-Larrecq. Sequent combinators: A Hilbert system for the lambda calculus. Mathematical Structures in Computer Science, 10:1–79, 2000.
[GL99]
Jean Goubault-Larrecq. Conjunctive types and SKInT. In Proceedings of the TYPES’98 Workshop, Lecture Notes in Computer Science. Springer-Verlag, Bad Irsee, Germany, 1999.
[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]