categories: Re: Real midpoints

[Dusko Pavlovic <dusko@kestrel.edu>]

> My point is that the definition of  g  is neither recursive nor
> co-recursive. The definition of  g  is merely expressed as a fixpoint
> equation, and Peter has set up things so that there is indeed a unique
> solution to this equation. However, the reason the fixpoint is unique
> is because the  "h"  part is contracting, and not because the equation
> is co-recursive.

what exactly do you mean by corecursive? (it's guarded, and guarded equations
do have unique fixpoints.)

-- dusko