Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

November 16, 2014

Jaynes on Mathematical Courtesy

Posted by Tom Leinster

In the last years of his life, fierce Bayesian Edwin Jaynes was working on a large book published posthumously as Probability Theory: The Logic of Science (2003). Jaynes was a lively writer. In an appendix on “Mathematical formalities and style”, he really let rip, railing against modern mathematical style. Here’s a sample:

Nowadays, if you introduce a variable xx without repeating the incantation that it is in some set or ‘space’ XX, you are accused of dealing with an undefined problem. If you differentiate a function f(x)f(x) without first having stated that it is differentiable, you are accused of lack of rigor. If you note that your function f(x)f(x) has some special property natural to the application, you are accused of lack of generality. In other words, every statement you make will receive the discourteous interpretation.

Discuss.

This is taken from the final section of this appendix, on “Mathematical courtesy”. Here’s most of the rest of it:

Obviously, mathematical results cannot be communicated without some decent standards of precision in our statements. But a fanatical insistence on one particular form of precision and generality can be carried so far that it defeats its own purpose; 20th century mathematics often degenerates into an idle adversary game instead of a communication process.

The fanatic is not trying to understand your substantive message at all, but only trying to find fault with your style of presentation. He will strive to read nonsense into what you are saying, if he can possibly find any way of doing so. In self-defense, writers are obliged to concentrate their attention on every tiny, irrelevant, nit-picking detail of how things are said rather than on what is said. The length grows; the content shrinks.

Mathematical communication would be much more efficient and pleasant if we adopted a different attitude. For one who makes the courteous interpretation of what others write, the fact that xx is introduced as a variable already implies that there is some set XX of possible values. Why should it be necessary to repeat that incantation every time a variable is introduced, thus using up two symbols where one would do? (Indeed, the range of values is usually indicated more clearly at the point where it matters, by adding conditions such as (0<x<10 \lt x \lt 1) after an equation.)

For a courteous reader, the fact that a writer differentiates f(x)f(x) twice already implies that he considers it twice differentiable; why should he be required to say everything twice? If he proves proposition AA in enough generality to cover his application, why should he be obliged to use additional space for irrelevancies about the most general possible conditions under which AA would be true?

A scourge as annoying as the fanatic is his cousin, the compulsive mathematical nitpicker. We expect that an author will define his technical terms, and then use them in a way consistent with his definitions. But if any other author has ever used the term with a slightly different shade of meaning, the nitpicker will be right there accusing you of inconsistent terminology. The writer has been subjected to this many times; and colleagues report the same experience.

Nineteenth century mathematicians were not being nonrigorous by their style; they merely, as a matter of course, extended simple civilized courtesy to others, and expected to receive it in return. This will lead one to try to read sense into what others write, if it can possibly be done in view of the whole context; not to pervert our reading of every mathematical work into a witch-hunt for deviations from the Official Style.

Therefore […] we issue the following:

Emancipation Proclamation

Every variable xx that we introduce is understood to have some set XX of possible values. Every function f(x)f(x) that we introduce is understood to be sufficiently well-behaved so that what we do with it makes sense. We undertake to make every proof general enough to cover the application we make of it. It is an assigned homework problem for the reader who is interested in the question to find the most general conditions under which the result would hold.

We could convert many 19th century mathematical works to 20th century standards by making a rubber stamp containing this Proclamation, with perhaps another sentence using the terms ‘sigma-algebra, Borel field, Radon-Nikodym derivative’, and stamping it on the first page.

Modern writers could shorten their works substantially, with improved readability and no decrease in content, by including such a Proclamation in the copyright message, and writing thereafter in the 19th century style. Perhaps some publishers, seeing these words, may demand that they do this for economic reasons; it would be a service to science.

Posted at November 16, 2014 2:01 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2779



40 Comments & 0 Trackbacks

Re: Jaynes on Mathematical Courtesy

Maybe I should have said something about the theme of Jaynes’s book. Here’s a passage from page xxii, quoted in William Faris’s review in the Notices of the AMS:

Our theme is simply: probability theory as extended logic. The ‘new’ perception amounts to the recognition that the mathematical rules of probability theory are not merely rules for calculating frequencies of ‘random variables’; they are also the unique consistent rules for conducting inference (i.e. plausible reasoning) of any kind, and we shall apply them in full generality to that end.

Posted by: Tom Leinster on November 16, 2014 2:27 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Courteous mathematics seems to correspond, roughly speaking, to what I would call “post-rigorous mathematics”: http://terrytao.wordpress.com/career-advice/there%E2%80%99s-more-to-mathematics-than-rigour-and-proofs/ . It is an appropriate level of mathematical discourse for those who have already mastered all the subtleties of rigorous mathematical reasoning. But it is somewhat dangerous to encourage this style of discourse before the discipline of mathematically rigorous argument has been instilled into the participants of the discussion. (Imagine for instance trying to deal “courteously” with some lightly trained mathematician who has managed to prove Fermat’s last theorem by differentiating the equation x n+y n=z nx^n+y^n=z^n in nn (or in xx, yy, or zz) and deriving a contradiction thereof - which is actually a surprisingly common tack towards FLT by amateur enthusiasts.)

Posted by: Terence Tao on November 16, 2014 3:41 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I like your characterization of “post-rigorous” mathematics. I get the impression, though, that you were thinking more of the doing of mathematics than the writing of mathematics, whereas Jaynes is explicitly talking about the latter.

I think there’s a significant difference. Jaynes doesn’t address the fact that mathematics is vastly more fragmented than it was in the 19th century, and different groups of mathematicians have different background assumptions and culture. As someone who often spends time reading books and papers on subjects that I’m not expert in, I really appreciate it when authors take a few lines to be explicit about their assumptions for those outside their immediate cultural group. So if, for instance, someone writes about the derivative of ff without having declared ff to be differentiable, I don’t have to guess whether what they have in mind is a distributional derivative or simply a tacit assumption that ff is now a differentiable function. As Todd says, constantly having to guess is wearying, and it wastes effort unnecessarily.

That said, there’s something in Jaynes’s rant I appreciate. There’s a message of “this way of doing things actually works, so why don’t we adopt it as our official practice?” It’s somewhat similar to categorical set theory (“this is close to how mathematicians use sets in practice, so let’s adopt it officially”) or synthetic geometry (“reasoning with infinitesimals of different orders works consistently, so let’s be up-front about it”).

Posted by: Tom Leinster on November 16, 2014 6:50 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Well, it’s a rant. It’s a little hard to tell how justified it is in his case, since he doesn’t really give examples that can be judged independently (it’s all more or less, “trust me, this really happened to me”). Which is not to say this type of thing has never happened.

I am a little tempted to turn the tables and inquire whether it’s courteous of the author not to be explicit about his assumptions. It can be very wearying to the reader to have to give the benefit of the doubt constantly as the confusions and doubts pile up.

Perhaps more to the point, I guess he might be railing against the dominance of the axiomatic spirit in the presentation of modern mathematics, which is indeed very much a 20th century thing and shows little sign of going away, as far as I can tell.

Posted by: Todd Trimble on November 16, 2014 5:24 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I agree with most of what you say, Todd, but I’m perhaps willing to give him a bit more benefit of the doubt when it comes to his claims of persecution (e.g. compare this MathOverflow question and the response to it). Which isn’t to say that the persecution/criticism is unjustified.

I wonder what you make of an earlier part of the same appendix, What is a legitimate mathematical function?. I’ve only skimmed it, but it’s less of a rant, and the topic is one on which a category theorist might have a point of view!

Posted by: Tom Leinster on November 16, 2014 7:32 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Without any pretensions to being an expert here, I guess I have a few shoot-from-the-hip reactions.

Yes, the tone is less rant-like, but I still find the exposition annoyingly tendentious. There is a suggestion that mathematicians (he mentions Titchmarsh) were blinkered by being so wedded to integral representations of the Fourier transform and convergence issues, followed by “Then a more sophisticated view emerged in theoretical physics…” I mean, it’s not as if mathematicians never entertained the idea of a formal algebra that abstracts the properties described in B.10-12. For example, there is a whole chapter in the book on Vertex Operator Algebras by Frankel-Lepowsky-Meurman (1988) that goes into formal algebra of manipulating the Dirac distribution δ(z)=∑ n∈ℤz n\delta(z) = \sum_{n \in \mathbb{Z}} z^n.

Even in more classical analysis settings, one recognizes that the Fourier transform as defined by an integral is defined only on a dense subspace of the “functions” one is interested in; for example it can be seen as the restriction of a more fundamental duality L 2(G)→L 2(G^)L^2(G) \to L^2(\hat{G}), or is sensible on still more general spaces of distributions, etc. Such developments cannot just be ascribed to the vision of courageous physicists.

I can’t quite figure out what he means when he says (section B.5.1) “Laurent Schwartz (1950) tried to make the notion of a delta-function rigorous, but from our point of view awkwardly, because he persisted in defining the term ‘function’ in a way inappropriate to analysis.” What awkwardness does he have in mind? (There are references to some work of Temple and Lighthill which are said to improve on the awkwardness, but I don’t know what the references are. Nothing he says about sequences of functions in sections B.5.1-3 strikes me, at first blush, as terribly surprising or revolutionary; perhaps I don’t fully appreciate what he driving at.)

Maybe I should stop. Some of this stuff sounds like an argument from a long time ago [long before publication in 2003] which by now sounds pretty antique. My rough impression is that he is underestimating the versatility of set-based mathematics. (Hm, what’s this B.6 about?)

Posted by: Todd Trimble on November 17, 2014 1:03 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Thanks. I didn’t know what he meant about Schwartz’s conception of function, either — that puzzled me.

If you strip out all the attitude (a major job, I concede), I think there’s something interesting here. One reading is that he wants an axiomatic world where he can do analysis of the kind he likes, without being bothered by any counterexamples of the kind he doesn’t like. Perhaps this amounts to formal algebra of the type you mention.

I guess Jaynes wouldn’t have enjoyed the idea of confining himself by formal axioms, but then again, the passage from the introduction to the book that I quoted earlier suggests that this might not be such a repulsive idea for mathematicians like him after all.

(Section B.6 is, I think, frankly shameful. He produces the most simplistic argument for why infinite sets don’t make sense.)

Posted by: Tom Leinster on November 17, 2014 11:35 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Possibly this work of Richard Blute and Prakash Panangaden would be of interest?

Again somewhat shooting from the hip, a decategorified version of such a formal algebra might be based on Hopf algebra modules (e.g. the way a Laurent polynomial algebra acts on its linear dual of ‘distributions’). It looks like maybe Blute and Panangaden touch on such things, but I haven’t had a look yet.

Posted by: Todd Trimble on November 17, 2014 12:53 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Thanks for the link. That paper does look interesting. From page 4:

Another goal of this paper is to related the notions arising in this paper and the vertex groups of Borcherds [9, 26]. Both can be viewed as axiomatizing the notion of singular map.

Here [26] is a reference to work of my PhD brother Craig Snydal, who carried out a categorical investigation of what happens when you compose maps with singularities of specified severities. (This was based on some then-recent work of Borcherds.)

There’s a bit in Miles Reid’s text Undergraduate Algebraic Geometry (which is also abundant in snark) where he points out that the composite of rational maps needn’t be rational, since e.g. if you do a constant map followed by a map with a singularity at that constant value, the result is nowhere defined. He then says something like “anyone upset by that is urged to drop this course and take a reading course in category theory instead”. That always struck me as exactly wrong. It’s a platitude that structures and their maps form a category, and no one, category theorists included, is going to get excited about that. Situations where they don’t form a category are much more likely to pique a category theorist’s interest.

Posted by: Tom Leinster on November 17, 2014 1:43 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I was just thinking about this the other day; Tom kindly directed me to the relevant page in Undergraduate Algebraic Geometry, where on page 14 of the pdf one reads

Rational functions (that is, ‘functions’ of the form f=g/hf = g/h where g,hg, h are polynomial functions) are not defined at points where the denominator vanishes. Although reprehensible, it is a firmly entrenched tradition among algebraic geometers to use ‘rational function’ and ‘rational map’ to mean ‘only partially defined function (or map)’. So a rational map f:V 1⤏V 2f: V_1 \dashrightarrow V_2 is not a map at all; the broken arrow here is also becoming traditional. Students who disapprove are recommended to give up at once and take a reading course in Category Theory instead.

Students who take up that recommendation might be surprised to learn (as Reid might be too) that Category Theorists do study categories that behave as categories of partial maps. One might surmise that Reid has an outdated notion of what category theorists actually do, or perhaps doesn’t realize just how flexibly we contemplate what the word ‘map’ can mean. (Otherwise I don’t understand the point of his snark. I am reminded here of Colin McLarty’s essay on Mac Lane as philosopher; section 2 opens with, “Weil misunderstood Mac Lane and under-estimated the resources of set theoretic mathematics. Weil supposed that if structures are sets then morphisms must be functions.” But category theory is much more flexible than that.)

Getting back to Reid’s observation (which is perfectly correct of course), one could also observe that rational functions are almost the same thing as regular (total) maps ℙ 1(k)→ℙ 1(k)\mathbb{P}^1(k) \to \mathbb{P}^1(k), the sole exception being that the constant map valued at “infinity” is not represented by a rational function. Maybe putting it that way would help relieve the discomfort of those who want morphisms always to mean total maps, without going to all the trouble of taking a reading course in Category Theory.

Posted by: Todd Trimble on January 6, 2015 4:16 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

He then says something like “anyone upset by that is urged to drop this course and take a reading course in category theory instead”. That always struck me as exactly wrong. It’s a platitude that structures and their maps form a category, and no one, category theorists included, is going to get excited about that. Situations where they don’t form a category are much more likely to pique a category theorist’s interest.

Right, there’s a suggestion that if you are so craven as to run away in horror from something like that, then maybe the ‘safe’ world of category theory would be right for you. But just a little tweak of the sentence would suggest exactly the attitude you advocate: “anyone intrigued by that might consider talking with a category theorist, to get her take on such situations”.

I remember being intrigued by Snydal’s thesis when I was there in England in 1999, and having the feeling that this was a good path for me to find out what VOA’s were really about. (Bearing in mind that I was a student at Rutgers where James Lepowsky is a professor; he and I talked quite a lot while I was there, but I still had trouble grokking VOA’s.)

Posted by: Todd Trimble on November 17, 2014 2:55 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

This thread is a million years old but I was reading it on my lunch hour. I thought you might be interested in this example.

http://math.stackexchange.com/questions/1422056/is-there-an-algorithm-for-computing-pushouts-in-sf-finset

i asked on stack exchange mathematics, “is there an algorithm for computing pushouts in FinSet. You can see the comments.

I was asked ‘what do you mean by finite set?’ and ‘what do you mean by algorithm’. interesting.

I tried coding this in R and it took me a long time. Maybe because I don’t know what I’m doing. But it didn’t seem trivial to me.

As an aside, I was trying to understand pushouts better, but purely for recreation. I was trying to understand, how big is the average pushout in FinSet? Or if you have a finite set X and two onto maps from X to Y and Z, then the pushout P, on average how big is P? Now there is an example of some imprecise language, but I bet you can understand what I was talking about. Anyway my compute told me the answer might be 1/e. I wonder if that is true. I doubt I will ever find out.

Cheers,

Rob

Posted by: Rob MacDonald on January 12, 2016 8:48 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

As someone who could generously be described as pre-lightly trained, I would be curious about how this squares with Voevodsky’s program to truly formalize proofs in terms of automated proof assistants. It would be hard to argue that Coq was being discourteous. Also, it is obvious from my perspective that intuition can lead one astray – or seemingly obvious things aren’t. I can believe that Terence Tao and you (and others) can move to the post rigour stage comfortably, but, still, even post rigorous mathematicians can make formal errors, why not put it into a checked formal form? If a blanket statement can ‘fix’ the problem, you have a syntax problem, from a programming perspective.

Posted by: avererageProgrammer on November 16, 2014 7:14 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Ah, but coq has type inference and implicit arguments — partial tricks to interpret outwardly ambiguous expressions — and the “admit” “tactic” (so you can distill your conjecture down to “the right” underlying property you had never thought of, and tell yourself afterwards that you were assuming it all along (whether that’s reasonable or not)).

Posted by: Jesse C. McKeown on November 17, 2014 2:05 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Thanks for the reply. Type inference and implicit arguments seem to be exactly what is being discussed, only in this case they have to resolve properly.

What am I missing?

What is the general feeling from the mathematics community regarding HoTT and proof assistants?

Posted by: averageProgrammer on November 17, 2014 6:51 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I’m not sure any one person is able to report on “the general feeling of the mathematics community”. Obviously there’s a lot of interest in homotopy type theory among people who read this website, since it’s so deeply connected to the ideas that make nn-categories a good thing.

As for proof assistants, I’ll only say my own personal feeling. I think they’re a great idea in principle, and will someday be a great idea in practice, as rigorous mathematical results get linked up into an enormous database that we can all tap into and use. I’m glad people are working on proof assistants. But personally, right now, I’m completely uninterested in using them in my own work. I don’t have time, and they wouldn’t save time. I try to work on things where the proofs are easy and the hard part was having the idea in the first place.

The niche for mathematicians who don’t want to use proof assistants is enormous now, but I expect it will gradually shrink, and eventually become untenable.

Posted by: John Baez on November 17, 2014 10:42 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I think that may be the first time I’ve heard “mathematicians who don’t want to use proof assistants” described as a “niche”. (-:

Posted by: Mike Shulman on November 18, 2014 11:55 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Niche in the sense of ecology. Once trilobites ruled the seas.

Posted by: John Baez on November 18, 2014 8:58 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Your comment reminds me of a quote often misattributed to Yogi Berra:

In theory there is no difference between theory and practice; in practice there is.

Posted by: Eugene on November 19, 2014 3:45 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Maybe I don’t know what you have in mind, but I don’t think Coq will let you write the sort of thing Jaynes wants to write. Typeclass inference for implicit arguments means that you don’t have to pass around witnesses to differentiablitiy, i.e. you can write derivative f rather than derivative f H where H is a proof that IsDifferentiable f; but no mathematician would ever consider doing the latter informally anyway. Typeclasses don’t absolve you of the need to put differentiability explicitly in the hypotheses of your theorems.

In general, I think I’m with Todd: Jaynes seems to be advocating giving more weight to the convenience of the author rather than the reader, when in general I think we ought to do the reverse. Reading mathematics is hard enough already.

Posted by: Mike Shulman on November 18, 2014 12:03 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I agree with the view that in general the writer should be made to do work rather than each individual reader. In practical terms, I think it would be acceptable to not specify ff is differentiable if a theorem is something like “For ff where |f′(x)|≤C|f'(x)| \le C when xx ….” but not really acceptable if the usage of f′f' occurs deep within the proof of a theorem and is otherwise not mentioned. This is partly because of the the general principle that a writer shouldn’t expect all their readers to read everything rather than having some who are just skimming to see if this is something they want to read in greater depth, etc.

However, another reason that I haven’t heard mentioned yet is that if the context is near enough that the use can be easily seen, it’s often more precise than you’d get by just “habituating people to mechanically say” things like “where we assume ff is differentiable”. Consider for example Rolle’s theorem. The entry to that article (which admittedly says it’s “roughly” the meaning) talks about a differentiable function, while it’s only in the precise description that you see that ff only needs to be differentiable within the interior of the line segment under consideration, excluding the end-points. (As someone who uses |x||x| quite a bit the difference between a differentiable function and a function differentiable over some interval is occasionally quite important to me.)

Posted by: davetweed on November 19, 2014 11:50 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Someday maybe people can write mathematics in a relaxed style like Jaynes wants, while a ‘mathematics assistant’ (some generalization of a proof assistant) makes plausible assumptions that justify what is being done, and keeps track of these. For example, if you write f″f'', the assistant will guess that ff is a twice differentiable function from the real numbers to the real numbers. Sometimes the assistant will get stuck, unable to find assumptions that justify what you’re saying. Then it will complain, and you can either help it along or admit you were mixed up—or perhaps say “shut up, I’m just fiddling around, I’m not ready to justify everything yet”.

And, continuing this fantasy further, the reader of such a text will be able to click on anything you’ve written, and find the implicit assumptions—or perhaps just the implicit assumptions ‘down to a certain depth’.

Posted by: John Baez on November 17, 2014 10:28 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I like this fantasy.

Many Café readers are much more informed about this kind of thing than me, but I have the impression that what you’re describing isn’t too far from current reality. Aren’t there programming languages where you can say things like “let xx be a variable of type ‘natural number’”, then later say “take the square root of xx”, and the compiler will understand that you now mean to move into the realm of the reals? (Or the algebraic numbers? Hmm, how does it know?) Is this what’s called lazy typing? (Am too lazy to type it into a search engine.)

Posted by: Tom Leinster on November 17, 2014 11:18 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

In a typed language, the type of the sqrt function will be nat -> R, or perhaps polymorphically

forall X:Number, X -> R,

where the Number class could be N, Z, Q, R. So, not much work is needed in the example you mention. In general, I guess you are thinking of Type inference.

Wolfram|alpha is perhaps the most advanced in guessing what you mean.

Posted by: Bas Spitters on November 18, 2014 8:01 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

It could also be just R -> R, as long as you have a coercion N -> R.

Posted by: Mike Shulman on November 18, 2014 11:53 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Thanks for the info. I was hoping someone like you two would show up with some expertise :-)

It could also be just R →\to R, as long as you have a coercion N →\to R.

So is “coercion” the jargon for an inclusion, or forgetful function/functor? That’s interesting.

Posted by: Tom Leinster on November 18, 2014 12:13 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

A coercion typically means when one type is implicitly converted to another. Such conversions are not necessarily well-behaved inclusions in some programming languages. For example, it is common to be able to convert a 64-bit “integer” into a 64 bit floating point value, which results in a loss of precision for large numbers. In C and some derived languages it’s also possible to coerce between a 64 bit “signed integer” and a 64 bit “unsigned integer”. This is both convenient and a common source of weird bugs. There is disagreement between people who think programming should be convenient and people who think programs should be correct as to whether this kind of programming language design choice is a good thing.

Posted by: Ciaran McCreesh on November 18, 2014 2:40 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Usually, a coercion is either an embedding or a forgetting. In general, though, a coercion can be any arbitrary function.

As a category theorist, you will be unsurprised to hear that the theorem we want to prove about them is actually a property about a whole system of coercions, and not about any particular coercion. That general principle is that coercions should be coherent, meaning that even if there multiple ways to add coercions to make a piece of mathematical text meaningful, all of them should be equivalent.

We currently only know how to implement this condition for relatively simple type theories; the coercion system in (say) Coq is incoherent, a fact which is occasionally the source of truly baffling difficulties.

In fact, one of the very earliest applications of category theory to the theory of programming language is John Reynolds’ 1980 paper Using Category Theory to Design Implicit Conversions and Generic Operators. (He told me once that this was the favorite of all the papers he had written, since the mathematics in it was entirely trivial.)

Posted by: Neel Krishnaswami on November 18, 2014 2:52 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

“John Reynolds’ 1980 paper Using Category Theory to Design Implicit Conversions and Generic Operators” can be found at http://repository.cmu.edu/cgi/viewcontent.cgi?article=2276&context=compsci. A quick glance suggests that it might be arguing that types should be defined by their semantics rather than their implementation. An idea whose time has surely finally come.

Posted by: Robert Smart on November 18, 2014 7:35 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Neel wrote:

the coercion system in (say) Coq is incoherent

Ouch–what a cock-up! I thought Coq was designed by sophisticated sorts who would instantly realize that your coercions need to form a commutative diagram, to avoid dangerous ambiguities.

Posted by: John Baez on November 18, 2014 8:56 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Maybe I don’t know exactly what Neel is talking about, but I thought Coq would at least warn you when you define a noncommutative system of coercions. It’s willing to give you enough rope to hang yourself, but it lets you know what it thinks as you’re stringing up the noose.

(Although actually, I think Coq doesn’t even try to check that your coercions commute; it just warns you whenever your directed graph of coercions contains parallel paths. So if you’re used to defining commutative diagrams of coercions and ignoring the warnings, I guess you might get a boy-who-cried-wolf effect when you mess up and make a noncommutative one.)

Posted by: Mike Shulman on November 18, 2014 10:13 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I would say that Jaynes’ attitude is typical among physicists, and maybe some other people who want to apply fairly advanced mathematics without wanting to fight their way through the technical details. Jaynes writes a bit like Feynman (in his work, not so much this rant). He’s full of good ideas but they’re not expressed in the form of theorems. Such people can do great things for mathematics, but they’re not mathematicians. Mathematicians shouldn’t force these people to act like mathematicians—but these people shouldn’t try to force mathematicians to act like them, either.

Posted by: John Baez on November 17, 2014 5:40 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Such people can do great things for mathematics, but they’re not mathematicians

that’s because they’re mathemagicians, at least according to Pierre Cartier here.

…there is another way of doing mathematics, equally successful, and the two methods should supplement each other and not fight.

Posted by: David Corfield on November 29, 2014 2:53 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Rip Grothendieck

Posted by: Michael Davis on November 18, 2014 4:58 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I can somewhat relate to the points Jaynes make. Though not if you read them (as seems to be the preferred reading on this comment thread) as advocating for the convenience of the writer rather than that of the reader.

That is: I tend to believe mathematics should be written in a style which facilitates understanding (on the reader side). And an excess of precision can play counter to that principle. There’s a catch of course: the optial amount of precision depends widely on the audience.

As it happens there is a trend which was very present in the 90s, but has all but disappeared after the turn of the century, which saw computing science paper riddled with unnecessary precisions. My favourite example is the following statement (which really used to be common):

a binary tree is a set of words on the alphabet {0,1} which is closed by prefix.

I really love that because this definition is perfectly precise, completely useless (as anyone capable of reading the paper knows what a tree is), and absolutely uninformative (if you don’t know what a tree is, you’re certainly not going to learn it from this statement).

Another beloved example is prefixing all definition of term grammars by:

We assume given a countably infinite set V of variables with decidable equality.

Posted by: Arnaud Spiwack on November 20, 2014 8:34 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

a binary tree is a set of words on the alphabet {0,1}\{0,1\} which is closed by prefix.

This is a good example. I take your point that it conveys no visual intuition about what a tree is. But I don’t agree that it’s useless or uninformative. As you say, different audiences require different levels and types of precision. And “tree” is one of those terms that does actually have multiple inequivalent definitions (like “graph”, but not as bad). Even “binary tree” does. Is the tree supposed to have a distinguished root? Is the empty tree allowed?

The sentence quoted above provides answers to such questions. Arguably, it would be better to spend the space writing “trees have roots, and the empty tree is allowed”, but then you’d have to be sure you’d cleared up all possible ambiguities, and it’s all too easy to overlook points that seem natural and obvious to you but don’t to others. Maybe everyone in your own particular subdiscipline always takes to be trees to be rooted (say), and if you’re happy for your paper to be easily be readable by only those within your subdiscipline, it’s OK not to be explicit about that. But it’s in the interests of anyone who wants a wider readership to assume as little shared culture as possible.

Posted by: Tom Leinster on November 20, 2014 11:05 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

Tom wrote:

But it’s in the interests of anyone who wants a wider readership to assume as little shared culture as possible.

I agree with that, but I don’t think this particular definition of binary tree solves that problem. Not sharing the necessary culture, I don’t know what ‘closed by prefix’ means, so this particular definition of binary tree means nothing to me. I can easily imagine it’s some standard trick for encoding a binary tree, but it doesn’t help me know if the tree has a distinguished root, whether it can be empty, etc.

This might be okay: I’m not claiming that anything I can’t instantly understand is no good. If I cared, I could look up this phrase! But increased precision is always a double-edged sword: it makes things clearer to some, less accessible to others.

Posted by: John Baez on November 30, 2014 5:32 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I agree that it’s not great.

I suppose I can guess what “closed by prefix” means: that if a 1…a na_1 \ldots a_n is in the set of words and 1≤k≤n1 \leq k \leq n then a 1…a ka_1 \ldots a_k is also in the set. And I suppose it’s true that some fairly large collection of theoretical computer scientists would understand the meaning, larger than the collection who would be sure they knew exactly what an author meant by “binary tree”.

(Like you, I assume there’s some standard way of relating this definition to the graphical notion of tree. I haven’t bothered to think it through.)

On the other hand, if the author ever wants to do anything like referring to a leaf or edge or node of a tree, then they’ll need to say what “leaf” etc. means in terms of the precise definition, in order for that definition to be of any use.

Posted by: Tom Leinster on December 1, 2014 1:09 AM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

The word-definition translates into graphs like this: Let T⊆{0,1} *T\subseteq\{0,1\}^* be closed under prefix. This corresponds to the graph G=(T,E)G = (T,E) where EE includes an edge between any two words a 1…a na_1\dots a_n and a 1…a na n+1a_1\dots a_n a_{n+1}. If TT is non-empty, then the empty word ϵ\epsilon is the root. A leaf t∈Tt\in T is a word that is not a proper prefix of any other word t′∈Tt'\in T.

So you have the empty word ϵ\epsilon as the root, it can have children 00 and 11 who in turn can have children 0000, 0101 and 1010, 1111 respectively. Thus, every node of the tree is labelled by the path one takes from the root to it.

Posted by: Dominik Peters on December 2, 2014 5:18 PM | Permalink | Reply to this

Re: Jaynes on Mathematical Courtesy

I suppose I can guess what “closed by prefix” means: that if a 1…a na_1\ldots a_n is in the set of words and 1≤k≤n1\le k\le n then a 1…a ka_1\ldots a_k is also in the set.

I think that the definition is meant to require closure under even empty prefices (k=0k = 0). Probably my pointing this out is an example of mathematical discourtesy. :-)

(For whatever little it’s worth, I like the elegance and novelty of the definition.)

Posted by: L Spice on January 15, 2016 9:57 PM | Permalink | Reply to this

Post a New Comment