# Publications on Coinduction

## 2018

- Coinductive Foundations of Infinitary Rewriting and Infinitary Equational LogicJörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra SilvaLogical Methods in Computer Science , 14 (1) (2018)
# Abstract

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 framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{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 suitable for formalizations in theorem provers. To wit, we provide the first formalization of the compression lemma in Coq.

This paper is an extended version of

*A Coinductive Framework for Infinitary Rewriting and Equational Reasoning*(RTA 2015). We build on ideas in*Infinitary Rewriting Coinductively*(TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).@article{infintary:rewriting:coinductive:2018, author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra}, title = {{Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic}}, journal = {Logical Methods in Computer Science}, volume = {14}, number = {1}, year = {2018}, doi = {10.23638/LMCS-14(1:3)2018}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {journal} }

## 2015

- A Coinductive Framework for Infinitary Rewriting and Equational ReasoningJörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra SilvaIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), pp. 143–159, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)
# Abstract

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 framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{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 suitable for formalizations in theorem provers.

We refer to

*Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic*(LMCS 2018) for an extended journal version of this paper.We build on ideas in

*Infinitary Rewriting Coinductively*(TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).@inproceedings{infintary:rewriting:coinductive:2015, author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra}, title = {{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA 2015)}, volume = {36}, pages = {143--159}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2015}, doi = {10.4230/LIPIcs.RTA.2015.143}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {conference} }

## 2013

- Circular Coinduction in Coq Using Bisimulation-Up-To TechniquesJörg Endrullis, Dimitri Hendriks, and Martin BodinIn: Proc. Conf. on Interactive Theorem Proving (ITP 2013), pp. 354–369, Springer (2013)
@inproceedings{circular:coinduction:2013, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Bodin, Martin}, title = {{Circular Coinduction in Coq Using Bisimulation-Up-To Techniques}}, booktitle = {Proc.\ Conf.\ on Interactive Theorem Proving (ITP~2013)}, volume = {7998}, pages = {354--369}, publisher = {Springer}, series = {LNCS}, year = {2013}, doi = {10.1007/978-3-642-39634-2\_26}, keywords = {rewriting, coinduction, formal verification}, type = {conference} }

## 2011

- Infinitary Rewriting CoinductivelyJörg Endrullis, and Andrew PolonskyIn: Proc. Conf. on Types for Proofs and Programs (TYPES 2012), pp. 16–27, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)
# Abstract

We provide a coinductive definition of strongly convergent reductions between infinite lambda terms. This approach avoids the notions of ordinals and metric convergence which have appeared in the earlier definitions of the concept. As an illustration, we prove the existence part of the infinitary standardization theorem. The proof is fully formalized in Coq using coinductive types.

The paper concludes with a characterization of infinite lambda terms which reduce to themselves in a single beta step.

The papers

*A Coinductive Framework for Infinitary Rewriting and Equational Reasoning*(RTA 2015)*Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic*(LMCS 2018)

The extension to reduction lengths beyond omega requires mixing of induction and coinduction. Therefore the simpler setup presented in the current paper (

*Infinitary Rewriting Coinductively*) is preferrable whenever there is no need for reductions longer than omega. This concerns for instance rewrite systems having the compression property, such as lambda calculus and left-linear term rewriting systems (with finite left-hand sides).@inproceedings{infintary:lambda:coinductive:2011, author = {Endrullis, J\"{o}rg and Polonsky, Andrew}, title = {{Infinitary Rewriting Coinductively}}, booktitle = {Proc.\ Conf.\ on Types for Proofs and Programs (TYPES~2012)}, volume = {19}, pages = {16--27}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2011}, doi = {10.4230/LIPIcs.TYPES.2011.16}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {conference} }