Bi-inductive structural semantics

Patrick Cousot, Radhia Cousot

Research output: Contribution to journalArticle

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 languageEnglish (US)
Pages (from-to)258-283
Number of pages26
JournalInformation and Computation
Volume207
Issue number2
DOIs
StatePublished - Feb 2009

Fingerprint

Inductive Definitions
Semantics
Structural Operational Semantics
Coinduction
Operational Semantics
Grammar
Calculus
Trace
Cover
Generalization
Abstraction

Keywords

  • Bi-inductive definition
  • Big-step semantics
  • Co-inductive definition
  • Divergence semantics
  • Fixpoint definition
  • Grammar
  • Inductive definition
  • Nonmonotone definition
  • Relational semantics
  • Small-step semantics
  • SOS
  • Structural operational semantics
  • Trace semantics

ASJC Scopus subject areas

  • Information Systems
  • Computational Theory and Mathematics
  • Theoretical Computer Science
  • Computer Science Applications

Cite this

Bi-inductive structural semantics. / Cousot, Patrick; Cousot, Radhia.

In: Information and Computation, Vol. 207, No. 2, 02.2009, p. 258-283.

Research output: Contribution to journalArticle

Cousot, Patrick ; Cousot, Radhia. / Bi-inductive structural semantics. In: Information and Computation. 2009 ; Vol. 207, No. 2. pp. 258-283.
@article{5cbe184afd0a435da3af51f173af438d,
title = "Bi-inductive structural semantics",
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).",
keywords = "Bi-inductive definition, Big-step semantics, Co-inductive definition, Divergence semantics, Fixpoint definition, Grammar, Inductive definition, Nonmonotone definition, Relational semantics, Small-step semantics, SOS, Structural operational semantics, Trace semantics",
author = "Patrick Cousot and Radhia Cousot",
year = "2009",
month = "2",
doi = "10.1016/j.ic.2008.03.025",
language = "English (US)",
volume = "207",
pages = "258--283",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier Inc.",
number = "2",

}

TY - JOUR

T1 - Bi-inductive structural semantics

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 2009/2

Y1 - 2009/2

N2 - 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).

AB - 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).

KW - Bi-inductive definition

KW - Big-step semantics

KW - Co-inductive definition

KW - Divergence semantics

KW - Fixpoint definition

KW - Grammar

KW - Inductive definition

KW - Nonmonotone definition

KW - Relational semantics

KW - Small-step semantics

KW - SOS

KW - Structural operational semantics

KW - Trace semantics

UR - http://www.scopus.com/inward/record.url?scp=70350273404&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70350273404&partnerID=8YFLogxK

U2 - 10.1016/j.ic.2008.03.025

DO - 10.1016/j.ic.2008.03.025

M3 - Article

VL - 207

SP - 258

EP - 283

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 2

ER -