  | 2 minutes, 59 seconds | The Order of Evaluation - slide 16 : 26 |
Theoretical results
The theoretical results mentioned on this page assure some very satisfactory properties of functional programming
The first Church-Rosser theorem. Rewriting with beta and eta conversions are confluent.
The second Church-Rosser theorem. If e0 => ... => e1, and if e1 is on normal form,
then there exists a normal order reduction of e0 to e1