Compact normalisation trace via lazy rewriting

DOI10.1016/S1571-0661(04)00269-5MaRDI QIDQ2841224zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Quang-Huy Nguyen

Publication date 24 July 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)00269-5

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Recommendations

• Normalization by leftmost innermost rewriting
• Optimal normalization in orthogonal term rewriting systems
• Normalization properties for shallow TRS and innermost rewriting
• Proving innermost normalisation automatically
• Lazy rewriting and context-sensitive rewriting

Cites work

• A refinement of strong sequentiality for term rewriting with constructors
• scientific article; zbMATH DE number 1231658 (Why is no real title available?)
• scientific article; zbMATH DE number 1332639 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS
• The evaluation strategy for head normal form with and without on-demand flags

Cited in

(8)

• Context-sensitive rewriting strategies
• Non-linear rewrite closure and weak normalization
• Lazy rewriting and context-sensitive rewriting
• Outermost ground termination
• Termination of lazy rewriting revisited
• Trace rewriting: Computing normal forms in time O(n log n)
• Normalization by leftmost innermost rewriting
• Normalization properties for shallow TRS and innermost rewriting

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Compact normalisation trace via lazy rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2841224)