A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs

C.A. Grabmayer

doi:10.1016/j.entcs.2002.09.007

A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs

C.A. Grabmayer

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are complete with respect to the notion of "recursive type equality" on a restricted class of recursive types in μ-term notation. Here we show the existence of an immediate duality with a geometrical visualization between proofs in a variant of the coinductive axiom system due to Brandt and Henglein and "consistency-unfoldings" in a variant of a 'syntactic-matching' proof system for testing equations between recursive types due to Ariola and Klop. Finally we sketch an analogous result of a duality between a similar pair of proof systems for bisimulation equivalence on equational specifications of cyclic term graphs. © 2007 Elsevier B.V. All rights reserved.

Original language	English
Pages (from-to)	59-74
Journal	Electronic Notes in Theoretical Computer Science
Volume	72
DOIs	https://doi.org/10.1016/j.entcs.2002.09.007
Publication status	Published - 2002

Bibliographical note

DBLP:journals/entcs/Grabmayer07
Proceedings title: Proceedings of the First International Workshop on Term Graph Rewriting (TERMGRAPH 2002)
Publisher: Elsevier

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1016/j.entcs.2002.09.007

Persistent URL (handle)

Persistent link

Cite this

@article{28e0362d09694d8995a8e5b699947cc0,

title = "A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs",

abstract = "This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are complete with respect to the notion of {"}recursive type equality{"} on a restricted class of recursive types in μ-term notation. Here we show the existence of an immediate duality with a geometrical visualization between proofs in a variant of the coinductive axiom system due to Brandt and Henglein and {"}consistency-unfoldings{"} in a variant of a 'syntactic-matching' proof system for testing equations between recursive types due to Ariola and Klop. Finally we sketch an analogous result of a duality between a similar pair of proof systems for bisimulation equivalence on equational specifications of cyclic term graphs. {\textcopyright} 2007 Elsevier B.V. All rights reserved.",

author = "C.A. Grabmayer",

note = "DBLP:journals/entcs/Grabmayer07 Proceedings title: Proceedings of the First International Workshop on Term Graph Rewriting (TERMGRAPH 2002) Publisher: Elsevier",

year = "2002",

doi = "10.1016/j.entcs.2002.09.007",

language = "English",

volume = "72",

pages = "59--74",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs

AU - Grabmayer, C.A.

N1 - DBLP:journals/entcs/Grabmayer07 Proceedings title: Proceedings of the First International Workshop on Term Graph Rewriting (TERMGRAPH 2002) Publisher: Elsevier

PY - 2002

Y1 - 2002

N2 - This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are complete with respect to the notion of "recursive type equality" on a restricted class of recursive types in μ-term notation. Here we show the existence of an immediate duality with a geometrical visualization between proofs in a variant of the coinductive axiom system due to Brandt and Henglein and "consistency-unfoldings" in a variant of a 'syntactic-matching' proof system for testing equations between recursive types due to Ariola and Klop. Finally we sketch an analogous result of a duality between a similar pair of proof systems for bisimulation equivalence on equational specifications of cyclic term graphs. © 2007 Elsevier B.V. All rights reserved.

AB - This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are complete with respect to the notion of "recursive type equality" on a restricted class of recursive types in μ-term notation. Here we show the existence of an immediate duality with a geometrical visualization between proofs in a variant of the coinductive axiom system due to Brandt and Henglein and "consistency-unfoldings" in a variant of a 'syntactic-matching' proof system for testing equations between recursive types due to Ariola and Klop. Finally we sketch an analogous result of a duality between a similar pair of proof systems for bisimulation equivalence on equational specifications of cyclic term graphs. © 2007 Elsevier B.V. All rights reserved.

U2 - 10.1016/j.entcs.2002.09.007

DO - 10.1016/j.entcs.2002.09.007

M3 - Article

SN - 1571-0661

VL - 72

SP - 59

EP - 74

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs

Abstract

Bibliographical note

UN SDGs

Access to Document

Persistent URL (handle)

Fingerprint

Cite this