Skip to main content
main-content

Über dieses Buch

In the 1930s, mathematical logicians studied the notion of "effective comput­ ability" using such notions as recursive functions, A-calculus, and Turing machines. The 1940s saw the construction of the first electronic computers, and the next 20 years saw the evolution of higher-level programming languages in which programs could be written in a convenient fashion independent (thanks to compilers and interpreters) of the architecture of any specific machine. The development of such languages led in turn to the general analysis of questions of syntax, structuring strings of symbols which could count as legal programs, and semantics, determining the "meaning" of a program, for example, as the function it computes in transforming input data to output results. An important approach to semantics, pioneered by Floyd, Hoare, and Wirth, is called assertion semantics: given a specification of which assertions (preconditions) on input data should guarantee that the results satisfy desired assertions (postconditions) on output data, one seeks a logical proof that the program satisfies its specification. An alternative approach, pioneered by Scott and Strachey, is called denotational semantics: it offers algebraic techniques for characterizing the denotation of (i. e. , the function computed by) a program-the properties of the program can then be checked by direct comparison of the denotation with the specification. This book is an introduction to denotational semantics. More specifically, we introduce the reader to two approaches to denotational semantics: the order semantics of Scott and Strachey and our own partially additive semantics.

Inhaltsverzeichnis

Frontmatter

Denotational Semantics of Control

Frontmatter

Chapter 1. An Introduction to Denotational Semantics

Abstract
To specify a programming language we must specify its syntax and semantics. The syntax of a programming language specifies which strings of symbols constitute valid programs. A formal description of the syntax typically involves a precise specification of the alphabet of allowable symbols and a finite set of rules delineating how symbols may be grouped into expressions, instructions, and programs. Most compilers for programming languages are implemented with syntax checking whereby the first stage in compiling a program is to check its text to see if it is syntactically valid. In practice, syntax must be described at two levels, for a human user through programming manuals and as a syntax-checking algorithm within a compiler or interpreter.
Ernest G. Manes, Michael A. Arbib

Chapter 2. An Introduction to Category Theory

Abstract
Going beyond the partial functions and multifunctions already considered, one might invent other useful notions of the input/output function from X to Y. In addition to the need to considerX, Y as “data structures,” there are theoretical approaches to semantics in which all X, Y must carry further structure. Rather than embark on the misguided task of presenting an exhaustive list of present and future possibilities, we introducecategories as a framework for semantics which possess so little structure that most models of semantics can be represented this way. Surprisingly, what structure remains can be extensively developed and there is a great deal to say.
Ernest G. Manes, Michael A. Arbib

Chapter 3. Partially Additive Semantics

Abstract
In Section 1.5 we introduced guard functions and finite and infinite sums of partial functions and multifunctions and used these as tools to describe guarded commands and various conditional and repetitive constructs. All this was in Pfn or Mfn. The task of this chapter is to develop axioms on a general semantic category to make similar constructions possible in a wider context and to clarify the algebraic processes of manipulation and simplification as partly demonstrated by Example 1.5.31.
Ernest G. Manes, Michael A. Arbib

Chapter 4. Assertion Semantics

Abstract
In the introductory Section 4.1 we informally define partial correctness assertions and notions relating to weakest preconditions with the Pascal fragment of Section 1.2 in mind. Here, we state a number of well-known properties and proof rules whose truth is intuitively evident.
Ernest G. Manes, Michael A. Arbib

Semantics of Recursion

Frontmatter

Chapter 5. Recursive Specifications

Abstract
A recursive specification “defines a function in terms of itself.” Recursive definitions occur commonly in the mathematical literature including that prior to the computer age. Here, the art of separating out “improper” recursive definitions was regarded as but one of the many skills necessary to write correct mathematics. But modern computer languages allow recursive specification to be expressed directly. Since the implementation of a programming language must respond to any recursive program, no matter how ill- conceived, we must pay attention to the mathematical question of what an “arbitrary” recursive specification should mean.
Ernest G. Manes, Michael A. Arbib

Chapter 6. Order Semantics of Recursion

Abstract
The task of the next three chapters is to better understand the abstract principles underlying the ideas associated with recursive definitions of partial functions as presented in Chapter 5 and to thereby elevate the theory to a wide class of semantic categories.
Ernest G. Manes, Michael A. Arbib

Chapter 7. Canonical Fixed Points

Abstract
The previous chapter considered a number of situations in which an object of semantic interest arises as the least fixed point of a continuous map ψ:(D, ≤)→(D, ≤) of some domain (D, ≤). So far, the domain structure is but a technical device to distinguish the least fixpoint from the other fixed points.
Ernest G. Manes, Michael A. Arbib

Chapter 8. Partially Additive Semantics of Recursion

Abstract
In Section 5.2, we used partially additive semantics in Pfn to describe a number of examples of recursive specification as “power-series” maps
$$\psi \left( h \right) = {H_0} + {H_1}\left( h \right) + {H_2}\left( {h,h} \right) + \cdots $$
in which the Kleene semantics could alternatively be given by the pattern-of-calls expansion.
Ernest G. Manes, Michael A. Arbib

Chapter 9. Fixed Points in Metric Spaces

Abstract
A metric space is a set equipped with a function which assigns a numerical “distance” to each pair of points. These objects arise naturally in many areas of mathematics. In Section 9.1 we prove a classical result due (essentially) to S. Banach that under appropriate hypotheses, an endomorphism ψ of a nonempty metric space has a unique fixed point x—indeed x is the limit (in the sense of ever decreasing distance) of the sequence x 0,ψx 0,ψ 2 x 0,… with any starting x 0. To illustrate the scope of this theorem we devote each of the remaining sections to an application. Section 9.2 establishes that an initial-value problem of ordinary differential equations has a unique solution. Section 9.3 introduces a tree-syntax for recursive specification in which repeated execution produces an infinite (but nonrecursive) syntax tree. The independence of the resulting infinite tree from “calling strategy” follows from the uniqueness assertion in the Banach theorem. Finally, we show in Section 9.4 that the language defined by a context-free grammar often arises as the unique fixed point of the Banach theorem.
Ernest G. Manes, Michael A. Arbib

Data Types

Frontmatter

CHAPTER 10. Functors

Abstract
Modern programming languages employ a variety of data structures which are (at least) sets of “structured elements” equipped with functions that allow combining, manipulating, and querying of such elements. A very rich supply of data types may be built—either directly or recursively—from finite sets using finite products and coproducts. Thus, if A is a character alphabet, A x A x A is “length 3 character arrays.” If prf: A x A x AA is the ith projection, pr i (w) evaluates the ith coordinate of w, providing the semantics of what would be written as w[i] in many programming languages. A precise definition of length 3 character arrays should specify exactly which maps such as the pr i should belong to the structure. For a recursive example, define “natural number” by 0 is a natural number if n is a natural number n0 is a natural number which is captured by the recursive specification
$${\text{N:: = }}\left\{ 0 \right\} + {\text{N}} \times \left\{ 0 \right\},$$
where we represent each number n by a string of zeros of length n + 1. A central concern will be to provide precise semantics to such specifications.
Ernest G. Manes, Michael A. Arbib

Chapter 11. Recursive Specification of Data Types

Abstract
Just as posets generalize categories, the Kleene fixed point theorem of 6.2.13 generalizes to provide a “co-continuous” endofunctor ψ: CC with a least fixed point as the “colimit” of the “right chain”
Ernest G. Manes, Michael A. Arbib

Chapter 12. Parametric Specification

Abstract
In Section 2 we will define “lists of E” in terms of the least fixed point specification
$$E*:: = 1 + E \times E*$$
(i.e., “a list is the empty list (1 = }Λ}) or an element of E followed by a list). But the parenthetical explication just given works only in Set, whereas the specification works in any category in which polynomial functors have least fixed points. In this sense E is a “parameter” for the “lists-of-” specifier. The specific parameter E may itself arise from another data type specification and may live in a category of arbitrary complexity subject to the technical needs of semantics.
Ernest G. Manes, Michael A. Arbib

Chapter 13. Order Semantics of Data Types

Abstract
Work initiated by D. S. Scott and C. Strachey in the 1960s, and contributed to by many up to the present writing, yields a framework for program semantics in which every data type is a domain and every computed function is continuous. We provide a critique of these basic assumptions in Section 1, but then proceed to develop an introduction to this theory of ordered semantics in the remaining sections.
Ernest G. Manes, Michael A. Arbib

Chapter 14. Equational Specification

Abstract
A collection of sets X1, …, Xn together with various functions of the form X i 1 x ⋯ x X i k→X i k+1 constitutes a “many-sorted algebra.” Section 1 gives examples of data types which arise as many-sorted algebras. An “equational specification” for a data type posits a many-sorted algebraic structure subject to a finite set of equations. What is attractive about this idea is that equational specifications are easily formalized within programming languages and have been partially implemented in experimental languages such as CLEAR, ACT ONE, CLU, and others. This provides a tool to define data types useful in programming and additionally promises to make available a useful research aid for pure mathematicians who study equationally defined algebraic structures.
Ernest G. Manes, Michael A. Arbib

Backmatter

Weitere Informationen