Pavel Panchekha

By

Share under CC-BY-SA.

Xifed points

While discussing the self-application of call/cc, I noted that ((call/cc call/cc) x) is the self-application (x x). Since (call/cc call/cc) is itself a self-application, there’s a fascinating fact: (call/cc call/cc) is equivalent to ((call/cc call/cc) call/cc), and we can keep applying the result to call/cc ad infinitum.

Now, this brings to mind the fixed-point combinator. The fixed-point combinator is defined so: 

(fix f) = (f (fix f))

What about the reverse? 

(xif f) = ((xif f) f)

Then (xif call/cc) could be (call/cc call/cc), since that satisfies the above equation. However, xif as defined above does not converge.

Convergence

Now, in a call-by-value calculus, neither does fix. Call-by-value demands that the argument is available before evaluating an application. Call by name dispenses with that requirement, but it still requires the function to be available before evaluating an application. Can we eliminate this assumption?

In any case, can we find a meaning for this xif operator? Let's step into the monad world for a moment to clarify things.

Interpretations of fixed points

If f is a monadic function (of type a -> m a), we can write a fixed-point operator for it like so: 

fixM f = (fixM f) >>= f

This does not converge, but it does capture the meaning of fix: it is the value that, when f is applied to it, does not change.

If we take the dual of fixM, we get xifW, which is analogous to a xifed-point operator for comonad functions: 

xifW f = extend f (xifW f)

Interpreting the comonads

We can try to interpret this function using some analogies. Comonads are like objects, and comonad functions are like commands. So the xifed-point of a command is the object you get by passing that command over and over again to an object.

Which object? You can have a different xifed-point if you start with different objects, just as you can have different fixed points if you start with different base cases. Normally the definition of fix and xif ignore the starting point (and so only make sense when there is one fixed/xifed-point). This is why using fix to define the factorial does not define what happens to negative inputs.

We can write fix and xif in an imperative style to make the dependence on the initial object clear: 

def fix(initial, f):
    while True:
        next = f(initial)
        if next == initial: break
        initial = next
    return initial

def xif(initial, f):
    while True:
        next = initial.execute(f)
        if next == initial: break
        initial = next
    return initial

We only use fix and xif in the usual forms because we are working with fixed/xifed-points that do not depend on the initial conditions in any interesting way.

When are xifed-points meaningful?

For xifed-points to be meaningful there have to be arguments for which the result of a function call does not depend on the function. So let's imagine that there exists a command become0, such that (f become0) is 0 for all f. You can think of this as a hard-reset command.

Then xif become0 must be 0, since 0 become0 = 0. Similarly, we can build an entire language of commands with if and such, and define their behavior on arbitrary objects. All we'd have done is shown that we can write all applications backwards and then compute fixed-points. So aren't fixed-points and xifed-points more or less identical, with the duality pretty meaningless?

But it is kind-of weird that the fixed-point operator can be typed, and the xifed-point operator cannot.