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