LMU ☀️ CMSI 585
PROGRAMMING LANGUAGE FOUNDATIONS
Final Exam
  1. Fill in the truth-table for the propositional formula $(p \supset q) \land (q \lor \neg p)$ in $K_3$.
    pq( p ⊃ q ) ∧ ( q ∨ ¬p)
    TT
    TF
    TO
    FT
    FF
    FO
    OT
    OF
    OO
  2. Write (in the logic notation used in this class) an encoding of “Those who once believed Socrates knew Type Theory may have a 35% chance of winning the US Open”.
  3. Gödel’s first incompleteness theorem states that:
    • No logical system can be both sound and complete.
    • Hilbert’s Entscheidungsproblem is unsolvable.
    • A second order logic is necessary to express certain mathematical truths.
    • No logical system can prove all truths about arithmetic unless it was inconsistent.
  4. What is $|\{ (x, y) \in \mathbb{N} \times \mathbb{N} \mid x \geq 2 \land y \geq 2 \land x \uparrow\uparrow y \lt 1000 \} |$ ?
  5. The untyped lambda calculus is good for ________________ but not for ________________.
  6. Reduce the expression $\,(\lambda x. \lambda y.\,x\,y)\,y\;$ to normal form, working from the outside in and showing each step. Annotate each step with the rule you are using ($\beta$ or $\eta\,$):
  7. Define the function “log-base-2 of a natural number” in the untyped lambda calculus using the $Y$ combinator, where the function counts the number of times you need to floor-divide a number to reach 1 or below. You can use actual numerals and operators (meaning you don’t need to use Church encodings nor the primitive definitions of addition and division, thankfully).
  8. Give the number of inhabitants for each type.
    $\textsf{Unit} \to \textsf{Unit}$ _______________________
    $\textsf{Void} \to \textsf{Void}$ _______________________
    $\textsf{Unit} \to \textsf{Void}$ _______________________
    $\textsf{Nat} \to \textsf{Bool}$ _______________________
    $\textsf{Bool} \to \textsf{Nat}$ _______________________
    $\textsf{Nat} \to \textsf{Nat}$ _______________________
    $\textsf{Bool} \to (\textsf{Bool} \to \textsf{Bool})$ _______________________
    $(\textsf{Bool} \to \textsf{Bool}) \to \textsf{Bool}$ _______________________
    $(\textsf{Nat} \to \textsf{Nat}) \to \textsf{Nat}$ _______________________
    $\textsf{Void} \to \textsf{Nat} \to \textsf{Bool}$ _______________________
  9. Here are the introduction rules for logical disjunction in propositional logic: $\frac{A}{A \lor B}$, $\frac{B}{A \lor B}$. Show the corresponding (Curry-Howard) typing rules in type theory.
  10. We learned that Set Theory is built on top of first-order logic, but that in Type Theory, logic emerges, since the logical operators can be defined in terms of typed functions. Show how to define the logical operators $\lor$, $\forall$, and $\exists$ as Type-theoretic functions $\textsf{or :Bool$\to$Bool$\to$Bool}$ and $\textsf{forall: ($t\to$Bool)$\to$Bool}$ and $\textsf{exists: ($t\to$Bool)$\to$Bool}$. You may assume that function equality is already defined.
  11. Complete the generative grammar for formulae in first-order predicate logic which is started below. You need only add the rule for Formula. Formulae should include truth, falsity, predicates applied to terms (remember $Lrj$—Romeo likes Juliet), negation, the four usual boolean connectives, and the quantified expressions. Require parentheses around all binary operators in order to avoid ambiguity—simpler than creating new syntactic categories to enforce precedence and associativity!

    $\begin{array}{lcl} \texttt{var} & \longrightarrow & \texttt{"p"} \mid \texttt{"q"} \mid \texttt{"r"} \mid \texttt{var "$'$"} \\ \texttt{constant} & \longrightarrow & \texttt{"a"} \mid \texttt{"b"} \mid \texttt{"c"} \mid \texttt{constant "$'$"} \\ \texttt{function} & \longrightarrow & \texttt{"f"} \mid \texttt{"g"} \mid \texttt{"h"} \mid \texttt{function "$'$"} \\ \texttt{predicate} & \longrightarrow & \texttt{"P"} \mid \texttt{"Q"} \mid \texttt{"R"} \mid \texttt{predicate "$'$"} \\ \texttt{Term} & \longrightarrow & \texttt{var} \mid \texttt{constant} \mid \texttt{function Term}^+ \mid \texttt{"(" Term ")"} \\ \end{array}$

  12. Explain, briefly, the difference between an entity and a value. To receive full credit you must define each term in 8 words or less, and give two examples of each. By examples we mean just the names of two things that are clearly values and names of two things that are clearly entities.
  13. Draw a picture of the value denoted by &(x: (1,2), y: &{type: "ok", set: "nope"})
  14. A grammar has the rule Exp -> Term ("+" Term)*. Which of the following best describes the + operator?
    • It is left associative
    • It is right associative
    • It is non-associative
    • Its associativity is indeterminate
  15. Draw the abstract syntax tree for the Astro program a = a ** 2 ** 1 + b - a; print a % (2 + 5.5);
  16. What is this natural semantics rule defining? $$ \dfrac{e_1,m \Longrightarrow a \;\;\;\; e_2,m \Longrightarrow b \;\;\;\; x\geq a \;\;\;\; x\lt b}{[\![e_1 \lozenge e_2]\!],m \Longrightarrow x}$$
    • Nothing, it is utter nonsense, $x$ is not defined
    • Nothing, there is a syntax error in the semantic rule
    • The diamond operator produces a random number between its left operand inclusive and its right operand exclusive
    • The static semantics of a TypeScript union type
    • The diamond operator is a modal operator meaning that $b$ is possible if $a$ is