CSC302 2006S, Class 13: Scheme Semantics (1)

Admin:
* This week, we're clearly doing stuff that looks like Math.
* Reading for Wednesday: The meaning of lambda (three equations, plus
  any auxiliaries).
* Revised assignment:
  * Why three lambda definitions? in syntax (or semantics)
* Note that I post your questions and comments (and some answers and responses) regularly.

Overview:
* About formal semantics
* About denotational semantics
* Abstract syntax of Scheme
* Domain sets
* Types of semantic functions
* First few parts of the definition of Script-E

/About Formal Semantics/

* General problem: How do you specify what the constructs of a language are supposed to do?
* Why do we care?
  * Gives understanding to the syntax
  * Provides a mechanism for comparing languages
  * Support implementers
  * Support programmers
* How?
  * Informally, with English
    * But not everybody speaks English
    * Ambiguous
    * Authors may not have thought carefully about some issues
  * With an implementation
    * Probably won't stand by itself
    * Difficult to distinguish intentional and unintentional behaviours
  * Simple formal defintiion: Translation to a known language
  * Advanced formal defintion: Using some Mathematical technique
    * E.g., Gries defines a Pascal variant using preconditions and postconditions for each kind of statement

/Denotational Semantics/

* Mostly formal mechanism for defining the meaning of constructs
* Translation of each construct to a simpler language: The typed
  lambda calculus
* Cyncial view: Implementation in lambda calclulus
  * That is, implementation in a language few understand
* Better view: Understanding through known, simple, concise, precise, model.

/Step 0: Formal Syntax/

/Step 1: Simplified Syntax/

* Do not care about particular text for valid expressions
* Care about the *form* of those expressions
* Four basic types:
  * Constants
  * Identifiers
  * Expressions
  * Statements (= Expressions)
* Expressions are used in a context in which you expect a value,
  statemnets in a context in which you do not.
* Lots of forms of expressions:
  * K ; constants
  * I ; Identifier - Expect to look up in some table
  * (E0 E*) ; Function call
  * (lambda (I*) Gamma* E0) ; Function definition
  * (lambda (I* . I) Gamma* E0) ; Function definition
  * (lambda I Gamma* E0) ; Function definition
  * (if E0 E1 E2) ; Conditional with else
  * (if E0 E1) ; Conditional w/o else
  * (set! I E) ; Change to memory

/Domain Sets/

* Typed lambda calculus
  * Types help ensure correctness
  * Types improve readability
* alpha in L: Locations
  * The particular form of the values doesn't matter!
* nu in N: Natural numbers
* Basic types
  * T: Boolean values
  * Q: Symbols: Atomic unit of expression, like foo or bar
  * H: Characters: Individual character, like #\a
  * R: Numbers
* Compound types
  * Ep = L x L x T: Pairs
  * Ev = L* x T: Vectors
  * Es = L* x T: Strings
  * Why does each include a Boolean?
    * Mutability!  See, for example, the def'n of setcar!
* M: Miscellaneous values
  * Like symbols, but reserved
  * true, false, null, undefined, unspecified
  * Particular implementation is implementation specific
* phi in F: Procedures
  * L x (E* -> K -> C)
    * Notation: Arrow means "function"
    * Curried: Function from E* and K to C
    * L might be for return value (we'll need to figure this out)
* E: Expressed values
* sigma in S = L -> (E x T): Store
  * Given a location, get back an expressed value and a truth value
  * Memory:
  * Truth value: Is the memory location in use (allocated)
  * How do we store something?  Pick a location that is not in use
    (using new), and write a new function.
    Suppose "store 'foo' at memory location 5", given existing store sigma0
    sigma1 = \alpha . alpha = 5 -> foo, (sigma0 alpha)
    * Important issue: No side effects permitted in the lambda calculus;
    * Simjulate side-effects by returning modified "functions"
* rho in U = Ide -> L: Environments
  * Givena  symbol, determine the correspnoding area in memory
  * Accessing value is a two-step process: apply rho then sigma
  * Note that this model permits aliasing
* Continuations:
  * Theta in C = S -> A, command continutations
    * Given a store, return an answer
    * A particular setting of memory determines your result.
  * kappa in K = E* -> S -> A: Expression continuations