Unique Normal Forms for Combinatory Logic with Parallel Conditional, a Case Study in Conditional Rewriting

摘要

The note presents a simple proof of the unicity of normal forms property for Combinatory Logic extended with 'Parallel Conditional,' that is, with constants C, T and F (conditional, true, false) and extra reduction rules CTxy to x, CFxy to y and Czxx to x. The proof makes use of a method involving conditional term rewriting systems that has more general application. This method is described and some other applications are discussed.