[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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?
The calculus presented in [Mu n96] enjoys both properties. This has led to Problem #88.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |