## 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?

## Comment viewing options

### a sketch =

  âŠ”nÂ·g^n(âŠ¥)
=   âŒ©use f.f.g=g.f and fâŠ¥=gâŠ¥, eg ggâŠ¥=gfâŠ¥=ffgâŠ¥=fffâŠ¥âŒª
âŠ”nÂ·f^(2^n - 1)(âŠ¥)
`