Plotkin also used a Church–Rosser theorem to prove that the evaluation of functional programs (for both lazy evaluation and eager evaluation) is a function from programs to values (a subset of the lambda terms).
Plotkin je također rabio Church-Rosserov teorem za dokaz da je evaluacija funkcijskih prorama (i za lijenu evaluaciju i za striktnu evaluaciju) funkcija iz programa u vrijednosti (podskup lambda termina).