Print Email Facebook Twitter Coinductive foundations of infinitary rewriting and infinitary equational logic Title Coinductive foundations of infinitary rewriting and infinitary equational logic Author Endrullis, Jörg (Vrije Universiteit Amsterdam) Hansen, H.H. (TU Delft Energy and Industry) Hendriks, Dimitri (Vrije Universiteit Amsterdam) Polonsky, Andrew (Universite Paris Diderot) Silva, Alexandra (University College London) Date 2018 Abstract We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform way. We define Equation found, the infinitary extension of a given equational theory =R, and →∞, the standard notion of infinitary rewriting associated to a reduction relation →R, as follows: (Formula Presented) Equation found Here μ and ν are the least and greatest fixed-point operators, respectively, and (Formula Presented) Equation found 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. Subject CoinductionInfinitary equational reasoningInfinitary rewriting To reference this document use: http://resolver.tudelft.nl/uuid:e2b88d01-096a-4de1-81f9-5e135256e528 DOI https://doi.org/10.23638/LMCS-14(1:3)2018 ISSN 1860-5974 Source Logical Methods in Computer Science, 14 (1) Part of collection Institutional Repository Document type journal article Rights © 2018 Jörg Endrullis, H.H. Hansen, Dimitri Hendriks, Andrew Polonsky, Alexandra Silva Files PDF 1706.00677.pdf 778.96 KB Close viewer /islandora/object/uuid:e2b88d01-096a-4de1-81f9-5e135256e528/datastream/OBJ/view