SOS Preliminary Version

Niveau: Supérieur
SOS 2007 Preliminary Version Bi-inductive Structural Semantics (Extended Abstract) Patrick Cousot 1 Département d'informatique, École normale supérieure, 45 rue d'Ulm, 75230 Paris cedex 05, France Radhia Cousot 2 CNRS & École polytechnique, 91128 Palaiseau cedex, France Abstract We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This general- ization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structural operational semantics to describe simultaneously the finite/terminating and infi- nite/diverging behaviors of programs. This is illustrated on the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value ?-calculus. Keywords: fixpoint definition, inductive definition, co-inductive definition, bi-inductive definition, structural operational semantics, SOS, trace semantics, relational semantics, small-step semantics, big-step semantics, divergence semantics, abstraction. 1 Introduction The connection between the use of fixpoints in denotational semantics [17] and the use of rule-based inductive definitions in axiomatic semantics [10] and structural operational semantics (SOS) [19,20,21] can be made by a generalization of inductive definitions [1] to include co-inductive definitions [8].

• inductive structural


• order-theoretic inductive


• finite behaviors


• big-step trace


• join can


• behaviors while avoiding


• evaluate e2


• e1 either


• semantics


• fixpoint definition