The Universe of Discourse


Wed, 07 Aug 2019

Technical devices for reducing the number of axioms

In a recent article, I wrote:

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. …

The fact that you can discard two of the axioms is mildly interesting, but of very little practical value in group theory.

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:

  1. !!H!! is closed under !!\ast!!
  2. !!G!!'s identity element is in !!H!!
  3. For each element !!h!! of !!H!!, its inverse !!h^{-1}!! is also in !!H!!

Often, however, it is more convenient to show instead:

For each !!a, b\in H!!, the product !!ab^{-1}!! is also in !!H!!

which takes care of all three at once.


[Other articles in category /math] permanent link

Mon, 05 Aug 2019

Princess Andromeda

After 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:

On the way home, as he flew over the coast of Ethiopia, Perseus saw, far below, a beautiful maiden chained to a rick by the sea. She was so pale that at first he thought she was a marble statue, but then he saw tears trickling from her eyes.

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:

As soon as Perseus, great-grandson of Abas, saw her fastened by her arms to the hard rock, he would have thought she was a marble statue, except that a light breeze stirred her hair, and warm tears ran from her eyes.

But he's also quite clear (in Book II) that Ethiopians have dark skin:

It was [during Phaethon episode], so they believe, that the Ethiopians acquired their dark colour, since the blood was drawn to the surface of their bodies.

(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:

Painting by Gustave Doré, 1869.

But at least not every time:

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 master from the last week that pertained to a certain ticket. The relevant commit messages all contained the ticket ID, so he knew which commits he wanted; that part is clear. Suppose Lemuel wanted to see the changes introduced in commits C, E, and H, but not those from A, B, D, F, or G.

The closest he could come was git show H E C, which wasn't quite what he wanted. It describes the complete history of the changes, but what he wantwa is more analogous to a diff. For comparison, imagine a world in which git diff A H didn't exist, and you were told to use git show A B C D E F G H instead. See the problem? What Lemuel wants is more like diff than like show.

Lemuel's imaginary command would solve another common request: How can I see all the changes that I have landed on master in a certain time interval? Or similarly: how can I add up the git diff --stat line counts for all my commits in a certain interval?

He said:

It just kinda boggles my mind you can't just get a collective diff on command for a given set of commits

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:

  1. It surely could, but nobody has done it yet
  2. It perhaps could, but nobody is quite sure how
  3. It maybe could, but what you want is not as clear as you think
  4. It can't, because that is impossible
  5. I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question

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:

Each commit is a snapshot of the state of the repo at a particular instant. A diff shows you the difference between two snapshots. When you do git show commit you're looking at the differences between the snapshot at that commit and at its parent.

Now suppose you have commit A with parent B, and commit C with parent D. I come to you and say I want to see the differences in both A and C at that same time. What would you have it do?

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 git show A C. Or it could print an error message Can't display changes from unrelated commits A, C and die without any more output. Either of those might be acceptable.

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:

Suppose, for example,that C changes some setting from 0 to 1, then B changes it again to be 2, then A changes it a third time, to say 3. What should the diff show?

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 git show A C.”)

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'm not trying to start an argument, just to reduce your bogglement by explaining why this may be less well-specified and more complex than you realize.)

I hoped that Lemuel would take up my invitation to continue the discussion and I tried to enocurage him:

I've wanted this too, and I think something like it could work, especially if all the commits are part of the same branch. … Similarly people often want a way to see all the changes made only by a certain person. Your idea would answer that use case also.

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:

  1. Take all the chunks produced by the diffs in the output of git show .... In fact we can do better: if A, B, and C are a contiguous sequence, with A the parent of B and B the parent of C, then don't use the chunks from git show A B C; use git diff A C.

  2. Sort the chunks by filename.

  3. Merge the chunks that are making changes to the same file:

    • If two chunks don't overlap at all, there's no issue, just keep them as separate chunks.

    • If two chunks overlap and don't conflict, merge them into a single chunk

    • If they overlap and do conflict, just keep them separate but retain the date and commit ID information. (“This change, then this other change.”)

  4. Then output all the chunks in some reasonable order: grouped by file, and if there were unmergeable chunks for the same file, in chronological order.

This is certainly doable.

If there ware no conflicts, it would certainly be better than git show ... would have been. Is it enough better to offset whatever weirdness might be introduced by the overlap handling? (We're grouping chunks by filename. What if files are renamed?) We don't know, and it does not even have an objective answer. We would have to try it, and then the result might be that some people like it and use it and other people hate it and refuse to use it. If so, that is a win!


[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:

I keep this one around on the shelf just so that I can pick it up ever few months and marvel at its opacity.

It is a superb example of the definition-theorem-remark style of mathematics textbooks. I have heard that this was a style pioneered by a book you are already familiar with, John Kelley's General Topology of 1955. If so, all I can say is, sometimes it works, and sometimes it doesn't. It worked for Kelley in 1955 writing about topology.

Here is an example of what is wrong with this book.

Everyone who knows anything about category theory knows that a category is a sort of abstraction of a domain of mathematical objects, like sets, groups, or topological spaces. A category has a bunch of "objects", which are the sets, the groups, or the topological spaces, and it has a bunch of "morphisms", which are maps between the objects that preserve the objects' special structure, be it algebraic, topological, or whatever. If the objects are sets, the morphisms are simply functions. If the objects are groups, the morphisms are group homomorphisms; if the objects are topological spaces, the morphisms are continuous maps. The basic point of category theory is to study the relationships between these structure-preserving maps, independent of the underlying structure of the objects themselves. We ignore the elements of the sets or groups, and the points in the topological spaces, and instead concentrate on the relationships between whole sets, groups, and spaces, by way of these "morphisms".

Here is the opening section of Categories, Allegories:

1.1 BASIC DEFINITIONS

The theory of CATEGORIES is given by two unary operations and a binary partial operation. In most contexts lower-case variables are used for the 'individuals' which are called morphisms or maps. The values of the operations are denoted and pronounced as:
!!□x!! the source of !!x!!,
!!x□!! the target of !!x!!,
!!xy!! the composition of !!x!! and !!y!!,
The axioms:
!!xy!! is defined iff !!x□ = □y!!,
!!(□x)□ = □x!! and !!□(x□) = x□!!,
!!(□x)x = x!! and !!x(x□) = x!!,
!!□(xy) = □(x(□y))!! and !!(xy)□ = ((x□)y)□!!,
!!x(yz) = (xy)z!!.

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:

There must be an identity !!e!! such that !!ex=x!! for all !!x!!, and for each !!x!! there must be an !!x^{-1}!! such that !!x^{-1}x=e!!.

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:

Another, briefer complaint about this book: Early on, no later than page 13, Freyd begins to allude to "Lazard sheaves". These are apparently an important example. Freyd does not define or explain what "Lazard sheaves" are. Okay, you are expected to do some background reading, perhaps. Fair enough. But you are doomed, because "Lazard sheaves" is Freyd's own private coinage, and you will not be able to look it up under that name.

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:

The abode is a flattened cylinder with rubber walls fifty meters in circumference and eighteen meters high. It is constantly illuminated by a dim, yellow light, and the temperature fluctuates between 5°C to 25°C, sometimes in as small an interval as four seconds. This leads to extremely parched skin, and the bodies brush against each other like dry leaves. Kisses make an "indescribable sound" and the rubber makes the footsteps mostly silent. There are 200 inhabitants, or one per square meter. Some are related to each other. Some are even married to each other, but the conditions make recognition difficult.

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

Calculating π with atan2()

[ 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(yx) 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.

Diagram showing
the atan2() function.  A ray from the origin through the point (1,1)
is labeled “atan2(1,1) = π/4”.  A ray through an arbitrary point (x,y)
has the angle θ with the positive x-axis.  And a ray pointing along
the negative x-axis is labeled “atan2(0,-1) = π”.

Note that the arguments have y first and x second. For example, atan2(17, 0) returns !!\frac\pi 2!!, because a line at angle !!\frac\pi 2!! passes through the point (0, 17). Similarly, atan2(-17, 0) returns -!!\frac\pi 2!!.

You can use atan2 to calculate π, by using !!4·{\operatorname{atan2}}(1,1)!!, as I mentioned above. Many people do; Google searching finds hundreds of examples. The manual for the standard Perl module constant.pm mentions this example.

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: atan2 should return an always-unique value from !!(-\pi, \pi]!!, but I have to say “almost-unique” because as usual IEEE 754 fucks everything up, this time with its stupid distinction between 0 and -0.)

[ Addendum: Leah Neukirchen suggests that the atan2(1,1) is a translation from earlier systems that provide a single-argument atan function but no atan2. In those systems, there is no workable analogue of atan2(0, -1) because the transformation !!{\operatorname{atan2}}(y, x)\Rightarrow {\operatorname{atan}}\left(\frac yx\right)!! gives !!{\operatorname{atan}}(0)!!, which doesn't work for this application as it yields !!0!! instead of the desired !!\pi!!. And similarly in languages with atan but not atan2 there is no analogue of !!\pi = 2·{\operatorname{atan2}}(1, 0)!!. So the simplest thing you can do is pi = 4 * atan(1), and after the transformation above one gets !!\pi = 4·{\operatorname{atan2}}(1,1)!!. ]


[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:

An isometric drawing of
the  abbatoir, which  is a handsome and
ornate building, featuring four blue spires at each corner. A grayscale photograph of
the abattoir depicted at left.  The Schuylkill river is in the
foreground.  The spires are clearly visible.  To left and right are
low storage buildings.  The abattoir has one very high lower story of
dark brick, surmounted by a lighter-colored cupola with tall windows
and an arched roof with a skylight.

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.

More details here.

[ 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:

A portion of a map, with buildings
marked in yellow and pink.  Several large yellow buildings, surrounded
and cut through with rail lines, are labeled CATTLE PENS.  Pink
buildings on the left and right are SLAUGHTER HOUSE and ABBATOIR.  In
between is a smaller pink building labeled HOTEL.  Just north of the
hotel are the HOG PENS.

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.

An isometric drawing of the site of
the office and hotel building, with “Stable and Hay Loft” to its
right, “Abbatoir” in the foreground, and “Pump House” in the
background.  These buildings, being brick, are colored pink; others
made of wood are colored yellow.  The abbatoir is a handsome and
ornate building, featuring four blue spires at each corner.

The survey includes a map of the site and a description of the facilities. Here's the detailed plan of the hotel:

Plan of the buildings,
including descriptions (Offices, 2 story, 43 feet by 78; hotel, 3
story, 43 feet by 100; both brick
with tin roof) and other details.

The full image is 105 MB:

An isometric drawing of the site of
the office and hotel building, with “Stable and Hay Loft” to its
right, “Abbatoir” in the foreground, and “Pump House” in the
background.  These buildings, being brick, are colored pink; others
made of wood are colored yellow.  The abbatoir is a handsome and
ornate building, featuring four blue spires at each corner.

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:

Five hundred head of cattle at a time would be held on the rooftop cow pens, right above the heads of the company’s executives,

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:

  1. If !!P_1!! and !!P_2!! are both products of some !!A!! and !!B!!, then !!P_1\cong P_2!!
  2. !!A×B \cong B×A!!
  3. !!(A×B)×C \cong A×(B×C)!!
  4. !!1×A\cong A!!
  5. !!0×A\cong 0!!
  6. !!A×A\cong A!! if and only if !!A!! is initial
  7. If !!f!! and !!g!! are both monic, then so is !!f×g!!
  8. If !!f×g!! is monic, so are !!f!! and !!g!!
  9. (etc…)

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:

Suppose !!A×B!! is a product with projection morphism !!π_1:A×B→A!!. Then !!π_1!! is epic.

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 2019

Cakes and Ale

I 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:

Any sufficiently advanced technology is indistinguishable from magic.

and Hanlon's Razor:

Never attribute to malice what can be explained by stupidity.

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!

Dated '80s graphic featuring neon-lit brushed-metal letters that
say “BDHAs LAZER”


[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 mjd.fix-bugs, you use a very thin client program to ask the Greenlight server to land your branch on master and publish it for you:

    greenlight submit mjd.fix-bugs

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 master and pushes the result back to master. If the push fails, it retries silently. Throughout, it communicates via Slack what is going on.

A user, Locksher, complained last week that it didn't do what he had expected. He had a Git pre-push hook he had written. Whenever he ran git push, his pre-push hook would look to see if he was pushing to master. If so, it would look at the messages of the commits he was trying to push. If any of them contained WIP or !fixup or !squash, it would abort the push.

With Greenlight, this check wasn't done, because Locksher never pushed to master himself. Instead he pushed to some topic branch, and then asked Greenlight to publish it to master, which it did, including his WIP commits. Oops!

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 greenlight client in a shell script that did the check he wanted. My second suggestion, less work for him but also less immediate, was that the Greenlight client could look in .git/hooks for a greenlight-pre-submit hook, and run that before communicating with the server, aborting the request if the hook failed. I think this would adequately solve the problem, especially if the calling convention for the new hook was identical to that of pre-push. Then you would just:

        ln -s pre-push .git/hooks/greenlight-pre-submit

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 greenlight client configuration should support this:

    [git]
    respect-git-hooks = true

I didn't have time then to answer in detail, so I just said:

I consider that very unlikely.

Here's what I said to him once I did have time to answer in detail:

  1. There are currently 23 documented Git hooks, and it's not immediately clear what it would mean to “respect” many of them. I'd have to go over the man page and decide, for each one, what the behavior should be, then possibly implement it, and then document it. Just to pick one example, should Greenlight “respect” your prepare-commit-message hook? If so, how?

  2. Even for the hooks where the correct behavior seemed clear to me, it might seem clearly something else to someone else. So the feature is severely under-specified and seems likely to cause confusion. I foresee a future of inquiries like “I set respect-git-hooks but Greenlight didn't run my pre-auto-gc hook.”

  3. It is an open-ended promise. The way the option is phrased, it guarantees to “respect” every hook. So it commits me to keep track of what new hooks are introduced in every future version of Git, and to decide what to do about each of them.

  4. Since greenlight runs on your local machine, the local version of Git may vary. What if the behavior of Git's pre-cake-slicing hook changes between Git 1.24 and Git 1.26? Now Greenlight will have to implement two behaviors, and look at your local Git version to decide what to do.

Oh, and 5, it is a YAGNI.

In contrast, the functionality provided by greenlight-pre-submit is something someone has actually asked for. It is small, sharply bounded in scope and its definition is completely under my control.

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 greenlight to “respect” his pre-push hook. Another user, say Zubi, could object, quite reasonably, that greenlight submit is not the same as git push, and that the correct way for it to “respect” her pre-push hook is to ignore it. “I want my pre-push hook run when I push a branch,” she might say, “not when I do greenlight submit.” Who could argue with that? (Other than Locksher, of course.)

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