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

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