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.
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.
(And related, eg, cubical type theory.)
This happened to me yesterday
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
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.
> 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
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! :)
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.
> 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.
There is however a canonical embedding of Z into Q, sending n to the class of (n,1).
One way to do things is to define N as von Neumann ordinals:
https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...
Then you define Z as an equivalence relation of NxN by the equivalence (a,b) ~ (c,d) iff a+d=c+b. This means each integer is itself an infinite set of pairs of natural numbers.
Then you define Q as an equivalence relation of ZxZ\{0} by (a,b) ~ (c,d) iff ad = cb. Again, each rational is now an infinite set of pairs of integers.
The point of the OP post is that we want to define things by their properties, but then we are defining what a set of rational numbers is, not what the set of rational numbers is, and we need to make sure we do all proofs in terms of the properties we picked (e.g. that Q is a field, there is a unique injective ring homomorphism i_ZQ: Z->Q, and if F is a field such that there is an injective ring homomorphism i_ZF: Z->F, then there is a unique field homomorphism i_QF: Q->F such that i_ZF = i_QF after i_ZQ) rather than relying on some specific encoding and handwaving that the proof translates to other encodings too. This might be easier or harder to do depending on which properties we use to characterize the thing, and the OP paper gives adding inverses to a ring as one of its examples in section 5 ("localization" is a generalization of the process of constructing Q from Z. For example, you could just add inverses for powers of 2 without adding inverses of other primes), proposing a different set of properties that they assert is easier to work with in Lean.
“A real number is a quantity x that has a decimal expansion
x = n + 0.d₁d₂d₃…, (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₁/10 + d₂/100 + ⋯ + dₖ/10^k ≤ x < n + d₁/10 + d₂/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.
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.
So does that mean you can have different 0 zero's ?
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 £1 in my bank account and I pay out £1 for a very small flower, my bank balance is now £0. Lovely model, all good except that interest calcs intervened and I actually have a balance of £0.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 £1 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.
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.
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.
Think of 0 as a prime number for the purpose of ratio factor reduction.
Treating 0/2 and 0/3 as the same number is an entirely different equivalence.
If you start saying 0/x is 0 then of course 0/2 and 0/3 are zero. (Or equivalently that 0 x 2 = 0 x 3 = 0.) But that is an entirely different equivalence from factor reduction.
If you don’t start with that assumption and reduce 0/2 and 0/3 only according to shared factors, you find that all three numbers, 0, 2, and 3 can only be factored as a product of 1 and themselves.
(Thus a slightly generalized version of primes, for whole numbers instead of just natural numbers.)
So 0/2 and 0/3 are completely factor reduced.
The equivalence of 0/x = 0/2 = 0/3 = 0/1 = 0 is a separate equivalence. One which is not reversible, I.e. it erases information, and may break commutivity requiring special handling (exception generation, NaN representation, or calculation reordering, etc) if it is applied during intermediate calculations.
If you don’t apply the zero equivalence’s until a final value is calculated, you will always get the same answer, but will have avoided a need for special handling of intermediate calculations.
For instance, an intermediate division by zero followed by a multiplication of zero will cancel, avoiding any need to reorder calculations and yet resulting in the same final answer.
0/1 = (1 - 1)/1 = 1/1 - 1/1
0/2 = (1 - 1)/2 = 1/2 - 1/2
...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).
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.
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.
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.
When you construct numbers using sets under ZFC axioms or inside lambda calculus what you get is representation. But 1 is just 1.
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.
Saying that 0 belongs to 1 is false no matter what one uses to represent those numbers in any ZFC formalisation of numbers.
It’s a map-territory distinction.
On a more serious note, if you are of a certain philosophical bent you may believe that the natural numbers have an existence independent of and outside of the minds of humans. If so, 1 is presumably not a set, even if we don’t fully understand what it is. I certainly don’t think of it as a set on a day to day basis!
But others may deny that the territory even exists, that all we have are the maps. So in this one map, 1 is a set containing zero, but in that other map, it is something different. The fact that all the different maps correspond one-to-one is what counts in this worldview, and is what leads to the belief – whether an illusion or not – that the terrain does indeed exist. (And even the most hard nosed formalist will usually talk about the terrain as if it exists!)
But this is perhaps taking us a bit too far afield. It is fortunate that we can do mathematics without a clear understanding of what we talk about!
For that matter, how do we know what infinite sets like Z and Q 'literally are', without appealing to a system of axioms? The naive conception of sets runs headlong into Russell's paradox.
For example, the "2" in "2π" 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 "8π" 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.
That by itself isn't a problem. But making all the other confusions you mention is a problem.
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.
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)
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.)