Advertisement
Published in:
2014 | OriginalPaper | Chapter
Proof Terms for Infinitary Rewriting
Authors : Carlos Lombardi, Alejandro Ríos, Roel de Vrijer
Published in: Rewriting and Typed Lambda Calculi
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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. Transfinite reductions can be faithfully represented as infinitary proof terms, unique up to infinitary associativity. We use proof terms to define equivalence of transfinite reductions on the basis of permutation equations. A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.