Final Exam Coverage

Logistics

• Apr 29, 8AM-10AM, SB 111
• You are permitted 2 letter-sized, double-sided pages of notes to use on the exam (no sharing notes)
• No electronics!
• The exam will NOT be cumulative!
• The exam will be ~30-40% objective (MC), and 60-70% written problems.

Topics

1. Semantics

   • Basic definitions: what is it? why do we care?
     • Math
     • ematical rigor!
   • Primary approaches:
     • Operational {big-step, small-step}
     • Denotational (but we didn’t cover this one)
     • Axiomatic
   • Rules of inference
     • Terms: premises, side-conditions, conclusion, axioms, etc.
   • Proof trees & Derivation strategies

2. Grammars

   • Why do we have them?
     • Formal specification of valid syntactic objects (for later semantic analysis)
   • Chomsky hierarchy
     • Regular, Context-free, Context-sensitive grammars/languages
   • Backus-Naur Form (BNF) -- used for specifying grammars
   • IMP language (described in BNF)

3. Big-step Semantics

   • e ⇓ v : e evaluates to v (in one big step)
     • ⇓ is a relation over syntactic objects, environments, and possible results
     • Equivalence to eval function (interpreter)
   • Big-step rules for IMP
   • Proof trees concerning IMP programs using ⇓
     • Concerning the result of evaluating expressions/statements
     • Concerning the equivalence of different programs
       • Why is this important?

4. λ Calculus

   • Syntax & Semantics
     • Study precedence rules
       • e.g., “λx.x λz.y z” fully parenthesized is 
“λx.(x (λz.(y z)))”
   • ASTs (draw and read)
   • Free variables & Variable capture
   • ɑ-conversion, β-reduction, η-reduction
   • Normal form
   • Evaluation strategies: applicative-order vs. normal-order
     • Equivalence to: eager/strict eval vs. lazy eval
     • Equivalence to: call-by-value vs. call-by-name
   • Data representation
     • Booleans
     • Church numerals

5. Axiomatic Semantics

   • Hoare triples, e.g., {P} C {Q}
     • Partial correctness
   • Language of assertions
   • IMP-language axiomatic semantic rules
   • Rule of Consequence
     • We can strengthen a valid Hoare triple’s preconditions and weaken its postconditions, and it will still hold
   • Strong vs. Weak assertions (relative)
   • Loop invariants used to prove the correctness/goal of loops

Written Problems

1. Big-step Semantics

   • Come up with rule(s) of inference to describe a new IMP language construct (similar to the for loop in the assignment)
   • Come up with a proof tree for some ⇓ assertion
     • I will provide all the IMP rules

2. λ Calculus

   • Given λ-calculus expressions, draw ASTs, identify free/bound variables
   • Given λ-calculus expressions, show reductions to get to normal form (or indicate that normal form is not reachable)

3. Axiomatic Semantics

   • Given an IMP program, derive the weakest precondition (given a postcondition that holds)
   • Come up with a loop invariant and loop goal for a looping program, and show that P → Q after the loop condition becomes false.