Programming Language Theory Book

Chapter 2. Inductive definitions

Concepts

Journey Parent

On this page

Judgments
Inference rules
Derivations
Rule induction
Iterated and simultaneous inductive definition
Defining functions by rules
Exercises

Inductive definitions cannot be dispensed in the study of programming languages.

TLDR
- Basic framework of inductive definitions.
- Examples of inductive definitions.
- Inductive definition = A set of Rules for deriving Judgments/Assertions of a variety of forms.
  - Judgment: A statement about one or more Abstract binding tree (ABT)s of some Sort.
  - The rules specify necessary and sufficient conditions for the validity of a judgment. -> Fully determine its meaning.

Judgments

TLDR: Judgment/Assertion about an Abstract binding tree (ABT).
Many forms of judgments:
n natn is a natural numbern1+n2=nn is the sum of n1 and n2τ typeτ is a typee:τexpression e has type τe⇓vexpression e has value v
- Personal notes
  - The notation $e : τ$ is familiar.
  - $e ⇓ v$ is maybe similar to Big-step/Natural operational semantics.
  - $n_{1} + n_{2} = n$ is not a boolean (**Boolean Blindness**).
  - $n nat$ and $τ type$ have the same structure but totally different meaning.
Judgment: A statement that one or more Abstract binding tree (ABT)s have a property (unary relation) or stand in some relation to one another.
- The property/relation $\to$ Judgment form.
- The judgment that an object or objects have that property or stand in that relation $\to$ An Instance of an inference rule.
Judgment form = Predicate.
The objects constituting an instance are its subjects. $\to$ Judgment form instance's subject.
The Judgment asserting that a Judgment form $J$ holds of the Abstract binding tree (ABT) $a$ is written as $a J$ or $J a$ . $\to$ Instance of the judgment form.
A general Judgment form can be written as $J -$ or $- J$ .
When it is not important to stress the subject of the judgment, we write $J$ to stand for an unspecified judgment, that is, an instance of some judgment form.

Inference rules

An Inductive definition of a Judgment form consists of a collection of Rules of the form:
J1 J2 … JkJ
in which $J$ and $J_{1}$ , $J_{2}$ , $\dots$ , $J_{k}$ are all judgment of the form being defined.
- The judgments above the line: Premises.
- The judgment below the line: Conclusion.
- No Premise $\to$ Axiom.
  Otherwise, a Proper rule.
If all premises hold $\to$ The conclusion hold.
The reverse does not hold.
Example - Inductive definition of the judgment form $- nat$

\frac{}{zero nat}

\frac{a nat}{succ (a) nat}

Example - Inductive definition of the judgment form $- tree$

\frac{}{empty tree}

\frac{a tree}{node (a_{1}; a_{2}) tree}

Example - Inductive definition of the judgment form $- is -$

\frac{}{zero is zero}

\frac{a is b}{succ (a) is succ (b)}

$\Rightarrow$ A notational convention for specifying an infinite family of Rules by a finite number of patterns, or Rule schemes.

A collection of Rules is considered to define the strongest Judgment form that is closed under, or respects, those rules.
- Closed under the rules = The rules are sufficient to show the validity of a judgment: $J$ holds if there is a way to obtain it using the given rules.
- Strongest judgment form = The rules are also necessary: $J$ holds only if there is a way to obtain it by applying the rules.
  $\to$ The sufficiency of the rules means that we may show that $J$ holds by deriving it by composing rules.
  $\to$ Their necessity means that we may reason about it using rule induction.

Derivations

To prove an inductively defined Judgment, it's sufficient to show a Derivation of it.
Derivation of a Judgment: A finite composition of rules, starting with axioms and ending with that judgment.
$\to$ A Derivation of $J$ is evidence for the validity of an inductively defined judgment $J$ .
Derivations are visualized as trees with the conclusion at the bottom and with the children of a node corresponding to a rule appearing above it as evidence for the premises of that rule.
Formalization:
- An inference rule: $\frac{J_{1} \dots J_{k}}{J}$ .
- Derivations of its premises: $▽_{1}, \dots, ▽_{k}$ .
  $\to$ $\frac{▽_{1} \dots ▽_{k}}{J}$ is a derivation of $J$ .
Two main methods for finding derivations:
- Forward chaining/Bottom-up construction.
  Start with the axioms and work towards the desired conclusion.
  Idea: Forward chaining search maintains a set of derivable judgments and continually extends this set by adding to it the conclusion of any rules all of whose premises are in that set.
  Assume that all rules are considered at every stag:
  - Forward chaining would eventually find a derivation of any derivable judgment. $\to$ Complete.
  - Forward chaining cannot decide when to stop & conclude that a judgment is not derivable.
    $\to$ Need to understand the global properties of the rules.
    Do not take into account the end goal when deciding how to proceed at each step. $\to$ Undirected.
- Backward chaining/Top-down construction.
  Start with the desired conclusion and work backwards towards the axioms. $\to$ Goal-directed.
  1. Initialization: The process begins with a queue containing only the final goal (the judgment to be derived).
  2. The loop:
    - A goal is removed from the queue.
    - The system searches for rules where the conclusion matches that goal.
    - The premises of those matching rules are added to the queue as new sub-goals.
  3. Success: The process terminates successfully when the queue is empty (all goals and sub-goals are satisfied).
    Same issues as Forward chaining.

Rule induction

An Inductive definition specifies the strongest Judgment form closed under a collection of rules.
$\to$ We can reason about them using Rule induction.
The principle of Rule induction states that to show that a property a $a 𝒫$ holds whenever a $a J$ is Derivable, it is enough to show that $𝒫$ is closed under, or respects, the rules defining the judgment form $J$ .
More precisely, the property $𝒫$ respects the rule:
$\frac{a_{1} J \dots a_{k} J}{J}$
if $𝒫 (a)$ holds whenever $𝒫 (a_{1}), \dots, P (a_{k})$ do.
$\to$ The assumptions $𝒫 (a_{1}), \dots, P (a_{k})$ are called the Inductive hypothesis, and $𝒫 (a)$ is called the Inductive conclusion of the inference.
To show that $𝒫 a$ whenever $a nat$ , it's sufficient to show that:
- $𝒫 (zero)$ .
- For every $a$ , if $𝒫 (a)$ then $𝒫 (succ a)$ .
  $\to$ The principle of Mathematical induction.
To show that $𝒫 a$ whenever $a tree$ , it's sufficient to show that:
- $𝒫 (empty)$ .
- For every $a_{1}$ and $a_{2}$ , if $𝒫 (a_{1})$ and $𝒫 (a_{2})$ then $𝒫 (node (a_{1}; a_{2}))$ .
  $\to$ The principle of Tree induction.

Iterated and simultaneous inductive definition

Iterated inductive definition: One inductive definition builds on top of another.
$\to$ The premises of a rule $\frac{J_{1} \dots J_{k}}{J}$ may be instances of either a previously defined judgment form, or the judgment form being defined.
Example: The $- list$ Judgment form.
$\frac{}{nil list}$

\frac{a nat b list}{cons (a; b) list}

Simultaneous inductive definition: A set of rules for deriving instances of several different judgment forms, any of which may appear as the premise of any rule.
$\to$ Those judgment forms are defined at once.
Example: The $- even$ and $- odd$ Judgment forms.
$\frac{}{zero even}$

\frac{a even}{succ (a) odd}

\frac{a odd}{succ (a) even}

$\to$ To show simultaneously that $𝒫 (a)$ whenever $a even$ and $𝒬 (b)$ whenever $b$ odd, it is enough to show the following:

1. $𝒫 (zero)$ . 2. For every $a$ , if $𝒫 (a)$ then $𝒬 (succ (a))$ . 3. For every $a$ , if $𝒬 (a)$ then $𝒫 (succ (a))$ .

Defining functions by rules

Functions can be defined by:
1. Providing the definition of its graph relating inputs to outputs.
2. Then showing that the relation uniquely determines the outputs for given inputs.
Example: The function $sum (a; b; c)$ with the intended meaning of $c$ being the sum of $a$ and $b$ .
$\frac{b nat}{sum (zero; b; b)}$ $\frac{sum (a; b; c)}{sum (succ (a); b; succ (c))}$

Theorem. For every $a nat$ and $b nat$ , there exists a unique $c nat$ such that $sum (a; b; c)$ .

Proof

Two parts:

Existence: If $a nat$ and $b nat$ , then there exists $c nat$ such that $sum (a; b; c)$ .
Uniqueness: If $sum (a; b; c)$ , and $sum (a; b; c^{'})$ , then $c$ is $c^{'}$ .

Exercises

Exercise 2.1

Problem statement. Give an inductive definition of the judgment $max (m; n; p)$ , where $m nat$ , $n nat$ , and $p nat$ , with the meaning that $p$ is the larger of $m$ and $n$ . Prove that every $m$ and $n$ are related to a unique $p$ by this judgment.

Solution

Definition

\frac{n nat}{\max (zero; n; n)} (1)

\frac{n nat}{\max (n; zero; n)} (2)

\frac{\max (m; n; p)}{\max (succ (m); succ (n); succ (p))} (3)

The judgment defines a function on $m$ and $n$
- Existence $(*)$ : For every $m nat$ and $n nat$ , there exists a $p$ such that $\max (m; n; p)$ .
  - If $m = zero$ or $n = zero$ , applying $(1)$ or $(2)$ suffices to show $(*)$ holds in these cases.
  - If $m = succ (m^{'})$ and $n = succ (n^{'})$ , then with $(3)$ , it's sufficient to show that $(*)$ holds in the case $m = m^{'}$ and $n = n^{'}$ . By the induction hypothesis, this is trivial.
- Uniqueness $(* *)$ : For every $m nat$ and $n nat$ , if there exists $p$ and $p^{'}$ such that $\max (m; n; p)$ and $\max (m; n; p^{'})$ , then $p = p^{'}$ .
  - If $m = zero$ or $n = zero$ , applying $(1)$ or $(2)$ is the only way to obtain such a $p$ . Therefore, $(* *)$ holds in these cases.
  - If $m = succ (m^{'})$ and $n = succ (n^{'})$ , then applying $(3)$ for the case $m = m^{'}$ and $n = n^{'}$ is the only way to obtain such a $p$ . By the induction hypothesis, this is trivial.

Exercise 2.2

Problem statement. Consider the following rules, which define the judgment $hgt (t; n)$ stating that the binary tree $t$ has height $n$ .

hgt (empty; zero)

\frac{hgt (t_{1}; n_{1}) hgt (t_{2}; n_{2}) \max (n_{1}; n_{2}; n)}{hgt (node (t_{1}; t_{2}); succ (n))}

Prove that the judgment $hgt$ defines a function from trees to natural numbers.

Solution

Existence $(*)$ : For every $t tree$ , there exists $h$ such that $hgt (t; h)$ .
For $t = empty$ , this is trivial that $n = zero$ , so $(*)$ holds.
For $t = node (t_{1}; t_{2})$ such that $t_{1} tree$ and $t_{2} tree$ .

By the induction hypothesis, there exists $n_{1} nat$ and $n_{2} nat$ such that $hgt (t_{1}; n_{1})$ and $hgt (t_{2}; n_{2})$ .

By Exercise 2.1, there exists $n nat$ such that $\max (n_{1}; n_{2}; n)$ .

By definition, $hgt (t; succ (n))$ .

Uniqueness $(* *)$ : For every $t tree$ , if $hgt (t; h)$ and $hgt (t; h^{'})$ , then $h = h^{'}$ .

Similar to $(*)$ .

Exercise 2.3

Problem statement. Given an inductive definition of ordered variadic trees whose nodes have a finite, but variable, number of children with a specified left-to-right ordering among them. Your solution should consist of a simultaneous definition of two judgments:

$t tree$ , stating that $t$ is a variadic tree.
$f forest$ , stating that $f$ is a "forest" (finite sequence) of variadic trees.

Solution

\frac{}{empty tree}

\frac{}{nil forest}

\frac{t tree f forest}{cons (t; f) forest}

\frac{f forest}{node (f) tree}

Exercise 2.4

Problem statement. Give an inductive definition of the height of a variadic tree of the kind defined in Exercise 2.3.

Your definition should make use of an auxiliary judgment defining the height of a forest of variadic trees.
It will be defined simultaneously with the height of a variadic tree.

Show that the two judgments so defined each define a function.

Solution (incomplete)

Definition

\frac{}{tree_hgt (empty; zero)}

\frac{}{forest_hgt (nil; zero)}

\frac{tree_hgt (t; n) forest_hgt (f; m)}{forest_hgt (cons (t; f); \max (n; m))}

\frac{forest_hgt (f; n)}{tree_hgt (node (f); succ (n))}

Exercise 2.5

Problem statement. Give an inductive definition of the binary natural numbers, which are either:

Zero
Twice a binary number
One more than twice a binary number

The size of such a representation is logarithmic, rather than linear, in the natural number it represents.

Solution

\frac{}{zero bin}

\frac{b bin}{twice (b) bin}

\frac{b bin}{twice_plus_one (b) bin}

Exercise 2.6

Problem statement. Give an inductive definition of addition of binary natural numbers as defined in Exercise 2.5.

Hint: Proceed by analyzing both arguments to the addition, and make use of an auxiliary function to compute the successor of a binary number.
Hint: Alternatively, define both the sum and the sum-plus-one of two binary numbers mutually recursively.

Solution (incomplete)

Definition

\frac{sum (b_{1}; b_{2}; b_{3})}{sum (b_{2}; b_{1}; b_{3})}

\frac{sum_plus_one (b_{1}; b_{2}; b_{3})}{sum_plus_one (b_{2}; b_{1}; b_{3})}

\frac{}{sum (zero; zero; zero)}

\frac{}{sum_plus_one (zero; zero; twice_plus_one (zero))}

\frac{sum (b_{1}; b_{2}; b_{3})}{sum (twice (b_{1}); twice (b_{2}); twice (b_{3}))}

\frac{sum (b_{1}; b_{2}; b_{3})}{sum (twice_plus_one (b_{1}); twice (b_{2}); twice_plus_one (b_{3}))}

\frac{sum_plus_one (b_{1}; b_{2}; b_{3})}{sum (twice_plus_one (b_{2}); twice_plus_one (b_{1}); twice (b_{3}))}

\frac{sum_plus_one (b_{1}; b_{2}; b_{3})}{sum_plus_one (twice_plus_one (b_{1}); twice (b_{2}); twice (b_{3}))}

\frac{sum (b_{1}; b_{2}; b_{3})}{sum_plus_one (twice (b_{1}); twice (b_{2}); twice_plus_one (b_{3}))}

\frac{sum_plus_one (b_{1}; b_{2}; b_{3})}{sum_plus_one (twice_plus_one (b_{1}); twice_plus_one (b_{2}); twice_plus_one (b_{3}))}

Chapter 2. Inductive definitions

Judgments ​

Inference rules ​

Derivations ​

Rule induction ​

Iterated and simultaneous inductive definition ​

Defining functions by rules ​

Exercises ​

Exercise 2.1 ​

Exercise 2.2 ​

Exercise 2.3 ​

Exercise 2.4 ​

Exercise 2.5 ​

Exercise 2.6 ​

Judgments

Inference rules

Derivations

Rule induction

Iterated and simultaneous inductive definition

Defining functions by rules

Exercises

Exercise 2.1

Exercise 2.2

Exercise 2.3

Exercise 2.4

Exercise 2.5

Exercise 2.6