Search

• < Previous
• 1
• Next >

Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence.&nbsp;[&hellip;]