6 ms·

Seemingly impossible functional programs (2007)

87 points by ogogmad 6y ago

amicin 6y ago
I took Martin Escardo’s course on functional programming at university. Nothing but positive things to say about the man. A fantastic teacher with a real care for his students. Makes me happy to see him on HN.
- m_j_g 6y ago
  You may be interested in his brand new course on HoTT in Agda https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes...
cvoss 6y ago
I think I have a half-baked understanding of what's going on here. Let me talk through it. Take a function f : unit_interval -> bool. I believe that if there is no bound on the execution time of f, then f must not be a total function. (So conversely, if f is total, then it has bounded execution time, and is therefore only considering prefixes of the digit streams of up to some bounded length. From there, searching for an example input x s.t. f(x) = true is easy.) Naively, it would seem plausible that there exists a total function which, nevertheless, takes longer and longer to run on a particular sequence of inputs. So let such a sequence be given, where the runtime of f(x_i) tends to infinity, even though it is finite for each x_i. But from topology, we know that a sequence of points in a compact space, like the unit interval, has a convergent subsequence. The interesting thing happens when you look at f(y) where y is the limit point of such a subsequence. It is the case that as i increases, x_i and y increasingly look the same for longer and longer prefixes of their decimal (binary) expansions. Therefore, f has to do more and more work to tell apart x_i and y, which gives us an argument that there is no bound on the runtime of f(y); i.e., f doesn't terminate for that particular input. (Except, you have to get nitpicky about redundant representations of reals like 0.0099999... vs 0.010000..., but we can always choose the representation of y that suits us: the one that looks more like the x_i's.)
- contravariant 6y ago
  Yeah I think there are some small problems with your argument, unless it was only meant to illustrate the idea. For the sake of argument let's say we simply input both decimal representations of each number. A program that simply tries to find the first decimal that isn't 9 for a number in [0,1] would take an arbitrary amount of time, but is still total because 1 can be identified in a single step. The problem here is that while the function is total it isn't continuous and so the compactness of the topology is irrelevant. As far as I can tell the article uses some trickery to ensure that computable functions _are_ continuous, in which case it does work.
  - cvoss 6y ago
    You're right, it's not a precise line of reasoning. I was considering only computable functions (else "runtime" isn't a meaningful concept) and treating the input domain as actually being the Cantor space, where 0.9999... and 1.0000... are actually distinct values. I just found it helpful to think about the Cantor space in terms of the unit interval.
    - JadeNB 6y ago
      > the Cantor space, where 0.9999... and 1.0000... are actually distinct value What do you mean here? The Cantor set is a subspace, not a cover, of [0, 1]; values in the Cantor set that are the same in [0, 1] are also the same in the Cantor set.
      - thaumasiotes 6y ago
        Sure, the Cantor set is the set of real numbers in [0,1] with trinary expansions that do not contain 1 at any point. A Cantor space is any set that can be mapped to (and from) the Cantor set. The Cantor space is the set of infinitely long bitstrings; instead of a trinary number 0.200220222200..., you'd conceive of the same entity as the string "100110111100...". The mapping is pretty obvious. 0.99999... and 1.0000... are neither of them bitstrings, so it's not really clear what cvoss was thinking of. But it's certainly true that "0999999..." and "1000000..." are distinct strings. Going back to the Cantor set, you'd usually represent 1 as 0.22222222... for obvious reasons of consistency (that is the only format matching the representation of the rest of the set). It would be weird to represent it as 1.000000000...; that would look like you were considering the left end of the Cantor set in [1,2] rather than the right end of the Cantor set in [0,1].
dang 6y ago
If curious see also 2015 https://news.ycombinator.com/item?id=10575626 https://news.ycombinator.com/item?id=10575626
Kednicma 6y ago
One way to imagine this space is as an indexed bank of light switches. Each switch starts out unset, and our goal is to find a configuration on a finite number of switches which will satisfy our search. The search can only check one switch at a time and must commit after each check. This allows a basic nemesis to compute a configuration by running the search repeatedly and rescuing it after each time it fails by checking the last switch checked. A gorgeous immediate consequence is that each search is looking for a solution to a SAT problem! Each SAT solution describes the edge of a region of Cantor space whose elements all have the searched-for property. And thus, while the search can proceed in finite time, it must sadly be NP-complete.
ridiculous_fish 6y ago
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.
ogogmad 6y ago
On a similar vein, you can write functional programs that can do exact Riemann integration: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54.395&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54....
billforsternz 6y ago
Sadly this goes over my head. But, I've got to say, this is a very nice looking website. It's nicely organised on github too.
ogogmad 6y ago
Here is an application of the technique to proving Conway's cosmological theorem: https://www.cs.cmu.edu/~kw/pubs/conway.pdf https://www.cs.cmu.edu/~kw/pubs/conway.pdf

87 points by ogogmad 6y ago

I took Martin Escardo’s course on functional programming at university. Nothing but positive things to say about the man. A fantastic teacher with a real care for his students. Makes me happy to see him on HN.

m_j_g 6y ago
You may be interested in his brand new course on HoTT in Agda https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes...

cvoss 6y ago

I think I have a half-baked understanding of what's going on here. Let me talk through it. Take a function f : unit_interval -> bool. I believe that if there is no bound on the execution time of f, then f must not be a total function. (So conversely, if f is total, then it has bounded execution time, and is therefore only considering prefixes of the digit streams of up to some bounded length. From there, searching for an example input x s.t. f(x) = true is easy.) Naively, it would seem plausible that there exists a total function which, nevertheless, takes longer and longer to run on a particular sequence of inputs. So let such a sequence be given, where the runtime of f(x_i) tends to infinity, even though it is finite for each x_i. But from topology, we know that a sequence of points in a compact space, like the unit interval, has a convergent subsequence. The interesting thing happens when you look at f(y) where y is the limit point of such a subsequence. It is the case that as i increases, x_i and y increasingly look the same for longer and longer prefixes of their decimal (binary) expansions. Therefore, f has to do more and more work to tell apart x_i and y, which gives us an argument that there is no bound on the runtime of f(y); i.e., f doesn't terminate for that particular input. (Except, you have to get nitpicky about redundant representations of reals like 0.0099999... vs 0.010000..., but we can always choose the representation of y that suits us: the one that looks more like the x_i's.)

contravariant 6y ago
Yeah I think there are some small problems with your argument, unless it was only meant to illustrate the idea. For the sake of argument let's say we simply input both decimal representations of each number. A program that simply tries to find the first decimal that isn't 9 for a number in [0,1] would take an arbitrary amount of time, but is still total because 1 can be identified in a single step. The problem here is that while the function is total it isn't continuous and so the compactness of the topology is irrelevant. As far as I can tell the article uses some trickery to ensure that computable functions _are_ continuous, in which case it does work.
- cvoss 6y ago
  You're right, it's not a precise line of reasoning. I was considering only computable functions (else "runtime" isn't a meaningful concept) and treating the input domain as actually being the Cantor space, where 0.9999... and 1.0000... are actually distinct values. I just found it helpful to think about the Cantor space in terms of the unit interval.
  - JadeNB 6y ago
    > the Cantor space, where 0.9999... and 1.0000... are actually distinct value What do you mean here? The Cantor set is a subspace, not a cover, of [0, 1]; values in the Cantor set that are the same in [0, 1] are also the same in the Cantor set.
    - thaumasiotes 6y ago
      Sure, the Cantor set is the set of real numbers in [0,1] with trinary expansions that do not contain 1 at any point. A Cantor space is any set that can be mapped to (and from) the Cantor set. The Cantor space is the set of infinitely long bitstrings; instead of a trinary number 0.200220222200..., you'd conceive of the same entity as the string "100110111100...". The mapping is pretty obvious. 0.99999... and 1.0000... are neither of them bitstrings, so it's not really clear what cvoss was thinking of. But it's certainly true that "0999999..." and "1000000..." are distinct strings. Going back to the Cantor set, you'd usually represent 1 as 0.22222222... for obvious reasons of consistency (that is the only format matching the representation of the rest of the set). It would be weird to represent it as 1.000000000...; that would look like you were considering the left end of the Cantor set in [1,2] rather than the right end of the Cantor set in [0,1].

dang 6y ago

If curious see also 2015 https://news.ycombinator.com/item?id=10575626 https://news.ycombinator.com/item?id=10575626

Kednicma 6y ago

One way to imagine this space is as an indexed bank of light switches. Each switch starts out unset, and our goal is to find a configuration on a finite number of switches which will satisfy our search. The search can only check one switch at a time and must commit after each check. This allows a basic nemesis to compute a configuration by running the search repeatedly and rescuing it after each time it fails by checking the last switch checked. A gorgeous immediate consequence is that each search is looking for a solution to a SAT problem! Each SAT solution describes the edge of a region of Cantor space whose elements all have the searched-for property. And thus, while the search can proceed in finite time, it must sadly be NP-complete.

ridiculous_fish 6y ago

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.

ogogmad 6y ago

On a similar vein, you can write functional programs that can do exact Riemann integration: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54.395&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54....

billforsternz 6y ago

Sadly this goes over my head. But, I've got to say, this is a very nice looking website. It's nicely organised on github too.

ogogmad 6y ago

Here is an application of the technique to proving Conway's cosmological theorem: https://www.cs.cmu.edu/~kw/pubs/conway.pdf https://www.cs.cmu.edu/~kw/pubs/conway.pdf