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'  Alphabetic index  Help page about these notes  Course home    Evaluation Order and Infinite Lists - slide 16 : 27

Theoretical results
The theoretical results mentioned on this page assure some very satisfactory properties of functional programming

The first Church-Rosser theorem.   If e1 <=> e2 then there exists an e3 such that e1 => e3 and e2 => e3
The second Church-Rosser theorem.   If e0 => ... => en , and if en is on normal form, then there exists a normal-order reduction of e0 to en