3 ms·

Here's my attempt to translate. I think it's probably wrong and welcome corrections. You have a function `p` which accepts an "element of the Cantor space" (in

Here's my attempt to translate. I think it's probably wrong and welcome corrections. You have a function `p` which accepts an "element of the Cantor space" (infinite sequence of bits) and returns true or false. You want to find some value where it returns true, or prove that it returns false for every value. Crucially `p` is not a math function, it is a Haskell function. So you can't say "p is true iff its argument is pi" because you can't write that in Haskell. In fact, all `p` can do is look at finitely many bits - if it looks at infinite bits, there is an input for which it will never return. And because it looks at finitely many bits, there is necessarily a largest bit-index which it looks at. Now a generic-imperative programmer might attempt: for (bignum x = 0; x < infinity; x++) if (p(x)) return x; return NotFound; but the problem is knowing when to stop, so as to return NotFound. However, if we could detect when `p` demands more bits than we have produced, then the search will terminate: int bits = 0; bignum x = 0; while (x < (1 << bits)) { try { if (p(x)) return x; x++; } catch (BitAccessOutOfBounds) { bits++; } } return NotFound; Haskell's laziness enables it to "drive the loop" but the idea is not so different.

Kednicma 6y ago
Yes, you have it exactly right, including the usage of non-local control flow to interrupt and restart the search. [0] is another implementation in an imperative language. [0] https://github.com/monte-language/typhon/blob/master/mast/fun/cantor.mt https://github.com/monte-language/typhon/blob/master/mast/fu...
shachaf 6y ago
Laziness isn't the essential thing here -- the article's construction specifically doesn't rely on laziness, and would work in a strict language (almost verbatim -- you might need to write "lambda i: f(i)" instead of "f" in a few places). I'd say that the thing that makes the article's version work is that you can pass a closure to the predicate, which is a channel for communicating extra information that makes it not quite a black box. In an imperative language, you could imagine passing in a function that mutates some state to get information out (or throws an exception, the way you set it up). The article shows that even that isn't necessary: You can pass in a sequence (represented as a function from index to value) that closes over the predicate itself, and recursively uses it to build a bit sequence that satisfies it, if one exists. By the way, there's a clearer (I think) version of the core idea here that uses conatural numbers (the naturals + infinity) that people don't usually present, but might be worth writing up.
- ridiculous_fish 6y ago
  In the article `p` really does take a list not a function! Haskell lists may be "backed by" functions but these functions must be pure - no back-channels. I'm not sure if this fact illuminates or obscures the point. Anyways you can't pass a closure to the predicate, and the Haskell version has no "back channels" other than termination. The idea is to arrange the recursive search so that the predicate (not the search) demands the bits. This is what terminates the recursion, and it's hard to arrange without laziness (except by introducing more functions as you say).
  - shachaf 6y ago
    No, the article's p takes a function: > type Cantor = Natural -> Bit > (#) :: Bit -> Cantor -> Cantor > x # a = \i -> if i == 0 then x else a(i-1) (You could represent bit streams with something like data Stream = Cons Bit Stream in Haskell, of course, but that's not what the article does. The code in the article works in e.g. Python almost as-is.) And you can certainly pass closures to the predicate. Not closing over a mutable variable, of course -- I just mean that the bit stream function itself has to have access to p, which is the trick that makes this possible. If you couldn't do that -- if you could only query it with bit sequences that were defined independently of p -- this wouldn't be possible.
    - ridiculous_fish 6y ago
      Coming back to this very late! > No, the article's p takes a function Yeah it does, but it's just misdirection. A lot of this theory is gamified "you pick YOUR function, THEN I'll pick MINE..." and the order is very important. Here representing sequences as functions only obscures. The important idea is that the sequence is lazy, BUT predetermined. It can't know what the predicate will be. That's where the black magic comes in. > You could represent bit streams with something like data Stream = Cons Bit Stream in Haskell I wish it did, it would be much clearer. The article makes that point itself: "For the type of infinite sequences, we could use the built-in type of lazy lists..." which is the point you made (which the article dismisses as insufficiently mathematical). > If you couldn't do that -- if you could only query it with bit sequences that were defined independently of p -- this wouldn't be possible. No, there's the rub! The bit sequence and `p` are independent. You choose your bit sequence, I choose `p`, and somehow execution finishes. That's exactly what makes this "seemingly impossible." There is a back-door dependence where `p` forces a lazy sequence to materialize bits, but nothing more. The sequence cannot introspect `p`, and vice-versa. I think this my third time encountering this post and it took me a few tries to get it!
panic 6y ago
Really nice explanation! I'd also add that it's not enough that p is continuous (only looks at a finite number of bits for each input) -- it must also be uniformly continuous (the number of bits it looks at can't become arbitrarily high for arbitrary inputs). For example, if you exclude the sequence of all ones 111111... from the Cantor set, you can write this function p which always returns false: function p(bits) { n = 0 while bits(n) == 1 { n++ } return false } This function would loop forever on the all-ones sequence. But since that sequence was excluded, p is a total function which looks at more and more bits depending on how many leading ones there are. While each particular input only demands a finite number of bits, there's no finite number of bits which lets you search the entire space. The compactness of the Cantor set ensures that all continuous functions are also uniformly continuous, but if you remove points from the set, it can stop being compact, and the magic spell can be broken!

Kednicma 6y ago

Yes, you have it exactly right, including the usage of non-local control flow to interrupt and restart the search. [0] is another implementation in an imperative language. [0] https://github.com/monte-language/typhon/blob/master/mast/fun/cantor.mt https://github.com/monte-language/typhon/blob/master/mast/fu...

shachaf 6y ago

Laziness isn't the essential thing here -- the article's construction specifically doesn't rely on laziness, and would work in a strict language (almost verbatim -- you might need to write "lambda i: f(i)" instead of "f" in a few places). I'd say that the thing that makes the article's version work is that you can pass a closure to the predicate, which is a channel for communicating extra information that makes it not quite a black box. In an imperative language, you could imagine passing in a function that mutates some state to get information out (or throws an exception, the way you set it up). The article shows that even that isn't necessary: You can pass in a sequence (represented as a function from index to value) that closes over the predicate itself, and recursively uses it to build a bit sequence that satisfies it, if one exists. By the way, there's a clearer (I think) version of the core idea here that uses conatural numbers (the naturals + infinity) that people don't usually present, but might be worth writing up.

ridiculous_fish 6y ago
In the article `p` really does take a list not a function! Haskell lists may be "backed by" functions but these functions must be pure - no back-channels. I'm not sure if this fact illuminates or obscures the point. Anyways you can't pass a closure to the predicate, and the Haskell version has no "back channels" other than termination. The idea is to arrange the recursive search so that the predicate (not the search) demands the bits. This is what terminates the recursion, and it's hard to arrange without laziness (except by introducing more functions as you say).
- shachaf 6y ago
  No, the article's p takes a function: > type Cantor = Natural -> Bit > (#) :: Bit -> Cantor -> Cantor > x # a = \i -> if i == 0 then x else a(i-1) (You could represent bit streams with something like data Stream = Cons Bit Stream in Haskell, of course, but that's not what the article does. The code in the article works in e.g. Python almost as-is.) And you can certainly pass closures to the predicate. Not closing over a mutable variable, of course -- I just mean that the bit stream function itself has to have access to p, which is the trick that makes this possible. If you couldn't do that -- if you could only query it with bit sequences that were defined independently of p -- this wouldn't be possible.
  - ridiculous_fish 6y ago
    Coming back to this very late! > No, the article's p takes a function Yeah it does, but it's just misdirection. A lot of this theory is gamified "you pick YOUR function, THEN I'll pick MINE..." and the order is very important. Here representing sequences as functions only obscures. The important idea is that the sequence is lazy, BUT predetermined. It can't know what the predicate will be. That's where the black magic comes in. > You could represent bit streams with something like data Stream = Cons Bit Stream in Haskell I wish it did, it would be much clearer. The article makes that point itself: "For the type of infinite sequences, we could use the built-in type of lazy lists..." which is the point you made (which the article dismisses as insufficiently mathematical). > If you couldn't do that -- if you could only query it with bit sequences that were defined independently of p -- this wouldn't be possible. No, there's the rub! The bit sequence and `p` are independent. You choose your bit sequence, I choose `p`, and somehow execution finishes. That's exactly what makes this "seemingly impossible." There is a back-door dependence where `p` forces a lazy sequence to materialize bits, but nothing more. The sequence cannot introspect `p`, and vice-versa. I think this my third time encountering this post and it took me a few tries to get it!

panic 6y ago

Really nice explanation! I'd also add that it's not enough that p is continuous (only looks at a finite number of bits for each input) -- it must also be uniformly continuous (the number of bits it looks at can't become arbitrarily high for arbitrary inputs). For example, if you exclude the sequence of all ones 111111... from the Cantor set, you can write this function p which always returns false: function p(bits) { n = 0 while bits(n) == 1 { n++ } return false } This function would loop forever on the all-ones sequence. But since that sequence was excluded, p is a total function which looks at more and more bits depending on how many leading ones there are. While each particular input only demands a finite number of bits, there's no finite number of bits which lets you search the entire space. The compactness of the Cantor set ensures that all continuous functions are also uniformly continuous, but if you remove points from the set, it can stop being compact, and the magic spell can be broken!