15 Judgments

$\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}} $

A judgment is a statement about syntactic objects, that is, asserts a relation on a set of objects. The form of the relation itself is often called a judgment form. Judgments are used pervasively in describing programming languages.

We have previously seen judgment forms, for example, relating an expression and a type: \[ e: \tau \] that is read “expression $e$ has type $\tau$.” This relation takes two parameters: an expression $e$ and a type $\tau$. The colon $:$ is simply punctuation. For readability, it is common for judgment forms to use a mix of punctuation symbols. As parameters are meta-variables for syntactic objects, they are typically written in italic font (e.g., $e$ and $\tau$).

Judgment forms are defined inductively using a set of inference rules. An inference rule takes the following form:

$\inferrule{ J_1 \and J_2 \and \cdots \and J_n }{ J }$

where the meta-variable $J$ stands for a judgment. The judgments above the horizontal line are the premises, while the judgment below the line is the conclusion. An inference rule states that if the premises can be shown to hold, then the conclusion also holds (i.e., the premises are sufficient to derive the conclusion). The set of premises may be empty, and such an inference rule is called an axiom.

15.1 Grammars and Inference Rules

15.1.1 Example: Syntax

Recall from that a grammar defines inductively a set of syntactic objects. For example, we can describe the natural numbers using a unary notation. We give an explicit name to the set of syntactic objects describing natural numbers (i.e., we call the language of natural numbers here $\mathbf{Nat}$).

\[ \begin{array}{rrrrl} \text{natural numbers} & \mathbf{Nat}& n & \mathrel{::=}& \mathsf{z}\mid\mathsf{s}(n) \end{array} \tag{15.1}\]

We now define the language of natural numbers using judgments and inference rules. Let $n \in \mathbf{Nat}$ be the (unary) judgment form that says, “Syntactic object $n$ is an element of the set we call $\mathbf{Nat}$.”

$\fbox{$n \in \mathbf{Nat}$}$

$\inferrule[Zero]{ }{ \mathsf{z}\in \mathbf{Nat} }$

$\inferrule[Successor]{ n \in \mathbf{Nat} }{ \mathsf{s}(n) \in \mathbf{Nat} }$

Figure 15.1: Defining the judgment form $n \in \mathbf{Nat}$ that says, “Syntactic object $n$ is an element of the set we call $\mathbf{Nat}$.”

We define the judgment form $n \in \mathbf{Nat}$ with two inference rules named $\TirName{Zero}$ and $\TirName{Successor}$. Rule $\TirName{Zero}$ is an axiom that says that $\mathsf{z}$ is an element of the set we call $\mathbf{Nat}$. Rule $\TirName{Successor}$ says that $\mathsf{s}(n)$ is an element in the set we call $\mathbf{Nat}$ if $n$ is an element in the set we call $\mathbf{Nat}$. The italicized if in the previous sentence corresponds to the horizontal line of the inference rule. As a convention, we list the judgment form we are defining with a set of inference rules as a header in a box.

In Section 12.1, we see a grammar as an inductive data type. For example, we might translate the above grammar (Equation 15.1) into the following inductive data type in Scala:

sealed abstract class Nat
case object Z extends Nat
case class S(n: Nat) extends Nat

defined class Nat
defined object Z
defined class S

We can see the inference rules defining the judgment form $n \in \mathbf{Nat}$ (Figure 15.1) as defining the same thing as the grammar (Equation 15.1) — an inductively-defined set $\mathbf{Nat}$. However, we can also see the inference rules as defining a unary relation that judges when a $n$ is the set named $\mathbf{Nat}$, which we might translate into the following function in Scala:

def isNat(n: Nat): Boolean = n match {
  // Zero
  case Z => true
  // Successor
  case S(n) => isNat(n)
}

isNat(Z)
isNat(S(Z))
isNat(S(S(Z)))

defined function isNat
res1_1: Boolean = true
res1_2: Boolean = true
res1_3: Boolean = true

Of course, this function is a silly one to write, as it will always return true. That is, we have this trivial meta-theorem:

Proposition 15.1 (All $n$s are elements of the set we call $\mathbf{Nat}$) For all $n$, $n \in \mathbf{Nat}$.

A standard shorthand is that when we write a judgment “$n \in \mathbf{Nat}$” in this context, we mean, “the judgment $n \in \mathbf{Nat}$ holds.”

The isNat function is called the characteristic function of the set $\mathbf{Nat}$.

With this trivial meta-theorem, we see grammars and this form of inference rules interchangeable for defining syntax. However, as inference rules are a more general form of inductive definitions (in that they are $n$-ary relations), we generally use grammars to define syntax and instead use inference rules to define semantics.

15.1.2 Key Intuition

While the function isNat function is silly, we see that the meta-language of judgment forms, inference rules, and judgments in mathematical specification corresponds to function signatures, function bodies, and function calls in code. Just like the that the meta-language of meta-variables, grammars, and terms corresponds to types, inductive data type definitions, and values.

15.2 Derivations of Judgments

A set of inference rules defines a judgment as the least relation closed under the rules. This statement means a judgment holds if and only if we can compose applications of the inference rules to demonstrate it. Such a demonstration is called a derivation of a judgment or sometimes simply a derivation. A derivation is a tree where each node in the tree is an application of an inference rule and whose children are derivations of the rule’s premises. The leaves of a derivation tree are applications of axioms.

For example, to demonstrate that the judgment $\mathsf{s}(\mathsf{s}(\mathsf{z})) \in \mathbf{Nat}$ holds, we give the following the derivation:

\[ \begin{prooftree} \AxiomC{} \RightLabel{$\TirName{Zero}$} \UnaryInfC{$\mathsf{z}\in \mathbf{Nat}$} \RightLabel{$\TirName{Successor}$} \UnaryInfC{$\mathsf{s}(\mathsf{z}) \in \mathbf{Nat}$} \RightLabel{$\TirName{Successor}$} \UnaryInfC{$\mathsf{s}(\mathsf{s}(\mathsf{z})) \in \mathbf{Nat}$} \end{prooftree} \]

We write the rule that is applied to the right of the horizontal line.

Note the same term derivation is also used in the context of a parsing derivation that witnesses when a given string is a sentence in a given grammar (cf. Section 11.2.1). Observe that in both cases, the term derivation refers to witnessing an instance of an inductive definition.

Given that the meta-language of judgment forms, inference rules, and judgments in mathematical specification corresponds to function signatures, function bodies, and function calls in code, the notion of derivations of a judgment corresponds to the execution of a function call.

We instrument isNat to show the correspondence between the derivation of the judgment $n \in \mathbf{Nat}$ and an execution trace of isNat(n) of some test cases for n, specifically Z, S(Z), and S(S(Z)).

def isNat(n: Nat): Boolean = {
  val r = n match {
    // Zero
    case Z => {
      val r = true
      println("------------- Zero")
      r
    }
    // Successor
    case S(n) => {
      val r = isNat(n)
      println("------------- Successor")
      r
    }
  }
  println(s"$n ϵ Nat")
  r
}

defined function isNat

isNat(Z)

------------- Zero
Z ϵ Nat

res3: Boolean = true

isNat(S(Z))

------------- Zero
Z ϵ Nat
------------- Successor
S(Z) ϵ Nat

res4: Boolean = true

isNat(S(S(Z)))

------------- Zero
Z ϵ Nat
------------- Successor
S(Z) ϵ Nat
------------- Successor
S(S(Z)) ϵ Nat

res5: Boolean = true

15.3 Inductively-Defined

15.3.1 Example: Structural Equality

As another example, let us define when two natural numbers $n_1, n_2$ are structurally equal. That is, we define the judgment form $n_1 =_{\mathbf{Nat}}n_2$ that we intend to mean, “Natural number $n_1$ is structurally equal to natural number $n_2$.” as the least relation closed under the inference rules specified in Figure 15.2.

$\fbox{$n_1 =_{\mathbf{Nat}}n_2$}$

$\inferrule[ZeroEq]{ \phantom{n_1 =_{\mathbf{Nat}}n_2} }{ \mathsf{z}=_{\mathbf{Nat}}\mathsf{z} }$

$\inferrule[SuccessorEq]{ n_1 =_{\mathbf{Nat}}n_2 }{ \mathsf{s}(n_1) =_{\mathbf{Nat}}\mathsf{s}(n_2) }$

Figure 15.2: Defining structural equality on natural numbers $n$. The judgment form $n_1 =_{\mathbf{Nat}}n_2$ says, “Natural number $n_1$ is structurally equal to natural number $n_2$.”

What it means to be the least relation is that we read the inference rules inductively. Intuitively, this means that a judgment holds if and only if there is a derivation for it.

def eqNat(n1: Nat, n2: Nat): Boolean = {
  val r = (n1, n2) match {
    // ZeroEq
    case (Z, Z) => {
      println("----------------------- ZeroEq")
      true
    }
    // SuccessorEq
    case (S(n1), S(n2)) => {
      val r = eqNat(n1, n2)
      println("----------------------- SuccessorEq")
      r
    }
    // No Rules
    case _ => false
  }
  println(s"$n1 =Nat $n2")
  r
}

defined function eqNat

We see using the instrumented function eqNat corresponding to the judgment form $n_1 =_{\mathbf{Nat}}n_2$ that we get complete derivations (i.e., end in applications of axioms) for the judgments $\mathsf{z}=_{\mathbf{Nat}}\mathsf{z}$ and $\mathsf{s}(\mathsf{z}) =_{\mathbf{Nat}}\mathsf{s}(\mathsf{z})$ that should hold:

eqNat(Z, Z)

----------------------- ZeroEq
Z =Nat Z

res7: Boolean = true

eqNat(S(Z), S(Z))

----------------------- ZeroEq
Z =Nat Z
----------------------- SuccessorEq
S(Z) =Nat S(Z)

res8: Boolean = true

And we cannot complete the derivation for the judgment $\mathsf{s}(\mathsf{s}(\mathsf{z})) =_{\mathbf{Nat}}\mathsf{s}(\mathsf{s}(\mathsf{s}(\mathsf{z})))$ that should not hold:

eqNat(S(S(Z)), S(S(S(Z))))

Z =Nat S(Z)
----------------------- SuccessorEq
S(Z) =Nat S(S(Z))
----------------------- SuccessorEq
S(S(Z)) =Nat S(S(S(Z)))

res9: Boolean = false

15.4 Functions versus Relations

Mathematically, judgment forms are inductively-defined relations. Thus far, when we translate them to functional programs, we have translated them into their characteristic functions (i.e., has return type Boolean). In some cases, the relations we define judgmentally are more naturally read as functions. And as such, we want to translate them to functions in Scala.

15.4.1 Example: Semantics

Let us write $i$ as the meta-variable for a mathematical integer (i.e., $\mathbb{Z}$). In particular, we do not define syntax for $i$. We define an interpretation of syntactic natural numbers $n$ into integers $i$ with the judgment form $n \Downarrow i$, which we read as, “Natural number $n$ evaluates to integer $i$.”

$\fbox{$n \Downarrow i$}$

$\inferrule[EvalZero]{ \phantom{\Downarrow} }{ \mathsf{z}\Downarrow 0 }$

$\inferrule[EvalSuccessor]{ n \Downarrow i }{ \mathsf{s}(n) \Downarrow i + 1 }$

Figure 15.3: Defining structural equality on natural numbers $n$. The judgment form $n_1 =_{\mathbf{Nat}}n_2$ says, “Natural number $n_1$ is structurally equal to natural number $n_2$.”

In defining a Scala implementation, let us choose the Scala type Int to represent $i$. Then, we see the judgment form $n \Downarrow i$ defines an eval function with which we are already familiar:

def eval(n: Nat): Int = {
  val i = n match {
    case Z => {
      println("------------ EvalZero")
      0
    }
    case S(n) => {
      val i = eval(n)
      println("------------ EvalSuccessor")
      i + 1
    }
  }
  println(s"$n ⇓ $i")
  i
}

defined function eval

eval(Z)

------------ EvalZero
Z ⇓ 0

res11: Int = 0

eval(S(Z))

------------ EvalZero
Z ⇓ 0
------------ EvalSuccessor
S(Z) ⇓ 1

res12: Int = 1

eval(S(S(Z)))

------------ EvalZero
Z ⇓ 0
------------ EvalSuccessor
S(Z) ⇓ 1
------------ EvalSuccessor
S(S(Z)) ⇓ 2

res13: Int = 2

We are able to translate the judgment form $n \Downarrow i$ into the eval function in Scala because we can show that it indeed defines a function:

Proposition 15.2 (Deterministic Evaluation) If $n \Downarrow i_1$ and $n \Downarrow i_2$, then $i_1 = i_2$.