CS611 Lecture 12 uF Semantics, Error Checking and Scope 9/26/2001Scribe: Manpreet Singh (manpreet@cs)Rohit Ananthakrishna (rohit@cs) Lecturer: Andrew MyersThe language uF presented in class is a call-by-value, left-to-right eager, untyped functional language. Itis an extension of the CBV λ-calculus introduced in the previous lecture.1. Syntax of uF: An expression is represented by the character e. A program is an expression containingno free variables. Suppose n denotes an integer literal, x denotes a variable name, and eidenotes anexpression. Expressions are then described by the following BNF grammarb ::= n | #t | #f | #u | se ::= b | x | e1⊕ e2| if e0then e1else e2| e1,e2|λx e | e1e2| let x = e1in e2| rec y(λx e)v ::= b | λx e | v1,v2#u denotes a unit,#t and #f denote the booleans true and false respectively, s represents the strings.#u is used when we want to return a dummy value. (This will become clear when we look at errorchecking in uF.)2. SOS to extend CBV semantics with rec: Note that we have added recursive functions to theCBV semantics. So, we extend the SOS of CBV λ-calculus with rec.rec y (λx e) −→ λx(e{rec y (λx e)/y})We are just unrolling the first recursive call in the above semantics. We illustrate the above semanticswith the following factorial examplelet fact = rec fλxif x == 0 then 1 else x ∗ f(x − 1) in fact 3−→ let fact = λx if x == 0 then 1 else x∗(recfλxif x == 0 then 1 else x∗f(x−1)) (x−1) in fact 3−→ (λx (if x == 0 then 1 else x ∗ (rec fλxif x == 0 then 1 else x ∗ (rec f (x − 1))(x − 1)))3−→β(if 3 == 0 then 1 else 3 ∗ (rec fλxif x == 0 then 1 else x ∗ (rec f(x − 1))(3 − 1))−→ 3 ∗ (rec fλxif x == 0 then 1 else x ∗ (rec f(x − 1))(2))...−→ 3 ∗ 2 ∗ 1If we stare at the SOS of rec the right hand side of the inference is the same as (λyλx e)(rec y (λx e)).That is we haverec y (λx e) −→ (λyλx e)(rec y (λx e))Therefore (rec y (λx e)) is a fixed point of (λyλx e). This gives us a clue to how we can translate “rec”into the simple CBV λ calculus. Equivalently,[[ rec y λx e]] = FIXCBV(λyλx [[ e ]] )13. Error Checking in uFOur previous translation-based semantics for uF didn’t deal with stuck configurations in a completelysatisfactory way. Once the operations (e.g., left) had been translated into lambda calculus, theirbehavior in situations that the operational semantics would consider to be stuck is to keep on computingbut generating gibberish. For example, if we evaluated the program left 0, we would get the identityfunction, which makes no sense.We can perform a translation that models run-time error checking. This means that the translatedprogram must check if operators have been passed with values of the right type. So we tag each of thedifferent possible values permitted in uF and check if an operand has operands having the desired tagvalues. This tagging corresponds fairly closely to what is done in real untyped languages like Scheme.Each value is now semantically equivalent to a pair where the first value is the tag value and the secondoperand the actual value. Here is how we translate values:[[ # u]] = 1, #u[[ # t]] = 2, #t[[ # f]] = 2, #f[[ n]] = 3,n[[ v1,v2]] = 4, [[ v1]] , [[ v2]] [[ λx e]] = 5,λx [[ e]] To the above we add 0, #u which is the tag for error. This is returned when a run-time error occurs.The value #u in this pair is chosen arbitrarily.We illustrate the above semantics by looking at two examples.(i) Error che cking in addition : The values to “+” must have a tag value of 3 otherwise it is anerror.[[ e1+ e2]] = l e t p1=[[e1]] i nlet p2=[[e2]] i nlet t1=leftp1inlet t2=leftp2inif t1=3 ∧ t2=3then 3, right p1+rightp2 else 0, #u(ii) Error che cking in function application : If we have a function application (e1e2), we have toensure that e1is indeed a function.[[ e1e2]] = l e t p1=[[e1]] inlet p2=[[e2]] i nlet t1=leftp1inif t1= 5 then (right p1) p2else 0, #uWhat is our notion of correctness for this translation? In addition to the earlier notions of correctness,we add the following: if an evaluation would have gotten stuck in the operational semantics, thetranslated program should evaluate to 0, #u.IfS is a representative stuck expression,e −→∗S ⇒ [[ e]] −→∗ 0, #uwhere2S ::= #u v | #t v | #f v | nv| v1,v2 v| if #uthene1else e2| ...| #u ⊕ #u | ...| left #u | right #u | ...4. Scope Rules: We have been looking at languages with block-structured static scope,inwhichidentifiers are bound to variables based on the static (lexical) structure of the program. With staticscope, the binding of a variable is determined by the point in the program at which the identifieroccurs.TheIMP language that we saw in this course has block-structured static scope. Because ourtranslational semantics makes environments into explicit first-class entities, we can describe alternatescoping mechanisms quite easily. With dynamic scope, the alternative, an identifier is bound to thevariable existing at the point where the function is cal led, not where the function expression is evaluated.Thus, the meaning of an identifier is determined by the state of the executing program.The following example evaluates differently in the two approaches:let delta = 2 inlet bump = λx (x +delta)inlet delta = 1 inbump 2With static scope, the identifier delta in the definition of the function bump is bound to the outervariable delta. The program returns the value 4. With dynamic scope, delta is bound to the variabledelta that is in the scope at the point where the function is called. The program returns the value 3.5. Semantics to capture the scope rules: The store that we saw in IMP maps locations totheir values. An environment is a map from strings to other things. We will explicitly represent theenvironments as uF term ρ that maps variable names (as strings) to their values. That is ρ (“x”)returns the value of x in ρ.1. Static scope:The denotational semantics for static scope areD[[ x]] = λρ ρ(“x”)Applying both sides to an arbitrary ρ,weget D[[ x]] ρ = ρ(“x”)D[[ b]] = λρ bD[[if e0then e1else e2]] = λρ if D[[ e0]] ρ then D[[ e1]] ρ else D[[ e2]] ρSemantics of function declaration and let are more complicated. In order to define this we use anew function extend.extend ≡ λρλxλv(λz if x = z then v else ρ(z))Intuitively, extend takes