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
a => newa
; b => newb
which is equivalent to
{a, b, newa, newb :
?FunCall(a,b)
; where(
a => newa
; b => newb
)
; !FunCall(newa,newb)
}
This equivalent specification uses [[MatchStrategy][match]] and [[build strategies]], and [[variable scopes]] indicated by ={}=.
=FunCall(s1,s2)= is also equivalent to:
R:
FunCall(a,b) -> FunCall( a, 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
(x1, env) => y1
; (x2, env) => y2
; ...
; (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
(x1, e-first) => (y1, e2)
; (x2, e2) => (y2, e3)
; ...
; (xn, en) => (yn, e-last)
-----
CategoryGlossary