4 ms·

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 u

• 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.