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 <s1> a => newa
          ; <s2> b => newb

(this equivalent specification uses a rewriting rule (see later))

which is equivalent to

  {a, b, newa, newb :
   ?FunCall(a,b)
   ; where(    
       <s1> a => newa
       ; <s2> b => newb
     )
   ; !FunCall(newa,newb)
  }

(this equivalent specification uses match and build strategies^?, and variable scopes^? indicated by {}) or shorter using term projection^?

  R: FunCall(a,b) -> FunCall(<s1> a, <s2> b)

(this equivalent specification uses a rewriting rule and term projection^?.

More exotic congruences

Also exist:

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 <s1> (x1,env) => y1;
            <s2> (x2,env) => y2;
            ...
            <sn> (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 <s1> (x1, e-first) => (y1,e2);
            <s2> (x2, e2) => (y2,e3);
            ...
            <sn> (xn, en) => (yn,e-last);

---

CategoryGlossary