Nick Scheel
what's the weakest type theory we can define arbitrary finite aleph numbers in? (arbitrary finite beth numbers are easy – just need natural numbers and functions)
Reed Mullanix
Be warned, the cardinals are not very well behaved in constructive math
Pretty much every direction you look, weird stuff starts to happen
Nick Scheel
yeah 🙂
I just find it weird that, with choice, all cardinals are aleph numbers, but beth numbers are the ones that are easy to construct in type theory
Reed Mullanix
I mean constructively even the finite cardinalities are weird
TL;DR subsingletons make life hard
Nick Scheel
ah hm
Reed Mullanix
Andrej has a great post on this
http://math.andrej.com/2009/09/08/constructive-stone-cardinality-of-sets/
Even defining the cardinality 1 is hard!
Nick Scheel
I suppose I've been mixing together theory and metatheory
Reed Mullanix
Even from a metatheory perspective things get weird a la Löwenheim–Skolem
Nick Scheel
yeah, that's not where I was being fuzzy
I mean, in a very simple type theory, with just ADTs and non-dependent functions, if you accept that those things construct the beth numbers (internally), I'm fairly sure you can get a metatheoretical result that every type has a bijection with a beth number (where the function witnessing the bijection and the beth number are both internal, but the proof that it is a bijection is external since it cannot be internalized without dependent types)
does that make sense?
the base case is that if you just have ADTs and no functions, you always get countable types … there's a simple algorithm to decide that
but I'm relying on the type theory being closed to extension, which is a huge red flag that it can't be internalized 🙂
Reed Mullanix
Yeah, you could go hunting for some weird model where the theorem doesnt hold
Reed Mullanix
Actually, I think our metatheorem may not be true... if our language is total, then the number of terms Nat -> Bool is countable, as there are countably many computable functions
Actually scratch the total part, should work even for partial functions
Nick Scheel
that's why I was saying the beth number and bijection are internal
you're talking about external cardinality there
Reed Mullanix
Serves me right for not reading carefully 🙂
Nick Scheel
but it does bring up a good question: what right have I to claim that nat, nat -> bool, (nat -> bool) -> bool, etc., model the beth numbers – when we could simply add an axiom that all functions are computable thus countable?
Robert Harper only externally. no computable function witnesses the countability of the computable functions.
Lorenzo Lipparini
This sounds really interesting; what would a function that witnesses such a proposition even look like? Would it be a function which takes a natural number and returns every computable function in existence, in some order?
I guess that the return value would need to be wrapped in a sigma type to account for the fact that every computable function might have a different type signature... or something like that?
Is the uncomputability of this function related to typing issues due to the fact that the function would need to return itself (or rather a sigma which "contains" itself), at some point?
Hopefully I haven't said anything too stupid, but I'd really like to know if there is an intuitive pseudo-proof of this theorem.
Nick Scheel
yes, something like the diagonal arguments (like Gödel’s incompleteness theorem, Russell’s paradox, Cantor’s argument, etc. – instances of Lawvere’s fixed-point theorem) would play a role
Nick Scheel
I think you could ignore the polytyping issues and just focus on functions from the naturals to the naturals, and I think the witness of computability would actually go the other way: (Nat -> Nat) -> Nat, and be interpreted as giving some encoding in a model of computability (turing machines, simply typed lambda calculus, etc.)
so the proofs that it actually witnesses computability could be separate
Nick Scheel
maybe you do need some amount of polymorphism for the diagonal proof to go through, idk
Nick Scheel
somewhat related (I haven’t fully grokked it yet): http://compilers.cs.ucla.edu/popl16/popl16-full.pdf
Lorenzo Lipparini
Thanks for the response @monoidmusician!
Working in terms of the actual definition of computability, restricting the domain to natural numbers, actually helps a lot 😅.
I'm not sure I understand though why you'd swap the input/output of the function to proceed with the proof; if you assume that you have a p : N -> (N -> N) which enumerates all computable functions, can't you just implement the diagonal argument as follows:
e : N -> N
e n = 1 + (p n) n
-- Forall n, e /= p n, since e n = 1 + (p n) n /= (p n) n
Wouldn't e be considered computable, since it is defined in terms of p which is computable by hypothesis?
Nick Scheel
okay, after thinking about it more, I think the proof that it is not computable is not quite a conventional diagonal argument:
Suppose that we had an internal, computable function C : (Nat -> Nat) -> Nat that witnesses the countability of computable functions. In particular, it has to be injective and return distinct outputs for distinct inputs.
Fix some arbitrary computable function f : Nat -> Nat. As a general result of computability theory (which can be formulated topologically), C f must inspect only finitely many values of f. (It would not be computable if it got to inspect infinitely many values!) Let’s say it inspects it at positions all less than m. We can create a new function g that differs from f only at position m. It is still computable, but obviously distinct from f. However, C g must equal C f since it only inspected its argument on inputs less than m! So C could not possibly witness the countability of computable functions.
Lorenzo Lipparini
Also, I rapidly looked up the definition of computable function (because I'm horribly ignorant 😶) on Wikipedia (https://en.wikipedia.org/wiki/Computable_function) and I don't quite get why it takes the input of computable functions to be a k-tuple of natural numbers: couldn't you just pick N, since any finite product N^k is still countable, and therefore its values could be re-encoded as plain natural numbers?
Lorenzo Lipparini
Oh, wait, what do you mean by "inspect" only finitely many values?
Nick Scheel
oh I see, that’s a nice diagonalization proof. my reasoning was that assuming A -> B is surjective is essentially giving a partial inverse function B -> A, which would be more useful internally
Nick Scheel
look at slides 9 and onwards in this talk: https://www.cs.bham.ac.uk/~mhe/.talks/popl2012/escardo-popl2012.pdf
or the blog post: http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
Lorenzo Lipparini
Oh, thanks! Now I'm trying to understand your proof: I'm still confused by the term "inspect", does it mean that C can't "evaluate" f at infinitely many values? And can only depend on a restriction of f to some finite domain?
Nick Scheel
yeah that’s right, evaluate might have been a better word there
Lorenzo Lipparini
Ah yes, that makes sense with the material you've shared 👌
Lorenzo Lipparini
By the way, now that I know that term I find your explanation really clear; also, you've touched on this idea of "continuity" of computable functions which sounds really interesting as well!
Nick Scheel
glad to hear 🙂 here's a little more on computability as topology, but it's about the real numbers: http://bollu.github.io/topology-is-really-about-computation-part-1.html
Nick Scheel
one minor detail:
any finite product N^k is still countable, and therefore its values could be re-encoded as plain natural numbers
this is correct, but only because the proof that N^k is countable, is constructive 😉 that is, there's an algorithm to compute the bijection between N^k and N.
Lorenzo Lipparini
By the way, I find it pretty funny how now I understand why a function that witnesses the countability of computable functions can't be computable, while I still don't know why computable functions should be countable in the first place 😅
I attempted to explain it to myself as follows:
Choose your favorite model of computation, which is surely the lambda calculus; the set of all possible programs is guaranteed to be smaller that the set of that of all syntactically valid lambda terms; given some suitable alphabet to encode the expressions (14 symbols should be enough, if you use De Bruijn indexing in base ten), the set of valid lambda terms is a subset of the set of strings of finite length in that alphabet, which is countable.
So the set of all possible programs is an infinite set which is no bigger than countable infinity, so it must be countable.
Is this correct?
Lorenzo Lipparini
Actually, this proof seems pretty constructive/computable: I think you can easily come up with a systematic way of enumerating all the possible strings (I guess you could just count all the natural numbers in base 14, which gives you all the combinations of the characters at your disposal); then, you can just get rid of the invalid lambda terms by doing a syntax check, which seems to be a simple enough algorithm...
I think there is one piece missing in the puzzle: you might have several lambda terms that end up encoding the same program, which makes the numbering of the programs inconsistent.
So I guess that the reason why the proof of countability of computable functions can't be computable has to do with the fact that you cannot write a program that tells if two syntactically distinct expressions correspond to the same program; if such a program existed, I think you could use it to convert the (constructive) enumeration of lambda terms from above into a (constructive) enumeration of the programs they represent (which correspond to all computable functions).
Lorenzo Lipparini
Actually, is this a valid proof of the fact that a program which takes as input two syntactically distinct programs and tells if they are equivalent cannot exist?
Nick Scheel
yeah, this sounds right!
Nick Scheel
in some sense, models of computation have to be syntactic ... but I can’t provide a good explanation of why, without resorting to existing models of computation
Nick Scheel
and syntactic means countable, essentially
Lorenzo Lipparini
Ah, maybe I see what you mean: we understand programs as "machines" that act on some sort of "memory", which ought to offer as much space as me might ever need, according to some rules.
I guess that the "memory", which corresponds to the state of the program at each instant, could be seen as a string of some sort, while the fixed rules which tell the machine how to manipulate the memory could be seen as "rewriting" rules for the string; I mean isn't ß-reduction (paired with a specification for the order of evaluation) just a particular rule for transforming a well-formed lambda term, which is just a string, into another string?
I suspect that Turing machines could be seen in a similar manner, where the "tape" corresponds to an arbitrary long string, and there are some rules to manipulate the string...
I don't know if this makes sense 😅
Nick Scheel
https://ncatlab.org/nlab/show/decidable+equality#examples
- Every finite set has decidable equality (though the same is not true for finitely-indexed or subfinite sets).
- The natural numbers have decidable equality.
Remark. In fact, these examples come close to to exhausting the sets than can be proven to have decidable equality in intuitionistic logic …
Lorenzo Lipparini
@monoidmusician I think I understand the article you've just shared on some level, although it's the first time I hear about "propositions as some types"; but I don't quite see how this relates to your previous comment
Nick Scheel
oh I just mean that having decidable equality is important for carrying out computation, kind of like what you were saying about memory
Nick Scheel
and already that constrains us to countable things (in constructive logic)
Lorenzo Lipparini
Mh, but doesn't decidable equality fail for types as simple as N -> N?
So you are suggesting that reasoning about computable functions (N -> N) in general is hard because proofs ought to be constructive if you want to find an actual computable witness, but the general N -> N type fails at decidable equality?
Lorenzo Lipparini
Just how, constructively, we cannot decidedly determine whether two lambda terms correspond to the same program?
Nick Scheel
hmm ... well, functions aren’t a model of computation, and we need to actually define a model of computation to work with computable functions (at which point we probably just want to work with that model of computation)
Nick Scheel
I guess I would say that intuitively, a model of computation should have the property that each “computer” is “finite” in some sense, although the collection of all computers is infinite ... this could be formalized with the concept of hereditarily finite sets I think, and the class of hereditarily finite sets is countable (it’s basically just rose trees)
but since each representation of a computer only contains a finite amount of information, it is clear that we can define decidable equality, and actually work the whole representation in a concrete way, whereas if I gave you an arbitrary function N -> N, you could only gain finite information out of the infinite information required to fully understand it
of course, the notion of infinity creeps back in when we let these finite programs run for an possibly infinite amount of time and try to look at semantic (not syntactic) properties (that’s the halting problem and Rice’s Theorem)
Lorenzo Lipparini
Mmmh, maybe the way I tried to explain the idea was kind of confusing; I might try with a somewhat more formal approach, which should clear things up for me, as well:
Abstractly, before we consider any specific model of computation, we would expect computable functions N -> N not to have decidable equality (constructively speaking).
Concretely, when we consider something like the lambda calculus, we find that we cannot write a lambda expression which checks if two other expressions (under some representation) have the same extensional behavior, and therefore correspond to the same function.
By “corresponding to the same function” I mean something like the following: the set of all computable functions, in the context of the lambda calculus, should correspond to the set of all lambda expression quotiented by an equivalence relation which pairs together expression which have the same extensional behavior, in the sense they produce the same result (or both loop) for any input (in N).
So what I was trying to say is that the problem of deciding the equality of two computable functions can always be reframed in your model of compution of choice, where it corresponds to checking that any two representations (lambda terms, turing machines...) of the functions are equivalent (since that is sufficient to conclude the equality of the equivalence classes).
Lorenzo Lipparini
I think that, although the equality between the representation of two computers might be trivial (such as checking two lambda terms character-by-character), the equality between the computers “themselves” (in the sense of the computable functions which they encode) is actually a problem which is, constructively, not decidable.
Lorenzo Lipparini
So even though we can easily decide the equality between the representation of the computers (because, as you’ve said, any sensible representation turns out to be finite), we cannot use this information to decide the equality between the “underlying computable functions”, since that would require to check the equivalence of the representations (in the sense of the message above) instead of the equality, and the former problem is not computable.
Nick Scheel
yeah, I think we're on the same page, just focusing on different aspects of it 🙂
Nick Scheel
@Lorenzo Lipparini would you mind if I archive this conversation in a gist later?
Lorenzo Lipparini
Not at all, it’d be great to have something to keep for future reference; be sure to drop a link! 🙂