[HN Gopher] Grothendieck's use of equality
___________________________________________________________________
Grothendieck's use of equality
Author : golol
Score : 171 points
Date : 2024-05-20 11:41 UTC (1 days ago)
(HTM) web link (arxiv.org)
(TXT) w3m dump (arxiv.org)
| fmap wrote:
| For this particular question we have a great answer in the form
| of homotopy type theory. It handles all the complications that
| the author mentions. This is one of the reasons type theorists
| were excited about HoTT in the first place.
|
| The only problem is that the author is working in Lean and
| apparently* dismissive of non-classical type theory. So now we're
| back to lamenting that equality in type theory is broken...
|
| *) I'm going by second hand accounts here, please correct me if
| you think this statement is too strong.
| bumbledraven wrote:
| For reference, the paper mentions the term "homotopy" exactly
| once, in this sentence:
|
| > The set-theoretic definition is too strong (Cauchy reals and
| Dedekind reals are certainly not equal as sets) and the
| homotopy type theoretic definition is too weak (things can be
| equal in more than one way, in contrast to Grothendieck's usage
| of the term).
| cwzwarich wrote:
| > For this particular question we have a great answer in the
| form of homotopy type theory. It handles all the complications
| that the author mentions. This is one of the reasons type
| theorists were excited about HoTT in the first place.
|
| Arguably, Homotopy type theory still doesn't solve the problem,
| because while it strengthens the consequences of isomorphism it
| doesn't distinguish between "isomorphism" and "canonical
| isomorphism", whereas (some?) mathematicians informally seem to
| think that there's a meaningful difference.
|
| > The only problem is that the author is working in Lean and
| apparently* dismissive of non-classical type theory. So now
| we're back to lamenting that equality in type theory is
| broken...
|
| In my opinion, Lean made a number pragmatic choices
| (impredicative Prop, non-classical logic including the axiom of
| global choice, uniqueness of identity proofs, etc.) that enable
| the practical formalization of mathematics as actually done by
| the vast majority of mathematicians who don't research logic,
| type theory, or category theory.
|
| It's far from established that this is possible at all with
| homotopy type theory, yet alone whether it would actually be
| easier or more economical to do so. And even if this state of
| affairs is permanent, homotopy type theory itself would still
| be an interesting topic of study like any other field of
| mathematics.
| lupire wrote:
| "Canonical" refers largely to the names we give to things, so
| that we maximize the extent to which an isomorphism maps the
| object named A in X to the object named A in Y. And also to
| choosing an isomorphism that embeds in a different
| isomorphism (of superstructures) that isn't strictly the
| topic of the current question.
|
| I don't think anyone thinks canonical isomorphisms are
| mathematically controversial (except some people having fun
| with studying scenarios where more than one isomorphism is
| equally canonical, and other meta studies), they are a
| convenient communication shorthand for avoiding boring
| details.
|
| https://en.m.wikipedia.org/wiki/Isomorphism_theorems
| moomin wrote:
| I think the original author makes a good case that a) the
| shorthand approach isn't going to fly as we formalise b)
| different mathematicians mean different things by canonical
| and these details matter when trying to combining results
| and that therefore 3) it would be better to provide a
| proper definition of what you're talking about and give it
| an unambiguous name.
| euiq wrote:
| let me guess: you haven't read the article, have you?
| xigoi wrote:
| > Please don't comment on whether someone read an
| article. "Did you even read the article? It mentions
| that" can be shortened to "The article mentions that".
|
| https://news.ycombinator.com/newsguidelines.html
| fmap wrote:
| > it doesn't distinguish between "isomorphism" and "canonical
| isomorphism"
|
| You can distinguish these concepts in (higher )category
| theory, where isomorphisms are morphisms in groupoids and
| canonical isomorphisms are contractible spaces of morphisms.
| These sound like complicated concepts, but in HoTT you can
| discover the same phenomena as paths in types (i.e.,
| equality) and a simple definition of contractibility which
| looks and works almost exactly like unique existence.
|
| > In my opinion, Lean made a number pragmatic choices
| (impredicative Prop, non-classical logic including the axiom
| of global choice, uniqueness of identity proofs, etc.) that
| enable the practical formalization of mathematics as actually
| done by the vast majority of mathematicians who don't
| research logic, type theory, or category theory.
|
| The authors of Lean are brilliant and I'm extremely happy
| that more mathematicians are looking into formalisations and
| recognizing the additional challenges that this brings. At
| the same time, it's a little bit depressing that we had
| finally gotten a good answer to many (not all!) of these
| additional challenges only to then retreat back to familiar
| ground.
|
| Anyway, there were several responses to my original comment
| and instead of answering each individually, I'm just going to
| point to the article itself. The big example from section 5
| is that of localisations of R-algebras. Here is how this
| whole discussion changes in HoTT:
|
| 1) We have a path R[1/f][1/g] = R[1/fg], therefore the
| original theorem is applicable in the case that the paper
| mentions.
|
| 2) The statements in terms of "an arbitrary localisation" and
| "for all particular localisations" are equivalent.
|
| 3) ...and this is essentially because in HoTT there is a way
| to define _the_ localisation of an R-algebra at a
| multiplicative subset. This is a higher-inductive type and
| the problematic aspects of the definition in classical
| mathematics stem from the fact that this is not
| (automatically) a Set. A higher-inductive definition is a
| definition by a universal property, yet you can work with
| this in the same way as you would with a concrete
| construction and the theorems that the article mentions are
| provable.
|
| ---
|
| There is much more that can be said here and it's not all
| positive. The only point I want to make is that everybody who
| ever formalised anything substantial is well aware of the
| problem the article talks about: you need to pick the correct
| definitions to formalise, you can't just translate a random
| math textbook and expect it to work. Usually, you need to
| pick the correct generalisation of a statement which actually
| applies in all the cases where you need to use it.
|
| Type theory is actually especially difficult here, because
| equality in type theory lacks many of the nice properties
| that you would expect it to have, on top of issues around
| isomorphisms and equality that are left vague in many
| textbooks/papers/etc. HoTT really does solve _this_ issue. It
| presents a host of new questions and it 's almost certain
| that we haven't found the best presentation of these ideas
| yet, but even the presentation we have solves the problems
| that the author talks about _in this article_.
| aureianimus wrote:
| I'd love to hear a little bit more on what you think the
| downsides are? (Or a recommendation for a resource to read
| up on this?)
| voxl wrote:
| Classical versus non-classical has nothing to do with it. HoTT
| does not work to capture what a mathematician means by "unique
| isomorphism" because witnesses of equality in HoTT are very
| much not unique.
| jhanschoo wrote:
| Can you elaborate more on how you think HoTT can solve the
| issue Buzzard mentions that when formalizing informal
| mathematics, the author frequently has a model (or, a
| particular construction) in mind and requires properties
| present in the model, and then claims that this is true for all
| "canonically equivalent" objects without actually spending time
| explicating the abstract nonsense required to properly specify
| the properties that canonically equivalent objects preserve,
| for their developement? (see: a product vs. the product)
|
| Edit: and furthermore, the situation where the obvious choice
| of universal property (read: level of isomorphism) was a poor
| one, in their attempt to formalize localizations.
| YetAnotherNick wrote:
| I think 99.9% of the people talking about HoTT haven't used
| HoTT in practice. They just see isomorphism is equivalent to
| equivalence(or something similar), comes up with a mental model
| and think this is the main contribution of HoTT, whereas
| isomorphism is a well studied thing even before formal set
| theory was a thing. HoTT gets weird and anyone who has tried
| any tool to prove anything in HoTT knows this, and this is the
| reason why it didn't got adopted even though many leading tools
| like lean worked hard to implement it.
| staunton wrote:
| Have you used it? If yes, could you elaborate? Or if you
| haven't, can you point to any recent source on what it's like
| to be using HoTT in 2024?
| YetAnotherNick wrote:
| [1] is the only video which I would say I found any bit
| accessible. But to be honest even after spending days, I
| couldn't grok it. And in my observation, different
| implementations of HoTT are quite different from each
| other.
|
| [1]: https://www.youtube.com/watch?v=x4cz1OgpU3M
| nicklecompte wrote:
| I think HOTT helps remove a lot of the footguns and
| computational hairiness around using type-theoretic
| mathematics. But the issues Buzzard is talking about are really
| more profound than that. This relates to a much deeper (but
| familiar and nontechnical) philosophical problem: you assign a
| symbol to a thing, and read two sentences that refer to the
| same symbol ("up to isomorphism"), but not necessarily the same
| thing. If the sentences contradict each other, is it because
| they disagree on the meaning of the symbol, or do they disagree
| on the essence of the thing? There is a strong argument that
| most debates about free will and consciousness are really about
| what poorly-understood thing(s) we are assigning to the symbol.
| Worse, this makes such debates ripe for bad faith, where flaws
| in an argument are defended by implicitly changing the meaning
| of the symbol.
|
| In the context of """simple""" mathematics, preverbal toddlers
| and chimpanzees clearly have an innate understanding of
| quantity and order. It's only after children fully develop this
| innate understanding that there's any point in teaching them
| "one," "two," "three," and thereby giving them the _tools_ for
| handling larger numbers. I don 't think it makes sense to say
| that toddlers understand the Peano axioms. Rather, Peano
| formulated the axioms based on his own (highly sophisticated)
| innate understanding of number. But given he spent decades of
| pondering the topic, it seems like Peano's abstract conception
| of "number" became different from (say) Kronecker's, or other
| constructivists/etc. Simply slapping the word "integer" on two
| different concepts and pointing out that they coincide for
| quantities we can comprehend doesn't actually do anything by
| itself to address the discrepancy in concept revealed by Peano
| allowing unbounded integers and Kronecker's skepticism. (The
| best argument against constructivism is essentially
| sociological and pragmatic, not "mathematically rational.")
|
| Zooming out a bit, I suspect we (scientifically-informed
| laypeople + many scientists) badly misunderstand the link
| between language and human cognition. It seems more likely to
| me that we have extremely advanced chimpanzee brains that make
| all sorts of sophisticated chimpanzee deductions, including the
| extremely difficult question of "what is a number?", but to be
| shared (and critically investigated) these deductions have to
| be squished into language, as a woefully insufficient
| compromise. And I think a lot of philosophical - and
| metamathematical - confusion can be understood as a discrepancy
| between our chimpanzee brains having a largely rigorous
| understanding of something, but running into limits with our
| Broca's and Wernicke's areas, limits which may or may not be
| fixed by "technological development" in human language. (Don't
| even get me started on GPT...)
| psychoslave wrote:
| The level of insights and clearness in your message, and most
| comments in this thread actually, is surprising great
| compared to what I often read on HN.
|
| Thank you very much for this
| Ericson2314 wrote:
| The fact that Buzzard is writing this paper at all to me shows
| a much higher degree of respect than before --- see how humble
| the overview is. I think this is great progress!
| zozbot234 wrote:
| > It handles all the complications that the author mentions.
| This is one of the reasons type theorists were excited about
| HoTT in the first place.
|
| It's not that simple, Buzzard actually seems to be quite
| familiar with HoTT. The HoTT schtick of defining equality
| between types as isomorphism does 'handle' these issues for you
| in the sense that they are treated rigorously, but there's no
| free lunch in that. You still need to do all the usual work
| establishing compatibility of values, functions etc. with the
| relevant isomorphisms, so other than the presentation being
| somewhat more straightforward there is not much of a gain in
| usability.
| juped wrote:
| Equality can be philosophically troubling, but as a practical
| matter, what you care about is the indiscernibility of
| identicals, and if every property you use follows from a
| universal property, then equal up to isomorphism is just equal.
| So every Rubik's cube is equal considered as a group of face
| rotations, and there's only one Rubik's cube, but if you care
| about chemical properties of sticker glue, they're no longer
| equal.
| moomin wrote:
| Something the author points out: sometimes theorems directly
| rely on specific constructions of mathematical objects, which
| are then used to establish things that do not mention the
| construction.
| passion__desire wrote:
| The glue point reminds me of Benacerraf problem.
|
| https://en.m.wikipedia.org/wiki/Benacerraf%27s_identificatio...
| generationP wrote:
| This is probably better known here under the name of implicit
| type conversions. Strictly speaking, the rational number 1 is not
| the same as the integer 1; we just have a conversion map that
| preserves all the relevant properties. It's all fun and games
| until there are 1000 types and 10000 conversion maps involved and
| the relevant diagrams no longer commute (i.e., it depends what
| order you go).
| actionfromafar wrote:
| I assume you mean any random enterprise codebase? Because that
| is any random enterprise codebase.
| 082349872349872 wrote:
| In other areas, one might compare code jurisdictions, where
| presumably all the legislative clauses share a common
| vocabulary (and probably even conceptual framework), with
| common law jurisdictions, where all the legislative clauses
| occur in different centuries and thus one adds "picking a
| parallel transport" between the legal languages of the times
| (and jurisdictions) to the difficulties of adjudication.
| om8 wrote:
| Not if you use a language that bans implicit type conversions
| (like go)
| actionfromafar wrote:
| I was thinking in _much_ more abstract terms. You have
| information from a webflow, at some point converted to an
| XML message, converted to database entry, again to a JSON
| document, combined with an Azure workitem, then sent to
| Salesforce.
|
| At any one point the data can interact with other systems,
| travel through codebases each seeing the data through their
| types, legacy APIs, the same-(ish) new-(ish) RPC API and in
| each service the data is represented in its own internal
| quirky way.
|
| Sure, throw Go in that mix, hell at this point the more
| merrier! :)
| nico wrote:
| Or when your formulas on Google sheets start failing because
| you do 1-1 and the result is not 0, and then you spend 30
| minutes creating new sheets, searching the web and double
| checking everything, until you realize that the value on the
| cell wasn't 1, but 1.
|
| This happened to me yesterday
| boppo1 wrote:
| Can you elaborate?
| gatane wrote:
| 1 vs 1.0 ???
| nico wrote:
| Now I noticed that the period at the end of the paragraph
| is a bit unfortunate
|
| The value was 1. which I guess is shorthand for 1.0 and
| it's technically not the same value as 1
|
| On top of that, sometimes values like 0.961727 will be
| shown as 1, so sometimes you think that the value in the
| cell you are referring to is a 1 but instead it's something
| close to it
|
| In particular I was making a list of array positions from 1
| to 32 and calculating x,y coordinates from the position
| using the formulas (x = (i-1) % width, y = (i-1)/width)
|
| Some of the coordinates were wrong, and it was because the
| i values were not integers, which I couldn't tell just by
| looking at the sheet, and only realized it when double
| clicked on the cells
| jkaptur wrote:
| It's frustrating that there isn't an easy way to see the
| "canonical" value and format of a cell (in Sheets or
| Excel).
|
| Just looking at a cell, it's not trivial to see if it's
| the number 1 or the string 1 (you can enter text by using
| a leading apostrophe, but that's not the _only_ way to
| get text in a cell!). Numbers and strings have different
| alignments by default, but that can be overridden. The
| numeric value of the string 1 is 0 if you 're using the
| SUM formula, but it's 1 if you use +. In other words,
| =A1+A2 does not necessarily equal =SUM(A1:A2)
|
| Then you can format numbers however you like. For
| example, dates are stored in spreadsheets as days since
| an epoch (not the Unix epoch). So you can have the number
| 2 in a spreadsheet cell, then format it as a date, but
| just the day of the month, and it can appear as 1.
|
| There's rounding, which bit you. 0.95 can appear as 1 if
| you display fewer decimal places.
|
| Finally, there's the fact that the calculation is done
| like IEEE 754. Programmers are used to floating point
| numbers and the fact that properties like associativity
| don't apply, but that's not obvious to everyone.
| nico wrote:
| You definitely know a lot about mangling data with
| spreadsheets!
|
| > Programmers are used to floating point numbers and the
| fact that properties like associativity don't apply, but
| that's not obvious to everyone
|
| One of my first programming assignments in college was to
| simulate a pool table. I had to go ask the TA what the
| hell was wrong with my code, the balls would never bounce
| because their distances to anything were never 0... fun
| times
| boppo1 wrote:
| Thank you!
| paulddraper wrote:
| 1 is an integer, a rational number, a positive integer, an odd
| integer, a power of 2, etc.
| sharkbot wrote:
| It's also a complex number, a Unicode character, an ASCII
| character, an Extended ASCII character, a glyph, the
| multiplicative identity element, a raster image, ...
|
| The GP point is correct; we implicitly convert between all
| these representations naturally and quickly, but there are
| interesting branches of mathematics that consider those
| conversions explicitly and find nuances (eg, category
| theory).
| kbolino wrote:
| But the integers are a subset of the rationals, which are a
| subset of the reals, which are a subset of the complex
| numbers. Looking only at the objects _and not their
| operations_ 1 (integer) = 1 (rational) = 1 (real) = 1
| (complex). Moreover, when we do account for the operations,
| we also see that 1 + 1 = 2 and 1 * 1 = 1 in every one of
| those systems. This isn 't just a coincidence, of course;
| it's by design.
|
| However, the way you arrive at 1 + 1 = 2 is _not_ the same
| (though I suppose you could short-circuit the algorithm).
| Rational addition requires finding a common denominator,
| while integer addition doesn 't. They achieve the same
| result when the inputs are integers, and again this is by
| design, but the process isn't the same. Ditto real addition
| vs. rational and complex addition vs. real.
|
| In higher-level mathematics, the operations on the objects
| become definitional. We don't look at just a set of things,
| we look at a set of things and the set of operations upon
| those things. Thus "1 with integer addition and integer
| multiplication" becomes the object under consideration
| (even if it's just contextually understood) instead of
| simply 1. This is why they don't satisfy higher-level
| notions of equivalence, even if they intentionally do
| satisfy simple equality as taught in grade school.
|
| Of course, the entire point of the submitted paper is to
| examine this in detail.
| JadeNB wrote:
| > But the integers are a subset of the rationals, which
| are a subset of the reals, which are a subset of the
| complex numbers.
|
| It depends on definitions, and, in some sense, the point
| of the common approach to mathematics is not just that
| one does not, but that one cannot, ask such questions.
| One approach is to look at natural numbers set
| theoretically, starting with 0 = [?]; to define integers
| as equivalence classes of pairs of natural numbers; to
| define rational numbers as equivalence classes of certain
| pairs of integers; and to define real numbers as
| equivalence classes of Cauchy sequences of rational
| numbers. In each of these cases there is an obvious
| injection which we are used to regarding as inclusion,
| but most of mathematics is set up to make it meaningless
| even to _ask_ whether the natural number 1 is the same as
| the integer 1 is the same as ....
|
| That is to say, if you're working on an application where
| encoding details are important, then you can and will ask
| such questions; but if I am writing a paper about natural
| numbers, I do not have to worry about the fact that, for
| some choice of encoding, the number 2 = {[?], {[?]}} is
| the same as the ordered pair (0, 0) = {0, {0, 0}} = {[?],
| {[?]}}, and in fact it is meaningless to test whether 2
| "equals" (0, 0). The philosophy of studiously avoiding
| such meaningless questions leads some to avoid even
| testing for equality, as opposed to isomorphism; failing
| to do so used to be referred to in category-theoretic
| circles as "evil", although, as the nLab points out if
| you try to go to https://ncatlab.org/nlab/show/evil , it
| seems common nowadays to avoid such language.
| generationP wrote:
| This is not the point of the article. Even at the level
| of the objects themselves, 1 : integer is not 1 :
| rational. The latter is an ordered pair (1, 1) of two
| coprime positive integers, or an equivalence class of
| ordered pairs up to cancelling. Some ugly hackery is
| required to really make the integers _equal_ to their
| respective rationals, and its consequences aren 't great
| either (just imagine that _some_ rationals are pairs
| while others are not -- that 's what you get if you
| forcibly replace the rational k/1 by the integer k), and
| no one wants to do that.
| passion__desire wrote:
| All the examples of shadows mentioned by Douglas in the
| video [0]:
|
| Traditional Shadow from Sunlight: A tree casting a shadow
| in bright sunlight during the summer, characterized by the
| typical darkening on the ground.
|
| Snow Shadow: Occurs in winter when a tree intercepts
| snowflakes, resulting in an absence of snow under the tree
| despite being surrounded by snow. This is likened to a
| shadow because it mimics the visual absence typical of
| shadows, even though caused by a different kind of
| blockage.
|
| Rain Shadow: Explained with the example of the Cascade
| Mountains, where the mountains block rain clouds leading to
| dry conditions on the leeward side, effectively creating a
| "shadow" where rain is absent due to the geographical
| barrier.
|
| Car Shadow by a Truck: Described during highway driving,
| where a large truck casts a "shadow" by preventing cars
| behind it from passing. This "shadow" is the area in front
| of the truck where cars tend to stay clear due to the
| difficulty in passing the truck.
|
| Shadow Cast by England Due to the Gulf Stream: This is a
| metaphorical shadow, where England blocks the warm Gulf
| Stream from reaching certain areas, resulting in colder
| temperatures on one side, while allowing it to pass above
| to northern Norway, warming it. This is referred to as the
| "shadow of England" on the coast of Norway, influenced by
| the flow of water rather than light.
|
| These examples use the concept of "shadow" in various
| physical and metaphorical contexts, showing disruptions in
| different types of flows (light, snow, rain, traffic, and
| ocean currents) caused by obstructions.
|
| [0] : https://youtu.be/LnTVzB5S8m4?t=973
| LudwigNagasena wrote:
| Saying 1 is both an integer and a rational number is wildly
| different from saying it is both an integer and an ASCII
| character. Z is a subset of Q. ASCII characters don't
| overlap with either.
|
| When you construct numbers using sets under ZFC axioms or
| inside lambda calculus what you get is representation. But
| 1 is just 1.
| pitched wrote:
| Your keyboard has a button with '1' printed on it. When
| you push that, you don't always get an integer or a
| rational number. You can convert what you get to either.
| So there must be overlap with ASCII somehow?
| LudwigNagasena wrote:
| There is some overlap in some sense somehow, but not in
| any literal sense unlike in the sense in which all
| elements of Z are elements of Q.
| LegionMammal978 wrote:
| By any common set-theoretic construction of Q (e.g.,
| equivalence classes of integer pairs under cross-
| multiplication), 1 as an element of Z is not literally an
| element of Q: 1 [?] Q merely _corresponds_ to 1 [?] Z,
| and this correspondence is carefully designed to preserve
| the ring operations of Z within a certain subset of Q. In
| this case, the distinction is so negligible that eliding
| it is harmless, but the whole point of the article is
| that such elisions can become harmful in more complex
| constructions.
|
| 1 [?] Z and ASCII '1' can similarly be seen as
| corresponding in terms of having the same glyph when
| displayed. But of course, there are far fewer meaningful
| operations common to the two.
| LudwigNagasena wrote:
| 1 is not a set, any set-theoretic construction of 1 is
| not literally 1.
| hanche wrote:
| I am not sure I understand what you mean by "literally"
| here. For sure, if you use Zermelo-Fraenkel set theory as
| the foundation of mathematics, as is commonly done, every
| mathematical object is a set. The first definition of 1
| encountered in that setting is the singleton set {0},
| where 0 is the empty set. (And 2={0,1}, 3={0,1,2} and so
| forth - you get the picture.) This is precisely the sort
| of thing this is all about: The natural numbers are
| uniquely described up to unique isomorphism by some
| variant of the Peano axioms after all.
| jiggawatts wrote:
| Mathematics is surprisingly weakly typed.
|
| For example, the "2" in "2p" is not the same type of "2" as
| in x^2 or 2x generally. Yet, physicists (to pick a random
| group) will blend in these factors, resulting in nonsense.
| As a random example, one of the Einstein field equations
| has "8p" in it. Eight _what!?_ What aspect of the universe
| is this counting out eight of -- a weirdly large integer
| constant? This actually ought to be "4(2pi)", and then "4"
| is the number of spacetime dimensions, which makes a lot
| more sense.
|
| Similarly, in at least one place the square of the
| pseudoscalar (I^2) was treated as a plain -1 integer
| constant and accidentally "folded" into other unrelated
| integer constants. This causes issues when moving from 2D
| to 3D to 4D.
| eru wrote:
| Haskell shows (one way of) how you can have numerical
| literals like 2 that can be used with many different
| types, but still be strongly statically typed.
|
| That by itself isn't a problem. But making all the other
| confusions you mention is a problem.
| generationP wrote:
| These examples miss the mark somewhat. The "2" in "2p"
| can mean several things (the nonnegative integer 2, the
| integer 2, the rational 2, the real 2) that are all
| commonly identified but are different. The "2" in "x^2"
| usually means the nonnegative integer 2. The "2" in "2x"
| can usually mean the nonnegative integer or the integer
| 2, but also the other 2's depending on what x is. The
| problem is not that the meaning of 2 varies across
| different expressions, but that it can vary within each
| single expression.
|
| The best example is perhaps the polynomial ring R[x][y],
| which consists of polynomials in the variable y over the
| ring of polynomials in the variable x over the real
| numbers. Any algebraist would tell you that it is
| obviously just the two-variable polynomial ring R[x, y]
| in disguise, because you can factor out all the y-powers
| and then the coefficients will be polynomials in x. But
| the rings are very much not the same at the level of
| implementation, and every time you use their "equality"
| (canonical isomorphy), you need to keep the actual
| conversion map (the isomorphism) in the back of your
| mind.
| gerdesj wrote:
| There are multiple things that we denote using a particular
| symbol: 1. 1 in and of itself is not a single concept. You
| could replace the symbol 1 with any other, even the sound of
| a fart and the concepts still remain the same. Given that we
| somehow agree that a fart sound shall be the way that we
| refer to a concept/object/thing.
|
| It's a largely useful conceit to use 1 for all of those
| objects and more besides. It makes talking about them easier
| but we do have to be careful to use the correct rule-set for
| their manipulation.
|
| I would personally prefer to see 1.0 for "rational 1" or
| perhaps 1. but that would require a convoluted sentence to
| avoid 1. being at the end of the sentence, unless we allow
| for: 1.! Well, that would work but what about 1.? Oh for ffs,
| I mean: 1..
|
| One notes that one's own ones may not be the same as one's
| other ones.
|
| If only I could spin "won", "own" and perhaps "wan" into that
| last sentence! ... Right, I've wedged in own. Needs some work
| 8)
| eru wrote:
| Well, you give give 1.0 for the rational one. But what
| about the real or complex one? Or what about the Gaussian
| Integer? What about the 2-adic one, or the 3-adic one, or
| any other p-adic one? What about the different kinds of
| floating point numbers?
|
| I don't think the rational one is special enough that we
| need to different notation just for her and for her alone.
| (Though that specific distinction can make sense in some
| contexts. Just not universally.)
| reaperman wrote:
| > (i.e., it depends what order you go)
|
| At the risk of utterly derailing this with irrelevant
| discussion: path-dependent systems are particularly tricky for
| some people IMHO. I think in a more state-based way, and my
| first rigorous dive into path-dependent calculation was during
| my chemical engineering degree -- I learned to be extremely
| vigilant about memorizing what was path-dependent and triple-
| checking if that affected the situation I was calculating.
|
| I do wish there was more rigorous exposure to them at lower
| levels of education and younger age. Because while I'm
| perfectly capable of handling path-dependent systems with
| proper focus and effort, my brain doesn't feel "native" when
| deriving solutions around those spaces - it feels similar to
| being "fluent enough" in another language. I feel this way
| about a lot of things -- I really feel I'd have been happier
| and more fulfilled if I'd been immersed in super rigorous
| first-principles education beginning around age 8-9. I didn't
| do well with things like "memorize this procedure for doing
| long division" and did much better with conceptual derivations
| of physics/math/science/historical arcs, etc.
| generationP wrote:
| The problem is that no one thinks of type conversions as
| taking any explicit paths! It's one thing to view the actual
| process of long division as path-dependent (something
| everyone who learns about Grobner bases is familiar with, as
| at the right level of generality even the result is path-
| dependent); it's another thing to apply the same intuition to
| the way the inputs are parsed. (You said divide 3 by 2 with
| remainder? Sure, the quotient is 3/2 and the remainder is 0.
| Problem?)
| reaperman wrote:
| > _The problem is that no one thinks of type conversions as
| taking any explicit paths!_
|
| Indeed. This is super surprising to me and I'm adding the
| topic to my "study" list. I had no idea until today - I
| easily could imagine it's possible if some of the type
| conversions are "lossy" (e.g. maps to lists), but I have a
| strong feeling that simpified lossy conversions are not
| what is being referenced.
| generationP wrote:
| Most of Buzzard's examples are indeed lossless (even
| bijective) conversions, but the notation mathematicians
| use (and programming languages often support) makes it
| look like they are completely absent, which comes back to
| bite you. In mathematics, it bites you when you want to
| actually compute your function and realize you don't
| remember how all those canonical arrows go. In
| programming, it bites you when the default conversions
| the compiler inserts aren't the ones you meant.
| zmgsabst wrote:
| Isn't that the intuition behind homotopy type theory --
| that equivalence is a path between types?
|
| (And related, eg, cubical type theory.)
| belter wrote:
| > Strictly speaking, the rational number 1 is not the same as
| the integer 1
|
| So does that mean you can have different 0 zero's ?
| lupire wrote:
| Yes
| gerdesj wrote:
| Note how your parent comment has specified "rational" 1 and
| "integer" 1. They use the symbol 1 for two similar concepts:
| We all "know" that 1 + 1 = 2 and 1.0 + 1.0 = 2.0. I have
| deliberately specified 1 for an int and 1.0 for a rational.
| Now we have two different representations for two very
| similar but not identical concepts.
|
| At which point does 1 + a tiny amount cease to be an integer?
| By definition that tiny amount can have any magnitude and 1
| plus anything will cease to be an integer. That is the
| property that defines an integer. Integers have subsequent
| "behaviours" that other types of numbers might lack.
|
| You have picked zero/0. Now that is a sodding complicated
| concept 8) There are lots of things called zero but no more
| nor less than any other.
|
| Zero might be defined by: 1 - 1 = 0. I have PS1 in my bank
| account and I pay out PS1 for a very small flower, my bank
| balance is now PS0. Lovely model, all good except that
| interest calcs intervened and I actually have a balance of
| PS0.00031. Blast. My pretty integer has morphed into a bloody
| complicated ... well is it a rational thingie or a ... what
| is it?
|
| Now I want to withdraw my balance. I put a shiny PS1 in,
| bought something and I have some change. What on earth does a
| 0.031p coin look like? Obviously, it doesn't exist. My lovely
| integer account has gone rational.
|
| Symbols mean what we agree on with some carefully and well
| chosen language. Mathematicians seem to think they are the
| ultimate aces at using spoken and written language to make
| formal definitions, derivations and so on. That is a bit
| unfair, obviously. We all believe that what we think is
| communicable in some way. Perhaps it is but I suspect that it
| isn't always.
|
| Have a jolly good think about what zero, nothing, 0 and so on
| really mean. Concepts and their description to others is a
| really hard problem, that some funky symbols sort of helps
| with.
|
| Yes there are loads of things called zero. If I had to guess:
| infinitely things are zero! Which infinity I could not say.
| eru wrote:
| Yes. 0/1, 0/2, 0/3 are all different in some sense, but they
| belong in the same equivalence class.
| Nevermark wrote:
| Even there, it would help to not apply the zero numerator
| equivalence class too early.
|
| I.e. 2/3, 2/5, 2/7 are the numbers that divide 2 to get 3,
| 5 and 7 respectively.
|
| Likewise, with full consistency, 0/1, 0/2, 0/3 cannot be
| reduced using common factors (the core equivalence for
| ratios), so have different ratio normal forms, and are the
| numbers that when they divide 0 produce 1, 2, and 3
| respectively. All consistently.
|
| The advantage of not applying zero numerator equivalence
| too early, is that you get reversibility, associativity and
| commutivity consistency in intermediate calculations even
| when zeros appear in ratios.
|
| You can still apply zero numerator ratio equivalence to
| final values, but avoid a lot of reordering of intermediate
| calculations required to avoid errors if you had applied it
| earlier.
|
| Of course, if you are coding it doesn't help that you are
| unlikely to find any numerical libraries, functions or
| numeric data types, that don't assume division by zero is
| an error, inf, or NaN, and that all zeros divided by non-
| zero numbers are equivalent to 0. So you simply can't get
| the benefits of holding off on that equivalence.
|
| You have to do a lot of reasoning and reordering to ensure
| generally correct results, as apposed to "I am sure it will
| be fine" results.
|
| I find it very surprising that this separate treatment of
| factor reduced equivalence, and zero numerator (and zero
| denominator) equivalences, on ratios, is not taught more
| explicitly. They are very different kinds of equivalence,
| with very different impacts on calculation paths.
| eru wrote:
| Thanks!
|
| I was actually toying with writing a rational number
| library going in the direction you sketch out. My
| inspiration was a trick in computational geometry for
| dealing with points at infinity. I think it's called
| homogeneous coordinates.
|
| My point was to treat both p and q in p/q as
| symmetrically as possible.
|
| Oh, I remember now: the motivating example was to write a
| nice implementation of an optimal player for the
| 'guessing game' for rational numbers.
|
| One player, Alice, commits to a (rational) number. The
| other player, Bob, makes guesses, and Alice answers
| whether the guess was too high, too low or was correct.
| Bob can solve this in O(log p + log q). And the
| continued-fraction-based strategy Bob wants to use is
| generally symmetrical between p and q. So I was looking
| into expressing the code as symmetrically as possible,
| too.
| xigoi wrote:
| How is the case of the zero numerator special? When you
| take any fraction 0/n with n>0 and reduce it by the
| greatest common factor, you get 0/1.
| ReleaseCandidat wrote:
| Which can be made "visible" by substituting 0 with e.g. `1
| - 1`: 0/1 = (1 - 1)/1 = 1/1 - 1/1
| 0/2 = (1 - 1)/2 = 1/2 - 1/2 ...
| zarzavat wrote:
| This doesn't sound right to me. The rational numbers are a
| superset of the integers. We know that there's only one 1 in
| the rational numbers, then it must be the same 1 object as the
| 1 in the integers.
|
| The statement "3/3 is in Z" is true. There's no conversion
| happening: 3/3 is a notation for 1, just like 0.999... is a
| notation for 1. Many notations, but only one 1 object.
|
| The case of R x R^2 = R^3 is different because the Cartesian
| product is _defined_ to produce a set of ordered pairs. So it
| cannot give rise to a set of triples any more than a dog can
| give birth to a cat. So either x is not a Cartesian product or
| = is isomorphism not equality.
| perforator wrote:
| Your statements such as
|
| > We know that there's only one 1 in the rational numbers,
| then it must be the same 1 object as the 1 in the integers. >
| The statement "3/3 is in Z" is true.
|
| make it sound very trivial while in reality it is not. I do
| not quite understand your example with R^3 but the _defined_
| applies equally to your statements. There are many ways to
| define and think about the objects you mentioned -- there is
| not one single truth. Unless you are a devoted platonist, in
| which case, it 's still like your opinion, man.
| ndriscoll wrote:
| Q is (usually) a set of equivalence classes of ZxZ\\{0}, so
| obviously it's not a superset of Z since they're not even the
| same types of things.
|
| There is however a canonical embedding of Z into Q, sending n
| to the class of (n,1).
| tobbe2064 wrote:
| Most people define it as the smallest set extending (the
| smallest set extending Z\\{0} where * is invertible) where
| + is invertible
| red_trumpet wrote:
| But such a set is not unique...
| eru wrote:
| You can easily define a Cartesian product that works on more
| than two sets at a time. See https://en.wikipedia.org/wiki/Ca
| rtesian_product#Cartesian_pr...
| jasomill wrote:
| 0.999... always reminds me of my favorite definition of the
| real numbers:
|
| "A _real number_ is a quantity _x_ that has a _decimal
| expansion_
|
| _x_ = _n_ + 0. _d_ 1 _d_ 2 _d_ 3..., (1)
|
| where _n_ is an integer, each _d_ is a digit between 0 and
| 9, and the sequence of digits doesn't end with infinitely
| many 9s. The representation (1) means that
|
| _n_ + _d_ 1/10 + _d_ 2/100 + [?] + _d_ [?]/10^k <= _x_ < _n_
| + _d_ 1/10 + _d_ 2/100 + [?] + _d_ [?]/10^k + 1/10^k
|
| for all positive integers _k_."[1]
|
| Defining the reals in terms of binary expansion is left as an
| exercise for the reader[2].
|
| [1] Knuth, _The Art of Computer Programming_ , Volume 1,
| Third Edition, p. 21.
|
| [2] _Ibid._ , p. 25, exercise 5.
| AlecBG wrote:
| I'm not sure I agree. That sort of type conversion involves
| inclusions, while the examples Buzzard talked about involved
| isomorphisms
| types_vs_sets wrote:
| Inclusions are a form of isomorphism. In the more common
| developments of elementary arithmetic, Q is _constructed_
| from Z, and in particular the subset of integral rational
| numbers are technically a different ring from Z. The
| conversion Z \to Q in particular is an isomorphism from Z to
| that subset.
|
| Type conversions in every day programming languages though
| sometimes not only fail to be surjective, they can also fail
| to be injective, for example int32 -> float32.
|
| type-conversions and "implicit isomorphisms" differ because
| the former does not need to be invertible, but they agree in
| that they are implicit maps, that are often performed without
| thought by the user. So I think that the type-conversions
| analogy is pretty good in that it captures the idea that
| implicit conversions, when composed in different ways from A
| to B, can arrive at various values, even if each stage along
| the way the choices seemed natural.
| nyc111 wrote:
| When this subject comes up I always think that the equality sign
| is loaded. It can mean, definition, equality, identity, and
| proportionality. How come this state of the equality sign is not
| mentioned in the paper?
| mikhailfranco wrote:
| _up to (non-)unique isomorphism_
| mxmlnkn wrote:
| As far as I remember, that's not a problem in math:
|
| := definition [?] identity = equality [?] proportionality
| nyc111 wrote:
| But this is how it works:
|
| = definition = identity = equality = proportionality
| Twisol wrote:
| Big-O notation is a famous example where = is some flavor
| of (asymptotic) proportionality, and it catches a lot of
| people out when they first learn about it.
| yau8edq12i wrote:
| As a mathematician, I have never, ever seen the equal sign used
| to denote proportionality. I cannot tell what you mean by
| "identity" that wouldn't be equality. And a definition in the
| sense you seem to mean is, indeed, also an equality. I guess
| this issue not mentioned in the paper because it doesn't exist.
| ducttapecrown wrote:
| [x:y] = [lx:ly]
|
| and I suppose the model of localization discussed in the
| article above counts as well.
| yau8edq12i wrote:
| ... What? That's just symbol soup. What are you trying to
| write? Do it in latex if it helps.
| laurent_du wrote:
| It's not symbol soup, it's projective coordinates. Did
| you claim to be a mathematician? I merely have a PhD in
| Mathematics and a few papers in peer-review journals, so,
| unlike you, not a real mathematician, and I immediately
| understood the point.
| yau8edq12i wrote:
| Uh... I have a PhD, I'm a tenured professor, and I even
| supervise a couple of PhD students. How about you? Given
| your snarky tone, it sounds like you'd have mentioned
| something like this. Not sure why you'd try to flex when
| you don't know much about me ;)
|
| With my font, the letter l looked like a vertical bar |.
| Hence why this looked like symbol soup. But okay, let's
| say it's about projective spaces. Then surely, you
| realize that the equal sign still denotes equality. The
| point [1:2] is literally equal to [2:4] in P^2, not
| "proportional". Perhaps you need a refresher: https://en.
| wikipedia.org/wiki/Equivalence_class#quotient_set
| xanderlewis wrote:
| I agree it's not really used symbolically, but isn't it
| referring to the difference between, say:
|
| (x + y)(x - y) = x^2 - y^2
|
| (an identity, since it's true for every x and every y) and
| something more arbitrary like
|
| 3x^2 + 2x - 7 = 0
|
| (an equation certainly not valid for all x and whose
| solutions are sought).
|
| Of course, really, the first one is a straightforward
| equality missing some universal quantification at the
| front... so maybe that's just what the triple equals sign
| would be short for in this case.
| lupire wrote:
| "When is one thing equal to some other thing?"
|
| Barry Mazur June 12, 2007
|
| https://bpb-us-e1.wpmucdn.com/sites.harvard.edu/dist/a/189/f...
|
| https://people.math.osu.edu/cogdell.1/6112-Mazur-www.pdf
| ajkjk wrote:
| I'm typing this after reading their section on page 6 about the
| "pentagon axiom". They write that RxR^2, R^2xR, and R^3 are
| isomorphic, but not literally equal under different
| constructions, because (a,(b,c)) is different from ((a,b), c),
| and that this is a problem. I feel like math kinda gets this
| wrong by treating sets as meaningful objects on their own.
| Physics gets it closer to correct because it tries to be
| "covariant", where the meaningful answers to questions have to
| either have units on them or be totally unitless e.g.
| irrespective of coordinate system.
|
| The two spaces Rx(RxR) and (RxR)xR have many isomorphisms between
| them (every possible coordinate change, for instance). But what
| matters, what makes them "canonically isomorphic", is not
| isomorphisms in how they are _constructed_ but in how they are
| _used_. When you write an element as (a,b,c), what you mean is
| that when you are asked for the values of three possible
| projections you will answer with the values a, b, and c.
| Regardless of how you define your product spaces, the product of
| (a), (b), and (c) are going to produce three projections that
| give the same answers when they are used (if not, you built them
| wrong). Hence they are indistinguishable, hence canonically
| isomorphic.
|
| This is exactly the way that physics always treats coordinates:
| sure, you can write down a function like V(x), but it's really a
| function from "points" in x to "points" in V, which happens to be
| temporarily written in terms of a coordinate system on x and a
| coordinate system on V. We just write it as V(x) because we're
| usually going to use it that way later. Any unitless predictions
| you get to any actual question are necessarily unchanged by those
| choices of coordinate systems (whereas if they have units then
| they are measured in one of the coordinate systems).
|
| So I would say that (a,(b,c)) and ((a,b), c) are just two
| different coordinate systems for R^3. But necessarily any math
| you do with R^3 can't depend on the choice of coordinates. There
| is probably a way to write that by putting something like "units"
| on every term and then expecting the results of any calculation
| to be unitless.
| generationP wrote:
| This is exactly the "specification by universal property" that
| the author is talking about. In your case, it's saying "a
| 3-dimensional vector space is a vector space with three chosen
| vectors e, f, g and three linear maps x, y, z such that each
| vector v equals x(v) e + y(v) f + z(v) g". But as the author
| points out, not everything follows from universal properties,
| and when it does, there is often several universal properties
| defining the same object, and that sameness itself needs to be
| shown.
| ajkjk wrote:
| Yes, I know it's the meaning of it, but I'm saying that the
| presence of "units" allows you to sort of... operationalize
| it? In a way that removes the ambiguity about what's going
| on. Or like, in theory. I dunno it's a comment on the
| internet lol.
| eru wrote:
| Units help with some common cases, but units still don't
| allow you to distinguish between, say, energy, work and
| torque.
| ajkjk wrote:
| I think that is due to insufficient imaginativeness. For
| example, energy and work are the same units but energy is
| an absolute quantity while work is a delta. So arguably
| work should be a sort of tangent element of the energy,
| rather than the same thing. There's no distinction in
| flat space but if you e.g. changed coordinates such that
| energy was on the surface of a sphere, then work is a
| spherical displacement instead, which is a totally
| different class of objects.
|
| Likewise, torque is only in the same units because we
| don't regard radians as a unit, but we should. They are
| distinctly different.
| eru wrote:
| Radians can be seen as a ratio of two lengths, the length
| of your arc and the length of the circumference of the
| unit circle. All units cancel in such ratios.
|
| > There's no distinction in flat space but if you e.g.
| changed units such that energy was on the surface of a
| sphere, then work is a spherical displacement instead,
| which is a totally different class of objects.
|
| Well, maybe. But in other circumstances you want to treat
| eg heat and work interchangeably. Just look at
| https://en.wikipedia.org/wiki/Work_(thermodynamics) and
| https://en.wikipedia.org/wiki/Work_(physics) and
| https://en.wikipedia.org/wiki/Work_(electric_field)
|
| Basically, how much you _want_ to encode in your type
| system depends on the needs of your application.
| (Approximately all type systems can be made to work for
| all applications. But they differ in the degree of
| convenience and error proneness.)
| yau8edq12i wrote:
| I think it's the first time that I witness this comic
| https://xkcd.com/793/ happening but with math as a target.
| mathgradthrow wrote:
| You use R^3 in your example of why coordinates don't matter.
| R^3 can be covered by _one_ chart. Maybe your argument would be
| more convincing if you pick a different manifold. I have no
| idea what your complaint is otherwise.
| ajkjk wrote:
| I'm not talking about charts of R^3; I'm talking about the
| different isomorphic constructions of products like ((a, b),
| c) and (a, (b, c)) as being a sort of 'choice of coordinate
| system' on the isomorphic class of objects.
| mathgradthrow wrote:
| yes, and these choices dont matter individually, but how
| these choices glue together does, in fact, depend on all of
| them collectively.
| rhelz wrote:
| This is a very old consideration (cf
| https://www.jstor.org/stable/2183530).
|
| If you want to frame a 'universal defining property', you have to
| frame it in some language. The definition, therefore, is
| inevitably idiosyncratic to that language, and, if you specify
| the same property using a different language, the definition is
| going to change. What's more, the two definitions can be
| incommensurable.
|
| And---all you have done is translate from the object language to
| the meet language--leaving the definitions of the terms of the
| meta language completely unexplicated.
|
| The solution to this is as old too---like "point", "line", etc,
| these terms can--and arguably should--remain completely _un_
| -defined.
| ysofunny wrote:
| whence did you learn this idiom of "the meet language"???
|
| i have _working_ definitions of line, point, etc.. in terms of
| dimensions. but I have some issues with the precise definition
| of "dimension" due to having picked up the concept of
| "density". I cannot say what's the difference between density
| and dimension
| jhanschoo wrote:
| Meet here is shorthand the comment author is using for:
| https://en.wikipedia.org/wiki/Join_and_meet
|
| You should read it as: "the largest group of properties that
| both languages agree about said abstractly defined
| mathematical object."
| yau8edq12i wrote:
| How can you frame a paper from 1965 as "very old" when the
| linked article is about Grothendieck, who started his math PhD
| in 1950 (and presumably studied math before that)?
| ysofunny wrote:
| reminicscent of Euler's use of Pi?
|
| I recall that Euler would write Pi but sometimes he meant 2*pi,
| or possibly pi/2 depending on context
| hackandthink wrote:
| This is an excellent text to understand mathematical
| structuralism.
|
| But it feels anticlimactic.
|
| At the beginning there are fundamental problems with mathematical
| equality.
|
| In the end, there is no great new idea but only the observation
| that in algebraic geometry some proofs have holes (two kinds),
| but they can be filled (quite) schematically.
| ducttapecrown wrote:
| "Some proofs" are the proof used to verify that the definition
| of an affine scheme makes sense, and the author motions in the
| direction that _every_ single proof in algebraic geometry uses
| identically wrong arguments when using the language of
| "canonical" maps.
|
| Thus the replication crisis of mathematics is revealed. In the
| words of John Conway: a map is canonical if you and your office
| neighbor write down the same map.
| abeppu wrote:
| I haven't actually dug up the source, so I'm not sure if the gaps
| here are related, but GC Rota apparently claimed that one reason
| the umbral calculus remained mysterious for as long as it did was
| about ambiguities with `=`.
|
| > Rota later stated that much confusion resulted from the failure
| to distinguish between three equivalence relations that occur
| frequently in this topic, all of which were denoted by "=".
|
| https://en.wikipedia.org/wiki/Umbral_calculus#The_modern_umb...
| dan_mctree wrote:
| There's so much ambiguous context that goes into your average
| '=', even when just talking about your standard functions on
| real numbers. You'll see it being used for anything from:
|
| - We've found these to be equal
|
| - We're hypothesizing this to be equal
|
| - These are approximately equal
|
| - These are defined to be equal
|
| - This is a way to calculate something else, whether it's equal
| is up to your philosophy (a^2+b^2=c^2)
|
| - I'm transforming my function into something else that looks
| different but is exactly the same
|
| - I'm transforming my function into something else that is the
| same for some of the stuff I care about (but for example does
| not work anymore for negative numbers, complex nrs, etc.)
|
| - I'm transforming my function into something else, but it's
| actually a trapdoor, and you can't convert it back.
|
| - This is kind of on average true within an extremely
| simplified context or we know it's not true at all, but we'll
| pretend for simplification (looking at you physics)
|
| - We are trying to check if these two are equal
|
| - This is equal, but only within a context where these
| variables follow some constraints mentioned somewhere else
| entirely
|
| - This is equal, but, we're not going to say whether you can or
| can't replace the variables with functions or whether it
| supports complex nrs, negative nrs, non-integers, etc.
|
| A lot of this is usually kind of clear from context, but some
| of these differences are a nightmare if you want to code it out
| perihelions wrote:
| I was just thinking about something adjacent to this the other
| day. I had this half-baked idea that you could classify all the
| "types" built out of, say (R, x, -) by algebraically replacing
| each copy of R with a finite set of cardinality _a_ and then
| counting the cardinality of the entire type expression. So you 'd
| formally associate, say, R^3 with the algebraic term a^3, and
| that holds regardless of how you rearrange R^3 = R^2 x R or R x
| R^2 or whatever. I liked the idea because it seemed (?) to derive
| non-obvious set theoretic equivalences, for free: such as
| R -> (R -> R) ~ (a^a)^a = a^(a^2) R^2 -> R ~
| a^(a^2) (R -> R)^2 ~ (a^a)^2 = a^(2a)
| R -> R^2 ~ a^(2a)
|
| The first equivalence is between a "curried", partial-
| application, function form of a function of two arguments, and
| the "uncurried" form which takes a tuple argument. The second
| equivalence is between a pair of real functions and a path in the
| plane R^2--the two functions getting identified with the
| coordinate paths x(t) and y(t). (Remember the cardinality of
| distinct functions over finite sets S -> T is |T|^|S|).
|
| And I think you can take this further, I'm not sure how far, for
| example by associating different formal parameters a,b,c... for
| different abstract types S,T,U... Is this a trick that's already
| known, in type theory?
|
| (My motivation was to try to classify the "complexity", "size",
| of higher-ordered functions over the reals. The inspiration's
| that you're imagining a numerical approximation on a grid of size
| _a_ for (a finite subinterval in) each copy of R: then that
| cardinality relates to the memory size of the numerical
| algorithm, working inside that space. And you could interpret the
| asymptotic growth of the formal function, as a complexity measure
| of the space. If you think of R^n - > R as a "larger" function
| space than R -> R^n, that observation maps to a^(a^n) being an
| asymptotically faster-growing function (of 'a') than (a^n)^a =
| a^(na). And similarly the functionals, (R -> R) -> R, and
| function operators (like differential operators) (R -> R) -> (R
| -> R), form a hierarchy of increasing "size").
| cvoss wrote:
| The connection between type isomorphisms and algebraic
| equalities is known and explored in a variety of interesting
| ways.
|
| I don't know the precise history of the development of the
| notation and vocabulary, but there's a reason types like A+B
| are notated with a plus symbol and called "sums". Similarly for
| products. And it may surprise you (or not) to learn that people
| sometimes call A -> B an exponential type, and even notate it
| with superscript notation.
|
| One of my favorites is the result that the binary tree type is
| isomorphic to septuples of binary trees, which you can arrive
| at by using the definition of binary trees as the fixed point
| solution of T = 1 + T*T and deriving T = T^7 with some algebra.
| [0]
|
| [0] https://arxiv.org/abs/math/9405205
| n_plus_1_acc wrote:
| This has been studied under the name algebraic data types.
| joewferrara wrote:
| kevin buzzard is a very good(usually math) expositor with a bent
| towards programming. love it
| _as_text wrote:
| I really like this. I remember my first serious math book, which
| was this old-school set theory and topology book, and being all
| excited about learning set theory up until I encountered iterated
| Cartesian product, and was forced to accept that ((x, y), z) and
| (x, (y, z)) are supposed to be indistinguishable to me. An answer
| on StackExchange said that "you will never, ever, ever need to
| worry about the details of set theory", but I still did.
| giardini wrote:
| And I thought "Grothendieck" was a German social disease! I'm
| getting a real education here on HN!
| hanche wrote:
| The story of Grothendieck is really fascinating. He was a
| superstar in algebraic geometry, only to suddenly reject the
| endeavor of mathematics and going off to grow vegetables in the
| Pyrenees. He also demanded that all notes from his lectures be
| destroyed. But those notes existed in so many hands, I don't
| think many people (if any) complied.
___________________________________________________________________
(page generated 2024-05-21 12:01 UTC)