Citation
D. Probst et T. Studer, How to normalize the Jay, THEOR COMP, 254(1-2), 2001, pp. 677-681
Citations number
4
Categorie Soggetti
Computer Science & Engineering
Journal title
THEORETICAL COMPUTER SCIENCE
ISSN journal
03043975
→ ACNP
Volume
254
Issue
1-2
Year of publication
2001
Pages
677 - 681
Database
ISI
SICI code
0304-3975(20010306)254:1-2<677:HTNTJ>2.0.ZU;2-K
Abstract
In this note we give an elementary proof of the strong normalization proper
ty of the J combinator by providing an explicit bound for the maximal lengt
h of the reduction paths of a term. This result shows clearly that in the t
heorem of Toyama, Klop and Barendregt on completeness of unions of left-lin
ear term rewriting systems, disjointness is essential. (C) 2001 Elsevier Sc
ience B.V. All rights reserved.