Page

Web

Wiki

# 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
```

(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
```

```   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