I have some reservations about the terminology used in Paulson's paper (though this may well be standard), so I am making
some adjustments which have very little impact on the proofs.
There are two problems.
The first is that he defines "lfp" to mean something which he later proves is the least fixed point.
I would prefer the definition of "lfp" to more directly state that the thing yielded us the least fixed point.
The second is that while he talks about fixed points, some of his formal material is really about closures.
So I'm going to talk about closures until I have proven the "fixed point" theorem, and then define "lfp" (actually as yielding
a fixed point which is the least closure, since this is slightly "stronger" than least fixed point).
Here you should first think of forming closures under certain operations.
This is hard to formalise in a general way because the signatures of the operations may vary.
So we suppose that we are doing an iterative process (like the iterative construction of the heirarchy of sets except that
that particular one never yields a closed).
At each step in this process new objects are formed from an existing set using the operations under which we are aiming for
closure, and these are added to the old objects to form a new set.
For the function doing this we usually use the name "h".
If we ever find a set closed under the operations then we find that the result of applying "h" to it is contained in the original
(no new objects result), and that is what the following definition of closed states:
xlholconst closed : GS → (GS → GS) → BOOL

∀A h• closed A h ⇔ h(A) ⊆_{g} A
