[...] A video of his talk is available over on his blog, and his presentation is remarkably clear, and would serve as a good preamble to the code I'm going to present below. [...]

In the pure functional case, the epsilon one gets is not just any epsilon - it is a minimization function.

To be precise, for the examples I've seen, there is a "search order" on Int (not necessarily the usual order, not necessarily well-founded). The order on Int then induces a lexicographical partial-order on (Int->Bool) (which is only a total order if the search-order is well-founded).

The search functionals (Cantor->Bool)->Cantor then I believe return the minimum (not just a minimal!) element for which the predicate holds (or the max. element if the predicate is empty). [That is true if all the examples I've seen written down, one can twist them so they do not, e.g., remapping Cantor->Cantor by flipping odd-numbered bits.]

And one can make the search functional parametrised by the search-order Int->Int->Bool, giving a parametrised minimisation operator (Int->Int->Bool) -> ((Int->Bool) -> Bool) -> Int->Bool.

Question: do all PCF-definable search functionals (Cantor->Bool)->Cantor minimise w.r.t. some [not PCF-definable] partial-order on Cantor? (I guess one should ask for the order to be on the extensional quotient of the total objects.)

It is not obvious to me whether or not one can do minimisation using the kind of "memoisation" techniques that speed up search in the non-functional case.

Question: in your favourite non-fully-abstract model of PCF, do there exist parametrised minimisation operators of the type above? [Conjecture - none will not exist in the stable model, but will exist in the continuous model.]

Too much coffee this morning!

Once you have a search functional you can define the uniform modulus of continuity and then compute finite graphs of members of Cantor->Bool & do any sort of minimisation you like.

So I was talking bollocks.

You're not toally off the mark, though. It is relevant to ask whether $\epsilon$ is extensional. Of course, if $\epsilon$ always finds the first witness in the lexicographic (or some other) order, then it is extensional. And, as you observe, given any $\epsilon$ we can always construct an extensioonal one. But still Martin's $\epsilon$ is extensional (because it is total and written in PCF), while mine is not (try applying it to XOR written in different orders).