Proof Terms for Infinitary Rewriting

DOI10.1007/978-3-319-08918-8_21MaRDI QIDQ5170824zbMATH OpenOpenAlexFDO

Authors Carlos Lombardi, A. Ríos, Roel de Vrijer

Publication date 24 July 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1402.2245

zbMATH Keywords

infinitary rewritingpermutation equivalenceproof terms

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Abstract: We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be faithfully represented as an infinitary proof term, which is unique up to, infinitary, associativity. Our main use of proof terms is in a definition of permutation equivalence for transfinite reductions, on the basis of permutation equations. This definition involves a variant of equational logic, adapted for dealing with infinite objects. A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.

Recommendations

• Infinite terms and infinite rewritings
• Infinitary rewriting: foundations revisited
• scientific article; zbMATH DE number 6678680
• Projections for infinitary rewriting
• Rewriting, inference, and proof
• Publication:3490953
• scientific article; zbMATH DE number 408817
• Term rewriting induction
• Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting
• Projections for infinitary rewriting (extended version)

Cited in

(11)

• Projections for infinitary rewriting
• Transfinite reductions in orthogonal term rewriting systems
• Composing proof terms
• Projections for infinitary rewriting (extended version)
• Declarative representation of proof terms
• scientific article; zbMATH DE number 6678680 (Why is no real title available?)
• Coinductive foundations of infinitary rewriting and infinitary equational logic
• scientific article; zbMATH DE number 952103 (Why is no real title available?)
• ProTeM: a proof term manipulator (system description)
• Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting
• Partial Order Infinitary Term Rewriting

This page was built for publication: Proof Terms for Infinitary Rewriting

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