4 ms·

It's possible, because you aren't a mathematician, that you aren't aware of who Terrence Tao is. He is one of the most celebrated mathematicians of our time, an

It's possible, because you aren't a mathematician, that you aren't aware of who Terrence Tao is. He is one of the most celebrated mathematicians of our time, and a prolific one at that. His goal is emphatically not to explain what dimensional analysis is, but to provide a basis for a mathematical formalism for it that does not fully exist yet.

gliese1337 14y ago
That doesn't seem to be any sort of refutation of the given complaint. Sure, Terrence Tao is a great mathematician, and he may trying to do something that type theorists haven't done yet, and we can reasonably give him the benefit of the doubt and assume that, even though he didn't mention it, he may well be familiar with type theory and left out reference to it on purpose. Nevertheless, for some audience, in which I am included, the connection to type theory seems blatantly obvious and it would've been a better article for us had it been presented in that light.
- banachtarski 14y ago
  It's not the same as type theory because the relationships between physical units are actually tied by real mathematical operations. A float and a string do not combine in any sensible way (aside from type-casting, which is entirely different). This suggests that type theory as you are familiar with isn't as connected as you might think.
  - gliese1337 14y ago
    Sure they do- by "multiplication" to form an instance of an algebraic product type (float,string).
  - evincarofautumn 14y ago
    There are plenty of systems making use of the algebraic operations of product (tuple) and sum (disjoint union) on types. These are regularly extended with notions of exponentiation, division, subtraction, complement, union, and intersection. There is little formal reason why an algebra of types shouldn’t include even more interesting operations.
dakimov 14y ago
OK, but what kind of experience does Tao (I was actually well aware of who he was) have with programming and type theory in particular? By the way, is not the type theory already a formalism? Cannot we construct formal proofs with it? Is it possible that he reinvents the wheel and describes a rather trivial thing in an overcomplicated roundabout way? Do you imply that a 'real' mathematical formalism is better than a formalism from the computer science? After all, equivalence is essential to mathematics, pretty everything can be represented and intuitively understood in a different equivalent way. This article is too long for me to crack it that fast, so maybe I am just not quite there yet in understanding.
- banachtarski 14y ago
  It isn't a mathematical formalism. I have studied books on lambda calculus and all that. A computer scientist's understanding of what "well-defined" means is very different from a mathematician's. It's not to say that it doesn't work, just that the standard is very very different. The standard of well-definedness for a physicist and a mathematician is also very different. Example: compare what constitutes a "good enough" definition of a real number to these three disciplines.
  - evincarofautumn 14y ago
    Could you elaborate on your perception of definitions of lambda calculus? Or, say, SK calculus. They’re very simple systems and entirely syntax-directed, so I’m curious to know where they “go wrong”—how would you prefer a definition be presented?

gliese1337 14y ago

That doesn't seem to be any sort of refutation of the given complaint. Sure, Terrence Tao is a great mathematician, and he may trying to do something that type theorists haven't done yet, and we can reasonably give him the benefit of the doubt and assume that, even though he didn't mention it, he may well be familiar with type theory and left out reference to it on purpose. Nevertheless, for some audience, in which I am included, the connection to type theory seems blatantly obvious and it would've been a better article for us had it been presented in that light.

banachtarski 14y ago
It's not the same as type theory because the relationships between physical units are actually tied by real mathematical operations. A float and a string do not combine in any sensible way (aside from type-casting, which is entirely different). This suggests that type theory as you are familiar with isn't as connected as you might think.
- gliese1337 14y ago
  Sure they do- by "multiplication" to form an instance of an algebraic product type (float,string).
- evincarofautumn 14y ago
  There are plenty of systems making use of the algebraic operations of product (tuple) and sum (disjoint union) on types. These are regularly extended with notions of exponentiation, division, subtraction, complement, union, and intersection. There is little formal reason why an algebra of types shouldn’t include even more interesting operations.

dakimov 14y ago

OK, but what kind of experience does Tao (I was actually well aware of who he was) have with programming and type theory in particular? By the way, is not the type theory already a formalism? Cannot we construct formal proofs with it? Is it possible that he reinvents the wheel and describes a rather trivial thing in an overcomplicated roundabout way? Do you imply that a 'real' mathematical formalism is better than a formalism from the computer science? After all, equivalence is essential to mathematics, pretty everything can be represented and intuitively understood in a different equivalent way. This article is too long for me to crack it that fast, so maybe I am just not quite there yet in understanding.

banachtarski 14y ago
It isn't a mathematical formalism. I have studied books on lambda calculus and all that. A computer scientist's understanding of what "well-defined" means is very different from a mathematician's. It's not to say that it doesn't work, just that the standard is very very different. The standard of well-definedness for a physicist and a mathematician is also very different. Example: compare what constitutes a "good enough" definition of a real number to these three disciplines.
- evincarofautumn 14y ago
  Could you elaborate on your perception of definitions of lambda calculus? Or, say, SK calculus. They’re very simple systems and entirely syntax-directed, so I’m curious to know where they “go wrong”—how would you prefer a definition be presented?