6 ms·
Seemingly impossible functional programs (2007)
- mycroftiv 5y agoI found this post and the code and math so fascinating it changed my life when I found it three years ago. I did not previously understand the capability of computers to work with the abstract logic of infinite sets in a meaningful way and it led me into the world of formalization of mathematics in the dependently typed programming language Agda, which is one of the current activities of the mathematician (Martin Escardo) who wrote this guest blog post.
- bckr 5y agoCan you mention some downstream effects such that your life was changed?
- gijvikvff 5y agoI think they just mean that they wouldn't necessarily have heard about or got into Agda otherwise.
- guerrilla 5y agoNow read their answer :)
- mycroftiv 5y agoI 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 like to figure out a type-theoretical translation of the set-theoretic large cardinal axioms at the level of measurable and beyond.
- agumonkey 5y agoSad to hear about your disability.. but somehow your path in life is fascinating.
- kevinwang 5y agoI find this very interesting, but I'm unable to understand it, so the result still seems impossible to me. Can someone explain how find works if the predicate is something like: return true if and only if every other bit is 1
- alew1 5y agoThe trick is that your predicate can’t be implemented in Haskell, because the predicate itself requires looking at infinitely many elements.
- CraneWorm 5y agoif a predicate depends on finitely many bits then you can exhaustively check whether it is total by enumerating all of it's possible inputs
- thesz 5y agoThe article mentions the inability to decide equality of functions. A paper [1] about proving properties of functional programs shows how to do that modulo halting theorem. E.g., if (\x -> f x == g x) halts we can decide whether f and g are equal. [1] http://xenon.kiam.ru/~roman/doc/2009-Klyuchnikov_Romanenko--Proving_the_Equivalence_of_Higher-Order_Terms_by_Means_of_Supercompilation--slides.pdf 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.
- bmc7505 5y agoOne 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 https://github.com/ilya-klyuchnikov/mrsc [2]: https://github.com/ilya-klyuchnikov/ttlite https://github.com/ilya-klyuchnikov/ttlite
- theamk 5y agoMaybe 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"
- lmm 5y agoYou can do symbolic algebra on symbolic function definitions. What's interesting about this stuff is that it works for "real" functions - plain Haskell functions that we can't inspect the definition of, just call in the normal way (there's no macros or monkeypatching or anything like that going on). It's like being able to use numerical methods but still somehow solve everything exactly.
- octachron 5y agoDeciding 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.
- jiveturkey 5y ago2007
- tyilo 5y agoThe first thing to note that, given a deterministic program that computes a boolean given an infinite bit string will either run in O(1) time for all inputs or will have an input where it doesn't halt. 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).
- quocanh 5y agoCan someone explain to me in plain English what this is? 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?
- Jtsummers 5y agop is a predicate, which is a function mapping elements of some type to true/false (booleans). A total function is a function which is defined for all possible inputs. So a total predicate is a function that maps all possible inputs to either true or false.
- pvillano 5y agoFor real numbers, f(x)=x² is a total function, but g(x)=√x is not, because g is undefined for x<0
- zvorygin 5y agoThank you for asking this, I was having a devil of a time googling what "total" meant in this context.
- pvillano 5y agoYeah, math is riddled with ungoogleables, for example, graph can mean network of nodes or function plot depending on context
- ZoltanAK2 5y agoCantor 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 with seemingly impossible functional programs. Thinking about Cantor space as "the type of infinite binary sequences" is good enough.
- Sniffnoy 5y ago(2007)
- recursive 5y ago> The Maybe type constructor is predefined by Haskell as [...] 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.
- wyager 5y agoProbably targeted at people who use other ML family languages (although this isn't a large crowd).
- dan-robertson 5y ago1. People often struggle to target the things they write well towards a specific group of people and that often leads to this sort of thing. 2. I think when I came across this when it was posted to hacker news 5-10 years ago, I didn’t know any Haskell or any ML language and I didn’t know the maths but the program was small enough and direct enough that I think I managed to puzzle through a lot of it just by trying to match the code to the type signature (though this isn’t really sufficient to get a good feel for what is going on)
- maxiepoo 5y agoA mathematician that has only used a type theory like Coq or Agda and never Haskell.
- ogogmad 5y agoSame ideas as the above: https://en.wikipedia.org/wiki/Computable_analysis https://en.wikipedia.org/wiki/Computable_analysis
- shikoba 5y agoAt first I was doubtful, but when I read the code I understand that the author was just searching exhaustively through a finite set. What a fraud.
- anfelor 5y agoThis 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?
- mycroftiv 5y agoI 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-revised.pdf 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.
- saithound 5y agoYour 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.