Chapter 3 untyped arithmetic expressions

Summary of desirable properties for a system ​

• Determinacy of the single-step evaluation relation.

  Should hold for all systems.

• Uniqueness of normal-forms.

  Should hold for all systems.

• Values are normal forms.

  Should hold for all systems.

• Normal forms are values.

  May not hold for all systems.

• Termination of evaluation.

  May not hold for all systems.

Introduction ​

The convention used is similar to the standard BNF [cf. Aho, Sethi, and Ullman, 1986].

t  ::=          terms:
       true         constant true
       false        constant false
       if t then t else t   conditional
       0            constant zero
       succ t       successor
       pred t       predecessor
       iszero t     zero test

A simple untyped expression language - Untyped calculus of booleans and numbers

• Syntactically, this language comprises of:

  • The boolean constants true and false.
  • Conditional expressions (if expression).
  • The numeric constant 0.
  • The arithmetic operators succ (successor) and pred (predecessor).
  • A testing operation iszero that returns true when it is applied to 0, and false when it is applied to some other number.

• Abstract syntax notation

  • Term definition ($\text{t} ::= \ldots$): The notation $\text{t} ::=$ declares the set of terms, with the letter $\text{t}$ (and variants like $\text{s}, \text{u}, \text{t}_1$) used as a metavariable to range over terms.

  • Metavariable: $\text{t}$ is a placeholder for a particular term of the object language, but belongs to the metalanguage (the language used for description).

    • This concept is borrowed from meta-mathematics, giving rise to the term metatheory (the formal study of a logical system's properties).

    • The prefix meta- comes from meta-mathematics, the subfield of logic whose subject matter is the mathematical properties of systems for mathematical and logical reasoning.

    • Metatheory: 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.

      -> Phrases like "metatheory of subtyping" can be understood as "the formal study of the properties of systems with subtyping".

  • A program is simply a term built from the forms defined in the grammar.

  • The symbol $\to$ is used to display the result of evaluating an example term.

    • Example: if false then 0 else 1 $\to$ 1.

  • Terms vs expressions:

    • Currently, term and expression are interchangeable.

    • Starting in Chapter 8:

      • Expression will be used for all syntactic phrases (terms, types, kinds). For calculi with additional syntactic categories such as types, expression is used for all sorts of syntactic phrases (including term expressions, type expressions, kind expressions, etc.)
      • Term will be reserved for phrases representing computations (i.e., phrases that can substitute for $\text{t}$).

  • Values:

    • The results of evaluation are terms of a simple form: boolean constants or numbers (nested succ applications to 0).
    • Values play a special role in formalizing evaluation order.

  • Abstract vs concrete syntax: Parentheses (e.g., in iszero(pred(succ 0))) are used for readability but are not part of the grammar's abstract syntax, which is currently unambiguous.

  • "Nonsensical" terms:

    • The syntax permits terms that are semantically dubious (e.g., succ true or if 0 then 0 else 0).
    • These terms are what make the simple language interesting, as the goal of the type system is precisely to exclude such ill-formed programs.

Syntax ​

• There are more than one way to describe a syntax of a language.

  • The BNF notation above.

  • Inductive definition (more verbose).

    The set of terms ($\mathcal{T}$) is the smallest set such that:

    1. $\{\text{true}, \text{false}, 0\} \subseteq \mathcal{T}$.
    2. If $\text{t}_1 \in \mathcal{T}$, then $\{\text{succ } \text{t}_1, \text{pred } \text{t}_1, \text{iszero } \text{t}_1\} \subseteq \mathcal{T}$ .
    3. If $\text{t}_1 \in \mathcal{T}, \text{ t}_2 \in \mathcal{T}, \text{ and } \text{t}_3 \in \mathcal{T}$, then $\text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \in \mathcal{T}$.

    • Structure of the definition

      • Clause 1 specifies base elements (true, false, 0).
      • Clause 2 specifies rules for building compound expressions (succ t1, if t1 then t2 else t3, etc.) from existing terms.
      • "Smallest set": This crucial phrase ensures that T contains no elements other than those absolutely required by the construction rules in the preceding clauses.

    • Formally, the definition defines T as a set of trees, not a set of linear strings.

    • The use of parentheses in written examples (the linear form) serves merely to clarify the underlying tree structure (the abstract syntax) of compound subterms.

  • 2-dimensional inference rule format.

    • A different shorthand for the same inductive definition of terms.

    • Commonly used in "natural deduction style" presentations of logical systems.

    • 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."

    • The fact that $T$ is the smallest set satisfying these rules is often (as here) not stated explicitly.

    • Inference rule (generic term): The term inference rule is used generically throughout the book to refer to any rule in the system, including both axioms and rules with one or more premises.

    • Axioms: Rules with no premises (like the first three base cases for true, false, and 0). They are often written without the horizontal bar.

    • Rule schemas (formal terminology): What are called "inference rules" are technically rule schemas because their premises and conclusions contain metavariables (t1, t2, etc.).

      • Each schema formally represents an infinite set of concrete rules that are obtained by consistently replacing the metavariables with all possible phrases from the appropriate syntactic category (e.g., replacing t with every possible term).

  • Concrete generator notation.

    • More "concrete" style that gives an explicit procedure for generating the elements of $T$.

Exercise 3.2.4 ​

Task: How many elements does $S_3$ have?

Exercise 3.2.5 ​

Task. Show that the sets $S_i$ are cumulative-that is, that for each $i$ we have $S_i \subseteq S_{i+1}$.

Induction on terms ​

• The explicit characterization of the set of terms $S$ in Proposition 3.2.6 justifies an important principle for reasoning about its elements based on its structure.

  If $t \in T$, then one of three things must be true about $t$:

  1. $t$ is a constant.

  2. $t$ has the form $\text{succ } t_1$, $\text{pred } t_1$, or $\text{isZero } t_1$ for some smaller term $t_1$.

  3. $t$ has the form $\text{if } t_1 \text{ then } t_2 \text{ else } t_3$ for some smaller terms $t_1, t_2$, and $t_3$.

     -> This observation can be applied in 2 ways:

  • Inductive definitions of functions can be given over the set of terms.
  • Inductive proofs of properties of terms can be given.

-> Structural induction.

$\text{Consts}(t)$ ​

The set of constants appearing in a term $t$, written $\text{Consts}(t)$, is defined as follows:

$\text{size}(t)$ ​

The size of a term $t$, written $\text{size}(t)$, is defined as follows:

That is, the size of $t$ is the number of nodes in its abstract syntax tree.

$\text{depth}(t)$ ​

The depth of a term $t$, written $\text{depth}(t)$, is defined as follows:

Equivalently, $\text{depth}(t)$ is the smallest $i$ such that $t \in S_i$, according to Definition 3.2.3.

Lemma: The number of distinct constants ​

Statement. The number of distinct constants in a term $t$ is no greater than the size of $t$ (i.e., $| \text{Consts}(t) | \le \text{size}(t)$).

General reasoning principle - Generalization of the previous lemma's proof structure ​

• Theorem [Principles of induction on terms]: Suppose $P$ is a predicate on terms.

  Induction on depth:

  If, for each term $s$, given $P(r)$ for all $r$ such that $depth(r) < depth(s)$, we can show $P(s)$, then $P(s)$ holds for all $s$.

  Induction on size:

  If, for each term $s$, given $P(r)$ for all $r$ such that $size(r) < size(s)$, we can show $P(s)$, then $P(s)$ holds for all $s$.

  Structural induction:

  If, for each term $s$, given $P(r)$ for all immediate subterms $r$ of $s$ we can show $P(s)$, then $P(s)$ holds for all $s$.

Semantic styles ​

• How to formulate the semantics of a language precisely?

• Three basic approaches to semantics formalization:

  • Operational semantics

    • Idea: Define a simple abstract machine for the language.

    • Abstract: The machine directly ses the terms of the language as its machine code.

    • State of the machine: For simple languages, it's just a term.

    • Transition function: Describe the machine's behavior - for each state, either:

      • Gives the next state by performing a step of simplification on the term.
      • Declares that the machine has halted.

    • The meaning of a term $t$ can be taken to be the final state that the machine reaches when started with $t$ as its initial state.

    • It is sometimes useful to give two or more different operational semantics for a single language:

      • Some more abstract, with machine states that look similar to the terms that the programmer writes.

      • Others closer to the structures manipulated by an actual interpreter or compiler for the language.

        -> Proving that the behaviors of these different machines correspond in some suitable sense when executing the same program amounts to proving the correctness of an implementation of the language.

  • Denotational semantics

    • More abstract.

    • The meaning of a term: Some mathematical object (number/function) rather than a sequence of machine states.

    • Giving denotational semantics for a language:

      1. Find a collection of semantic domains.

      2. Define an interpretation function mappings terms into elements of these domains.

         -> Domain theory: Facilitate the search for appropriate semantic domains for modeling various language features.

    • Major advantages of denotational semantics:

      • Abstracts from the gritty details of evaluation.

      • Highlights the essential concepts of the language.

      • The properties of the chosen collection of semantic domains can be used to derive powerful laws for reasoning about program behaviors.

        • Laws for proving that two programs have exactly the same behavior.
        • Laws for that a program's behavior satisfies some specification.

      • From the properties of the chosen collection of semantic domains, it is often immediately evident that various (desirable or undesirable) things are impossible in a language.

  • Axiomatic semantics

    • Idea: Define a language by its proof rules/laws, rather than by first defining how programs run (operational) or what they denote mathematically (denotational) and then deriving laws.
    • So the "meaning" of a program/term is whatever properties you can prove about it using the axioms and inference rules.
    • Strength: Centers the whole story on reasoning about programs, which led to key techniques like invariants.

  • A bit of history & comparison

    • 1960s-1970s: Operational semantics was often seen as inferior to denotational and axiomatic semantics-okay for "quick and dirty" feature definitions, but viewed as less elegant and less mathematically strong.

    • 1980s shift: Denotational/axiomatic approaches ran into tougher technical issues (denotational: nondeterminism & concurrency; axiomatic: procedures), making operational semantics' simplicity + flexibility more appealing.

    • Key developments that boosted operational semantics:

      • Structural operational semantics (SOS) [Plotkin, 1981]

      • Natural semantics [Kahn, 1987]

      • CCS [Milner, 1980; 1989; 1999]

        These introduced cleaner formalisms and helped transfer techniques from denotational semantics into operational settings.

    • Today: Operational semantics is a major research area and often the default method for defining languages and proving properties.

Evaluation ​

Operational semantics of boolean expressions

• Three sections in the definition above.

  • The set of terms.

  • The set of values, a subset of terms (possible final results of evaluation).

    -> Just constants true and false.

    -> The meta variable v is often used.

  • The inference rules for the evaluation relation.

    • Written $t \to t'$.
    • Pronounced "$t$ evaluates to $t'$ in one step".
    • Intuition: If $t$ is the state of the abstract machine at a given moment, then the machine can make a step of computation and change its state to $t'$.
    • This relation is defined by three inference rules (or, if you prefer, two axioms and a rule, since the first two have no premises).

• What the evaluation rules do not say is just as important as what they do say.

  • The constants true and false do not evaluate to anything, since they do not appear as the left-hand sides of any of the rules.

  • There is no rule allowing the evaluation of a then- or else-subexpression of an if before evaluating the if itself.

  • The set of evaluation rules, taken together forces a specific evaluation order (strategy).

    • Congruence rule = "where to evaluate next" (it propagates evaluation into a subterm; it sets the strategy/order).
    • Computation rule = "the actual reduction" (they perform the meaningful work once the guard is a value).

Intuition formalization ​

• Instance of an inference rule: ****An instance of an inference rule is obtained by consistently replacing each metavariable by the same term in the rule's conclusion and all its premises (if any).

• Rule satisfied by a relation: A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not.

  • What does this mean? (ChatGPT)

    • Setup

      • A rule has premises and a conclusion.
      • An instance of a rule = a concrete version after substituting its metavariables.
      • A relation R = a set of judgments you consider "true" (e.g., e \to e', or \Gamma \vdash e : \tau).

    • Definition

      A rule instance

      • Premises: P1, P2, ..., Pn

      • Conclusion: C

        is satisfied by a relation R iff:

      • either C \in R

      • or at least one premise is missing from R (i.e., Pi \notin R for some i)

        In words:

        You can't have all the premises in R while the conclusion is not in R.

    • Equivalent logical form

      Closure form

      • If all premises are in R, then the conclusion must be in R.

        (P1 \in R \wedge ... \wedge Pn \in R) \Rightarrow (C \in R)

        "No counterexample" form

      • There is no rule instance where all premises are in R but the conclusion is not.

        \neg((P1 \in R \wedge ... \wedge Pn \in R) \wedge (C \notin R))

    • Operational semantics intuition (small-step)

      If the rule is:

      • Premise: e1 \to e1'.

      • Conclusion: e1 e2 \to e1' e2.

        Then "R satisfies the rule" means: Whenever e1 \to e1' is in R, e1 e2 \to e1' e2 must also be in R.

        Satisfying a rule = being closed under that rule.

• One-step evaluation relation \to: The \to is the smallest binary relation on terms satisfying all the inference rules. When the pair $(t, t')$ is in the evaluation relation, we say that "the evaluation statement (or judgment) $t \to t'$ is derivable."

  • Why "smallest"?

    Statement $t \to t'$ is derivable iff it is justified by the rules:

    • Either it is an instance of one of the axioms.
    • Else it is the conclusion of an instance of rule whose premise is derivable.

• The derivability of a given statement can be justified by exhibiting a derivation tree.

  • Example

    The derivability of:

    is witnessed by the following derivation tree:

    • The bottom is the root.
    • The top are the leaves.

• An evaluation statement $t \to t'$ is derivable iff there is a derivation tree with $t \to t'$ as the label at its root.

  -> Often useful when reasoning about properties of the evaluation relation.

  -> A proof technique: induction on derivations.

Induction on derivations ​

At each step of the induction:

• Assume the target property holds for all smaller derivations.
• Perform a case analysis of the evaluation rule used at the root of the derivation.

-> We're looking at a single step of evaluation.

Theorem: Determinacy of one-step evaluation ​

Problem. If $t \to t'$ and $t \to t''$, then $t' = t''$.

Exercise 3.5.5 ​

Problem. Spell out the induction principle used in the preceding proof, in the style of Theorem 3.3.4.

Induction on derivation:

If, for each derivation $D$, given $P(D')$ for all $D'$ such that $| D' | < | D |$, we can show $P(D)$, then $P(D)$ holds for all $D$.

Normal form ​

• The final value of computation is particularly interested - states in which the machine cannot take a step.

• A term $t$ is in normal form if no evaluation rule applies to it- i.e., if there is no $t'$ such that $t \to t'$.

  (We sometimes say "$t$ is a normal form" as shorthand for "$t$ is a term in normal form.")

Theorem: Value is in normal form ​

Statement. Every value is in normal form.

• Trivial theorem for the current system.
• In most systems, this theorem should hold - otherwise, the language is simply broken.
• Being in normal form is part of what it is to be a value (i.e., a fully evaluated result).

Theorem: Normal form implies value ​

Statement. If $t$ is in normal form, then $t$ is a value.

Multi-step evaluation relation ​

• The multi-step evaluation relation $\to^*$ is the reflexive, transitive closure of one-step evaluation.

Exercise 3.5.10 ​

Problem. Rephrase Definition 3.5.9 as a set of inference rules.

Theorem: The uniqueness of normal form ​

Statement. If $t \to^* u$ and $t \to^* u'$, where $u$ and $u'$ are both normal forms, then $u = u'$.

Theorem: Termination of evaluation ​

Statement. For every term $t$ there is some normal form $t'$ such that $t \to^* t'$.

Exercise 3.5.13 ​

Statement 1. Suppose we add a new rule:

to the ones in Figure 3-1. Which of the above theorems (3.5.4, 3.5.7, 3.5.8, 3.5.11, and 3.5.12) remain valid?

Statement 2. Suppose instead that we add this rule:

Now which of the above theorems remain valid? Do any of the proofs need to change?

Evaluation - Arithmetic expressions ​

Operational semantics of arithmetic expressions - An extension of boolean expressions above

• A new syntactic category of numeric values.

  The final result of evaluating an arithmetic expression can be a number, where a number is either $0$ or the successor of a number. (but not the successor of an arbitrary value: we will want to say that $\text{succ}(\text{true})$ is an error, not a value).

• Note that in E-PredSucc, only numeric values are allowed.

  -> $\text{pred }(\text{succ } (\text{pred } 0)) \not\to \text{pred } 0$.

  -> This is prohibited to preserve the determinacy of one-step evaluation.

  The unique next step.

Exercise 3.5.14 - Determinacy of one-step evaluation ​

Statement. Show that Theorem 3.5.4 is also valid for the evaluation relation on arithmetic expressions: if $t \to t'$ and $t \to t''$, then $t' = t''$.

Stuck terms ​

• A closed term is stuck if it is in normal form but not a value.

  -> "Stuckness" represents a simple notion of run-time error for our simple machine.

  -> Stuckness characterizes the situations where the operational semantics does not know what to do because the program has reached a "meaning-less state."

  -> In a more concrete implementation of the language, these states might correspond to machine failures of various kinds: segmentation faults, execution of illegal instructions, etc.

  -> All these kinds of bad behavior are collapsed into the single concept of "stuck state."

Exercise 3.5.16 - Explicit failure state in operational semantics ​

Statement.

A different way of formalizing meaningless states of the abstract machine is to:

1. Introduce a new term called $\text{wrong}$.
2. Augment the operational semantics with rules that explicitly generate $\text{wrong}$ in all the situations where the present semantics gets stuck.

To do this in detail, we introduce 2 new syntactic categories:

and we augment the evaluation relation with the following rules:

Show that these 2 treatments of run-time errors agree by:

1. Finding a precise way of stating the intuition that "the two treatments agree,"
2. Proving it.

As is often the case when proving things about programming languages, the tricky part here is formulating a precise statement to be proved - the proof itself should be straightforward.

Observation:

• badnat contains wrong and normal booleans.
• badbool contains wrong and nv.
• So, a term can fall within multiple syntactic categories.

Exercise 3.5.17 ​

Statement. Two styles of operational semantics are in common use.

• The one used in this book is called the small-step style, because the definition of the evaluation relation shows how individual steps of computation are used to rewrite a term, bit by bit, until it eventually becomes a value.

  On top of this, we define a multi-step evaluation relation that allows us to talk about terms evaluating (in many steps) to values.

• An alternative style, called big-step semantics (or sometimes natural semantics), directly formulates the notion of "this term evaluates to that final value," written $t \Downarrow v$. The big-step evaluation rules for our language of boolean and arithmetic expressions look like this:

Show that the small-step and big-step semantics for this language coincide, i.e. $t \to^* v$ iff $t \Downarrow v$.

Observation: The right-hand-side for the $\Downarrow$ is always a normal form.

Exercise 3.5.18 ​

Statement. Suppose we want to change the evaluation strategy of our language so that the $\text{then}$ and $\text{else}$ branches of an $\text{if}$ expression are evaluated (in that order) before the guard is evaluated. Show how the evaluation rules need to change to achieve this effect.

Related resources ​

• Abstract and concrete syntax, parsing: Dozens of textbooks on compilers.

• Inductive definitions, systems of inference rules, and proofs by induction: [Winskel, 1993; Hennessy, 1990].

• The style of operational semantics that we are using here: A technical report by [Plotkin, 1981].

• The big-step style (Exercise 3.5.17): [Kahn, 1987].

  See [Astesiano, 1991] and [Hennessy, 1990] for more detailed developments.

• Structural induction was introduced to computer science by [Burstall, 1969].