2015/05/05 by Jörg Endrullis, Endrullis, Jörg, Helle Hvid Hansen +7
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.1505.01128
arXiv admin note: substantial text overlap with arXiv:1306.6224
arxiv created 2015/05/05 · openalex publication_date 2015/05/05 · arxiv updated 2015/05/06 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
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 rewriting as follows: =infty := nu R. ( <-root + ->root + lift(R) )^* ->infty := mu R. nu S. ( ->root + lift(R) )^* ; lift(S) where lift(R) := (f(s1,...,sn), f(t1,...,tn)) | s1 R t1,...,sn R tn + id , and where mu is the least fixed point operator and nu is the greatest fixed point operator. 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.