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 and notes together  slide -- Keyboard shortcut: 't'  Help page about these notes  Alphabetic index  Course home  Lecture 4 - Page 16 : 27
Programming Paradigms
Evaluation Order and Infinite Lists
Theoretical results

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

The rewriting => is confluent if for all e, e 1 and e 2 , for which e => e 1 and e => e 2 , there exists an e 3 such that e 1 => e 3 and e 2 => e 3

The first Church-Rosser theorem.   If e1 <=> e2 then there exists an e3 such that e1 => e3 and e2 => e3

  • Rewriting with beta and eta conversions are confluent

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

  • Normal-order reduction is the most powerful evaluation order