3 ms·

Maybe I've been doing too much computer-assisted proofs recently, but I'm not understanding what all the fuss is. At some point you need a `Nat.mul` that's con

by kmill 6y ago

Maybe I've been doing too much computer-assisted proofs recently, but I'm not understanding what all the fuss is. At some point you need a `Nat.mul` that's concretely defined, and probably the only reasonable definition is recursively using repeated addition (and if your natural numbers are in unary, which is theoretically the simplest, then even `Nat.add` is going to be defined recursively by repeated incrementing! like taking a bead from a pile one at a time and putting it into another). Then you can define an interface with abstract operations like addition and subtraction, then any given number system can try to implement this interface. Naturals, integers, rationals, reals, polynomials, rational functions, complex numbers, and many others can implement at least the semiring interface. But what's important, I think, is that there's no universal multiplication operation -- it's just a word that fills in for whatever is the right multiplication operation at the moment. It's some ad-hoc polymorphism. Unless you're accepting the real line as being axiomatic (maybe from geometry, where you can define all the basic operations using ruler-and-compass constructions), all the definitions of multiplication for all the above number systems are going to be, eventually, based on the one for the naturals.

pdonis 6y ago
> At some point you need a `Nat.mul` that's concretely defined And since your computer can only perform finite operations on numbers with a finite bit size, which means operations on a set of numbers isomorphic to the integers, then yes, repeated addition works fine for your concrete implementation. But that's not at all the same as saying that multiplication is repeated addition, without any qualification whatsoever. The latter claim is the claim I'm arguing against. > Unless you're accepting the real line as being axiomatic Your computer can't manipulate real numbers. It can only implement finite operations on numbers with a finite bit size, which, as above, is a set of numbers isomorphic to the integers. So if you want to work with the real numbers themselves, abstractly, then you can't expect what the computer does to carry over.
- kmill 6y ago
  My computer can manipulate and prove things about real numbers just fine. I think it can do at least everything I can do normally, though much more laboriously. What I was mostly responding to in your previous comment is the idea of "emulating" multiplication for whole numbers by repeated addition. What I got from that is that you were thinking of the whole numbers as being inside the real numbers. My point was that to get the real numbers you usually have to start with the whole numbers and build up to the reals (say by Dedekind cuts or Cauchy sequences), and then you can embed the whole numbers inside and pretend that that was where they were the whole time. I do get that you were giving different pedagogical approaches, and this was just one of them, but I think this one is at least as bad of a misrepresentation as saying "multiplication is repeated addition" without specifying "for whole numbers." That is, unless you're like the Greek geometers and accept a continuum from the start. (There are other number systems that the integers sit inside, though, that don't themselves sit inside the real or complex numbers, which is a reason I would hesitate to think about whole numbers this way in general.)
  - pdonis 6y ago
    > My computer can manipulate and prove things about real numbers just fine. If you mean it can, with appropriate software, do symbolic manipulations of general formulas that are valid for real numbers, yes, of course. But that's not the same as doing specific concrete computations with them. > What I was mostly responding to in your previous comment is the idea of "emulating" multiplication for whole numbers by repeated addition. What I got from that is that you were thinking of the whole numbers as being inside the real numbers. My point was that to get the real numbers you usually have to start with the whole numbers and build up to the reals (say by Dedekind cuts or Cauchy sequences) Ah, I see. As far as I know the axiomatic reasoning involved can go either way. But in any case, that wasn't what I was trying to get at with the term "emulating"; I'm sorry if my use of that term caused confusion, and I agree with you that telling a child something like "the whole numbers are inside the real numbers" without qualification would also be a misrepresentation. My point was simply that teaching a child a specific computational procedure, repeated addition, in order to get an answer to particular multiplication problems does not require telling the child that multiplication is repeated addition, without qualification. The two things are distinct, and I am fine with the former; I only object to the latter.

by kmill 6y ago

pdonis 6y ago

> At some point you need a `Nat.mul` that's concretely defined And since your computer can only perform finite operations on numbers with a finite bit size, which means operations on a set of numbers isomorphic to the integers, then yes, repeated addition works fine for your concrete implementation. But that's not at all the same as saying that multiplication is repeated addition, without any qualification whatsoever. The latter claim is the claim I'm arguing against. > Unless you're accepting the real line as being axiomatic Your computer can't manipulate real numbers. It can only implement finite operations on numbers with a finite bit size, which, as above, is a set of numbers isomorphic to the integers. So if you want to work with the real numbers themselves, abstractly, then you can't expect what the computer does to carry over.

kmill 6y ago
My computer can manipulate and prove things about real numbers just fine. I think it can do at least everything I can do normally, though much more laboriously. What I was mostly responding to in your previous comment is the idea of "emulating" multiplication for whole numbers by repeated addition. What I got from that is that you were thinking of the whole numbers as being inside the real numbers. My point was that to get the real numbers you usually have to start with the whole numbers and build up to the reals (say by Dedekind cuts or Cauchy sequences), and then you can embed the whole numbers inside and pretend that that was where they were the whole time. I do get that you were giving different pedagogical approaches, and this was just one of them, but I think this one is at least as bad of a misrepresentation as saying "multiplication is repeated addition" without specifying "for whole numbers." That is, unless you're like the Greek geometers and accept a continuum from the start. (There are other number systems that the integers sit inside, though, that don't themselves sit inside the real or complex numbers, which is a reason I would hesitate to think about whole numbers this way in general.)
- pdonis 6y ago
  > My computer can manipulate and prove things about real numbers just fine. If you mean it can, with appropriate software, do symbolic manipulations of general formulas that are valid for real numbers, yes, of course. But that's not the same as doing specific concrete computations with them. > What I was mostly responding to in your previous comment is the idea of "emulating" multiplication for whole numbers by repeated addition. What I got from that is that you were thinking of the whole numbers as being inside the real numbers. My point was that to get the real numbers you usually have to start with the whole numbers and build up to the reals (say by Dedekind cuts or Cauchy sequences) Ah, I see. As far as I know the axiomatic reasoning involved can go either way. But in any case, that wasn't what I was trying to get at with the term "emulating"; I'm sorry if my use of that term caused confusion, and I agree with you that telling a child something like "the whole numbers are inside the real numbers" without qualification would also be a misrepresentation. My point was simply that teaching a child a specific computational procedure, repeated addition, in order to get an answer to particular multiplication problems does not require telling the child that multiplication is repeated addition, without qualification. The two things are distinct, and I am fine with the former; I only object to the latter.