orthogonality (term rewriting)
   HOME

TheInfoList



OR:

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 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 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 (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