Affordable Access

Operational conservativity with binding terms

Technische Universiteit Eindhoven
Publication Date
  • Linguistics
  • Mathematics


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], 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.