Meeting 10 - Judgments

Dakota Bryan

Thursday, September 26, 2024

\(\newcommand{\TirName}[1]{\text{#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}} \)

\[ \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}} \]

Meeting 10 - Judgments

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 class Nat

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