A coinductive framework for infinitary rewriting and equational reasoning

Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, A. Polonsky, Alexandra Silva

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. We define the relation ∞=, a notion of infinitary equational reasoning, and →∞, the standard notion of infinitary rewriting as follows: ∞=:= νR. (=R ≊ R)→∞ := μR. νS.(→R ≊ R)o S where μ and ν are the least and greatest fixed-point operators, respectively, and where R := {f(s1, . . . , sn), f(t1, . . . , tn) f∈∑ s1 R t1, . . . , snR tn } ≊ Id . The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

Original languageEnglish
Title of host publication26th International Conference on Rewriting Techniques and Applications, RTA 2015
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages143-159
Number of pages17
Volume36
ISBN (Electronic)9783939897859
DOIs
Publication statusPublished - 1 Jun 2015
Event26th International Conference on Rewriting Techniques and Applications, RTA 2015 - Warsaw, Poland
Duration: 29 Jun 20151 Jul 2015

Conference

Conference26th International Conference on Rewriting Techniques and Applications, RTA 2015
CountryPoland
CityWarsaw
Period29/06/151/07/15

Keywords

  • Coinduction
  • Infinitary rewriting

Cite this

Endrullis, J., Hansen, H. H., Hendriks, D., Polonsky, A., & Silva, A. (2015). A coinductive framework for infinitary rewriting and equational reasoning. In 26th International Conference on Rewriting Techniques and Applications, RTA 2015 (Vol. 36, pp. 143-159). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.RTA.2015.143