2018

  1. Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
    Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva
    Logical Methods in Computer Science , 14 (1) (2018)
    paper

    Summary

    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).

    Bibtex

    @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}
}

    Digital Object Identifier

    10.23638/LMCS-14(1:3)2018

2015

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

    Summary

    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).

    Bibtex

    @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}
}

    Digital Object Identifier

    10.4230/LIPIcs.RTA.2015.143

2013

  1. Circular Coinduction in Coq Using Bisimulation-Up-To Techniques
    Jörg Endrullis, Dimitri Hendriks, and Martin Bodin
    In: Proc. Conf. on Interactive Theorem Proving (ITP 2013), pp. 354–369, Springer (2013)
    paper

    Bibtex

    @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}
}

    Digital Object Identifier

    10.1007/978-3-642-39634-2_26

2011

  1. Infinitary Rewriting Coinductively
    Jörg Endrullis, and Andrew Polonsky
    In: Proc. Conf. on Types for Proofs and Programs (TYPES 2012), pp. 16–27, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)
    paper

    Summary

    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

    extend the idea in this paper to reductions of length beyond omega.

    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).

    Bibtex

    @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}
}

    Digital Object Identifier

    10.4230/LIPIcs.TYPES.2011.16