Home » forums » LtU Forum

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,
Ohad.

By Ohad Kammar at 2006-09-14 09:02 | LtU Forum | previous forum topic | next forum topic | other blogs | 7837 reads

Comment viewing options

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

a sketch =


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

By Albert Y.C. Lai at Fri, 2006-09-15 19:53 | login or register to post comments

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,
Ohad.

By Ohad Kammar at Sat, 2006-09-16 16:38 | login or register to post comments