Chapter 10: Domain Theory and Fixed-Point Semantics
10.1 Concepts and Examples
- Recursive Definitions of Functions
- Recursive Definitions of Sets (Types)
- Modeling Nontermination
- Exercises
- Recursive Definitions of Sets (Types)
10.2 Domain Theory
- Elementary Domains
- Product Domains
- Sum Domains (Disjoint Unions)
- Function Domains
- Continuity of Functions on Domains
- Exercises
- Product Domains
10.3 Fixed-Point Semantics
- First Step
- Second Step
- Continuous Functionals
- Fixed points for Nonrecursive Functions
- Revisiting Denotational Semantics
- Fixed-Point Induction
- Exercises
- Second Step
10.4 Laboratory: Recursion in the Lambda Calculus
- Conditional Expressions
- Paradoxical Combinator
- Fixed-Point Identity
- Exercises
- Paradoxical Combinator
10.5 Further Reading
Chapter 11: Axiomatic Semantics
11.1 Concepts and Examples
- Axiomatic Semantics of Programming Languages
11.2 Axiomatic Sematnics for Wren
- Assignment Command
- Input and Output
- Rules of Inference
- While Command and Loop Invariants
- More on Loop Invariants
- Nested While Loops
- Exercises
- Input and Output
11.3 Axiomatic Semantics for Pelican
- Blocks
- Nonrecursive Procedures
- Recursive Procedures
- Exercises
- Nonrecursive Procedures
11.4 Proving Termination
- Steps in Showing Termination
- Termination of Recursive Procedures
- Exercises
- Termination of Recursive Procedures
11.5 Introduction to Program Derivation
- Table of Cubes
- Binary Search
- Exercises
- Binary Search
11.6 Further Reading
Chapter 12: Algebraic Semantics
12.1 Concepts and Examples
- A Module for Truth Values
- Module Syntax
- A Module for Natural Numbers
- A Module for Characters
- A Parameterized Module and Some Instantiations
- A Module for Finite Mappings
- Exercises
- Module Syntax
12.2 Mathematical Foundations
- Ground Terms
- Sigma-Algebras
- A Congruence from the Equations
- The Quotient Algebra
- Homomorphisms
- Consistency and Completeness
- Exercises
- Sigma-Algebras
12.3 Using Algebraic Specifications
- Data Abstraction
- A Module for Unbounded Queues
- Implementing Queues as Unbounded Arrays
- Verification of Queue Axioms
- ADTs As Algebras
- Abstract Syntax and Algebraic Specifications
- Exercises
- A Module for Unbounded Queues
12.4 Algebraic Semantics for Wren
- Types and Values in Wren
- Abstract Syntax for Wren
- A Type Checker for Wren
- An Interpreter for Wren
- A Wren System
- Exercises
- Abstract Syntax for Wren
12.5 Laboratory: Implementing Algebraic Semantics
- Module Booleans
- Module Naturals
- Declarations
- Commands
- Expressions
- Exercises
- Module Naturals
12.6 Further Reading
13.1 Concepts and Examples
- Data and Sorts
- Yielders
- Actions
- The Functional Facet
- The Imperative Facet
- Exercises
- Yielders
13.2 Action Semantics of a Calculator
- Semantic Functions
- Semantic Equations
- A Sample Calculation
- Exercises
- Semantic Equations
13.3 The Declarative Facet and Wren
- The Programming Language Wren
- Exercises
13.4 The Reflective Facet and Pelican
- The Reflective Facet and Procedures
- Procedures Without Parameters
- Procedures With A Parameter
- Recursive Definitions
- Translating to Action Notation
- Exercises
- Procedures Without Parameters
13.5 Laboratory: Translating into Action Notation
- Exercises
13.6 Further Reading
Appendix A: Logic Programming with Prolog
- Prolog
- Prolog Syntax
- BNF Syntax for Prolog
- A Prolog Example
- Predefined Predicates
- Recursion in Prolog
- Control Aspects of Prolog
- Lists in Prolog
- Sorting in Prolog
- The Logical Variable
- Equality and Comparison in Prolog
- Input and Output Predicates
- Prolog Syntax
Appendix B: Functional Programming with Scheme
- Lisp
- Scheme Syntax
- Functions on S-expressions
- Lists in Scheme
- Syntax for Functions
- Scheme Evaluation
- Special Forms
- Defining Functions in Scheme
- Recursive DeŽnitions
- Lambda Notation
- Recursive Functions on Lists
- Scope Rules in Scheme
- Proving Correctness in Scheme
- Higher-Order Functions
- Currying
- Tail Recursion
- Scheme Syntax
Bibliography
Index
To Ken Slonneger's
Home Page