21–30 of 46 posts
> 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.
I 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 Esc…
Can you mention some downstream effects such that your life was changed?
The 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 query…
Can 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?
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…
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 bitstring.
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?
The 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 query…
How is not halting O(1)? Wouldn't that be O(∞)?
> Thus if you assume that the function is total and thus does halt, it must run in O(1) time.
Since that's what total means.