Church-Rosser property

English

Etymology

Alonzo Church and J. Barkley Rosser proved in 1936 that lambda calculus has this property.

Noun

Church-Rosser property (plural Church-Rosser properties)

1. (logic, computer science) The property of a rewriting system for which $x{\stackrel {*}{\leftrightarrow }}y$ implies $x{\mathbin {\downarrow }}y$ for all objects $x$, $y$.