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 e
1
<=> e
2
then there exists an e
3
such that e
1
=>
e
3
and e
2
=>
e
3
Rewriting with beta and eta conversions are
confluent
The second Church-Rosser theorem
. If e
0
=>
...
=>
e
n
, and if e
n
is on normal form, then there exists a normal-order reduction of e
0
to e
n
Normal-order reduction is the most powerful evaluation order
Foldoc: church-rosser
