A term consisting of a constructor C and subterms ti: C(t1, t2, ..., tn) defines a congruence operator C(s1, s2, ..., sn) This is an operator that first matches a term =C(t1, t2,...,tn)=, then applies =s1= to =t1=, =s2= to =t2=, ..., =sn= to =tn=. This is used e.g. in conjunction with the recursive traversal operator to define specific data structure traversals. For example, using the congruence strategy =FunCall(s1,s2)= is equivalent to applying R : FunCall(a,b) -> FunCall(newa,newb) where a => newa ; b => newb which is equivalent to {a, b, newa, newb : ?FunCall(a,b) ; where( a => newa ; b => newb ) ; !FunCall(newa,newb) } This equivalent specification uses [[MatchStrategy][match]] and [[build strategies]], and [[variable scopes]] indicated by ={}=. =FunCall(s1,s2)= is also equivalent to: R: FunCall(a,b) -> FunCall( a, b) This specification uses a rewriting rule and [[term projection]]. ----++ More exotic congruences Tuple congruences =(s1,s2,...,sn)= List congruences =[s1,s2,...,sn]= A special list congruence is [] which "visits" the empty list ----+++ Distributing congruences c^D(s1, s2, ..., sn) =c= is term constructor =^D= syntax to denote distributing congruence =s1, ..., sn= are strategies. The meaning is given by c^D(s1, ..., sn): (c(x1, ..., xn), env) -> c(y1, ..., yn) where (x1, env) => y1 ; (x2, env) => y2 ; ... ; (xn, env) => yn ----+++ Threading congruences c^T(s1, s2, ..., sn) =c= is term constructor =^T= is syntax to denote threading congruence The meaning is given by: c^T(s1, ..., sn): (c(x1, ..., xn), e-first) -> (c(y1, ..., yn), e-last)) where (x1, e-first) => (y1, e2) ; (x2, e2) => (y2, e3) ; ... ; (xn, en) => (yn, e-last) ----- CategoryGlossary