Abstract

We consider an intersection type assignment system for term rewriting systems extended with application, and define a notion of (finite) approximation on terms. We then prove that for typeable rewrite systems satisfying a general scheme for recursive definitions, every typeable term has an approximant of the same type. This approximation result, and the proof technique developed to obtain it, allow us to deduce in a direct way a head-normalization, a normalization, and a strong normalization theorem, for different classes of typeable terms.

Appeared as:

@Inproceedings {Bakel-Fernandez-HOA'95,

Author = "S. van Bakel and M. Fern\'andez",
Title = "{A}pproximation and {N}ormalization {R}esults for {T}ypeable {T}erm {R}ewriting {S}ystems",
Booktitle = "Proceedings of HOA '95. Second {I}nternational {W}orkshop on {H}igher {O}rder {A}lgebra, {L}ogic and {T}erm {R}ewriting, {\rm {P}aderborn, {G}ermany}. {S}elected {P}apers",
Editor = "Gilles Dowek and Jan Heering and Karl Meinke and Bernhard M{\"o}ller",
Series = "Lecture Notes in Computer Science",
Volume = "1074",
Publisher = "Springer-Verlag",
Year = "1996",
Pages = "17-36"
}