Types and Programming Languages Chapter 3 Untyped Arithmetic Expressions

3.5.8

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

• @tomstuart: Notice that this is only true because the language has booleans and nothing else, so it happens to be impossible to “make a mistake” when you write a term.

  The condition in an if … then … else … term inevitably evaluates to a boolean because that’s the only kind of thing there is, so either E-IfTrue or E-IfFalse must eventually apply, and both rules dismantle the if … then … else … and replace it with a smaller expression.

  If the language supported other kinds of thing (e.g. numbers) then this wouldn’t be true any more: a badly-written if … then … else … term with a non-boolean condition doesn’t have an evaluation rule, so it’s in normal form, but it isn’t a value.

3.5.12

First, we choose some well-founded set S and give a function f mapping “machine states” (here, terms) into S.

• @tomstuart: “well-founded set” means “you always run out of smaller elements” (see 2.2.10 on page 18).

  For example, the natural numbers are a well-founded set because zero is smaller than every other natural number. (An example of a non–well-founded set is the integers, because there is no smallest integer: -1 is smaller than 0, but -2 is even smaller, -3 is smaller again, and so on.)

  The termination proof assumes you realise that a) the size of a term is a natural number, and b) the natural numbers are well founded. In other words: if you can prove that evaluation always reduces the size of a term, then evaluation must eventually finish because the size can’t go below zero.