Conditional Linearization
			
R.C. de Vrijer



Abstract 

A non-leftlinear term rewriting system lacking the Church-Rosser
property can sometimes be shown to satisfy the unique normal form property by
shifting attention to an associated conditional term rewriting system that is
leftlinear. We call this the method of conditional linearization. In the present
paper the method is described in a general setting and some applications are
discussed. In particular we present a simple proof of the unique normal form
property for Combinatory Logic extended with 'Parallel Conditional', that
is, with constants C, T and F (conditional, true, false) and extra reduction
rules CTxy -> x, CFxy -> y and Czxx -> x. A special feature of this application is
that it involves the use of negative conditions.

Contents

Introduction 
1.  Four non-leftlinar, non-confluent TRSs
2.  Conditional Term Rewriting Systems
3.  Application of CTRSs to prove uniqueness of normal forms
4.  The case of Combinatory Logic plus Parallel Conditional
5.  Chew¹s theorem
6.  Remarks and further questions
References