Lecture Notes 1-2 (Aug 28 - 30): Introduction; Predicate Logic

CS430/530: Formal Semantics, Fall 2013, Yale University

Please read and understand everything in Reynolds Chapter 1 and Appendix (even A.5 and A.6, which were not covered in class)

Here is the PDF file for the slides used in the first two lectures.

Additional comments:

  1. In this course, we are primarily interested in studying the meanings of programming languages (e.g., C, C++, C#, Java, Eiffel, JavaScript, ML, Haskell) and specification languages (e.g., Z, TLA+, VDM, B, Alloy, CASL, UML).

    Note some programming languauges support static type annotations or "design by contract", that is, a programmer can annotate various program constructs with some sort of type information or program assertions. A typechecker or contract-checker (done at compile- or run time) can be used to help rule out certain classes of bugs.

    Specification languages can be used to formally build "models" or "blueprints" for any system (not necessarily software) --- they often come with tools that can be used to generate test cases, detect bugs, or verify the integrity of the underlying system.

  2. Before we can describe the formal semantics of any programming- or specification language, we first need to pick a "meta language" --- a language which we can use to define the "meaning" of the "object" language we are interested in formalizing.

    The most common "meta language" for describing mathematical systems is some sort of set theory formalized using first-order logic, e.g., the Zermelo-Fraenkel set theory with axiom of choice.

    For this class, we will stick to the familiar set theory as documented in the Appendix of Reynolds book; we will also assume the availability of inductive definitioins as discussed in Chapters 1-3 of Harper.

  3. If you are unhappy with the *informal nature* of the meta language and meta reasoning we use, you can use a formalized "meta language", such as the Calculus of Inductive Constructions (CIC) implemented in the Coq proof assistant. CIC is a rich high-order predicate logic extended with inductive definitions. Coq allows you to write down machine-checkable mathematical proofs so that you are sure that the mathematical reasoning you did is indeed correct (assuming that the underlying meta logic is consistent and the implementation of the proof checker is correct).
  4. The Appendix of Reynolds gets you acquainted with some of the most important notations and properties in set theory. Reynolds Chapter 1 defines the formal semantics of one sample object language (i.e., a first-order predicate logic with integer expressions). This example language is not a programming language but rather a specification language (for example, in this language, you don't write programs but write specifications instead).
  5. Denotational semantics is to give the meaning of a language by mapping each "abstract syntax tree" in the object language into a mathematical object (often called "a denotation") in the meta language.

    For example, In Reynolds Charper 1, there are two semantic functions:

    [[ - ]]intexp maps each "intexp" expression into a mathematical function from Σ to Z;

    [[ - ]]assert maps each "assert" expression into a mathematical function from Σ to B;

    where Σ is a mathematical function from variables to Z.

  6. Reynolds Chapter 1 also serves as a review of familiar concepts in predicate logic, e.g., what are logical inference rules and axioms, what are formal proofs, what makes a logic sound, and what are bound and free variables. If you want to learn more about formal logic, please read the Chapters 1 and 2 of Huth and Ryan.

Copyright (c) 2011 Zhong Shao, Dept. of Computer Science, Yale University