This seems like little more than a parlor trick.<p>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?<p>> 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.<p>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?