5 September 2006
----------------

CS 520 PRINCIPLES OF PROGRAMMING LANGUAGES

Instructor: Assaf Kfoury

Read information on the course homepage:

http://www.cs.bu.edu/~kfoury/CVS-Working-Files/CS520-Fall06/Home.html

==============================================================

Things you need to do immediately:

(1) Add yourself to the class mailing list, by issuing the
    command "csmail -a cs520" from your csa.bu.edu account.

(2) Buy the required textbook, by Benjamin Pierce. Copies 
    available at the BU Bookstore.

Things you need to do frequently, before and after every lecture:

(1) Inspect course webpages for new handouts and announcements.

(2) Do reading assignments and homework assignments as soon as
    they are posted.

==============================================================

READING ASSIGNMENT

(1) Pierce, Ch 1: Pleasant and easy introduction to type systems in
    programming languages. Not presented in lecture.

(2) Pierce, Ch 2: Read and study as much as you can. Induction in
    Section 2.4 is a big topic, and we will cover it in different
    ways, some omitted by Pierce.

(3) Pierce, Ch 3: Read inasmuch as you need to understand class
    presentation.

==============================================================

UNTYPED ARITHMETIC EXPRESSIONS (Ch 3)

SYNTAX (Sect 3.1 and 3.2)
======

BNF Style Definition (p 24)
--------------------

   t ::=                          terms
        true                         constant
        false                        constant
        if t then t else t           conditional
        0                            constant
        succ t                       successor
        pred t                       predecessor
        iszero t                     zero test


Definition by Induction (p 26)
-----------------------

The set T of terms is the smallest such that:

   1. {true, false, 0} is a subset of T,
   2. if t is in T, then 
         {succ t, pred t, iszero t} is a subset of T,
   3. if t1, t2, and t3 are in T, then
         "if t1 then t2 else t3" is in T.

Definition by Inference Rules (p 26)
-----------------------------

   -------------      --------------         ----------
    "true" in T        "false" in T           "0" in T


     t in T               t in T                t in T
   --------------     ---------------        ----------------
   "succ t" in T       "pred t" in T          "iszero t" in T


     t1 in T    t2 in T    t3 in T
   --------------------------------
     "if t1 then t2 else t3" in T


Concrete Definition (p 27)
-------------------

    S_0 = empty set

    S_{i+1} = { true, false, 0 } union

              { succ t, pred t, iszero t | t in S_i } union

              { if t1 then t2 else t3 | t1, t2, t3 in S_i }
   

    S = Union { S_i | i = 0, 1, 2, ... }


PROPOSITION (p 28)  T = S.


INDUCTION ON TERMS (Sect 3.3)
==================

Inductive definition of the "set of constants in term t", Consts(t) -- page 29.

Inductive definition of the "size of term t", size(t) -- page 29.

Inductive definition of the "depth of term t", depth(t) -- page 30.

THEOREM [Principles of Induction on Terms] -- page 31




SEMANTICS (Sect 3.4 and 3.5)
=========