How to normalize the Jay
In this note we give an elementary proof of the strong normalization property of the J combinator by providing an explicit bound for the maximal length of the reduction paths of a term. This result shows clearly that in the theorem of Toyama, Klop and Barendregt on completeness of unions of left-linear term rewriting systems, disjointness is essential. (C) 2001 Elsevier Science B.V. All rights reserved.
strong normalization term rewriting systems combinatory logic