1
2
(*** Section 10.4 ***)
3
4
Ex1 = LCF +
5
6
consts
7
P :: "'a => tr"
8
G :: "'a => 'a"
9
H :: "'a => 'a"
10
K :: "('a => 'a) => ('a => 'a)"
11
12
rules
13
P_strict "P(UU) = UU"
14
K "K = (%h x. P(x) => x | h(h(G(x))))"
15
H "H = FIX(K)"
16
17
end