Misplaced Pages

Orthogonality (term rewriting)

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Property of term rewriting systems

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 between them, i.e. the TRS has no critical pairs. For example D ( x , x ) → E {\displaystyle 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 ρ 1 :   f ( x , y ) → g ( y ) ρ 2 :   h ( y ) → f ( g ( y ) , y ) {\displaystyle {\begin{array}{lrcl}\rho _{1}:\ &f(x,y)&\rightarrow &g(y)\\\rho _{2}:\ &h(y)&\rightarrow &f(g(y),y)\end{array}}} 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 ) {\displaystyle (t,s)} is a critical pair then t = s {\displaystyle 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

  1. ^ Klop, J. W. "Term Rewriting Systems" (PDF). Papers by Nachum Dershowitz and students. Tel Aviv University. p. 69. Retrieved 14 August 2021.
  2. Terese (20 March 2003). Term Rewriting Systems. Cambridge University Press. p. 140. ISBN 978-0-521-39115-3.
  3. Raamsdonk, Femke van (2 April 1997). "Outermost-Fair Rewriting". Proceedings of the Third International Conference on Typed Lambda Calculi and Applications. Springer-Verlag: 284–299. CiteSeerX 10.1.1.36.8258.
Stub icon

This computer science article is a stub. You can help Misplaced Pages by expanding it.

Γ ⊢ {\displaystyle \Gamma \!\vdash }

This programming language theory or type theory-related article is a stub. You can help Misplaced Pages by expanding it.

Categories: