Yes - to elaborate, a constructive logic is a logic without P or not P. This doesn't have much to do with whether a tool can tell you what obligations you haven't proven. The separation logic based provers I've used have all had excluded middle.
> To attack classic OTP, you’d brute force the keyspace. Since we’re XORing, whatever we encode the key as, it’s fundamentally being used in binary to XOR between plaintext and ciphertext. So your key is a binary blob the same length as the ciphertext. You keep trying and looking for what seems to be viable plaintext. You never get “all English strings of the given length”, because you’re not brute forcing the output, you’re brute forcing the key, which isn’t necessarily English.
If your key for OTP is uniform random bits without any additional encoding, and of the same length as the plaintext, then won't you enumerate all possible messages of the given length? E.g., "abcdef" and "123456" are indistinguishable when encrypted without knowing the key because there exist keys that map each string to the same ciphertext.
You don't have to. See my top level comment. In short, you have to strengthen your goal in order to have a strong enough inductive hypothesis to prove anything. E.g., instead of "picking a base case" that's sufficient, you work the base case into the goal, like n >= 2 -> P(n). Then you do the base case as part of a branch in the inductive step, without using your inductive hypothesis.
I started to write out what is happening here more formally, but I think it was not very elucidating. No matter what, the problem is that the proof of the inductive step is wrong. The problem is (as mentioned in the article), that for sets of size two, your inductive hypothesis is not sufficient to prove that h1 and h2 are the same color.
Saying it's the base case that's wrong is a little weird. In general your base case can be vacuously true without any issue. However, if it is (and your goal is non-vacuously true for something), then your inductive step will require a branch in it. One side of the branch in your proof will look like a proof of a base case.
I have maybe a skewed view on this from using Coq.
You're 100% correct. I would be more unequivocal -- saying that the problem is the base case isn't just a little weird, it is incorrect. Your analysis nails it.
Disagree. The induction step works perfectly fine for n>=2. In particular, if you can give me the base case "any two horses have the same color", then this proof works and all horses have the same color.
The problem is that the base case is n=2, but the student checked n=0 and n=1.
We don't even disagree about anything here....
We both say "P(n) => P(n+1)" does not work for n=1, but does work for n>1.
I would like to give the student partial credit for the "works for n>1" part and deduct points for the missing n=1 case.
The two obvious ways to "fix" that are either giving a proof for "P(1)=>P(2)" (which is currently missing) or establishing P(2) another way and then using induction. Both are fixes of the same thing and not at all "completely different".
The proof has errors, there is no fixing it, you can't prove that all horses have the same color given no data about horses. In this proof the base statement is 100% correct, in all sets of 1 horse all horses will have the same color. Hence the error has to be in the other part.
If a student was tasked with proving that all horses has the same color given no information about horses then the correct answer is "I can't prove this", the answer given in this article would give 0 points since the student obviously doesn't understand what they are doing. When you check that test, would you mark the base case as the source of the error of the proof, or would you mark the inductive step? The base case is correct, if you marked that part wrong the student would rightfully complain, their logic works there.
The base case is proven correctly, the inductive rules is proven OK except that the transitive set rule they invoke requires n>1
As such, the only data you would need yo prove that all sets of horses are the same color is that all pairs of horses are the same color.
I think zero points would be a very harsh grade given that an understanding of how to do an inductive proof was demonstrated and one minor error was made in an otherwise correct proof.
> I think zero points would be a very harsh grade given that an understanding of how to do an inductive proof was demonstrated and one minor error was made in an otherwise correct proof.
Who says the question was to demonstrate an inductive proof? Being able to prove that all horses are the same color if all pairs of horses are the same color isn't particularly useful, as typically that would be the definition of all horses having the same color. All that humbug didn't add any extra information to the problem at all, it didn't make things clearer it just made them harder to understand.
> You mean to tell me that horses are actually different colors? Really? /s
Right, the goal here is to find the logical error in an obviously wrong proof, not how to fix this proof as the proof is obviously wrong from the start. You trying to argue how to "fix" it is the one side-tracking the whole thing.
If you say "B wouldn't be wrong if you changed A, so A is wrong!" then that isn't how you find errors. If A is a correct statement and B is an incorrect statement then B is the wrong statement. If you can make B correct by changing A, then B is still an incorrect statement.
If this was a memorization question where you were supposed to find a particular A and B, then you could say that A is wrong even if the statement is correct, since you knew what A and B are supposed to be. But it isn't, we are just here to find the error in the statement to prove that the proof is wrong, we aren't here trying to find a correct version of this statement.
Their inductive step is perfectly valid. However, requires a group of horses with one removed to still have a horse remaining. Using N=1 is an incorrect base case. Had they proved the N=2 base case, their entire argument would work.
Of course, you can’t prove the N=2 base case, so that’s why the argument uses the wrong base case.
The inductive step introduces a premise that “requires a group of horses with one removed to still have a horse remaining.” It is not valid to introduce this premise. The inductive step is not valid.
I mean “valid” in the mathematical/logical sense. It does not follow from the stated assumptions that n > 1, in the inductive step is this proof.
This has nothing to do with the idea that it can be common practice to prove claims of the form for all n > N, P(n) by induction when N is a number like 4. Yes there is a perfectly valid way to use proof by induction to do such proofs. Has nothing to do with this blog post.
In a proof, you can absolutely assume something like "A is true", you do it as a part of a sub-proof. Then anything you prove in the sub-proof like "B is true" can be brought back into the main proof in the form: A implies B is true.
The blog post glosses over this assumption and thus ends up concluding "p(n) implies p(n+1)" instead of "p(n) implies (n>1 implies p(n+1))”
Nah, the inductive step is simply incorrect. For it to be correct it needs to say "for n > 1 the following is true", but it doesn't, the statement isn't true since they forgot to add that part. And if you added "for n > 1" to make the inductive statement correct then it is obvious where the reasoning goes wrong.
In other words, the base case is correct, in all sets of 1 horse all horses has the same color. The inductive step is not correct. Even if you changed the where you put the base case to N=2, the inductive steps reasoning is still wrong as long as it doesn't include the "for n > 1" part.
You wouldn't need to add "for n > 2" to the inductive step, any more than you need to include "for n > 1" for arguments where the base step is 1, or "for n > 20" for arguments where the base step is 20.
You need to do it because you prove the statements separately. Currently the inductive step statement is false, it says that applies for all sets. It doesn't.
Note that you can use false intermediate steps like that and still reach a correct conclusion. Then the conclusion is correct but the proof is still wrong since the steps you used were wrong.
The “vacuously true” part seems unnecessary (and weirdly subjective). The N=1 base case requires considering N=2 when you apply the inductive step and that fails.
The example I'm about to give is overkill, but I'm trying to make my point very carefully.
Suppose you want to prove something for integers >= 2. E.g., suppose you want to prove for all n >= 2, n is positive. The statement you're trying to prove for a given n is actually
P(n) := n >= 2 -> n is positive
Let's prove it by induction.
P(0) is 0 >= 2 -> 0 is positive. P(0) is vacuously true, because 0 < 2.
Suppose P(n). We want to show P(n + 1). Our goal is
n + 1 >= 2 -> n + 1 is positive. Let's break this into the cases n >= 2 and n < 2.
For n >= 2, we assume P(n) and have the LHS of the implies. This gives us n is positive. Say by definition or by a lemma that n positive -> n + 1 is positive, and we handle this branch.
For n < 2, the inductive hypothesis tells us nothing. Assume the LHS of our goal, i.e. n + 1 >= 2. We want to prove n + 1 is positive. Well 2 is positive and therefore n + 1 is positive by transitivity.
This is what I mean by the base case not being special. E.g., in Coq, induction over the natural numbers always starts at 0. When you think about doing induction starting at another number, you're transforming your goal to include something of the form n >= m -> P(n).
> E.g., in Coq, induction over the natural numbers always starts at 0. When you think about doing induction starting at another number, you're transforming your goal to include something of the form n >= m -> P(n).
The concept of a “minimal base case” really weirded me out but I couldn’t quite put my finger on why. Thanks for the painstaking explanation, this was perspective-broadening.
But does this do anything meaningful, or is it just pointless drudgery because Coq is a machine and can't 'understand'/assume even simple maths/logic if it isn't explicitly stated? This is not a slight on Coq by any means, just pointing out the difference between human proofs and machine proofs. (Humans can of course be tricked into thinking that subtly false statements are trivially true, which the much more meticulous machine proof would discover)
That is, what is being gained by looking at the vacuously true cases where n<2, when the only interesting base case is the one where the LHS of the implication is true?
I wrote out quite a bit for this, but I think that the main point is that by falling back to the formalism, we see the the LHS of the implication affects our inductive hypothesis. I think this is something that is not clear if you just do "base case starting at n" style proofs."
As far as drudgery, Coq will solve the trivial cases automatically, so you'd never have to prove the n = 0 case by hand. That said, there's a reason most math is done on paper and not in Coq - there's usually an order of magnitude more detail and drudgery in a formal proof, even with automation.
I don't understand why it's more or less weird to say the base case is wrong vs. the inductive case is wrong. If H(n) is 'all sets of horses of size n contain horses of the same colour', the linked argument seems like
H(1) is true
H(n) => H(n+1) (with a sleight of hand that it's only for n >= 2)
It seems to me like changing either the argument to assert H(2) is true, or the scope of the second statement to include n = 1, would be enough. It seems the fault of both statements equally to not fit with the other, so why is it weirder to say the base case is wrong?
You just said it. The base case is true. The inductive case is wrong. You called it true “with sleight of hand”, but that’s more of a poetic statement; mathematically it’s simply wrong.
One could write a completely different proof where the base case(s) cover n=1,2 and the inductive step is as in the post. In such a proof, the base case would be wrong and the inductive step would be correct. But that’s a different proof, not the one in the post.
I don't think this is correct. The main argument uses a very specific inductive invariant of applying transitivity of equality to a non-empty set. The argument doesn't apply in the base cases because it is vacuously true so the minimal base case is actually a set with 3 horses because that is the only case where transitivity of equality can be used non-trivially.
No I'm still with eperdew on this. You don't apply an inductive argument to base cases, so that statement doesn't really make sense. From a pedagogical point of view, I think it is very important to drive home the point that there is nothing special about your choice of base case, other than that it affects the argument in your inductive step, otherwise it's too easy to make the choice of base case seem "magical."
In fact I'd go further. Whenever you have an error in an inductive argument, it is always in the inductive step and never the base case, since you can always choose whatever base case you want (you might just find it makes your inductive step impossible to prove, so if you do prove something, you've made a logical error in your inductive step).
At worst, an "error" in choice of base case leads to a proof that cannot be completed, not an erroneous proof.
EDIT: "it is always in the inductive step and never the base case" except of course if you've somehow made an error in the initial proof of the base case, but that is distinct from choosing the "wrong" base case.
EDIT 2: I just understood what you meant by "apply," (doesn't fulfill the preconditions of the inductive step, vs I thought you meant relevant to proving the base case) sure that's a reasonable way of looking at it too, but again I'm very wary of saying that it's the wrong base case that leads to proving a falsehood as I lay out elsewhere.
> you might just find it makes your inductive step impossible to prove, so if you do prove something, you've made a logical error in your inductive step
The inductive step should be proven completely independently of proving a base case. Indeed, if the inductive step is proven correctly you see that it is limited in scope to n>1.
You can then use any base case you can prove where n>1. Let's say you pick a base case of one trillion. Easy enough to show thay every set of one trillion horses is the same color (since no such sets can exist). You can then easily use induction to show that every set larger than one trillion horses is also the same color!
So really, both base and induction were wrong in different ways but if the induction had been proven correctly, the inapplicable base case would have been clear.
The inductive step is being obscured (intentionally of course in the article to illustrate how the error can hide) behind the n.
The inductive step here is not true for all n, n + 1 pairs.
It is only true for all n, n + 1 pairs given that n is greater than or equal to 2.
The error is to drop that >= condition. Hence the inductive step is wrong as stated in the article (for all n), and its proof is erroneous.
Again while changing the base case can "fix" the argument in that it no longer proves an falsehood, without altering the statement of the inductive step it is still not a valid argument and only happens to prove a true statement "by chance."
If the base case was the error in the sense of proving a falsehood, then it would be possible to have an unsound inductive argument by choosing the wrong base case, but that's impossible. Rather the wrong base case (but correct inductive step) simply means you end up unable to complete your proof.
I think that is a complicated way to look at things. The error is that the argument assumes that for a, b being elements of H, the sets H - {a} and H - {b} meet. This is true for |H|>2 but the first induction case is for |H|=2, where the assumption is obviously false. But when you read the induction case you may think of n as being large and so not notice the error.
I think that what I wrote is implicitly agreeing with the GP that the induction argument is wrong not the base case. And I think that you attempted to refute it, but I couldn’t really understand how what you wrote would relate to either side. Do you mean that you agree that your description above was complicated, or that you agree that what I wrote is a fair description of the problem, or do you (now as opposed to before?) think that the problem was the induction step not the base case? Or are you talking about the statement that it is easy to miss the error by thinking of n as big rather than n=2? Maybe it doesn’t matter.
The argument in the article is the following: Given some function f, if f(A) = f(B) = f(A ⋂ B) then f is equal to some constant c and f(A ⋃ B) = c. This argument is valid only if A ⋂ B ≠ ∅. It doesn't apply to the base cases because anything is true for the empty set and any function on a one element set is trivially constant. So the minimal case where this can be applied in a non-trivial way is a set with 3 elements.
> The argument in the article is the following: Given some function f, if f(A) = f(B) = f(A ⋂ B) then f is equal to some constant c and f(A ⋃ B) = c.
This is not the argument.
> This argument is valid only if A ⋂ B ≠ ∅.
No, it isn't; it isn't even valid then. Consider a function over sets of real numbers:
f([0,2]) = 5
f([1,3]) = 5
f([1,2]) = 5
f([0,3]) = 6
plus other values...
I've constructed this function so that, obviously, f(A) = f(B) = f(A ⋂ B) = 5, and A ⋂ B = [1,2] ≠ ∅, but f is not a constant function and f(A ⋃ B) is not 5. f is still a function.
We can state the proposition "in a group of N or fewer horses, all of the horses are the same color" like so:
∀G∃c∀x( (|G| ≤ N ∧ x ∈ G) → f(x) = c )
where f is the function that tells you what color a horse is, and N is a free variable.
The proof claims that if this proposition is true for the value N = k, then it is also true for the value N = k+1. This claim is correct for all k > 1, but it is not correct for k=1. The problem is that we only show the truth of the proposition for N=1.
Abstracting a little further, we can view the proposition above as the potential output of a function of N:
p(0) = ∀G∃c∀x( (|G| ≤ 0 ∧ x ∈ G) → f(x) = c )
p(1) = ∀G∃c∀x( (|G| ≤ 1 ∧ x ∈ G) → f(x) = c )
p(2) = ∀G∃c∀x( (|G| ≤ 2 ∧ x ∈ G) → f(x) = c )
p(3) = ∀G∃c∀x( (|G| ≤ 3 ∧ x ∈ G) → f(x) = c )
p(4) = ∀G∃c∀x( (|G| ≤ 4 ∧ x ∈ G) → f(x) = c )
We can now say that the proof is claiming that whenever p(k) is true, p(k+1) is also true, that this claim is correct for all k > 1, and that p(1) has been established. But p(2) has not.
> This claim is correct for all k > 1, but it is not correct for k=1. The problem is that we only show the truth of the proposition for N=1.
This is exactly what the person you are responding to was saying. They were talking about the transitive part of the inductive step that the article handwaves to with this line:
>> In particular, h_1 is brown. But when we removed h_1, we got that all the remaining horses had the same color as h_2. So h_2 must also be brown.
the "remaining horses" is the A ⋂ B set that was mentioned and if that set is empty then know it is the same color as set A is meaningless. Thus given f(A ⋂ B) = f(A) and f(A ⋂ B) = f(B), you only know that f(A ⋃ B) is constant if A ⋂ B is non-empty.
Given that in this case A and B are formed by removing different elements from a set of size n+1, the proof only works if n+1>=3 so that A ⋂ B can have at least one member.
> Thus given f(A ⋂ B) = f(A) and f(A ⋂ B) = f(B), you only know that f(A ⋃ B) is constant if A ⋂ B is non-empty.
But this is wrong. Given f(A ⋂ B) = f(A) and f(A ⋂ B) = f(B), you do not know that f is constant, regardless of whether A ⋂ B is or isn't a non-empty set. poetically described a completely different and obviously false claim instead of the actual claim made by the false proof.
You must not understand the notation. f(A ⋂ B) = f(A) is saying that every result of f(A ⋂ B) is equal to every result of f(A), this is trivially true if A ⋂ B is the empty set and thus tells you nothing. However if A ⋂ B is not empty, it follows from knowing f(A) is constant.
Poetically is correctly identified the exact step when the n>1 assumption is introduced. The argument is condensed but accurate.
> if f(A) = f(B) = f(A ⋂ B) then f is equal to some constant c and f(A ⋃ B) = c. This argument is valid only if A ⋂ B ≠ ∅.
It is very clearly the assumption that "all the remaining horses" is not empty that introduces the n>1 condition. It is the non emptiness of that set that allows you to say that since f(A) is constant and f(B) is constant (and we already know that because |A|=n and |B|=n), then f(A ⋃ B) is also constant.
> However if A ⋂ B is not empty, it follows from knowing f(A) is constant.
That f(A) is constant is supposedly a conclusion, not a premise. It is not a valid conclusion to draw from the stated premises.
> f(A ⋂ B) = f(A) is saying that every result of f(A ⋂ B) is equal to every result of f(A)
As I just responded above, interpreting the claim this way doesn't get it to make any more sense. When f(A ⋂ B) = f(A), there is no basis from which to conclude that f is constant. You have no information about whether f is or isn't constant.
This is not the claim made in the false proof, nor does it have anything to do with the claim made in the false proof. It is a creation of poetically's own mind, and it makes no sense.
> You have no information about whether f is or isn't constant
You seem to have forgotten what we are talking about. A ⋃ B is an arbitrary set of horses of size n+1, A and B are subsets of A ⋃ B, each with a single different element removed and thus of size n. We already know that f() is constant over A and over B because they are of size n and we have assumed that all sets of horses of size n have the same color (which I already pointed out in my last comment.) We also know that f() is constant over A ⋂ B becasue it is a subset of sets we already know f() is constant over. The only thing that needs to be proven is that f() is constant over the set A ⋃ B. That proof is impossible if A ⋂ B is empty. We can only assert A ⋂ B is not empty if we assume that A ⋃ B must have a size of at least 3. From assuming n+1>=3 we are able to correctly conclude that n>1 implies the inductive step is valid.
I think you just misunderstood the notation. f is a function from (say) X -> Y. But the parent talks about it as if it were a function from the power set P(X). That is, for A a subset of X, when the commenter above says that f(A) is a constant, they meant that f(A) = {c} for some c in X. This is a bit of loose usage of the standard notation f(A) := {f(a) : a in A} is commonly understood.
Obviously an arbitrary function f : P(X) -> … needn’t satisfy the properties but no one was suggesting that.
Under your interpretation, poetically's claim still does not reflect the claim from the false proof, and it is still itself obviously wrong.
(I'll assume that when you say "f(A) = {c} for some c in X", you mean "f(A) = {c} for some c in Y", since the values of f come from Y.)
So consider these definitions:
f(x) = x²
A = [0,1]
B = [-1, 1]
We can easily see that f(A) = f(B) = f(A ⋂ B) = A. But it is not true that f takes a constant value over any of those domains. (It is true that f(A ⋃ B) = f(A), but this is required by the premise f(A) = f(B).)
In your example f(A) is not a singleton. I think that the image f(A) being a singleton {c} is what was meant by “f(A) is some constant c”.
It feels to me like you are taking advantage of imprecise language to demonstrate counter-examples to statements that no one was trying to prove.
Do you actually think that 'poetically (or I) are trying to use obviously false properties of functions (specifically the properties you keep providing counter-examples to) or are just being nit-picky about language?
Usually I find much mathematical writing can be hard to read because much of the context or scope of variables, assumptions, or definitions is so implicit. But when something seems obviously wrong it is an exercise to figure out what constraint I’ve missed that makes it true.
When one first learns analysis, the statement of so many of the theorems begins “given a continuous function f” and this continues in formal writing but when people communicate more casually they usually just say function and everyone knows/figures that a continuous function is meant instead of pointing out an obvious counter-example.
In the context of this thread, it is obvious to me that the thing being talked about is when the image of a function restricted to some subset of the domain is a singleton. The reasons it is obvious to me are:
- The f(A) := {f(a) | a in A} notation is standard and implied by the choice of letters
- It is meaningless to say that the value of a function is constant—you always get the same result, so for the word to mean something, I think it is reasonable to take it as implying the restriction is a constant function, or in other words that f(A) = {c}, a singleton.
- It seemed obvious to me from the context of the article
- It seems a reasonable interpretation that changes the statements from nonsense into a reasonable description
At first I thought you just weren’t familiar with the notation, but now it seems you knew it so was it just not obvious to you that that is what was meant? Or do you actually think people were trying to prove or rely on the statements you disproved? Or that people should write more precisely and deserve to be punished with pedantry when they assume some mathematical maturity instead? I’m genuinely curious what you think is going on here because I’m struggling to fit these comments to a model of how hn commenters think and act.
> In your example f(A) is not a singleton. I think that the image f(A) being a singleton {c} is what was meant by “f(A) is some constant c”.
What? What are you quoting? Here's the full relevant text I responded to:
> The argument in the article is the following: Given some function f, if f(A) = f(B) = f(A ⋂ B) then f is equal to some constant c and f(A ⋃ B) = c.
There is no claim (in the premises) that f is constant over A. There is such a claim in the conclusion, since that is a corollary of f being constant everywhere. But it's not in the premises.
So this is my model of what's happening:
- poetically has attempted to write down the claim of the false proof. He probably has a fair, if fuzzy, idea of what the proof is saying. But he doesn't know how to write it down; he has written down some things that sound kind of similar while, in the details, being mostly unrelated to the false proof. While I do believe that he broadly understands the OP, I do not believe that he understands the stuff he wrote down himself.
- You have a clear idea of what the proof is saying and you would like to read poetically as saying the same thing if at all possible. This is causing you to read things into poetically's claim that aren't there, but which would be necessary in order for him to be making sense. So it's unfair for me to use an example in which the image of A isn't a singleton, because, in the original post, the image of every set is a singleton. That the image of every set is a singleton is part of the inductive hypothesis. But in the claim attributed to the post, A is a set with no constraints on it, and f is a function with no constraints on it.
- At a wider level, poetically has described a post which contains a pretty clever false proof which is very nearly correct as instead making a claim which is so obviously incorrect that, if you believe poetically, it would make no sense to read the post.
So my initial thought process went like this:
1. Read poetically's comment. Notice that it is presented as a description of the argument in the post, but it makes no sense.
2. Leave a comment explaining how to describe the argument in the post.
This was a failure, in that poetically responded to the effect that he didn't see any difference between what he wrote and what I wrote.
In this subthread, you keep trying to provide interpretations that would cause poetically's original claim to make more sense, and I keep pointing out that the new interpretation doesn't help. In this case, the image of A being a singleton is most definitely not part of the original claim. But if I assume that it was, the adjusted claim still makes no sense. The new counterexample is:
f(x) = ⌊x⌋
A = [0.2, 0.6]
B = [0.4, 0.8]
This function is constant over A, B, and -- of necessity -- A ⋂ B. A ⋂ B is a nonempty set. But the function is not constant everywhere.
Moving back into the project of reading poetically's mind, I have to interpret his statement "This argument is valid only if A ⋂ B ≠ ∅" as an attempt to explain under what circumstances the argument he describes in the previous sentence is valid. This indicates a fairly serious error in understanding somewhere, because that argument is never valid. The observation that the intersection of A and B is or isn't empty has zero explanatory power.
(Note also that if you believe poetically was restricting himself to cases where the image of every set under consideration is a singleton, it doesn't make a lot of sense to describe for him to state his premise as "f(A) = f(B) = f(A ⋂ B)". When every image is a singleton, it's sufficient to say that "f(A) = f(B)". (And this is exactly how the false proof proceeds - it proves that f(A) = f(B) by observing that each is necessarily equal to f(A ⋂ B).) But this is fairly weak evidence; people bring up redundant information all the time.)
> At first I thought you just weren’t familiar with the notation, but now it seems you knew it so was it just not obvious to you that that is what was meant?
Yes, I'm familiar with that notation, and no, it wasn't obvious to me that that was what was meant. It still isn't, frankly. I cannot be confident about what was meant because there are no options that would make sense.
However, I will note that I don't think my response above indicates that I was familiar with the notation. You provided a definition and I used it while talking to you; I'm using "singleton" in this comment and that is a usage I was not previously familiar with.
This is incorrect. You attribute an argument to the article that it does not make.
> This argument is valid only if A ⋂ B ≠ ∅
This is vacuously true in that the argument is not valid and its validity therefore implies all propositions including that A ⋂ B ≠ ∅. Although I tend to suspect that that isn't what you meant to say. It is equally true that "This argument is valid only if A ⋂ B = ∅". It is not true that if a function f takes a constant value, you can conclude that A ⋂ B ≠ ∅ for arbitrary A and B.
Why is the base case 3? H(1) contains one colour of horse. H(2) when removing one horse contains one colour of horse.
The problem afaics is that there is a supposition that we are talking about sets of horses with the same colour. So if you "suppose for all sets of n horses, every horse in the set has the same color" then you can prove that horses in that set have the same colour. If P then P.
Yes, I also think it has nothing to do with base case and general case, there is just a flaw in the argument. When arguing that h2 also is brown one assumes wrongly that there are other elements in the reduced set left.
>> It's part of the inductive proof process. Assuming that it holds for n you need to show that it implies that it holds for n + 1 as well.
No. That's wrong. They assert it up front (that it is true for any n horses) and then go on to use it in the proof for n+1. The only time it's OK to assert your claim up front is if you're trying to prove it false by contradiction.
For an inductive proof, you must prove that if it holds for one case (n=1 here) it also holds for the next case. The base case is important and is proven (or obviously) true. A set of n is not the base case here, and they assert something about it without proof.
EDIT: Nope, my dumb. The wording is odd, but for induction we show that it is true for n=X (X is the base case and is 1 in this example). the inductive step is to show that being true for n implies being true for n+1 which is what they did here.
That isn't really a problem, just poorly worded (like a number of sentences in the article.) This is a pretty standard step of an inductive that should read more like: Given that n is some positive integer where every set of n horses has the same color...then you try to prove that holds true for n+1 as well.
The actual problem in that proof is setting up the proofs of the inductive rule. There is an implicit assumption/condition that n+1 >= 3 that is not acknowledged.
If you acknowledge that condition, then it becomes quite clear that you can only prove a base case for n = 1 and only prove an induction rule for n >= 2 .
I feel like I'm too ignorant of mathematics to be confused by this "proof".
When you set out to prove "for any set of n horses, every horse in that set has the same color" and you then "suppose for all sets of n horses, every horse in the set has the same color" as a first step, you're messing with a tautology, aren't you? I mean if you've supposed that it's true for all, it's definitely true for any, right?
What am I missing that makes the problem subtle and interesting, rather than just blatantly circular from the start?
> But why would anyone assume that n horses, for arbitrary n, are the same color?
because that's how inductive proofs work. You assume something is true for N and show that this implies that it's also true for N+1. This combined with base case (for example for N=1) proves that it's true for all N >= 1.
The assumption is just a tool used to check if you can prove the implication, the real "meat" of the proof is in the implication.
Are you aware of proofs by contradiction? A: "assume N is the largest natural number". If that's true then there shouldn't be any natural numbers larger than N, but we can create N+1 and show it's larger AND natural, so assumption A leads to contradiction, so there is no such thing as the largest natural number.
We used false assumption in our proof, but the proof was correct.
It's a similar idea with inductive proofs - you make an assumption and see where it leads you. You don't use the assumption for the proof, you use the implication A(N)=> A(N+1) for the proof, the assumption A is just a way to see if you can prove the implication.
> You might as well say "We can prove that coconuts can migrate. First, assume that coconuts can migrate. Thus, coconuts migrate". It's equally valid logic.
The logic isn't actually circular, your coconut analogy is wrong. Correct analogy would be:
"when we assume N coconuts can migrate we can formally show that it implies N+1 coconuts can migrate" + "we can show that 1 coconut can migrate". You only need these 2 facts to prove all coconuts can migrate.
Well, anyone who's seen a field of horses knows that "assume any set of n horses has the same color" is not valid.
So if what you say is true, then that implies the entire field of inductive reasoning is horse shit. But I don't think that's the case, so something's missing.
> Well, anyone who's seen a field of horses knows that "assume any set of n horses has the same color" is not valid.
That's not even true! If n is 0 or 1 then the statement is correct, for example.
If your response is "It's not true for all n, though." well, the inductive proof doesn't assume it for all n either. It only assumes it for one n at a time.
But also, you're getting too hung up on the exact wording of the statement.
For example, we could do the same proofs, but put "on farmer Joe's land" onto the statements.
If we do that, "anyone who's every seen a field with horses in it" can't tell us if the statement is true or not. Maybe all groups of 2 horses in a field on farmer Joe's land do have the same color, because he sorts his horses. And obviously all groups of 3 horses would have to have the same color, etc. etc.
So on farmer Joe's land, A(n=2) is true. And the induction is valid. And using it gives you the correct results! What's the problem with inductive reasoning here?
You seem upset that the induction itself might be valid even if n=2 isn't, but I don't know why. The induction is the same no matter whose farm you're on. That's why you need to prove the base case too.
> But you're not trying to prove X = 3 and starting out by assuming X = 3.
It's really not. There's an entire series of X, and we're saying if we can prove one we can prove the next. You never assume an X when proving that X. And you never assume a higher X when proving a lower X. There are no circles. It's a chain.
"Assume X is 3. Then 2*X=6" is just a different way of saying "If X is 3, then 2*X=6"
You can rewrite the entire thing without the word assume if you want.
You can do the whole thing as "if Y, then Z". "if A(n), then A(n+1)". If pairs of horses are the same color, then triples of horses must be the same color. If triples of horses are the same color, then quads of horses must be the same color. Those sound like reasonable statements to me.
Even if we're talking about all horses in the entire world, I could theoretically go kill every non-brown horse, and the original statements would all become true.
This is math. You can't object to abstract logic by mentioning real-world facts that could change at any moment.
> But you're not trying to prove X = 3 and starting out by assuming X = 3.
No, you're trying to prove
for all N>=1: A(N) is true
and start by proving that
IF A(N) is true THEN A(N+1) is true
This implication can be true even if A(N) is false, and your final proof will only use the implication, not the assumption used when proving that implication.
Assumptions in math proofs can have scopes. For example in many proofs you split the domain into subsets and prove that something is true assuming X>=0 and X<0 separately. Naively you would say that we cannot assume X>=0 and then assume X<0 in the same proof because that's a contradicion.
But these assumptions were used in different scopes so there's no contradiction.
So it's worth noting that the inductive hypothesis isn't false for all values of n - namely, it is true for n = 0,1.
But beyond that, in mathematical logic, for p -> q, you can still prove this to be true, even if p is false. In fact, if you can prove p is always false, p -> q is 'vacuously true' - it's true because you can never come up with an example of 'p and not q'.
So mathematically, there's no problem with assuming an induction hypothesis that's actually false here. The real problem occurs is that the result doesn't follow from the assumption because the induction step of the 'proof' sneakily assumes that n >= 3, i.e., the induction step simply doesn't work for the n = 2 case.
>> The inductive step assumes the hypothesis is true for n
You don't get to assume the thing you're trying to prove is true as a part of the proof that it's true. The only time we assume something like that is in a proof by contradiction, where the contradiction implies either an error in our logic, or an error in the assumptions.
As the article says there is a problem talking about equality among members of a set with size 1. So saying "all the horses in a set of size 1 are the same color" begs the question "same as what?" and that's where the real problem is, and the difficulty in pinning down that kind of thing is why I'm not a mathematician ;-)
There are several 'mathematical' ways you could phrase it (glossing over how to define the colour of a horse):
1) In a set of horses with size n, if horses A and B being both members of this set implies horse A has the same colour as horse B, then all horses in the set have the same colour.
2) In a set of horses with size n, and let f be a function on this set that produces each horse's colour. Then all horses in this set have the same colour if and only if the codomain of f on this set has size 1.
You could probably prove these are equivalent definitions.
one is proving the inductive rule that: p(n) implies p(n+1)
the other is proving that there exists some number i for which p(i) is true. This, combined with the proof of the inductive rule, allows you to prove that p(n) is true for all n >= i.
In simpler terms the two steps for this problem are:
1. There exists some number of horses where all horses are of the same color. This is obviously true when you have 1 horse.
2. The second step is that you have to prove that if you have some number of horses n, and they are all of the same color, then if you add another horse all the horses are of the same color.
He's saying there is some set of n+1 horses, n of which are of the same color. Then he makes the (false) claim that removing one horse at random leaves you with n horses, which therefore must all be of the same color. This is incorrect because the assumption is that there is a set of n horses, not "if you have n number of horses they are all the same color.
The base case of n=1 is just fine. It's adding a randomly colored horse to a set of horses that doesn't always result in an n+1 set of like-colored horses. He doesn't even explain the illogical step correctly, so the whole thing is a mess.
> He's saying there is some set of n+1 horses, n of which are of the same color.
> This is incorrect because the assumption is that there is a set of n horses, not "if you have n number of horses they are all the same color.
You have this exactly backwards. The assumption you say is not being made is exactly the one that is being made (and is a step that occurs similarly in every inductive proof.)
But you don't go from n-1 to n. You'd have to start at the infinite horses case where the conjecture must be true for, well, who knows what reason. Intuitively, "Consider the conjecture proven. If we reduce the difficulty, it's still proven" just seems obviously wrong.
1. Assuming that a property is true for N, prove that it is true for N+1.
2. Prove that the property is true for some concrete N where the proof for step 1 holds.
The trick is that you need to be sure to pick your concrete N correctly, as the article demonstrates. In particular, the problem with the "solution" in the article is that the proof given for step 1 doesn't hold for N=1, because N+1=2, and then just follow the rest of the argument from the article.
I still don’t quite understand. The inductive step shows n + 1 → n right? However with any positive base case b, n → n + 1 isn’t certain for any integers above b, only below it.
Say you’ve proved the case for n = 3 and that n + 1 → n. Then you’ve proven that 2 + 1 → 3, and by induction 1 + 1 → 2, However you’ve never proven it for n = 4 because n → n + 1 has never been established.
Or am I missing something here?
EDIT: I’ve seen in other posts that this the problem with OP is that it hides the transitivity of the operation. In fact the failure of the proof was that it proved transitivity with a false premise. If transitivity was true, then using n + 1 → n is just fine. The Wikipedia article for this statement is actually a lot clearer. https://en.wikipedia.org/wiki/All_horses_are_the_same_color
That’s not the issue at all, since the base case of n=1 is established trivially and so the quoted statement is merely the inductive hypothesis. But the inductive argument relies on n>2 to invoke transitivity on a non-empty intersection necessitating a separate justification for n=2.
To me, adding parentheses when using common operators signals that I should read it carefully, because normal precedence is probably broken. When that is not the case, I spend a bit more time parsing the expression for no gain as a reader.
Yeah, but char sucks. It's not a synonym for octet. Not guaranteed to be 8 bits. Its signedness is even ambiguous unless unsigned is specified.
The correct type is uint8_t/u8. Sadly, using that to alias other types is undefined. I've also seen hashing algorithms which used uint16_t/u16, with similar aliasing optimization bugs. Sometimes you want to reinterpret things as a struct, too.
This is the reason why Linux compiles with strict aliasing disabled.
Aliasing with unsigned char* is also allowed. (Oddly, signed char is not, even if char is signed.)
uint8_t is not guaranteed to be unsigned char but in practice almost always is. GCC did originally have separate 8 bit types when stdint.h was introduced but quickly changed to a typedef for char-based types precisely to allow using it for aliasing.
Yes, technically char may not be 8 bits but in practice that is very rare (and you can statically assert it).
Overall IMO the best solution is always use uint8_t and turn off optimisations on those rare weird platforms where it's not an alias for unsigned char for whatever reason.
`char` is not guaranteed to be 8 bits and in some more exotic environments (DSPs for instance) may not be.
IIRC POSIX guarantees that char is 8 bits though (but I still think that the sign is implementation-dependent).
But as I said in a parent comment, I don't understand why it's even relevant. If you want to alias any type then use `char *` and not anything else. I don't understand why one would prefer using stdint for that.
Because sometimes people need to reinterpret data as an array of 8/16/32/64 bit elements. Sometimes people also need to reinterpret things as a structure.
This is independent of how many bytes the underlying platform can address. If we have 8 bit processing code but the platform can only address 16 bits at a time, it should be up to the compiler to generate code that works. Compilers already do stuff like that in other circumstances.
Those people need to be copying, otherwise the reinterpretation might not be working. The char data might not be correctly aligned, for example. Recently went through a big nightmare where a C++ codebase that had accreted on x86 was thought to be ported to another platform where alignment actually matters and there were all manner of rare low-level malfunctions stemming from the idea that you can just wantonly cast a char* to structured data.
The strict aliasing rules look through typedefs (and const/volatile-qualifiers). It's possible to use char, signed char, and unsigned char, or any typedef thereof, or any typedef of any typedef, etc., to access any memory whatsoever.
Agreed. I alleviated this in my last zig project by just declaring a type alias, however. Strings could use some nice support from the stdlib once it gets fleshed out.
I'm not sure if this is done in practice, but in theory, if you compile a regex to a DFA, you can then minimize the DFA. I don't know if you can do anything similar with parser combinators, but if not, that could be a potential performance gap to watch out for.
I imagine this works for regex engines like RE2 that don't support backtracking, but would not be possible if supporting more advanced regex features like backtracking?
I definitely have more to learn about automata and FSMs :)
In practice, production grade general purpose regex engines are never implemented with formal DFAs in all cases. They take too long to build and use way too much memory, especially when Unicode is involved. For example:
And this is including oodles of tricks for shrink the DFA's size. (Note though that the above examples minimize the DFA, which adds significant time. Without minimization, the latter is about an order of magnitude faster.)
So even this simple regex is 3MB in size.
Finally, DFAs can grow exponentially in the size of the regex, which means you can't really use them with untrusted regexes.
In practice, regex engines like RE2 use a hybrid NFA/DFA, or "lazy DFA." The DFA is computed at search time and cached. If too much cache is used, then the regex engine falls back to an NFA simulation.
Beating the performance of a DFA without going into more exotic things like vectorized algorithms or more specialized regex engines (bit-parallel NFAs) is pretty tricky.
And also, do not repeat the same mistake that the OP seems to make: conflating what DFA and NFA mean. A lot of people like to call things like PCRE an "NFA" implementation, but it's not, because meaningfully more powerful than what an NFA can do. General purpose regex engines tend to be split between ones that are based on finite automata and ones that are based on backtracking.
Thanks for the super detailed response again, Andrew! I have a ton to learn from you about how production grade regex engines work honestly :) Do you have any tips for learning as much as you have aside from mulling over papers and existing implementations?
Also, by "do not repeat the same mistake that the OP seems to make: conflating what DFA and NFA mean." do you mean in the article? I wrote that mostly with the intent to say _"this ain't how things are normally done, DFA/NFA exist and are used"_ but admittedly don't have more than a surface-level understanding of them. If you have tips on how to clarify that wording so I don't confuse others, at the very least, I'd much appreciate it! :)
Yes, I mean in the article. Perhaps I was too brief, but the TL;DR is to use "finite automata based regex engines" and "backtracking based regex engines."
Basically, there's a long tradition of calling the latter "NFA engines" and the former "DFA engines." But doing so is inaccurate and confusing. Especially since "DFA engines" also include things called "NFA engines" that are different from the former "NFA engines" as used when describing backtracking engines.
If that doesn't make sense, then just remember this: DFAs and NFAs have equivalent expressive power. So if you're describing a regex engine that gives you thinks like backreferences, recursion and all sorts of other bells and whistles, then it can't be an NFA. It is almost certainly implemented with backtracking.
> Do you have any tips for learning as much as you have aside from mulling over papers and existing implementations?
I started with Russ Cox's article series and read the RE2 source code. Then I built my own.
I'd also check out anything related to Hyperscan. It's a deep rabbit hole to tumble down though.
Understood, this helped me a lot, thank you. I definitely had confusion around DFA/NFA being a _type of regex engine implementation_ and see now why that is incorrect.
I updated the article[0] so as to hopefully not confuse others, really appreciate you taking the time to respond to me again, and sorry for not understanding your earlier comment :)
There are some features exclusive to errors though (errdefer, stack traces, implicit error unions). Did you find yourself missing any of these by doing it this way? I'm partially asking because I was just making this decision the other day, and I went with errors for now.
For parsing specifically, I haven't felt the need for them (errdefer is not really relevant since I don't typically need to clean up resources half-way through parsing, and likewise, zig stack traces aren't necessarily as useful to an end user as contextual parsing metadata.
I do use errors for other stuff, and I wish I could, for example, attach actionable error messages to errors, to be dispatched to whatever logging mechanism is setup. Bubbling up an error from stdlib and printing it from main makes for poor end user experience, and pattern matching an entire application's worth of an error union in order to map an error to a descriptive message is not as ideal as writing the messages where they come from as you would w/ e.g. golang's `errors.New(message)`.
