Computing Publications

Publications Home » Normalization Results for Typeabl...

Normalization Results for Typeable Rewrite Systems

Steffen van Bakel, Maribel

Journal Article
Information and Computation
Volume 133
Issue 2
March, 1997
DOI 10.1006/inco.1996.2617

In this paper we introduce Curryfied Term Rewriting Systems, and a notion of partial type assignment on terms and rewrite rules that uses intersection types with sorts and omega. Three operations on types – substitution, expansion, and lifting – are used to define type assignment, and are proved to be sound. With this result the system is proved closed for reduction. Using a more liberal approach to recursion, we define a general scheme for recursive definitions and prove that, for all systems that satisfy this scheme, every term typeable without using the type-constant omega is strongly normalizable. We also show that, under certain restrictions, all typeable terms have a (weak) head-normal form, and that terms whose type does not contain omega are normalizable.

PDF of full publication (297 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.