Denotational Semantics: A Methodology for Language Development

By David Schmidt

Denotational semantics is a methodology for giving mathematical meaning to programming languages and systems. It was developed by Christopher Strachey’s Programming Research Group at Oxford University in the 1960s. The method combines mathematical rigor, due to the work of Dana Scott, with notational elegance, due to Strachey. Originally used as an analysis tool, denotational semantics has grown in use as a tool for language design and implementation. This book was written to make denotational semantics accessible to a wider audience and to update existing texts in the area. I have presented the topic from an engineering viewpoint, emphasizing the descriptional and implementational aspects. The relevant mathematics is also included, for it gives rigor and validity to the method and provides a foundation for further research.

The book is intended as a tutorial for computing professionals and as a text for university courses at the upper undergraduate or beginning graduate level. The reader should be acquainted with discrete structures and one or more general purpose programming languages. Experience with an applicative-style language such as LISP, ML, or Scheme is also helpful.

The Introduction and Chapters 1 through 7 form the core of the book. The Introduction provides motivation and a brief survey of semantics specification methods. Chapter 1 introduces BNF, abstract syntax, and structural induction. Chapter 2 lists those concepts of set theory that are relevant to semantic domain theory. Chapter 3 covers semantic domains, the value sets used in denotational semantics. The fundamental domains and their related operations are presented. Chapter 4 introduces basic denotational semantics. Chapter 5 covers the semantics of computer storage and assignment as found in conventional imperative languages. Nontraditional methods of store evaluation are also considered. Chapter 6 presents least fixed point semantics, which is used for determining the meaning of iterative and recursive definitions. The related semantic domain theory is expanded to include complete partial orderings; ‘‘predomains’’ (complete partial orderings less ‘‘bottom’’ elements) are used. Chapter 7 covers block structure and data structures. Chapters 8 through 12 present advanced topics. Tennent’s analysis of procedural abstraction and general binding mechanisms is used as a focal point for Chapter 8. Chapter 9 analyzes forms of imperative control and branching. Chapter 10 surveys techniques for converting a denotational definition into a computer implementation. Chapter 11 contains an overview of Scott’s inverse limit construction for building recursively defined domains. Chapter 12 closes the book with an introduction to methods for understanding nondeterminism and concurrency.

Throughout the book I have consistently abused the noun ‘‘access,’’ treating it as a verb. Also, ‘‘iff’’ abbreviates the phrase ‘‘if and only if.’’

Read More/Download

Categories. Types and Structures: An Introduction to Category Theory for the working computer scientist

By Andrea Asperti and Giuseppe Longo

The main methodological connection between programming language theory and category theory is the fact that both theories are essentially “theories of functions.” A crucial point, though, is that the categorical notion of morphism generalizes the set-theoretical description of function in a very broad sense, which provides a unified understanding of various aspects of the theory of programs. This is one of the reasons for the increasing role of category theory in the semantic investigation of programs if compared, say, to the set-theoretic approach. However, the influence of this mathematical discipline on computer science goes beyond the methodological issue, as the categorical approach to mathematical formalization seems to be suitable for focusing concerns in many different areas of computer science, such as software engineering and artificial intelligence, as well as automata theory and other theoretical aspects of computation.

This book is mostly inspired by this specific methodological connection and its applications to the theory of programming languages. More precisely, as expressed by the subtitle, it aims at a selfcontained introduction to general category theory (part I) and at a categorical understanding of the mathematical structures that constituted, in the last twenty or so years, the theoretical background of relevant areas of language design (part II). The impact on functional programming, or example, of the mathematical tools described in part II, is well known, as it ranges from the early dialects of Lisp, to Edinburgh ML, to the current work in polymorphisms and modularity. Recent applications, such as CAML, which will be described, use categorical formalization for the purposes of implementation.

In addition to its direct relevance to theoretical knowledge and current applications, category theory is often used as an (implicit) mathematical jargon rather than for its explicit notions and results. Indeed, category theory may prove useful in construction of a sound, unifying mathematical environment, one of the purposes of theoretical investigation. As we have all probably experienced, it is good to know in which “category” one is working, i.e., which are the acceptable morphisms and
constructions, and the language of categories may provide a powerful standardization of methods and language. In other words, many different formalisms and structures may be proposed for what is essentially the same concept; the categorical language and approach may simplify through abstraction, display the generality of concepts, and help to formulate uniform definitions. This has been the case, for example, in the early applications of category theory to algebraic geometry.

The first part of this book should encourage even the reader with no specific interest in programming language theory to acquire at least some familiarity with the categorical way of looking at formal descriptions. The explicit use of deeper facts is a further step, which becomes easier with access to this information. Part II and some chapters in part I are meant to take this further step, at least in one of the possible directions, namely the mathematical semantics of data types and programs as objects and morphisms of categories.

Read  More/Download

Semantics with Applications

This book is one of the best for knowing formal semantics of programming languages. You will learn how to use semantics for validating prototype implementations of programming language, how to use semantics for verifying analyses used in more advanced implementations of programming languages and how to use semantics for verifying useful program properties including information about execution time.

Read More/Download