Andrew Polonsky

A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (Extended Version)

2015 · arXiv (Cornell University)

We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. We define the relation =^infty, notion of infinitary equational reasoning, and ->^infty, the standard notion of infinitary …