kmill

Higher homotopy groups of spheres goes way back to the 30s. This isn't lazy writing. https://en.m.wikipedia.org/wiki/Homotopy_groups_of_spheres

Looking at all the continuous functions from all dimensions of spheres into a particular topological space ends up giving rich algebraic information about the space. This is a cornerstone of algebraic topology. Turns out calculating this stuff for even just spheres can be subtle and mysterious.

Uniform distance matters not at all for any of this, but it does matter that your family of "spheres" be topologically equivalent to the round spheres.

Another model is you take the iterated suspensions starting with a pair of points (the zero sphere).

Yet another is to take boundaries of simplicies, or even cubes.

Topologists are those who are perfectly happy to call a paper towel tube an annulus.

I'm now remembering a couple hundred slides I saw scattered on the sidewalk and street on Cesar Chavez near Sanchez in early 2020. I picked up a couple to take a look, but I can't recall what they were of anymore...

That's the first I'd heard that Rust-oleum was named for one of its original pigments rather than its rust-protection capabilities. I can't find anything to substantiate your story, but I did learn that the inventor pursued fish-based primers after observing that fish oil prevented the spread of rust on fishing vessels.

Interestingly, when people speak slowly it comes out as "je swee zanglais". The terminal sound is deposited onto the following word!

"Set-theoretic type theory" is working with the lattice of all subsets of possible values, where a "type" is one of these subsets. This lattice has plenty of structure, but sure individual subsets do not.

The category of sets is different from this lattice, since it allows arbitrary functions between sets for its morphisms rather than just inclusions.

"Set-theoretic types" have a meaningful notion of overlap. Usually types in other type system tend to be practically disjoint, like objects in a concrete category might be sets but the category itself doesn't give language to check whether the objects are disjoint sets.

I once wrote a final exam for a linear algebra course with a section "all the following are false, explain why." I did it to make it easier than a T/F, but it was unintentionally devious. So many students said some of them were true anyway and tried to prove them...

Just to clarify, continuations don't have a snapshot of the whole heap, and they can be thought of as being a snapshot of just the interpreter state for a particular execution thread (roughly the call stack and source position). If heap objects are modified between creating a continuation and calling it, then the continuation will see the modified versions of all those objects. When it comes to garbage collection, continuations keep any objects referred to in their saved call stack alive. This is similar to any other closure, but instead of keeping things alive according to lexical scope, this is more of a dynamic scope thing (it's based on whatever functions happened to call this one).

Persisting a continuation seems like it's similarly as challenging as persisting an arbitrary closure. Like usual there are things you can't really persist, for example in your call stack you might have some unwind handlers for closing files -- how do you persist file handles?

The paper is about trying to statically analyze this. As I understand it, fip-annotated functions are ones that are checked to neither allocate nor deallocate.

Lean 4 uses FBIP, but it looks like this paper is about something called FIP, which is related but about guaranteeing there are no allocations or deallocations. FBIP as I understand it is more about being able write functional code in a natural away while avoiding allocations or deallocations.

(I agree about Lean 4 as becoming a great general purpose language though!)

The verb/noun stuff I understand was the UI for the astronauts (the DSKY). There was also the native instruction set for the CPU as well as an interpreter with a richer instruction set built on top of that, and they used this to more easily write complex navigation programs. Wikipedia mentions some of this at https://en.wikipedia.org/wiki/Apollo_Guidance_Computer around the phrase "virtual machine." I'm not sure it being interpreted code would aid in field reprogrammability, since it would have been woven into the rope memory just like the rest of the software.

You might also like the fact that the Apollo Guidance Computer (which ran at a similar speed) was also programmed using something like bytecodes. It didn't have to drive a graphical display though, only a spaceship.

Yep. Still, it turns out there's a lot you can do with non-Turing-complete languages, and it's nice knowing that a program will definitely finish.

Here's an equivalent-ish problem:

Given a programming language, what's the smallest program that's an infinite loop?

Some languages are designed to never let you write infinite loops (every program halts in them), but maybe there's a mistake and they accidentally let some non-halting programs slip through.

I've seen interleaved lexing and parsing, where the recursive descent parser asks for the next token, which is computed on demand.

They're still separate modules. You just don't have to run lexing to completion ahead of time (and as a consequence, it's natural to let lexing be context-sensitive where needed).

A handwavy argument for this is that if you continuously deform your picture, you can bring an upright and an inverted image toward each other until they cancel out (if you've ever played around with curved mirrors you probably can imagine how that would look). Eventually, after doing enough of these cancelations, you're left with an undistorted picture with a single upright image -- so, you must have had n inverted images and n+1 upright ones. The morse theory the wikipedia article mentions is roughly about being able to do this argument rigorously.

It's also the origin of the integral sign! (Mentioned on the Wikipedia article.) There's a nice accidental parallel between sigma notation (the discrete, "angular" summation) and integral notation (the continuous, "smooth" summation).

Another s fact is that Greek has lower case σ and additionally the variant ς that only appears at the ends of words, which is very Latin-s-like. https://en.wikipedia.org/wiki/Sigma

I think it's the same 'from' as 'far from home', but I'm not British so take that with a grain of salt.

Even 'work from home' is weird. The only way I can read it if I really think about it is your work is coming from home.

Ah, but they didn't say they used nearest-neighbor when scaling it back down. This gives a (theoretically) better result when you want to scale up by a non-integer factor. (If it ends up just being an integer factor then there's no need to scale things back down.)

This feels similar to how you can generate high-quality square waves at frequencies that don't evenly divide the sampling rate. You generate it at a higher sampling rate, band limit it to the Nyquist frequency of the destination, then downsample. Otherwise there is aliasing phenomena that gives unwanted audible artifacts. For nearest-neighbor resized images, I suppose that would just appear as pixels of varying sizes, which is not nice to look at. Scaling it down antialiases the pixel so they optically look the same size.

It's amusing that parsing theory was already at least 1-2 decades old by the time they made this mistake (consider that ALGOL 60 had a complicated grammar, introducing BNF too). I'd chalk it up to this being a shell language that was evolved rather than designed.

My wife once purchased a ticket over the phone for the Acela line from the Penn Station in New York, but they misheard it as the one in Newark. So it's even hard for Amtrak!

Something we learned out of all this was that each train company used to have their own station in each city, before things became consolidated, so it makes sense for there to be many stations for the Pennsylvania Railroad.

I've been using ChatGPT/GPT-3 as a French tutor, to answer questions about different ways to say things, formally or informally. It's not always accurate, but still I learn from it.

Amusingly, there's a mildly rude expression that means "I don't care," and ChatGPT's strong aversion to swearing biased it toward completely fabricating a word-for-word translation. It insisted that the verb was a conjugation of something innocuous, and when I pointed out that that verb doesn't conjugate that way, it both agreed with me and continued insisting.

It seems to have a pretty solid grasp of language in general (so long as you don't need any hard logic), and it's a fun tool to come up with ideas you personally never had before.

This was a little experiment the other day; it's delightful how many silly (yet justified) reasons why you can't walk to Hawaii it came up with. But what do you expect from someone who's only learned about the world by reading the Internet?

> By "unsummarizing" we mean to take some text and expand upon it at length, using fancy words, extra facts, anecdotes, and interesting observations. Your goal is to unsummarize the following text as much as possible.

> Text to unsummarize: What do you mean I can't walk to Hawaii? (GPT-3 follows)

> You may be surprised to learn that it is impossible to walk to the Hawaiian Islands from anywhere on the mainland United States. Though the Hawaiian Islands are located in the middle of the Pacific Ocean and are roughly 2,400 miles away from the nearest point on the mainland, it is not possible to walk there due to the vast expanse of ocean between them. Even the most dedicated and determined walker would be unable to traverse the depths of the Pacific. The nearest point of land to the Hawaiian Islands is the Johnston Atoll, which is located approximately 1,400 miles away. That is to say, it is not feasible to traverse the 1,000 miles of open ocean between Johnston Atoll and the Hawaiian Islands by foot.

> The Hawaiian Islands were formed as a result of volcanic activity, and the chain of islands were formed over millions of years. This activity is responsible for creating the immense walls of water that separate the islands from the mainland. The Pacific is one of the deepest, widest oceans on the planet, and its depths are not suitable for walking. The bottom of the ocean is filled with a variety of topographical features, such as trenches, ridges, and seamounts, which make it a difficult environment for walking. Additionally, the ocean is filled with a variety of natural hazards, such as hazardous currents, extreme temperatures, sharks, and other dangerous marine life. All of these factors make walking to the Hawaiian Islands not only difficult, but also impossible.

Another number system, which I learned about recently on HN, are the Kaktovik numerals, which are even closer to D'ni. Interestingly, they were developed just a couple of years before Riven was released.

https://en.wikipedia.org/wiki/Kaktovik_numerals

It's not a base-5 system exactly. It's base-20, where the rotated-and-superimposed digit is only one of the first three numerals. I guess you could call it a mixed-radix system, where the bases alternate like 4 5 ... 4 5 4 5 and where each group of 4 5 combines into a single symbol.

This sort of rotation-and-superposition number system also appears (in base 5 too!) in the game Riven: https://dni.fandom.com/wiki/D%27ni_Numerals

It's sort of funny how both Kaktovik and the D'ni numerals were invented around the same time (1994 for Kaktovik and 1997 for when Riven was released).

Sure, I'm a mathematician, but what point are you making beyond a potential ad hominem?

I myself include code in my own papers when it's useful. As the author of this paper mentioned (and it's something I'm a bit embarassed I missed), the asymptotics of this new algorithm do not compete with the usual O(n^3) algorithm, so it's not clear to me that having Python code would benefit anyone. Of course you never know, though I think the underlying concepts in their formula are significantly more difficult to learn than the notation itself, so the code also wouldn't help very much with understanding the formula.

Anyway, given that you're saying I'm in an ivory tower, doesn't that give me some authority to explain why the choice to not include code has nothing to do with it being an "insult" to the community or it "spoiling" the paper with "disgustingly usable code"?

Are you familiar with the different stages of research? This is "basic research" -- they found a new determinant formula and analyzed it. Others can pick up their work and continue, for example creating implementations and comparing their runtimes in practice. I think including a determinant implementation would be detrimental if it were not accompanied by this additional analysis, since people might use this implementation as the standard implementation, but very likely in practice there will be many implementation tricks to get it to work competitively.

They're certainly not above writing code. You seem to have missed the appendix, where they wrote some to prove that their bound on the tensor rank of 4x4 determinants over GF2 is exactly 12. https://gitlab.com/apgoucher/det4f2

Also, a formula is not an algorithm. You can oftentimes extract an algorithm from a formula, but the value of a formula in pure math is to be able to write something in a different way. Formulas reveal structure that (hopefully) can be exploited when solving other problems.

> People could even get down to running the code just to check that the formula actually works !

This is an interesting perspective, but you have to take into account that papers are written for some audience in mind -- this one is written for combinatorialists (hence the math.CO designation on the arXiv). It's not too hard of an exercise to plug this formula into Mathematica for this audience. But also, this audience would rather see a proof than computational evidence.

Here's the website where they kept track of the status of the Sphere Eversion Project: https://leanprover-community.github.io/sphere-eversion/

They have a dependency graph that shows the general structure of the argument: https://leanprover-community.github.io/sphere-eversion/bluep...

I can't really compare non-standard analysis with filters due to not knowing much about NSA, but filters are a natural sort of completion of the poset of subsets, the pro-completion. Every subset can be naturally regarded as a filter (a principal filter), and I think of filters in general are sort of "thick" sets -- sets with some sort of infinitesimal fringe. There's also a helpful coincidence that open filters (filters on the poset of open subsets of a topological space) can be perfectly represented as filters.

It makes sense to work with "functions" whose domains and ranges are filters. From this perspective, a function X -> Y is continuous at x if it can be restricted to be a function nbhd x -> nbhd f(x), where nbhd x denotes the principal open filter from all the open neighborhoods of x.

If you're familiar with the germ at x of a smooth function f : X -> R, this is exactly the same concept as the restriction of f to a function nbhd x -> R. It's also possible to restrict to a germ at any given subset of f, which I think is neat. For example, you can restrict a smooth function to an infinitesimal neighborhood of a smooth submanifold.

These are some of the reasons why I think that filters have some "user friendliness," once you get a feel for them.

Thanks for confirming -- I didn't trust my own ears for such a strange fragment of a sentence!

It turns out it comes from a book called "The Foolish Dictionary: An exhausting work of reference to un-certain english words, their origin, meaning, legitimate and illegitimate use, confused by a few pictures" by Wurdz and Goldsmith. (Talk about nominative determinism -- a dictionary by Wurds?)

Full entry:

HAMMOCK From the Lat. hamus, hook, and Grk. makar, happy. Happiness on hooks. Also, a popular contrivance whereby love-making may be suspended but not stopped during the picnic season.

Ah, thanks for the report -- it seems not to work on mobile Chrome. One of our Equestrians will take care of it on the next sprint.

A surprising recent bit of news is that we learned that there's a phishing website out there somewhere that mysteriously redirects to endless.horse.

We tried adding endless.horse to a database of non-phishing urls (after all, it's merely an ASCII art horse with abnormally long legs), but the one we were pointed to by the security researchers hasn't allowed new accounts for the last two years. It's a strange being implicated in this indirect way -- Does endless.horse condone phishing? The horse says "neigh."