CSC302 2006S, Class 14: Scheme Semantics (2)

Admin:
* Cookies!
* This week, we're clearly doing stuff that looks like Math.
* Reading for Friday: The meaning of lambda (three equations, plus
  any auxiliaries). [May be updated]
* Extra credit for tomorrow's talk!

Overview:
* The three lambdas
* About the four semantic functions
* First few parts of the definition of Script-E

/Detour: Actuals vs. Formals
Consider
  ((lambda (a b c) ...) e f g)
* We call a b and c "parameters"
* We also call e f and g "parameters"
* Whoops!  Need to use terms that distinguish the two!
* Custom: a b and c are "formal parameters" - "formals"
* Custom: e f and g are "actual parameters" - "actuals"

/Why are there three forms of lambda?/
* Here they are
  (lambda (I*) Gamma* E0)
  (lambda (I* . I) Gamma* E0)
  (lambda I Gamma* E0)
* All three end with "Gamma* E0"
  * The body of a lambda must have a sequence of commands and then a single expression
    * Assumption: The return value is the value of the expression
    * Lambdas *must* have an expression
    * Commands are not necessary
* There are three forms because Scheme supports both fixed and
  variable arity lambdas
  * (lambda (I*) Gamma* E0) - Fixed arity; Semantics will need to include something that confirms that the number of actuals equals the number of formals
  * (lambda (I* . I) Gamma* E0) - Minimum variable arity: Must have one actual for each formal in I*, all remaining parameters are bound in a list and assigned to the formal given by the last I
  * (lambda I Gamma* E0) - Pure variable arity: All parameters are shoved in a list and assigned to the formal given by the I
  * Since the third is just a variant of the second, you'll see
    ScriptE[[(lambda I Gamma* E0)]] = ScriptE[[(lambda (. I) Gamma* E0)]]

/On to the Semantic Functions and Helper Functions/

* Semantic functions: Purpose is to assign a "meaning" to each
  valid expression
  * That is, translate to an operation in the lambda calculus
* Four semantic functions for four kinds of things to which we assign meanings:
  * ScriptE: Gives meaning to expressions
    ScriptE is a function of "three" parameters
    ScriptE: Exp -> U -> K -> C
  * ScriptE*: Gives meaning to a sequence of expressions
    * Will probably need to update the environment and/or store
    * ScriptE*: Exp* -> U -> K -> C
    * Note: K = E* -> C (expects a sequence of expressions)
  * ScriptC: Gives meaning to commands
    * Probably lke ScriptE, but no use of result
    ScriptC: Com -> U -> C -> C
    * Suppose we're going to do "theta" with this command.
      What do we do with the stuff that happens after command?
  * ScriptK: Gives meaning to constant values
    * ScriptK: Con -> E
    * Definition deliberately ommitted.  Why?

Coming next: Assigning of meanings to each of the syntactically
valid utterences

Uses associated helper functions (defined on pp. 42 and 43)
* "You gotta read the code to figure out what they do."

What is the meaning of a constant?  More precisely, suppose
we have a constant, an environment, and a continuation,
what is the continuation after evaluating that constant?
* Approximately: Get the value, send it to the continuation, and do whatever is left

ScriptE[[K]] = \rho kappa . send (scriptK[[K]]) kappa
* Because rho does not appear on the rhs, we know that the
  evaluation of constants is independent of the environment
* What does the helper function send do?
  * Send provides a value to a continuation
  send : E -> K -> C : Send is a function that takes an exp. and an exp. cont. and returns a command cont.
  * Expression continuations are functions from E* to C
  * Send will need to package the single E into an E* and then
    call K on it
  send = \ epilon kappa . kappa <epsilon>
  * Could we have just written
ScriptE[[K]] = \rho kappa . kappa <(scriptK[[K]])>
  * The "send" clarifies

What do you expect to do with an identifier?
* We'll look it up in the environment
* Send the retrieved value to the continuation
* Whoops!  Also need to check to make sure that it's valid
  (Build a new continuation that checks validity and, if valid,
    calls the original continuation)

ScriptE[[I]] = 
  \ rho kappa . hold (lookup rho I)
                     (single (\ epsilon . 
                                epsilon = undefined
                                -> wrong "undefined variable"
                                ,send epsilon kappa))

What do you expect lookup to do?
* See if I is in rho, and, if so, return its location
* Otherwise, return undefined
lookup = U -> Ide -> L
lookup = \ rho I . rho I
* Exists primarily for readability

What do you expect single to do?
* Sam expects single to convert a \e function to a \e* function
single: (E->C) -> K
single: (E->C) -> (E*->C)
single: (E->C) -> E* -> C
single = \ psi epsilon* .
  #epsilon* = 1 -> psi (e* down 1)
                , wrong "bozo"

We're not sure what hold does, except that it sounds like "hold on a minute"
* Hold handles the "whoops, I have a location and need a value" problem