Fixed-Point Induction

Lately I started learning by myself the domain theory approach to semantics using G. Plotkin's "Domains" (1983). While doing the excercises, I bumped into the next question regarding fixed-point induction:

Let f,g: D -> D be continuous functions, such that f.f.g = g.f, and f _|_ = g_|_. Show that Yf = Yg.

(Here `.' is the analytic function composition: f.g(x) = f(g(x)) and _|_ denotes the least element, of course).

[Chap. 2 question 21]

It is more or less clear how to prove it using normal induction and the least fixed point formula, but I have no idea which inclusive predicates to choose. I was hoping someone here could supply some hints\directions.

On a more general note: Is there an intuition as to how to choose these inclusive predicates? I imagine it is acquired in time and practice, so do you know of a list of properties that can be proved using fixed-point induction?

Thanks in advance,

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

a sketch =

=   〈use f.f.g=g.f and f⊥=g⊥, eg gg⊥=gf⊥=ffg⊥=fff⊥〉
  ⊔n·f^(2^n - 1)(⊥)
=   〈exercise〉

I was aiming for fixed-point induction...

Thanks a heap for your help, but I already got that solution. I wanted to try this question using fixed-point induction, but I just can't seem to find the correct inclusive predicate.

I was hoping someone here will be able to direct me, or even maybe explain about the intuition that leads to it (if it exists...).

Thanks nontheless,