Archive:
Subtopics:
Comments disabled |
Wed, 07 Aug 2019
Technical devices for reducing the number of axioms
In a recent article, I wrote:
There was a sub-digression, which I removed, about a similar sort of device that does have practical value. Suppose you have a group !!\langle G, \ast \rangle!! with a nonempty subset !!H\subset G!!, and you want to show that !!\langle H, \ast \rangle!! is a subgroup of !!G!!. To do this is it is sufficient to show three things:
Often, however, it is more convenient to show instead:
which takes care of all three at once. [Other articles in category /math] permanent link Mon, 05 Aug 2019After decapitating Medusa the Gorgon, Perseus flies home on the winged sandals lent to him by Hermes, But he stops off to do some heroing. Below, he spots a beautiful princess Andromeda, chained to a rock. Here's the description my kids got from D'Aulaire's Book of Greek Myths:
Here's the d’Aulaires’ picture of the pasty-faced princess: Andromeda has been left there to distract a sea monster, which will devour her instead of ravaging the kingdom. Perseus rescues her, then murders her loser ex-boyfriend, who was conspicuously absent from the rendezvous with the monster. Perseus eventually marries Andromeda and she bears his children. Very good. Except, one problem here. Andromeda is Princess Royal of Ethiopia, the daughter of King Cepheus and Queen Cassiopeia. She is not pale like a marble statue. She has dark skin. How dark is not exactly clear. For the Greeks “Aethiopia” was a not entirely specific faraway land. But its name means the land of people with burnt faces, not the land of people who are pale like white marble. The D'Aulaires are not entirely at fault here. Ovid's Metamorphoses compares her with marble:
But he's also quite clear (in Book II) that Ethiopians have dark skin:
(Should we assume that Ovid evokes marble for its whiteness? Some marble isn't white. I don't know and I'm not going to check the original Latin today. Or perhaps he only intended to evoke its stillness, for the contrast in the next phrase. Anyway, didn't the Romans paint their marble statuary?) Andromeda was a popular subject for painting and sculpture over the centuries, since she comes with a a built-in excuse for depicting her naked or at least draped with wet fabric. European artists, predictably, made her white: But at least not every time:
Abraham van Diepenbeeck, 1655
Copy by Bernard Picart, 1731
[Other articles in category /book/myth] permanent link Sat, 03 Aug 2019
Git wishlist: aggregate changes across non-contiguous commits
(This is actually an essay on the difference between science and engineering.) My co-worker Lemuel recently asked if there was a way to see all the
changes to The closest he could come was Lemuel's imaginary command would solve another common request: How can
I see all the changes that I have landed on He said:
I remember that when I was first learning Git, I often felt boggled in this way. Why can't it just…? And there are several sorts of answers, of which one or more might apply in a particular situation:
Often, engineers will go straight to #5, when actually the answer is in a higher tier. Or they go to #4 without asking if maybe, once the desiderata are clarified a bit, it will move from “impossible” to merely “difficult”. These are bad habits. I replied to Lemuel's (implicit) question here and tried to make it a mixture of 2 and 3, perhaps with a bit of 4:
If A and B are on a separate branch and are completely unrelated to C
and D, it is hard to see what to do here. But it's not impossible.
Our hypothetical command could produce the same output as And if A, B, C, D are all related and on the same branch, say with D , then C, then B, then A, the situation is simpler and perhaps we can do better. If so, very good, because this is probably the most common case by far. Note that Lemuel's request is of this type. I continued:
This is a serious question, not a refutation. Lemuel could quite
reasonably reply by saying that it should show 0 changing to 3, the
intermediate changes being less important. (“If you wanted to see
those, you should have used It may be that that wouldn't work well in practice, that you'd find there were common situations where it really didn't tell you what you wanted to know. But that's something we;d have to learn by trying it out. I was trying really hard to get away from “what you want is stupid” and toward “there are good reasons why this doesn't exist, but perhaps they are surmountable”:
I hoped that Lemuel would take up my invitation to continue the discussion and I tried to enocurage him:
Let's consider another example. Suppose some file contains functions X, Y, Z in that order. Commit A removes Y entirely. Commit B adds a new function, YY, between X and Z. Commit C modifies YY to produce YY'. Lemuel asks for the changes introduced by A and C; he is not interested in B. What should happen? If Y and YY are completely unrelated, and YY just happens to be at the same place in the file, I think we definitely want to show Y being removed by A, and then that C has made a change to an unrelated function. We certainly don't want to show all of YY beind added. But if YY is considered to be a replacement for Y, I'm not as sure. Maybe we can show the same thing? Or maybe we want to pretend that A replaced Y with YY? That seems dicier now than when I first thought about it, so perhaps it's not as big a problem as I thought. Or maybe it's enough to do the following:
This is certainly doable. If there ware no conflicts, it would certainly be better than [Other articles in category /prog] permanent link Tue, 23 Jul 2019
Obtuse axiomatization of category theory
About ten years ago I started an article, addressed to my younger self, reviewing various books in category theory. I doubt I will ever publish this. But it contained a long, plaintive digression about Categories, Allegories by Peter Freyd and Andre Scedrov:
In light of my capsule summary of category theory, can you figure out what is going on here? Even if you already know what is supposed to be going on you may not be able to make much sense of this. What to make of the axiom that !!□(xy) = □(x(□y))!!, for example? The explanation is that Freyd has presented a version of category theory in which the objects are missing. Since every object !!X!! in a category is associated with a unique identity morphism !!{\text{id}}_X!! from !!X!! to itself, Freyd has identified each object with its identity morphism. If !!x:C\to D!!, then !!□x!! is !!{\text{id}}_C!! and !!x□!! is !!{\text{id}}_D!!. The axiom !!(□x)□ = □x!! is true because both sides are equal to !!{\text{id}}_C!!. Still, why phrase it this way? And what about that !!□(x(□y))!! thing? I guessed it was a mere technical device, similar to the one that we can use to reduce five axioms of group theory to three. Normally, one defines a group to have an identity element !!e!! such that !!ex=xe=x!! for all !!x!!, and each element !!x!! has an inverse !!x^{-1}!! such that !!xx^{-1} = x^{-1}x = e!!. But if you are trying to be clever, you can observe that it is sufficient for there to be a left identity and a left inverse:
We no longer require !!xe=x!! or !!xx^{-1}=e!!, but it turns out that you can prove these anyway, from what is left. The fact that you can discard two of the axioms is mildly interesting, but of very little practical value in group theory. I thought that probably the !!□(x(□y))!! thing was some similar bit of “cleverness”, and that perhaps by adopting this one axiom Freyd was able to reduce his list of axioms. For example, from that mysterious fourth axiom !!□(xy) = □(x(□y))!! you can conclude that !!xy!! is defined if and only if !!x(□y)!! is, and therefore, by the first axiom, that !!x□ = □y!! if and only if !!x□ = □(□y)!!, so that !!□y = □(□y)!!. So perhaps the phrasing of the axiom was chosen to allow Freyd to dispense with an additional axiom stating that !!□y = □(□y)!!. Today I tinkered with it a little bit and decided I think not. Freyd has: $$\begin{align} xy \text{ is defined if and only if } x□ & = □y \tag{1} \\ (□x)□ & = □x \tag{2} \\ (□x)x & = x \tag{3} \\ □(xy) & = □(x(□y)) \tag{4} \end{align} $$ and their duals. Also composition is associative, which I will elide. In place of 4, let's try this much more straightforward axiom: $$ □(xy) = □x\tag{$4\star$} $$ I can now show that !!1, 2, 3, 4\star!! together imply !!4!!. First, a lemma: !!□(□x) = □x!!. Axiom !!3!! say !!(□x)x = x!!, so therefore !!□((□x)x) = □x!!. By !!4\star!!, the left-hand side reduces to !!□(□x)!!, and we are done. Now I want to show !!4!!, that !!□(xy) = □(x(□y))!!. Before I can even discuss the question I first need to show that !!x(□y)!! is defined whenever !!xy!! is; that is, whenever !!x□ = □y!!. But by the lemma, !!□y=□(□y)!!, so !!x□ = □(□y)!!, which is just what we needed. At this point, !!4\star!! implies !!4!! directly: both sides of !!4!! have the form !!□(xz)!!, and !!4\star!! tells us that both are equal to !!□x!!. Conversely, !!4!! implies !!4\star!!. So why didn't Freyd use !!4\star!! instead of !!4!!? I emailed him to ask, but he's 83 so I may not get an answer. Also, knowing Freyd, there's a decent chance I won't understand the answer if I do get one. My plaintive review of this book continued:
Apparently some people like this book. I don't know why, and perhaps I never will. [Other articles in category /math] permanent link Thu, 11 Jul 2019
The New York City passport office
Earlier this week I reported on a good visit I had had to the Philadelphia offices of the Social Security Administration. Philadelphia government offices, in my experience, are generally better than those I have visited elsewhere. I've never been to the New York DMV office (do they even have one?) but the Philadelphia ones are way better than the New Jersey ones I used to use. Instead of standing in line for forty-five minutes, you get a number and sit down until your number is called. The passport office was the biggest surprise. I first went in to deal with some passport thing shortly after I arrived in Philadelphia, maybe 1990 or so. The office was clean and quiet, the line was short, I got my business done quickly. None of those is the case in the New York passport office. The New York passport office. Wow. Where to begin? I want to say that it defies description. But, I learned later, it has been described by no less a person than Samuel Beckett:
Here's a story of the New York passport office told to me by a friend many years ago. He stood in the line for forty-five minutes, and when he reached the window, he handed over his forms. The clerk glared at him for a few seconds, then, without a word, pushed them back. “Is something wrong?” asked my friend. There was a long pause. The clerk, too disgusted or enraged to reply immediately, finally said “They're not stapled.” “Oh,” said my friend. “I see you have a stapler on your desk there.” “You're supposed to staple them.” “May I use your stapler?” “No, your stapler is on the table at the back of the room.” At this point my friend realized he was dealing with a monster. “Okay, but I can come right back to the window afterward, right?” “No, you have to wait, like everyone else.” At that moment my friend felt a tap on his shoulder. A man a few places behind him in line reached into his suit pocket and handed him a stapler. My friend says that as he stapled his papers and turned them in, the look on the clerk's face was of someone whose whole day had just been ruined. “Thanks so much,” said my friend to Stapler Man. “Why did you happen to have a stapler in your pocket?” “Oh,” said Stapler Man. “I do a lot of business at the passport office.” [Other articles in category /misc] permanent link Sun, 07 Jul 2019[ I wrote this in 2007 and forgot to publish it. Or maybe I was planning to finish it first. But if so I have no idea what I was originally planning to say, so here we are. ] In computer programs, it's quite common to need a numerical value for π. Often you see something like: #define PI 3.141592654 This has the drawback of not representing π as exactly as possible. But to do that in C probably requires putting in 16 digits after the decimal point, and most people don't have so much memorized. And anyway, you don't really know at compile time what the floating-point precision will be; some platforms support quad-width floats. So you can do better, maybe, by using the math library to calculate π. And people do: static double pi = 4*atan2(1,1); The atan2(y, x) function produces the (almost-)unique value θ from the range !![-\pi, \pi]!! such that a ray from the origin, passing through point (x, y), makes angle θ with the x-axis. Note that the arguments have y first and x second.
For example, You can use But this is a bit strange. Why is this so well-known? Why calculate 4*atan2(1,1) when $$\pi = {\operatorname{atan2}}(0,-1)$$ produces the same result and is simpler? (Obligatory IEEE 754 complaining: [ Addendum: Leah Neukirchen suggests that the [Other articles in category /prog] permanent link Tue, 02 Jul 2019
Philadelphia Slaughterhouse Hotel
More information about the mysterious slaughterhouse hotel has come to light, thanks to Chas. Owens, Pete Krawczyk, and this useful blog post by D.S. Rosenstein. Most important, the perplexing “hotel” is not intended for humans. “Hotel” is apparently stockyard jargon for a place where livestock are quartered temporarily just prior to slaughter. I am so glad to have this cleared up. Also, M. Rosenstein has a photograph of the fancy abattoir with the spires: They don't make industrial buildings like they used to. Check out the ornamental pattern in the bricks on the lower floor and the baluster along the riverside façade. [ Addendum: Josh Bevan of Hidden City Philadelphia on When Cattle Men Reigned In The West (of Philadelphia). ] [Other articles in category /history] permanent link
Philadelphia Slaughterhouse Hotel
Yesterday on my other blog I posted about the most hilariously mislocated hotel I've ever heard of. It's the hotel that in 1910 was located in the Philadelphia stockyards, just the other side of the railroad tracks from the hog pens, between the slaughter house and the abbatoir: I thought that would be the end of it, but Chas. Owens did a little digging around and found a picture of the hotel, provided by the Greater Philadelphia GeoHistory Network. It's from R. Hexamer's insurance survey of 1877. At that time, the building was partly a hotel and partly the offices of the Philadelphia Stock Yard Company. The survey includes a map of the site and a description of the facilities. Here's the detailed plan of the hotel: The full image is 105 MB: None of these buildings is still standing. (As I mentioned yesterday, the site is now occupied by the Cira Centre.) But the neighborhood's history as the center of Philadelphia's meatpacking district is not completely lost. According to this marvelous article from Hidden City Philadelphia, in 1906 the D.B. Martin company built a new combination office building and slaughterhouse only two blocks away at 3000 Market Street. Here's my favorite detail from the article:
That building still stands, although I believe it's no longer used as a slaughterhouse. [ Addendum 20190702: The “hotel” is explained: it is a temporary residence for livestock, not for humans. ] [Other articles in category /history] permanent link Tue, 25 Jun 2019
Projection morphisms are (not) epic
I don't have a good catalog in my head of basic theorems of category theory. Every time I try to think about category theory, I get stuck on really basic lemmas like “can I assume that a product !!1×A!! is canonically isomorphic to !!A!!?” Or “Suppose !!f:A→B!! is both monic and epic. Must it be an isomorphism?” Then I get sidetracked trying to prove those lemmas, or else I assume they are true, go ahead, and even if I'm right I start to lose my nerve. So for years I've wanted to make up a book of every possible basic theorem of category theory, in order from utterly simple to most difficult, and then prove every theorem. Then I'd know all the answers, or if I didn't, I could just look in the book. There would be a chapter on products with a long list of plausible-seeming statements:
and each one would either be annotated, Snopes-style, with “True”, or with a brief description of a counterexample. On Sunday I thought I'd give it a shot, and I started with:
This seems very plausible, because how could the product possibly work if its left-hand component couldn't contain any possible element of !!A!!? I struggled with this for rather a long time but I just got more and more stuck. To prove that !!π_1!! is an epimorphism I need to have !!g,h:A→C!! and then show that !!g ∘ π_1 = h ∘ π_1!! only when !!g=h!!. But !!π_1!! being a projection arrow doesn't help with this, because products are all about arrows into !!A!! and !!B!! and here I need to show something about arrows out of !!A!!. And there's no hope that I could get any leverage by introducing some arrows into !!A!! and !!B!!, because there might not be any arrows into !!B!!. (Other than !!\text{id}_B!!, of course, but then you need an arrow !!B→A!! and that might not exist either.) Or what if I consider how the arrows from !!A×B!! factor through !!C×B!! — ah ah ah, not so fast! !!C×B!! might not exist! I eventually gave up and looked it up online, and discovered that, in fact, the claim is not true in general. It's not even true in Set. The left projection !!π_1: X×\emptyset → X!! is not epic. (Which answers my rhetorical question above that asks “how could the product possibly work if…”) So, uh, victory, I guess? I set out to prove something that is false, so failing to produce a proof is the best possible outcome. And I can make lemonade out of the lemons. I couldn't prove the theorem, and my ideas about why not were basically right. Now I ought to be able to look carefully at what additional tools I might be able to use to make the proof go through anyway, and those then become part of the statement of the theorem, which then would become something like “If all binary products exist in a category with an initial object, then projection morphisms are epic.” [Other articles in category /math] permanent link Mon, 24 Jun 2019I just finished Cakes and Ale, by W. Somerset Maugham. I have enjoyed Maugham all my life, and this is considered one of his best books (it was his personal favorite) but I hadn't read it before. I enjoyed it a lot. It has a story, but at the center instead of a big problem there is a character, Rose Gann. (To other characters she appears to be a big problem, but she sails placidly through the book doing what she wants.) She's really sweet, and I'm glad I had a chance to meet her. The other side of the book is that it is a very pointed satire of the social-climbing literary circles in which Maugham traveled. Another such satire is his short story The Creative Impulse. That one was exaggerated for comic effect. This one isn't, and because of that it's much more biting. Rose, who is not literary, is contrasted with the literary characters, who are hypocritical, self-serving, manipulative, and pretentious. Rose is none of those things. The book is quasi-autobiographical, the way Of Human Bondage or the Ashenden stories are. The narrator is named Willie Ashenden and the pattern of his life is the same as Maugham's, growing up in Whitstable with his vicar uncle (in the book it's called “Blackstable”) and then going to medical school in London, etc. Rose Gann was inspired by a woman that Maugham had been in love with. There was a scandal when the book was published; one of the characters was widely understood to be a rather vicious parody of Maugham's literary acquaintance Hugh Walpole. (Maugham denied it, but I've also read that later, when the danger of a libel suit was past, he confessed it was true.) Parts of Cakes and Ale reminded me strongly of Robertson Davies' The Manticore. In both books, a famous and important man has died and everyone is rushing around to grab a piece of his legacy. In both cases there's also an embarrassing first wife that everyone wants to write out of the story. I imagine Davies had probably read Cakes and Ale and I wondered if he had been thinking of it. Davies wrote an essay about Maugham, which I suppose I've read, but I don't remember what he said. [Other articles in category /book] permanent link Thu, 20 Jun 2019
Sufficiently advanced software
A couple of days ago my sleepy brain mashed up Clarke's Law:
and Hanlon's Razor:
to produce these words of wisdom: Any sufficiently advanced software is indistinguishable from malice. (Why yes, I had spent the evening dealing with Git. Why do you ask?) This sounded like something Bryan Horstmann-Allen would have said, so with his permission, I am naming it after him. BDHA's Law? BDHA's Razor? No! [Other articles in category /misc] permanent link Mon, 17 Jun 2019
Don't let the man page write checks that the programmer can't cash
My big work project is called “Greenlight”. It's a Git branch merging
service. After you've pushed a remote branch, say
Greenlight analyzes the branch to see if it touches any sensitive code
that requires signoffs. If so it contacts the correct people on
Slack, and asks them to review it. Once they have approved it,
Greenlight rebases the branch onto the current
A user, Locksher, complained last week that it didn't do what he had
expected. He had a Git With Greenlight, this check wasn't done, because Locksher never pushed
to Locksher asked if it was possible to have Greenlight “respect local
hooks”. Once I understood what he wanted, my first suggestion was
that he wrap the
and get exactly the desired behavior. I said that if Locksher wanted to implement this, I would include it in the standard client, or alternatively I would open a ticket to implement it myself, eventually. Locksher suggested instead that the
I didn't have time then to answer in detail, so I just said:
Here's what I said to him once I did have time to answer in detail:
I will elaborate a little on the main items 1–2, that different
people might have different ideas about what it means to “respect” a
local hook. Consider Locksher's specific request, for So then I would have to add an escape hatch for Zubi, so that everyone who didn't want Locksher's feature would have to affirmatively opt out of it. Nah. [Other articles in category /prog] permanent link |