[1] http://xenon.kiam.ru/~roman/doc/2009-Klyuchnikov_Romanenko--...

Basically, if supercompilation of the expression above results in a huge nested case that has either True as a result (termination) or an application of function (not terminated due to infinite data structures, for example), then functions are equivalent. Otherwise, if there is at least one False, they are not, the path to False provides a counterexample.

I looked up Cantor Sets so I have a vague understanding... but there are many things I don't understand. Like what does it mean to have a sequence with a bit appended to a Cantor Set? Why is that a Cantor Set? What the heck is a total p - is it a function?

First, a true "exhaustive search" is actually impossible. The cantor space is uncountable (which can be seen by prepending '0.' before every binary sequence which gives the real number interval [0,1).) But an exhaustive search will visit all elements in some order which provides an ordering. Thus its existence implies that the cantor space is countable. Contradiction. The post gets around this by only looking at the first n elements of every binary sequence: f,g and h evaluate little more than the 7th digit. Sure, exhaustively searching 2^7 elements can be done in less than a second, why is this new?

> In fact, e.g. the function type Integer -> Integer doesn’t have decidable equality because of the Halting Problem, as is well known. However, common wisdom is not always correct, and, in fact, some other function types do have decidable equality, for example the type Cantor -> y for any type y with decidable equality, without contradicting Turing.

I fail to see how this can be true. We can set y = Integer, since integers have decidable equality. Then we can encode every integer as an element of cantor space by converting it into binary with the least significant digit first (and using the 0th element of the sequence to distinguish positive and negative integers) and padding the sequence with zeros towards infinity. Then two functions f,g : Integer -> Integer are equal iff their transformed representations f . p, g . p : Cantor -> Integer are equal. Thus functions from the cantor space having decidable equality implies functions from the integers having decidable equality which "solves" the halting problem. Again the post gets around this by only looking at the first few elements... but equality of functions f,g : Integer -> Integer is trivially decidable if f and g are zero for integers bigger than some N, so how is this new?

Thus if you assume that the function is total and thus doesn't halt, it must run in O(1) time.

To find an infinite input bit string where the function halts, we can just record which k = O(1) bits the function is querying and then try all 2^k possibilities and as calculating the function is O(1) the total time is also O(1). (We don't always have to try all 2^k possibilities).

It's hard for me to imagine a reader that understands the rest of this jargon, presented without explanation, who does not know what `Maybe` is.

Sure, this is interesting, but in the sense of "look at this emergent behavior -- such a simple system can do unusually complex result", rather than "wow! no one could do such things with computer before"

Can someone explain how find works if the predicate is something like: return true if and only if every other bit is 1

Your comment, "the post gets around this by only looking at the first n elements of every binary sequence" is also wrong. This is not at all what the `equal` function does.

You can do the same trick with natural numbers to "prove" that they are uncountable too - just drop the duplicates. 0.0, 0.1, 0.2, 0.3, ... 0.9, 0.11, 0.12, 0.13...

Unfortunately, neither of these sequences contain the real 1/3, so they have gaps.