Confluence, and its use for conversion checking

Published: March 11, 2020, 8 p.m.

b'

The basic property of confluence of a nondeterministic reduction semantics: if from starting term t you can reach t1 and also t2 (by two finite reduction sequences), then there is some t3 to which t1 and t2 both reduce in a finite number of steps.\\xa0 The use of confluence for ensuring completeness of the conversion-checking algorithm that tests conversion of t1 and t2 by normalizing both terms and checking for alpha-equivalence (or maybe alpha,eta-equivalence).

'