Post B5ad7uTgJQe8Uudm76 by neauoire@merveilles.town
(DIR) More posts by neauoire@merveilles.town
(DIR) Post #B5abH2pOR6FJ5q1YAq by neauoire@merveilles.town
0 likes, 0 repeats
Made this little graphic to explain how Rejoice does rewriting.https://wiki.xxiivv.com/site/rejoice
(DIR) Post #B5acBmf5DMKhScFzWa by d6@merveilles.town
0 likes, 0 repeats
@neauoire maybe it's just my previous exposure to overline notation in logic/type systems where the premise goes above the conclusion but i found this pretty hard to read.also, the use of y in x^y to refer to the "current" y's exponent also confused me for a moment until i realized what you were doing -- i'm used to seeing this notation in math where x^y would have a totally different meaning.
(DIR) Post #B5acESZqLQmA2R59P6 by neauoire@merveilles.town
0 likes, 0 repeats
@d6 yeah that's why I made the video :)
(DIR) Post #B5acH8kYWBylPjN39E by d6@merveilles.town
0 likes, 0 repeats
@neauoire ohhhhhh :) it didn't animate for me.sorry for the noise!
(DIR) Post #B5acQWXDSL7fmtbc9o by labtoast@social.nouveau.community
0 likes, 0 repeats
@neauoire that first arc from the x to the denominator x is unclear to me. Why does the y exponent become a negative 2 and what does that have to do with x^3?
(DIR) Post #B5acdO1aPLyn9swce8 by neauoire@merveilles.town
0 likes, 0 repeats
@labtoast variable exponents take the value of the symbol during application. If y is 5, then x^y means x^5.
(DIR) Post #B5aczD0e2i9hMluTWS by labtoast@social.nouveau.community
0 likes, 0 repeats
@neauoire right, so how do we know that y is 2 here? We raise it to the 2nd power in the first bit, but that's all the info we're given on it as far as I can tell.
(DIR) Post #B5ad1NrQfVzxbHdWOu by neauoire@merveilles.town
0 likes, 0 repeats
@d6 aaah yes, damn, I took for granted that just any could mouse-hover, but I didn't think of people on mobile X(
(DIR) Post #B5ad7uTgJQe8Uudm76 by neauoire@merveilles.town
0 likes, 0 repeats
@labtoast what do you mean by "how do we know"?
(DIR) Post #B5ad8Syi2ZfTUzQ2CG by khm@hj.9fs.net
0 likes, 0 repeats
I do not understand any individual aspect of what is going on here
(DIR) Post #B5adGQhmNLeSlXIUOO by neauoire@merveilles.town
0 likes, 0 repeats
@khm mhmm let's see. If I say.. the multiplication of a number by a fraction is like adding the prime factor in the numerator and subtracting the prime factor in the denumerator, does it helps understanding the idea better?
(DIR) Post #B5adQuvOsGlXO0fXrk by labtoast@social.nouveau.community
0 likes, 0 repeats
@neauoire "Variable exponents take the value of the symbol during application." y is translated into 2 here, no? So that must mean the value of y is 2. Where is y set to 2?I get the sense that I'm thinking about this the wrong way. Perhaps this diagram isn't meant to stand alone? Let me read up on rejoice more and come back to this.
(DIR) Post #B5adahg8ygENCTCQrI by neauoire@merveilles.town
0 likes, 0 repeats
@labtoast on the left, y^2 means there are two instances of y in the "bag".Similarly to how the number 18 is made of [2 3^2], or [2 3 3], or 2 * 3 * 3. Imagine that instead of using numbers, you used symbols, so [a b^2].If you want to add as many instances of "c" as there are "b", you could say c^b
(DIR) Post #B5adjgL9K9Ofeef1xw by labtoast@social.nouveau.community
0 likes, 0 repeats
@neauoire ooooh, so you take the current exponent value of y when interpreting it as a variable exponent, but the value of y itself is irrelevant as it's just a symbol. I see!Super cool :D
(DIR) Post #B5aeQlTK7Tzs1U1m2C by khm@hj.9fs.net
0 likes, 0 repeats
18 * (5/9) = 10 is something I can get behindwhat are [233] [3^2] and [25] here?
(DIR) Post #B5al3nlu6R0SAqiS3s by neauoire@merveilles.town
0 likes, 0 repeats
@khm these are the prime factors of the values above.18 = 2 * 3 * 39 = 3 * 310 = 2 * 5
(DIR) Post #B5al9NBhqzdfSmRQg4 by shanecelis@mastodon.gamedev.place
0 likes, 0 repeats
@neauoire Wow, Gödel numbering is still kind of mind bending.
(DIR) Post #B5al9NYkTK4QcFDpaq by neauoire@merveilles.town
0 likes, 0 repeats
@shanecelis it is! And its relationship to the application of fractions to encode computation is just wild.