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

Revision: r1.3 - 28 Apr 2005 - 22:24 - Main.wiki
Stratego > StrategoGlossary > CongruenceOperator
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