Congruence Operator

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

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 {}.

FunCall(s1,s2) is also equivalent to:

R:
  FunCall(a,b) -> FunCall(<s1> a, <s2> 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
    <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