|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'503'724
Articles rated: 2609
23 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (Extended Version) | | Jörg Endrullis
; Helle Hvid Hansen
; Dimitri Hendriks
; Andrew Polonsky
; Alexandra Silva
; | | Date: |
5 May 2015 | | Abstract: | 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(s_1,...,s_n), f(t_1,...,t_n)) | s_1 R t_1,...,s_n R t_n } +
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. | | Source: | arXiv, 1505.1128 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER