CS463 - Midterm Review - Spring 2024

Definition of the core lambda calculus' terms;

t ::= x | λx.t | (t t)

• x represents a variable.
• λx.t represents a "lambda" (a function, an abstraction). The function is anonymous, because it has no name. The parameter has a name, though (here, we've named it x).
• (t t) represents an application of one term onto another - assumedly the left term evaluates to a λ value, or else we won't be able to reduce this application term (nor reach a value overall with evaluation).
  • when application is implied we often omit the parentheses and rely on adjacency. For example, f a b c is the same as (((f a) b) c).

We also define what terms in our language are values (terms that cannot be further evaluated and represent a "normal form"). For the core untyped lambda calculus, just lambas are values. (We often extend our language, adding more terms and more values).

v ::= λ x . t

Evaluating a term in the untyped lambda calculus means applying evaluation rules upon a term until the result is a value.

• Lambdas are by definition already values. (thus there are no evaluation rules that look at just a lambda all by itself, turning it into some even-simpler forms).
  • This is why you'll never look inside a lambda for evaluation steps to take, even if you see a nice "1+2" hiding in there; no evaluation rules will give you the chance to peek inside.
• We never actually evaluate a variable, because they should be substituted away before we ever reach them. Finding a variable that is "free" (not enclosed by an accompanying lambda that introduces the variable name) would essentially be a runtime error during evaluation: the variable is undefined there.
• Applications are not values and thus may be evaluatable. They need a lambda as the left term; if it isn't yet a lambda, evaluate it until it becomes one.
  • Progress towards a function argument:

                  t1  ->  t1'
    E-App1  -----------------------
             (t1 t2)  ->  (t1' t2)
    

  • assumedly when t1 has no more evaluation possible, it's both a value and is specifically a lambda. If not, our application is not able to simplify to a value overall; for example, (5 6) makes no sense as a request to use 5 as a function. So let's think just about cases where t1 did eventually end up as a lambda.
• we also will choose (this time) to require that in our language, only values are supplied as arguments to lambdas; so we need to make progress on the second subterm in an application once we've already got a value for the first subterm:
  • Progress towards a value as the argument to our lambda:

                  t2  ->  t2'
    E-App2  -----------------------
             (v t2)  ->  (v t2')
    

  • again, we're hoping/assuming that v is actually a lambda, but this rule doesn't need to be explicit about it. For now, any value will do there, and we enforce the "actually a lambda" requirement later.
• evaluation of an application of a lambda and any other value means to substitute that value (the function's argument) for the variable that the lambda introduces, throughout the body-term of the lambda.

              
  E-App-Abs  ----------------------------
              ((λ x . t) v)  ->  t[x ↦ v]
  

We can embody lazy semantics (where we don't have to evaluate arguments to value before substituting them) by throwing out E-App2 and modifying our E-App-Abs rule to allow arbitrary terms as the argument. Note below that we have t2 instead of v, meaning that we can substitute some arbitrarily large term (perhaps into more than one usage of the parameter if the variable had shown up in the lambda more than once), instead of only being able to substitute values.

            
E-App-Abs-Lazy  ---------------------------------
                 ((λ x . t1) t2)  ->  t1[x ↦ t2]

• this rule is not a usual part of the lambda calculi we've looked at! This is a variant (just E-App-1 and E-App-Abs-Lazy would be present).

We looked at how to represent some things by effectively writing code in our language (instead of extending the language with extra terms and values and evaluation rules), primarily what are called "Church Booleans" and operations on them. This shows us that we can use this very terse language as-is to start describing more familiar calculations, but we learned that extending the language with boolean primitives was far more inviting. We could still encode functions and other useful things using extensions, giving us the best of both worlds. Here were the expressions we used to represent common true/false values and operations.

Encoding booleans and operations in the core untyped lambda calculus

true  = λ x . λ y . x
false = λ x . λ y . y
not   = λ x . ((a false) true)
or    = λ a . λ b . ((a a) b)
and   = λ a . λ b . ((a b) a)
if    = λ b . λ x . λ y . ((b x) y)

• a closing comment: if you extend the language to natively include booleans, you should not use the above encodings, because in that case true is not the same thing as λx.λy.x; one's an atomic token (true) term, one's a lambda term. Above, we are simulating having booleans by using lambdas, but we never had actual booleans in the language itself.

• Language extensions:

  t ::= ... | true | false | if t t t | equals t t
  v ::= ... | true | false
  

• evaluation extensions:

                        t1  ->  t1'
  E-If        -------------------------------
               if t1 t2 t3  ->  if t1' t2 t3
  

  E-If-true   -----------------------
               if true t2 t3  ->  t2
  

  E-If-false  ------------------------
               if false t2 t3  ->  t3
  

  • rules for equals might need to be exhaustive as our language grows. We could also just leverage some other total predicate function over terms, such as alpha-equivalence α (see our implementation in class; honestly, I will be avoiding equality on our test).

                               (λx1.t1) =α (λx2.t2)
  E-Equal-lambda-true  ------------------------------------------
                        (equal (λ x1 . t1) (λ x2. t2)  -->  true
  

                               (λx1.t1) ≠α (λx2.t2)
  E-Equal-lambda-false -------------------------------------------
                        (equal (λ x1 . t1) (λ x2. t2)  -->  false
  

There are two approaches here to extending the language with numbers. We can try to implement our own numbers with zero and successor and predecessor, or we can borrow from our host language.

• Many other extensions are simple to add, such as pairs, lists, records, and so on. We performed some of these in class (see class notes), and you might want to be prepared to either describe the process or carry it out. For instance, we might show the standard definitions of evaluation and substitution for the lambda calculus, and have you extend the language somehow. Or, we might need to write evaluation rules for some extra feature of the language. (later in the semester we would also want to write new type checking rules).
• many much more significant language features can also be added in this fashion: assignments (and state); classes/objects; case statements; abstract data types; type inference. We will not tackle some giant new extension on the test!

• the Ω-combinator always diverges - it evaluates to itself.

  Ω = ( (λ x . x x)  (λ x . x x) )
  

• the Y-combinator helps us define recursive definitions in a language that doesn't directly support recursion:

  Y = λf. ( (λx. (f (λy.x x y)))
            (λx. (f (λy.x x y)))
          )
  

  • define a function whose first argument is assumedly going to be an entire copy of itself. Feed that "stub" of a function to the Y combinator and it will "tie the recursive knot" for you.

  factStub = λself.  λn. if (n=1) 1 (n*(self (n-1)))
  fact = (Y factSub)
  

  • you can test definitions like this in our class-provided code:

  ULC>  eval (App fact (Num 5))
  (Num 120)
  

Note that the y-combinator uses untyped lambdas. When we explore the simply typed lambda calculus, without extending our language significantly, we won't be able to represent recursion such as this. There, only the extension version will suffice when we have types; there's a hidden point at which the types need to be ignored for the Y combinator to do its trick.

We also explored the fix extension. Happily, it expects something of the exact same shape that the Y-combinator does (see factStub above).

t ::= ... | fix t
(no new values!)

We use it by creating a term like fix factStub. Often this may just be used as part an entire encoding definition, without bothering to name the stub.

fact = fix (λself. λn. if (n=1) 1 (n*(self (n-1))))

And then we call it like any other function: (fact 5).

If you are working on values that are recursively built up, like navigating lists, you will likely need to use recursion in order to write functionality using those terms.

• readability (ease of understanding progs)
  • simplicity, orthogonality, available data types, syntax
• writability (ease in creating/modifying progs)
  • simplicity and orthogonality, abstractions available, expressivity (ways to write same task)
• reliability (conformance to specs)
  • type checking, exception handling, aliasing, minimal implicit coercions, good readability/writability
• cost (time, training, money…)
  • training time, compilation time, runtime, cost of tools, cost of maintenance

• sentence: string of characters from an alphabet
• language: set of sentences
• lexeme: the characters from a sentence that correspond to a token (e.g. "foo", "123")
• token: representation of a lexical unit, e.g. (Identifier "foo"), (Number 123)
• recognizer: device that finds out if string-inputs are sentences of a specific language
• generator: device that generates sentences of a language. (Hard to build/use well)

• Type 3: regular languages.
• Type 2: context-free languages.
• Type 1: context-sensitive languages.
• Type 0: recursively enumerable languages.

• abstractions (non-terminals) for groups of syntactic structures. They can build on each other/themselves to completely define specific languages.
• terminals are lexemes (specific characters)
• production rules: define possible patterns that can be used to replace non-terminals.
  • our syntax:
    • use UPPERCASE or CamelCase style for non-terminals
      • and just notice that if something is on the left side of a production rule, it needs to be a non-terminal thanks to the rules of how to generate production rules in a Type 2 grammar.
    • lefthand side: exactly one non-terminal
    • righthand side: any mixture of terminals and non-terminals (can also just be epsilon, ε, to indicate the empty string)
    • for convenience, you can put multiple production rules of the same non-terminal in one line, e.g. S -> S+T | S-T | T
• derivation: repeated substitutions of non-terminals (one at a time please) to arrive at a sentence in a language. May be a left-, right-derivation (or neither) based on which non-terminal we choose to replace in each step of the derivation.
  • sentential form: the string of symbols in one step of a derivation. Only all-terminal forms are sentences.

• a hierarchical representation of a derivation. Inner nodes (including the root) are non-terminals, leaves are the terminals. Since there's no record of which part of the tree you drew when, there's no notion of a "leftmost parse tree generation" that would correspond to a leftmost sentence derivation.
• ambiguity: a grammar is ambiguous IFF there exists a sentence that has 2+ unique parse trees for it. You can also show this sufficiently with 2+ unique leftmost derivations (or 2+ unique rightmost derivations) of the sentence, because it will force you to show at which step there were two different choices for the same non-terminal (the place where the two parse trees differ from each other).
• associativity: operators can associate left or right. Left-only recursion of production rules results in left-associativity, as well as parse trees that are "heavier" on the left.
  • Example: the plus operator is left-associative in this example because the production rule for S puts S to the left of the plus: S -> S+T

AGs allow us to decorate a parse tree with values, encoding some (but not all) semantic information. We place these attributes at any node in the parse tree (both leaves and interior nodes), based upon parent or child nodes' attributes or structure, and generated by use of semantic functions. Lastly, we also may enforce predicates about these attribute values at any node.

• specific attribute values are associated with specific symbols (non-terminals/terminals)
• all production rules get "semantic functions" that define attributes of the non-terminals in that rule
  • some are synthetic: building up attributes from leaves to root.
  • some are inherited: deciding attributes from root to leaves.
  • some are intrinsic: only dependent upon the node itself.
• production rules also get predicates that must be true for the sentence to be in the grammar. These compare attribute values.

We had an example that looked at two attribute values - representing the actual type of a term, and separately the expected type of a term. We saw some of the semantic functions for specific production rules to see how the attributes were added, and we also looked at some attribute predicates e.g. that the actual type and expected type values at a node needed to be compatible.

You will not need to perform these steps; however, you should be able to discuss some of the high-level reasons to use AGs.

• There's no 'best' approach, because we want to encode the meaning of programs, which can be better described in different ways for different situations. The intended audience can greatly affect what style is most useful: e.g. language implementers, programmers, or someone proving properties about a specific program.
• three approaches discussed: operational, denotational, axiomatic