Orthogonality as a property of
term rewriting systems (TRSs) describes where the reduction rules of the system are all left-linear, that is each variable occurs only once on the left hand side of each reduction rule, and there is no
overlap
Overlap may refer to:
* In set theory, an overlap of elements shared between sets is called an intersection, as in a Venn diagram.
* In music theory, overlap is a synonym for reinterpretation of a chord at the boundary of two musical phrases
* O ...
between them, i.e. the TRS has no
critical pairs. For example
is not left-linear.
Orthogonal TRSs have the consequent property that all reducible expressions (redexes) within a term are completely disjoint -- that is, the redexes share no common function symbol.
For example, the TRS with reduction rules
is orthogonal -- it is easy to observe that each reduction rule is left-linear, and the left hand side of each reduction rule shares no function symbol in common, so there is no overlap.
Orthogonal TRSs are
confluent
In geography, a confluence (also: ''conflux'') occurs where two or more flowing bodies of water join to form a single channel. A confluence can occur in several configurations: at the point where a tributary joins a larger river (main stem); o ...
.
Weak orthogonality
A TRS is weakly orthogonal if it is left-linear and contains only trivial critical pairs, i.e. if
is a critical pair then
.
[ Weakly orthogonal TRSs are confluent.
A TRS is almost orthogonal if it is weakly orthogonal and has the additional property that overlap between redex occurrences occurs only at the root of the redex occurrences.]
References
{{plt-stub
Rewriting systems