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.

Authors

• Dieter Probst
• Thomas Studer

Keywords

• Term rewriting systems
• Combinatory logic
• Strong normalization