Abstract
We propose a simple order-theoretic generalization, possibly nonmonotone, of settheoretic 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 λ-calculus (for which co-induction is shown to be inadequate).
| Original language | English (US) |
|---|---|
| Pages (from-to) | 258-283 |
| Number of pages | 26 |
| Journal | Information and Computation |
| Volume | 207 |
| Issue number | 2 |
| DOIs | |
| State | Published - Feb 2009 |
Keywords
- Bi-inductive definition
- Big-step semantics
- Co-inductive definition
- Divergence semantics
- Fixpoint definition
- Grammar
- Inductive definition
- Nonmonotone definition
- Relational semantics
- SOS
- Small-step semantics
- Structural operational semantics
- Trace semantics
ASJC Scopus subject areas
- Theoretical Computer Science
- Information Systems
- Computer Science Applications
- Computational Theory and Mathematics