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