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 * 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