| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Jean-Pierre Jouannaud
Date: April 1995
Summary: Extend combination results on rewrite orderings to systems involving βη reductions.
A collection of rewrite orderings operating on disjoint signatures can be extended to an ordering operating on the union of the signatures, while still preserving part of the properties [Rub94]. Such constructions can be used for proving modular termination properties of rewrite systems. Do they extend to the case where one of the starting orderings is given by βη reductions on typed lambda terms?
| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |