Types and Programming Languages | Definition Styles

We will use the untyped arithmetic expression as example.

BNF Definition

One way to describe our grammar is using BNF. Parentheses are not mentioned in the grammar of terms, which defines only their abstract syntax.

t ::= true
      false
      if t then t else t
      0
      succ t
      pred t
      iszero t

The symbol t in the right-hand sides of the rules of this grammar is called a metavariable. It is a place-holder for some particular term.

- "meta" means that it is not a variable of the object language - the language whose syntax we are currently describing but rather of the metalanguage - the notation in which the description is given.

Definition: The term metatheory means the collection of true statements that we can make about some particular logical system (or programming language) and, by extension, the study of such statements.

Inductive Definition

The set of terms is the smallest set $T$ such that

{

true, false, 0

} \subseteq T

- if

t_{1} \in T

then

succ t_{1}, pred t_{1}, iszero t_{1} \subseteq T

- if

t_{1} \in T, t_{2} \in T

and

t_{3} \in T

then

if t_{1} then t_{2} else t_{3} \in T

This can also be written as the natural deduction style:

t r u e \in T f a l se \in T 0 \in T \frac{t _{1} \in T}{succ t _{1} \in T} \frac{t _{1} \in T}{pred t _{1} \in T} \frac{t _{1} \in T}{iszero t _{1} \in T} \frac{t _{1} \in T t _{2} \in T t _{3} \in T}{if t _{1} then t _{2} else t _{3} \in T}

Each rule is read "If we have established the statements in the premise(s) listed above the line, then we may derive the conclusion below the line."
Rules with no premises (like the first three above) are often called axioms.

To be completely pedantic, what we are calling inference rules are actually rule schemas, since their premises and conclusions may include metavariables.

- for example, you can replace the metavariable

t_{1}

by all phrases from the appropriate syntactic category

Like the BNF grammar, this definition says nothing about the use of parentheses to mark compound subterms. Formally, what's really going on is that we are defining $T$ as a set of trees.

Concrete Definition

For each natural number $i$ , define a set $S_{i}$ as follows:

S_{0} = S_{i + 1} = ϕ {t r u e, f a l se, 0} \cup {succ t_{1}, pred t_{1}, iszero t_{1} ∣ t_{1} \in S_{i}} \cup {if t_{1} then t_{2} else t_{3} ∣ t_{1}, t_{2}, t_{3} \in S_{i}}

Finally, let $S = ⋃_{i} S_{i}$

Equivalence between Inductive Definition and Concrete Definition

Use $T$ to represent the one defined by inductive definition and $S$ to represent the one defined by concrete definition.

$T$ was defined as the smallest set satisfying certain conditions. so our proof consists of two pars:

$S$ satisfies these conditions

the constants are trivial
if $t \in S$ then $\exists i, s . t . t \in S_{i}$ , then by definition of $S_{i + 1}$ , we have $succ t \in S_{i + 1} \subseteq S$ , similarly, we see that $pred t \in S_{i + 1} \subseteq S$ and $iszero t \in S_{i + 1} \subseteq S$
if $t_{1} \in T, t_{2} \in T$ and $t_{3} \in T$ , similarly $if t_{1} then t_{2} else t_{3} \in S i + 1 \subseteq S$

$S$ is the smallest set, in other words, any set satisfying the conditions has $S$ as a subset

suppose that some set $S^{'}$ satisfies the conditions, we will argue by complete induction on $i$ , that every $S_{i} \subseteq S^{'}$ , from which it clearly follows $S \subseteq S^{'}$

Suppose that $S_{j} \subseteq S^{'}$ for all $j < i$ , we are to show that $S_{i} \subseteq S^{'}$ . By the definition of $S_{i}$ , there are two cases to consider

$i = 0$ : it's trivial
$i > 0$ : $\exists j, s . t . i = j + 1$ . Since $S_{j + 1}$ is defined as the union of three smaller sets, an element $t \in S_{j + 1}$ must come from one of these sets:
- if $t$ is constant, then it's trivial $t \in S^{'}$
- if $t$ has the form $succ t_{1}$ for some $t_{1} S_{j}$ , then by the induction hypothesis, $t_{1} \in S^{'}$ and by condition (2) $t \in S^{'}$
- if $t$ has the form $if t_{1} then t_{2} else t_{3}$ , for the same reason in (ii), $t \in S^{'}$

Thus, we have shown that each $S_{i} \subseteq S^{'}$ . By the definition of S as the union of all the $S_{i}$ , this gives $S \subseteq S^{'}$ , completing the argument.