A term consisting of a constructor C and subterms ti:
^{?}, and variable scopes^{?} indicated by ^{?}.
## More exotic congruences

### Distributing congruences

### Threading congruences

CategoryGlossary

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 => newbwhich 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

`{}`

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

Tuple congruences `(s1,s2,...,sn)`

List congruences `[s1,s2,...,sn]`

A special list congruence is [] which "visits" the empty list

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

Revision: r1.3 - 28 Apr 2005 - 22:24 - Main.wiki

Copyright © 1999-2020 by the contributing authors.
All material on this collaboration platform is the property of the contributing authors.

Ideas, requests, problems regarding TWiki? Send feedback

Ideas, requests, problems regarding TWiki? Send feedback