Bi-inductive structural semantics
We propose a simple order-theoretic generalization, possibly nommonotone, of set-theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows structural operational semantics to describe simultaneously the finite/terminating and infinite/diverging behaviors of programs. This is illustrated on grammars and the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value X-calculus (for which co-induction is shown to be inadequate). (c) 2008 Elsevier Inc. All rights reserved.
inductive definition bi-inductive definition structural operational semantics grammar fixpoint definition co-inductive definition nonmonotone definition sos trace semantics relational semantics small-step semantics big-step semantics divergence semantics