Infinitary term graph rewriting is simple, sound and complete

Patrick Bahr

doi:10.4230/LIPIcs.RTA.2012.69

Infinitary term graph rewriting is simple, sound and complete

Patrick Bahr

Department of Computer Science

6 Citations (Scopus)

1572 Downloads (Pure)

Abstract

Based on a simple metric and a simple partial order on term graphs, we develop two infinitary calculi of term graph rewriting. We show that, similarly to infinitary term rewriting, the partial order formalisation yields a conservative extension of the metric formalisation of the calculus. By showing that the resulting calculi simulate the corresponding well-established infinitary calculi of term rewriting in a sound and complete manner, we argue for the appropriateness of our approach to capture the notion of infinitary term graph rewriting.

Original language	English
Title of host publication	23rd International Conference on Rewriting Techniques and Applications (RTA'12)
Editors	Ashish Tiwari
Number of pages	16
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Publication date	2012
Pages	69-84
ISBN (Electronic)	978-3-939897-38-5
DOIs	https://doi.org/10.4230/LIPIcs.RTA.2012.69
Publication status	Published - 2012
Event	23rd International Conference on Rewriting Techniques and Applications - Nagoya, Japan Duration: 28 May 2012 → 2 Jun 2012 Conference number: 23

Conference

Conference	23rd International Conference on Rewriting Techniques and Applications
Number	23
Country/Territory	Japan
City	Nagoya
Period	28/05/2012 → 02/06/2012

Series	Leibniz International Proceedings in Informatics
Volume	15
ISSN	1868-8969

Keywords

Faculty of Science
term graphs
infinitary rewriting
simulation
normalising
strong convergence

Access to Document

10.4230/LIPIcs.RTA.2012.69Licence: CC BY-NC-ND

Bahr_2012_Infinitary_term_graphFinal published version, 453 KBLicence: CC BY-NC-ND

Cite this

Infinitary term graph rewriting is simple, sound and complete. / Bahr, Patrick.

23rd International Conference on Rewriting Techniques and Applications (RTA'12). ed. / Ashish Tiwari. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. p. 69-84 (Leibniz International Proceedings in Informatics, Vol. 15).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Bahr, P 2012, Infinitary term graph rewriting is simple, sound and complete. in A Tiwari (ed.), 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics, vol. 15, pp. 69-84, 23rd International Conference on Rewriting Techniques and Applications, Nagoya, Japan, 28/05/2012. https://doi.org/10.4230/LIPIcs.RTA.2012.69

@inproceedings{b1da3943daf8438b87bb5e1e4071eb4e,

title = "Infinitary term graph rewriting is simple, sound and complete",

abstract = "Based on a simple metric and a simple partial order on term graphs, we develop two infinitary calculi of term graph rewriting. We show that, similarly to infinitary term rewriting, the partial order formalisation yields a conservative extension of the metric formalisation of the calculus. By showing that the resulting calculi simulate the corresponding well-established infinitary calculi of term rewriting in a sound and complete manner, we argue for the appropriateness of our approach to capture the notion of infinitary term graph rewriting.",

keywords = "Faculty of Science, term graphs, infinitary rewriting, simulation, normalising, strong convergence",

author = "Patrick Bahr",

year = "2012",

doi = "10.4230/LIPIcs.RTA.2012.69",

language = "English",

series = "Leibniz International Proceedings in Informatics",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

pages = "69--84",

editor = "Ashish Tiwari",

booktitle = "23rd International Conference on Rewriting Techniques and Applications (RTA'12)",

note = "23rd International Conference on Rewriting Techniques and Applications, RTA'12 ; Conference date: 28-05-2012 Through 02-06-2012",

}

TY - GEN

T1 - Infinitary term graph rewriting is simple, sound and complete

AU - Bahr, Patrick

N1 - Conference code: 23

PY - 2012

Y1 - 2012

N2 - Based on a simple metric and a simple partial order on term graphs, we develop two infinitary calculi of term graph rewriting. We show that, similarly to infinitary term rewriting, the partial order formalisation yields a conservative extension of the metric formalisation of the calculus. By showing that the resulting calculi simulate the corresponding well-established infinitary calculi of term rewriting in a sound and complete manner, we argue for the appropriateness of our approach to capture the notion of infinitary term graph rewriting.

AB - Based on a simple metric and a simple partial order on term graphs, we develop two infinitary calculi of term graph rewriting. We show that, similarly to infinitary term rewriting, the partial order formalisation yields a conservative extension of the metric formalisation of the calculus. By showing that the resulting calculi simulate the corresponding well-established infinitary calculi of term rewriting in a sound and complete manner, we argue for the appropriateness of our approach to capture the notion of infinitary term graph rewriting.

KW - Faculty of Science

KW - term graphs

KW - infinitary rewriting

KW - simulation

KW - normalising

KW - strong convergence

U2 - 10.4230/LIPIcs.RTA.2012.69

DO - 10.4230/LIPIcs.RTA.2012.69

M3 - Article in proceedings

T3 - Leibniz International Proceedings in Informatics

SP - 69

EP - 84

BT - 23rd International Conference on Rewriting Techniques and Applications (RTA'12)

A2 - Tiwari, Ashish

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - 23rd International Conference on Rewriting Techniques and Applications

Y2 - 28 May 2012 through 2 June 2012

ER -

Infinitary term graph rewriting is simple, sound and complete

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this