Orthogonality as a property of

term rewriting system In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or red ...

s (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 * ...

between them, i.e. the TRS has no critical pairs. For example

D(x,x) \to E

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

\begin
\rho_1:\ & f(x,y) & \rightarrow & g(y) \\
\rho_2:\ & h(y) & \rightarrow & f(g(y), y)
\end

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.

Weak orthogonality

A TRS is weakly orthogonal if it is left-linear and contains only trivial critical pairs, i.e. if

(t,s)

is a critical pair then

t=s

. 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