You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Verity Scheel (Jul 29 2022 at 20:17):Hey! I haven’t been active here in several months. I just wanted to stop by and share a blog post I wrote about the Eudoxus construction of the real numbers:
https://cofree.coffee/~verity/Eudoxus.html
Of course I learned about the construction on the nlab, and I decided to blog about it once I had the insight that it’s all about slope! This is why function composition gives multiplication in this setting. And in particular it’s about slope as we could interpret it from a graphing calculator: pixelated lines aka integer functions.
That’s the key insight in the blogpost and if you’re too advanced you might not get a whole lot out of it, but I tried to make it more accessible and explain the intuition behind what’s happening, with some graphs to help explain. I’m also really proud of my efforts styling it as well 😊
I have another post on LR(1) parsing that I’m hoping to turn into a series. And I hope to keep posting on other topics too. Interactive type theory, intricacies of FRP, music notation – we’ll see.
P.S. If you have any easily-digestible references on what decidability means, I would be happy to link to them. Decidability comes up with monotonicity and defining inverses. It’s cool to see those issues in this setting: you need to know whether an integer function is representing a positive or negative slope before you can monoticize it or define its inverse. Contrast that with Cauchy reals, where you can roughly define the data of the inverse for an arbitrary sequence, but need to know that the sequence converges away from zero to prove that the inverse sequence converges.
Alex Gryzlov (Jul 29 2022 at 20:43):Decidability comes up in constructive settings, as it's trivial in a classical one. nlab has https://ncatlab.org/nlab/show/decidable+subset, which also links to decidable equality and decidable objects.
Verity Scheel (Jul 29 2022 at 20:56):Yeah. Ideally I'd like something that explains in some depth why some properties are undecidable and what that means without using a ton of jargon, and how it differs from proving a property/knowing from a proof that the property holds. I just liked to the Wikipedia page on computable sets for now: https://en.wikipedia.org/wiki/Computable_set. It does a little better on the jargon front than the nlab but doesn't have a lot of depth either.
Alex Gryzlov (Jul 29 2022 at 22:10):https://en.wikipedia.org/wiki/Decision_problem might be a bit better as an intro?
Verity Scheel (Jul 29 2022 at 23:55):Ah yes, that looks more substantial. Thanks!
Eduardo Ochs (Jul 30 2022 at 03:03):Verity Scheel said:
I have another post on LR(1) parsing that I’m hoping to turn into a series. And I hope to keep posting on other topics too. Interactive type theory, intricacies of FRP, music notation – we’ll see.
Your post on parsing is fantastic! I was looking for something like that to show to my students... thanks! =)
Lucas Queiroz (he/him/his) (Jul 31 2022 at 15:20):Verity Scheel said:
Hey! I haven’t been active here in several months. I just wanted to stop by and share a blog post I wrote about the Eudoxus construction of the real numbers:
https://cofree.coffee/~verity/Eudoxus.htmlOf course I learned about the construction on the nlab, and I decided to blog about it once I had the insight that it’s all about slope! This is why function composition gives multiplication in this setting. And in particular it’s about slope as we could interpret it from a graphing calculator: pixelated lines aka integer functions.
That’s the key insight in the blogpost and if you’re too advanced you might not get a whole lot out of it, but I tried to make it more accessible and explain the intuition behind what’s happening, with some graphs to help explain. I’m also really proud of my efforts styling it as well 😊
I have another post on LR(1) parsing that I’m hoping to turn into a series. And I hope to keep posting on other topics too. Interactive type theory, intricacies of FRP, music notation – we’ll see.
P.S. If you have any easily-digestible references on what decidability means, I would be happy to link to them. Decidability comes up with monotonicity and defining inverses. It’s cool to see those issues in this setting: you need to know whether an integer function is representing a positive or negative slope before you can monoticize it or define its inverse. Contrast that with Cauchy reals, where you can roughly define the data of the inverse for an arbitrary sequence, but need to know that the sequence converges away from zero to prove that the inverse sequence converges.
I think the Eudoxus construction of the real numbers is very interesting and fascinating. I wish I had heard of it before!
Verity Scheel (Jul 31 2022 at 15:45):Yeah I think the Eudoxus construction is cool! Besides the historical accidents, I think it's less well-known because it doesn't correspond to a familiar completion operation like the Cauchy and Dedekind constructions do (c.f. https://mathoverflow.net/questions/239921/concept-associated-to-the-eudoxus-reals). I just think it's cool for the intuition and the fact it doesn't use rationals. In fact, I think you can construct the nonnegative reals using only natural numbers.
Verity Scheel (Jul 31 2022 at 16:59):Eduardo Ochs said:
Your post on parsing is fantastic! I was looking for something like that to show to my students... thanks! =)
Thanks for your feedback! If you have any suggestions or requests I'd be happy to hear them :) I know there's still a lot of work to do there before I will be satisfied.
Jason Erbele (Aug 01 2022 at 15:43):I'm just now reading your (very cool) blog post on Eudoxus reals, and there's a minor error in the Details box in the Slope converges section. The long inequality at the top of the box should end with instead of . Fortunately it doesn't affect any results, but fixing it gets you to a bound on slightly more directly. :upside_down:
Verity Scheel (Aug 01 2022 at 16:17):Ooops, silly mistake. Pushed a fix now. Thank you!