[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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?
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?
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |