Book contents
- Frontmatter
- Contents
- Preface to the Second Edition
- Preface to the First Edition
- Part I Judgments and Rules
- Part II Statics and Dynamics
- 4 Statics
- 5 Dynamics
- 6 Type Safety
- 7 Evaluation Dynamics
- Part III Total Functions
- Part IV Finite Data Types
- Part V Types and Propositions
- Part VI Infinite Data Types
- Part VII Variable Types
- Part VIII Partiality and Recursive Types
- Part IX Dynamic Types
- Part X Subtyping
- Part XI Dynamic Dispatch
- Part XII Control Flow
- Part XIII Symbolic Data
- Part XIV Mutable State
- Part XV Parallelism
- Part XVI Concurrency and Distribution
- Part XVII Modularity
- Part XVIII Equational Reasoning
- Part XIX Appendices
- References
- Index
5 - Dynamics
from Part II - Statics and Dynamics
Published online by Cambridge University Press: 05 March 2016
- Frontmatter
- Contents
- Preface to the Second Edition
- Preface to the First Edition
- Part I Judgments and Rules
- Part II Statics and Dynamics
- 4 Statics
- 5 Dynamics
- 6 Type Safety
- 7 Evaluation Dynamics
- Part III Total Functions
- Part IV Finite Data Types
- Part V Types and Propositions
- Part VI Infinite Data Types
- Part VII Variable Types
- Part VIII Partiality and Recursive Types
- Part IX Dynamic Types
- Part X Subtyping
- Part XI Dynamic Dispatch
- Part XII Control Flow
- Part XIII Symbolic Data
- Part XIV Mutable State
- Part XV Parallelism
- Part XVI Concurrency and Distribution
- Part XVII Modularity
- Part XVIII Equational Reasoning
- Part XIX Appendices
- References
- Index
Summary
The dynamics of a language describes how programs are executed. The most important way to define the dynamics of a language is by the method of structural dynamics, which defines a transition system that inductively specifies the step–by–step process of executing a program. Another method for presenting dynamics, called contextual dynamics, is a variation of structural dynamics in which the transition rules are specified in a slightly different way. An equational dynamics presents the dynamics of a language by a collection of rules defining when one program is definitionally equivalent to another.
Transition Systems
A transition system is specified by the following four forms of judgment:
s state, asserting that s is a state of the transition system.
s final, where s state, asserting that s is a final state.
s initial, where s state, asserting that s is an initial state.
s ⟼ s', where s state and s' state, asserting that state s may transition to state s'.
In practice, we always arrange things so that no transition is possible from a final state: if s final, then there is no s' state such that s ⟼ s'. A state from which no transition is possible is stuck.Whereas all final states are, by convention, stuck, theremay be stuck states in a transition system that are not final. A transition system is deterministic iff for every state s there exists at most one state s' such that s ⟼ s'; otherwise, it is non-deterministic.
A transition sequence is a sequence of states s0, …, sn such that s0 initial, and si ⟼ si+1 for every 0 ≤ i < n. A transition sequence is maximal iff there is no s such that sn ⟼ s, and it is complete iff it is maximal and sn final. Thus, every complete transition sequence is maximal, but maximal sequences are not necessarily complete. The judgment s ↓ means that there is a complete transition sequence starting from s, which is to say that there exists s' final such that s ⟼*s'.
- Type
- Chapter
- Information
- Practical Foundations for Programming Languages , pp. 39 - 47Publisher: Cambridge University PressPrint publication year: 2016