defined class Nat
Meeting 10 - Judgments
\[ \newcommand\TirName[1]{\text{\small #1}} \newcommand\inferrule[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand\infer[3]{\inferrule{#1}{#2}{#3}} \]
What questions does your neighbor have?
In-Class Slides
In-Class Jupyter
Book Chapter
Announcements
- Lab 2 due next Monday (9/30) 6pm
Today
- Judgments
- Triage Your Questions
Questions?
Review: Type Judgments
\[ e: \tau \]
- How do we read this?
- A judgment is a statement about syntactic objects
- This is a judgment form for type checking
Inference rules
- We define judgment forms inductively using a set of inference rules:
\[ \inferrule{}{ J_1 \and J_2 \and \cdots \and J_n }{ J } \]
- If we can show \(J_1, J_2, ... J_i\), then \(J\) holds, i.e. we can derive \(J\) - the conclusion
Example - Syntax of natural numbers
\[ \fbox{$n \in \textbf{Nat}$} \] \[ \inferrule{Zero}{ }{ \mathsf{z} \in \textbf{Nat} } \] \[ \inferrule{Successor}{ n \in \textbf{Nat} }{ \mathsf{s}(n) \in \textbf{Nat} } \]
- What is the judgment form?
- How do we read the two inference rules?
- This can also be represented as a grammar for nats: \[ \begin{array}{rrrrl} \text{natural numbers} & \textbf{Nat} & n & \mathrel{::=}& \mathsf{z} \mid\mathsf{s}(n) \end{array} \]
Let’s code it
defined function isNat
- This is the characteristic function of the set \(\textbf{Nat}\)
- Notice the correspondence between the mathematical specification and the implementation
Derivations
- A judgment holds if and only if we can compose applications of the inference rules to demonstrate it
\[ \mathsf{s}(\mathsf{s}(\mathsf{z})) \]
- this can be represented in code, as each judgment corresponds to a function call
defined function isNatDerivation
Structural Equality
\[ \fbox{$n_1 \mathsf{=_{\textbf{Nat}}} n_2$} \]
defined function eqNat
Semantics
- What if we want to turn our syntactical evaluation of \(\textbf{Nat}\)s into a semantical evaluation by deriving what integer value a \(\textbf{Nat}\) holds?
- What is our judgment form?
\[ \fbox{$n \Downarrow i$} \]
\[ \] \[ \]
- What does \(\mathsf{z}\) evaluate to?
- For our successor inference rule: given ??? as a premise, what does ??? evaluate to?
defined function eval
Let’s try lists
- Inductively define with judgments and inference rules
\[ \fbox{$l : \textbf{List}$} \] \[ \inferrule{Nil}{ }{ \mathsf{Nil} : \textbf{List} } \] \[ \inferrule{Successor}{ tail : \textbf{List} }{ \mathsf{Cons}(head, tail) : \textbf{List} } \]
\[ \fbox{$l : \textbf{IntList}$} \] \[ \inferrule{Nil}{ }{ \mathsf{Nil} : \textbf{IntList} } \] \[ \inferrule{Successor}{ head : \textbf{Int} \ \ \ \ \ \ \ \ tail : \textbf{IntList} }{ \mathsf{Cons}(head, tail) : \textbf{IntList} } \]
defined class MyIntList
defined function isMyIntList
List equality
defined function eqMyIntList