# Congruence Operator

Stratego -- Strategies for Program Transformation

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