Notes (LCBB 04/07): Reduction

4 Reduction

4.1 Definition of compatible relations

4.2 Definition of ->_β, ->>_β and =_β

4.3 Examples of ->, ->> and =

4.4 Example of =

KIΩ -> (\ y. I)Ω -> I
II -> I

So, equality, or β-convertibility, is like asking “do these two expressions perform the same computation, i.e. return the same expressions for the same inputs.

4.5 Proposition (equivalence of β-convertibility and λ-provable equality)

If you look at section 2.7, you’ll see that λ-provable equality is a binary relation that is:

Which is exactly the same structure as the β-convertibility relation. So if we have a proof that λ |- M = N, we can convert each step into a proof that M =_β N and vice-versa.

4.6 Definition of β-redex and β-normal form

4.8 Lemma

The triple line equals sign is confusing here, and is not disambiguated from regular equals in the text. I think that triple line equals means term-substitution, so this lemma is saying that if M is β-reducible to N, then you can substitute any N for an M.

4.9 Church-Rosser Theorem

If M has two different reduction paths to distinct terms N1 and N2, then both of those terms will have reduction paths that converge on a third term N3. In other words, it doesn’t matter what order you reduce sub-terms of M, because you’ll always have a way to converge back to a common term. Even if you have divergent terms in M like Ω and you can make infinite reductions without converging, at every step you’ll always have a way to come back to the convergent path.

4.10 Corrolary

If M = N, then there is a common L to which they both reduce M ->> L, N ->> L

There are only three cases where M = N (from the definition of =_β in 4.2).

  1. M ->> N => M = N
  2. N = M => M = N
  3. M = N', N' = N => M = N

An intuitive way to see that there are only three cases where M = N is by looking at the diagram in the text and visualizing the arrows as a kind of fluid flow, where M = N means that there is a waterway between M and N. If there is a waterway, then either

M is downstream from N, N ->> M M is upstream from N M ->> N M is both upstream and downstream from N, N ->> M && M ->> N M is neither upstream nor downstream from N

The first two cases can be thought of as the same, because = is symmetric.

Only the last case, where the waterway between M and N changes direction is tricky and requires induction.

4.11 Corrolary

λ-terms are β-reducible to their normal forms, and have at most one such normal form.

4.12 Some consequences

4.13 Definition of Underlining

4.14 Definition of φ : Λ_ → Λ

φ(x) = x
φ(M N) = φ(M)φ(N)
φ(\x.M) = \x.φ(M)
φ((\_x.M)N) = φ(M)[x:= φ(N)]

Okay, so what’s going on here is that φ is reducing all the underlined \_ redexes, but leaving the non-underlined ones \ intact.

4.15 Lemma

This diagram is saying that in an underlined redex, dropping the underlines and β-reducing is the same as β_-reducing and then dropping the underlines. Remember that the ->>_ arrow (any-step β_ reduction) treats underlined lambda abstractions the same as non-underlined ones.

4.16 Lemma