2015
A Coinductive Treatment of Infinitary Term Rewriting and Equational Reasoning
Publication
Publication
Presented at the
International Conference on Rewriting Techniques and Applications, Warsaw, Poland
We present a coinductive framework for defining infinitary analogues of equational reasoning and
rewriting in a uniform way. We define the relation 1=, a hitherto unknown notion of infinitary
equational reasoning, and !1, the standard notion of infinitary rewriting as follows:
1= := R. (=E [ R)
!1 := μR. S. (!R [ R) S
where μ and are the least and greatest fixed-point operators, respectively, and where
R := { hf(s1, . . . , sn), f(t1, . . . , tn)i | f 2 , s1 R t1, . . . , sn R 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.
| Additional Metadata | |
|---|---|
| Schloss Dagstuhl - Leibniz Center of Informatics | |
| doi.org/10.4230 | |
| Leibniz International Proceedings in Informatics (LIPIcs) | |
| International Conference on Rewriting Techniques and Applications | |
| Organisation | Computer Security |
|
Endrullis, J., Hansen, H., Hendriks, D., Polonsky, A., & Silva, A. (2015). A Coinductive Treatment of Infinitary Term Rewriting and Equational Reasoning. In Proceedings of International Conference on Rewriting Techniques and Applications 2015 (RTA) (pp. 143–159). Schloss Dagstuhl - Leibniz Center of Informatics. doi:10.4230 |
|
