A confluent reduction system, also called globally confluent, is one in which for all 
, 
,
and 
such that 
and 
, there exists a 
such that 
and 
. A reduction system
is said to be locally confluent if, for all 
, 
,
and 
such that 
and 
, there exists a 
such that 
and 
. Here, the notation 
indicates that 
is reduced to 
in one step, and 
indicates that 
is reduced to 
in zero or more steps.
A reduction system is confluent iff it has the Church-Rosser property (Wolfram 2002, p. 1036). In finitely terminating reduction systems, global and local confluence are equivalent, for instance in the systems shown above. Reduction systems that are both finitely terminating and confluent are called convergent. In a convergent reduction system, unique normal forms exist for all expressions.
The problem of determining whether a given reduction system is confluent is recursively undecidable.
The property of being confluent is called confluence. Confluence compares the states reached by different reduction paths, while causal invariance compares their causal graphs. In general, neither condition implies the other with the graph isomorphism definition of causal invariance (Piskunov 2020).
