12 ms·

Seemingly Impossible Swift Programs

179 points by wool_gather 8y ago

kccqzy 8y ago
Nitpicking but I don't think this is quite right: > The BitSequence type holds infinitely many values. In fact, it holds an unconscionable number of values. It has more values than String does. Assuming UInt is infinite precision and Strings can be infinitely long, there is an easy injection from BitSequence to String, therefore String is at least as equinumerous as BitSequence. If we bend the definition a bit and allow UInt to be infinite precision (which it is not), there's no reason not to allow String to have infinite length as well. Also, the article mentioned multiple times how awesomely large the cardinality of BitSequence is. But in fact, the cardinality is the same as that of the real numbers—both have cardinality $2^{\aleph_0}$. So its size is rather intuitively grasped.
- saagarjha 8y ago
  I think the assumption is that String is a possibly infinitely long ordered list of fixed-size characters, in which case it is countably infinite. Edit: I actually meant "arbitrarily long but finite" instead of "possibly infinitely"; thanks dagw.
  - rcthompson 8y ago
    We're not talking about the size of single values, we're talking about the cardinality of the set of all distinct values of a given type. I.e. "How many different Strings are there?"
    - saagarjha 8y ago
      Yes, I'm aware of that. The set of all languages over a finite alphabet should be countably infinite, since you can list them all. For example, for the alphabet {0, 1} all your strings are just the binary representations of natural numbers, which is countable since ℕ is.
      - dagw 8y ago
        If you only allow arbitrarily long, but finite, strings then the set is countable. If you allow infinitely long strings then the cardinality of that set is uncountable. For a trivial example consider the string representation of every element in ℝ in the alphabet {0-9,.}
        saagarjha 8y ago
        Yes, you're right; this is what I meant, and I see why my current wording is wrong.
    - tomp 8y ago
      Each string is finite, its characters come from a finite set; that’s countably infinite (think of it as integers written in base Unicode). Bitsequences are infinitely long, so that’s uncountably infinite or continuity (think of it as real numbers between 0 and 1, written in binary).
      - rcthompson 8y ago
        The point of the original comment was that if you consider BitSequences to be of infinite length, then for consistency you also have to allow infinite-length strings. Otherwise you're ignoring the limitations of machine representation for one type but not the other, which is comparing apples to oranges.
  - nicky0 8y ago
    *infinite?
    - saagarjha 8y ago
      Yup, sorry. Fixed.
  - pedrosorio 8y ago
    > String is a possibly infinitely long ordered list of fixed-size characters, in which case it is countably finite. BitSequence, as defined in the blogpost, is an "infinitely long ordered list of fixed-size characters" (where the size is 1 bit in this case) - the set of all BitSequence values is infinite - and uncountable. By the same logic, the set of infinite strings is also uncountable (as the GP says, it's trivial to do an injection from BitSequence to infinite strings, so it can't have lower cardinality).
    - saagarjha 8y ago
      Yes, you're right. I have amended my comment; I had meant to say that Strings must have finite length. The "meat" of my comment was an argument that Strings could not infinitely long, which was exactly the opposite of what I actually ended up saying ;)
    - hawkice 8y ago
      It's not uncountable because they have to be computable, which makes them countable again.
    - nicky0 8y ago
      I think there is some confusion of terminology going on here. What you are calling "uncountable" is what is also known as "countably infinite".
      - pedrosorio 8y ago
        There is no confusion here. The set of infinite strings is not countably infinite, it has cardinality larger than the set of integers.
        brianpgordon 8y ago
        Why? If your alphabet is [0-9] then it seems like your set is just the integers, and those are countably infinite. This case is even more restricted, where you only have two elements in the alphabet. So where does the continuum come in?
- DougBTX 8y ago
  > Assuming UInt is infinite precision and Strings can be infinitely long, there is an easy injection from BitSequence to String, therefore String is at least as equinumerous as BitSequence. You’re right that a particular series of bits can be mapped to a string, but here the article is talking about the function that produces the bit sequence not the bit sequence itself. There are an infinite number of functions that can create a particular bit sequence, and each bit sequence can be mapped to a single string, so there must be more functions than strings.
  - kccqzy 8y ago
    > The BitSequence type holds infinitely many values. In fact, it holds an unconscionable number of values. It has more values than String does. In the last sentence, the word "it" seems to refer to "the BitSequence type" and not a function that produces it.
  - saagarjha 8y ago
    > There are an infinite number of functions that can create a particular bit sequence, and each bit sequence can be mapped to a single string, so there must be more functions than strings. I don't think this logic works. For example, there are an infinite number of "rational numbers" of the form np/p where n, p ∈ ℤ, and each of these can be mapped to a single integer (namely, n). But there are not more these "rational numbers" than integers.
    - kccqzy 8y ago
      When you have an injection from A to B, you only know that B is at least as equinumerous as A. Maybe their cardinality is the same, and maybe the cardinality of B is strictly bigger. For your example, we can construct an injection from rational numbers to integers, as well as an injection from integers to rational numbers. Therefore, by the Schröder–Bernstein theorem they are equinumerous.
  - ulucs 8y ago
    Considering cardinalities, functions and strings are equal. Using javascript notation, ‘fn => fn.toString()’ is an injective function from functions to strings and ‘str => () => str’ is an injective function from strings to functions.
- omaranto 8y ago
  I think that probably in Swift each individual string is required to be of finite length, as in most programming languages. The set of finite (but arbitrary) length strings drawn from a finite set of characters is countable. On the other hand this type BitSequence (pretending UInt contains all non-negative sequences) is the set of all countable infinite sequences of bits. That set, as you explained, has the cardinality of the continuum.
- JadeNB 8y ago
  > > The BitSequence type holds infinitely many values. In fact, it holds an unconscionable number of values. It has more values than String does. I like the typo of 'unconscionable' for 'uncountable'.
kccqzy 8y ago
I have translated the pretty long Swift code belabored with manual laziness handling into Haskell where lists are inherently lazy: type BitSequence = [Bool] allSatisfy :: (BitSequence -> Bool) -> Bool allSatisfy p = not (anySatisfy (not . p)) anySatisfy :: (BitSequence -> Bool) -> Bool anySatisfy p = p (find p) find :: (BitSequence -> Bool) -> BitSequence find p = if anySatisfy (\s -> p (False : s)) then False : find (\s -> p (False : s)) else True : find (\s -> p (True : s)) The code still works the same. But now, it is clearer what actually happens. The lexical call chain goes like this: anySatisfy p ===> find p ===> anySatisfy (\s -> p (False : s)) ===> find (\s -> p (False : s)) ===> anySatisfy (\s -> (\s -> p (False : s)) (False : s)) ===> find (\s -> (\s -> p (False : s)) (False : s)) === (by alpha conversion) find (\s -> (\s1 -> p (False : s1)) (False : s)) === (by beta reduction) find (\s -> p (False : False : s)) where I used the long arrow to mean a deeper lexical call chain, and triple-equal to mean a single step of reduction and/or . In other words, as long as the given predicate p consumes a finite prefix of the infinite bit sequence to produce a result, this will successfully return a result. Which is quite intuitive because the function is essentially doing an exhaustive search. It has nothing to do with topology or continuous functions or compactness, IMO. It also has nothing to do with Curry–Howard correspondence. Here's an example when the function fails to terminate: anySatisfy and Here's another example: let parity (False : s) = parity s; parity (True : s) = not (parity s) in anySatisfy parity
- repsilat 8y ago
  > Here's an example when the function fails to terminate: I figured this seemed too good to be true. In fact, isn't there a simple reduction to the halting problem? Make a "sequence" i -> M halts in i steps for an arbitrary Turing Machine `M`. You can implement the "bit lookups" by simulating `M`. The author says their Swift code can run `anySatisfy` on this "sequence" in finite time, right? EDIT: quoted at the top, but afaict not mentioned later, the article says, >> It is well known that it is impossible to define equality between arbitrary functions. However, there is a large class of functions for which we can determine equality It would have been nice if the author had been explicit about the class of functions for which their program terminates.
svat 8y ago
See also “Seemingly impossible functional programs” by Martin Escardo, from 2007 ([1], also at [2]). It covers similar ground and is referenced at the bottom of the article (along with three other references also by Martín Escardó), but I thought it worth mentioning explicitly because I remember reading it many years ago and finding it really fun. [1]: http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ http://math.andrej.com/2007/09/28/seemingly-impossible-funct... [2]: http://www.cs.bham.ac.uk/~mhe/papers/seemingly-impossible.html http://www.cs.bham.ac.uk/~mhe/papers/seemingly-impossible.ht...
nathan_f77 8y ago
That was really interesting! > This is completely impossible to do with Int’s and String’s, but here we have done it for BitSequence I'm still confused by this part. Can't you convert any Int or String value into a BitSequence?
- fmap 8y ago
  He means that it's impossible to write such a function from the natural numbers. It's possible for all finite types such as UInt in Swift. In general, you can do this exhaustive search with any "compact" type and there are a lot of compact types. In particular, the (total continuous) functions from a discrete (i.e. a type with decidable equality) into a compact type are compact. And as the article shows, the (total continuous) functions from a compact into a discrete type are discrete. Together with the observation that the type of natural numbers is discrete and that every finite type is compact and discrete already gives you infinitely many compact types to play with. One caveat with this whole work (which goes back to Martin Escardo by the way) is that this doesn't work with general recursion. E.g. in a language with general recursion you can write a program kleene : (nat -> bool) -> bool which computes the paths in the Kleene tree, where roughly "all total computable paths are terminating, but all uncomputable paths diverge". However, if you have a (total) language with, e.g., only structural recursion, everything works out and you can apply this epsilon operator to arbitrary programs.
  - nathan_f77 8y ago
    Thanks for your reply! I think I understood some of your comment, but got very lost at the end. I don't know anything about: Kleene trees [1], "total" languages [2], general recursion vs structural recursion [3], or epsilon operators [4]. (But I've looked those up and provided some links.) I think I understood some of the first paragraph. I'll have to do some mathematics and computer science courses on Khan Academy. [1] https://en.wikipedia.org/wiki/Kleene%E2%80%93Brouwer_order https://en.wikipedia.org/wiki/Kleene%E2%80%93Brouwer_order [2] https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [3] https://stackoverflow.com/questions/14268749/how-does-structural-recursion-differ-from-generative-recursion https://stackoverflow.com/questions/14268749/how-does-struct... [4] https://en.wikipedia.org/wiki/Epsilon_calculus https://en.wikipedia.org/wiki/Epsilon_calculus This seems like a very advanced topic!
n4r9 8y ago
Hmm, some questions from someone who isn't familiar with Swift or much functional programming: - What does this have to do with Swift? Other commenters seem to agree that Haskell would be more appropriate. - What does this have to do with functional programming? As far as I can tell, an algorithm about bitstrings has been wrapped up and reframed in terms of types. Could you not do this in C without too much headache? - The recursion aspect confuses me a bit; is it possible to "find" a predicate like "all indices of the bitstring are 1"? Or is that not an allowed type of predicate? - Again with the recursion, how does the "find" procedure know to terminate if no viable bit string exists? EDIT: I should have read kccqzy's post more carefully. I believe it answers the third and fourth questions.
- saagarjha 8y ago
  For the first two: not much, and somewhat. The commenters are correct that this logic is much more easily expressed in Haskell, since it has better support for this kind of programming. Swift is able to do this because it has lazy evaluation as a opt-in feature as well as the parts of the type system that matter; I don’t think you would be able to port this to C easily.
- kccqzy 8y ago
  For your third question, that predicate doesn't work. For your fourth question, I didn't quite explain that but it's due to laziness. All of this recursion happens inside a lazy function argument. So if p chooses to return True without inspecting more values from the bit sequence, the recursion is then stopped.
tylerhou 8y ago
> It’s so large that it can hold an infinite number of disjoint copies of the natural numbers inside it! Nit: you can embed infinite copies of the natural numbers inside the natural numbers as well, with room to spare. Consider the primes raised to integer powers.
srikz 8y ago
Off topic: DeMorgan's law > the negation of a disjunction is the conjunction of the negations As a non-English speaker I hated this definition until someone told me to remember > 'break the line, change the sign'. This is of course referring the representation in boolean algebra, where, NOT(A AND B) is represented with a single long horizontal line on top of (A AND B). This becomes NOT(A) OR NOT(B), i.e., Ā | B̄ according to DeMorgan's law.
- giornogiovanna 8y ago
  De Morgan's law is just "not all true <=> at least one's false". I'm not sure why people complicate it beyond that.
  - blattimwind 8y ago
    In university I had a course (curse?) called "logic in formal systems" (or something like that); I doubt many using only the course's materials truly understood the logic principles demonstrated there. Coincidentally, the course insisted on using ∧, ∨, ¬ etc., while another course also dabbling in a lot of logic using natural symbols was far better in terms of presentation and explanations. (To this day I have to look ∧, ∨, con- and disjunction up to be sure which is which).
    - Izkata 8y ago
      > To this day I have to look ∧, ∨, con- and disjunction up to be sure which is which Tip: ∧ is shaped like the "A" in "And". Hopefully others know tricks for the other symbols.
      - blattimwind 8y ago
        > Tip: ∧ is shaped like the "A" in "And". Meanwhile ∨ is shaped like the "U" in "Und" ...
Skeime 8y ago
Here is a more imperative version (using exceptions): The assumption is (as in the article) that each predicate terminates for every bit sequence and that the predicates are actual functions, i.e. they have no state. Also, predicates don’t catch exceptions. We can implement find as follows: Start with n = 0 and generate the bit sequences with all prefixes of length n. Have them throw an exception if somebody tries to access an index past that prefix. This way, you get finitely many partial bit sequences. Apply the predicate to all these sequences. There are three cases: - The predicate returns true for one of the partial sequences. Because it doesn’t catch exceptions, it only looked at values within the prefix. Hence, the result of the predicate doesn’t change if we change the rest of the sequence—for example, we can set the rest of the sequence to 0 and we have found a sequence that satisfies the predicate. - The predicte returns false for all our partial sequences. Similarly to the case above, the result does not depend on bits beyond the prefix, so no matter what we do, we will not find a sequence satisfying the predicate and we can return any sequence (by the definition of find, it returns any sequence if the predicate is unsatisfiable). - For some of our partial sequences, we get an exception. Then we increase n and try again. This algorithm has to terminate: if it doesn’t, we get the third case each time. But taking the bit sequence that we get by always extending our prefix on a path that keeps throwing exceptions, we get a bit sequence on which our predicate does not terminate, contrary to our assumption that it always does.
mrmr1993 8y ago
> It’s going to seem incredible, almost magical, but be assured you there are no tricks involved. The trick involved is: BitSequence.find is a naïve brute-force search, but the predicates only check n bits (for some n), and laziness ensures that at most n bits are generated. We run into the expected problems if n is large, or there is no such n. For example, func evenNumberOfOnesAtStart(_ s : BitSequence) { return (s.atIndex(0) == .zero || (s.atIndex(1) == .one && evenNumberOfOnes(BitSequence { s.atIndex($0 + 2) }))) } evenNumberOfOnesAtStart == evenNumberOfOnesAtStart will never terminate. (Disclaimer: I don't write Swift.) While it's nice to try smuggling in some mathematics at the end, I think a better conclusion for the article to draw is: if you ask a computer to do a brute-force search on some fixed number of bits, it will do it, even where has to compute this number of bits itself along the way.
- Spivak 8y ago
  I think there might be a clearer explanation. If a predicate only looks a finite number, n, of bits of a bitsequence then you can brute-force search the space containing the (2^n) sequences shorter than n. And a predicate can't possibly look at infinitely many bits of a bitsequence as the function which resolves that predicate would never terminate.
  - mrmr1993 8y ago
    Agreed. (Although it's (2^m) sequences, where m is the largest index of the n.)
riskable 8y ago
This article does a great job at pointing out just how needlessly difficult computer science makes itself when it doesn't have to. Example: !(a || b) == (!a && !b) `a` and `b`. They're meant to represent, well anything really but to the average person (or weirdos like me) it would be infinitely easier to understand if the author wrote it like this: !(Bob || Sally) == (!Bob && !Sally) I don't know why but whenever I encounter single-characters-as-math-variables in computer science I have to spend far more time unpacking such statements into things my brain can understand. It is so much easier if such statements are written as nouns that describe actual things. I remember having a hard time working with C for loops until a friend of mine wrote one like this: for (int number = 0; number < 10; number = number + 1) Suddenly it all made sense! I am not alone in this! I have taught programming to kids and others who have struggled to learn programming and this seems to be how normal people think. Note: We, as a geeky community are not normal. I just have a strange exception in that at least one little part of me thinks like a normal person and that is with "what we name things" :)
- chrisseaton 8y ago
  I can't understand any point to writing 'a' rather than writing 'Sally'. What practical difference does it make?
  - Ensorceled 8y ago
    That’s the entire point of their post, it doesn’t make a practical difference to you but does to other people.
    - deleted 8y ago
      [deleted]
    - chrisseaton 8y ago
      I know that, but I don't know what it is that makes a difference to them and I'm interested in understanding it.
      - 8y ago
xondono 8y ago
Noob here woth a doubt: “Incredible! We are exhaustively searching an uncountably infinite space in finite time” Isn’t this like a long stretch? Once lazy evaluation is introduced he is pretty much checking until a first hit happens, isn’t he? What would happen if I call the function with predicate ‘x == one AND x == zero’?
- blattimwind 8y ago
  > What would happen if I call the function with predicate ‘x == one AND x == zero’? Then the algorithm never halts.
- jozefg 8y ago
  This algorithm is only total if the predicates supplied are total. Since `x == one AND x == zero` is not total the algorithm will diverge. It will not return the incorrect answer though.
ken 8y ago
He lost me when he started talking about the Halting Problem. How is checking all Swift.String or Swift.Int values equivalent to that? There are a lot of Swift.Int values to check (2^64, on a 64-bit platform), and even more Swift.String values (every combination of characters up to that length), but simply being infeasibly slow to run on your Pentium "in a reasonable amount of time" doesn't mean it's an "impossible function to implement, and also equivalent to the halting problem". We could easily write a function to enumerate all Swift.Int values (though it might take 100 years to run). He throws out the parenthetical remark "it’s best to think of Int as modeling the infinite set of all integers" without explanation. When you're discussing whether something is theoretically impossible or not, thinking of a finite set as equivalent to an infinite set is brushing over a pretty major distinction.
- joshuamorton 8y ago
  With Int you may be right. But there are an infinite number of strings (and indeed every Turing machine may be represented as a String in swift), so it is indeed related to the halting problem.
  - wtetzner 8y ago
    Swift strings don't have a maximum length? Are they nul-terminated?
  - ken 8y ago
    Swift.String is composed of a finite set of symbols, with a finite maximum length. How can you create an infinite number of these? The article ignores the distinction in many places, but "String" in a Swift function means "the Swift.String type", not "an abstract string type like those used to represent Turing machine state".
    - timjver 8y ago
      You're not wrong, but the author's code does in no way rely on the fact that you could theoretically iterate over all the valid Int values in Swift, so it would have made no difference if the Int type was somehow truly infinite. And the author clearly acknowledges this: >it’s best to think of Int as modeling the infinite set of all integers
SeanLuke 8y ago
Apple's been in this game a long time. NewtonScript had a powerful function called "IsHalting". See Page 23-84 of http://www.newted.org/download/manuals/NewtonProgrammerRef20.pdf http://www.newted.org/download/manuals/NewtonProgrammerRef20...
keithalewis 8y ago
Balderdash, as others have more graciously pointed out. How wrong do you have to be before having your nonsense deleted from HN?
- wool_gather 8y ago
  Even if it is balderdash, isn't there value in analyzing(/refuting) it? I submitted the post (it's not mine) because I was interested in hearing people with more maths than I have expand/comment on it -- perhaps even people who had read the original papers. If there's something particular in the post that you find problematic, I personally am all ears.
  - keithalewis 8y ago
    The author is correct that checking if two functions having infinite domains are equal is often impossible. He also has correct statements of some mathematical theorems. But people in this thread have provided counterexamples to his claim. That means he needs to fix the mistakes he made. If you are interested in what serious mathematicians have to say on this topic see https://homotopytypetheory.org/ https://homotopytypetheory.org/.
    - jozefg 8y ago
      It is possible in certain cases, that's the point of the article. One of the contributors to HoTT is the author of the paper introducing these algorithms :)
aaaaaaaaaab 8y ago
I don't get it. What prevents us from doing the exact same approach for the natural numbers? I.e. represent the naturals lazily via the successor function and use the same exhaustive search as the OP for BitSequence. Of course if the predicate doesn't stop evaluating successor(x) for any finite x then we're out of luck and the computation doesn't halt, but this caveat also holds for OP's BitSequence, as others have pointed out in this thread...
- jozefg 8y ago
  So this article shows how to check equality on `(nat -> bool) -> bool`. Your question, I think, is to figure out how to check `nat -> bool` for equality. The issue is that there are more operations we can do with `nat`, more properties we can check, than there are with `nat -> bool`. With `nat -> bool` we can basically check `i` indices and so the behavior of any predicate `(nat -> bool) -> bool` is basically determined by the first `i` indices. And that's finite. This algorithm is basically implicitly finding the indices considered by the supplied predicate and then brute-forcing all those entries. With `nat` there's no such finite cut off point. It's never the case that it suffices to test a predicate `nat -> bool` on finitely many entries to fully determine it. So we cannot do the same brute force search.
  - aaaaaaaaaab 8y ago
    But a natural number can be viewed as a function from the natural numbers to {0, 1} via its binary expansion. There's a trivial isomorphism between the natural numbers and binary sequences with finitely many ones, so a predicate of type `nat -> bool` can be viewed as a predicate of type `(nat -> bool) -> bool`.
    - jozefg 8y ago
      It's not an isomorphism though, it misses the always true map. This means that many predicates on nat do not terminate on nat -> bool.

179 points by wool_gather 8y ago

Nitpicking but I don't think this is quite right: > The BitSequence type holds infinitely many values. In fact, it holds an unconscionable number of values. It has more values than String does. Assuming UInt is infinite precision and Strings can be infinitely long, there is an easy injection from BitSequence to String, therefore String is at least as equinumerous as BitSequence. If we bend the definition a bit and allow UInt to be infinite precision (which it is not), there's no reason not to allow String to have infinite length as well. Also, the article mentioned multiple times how awesomely large the cardinality of BitSequence is. But in fact, the cardinality is the same as that of the real numbers—both have cardinality $2^{\aleph_0}$. So its size is rather intuitively grasped.

saagarjha 8y ago
I think the assumption is that String is a possibly infinitely long ordered list of fixed-size characters, in which case it is countably infinite. Edit: I actually meant "arbitrarily long but finite" instead of "possibly infinitely"; thanks dagw.
- rcthompson 8y ago
  We're not talking about the size of single values, we're talking about the cardinality of the set of all distinct values of a given type. I.e. "How many different Strings are there?"
  - saagarjha 8y ago
    Yes, I'm aware of that. The set of all languages over a finite alphabet should be countably infinite, since you can list them all. For example, for the alphabet {0, 1} all your strings are just the binary representations of natural numbers, which is countable since ℕ is.
    - dagw 8y ago
      If you only allow arbitrarily long, but finite, strings then the set is countable. If you allow infinitely long strings then the cardinality of that set is uncountable. For a trivial example consider the string representation of every element in ℝ in the alphabet {0-9,.}
      - saagarjha 8y ago
        Yes, you're right; this is what I meant, and I see why my current wording is wrong.
  - tomp 8y ago
    Each string is finite, its characters come from a finite set; that’s countably infinite (think of it as integers written in base Unicode). Bitsequences are infinitely long, so that’s uncountably infinite or continuity (think of it as real numbers between 0 and 1, written in binary).
    - rcthompson 8y ago
      The point of the original comment was that if you consider BitSequences to be of infinite length, then for consistency you also have to allow infinite-length strings. Otherwise you're ignoring the limitations of machine representation for one type but not the other, which is comparing apples to oranges.
- nicky0 8y ago
  *infinite?
  - saagarjha 8y ago
    Yup, sorry. Fixed.
- pedrosorio 8y ago
  > String is a possibly infinitely long ordered list of fixed-size characters, in which case it is countably finite. BitSequence, as defined in the blogpost, is an "infinitely long ordered list of fixed-size characters" (where the size is 1 bit in this case) - the set of all BitSequence values is infinite - and uncountable. By the same logic, the set of infinite strings is also uncountable (as the GP says, it's trivial to do an injection from BitSequence to infinite strings, so it can't have lower cardinality).
  - saagarjha 8y ago
    Yes, you're right. I have amended my comment; I had meant to say that Strings must have finite length. The "meat" of my comment was an argument that Strings could not infinitely long, which was exactly the opposite of what I actually ended up saying ;)
  - hawkice 8y ago
    It's not uncountable because they have to be computable, which makes them countable again.
  - nicky0 8y ago
    I think there is some confusion of terminology going on here. What you are calling "uncountable" is what is also known as "countably infinite".
    - pedrosorio 8y ago
      There is no confusion here. The set of infinite strings is not countably infinite, it has cardinality larger than the set of integers.
      - brianpgordon 8y ago
        Why? If your alphabet is [0-9] then it seems like your set is just the integers, and those are countably infinite. This case is even more restricted, where you only have two elements in the alphabet. So where does the continuum come in?
DougBTX 8y ago
> Assuming UInt is infinite precision and Strings can be infinitely long, there is an easy injection from BitSequence to String, therefore String is at least as equinumerous as BitSequence. You’re right that a particular series of bits can be mapped to a string, but here the article is talking about the function that produces the bit sequence not the bit sequence itself. There are an infinite number of functions that can create a particular bit sequence, and each bit sequence can be mapped to a single string, so there must be more functions than strings.
- kccqzy 8y ago
  > The BitSequence type holds infinitely many values. In fact, it holds an unconscionable number of values. It has more values than String does. In the last sentence, the word "it" seems to refer to "the BitSequence type" and not a function that produces it.
- saagarjha 8y ago
  > There are an infinite number of functions that can create a particular bit sequence, and each bit sequence can be mapped to a single string, so there must be more functions than strings. I don't think this logic works. For example, there are an infinite number of "rational numbers" of the form np/p where n, p ∈ ℤ, and each of these can be mapped to a single integer (namely, n). But there are not more these "rational numbers" than integers.
  - kccqzy 8y ago
    When you have an injection from A to B, you only know that B is at least as equinumerous as A. Maybe their cardinality is the same, and maybe the cardinality of B is strictly bigger. For your example, we can construct an injection from rational numbers to integers, as well as an injection from integers to rational numbers. Therefore, by the Schröder–Bernstein theorem they are equinumerous.
- ulucs 8y ago
  Considering cardinalities, functions and strings are equal. Using javascript notation, ‘fn => fn.toString()’ is an injective function from functions to strings and ‘str => () => str’ is an injective function from strings to functions.
omaranto 8y ago
I think that probably in Swift each individual string is required to be of finite length, as in most programming languages. The set of finite (but arbitrary) length strings drawn from a finite set of characters is countable. On the other hand this type BitSequence (pretending UInt contains all non-negative sequences) is the set of all countable infinite sequences of bits. That set, as you explained, has the cardinality of the continuum.
JadeNB 8y ago
> > The BitSequence type holds infinitely many values. In fact, it holds an unconscionable number of values. It has more values than String does. I like the typo of 'unconscionable' for 'uncountable'.

kccqzy 8y ago

I have translated the pretty long Swift code belabored with manual laziness handling into Haskell where lists are inherently lazy: type BitSequence = [Bool] allSatisfy :: (BitSequence -> Bool) -> Bool allSatisfy p = not (anySatisfy (not . p)) anySatisfy :: (BitSequence -> Bool) -> Bool anySatisfy p = p (find p) find :: (BitSequence -> Bool) -> BitSequence find p = if anySatisfy (\s -> p (False : s)) then False : find (\s -> p (False : s)) else True : find (\s -> p (True : s)) The code still works the same. But now, it is clearer what actually happens. The lexical call chain goes like this: anySatisfy p ===> find p ===> anySatisfy (\s -> p (False : s)) ===> find (\s -> p (False : s)) ===> anySatisfy (\s -> (\s -> p (False : s)) (False : s)) ===> find (\s -> (\s -> p (False : s)) (False : s)) === (by alpha conversion) find (\s -> (\s1 -> p (False : s1)) (False : s)) === (by beta reduction) find (\s -> p (False : False : s)) where I used the long arrow to mean a deeper lexical call chain, and triple-equal to mean a single step of reduction and/or . In other words, as long as the given predicate p consumes a finite prefix of the infinite bit sequence to produce a result, this will successfully return a result. Which is quite intuitive because the function is essentially doing an exhaustive search. It has nothing to do with topology or continuous functions or compactness, IMO. It also has nothing to do with Curry–Howard correspondence. Here's an example when the function fails to terminate: anySatisfy and Here's another example: let parity (False : s) = parity s; parity (True : s) = not (parity s) in anySatisfy parity

repsilat 8y ago
> Here's an example when the function fails to terminate: I figured this seemed too good to be true. In fact, isn't there a simple reduction to the halting problem? Make a "sequence" i -> M halts in i steps for an arbitrary Turing Machine `M`. You can implement the "bit lookups" by simulating `M`. The author says their Swift code can run `anySatisfy` on this "sequence" in finite time, right? EDIT: quoted at the top, but afaict not mentioned later, the article says, >> It is well known that it is impossible to define equality between arbitrary functions. However, there is a large class of functions for which we can determine equality It would have been nice if the author had been explicit about the class of functions for which their program terminates.

svat 8y ago

See also “Seemingly impossible functional programs” by Martin Escardo, from 2007 ([1], also at [2]). It covers similar ground and is referenced at the bottom of the article (along with three other references also by Martín Escardó), but I thought it worth mentioning explicitly because I remember reading it many years ago and finding it really fun. [1]: http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ http://math.andrej.com/2007/09/28/seemingly-impossible-funct... [2]: http://www.cs.bham.ac.uk/~mhe/papers/seemingly-impossible.html http://www.cs.bham.ac.uk/~mhe/papers/seemingly-impossible.ht...

nathan_f77 8y ago

That was really interesting! > This is completely impossible to do with Int’s and String’s, but here we have done it for BitSequence I'm still confused by this part. Can't you convert any Int or String value into a BitSequence?

fmap 8y ago
He means that it's impossible to write such a function from the natural numbers. It's possible for all finite types such as UInt in Swift. In general, you can do this exhaustive search with any "compact" type and there are a lot of compact types. In particular, the (total continuous) functions from a discrete (i.e. a type with decidable equality) into a compact type are compact. And as the article shows, the (total continuous) functions from a compact into a discrete type are discrete. Together with the observation that the type of natural numbers is discrete and that every finite type is compact and discrete already gives you infinitely many compact types to play with. One caveat with this whole work (which goes back to Martin Escardo by the way) is that this doesn't work with general recursion. E.g. in a language with general recursion you can write a program kleene : (nat -> bool) -> bool which computes the paths in the Kleene tree, where roughly "all total computable paths are terminating, but all uncomputable paths diverge". However, if you have a (total) language with, e.g., only structural recursion, everything works out and you can apply this epsilon operator to arbitrary programs.
- nathan_f77 8y ago
  Thanks for your reply! I think I understood some of your comment, but got very lost at the end. I don't know anything about: Kleene trees [1], "total" languages [2], general recursion vs structural recursion [3], or epsilon operators [4]. (But I've looked those up and provided some links.) I think I understood some of the first paragraph. I'll have to do some mathematics and computer science courses on Khan Academy. [1] https://en.wikipedia.org/wiki/Kleene%E2%80%93Brouwer_order https://en.wikipedia.org/wiki/Kleene%E2%80%93Brouwer_order [2] https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [3] https://stackoverflow.com/questions/14268749/how-does-structural-recursion-differ-from-generative-recursion https://stackoverflow.com/questions/14268749/how-does-struct... [4] https://en.wikipedia.org/wiki/Epsilon_calculus https://en.wikipedia.org/wiki/Epsilon_calculus This seems like a very advanced topic!

n4r9 8y ago

Hmm, some questions from someone who isn't familiar with Swift or much functional programming: - What does this have to do with Swift? Other commenters seem to agree that Haskell would be more appropriate. - What does this have to do with functional programming? As far as I can tell, an algorithm about bitstrings has been wrapped up and reframed in terms of types. Could you not do this in C without too much headache? - The recursion aspect confuses me a bit; is it possible to "find" a predicate like "all indices of the bitstring are 1"? Or is that not an allowed type of predicate? - Again with the recursion, how does the "find" procedure know to terminate if no viable bit string exists? EDIT: I should have read kccqzy's post more carefully. I believe it answers the third and fourth questions.

saagarjha 8y ago
For the first two: not much, and somewhat. The commenters are correct that this logic is much more easily expressed in Haskell, since it has better support for this kind of programming. Swift is able to do this because it has lazy evaluation as a opt-in feature as well as the parts of the type system that matter; I don’t think you would be able to port this to C easily.
kccqzy 8y ago
For your third question, that predicate doesn't work. For your fourth question, I didn't quite explain that but it's due to laziness. All of this recursion happens inside a lazy function argument. So if p chooses to return True without inspecting more values from the bit sequence, the recursion is then stopped.

tylerhou 8y ago

> It’s so large that it can hold an infinite number of disjoint copies of the natural numbers inside it! Nit: you can embed infinite copies of the natural numbers inside the natural numbers as well, with room to spare. Consider the primes raised to integer powers.

srikz 8y ago

Off topic: DeMorgan's law > the negation of a disjunction is the conjunction of the negations As a non-English speaker I hated this definition until someone told me to remember > 'break the line, change the sign'. This is of course referring the representation in boolean algebra, where, NOT(A AND B) is represented with a single long horizontal line on top of (A AND B). This becomes NOT(A) OR NOT(B), i.e., Ā | B̄ according to DeMorgan's law.

giornogiovanna 8y ago
De Morgan's law is just "not all true <=> at least one's false". I'm not sure why people complicate it beyond that.
- blattimwind 8y ago
  In university I had a course (curse?) called "logic in formal systems" (or something like that); I doubt many using only the course's materials truly understood the logic principles demonstrated there. Coincidentally, the course insisted on using ∧, ∨, ¬ etc., while another course also dabbling in a lot of logic using natural symbols was far better in terms of presentation and explanations. (To this day I have to look ∧, ∨, con- and disjunction up to be sure which is which).
  - Izkata 8y ago
    > To this day I have to look ∧, ∨, con- and disjunction up to be sure which is which Tip: ∧ is shaped like the "A" in "And". Hopefully others know tricks for the other symbols.
    - blattimwind 8y ago
      > Tip: ∧ is shaped like the "A" in "And". Meanwhile ∨ is shaped like the "U" in "Und" ...

Skeime 8y ago

Here is a more imperative version (using exceptions): The assumption is (as in the article) that each predicate terminates for every bit sequence and that the predicates are actual functions, i.e. they have no state. Also, predicates don’t catch exceptions. We can implement find as follows: Start with n = 0 and generate the bit sequences with all prefixes of length n. Have them throw an exception if somebody tries to access an index past that prefix. This way, you get finitely many partial bit sequences. Apply the predicate to all these sequences. There are three cases: - The predicate returns true for one of the partial sequences. Because it doesn’t catch exceptions, it only looked at values within the prefix. Hence, the result of the predicate doesn’t change if we change the rest of the sequence—for example, we can set the rest of the sequence to 0 and we have found a sequence that satisfies the predicate. - The predicte returns false for all our partial sequences. Similarly to the case above, the result does not depend on bits beyond the prefix, so no matter what we do, we will not find a sequence satisfying the predicate and we can return any sequence (by the definition of find, it returns any sequence if the predicate is unsatisfiable). - For some of our partial sequences, we get an exception. Then we increase n and try again. This algorithm has to terminate: if it doesn’t, we get the third case each time. But taking the bit sequence that we get by always extending our prefix on a path that keeps throwing exceptions, we get a bit sequence on which our predicate does not terminate, contrary to our assumption that it always does.

mrmr1993 8y ago

> It’s going to seem incredible, almost magical, but be assured you there are no tricks involved. The trick involved is: BitSequence.find is a naïve brute-force search, but the predicates only check n bits (for some n), and laziness ensures that at most n bits are generated. We run into the expected problems if n is large, or there is no such n. For example, func evenNumberOfOnesAtStart(_ s : BitSequence) { return (s.atIndex(0) == .zero || (s.atIndex(1) == .one && evenNumberOfOnes(BitSequence { s.atIndex($0 + 2) }))) } evenNumberOfOnesAtStart == evenNumberOfOnesAtStart will never terminate. (Disclaimer: I don't write Swift.) While it's nice to try smuggling in some mathematics at the end, I think a better conclusion for the article to draw is: if you ask a computer to do a brute-force search on some fixed number of bits, it will do it, even where has to compute this number of bits itself along the way.

Spivak 8y ago
I think there might be a clearer explanation. If a predicate only looks a finite number, n, of bits of a bitsequence then you can brute-force search the space containing the (2^n) sequences shorter than n. And a predicate can't possibly look at infinitely many bits of a bitsequence as the function which resolves that predicate would never terminate.
- mrmr1993 8y ago
  Agreed. (Although it's (2^m) sequences, where m is the largest index of the n.)

riskable 8y ago

This article does a great job at pointing out just how needlessly difficult computer science makes itself when it doesn't have to. Example: !(a || b) == (!a && !b) `a` and `b`. They're meant to represent, well anything really but to the average person (or weirdos like me) it would be infinitely easier to understand if the author wrote it like this: !(Bob || Sally) == (!Bob && !Sally) I don't know why but whenever I encounter single-characters-as-math-variables in computer science I have to spend far more time unpacking such statements into things my brain can understand. It is so much easier if such statements are written as nouns that describe actual things. I remember having a hard time working with C for loops until a friend of mine wrote one like this: for (int number = 0; number < 10; number = number + 1) Suddenly it all made sense! I am not alone in this! I have taught programming to kids and others who have struggled to learn programming and this seems to be how normal people think. Note: We, as a geeky community are not normal. I just have a strange exception in that at least one little part of me thinks like a normal person and that is with "what we name things" :)

chrisseaton 8y ago
I can't understand any point to writing 'a' rather than writing 'Sally'. What practical difference does it make?
- Ensorceled 8y ago
  That’s the entire point of their post, it doesn’t make a practical difference to you but does to other people.
  - deleted 8y ago
    [deleted]
  - chrisseaton 8y ago
    I know that, but I don't know what it is that makes a difference to them and I'm interested in understanding it.
    - 8y ago

xondono 8y ago

Noob here woth a doubt: “Incredible! We are exhaustively searching an uncountably infinite space in finite time” Isn’t this like a long stretch? Once lazy evaluation is introduced he is pretty much checking until a first hit happens, isn’t he? What would happen if I call the function with predicate ‘x == one AND x == zero’?

blattimwind 8y ago
> What would happen if I call the function with predicate ‘x == one AND x == zero’? Then the algorithm never halts.
jozefg 8y ago
This algorithm is only total if the predicates supplied are total. Since `x == one AND x == zero` is not total the algorithm will diverge. It will not return the incorrect answer though.

ken 8y ago

He lost me when he started talking about the Halting Problem. How is checking all Swift.String or Swift.Int values equivalent to that? There are a lot of Swift.Int values to check (2^64, on a 64-bit platform), and even more Swift.String values (every combination of characters up to that length), but simply being infeasibly slow to run on your Pentium "in a reasonable amount of time" doesn't mean it's an "impossible function to implement, and also equivalent to the halting problem". We could easily write a function to enumerate all Swift.Int values (though it might take 100 years to run). He throws out the parenthetical remark "it’s best to think of Int as modeling the infinite set of all integers" without explanation. When you're discussing whether something is theoretically impossible or not, thinking of a finite set as equivalent to an infinite set is brushing over a pretty major distinction.

joshuamorton 8y ago
With Int you may be right. But there are an infinite number of strings (and indeed every Turing machine may be represented as a String in swift), so it is indeed related to the halting problem.
- wtetzner 8y ago
  Swift strings don't have a maximum length? Are they nul-terminated?
- ken 8y ago
  Swift.String is composed of a finite set of symbols, with a finite maximum length. How can you create an infinite number of these? The article ignores the distinction in many places, but "String" in a Swift function means "the Swift.String type", not "an abstract string type like those used to represent Turing machine state".
  - timjver 8y ago
    You're not wrong, but the author's code does in no way rely on the fact that you could theoretically iterate over all the valid Int values in Swift, so it would have made no difference if the Int type was somehow truly infinite. And the author clearly acknowledges this: >it’s best to think of Int as modeling the infinite set of all integers

SeanLuke 8y ago

Apple's been in this game a long time. NewtonScript had a powerful function called "IsHalting". See Page 23-84 of http://www.newted.org/download/manuals/NewtonProgrammerRef20.pdf http://www.newted.org/download/manuals/NewtonProgrammerRef20...

keithalewis 8y ago

Balderdash, as others have more graciously pointed out. How wrong do you have to be before having your nonsense deleted from HN?

wool_gather 8y ago
Even if it is balderdash, isn't there value in analyzing(/refuting) it? I submitted the post (it's not mine) because I was interested in hearing people with more maths than I have expand/comment on it -- perhaps even people who had read the original papers. If there's something particular in the post that you find problematic, I personally am all ears.
- keithalewis 8y ago
  The author is correct that checking if two functions having infinite domains are equal is often impossible. He also has correct statements of some mathematical theorems. But people in this thread have provided counterexamples to his claim. That means he needs to fix the mistakes he made. If you are interested in what serious mathematicians have to say on this topic see https://homotopytypetheory.org/ https://homotopytypetheory.org/.
  - jozefg 8y ago
    It is possible in certain cases, that's the point of the article. One of the contributors to HoTT is the author of the paper introducing these algorithms :)

aaaaaaaaaab 8y ago

I don't get it. What prevents us from doing the exact same approach for the natural numbers? I.e. represent the naturals lazily via the successor function and use the same exhaustive search as the OP for BitSequence. Of course if the predicate doesn't stop evaluating successor(x) for any finite x then we're out of luck and the computation doesn't halt, but this caveat also holds for OP's BitSequence, as others have pointed out in this thread...

jozefg 8y ago
So this article shows how to check equality on `(nat -> bool) -> bool`. Your question, I think, is to figure out how to check `nat -> bool` for equality. The issue is that there are more operations we can do with `nat`, more properties we can check, than there are with `nat -> bool`. With `nat -> bool` we can basically check `i` indices and so the behavior of any predicate `(nat -> bool) -> bool` is basically determined by the first `i` indices. And that's finite. This algorithm is basically implicitly finding the indices considered by the supplied predicate and then brute-forcing all those entries. With `nat` there's no such finite cut off point. It's never the case that it suffices to test a predicate `nat -> bool` on finitely many entries to fully determine it. So we cannot do the same brute force search.
- aaaaaaaaaab 8y ago
  But a natural number can be viewed as a function from the natural numbers to {0, 1} via its binary expansion. There's a trivial isomorphism between the natural numbers and binary sequences with finitely many ones, so a predicate of type `nat -> bool` can be viewed as a predicate of type `(nat -> bool) -> bool`.
  - jozefg 8y ago
    It's not an isomorphism though, it misses the always true map. This means that many predicates on nat do not terminate on nat -> bool.