Affordable Access

Operational conservativity with binding terms

Authors
Publisher
Technische Universiteit Eindhoven
Publication Date
Disciplines
  • Linguistics
  • Mathematics

Abstract

Operational Conservativity with Binding Terms C.A. Middelburg∗ Computing Science Department, Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, the Netherlands Department of Philosophy, Utrecht University P.O. Box 80126, 3508 TC Utrecht, the Netherlands mailto:[email protected], http://www.win.tue.nl/~keesm Abstract In a previous paper the approach to structural operational semantics using tran- sition system specifications (TSSs) was extended to deal with variable binding operators. It was shown that in this setting a generalization of the transition rule format known as the panth format guarantees that bisimulation is a con- gruence for meaningful TSSs. In this paper, it is shown that certain syntactic criteria, originating from Fokkink and Verhoef, to determine whether a TSS is an operational conservative extension of another TSS are applicable in this set- ting as well. This result can for example be used to simplify proofs of axiomatic conservativity and completeness in cases where an existing process calculus is extended with new features. Keywords: structural operational semantics, transition system specifications, operational conservative extension, variable binding operators, binding terms, panth format, bisimulation, congruence 1994 CR Categories: D.3.1, F.1.1, F.3.2, F.4.1, I.2.3. 1 Introduction Transition system specifications (TSSs) are used in an approach to structural operational semantics (SOS) that considers transition systems where the states are the closed terms over a given signature. The notion of TSS was first in- troduced in [11]. The original TSSs define binary transition relations by means of transition rules with positive premises. The notion of TSS was generalized in [3], [9], [16] and [6] to TSSs that define unary and binary transition relations by means of transition rules with positive and negative premises. In [13], we generalized it further to cover variable binding operators. The new TSSs can amongst other things deal wi

There are no comments yet on this publication. Be the first to share your thoughts.

Statistics

Seen <100 times
0 Comments

More articles like this

An alternative formulation of operational conserva...

on The Journal of Logic and Algeb... Jan 01, 2003

MOLECULAR BINDING AND LOW S TERMS OF N AND C.

on Proceedings of the National Ac... Jun 15, 1929

A syntactical proof of the operational equivalence...

on Theoretical Computer Science Jan 01, 1997
More articles like this..