Confluence of a binary relation → on a set is defined as the existence of two derivations v →* s and w →*v s reaching some s for any two divergent derivations u →*v and u →*w issuing from the same u. In case → describes some non-deterministic intentional computation, confluence expresses that the associated extensional relation is functional. Confluence is therefore an essential, but undecidable property of Turing-complete languages.
In this talk we shall describe a general method which captures both Hindley's method targeting non-terminating relations, as well as Newman's method targeting terminating relations, and elaborate some of its practical consequences if time permits.