A term consisting of a constructor C and subterms ti:
<verbatim>
C(t1, t2, ..., tn)
</verbatim>
defines a congruence operator
<verbatim>
C(s1, s2, ..., sn)
</verbatim>

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
<verbatim>
R :
  FunCall(a,b) -> FunCall(newa,newb) 
  where
	 <s1> a => newa
  ; <s2> b => newb
</verbatim>
which is equivalent to
<verbatim>
{a, b, newa, newb :
  ?FunCall(a,b)
  ; where(	 
		<s1> a => newa
	 ; <s2> b => newb
	 )
  ; !FunCall(newa,newb)
}
</verbatim>
This equivalent specification uses [[MatchStrategy][match]] and [[build strategies]], and [[variable scopes]] indicated by ={}=.

=FunCall(s1,s2)= is also equivalent to:
<verbatim>
R:
  FunCall(a,b) -> FunCall(<s1> a, <s2> b)
</verbatim>
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

<verbatim>
c^D(s1, s2, ..., sn)
</verbatim>
=c= is term constructor
=^D= syntax to denote distributing congruence
=s1, ..., sn= are strategies. 

The meaning is given by
<verbatim>
c^D(s1, ..., sn):
  (c(x1, ..., xn), env) -> c(y1, ..., yn)
  where
	 <s1> (x1, env) => y1
  ; <s2> (x2, env) => y2
  ; ...
  ; <sn> (xn, env) => yn
</verbatim>

----+++ Threading congruences

<verbatim>
c^T(s1, s2, ..., sn)
</verbatim>
=c= is term constructor
=^T= is syntax to denote threading congruence

The meaning is given by:
<verbatim>
c^T(s1, ..., sn):
  (c(x1, ..., xn), e-first) -> (c(y1, ..., yn), e-last))
  where
	 <s1> (x1, e-first) => (y1, e2)
  ; <s2> (x2, e2) => (y2, e3)
  ; ...
  ; <sn> (xn, en) => (yn, e-last)
</verbatim>				

-----
CategoryGlossary