Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Seemingly impossible functional programs (2007)

math.andrej.com

Post reply on HN
Print view View original

31–40 of 46 posts

Re: Seemingly impossible functional programs (2007)

#31

Post by anfelor »

This seems like little more than a parlor trick.

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?

Re: Seemingly impossible functional programs (2007)

#32

Post by agumonkey »

mycroftiv wrote: post #22
bckr wrote: post #13

Earlier quoted context omitted.

Can you mention some downstream effects such that your life was changed?

I made the study of mathematical logic and the connections between set theory and type theory and formalization in Agda my full-time focus. Increasing physical disability ended my career as a performing musician a few years ago and I had a life-long interest in philosophical topics connected with infinity. In the past two years I've written over 100,000 lines of Agda code as a product of my learning and research. I'd…

Sad to hear about your disability.. but somehow your path in life is fascinating.

Re: Seemingly impossible functional programs (2007)

#33

Post by mycroftiv »

anfelor wrote: post #31

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

I would suggest you look at more of Escardo's writing and research on related topics. https://www.cs.bham.ac.uk/~mhe/papers/omniscient-journal-rev... is one such paper. The issues of compactness of cantor space in classical and constructive math and the computational interpretation of principles like Brouwer's fan theorem in relation to dependent choice and weak König's lemma is really deep.

Re: Seemingly impossible functional programs (2007)

#34

Post by saithound »

anfelor wrote: post #31

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

Your argument is wrong. The function that encodes every Integer as an element of Cantor, the one you call `p`, has signature `p: Integer -> Cantor`. This means that the compositions `(f.p)` and `(g.p)` are not defined. The compositions in the opposite order, `(p.f)` and `(p.g)`, are defined, but have signature `Integer->Cantor`, which is not in the form `Cantor->y`.

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.

Re: Seemingly impossible functional programs (2007)

#35

Post by Sharlin »

Sharlin wrote: post #26
ZoltanAK2 wrote: post #11

Earlier quoted context omitted.

Cantor space is just the space formed by infinite binary sequences, that is sequences which assumes only the values 0 or 1. Considered as a topological space, Cantor space happens to have the same structure as the Cantor set, a highly disconnected subset of the real numbers that has some at-first-unintuitive properties. But you don't have to understand, or even worry about this correspondence to grasp what's going on…

> Considered as a topological space, Cantor space happens to have the same structure as the Cantor set […] And this is, intuitively, because every element of the (standard) Cantor set can be expressed as a trinary number in the range [0, 1) where every digit is either 0 or 2 (because at every level the middle third is excluded in the construction of the set). That is, a string of exactly two symbols – that is, a bits…

(Late edit: [0, 1] of course rather than [0, 1) since famously 0.222…_3 = 1!)

Re: Seemingly impossible functional programs (2007)

#36

Post by noduerme »

ajkjk wrote: post #6
bmc7505 wrote: post #5

Earlier quoted context omitted.

One of the authors of this work apparently now works on supercompilers at Meta and open sourced some nice tools for equivalence checking based on graph rewriting [1] and constructive type theory [2]. If you're interested in that kind of thing I would recommend checking out his work: [1]: https://github.com/ilya-klyuchnikov/mrsc [2]: https://github.com/ilya-klyuchnikov/ttlite

Are we already calling it 'Meta' unironically?

No one should ever call that thing Meta. We have to draw the line somewhere. Facebook needs to be gratuitously dead named.

Re: Seemingly impossible functional programs (2007)

#37

Post by anfelor »

saithound wrote: post #34
anfelor wrote: post #31

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

Your argument is wrong. The function that encodes every Integer as an element of Cantor, the one you call `p`, has signature `p: Integer -> Cantor`. This means that the compositions `(f.p)` and `(g.p)` are not defined. The compositions in the opposite order, `(p.f)` and `(p.g)`, are defined, but have signature `Integer->Cantor`, which is not in the form `Cantor->y`. Your comment, "the post gets around this by only lo…

You are right, a decoding function is needed. The decoding for my given encoding function is not computable because you need to look at all elements of the sequence to see if the rest are the padded zeros or part of the number (because there is a '1' somewhere). But here is a computable, surjective decoding function: 1. The first bit tells you whether the integer should be positive or negative. 2. Then we parse blocks of ten bits. The first bit tells you whether this block is part of the number ('1') or if we reached the end ('0'). If it is part of the number, then the next nine bits are part of the binary encoding of the integer.

This will not terminate for some sequences (for example the all '1' sequence), but it terminates for all sequences that denote integers. Wouldn't this encoding be valid? (I don't know too much about the halting problem so I might well be wrong here).

> This is not at all what the `equal` function does.

Could you explain what it does do? The way I see it the `find` function constructs a counter-example lazily. The `p` predicate is then applied to this counter-example in `forsome`: `forsome p = p(find(\a -> p a))`. Only if the `p` predicate can determine if the counter-example is valid by looking at a finite amount of digits will the function terminate.

Re: Seemingly impossible functional programs (2007)

#38

Post by TheNewAndy »

anfelor wrote: post #31

This seems like little more than a parlor trick. 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 cantor space is uncountable (which can be seen by prepending '0.' before every binary sequence which gives the real number interval [0,1).)

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.

Re: Seemingly impossible functional programs (2007)

#39

Post by tetromino_ »

saithound wrote: post #34
anfelor wrote: post #31

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

Your argument is wrong. The function that encodes every Integer as an element of Cantor, the one you call `p`, has signature `p: Integer -> Cantor`. This means that the compositions `(f.p)` and `(g.p)` are not defined. The compositions in the opposite order, `(p.f)` and `(p.g)`, are defined, but have signature `Integer->Cantor`, which is not in the form `Cantor->y`. Your comment, "the post gets around this by only lo…

Let's try fixing grandparent's argument: let p be the decoder function, Cantor -> Integer. We can define it as the length of the initial run of zeroes (treat the initial bit as sign). This almost works.

Where it fails is the infinite sequence of zeroes: p would count forever; f.p and g.p are not decidable.

So grandparent's argument in fact shows that OpenCantor -> y does not have decidable equality (where OpenCantor is Cantor with the zero sequence - or by extension, any one computable element - excluded). One special element makes all the difference!

Re: Seemingly impossible functional programs (2007)

#40

Post by octachron »

theamk wrote: post #4

Maybe I am not a enough of a functional programmer, but I don't see what's impossible here? Any symbolic algebra system (like Wolfram Mathematica) can do such derivations, and much more. 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"

Deciding that symbolic expressions are equal is in fact undecidable for even relatively simple sets of symbolic expressions: this is Richardson's theorem.

So this is an example of carefully constrained conditions where equality between all total functions on an infinite set is decidable.

Post reply on HN