Seemingly impossible functional programs (2007)
math.andrej.com
Seemingly impossible functional programs (2007)
1–10 of 46 posts
Re: Seemingly impossible functional programs (2007)
#2The 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--...
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.
Re: Seemingly impossible functional programs (2007)
#3I 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.
Re: Seemingly impossible functional programs (2007)
#4Maybe 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"
Re: Seemingly impossible functional programs (2007)
#5The 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--... Basically, if supercompilation of the expression above results in a huge nested case that has either Tru…
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:
Re: Seemingly impossible functional programs (2007)
#6The 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--... Basically, if supercompilation of the expression above results in a huge nested case that has either Tru…
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?
Re: Seemingly impossible functional programs (2007)
#72007
Re: Seemingly impossible functional programs (2007)
#8The 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).
Re: Seemingly impossible functional programs (2007)
#9Can 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?
Re: Seemingly impossible functional programs (2007)
#10Can 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?
p 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.