The computation may be finite, it may be infinite, but a very important property of this process is that if a normal form exists, then this normal form is unique. This is a consequence of quite a deep result that is called the Church-Rosser theorem, which is stated on the slide and which is summarised in this picture. Suppose we have a term M, which reduces to different terms, M' and M''. The theorem guarantees that there exists a term P such that both M' and M'' reduce to P. So, in a sense, this expresses that computation, which can be non-deterministic during the process of computation, it is deterministic as far as normal forms are concerned. If there is a normal form for P, then this normal form is unique. And this is a very handy property to have, because since we are looking at terms as programmes, as programmes applied to arguments, then we want to get back from programmes just a single result and not a non-deterministic behaviour.

---