Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples
We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property fails by an example of a weakly orthogonal TRS with two collapsing rule...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2014-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/752/pdf |
| _version_ | 1797268692353941504 |
|---|---|
| author | Joerg Endrullis Clemens Grabmayer Dimitri Hendriks Jan Willem Klop Vincent van Oostrom |
| author_facet | Joerg Endrullis Clemens Grabmayer Dimitri Hendriks Jan Willem Klop Vincent van Oostrom |
| author_sort | Joerg Endrullis |
| collection | DOAJ |
| description | We present some contributions to the theory of infinitary rewriting for
weakly orthogonal term rewrite systems, in which critical pairs may occur
provided they are trivial. We show that the infinitary unique normal form
property fails by an example of a weakly orthogonal TRS with two collapsing
rules. By translating this example, we show that this property also fails for
the infinitary lambda-beta-eta-calculus. As positive results we obtain the
following: Infinitary confluence, and hence the infinitary unique normal forms
property, holds for weakly orthogonal TRSs that do not contain collapsing
rules. To this end we refine the compression lemma. Furthermore, we establish
the triangle and diamond properties for infinitary multi-steps (complete
developments) in weakly orthogonal TRSs, by refining an earlier
cluster-analysis for the finite case. |
| first_indexed | 2024-04-25T01:36:31Z |
| format | Article |
| id | doaj.art-5736b44353244d7887eaa6c7f4d4b8e8 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:31Z |
| publishDate | 2014-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-5736b44353244d7887eaa6c7f4d4b8e82024-03-08T09:36:21ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742014-06-01Volume 10, Issue 210.2168/LMCS-10(2:7)2014752Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and CounterexamplesJoerg Endrullishttps://orcid.org/0000-0002-2554-8270Clemens GrabmayerDimitri HendriksJan Willem KlopVincent van Oostromhttps://orcid.org/0000-0002-4818-7383We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property fails by an example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that this property also fails for the infinitary lambda-beta-eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence the infinitary unique normal forms property, holds for weakly orthogonal TRSs that do not contain collapsing rules. To this end we refine the compression lemma. Furthermore, we establish the triangle and diamond properties for infinitary multi-steps (complete developments) in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the finite case.https://lmcs.episciences.org/752/pdfcomputer science - logic in computer science |
| spellingShingle | Joerg Endrullis Clemens Grabmayer Dimitri Hendriks Jan Willem Klop Vincent van Oostrom Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples Logical Methods in Computer Science computer science - logic in computer science |
| title | Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples |
| title_full | Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples |
| title_fullStr | Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples |
| title_full_unstemmed | Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples |
| title_short | Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples |
| title_sort | infinitary term rewriting for weakly orthogonal systems properties and counterexamples |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/752/pdf |
| work_keys_str_mv | AT joergendrullis infinitarytermrewritingforweaklyorthogonalsystemspropertiesandcounterexamples AT clemensgrabmayer infinitarytermrewritingforweaklyorthogonalsystemspropertiesandcounterexamples AT dimitrihendriks infinitarytermrewritingforweaklyorthogonalsystemspropertiesandcounterexamples AT janwillemklop infinitarytermrewritingforweaklyorthogonalsystemspropertiesandcounterexamples AT vincentvanoostrom infinitarytermrewritingforweaklyorthogonalsystemspropertiesandcounterexamples |