Play audio slide show -- Keyboard shortcut: 'x'  Lecture overview -- Keyboard shortcut: 'u'  Previous page: An example of normal versus applicative evaluation -- Keyboard shortcut: 'p'  Next page: Practical implications -- Keyboard shortcut: 'n'  Lecture notes - all slides together  Annotated slide -- Keyboard shortcut: 't'  Textbook -- Keyboard shortcut: 'v'  Alphabetic index  Help page about these notes  Course home      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