4905
|
1 |
|
|
2 |
(*** Example 3.8 ***)
|
|
3 |
|
|
4 |
Ex2 = LCF +
|
|
5 |
|
|
6 |
consts
|
|
7 |
P :: "'a => tr"
|
|
8 |
F :: "'a => 'a"
|
|
9 |
G :: "'a => 'a"
|
|
10 |
H :: "'a => 'b => 'b"
|
|
11 |
K :: "('a => 'b => 'b) => ('a => 'b => 'b)"
|
|
12 |
|
|
13 |
rules
|
|
14 |
F_strict "F(UU) = UU"
|
|
15 |
K "K = (%h x y. P(x) => y | F(h(G(x),y)))"
|
|
16 |
H "H = FIX(K)"
|
|
17 |
|
|
18 |
end
|