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

Clemens Grabmayer | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

Author(s) -

Clemens Grabmayer

Publication year - 2007

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2002.09.007

Subject(s) - bisimulation , mathematics , equivalence (formal languages) , term (time) , duality (order theory) , type (biology) , discrete mathematics , algebra over a field , pure mathematics , physics , quantum mechanics , ecology , biology

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research