2015
A Coinductive Treatment of Infinitary Term Rewriting and Equational Reasoning (Extended Version).
Publication
Publication
rewriting in a uniform way. We define the relation 1=, a notion of infinitary equational reasoning,
and !1, the standard notion of infinitary rewriting as follows:
1= := R. (=R [ 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 | |
---|---|
Cornell University Library | |
arXiv.org e-Print archive | |
Organisation | Computer Security |
Endrullis, J., Hansen, H., Hendriks, D., Polonsky, A., & Silva, A. (2015). A Coinductive Treatment of Infinitary Term Rewriting and Equational Reasoning (Extended Version).. arXiv.org e-Print archive. Cornell University Library . |