It's always fun to make fun of cranks. Thanks for linking that. The author really needs to find the right statement of what they call the Nested Interval Theorem. I cracked up at the complete misuse of it in the "Interval Argument for the Rationals" section
2 line explanation of where e comes from here: to represent a number x in base b, you need roughly log_b(x) digits. If you weight that by the number of different digits in base b, you get b * log_b(x) = b * log(x)/log(b) = b/log(b) * log(x) (where now the log is any base you care to choose).
So assuming x > 1, this is minimized precisely when b/log(b) is minimized. The derivative of b/log(b) is (log(b) - log(e))/log(b)^2, so this is zero when b = e. (The second derivative is 1/(e log(e)) > 0, so this is a minimum).
Why should we weigh by the number of different digits? I.e. is there an argument why the cost of a single digit is linearly proportional to the number of values it can hold?
To me this seems like the weak point in the argument.
It's called radix economy. Different radices have different efficiencies as defined by the ratio of number of digits in a radix alphabet over the number of placeholders required.
Simple example, base 1 is obviously inefficient once counting past 1. Similarly base 1 million is inefficient (until you're counting in the bazillions)
If you can store one digit of a number base million in one physical element then it's exactly as efficient when it comes to storage of digits as binary. One element per one digit.
But it's about 20 times more efficient when it comes to storage of whole numbers because you can store number up to a million in a single physical elements while binary needs 20 elements.
I see what you're trying to say, like I understand the intuition, but like I was saying earlier this is an already understood topic https://en.wikipedia.org/wiki/Radix_economy and that point has been addressed. Sorry, not trying to be a jerk. Just wanted to point that out in case you're interested in this subject.
In the example you gave, I'm assuming by 'physical element' you mean 'placeholder' or digit. Storing more numbers in a single placeholder seems like you're just getting efficiency for free, but that's not how information works. You have to come up with a unique symbol for one million numbers (0 - 999,999). Which you have to pay for.
base 64 is a more realistic example. With 64 characters per digit, it may seem like it's more efficient, since you require less digits to express the same number as base 10 or 2, but you still have to encode 64 unique characters, and it ends up being less efficient. That doesn't mean less efficient is worse. It just means it is more specialized and used for different things. For example, base64 gets used when you want to encode information in a small amount of space. Otherwise, for the actual storage and computation of data, lower bases are preferred, and base 64 is still obviously stored as binary.
For what it's worth, the base integer with the best radix economy is 3, followed by 2.
Thanks. I should have googled this when you mentioned it.
I see that radix economy makes some sense if you assume that the "cost" of the "element" is not fixed but linearly proportional to the number of different states it needs to hold. It was apparently linear for the computers built with triodes but log2(n) to hold n states seems more realistic in electronics. Maybe little more for error resiliency.
I think the b factor is due to the analog representation: if the base has b values, you use on average b/2 voltage for representation. I would think the mean square value in might have been more appropriate though? (as voltage energy losses usually are V^2 / R or C V^2)
Repeating the calculation (for k bits and b values) using square values, you get E = b^2 * log_b(k) and dE/db = 2b/ln(b) - b^2 / (ln(b))^2 / b = b/ln(b) * (2 - 1/ln(b)). Setting dE/db to 0, we get 2 - 1/ln(b) = 0, ln(b) = 1/2,
That's true, if you use binary encoding to represent the b states. I were referring to base b representation, in which by definition we use b states to represent log2(b) bits: for example, 4 states to represent bits 00,01,10,11, which could correspond to voltage levels 0V,1V,2V,3V of a variable (analogous for other values of b).
In this case, the average voltage used would be the average of 0, 1, 2^2, 3^2, which is 0+1+...+(b-1)^2 / b ~ b^2 (proportional to b^2). I showed that in this case in theory the "optimal" base would be sqrt(e), but I can't think of simple representations of a variable with less than 2 states (you could have say 2 variables representing less than 4 states, for example the 3 pairs { 0V/1V, 1V/0V, 0V/0V }, but that seems a tad complicated![1]), so the least non-trivial integer base is just 2.
I think in reality this kind of argument doesn't apply to real computers in a straightforward way, because there are many other factors at play than what I would call a 'dynamic power consumption' associated with the square voltage. There are things like leakage currents (that consume some fixed power per transistor) and other effects that significantly complicates things, so that such simple claims of being "optimal" don't apply (so I agree with the other comment about avoiding absolute claims!). But they can inspire designs and we can see if there are any advantages in more realistic cases.
[1] Further analysis: In our example, the 3 voltage pairs have mean square voltage 1/3. If we instead use the pairs { 0V/0V, 0V/1V, 1V/0V, 1V/1V }, the mean squared voltage is 1/2. In the first case, we encode log2(3)/2 bits of information per voltage value, in the second, 1 bit per value. So the energy per bit is (energy per value)/(bits per value) = (1/3)/(log2(3)/2) = 0.420... for the first case, and 0.5 for the second case. Unfortunately, it's a loss!
As an exercise, I believe that if we delete the state 1V/1V/.../1V of a k-voltage tuple, for large enough k-tuple, we come out ahead (probably not by much), although again that's not necessarily useful in practice.
Correction: I've just realized I've drawn an incorrect conclusion, the energy per bit in the case I've shown is indeed lower than the standard 2 bit encoding, so it's actually a win! Again, for a myriad reasons, I'm not sure you'd want to use that encoding in real life, but it does consume a little under 20% less power in terms of V^2 losses.
Yes, that would be an example, though not all formalizations are written in software. I was originally talking just about standard formal logic, which is just first-order predicate calculus. Proof assistants use much more powerful systems in order to gain the same expressibility as the natural language which is used in informal proofs. (Which is kind of strange: In using natural language mathematicians don't seem to be using some advanced type theory.)
So I can't actually read these proof assistant languages, as they are using some advanced type theory based language. So just a few comments.
Lean: It looks suspicious that this seems to involve just one to two lines. Are they actually proving anything here? It doesn't look at all like Cantor's diagonal argument.
Coq: This looks better, at least from the description, and that it actually looks like a proof (Coq actually has a Qed keyword!). Though they, unlike Cantor, don't talk about real numbers here, just about sequences of natural numbers. Last time I read a discussion about it, it was mentioned that this exactly was a problem for the formal proof: Every natural number sequence (with a decimal point) corresponds to some real number, but real numbers don't necessarily have just one decimal expression, e.h. 0.999...=1. So real numbers and sequences can't straightforwardly be identified.
Isabelle: That seems to be a formalization of Cantor's powerset argument, not his diagonal argument.
Overall, this highlights a major problem with formalization of existing proofs. There is no way (at least no obvious way) to "prove", that a formal proof X actually is a formalization of some informal proof Y. X could be simply a different proof, or one which is similar but uses stronger or question begging assumptions, etc. One such example is informal proofs (like Cantor's) which didn't work in any axiomatized system, and where it isn't clear how much you can assume for a formal version without being question begging.
You have literally been given a fully formal proof of Cantor diagonalization.
The lean proof seens correct, I can't read lean well, but it appears to just be a formalization of the standard proof. It at least constructs the set needed for the proof.
>Proof assistants use much more powerful systems in order to gain the same expressibility as the natural language which is used in informal proofs. (Which is kind of strange: In using natural language mathematicians don't seem to be using some advanced type theory.)
Look up "Curry-Howard isomorphism".
>Overall, this highlights a major problem with formalization of existing proofs. There is no way (at least no obvious way) to "prove", that a formal proof X actually is a formalization of some informal proof Y.
And? This seems not relevant to the question at hand. Surely some textbook contains an insufficient proof, which couldn't be formalized without more steps. Why does that matter. The question still is whether "folk theorems" are real. Certainly Cantor's theorem is no such folk theorem, as you have just been given a fully formal proof.
>Though they, unlike Cantor, don't talk about real numbers here
Cantors theorem usually refers to the existence of uncountable sets, which can be proven by showing that there is no bijection between N and R, but also by showing that there is no bijection between a set and its powerset.
>Every natural number sequence (with a decimal point) corresponds to some real number, but real numbers don't necessarily have just one decimal expression, e.h. 0.999...=1. So real numbers and sequences can't straightforwardly be identified.
This is only relevant if you say that the real numbers are "infinte strings of digits", which is not a formal definition and therefore not used in mathematics.
> The question still is whether "folk theorems" are real. Certainly Cantor's theorem is no such folk theorem, as you have just been given a fully formal proof.
I didn't say that Cantor's theorem is a folk theorem, only that some proofs aren't even trivial to formalize. Many other things are trivial to formalize, but they still require filling in a lot of obvious steps. It often wouldn't be practically feasible to prove them with a standard first-order calculus, otherwise proof system languages wouldn't need higher order systems with advanced type theory.
> Cantors theorem usually refers to the existence of uncountable sets, which can be proven by showing that there is no bijection between N and R, but also by showing that there is no bijection between a set and its powerset.
Yes, but I was talking about his diagonal argument, not his powerset argument. That's a different proof from a different paper.
> This is only relevant if you say that the real numbers are "infinte strings of digits", which is not a formal definition and therefore not used in mathematics.
Well, I'm not saying that, but the Coq proof seems to assume it. That was the problem I was talking about.
Check out the replies to this comment [1] with the same attempted counterexample. Your set isn't union closed because {1}U{2} = {1, 2} isn't in it (same for {1}U{3} etc.).
I don't see the problem. For example, if something finishes in 10 minutes, it has 6 completions per hour. If a competitor finishes in 1 minute, it has 60 completions per hour. It both finishes in 1/10 of the time (time per completion) and is 10 times faster (completions in a given amount of time).
If you don't like the unit "completions per hour", consider that you don't have to drive for an hour or even go a mile to go 60 miles per hour.
You are of course completely correct. However, I do think numbers like these are more intuitive when people talk about duration (or latency, or time taken; depending on context) rather than speed outside of very narrow situations.
In a car, 60mph has some kind of well-known interpretation; there's an experience to that that people can at least vaguely identify. And it's also related to fairly intrinsic limits, such as legal speed limits, safety, etc.
But even in a car, people tend to care about trip-times, not speeds. And speeds are harder to work with; If you travel 30mph on your commute to work due to traffic; and 60mph on your way home - what was your average speed? Not 45.
Outside of a car and in a computation context, it's even more impractical to talk about "speed" - after all, we're usually dealing with lots of stages; and it's rather easier to simply add up latencies than it is to some reciprocal of reciprocals dance. Even if time is workload dependent, then the time-per-workload framing tends to be more helpful than the workload-per-time framing.
As a corollary, people currently talk about high refresh gaming, and will happily report how some workload went from 300fps to 400fps, without noting that this is the same frametime reduction as going from 48 to 50fps (setting aside perceptual limitations). Workload-per-time is pretty unintuitive.
That's actually a nice way to look at it, and helped me see why and in what cases I dislike this phraseology - I couldn't really articulate this before. So I think my issue is presenting something in time-units per action and talking about an optimisation of it as multiples of actions per time-unit faster.
Well, speed is distance/time. For the "speed" analogy to make sense when talking about performance, we have to translate "distance" to something more abstract, let's call it "work". That means we have speed = work/time. If you have 1 unit of work (say you think of "build the whole app" as one atomic operation) which used to take 20 seconds, and now it takes 2 seconds, you went from a speed of 1/20=0.05 to a speed of 1/2=0.5, which is a 10x increase.
Hence, "it's 10x faster" is a valid way to write "it does the same work in 1/10 the time".
Yeah I get it - it just feels a bit clumsy to use the flipped units when summarising the optimisation. Just a personal taste thing though.
I still think "X times less than" can GTFO though - as in 10,000 is "seven times less than" 70,000 - which is the kind of thing I'm seeing more recently. That wasn't mentioned in the article though, it was maybe a bit unfair to lump them together.
