Is there a difference between the ‘compatible closure of a binary relation’ (Felleisen and Hieb, 1992): > The one-step v-reduction —>v is the compatible closure of v: e —>v e’ if (p, q) ∊ v, e ≡ C[p] and e’ ≡ C[q] for some expressions p and q and context C. and the ‘monotonicity w.r.t. the term structure’ (Bachmair et al., 1989, “Completion without failure”): > A binary relation —> is monotonic with respect to the term structure if s —> t implies u[s] —> u[t] for all terms u, s, t. where > we write t[s] to indicate that the term t contains s as a subterm and (ambiguously) denote by t[u] the result of replacing a particular occurrence of s by u.

I’m trying to trace back the two definitions (if they are equivalent), I could find another mention of ‘compatible’ by Huet, 1981 (“Confluent rewriting systems”). Did Bachmair et al invent a new name for something that was already known, then?

I don’t know for sure, but those certainly look the same.

thanks