book
book copied to clipboard
HoTT
How to insert new theorems in edition 1
The incremental improvements to the book are working very nicely, I think. But the fact that we decided not to change numbering is making it hard to iterate towards a second edition. In fact, it is going to be hard to ever begin working on a second edition because the incremental corrections work so well.
Of course, not changing the numbering was the correct decision to make. People refer to theorems by their numbers. However, let us think about relaxing the scheme so that we can in fact add new theorems. It is simple, really, once we recognize the fact that nothing prevents us from using a dense linear order.
For example, we could insert new theorems in such a way that they would receive numbers between those already in the book. I think it could be made to work. At some point we can "reset" the scheme and announce a 2nd edition, but I suspect it would be better to plan for a neverending stream of improvements.
Now that I think about this, it is not so clear how it cold be done. I was thinking of some sort of "bisection" method. Suppose we introduce new envrionments newthm, newdef and so on for insertion of new items. If three newthm are inserted between 4.2.10 and 4.2.11, they might be numbered 4.2.10.X. But how would we allocate the X's and respect the order in which they were inserted?
One option is to give explicit infromation on the ordering somewhere, but that sounds annoying.
One option is to allocate the X's manually (newthm and newdef take X as an argument), and then when you "reset", you remove the manual numbering. Another option is to take a label for the preceeding theorem, and a boolean that says whether to start a new counter or use the previous one. Then you write some LaTeX black magic code to compute the numbers correctly.
For what it's worth, I don't think that the 2nd edition should be just a collection of minor improvements. I'd rather not call anything the 2nd edition until we want to make some more major change, like adding substantial new material or changing the underlying type theory.
However, this is a good idea. But it does seem impossible in principle for LaTeX to tell from three un-annotated newthms in between 4.2.10 and 4.2.11 which of them was inserted first, and without that information there seems no way to allocate numbers to them automatically in a way that will be stable under inserting new ones.
Well, LaTeX could use \write18 to call git blame on the input .tex file and parse the output of that to figure out the ordering, but that seems rather insane. Another option if to have travis auto-annotate new theorems with dates (similar to what it does with errata), or to have the makefile pre-process the .tex file using git blame.
I agree there is no automagic. What is the least amount of manual work that is needed? Also, we need a scheme that protects us from ourselves. Here's a possiblity: the new environment newthm takes a fraction between 0 and 1 (I am not kidding). We check that the newthm's appearing between two old thm's are ordered strictly linearly. That is, the fractions appear in a strict increasing order. Thus, between 4.2.10 and 4.2.11 we would have 4.2.10½ and 4.2.10⅔ and so on. This would be kind of crazy but it would work.
I don't like coupling the solution with git. It should be a pure LaTeX solution.
The strict linear order thingy can be checked fairly easily. We remember the last fraction seen. Old environments set it to 0. New environments check that the last fraction seen is strictly greater than the given one.
I actually like the use of fractions: I would prefer 4.2.10½ over 4.2.10.5 because with the latter choice, some theorems are numbered x.x.x and others are numbered x.x.x.x, which seems potentially confusing. Using fractions makes it clear that all theorems come in the same sequence.
At first I thought it would be hard to program TeX to compare fractions, but then I realized it's easy as long as it can multiply and compare integers.
Actually, there is a sensible and quite general way to assign numbers to new theorems. The location of a new theorem to be added in a section defines a cut of the existing theorem numbers in that section, and therefore identifies a unique simplest number inhabiting that cut (in the sense of the surreals). For instance, if a new theorem is added in between 4.2.10 and 4.2.11, then the cut { 1,2,3,...,10 | 11,12,...,n } defines the number 10½, while if a new theorem is added at the end, then the cut { 1,2,3,...,n | } defines the number n+1. With this scheme we'd be okay even if sometime we have to add infinitely many theorems.
One slight problem with it is that if a new theorem is added to a section which previously contained no theorems, then for consistency it should be numbered 1, but the cut { | } defines the number 0. (Of course, this would not be a problem if we had consistently numbered theorems starting from 0 in every section to begin with.) We could assume an implicit "theorem 0" at the very beginning of every section to prevent this, but that would have the additional effect that a new theorem added to section 4.2 before theorem 4.2.1 would become 4.2.½ rather than 4.2.0. I'm not sure whether that's the right thing to do -- should theorem numbers always be positive?
Another question is what to do when multiple theorems are added at the same time. If we add two theorems in between 4.2.10 and 4.2.11 at the same time, the above scheme would require us to first number one of them 4.2.10½ and then the other one either 4.2.10¼ or 4.2.10¾, depending on which order we chose to number them in. But it would arguably be more natural to number them as 4.2.10⅓ and 4.2.10⅔.
When does 1/3 happen? Or do we keep getting dyadics? I like a canonical choice of numbers.
With the surreal scheme, we would never get past dyadics as long as every section contains only finitely many theorems. But we would have to decide what to do about the issues in my second two paragraphs, and the latter might lead to theorems being numbered with thirds. Any thoughts about whether theorem numbers should always be positive?
Another canonical scheme would be:
- if adding n theorems at the end, take the least n positive integers not yet in use.
- if adding n theorems at the beginning (to a section that already contains theorems), take the greatest n integers not yet in use.
- if adding n theorems in between two existing theorems numbered X and Y, divide (Y-X) into n equal parts and use the boundary points.
That way if we add two theorems in between 4.2.10 and 4.2.11, they would be 4.2.10⅓ and 4.2.10⅔, and then if we later add three theorems in between 4.2.10 and 4.2.10⅓ they would be 4.2.10 1/12, 4.2.10 1/6, and 4.2.10 1/4.
But we do not know ahead of time how many theorems will appear between 4.2.10 and 4.2.11. So we really do need to mark theorems so that we can tell in what order they were added.
Better than what?
As for "generations", well sort of, but not exactly. E.g. if we add one theorem in between 4.2.10 and 4.2.11, and then another one in between 4.2.10 and 4.2.10½, and then another one in between 4.2.10½ and 4.2.11, the resulting sequence of numbers would be indistinguishable from if we added three theorems at once in between 4.2.10 and 4.2.11.
I feel like we are talking past each other about something. I'm not proposing that TeX can automatically calculate these fractions, although I suppose it would be possible -- I was just proposing a way for us to decide canonically on what fractions to give to the newthm command.
Yes, we were talking past each other. I suppose people might find it cute to insert 4.2.10⅛ because it was "just a corollary of 4.2.10".
I suppose they might, but I think it's better to have a well-defined rule for what numbers are assigned to new theorems.
Does anyone else have an opinion?
Another thought: if we do this, we should probably add some comment to the introduction explaining the meaning of fractional theorem-numbers, for the benefit of readers with only a printed copy.
wait — I thought fractions were a joke. are you really serious about fractional theorem numbers?
On Jan 15, 2014, at 6:21 PM, Mike Shulman [email protected] wrote:
Another thought: if we do this, we should probably add some comment to the introduction explaining the meaning of fractional theorem-numbers, for the benefit of readers with only a printed copy.
— Reply to this email directly or view it on GitHub.
With the conventional scheme, we can't insert new theorems in between 4.6.10 and 4.6.11 without changing the latter to 4.6.12.
By the way, I think being able to add new numbers in between existing ones (however we do it) may be even more useful for equations than for theorems. I think it's already happened that it would have been useful to be able to give a number to a previously unnumbered equation.
the problem with 4.6.10.1 is that next time one doesn’t know whether to use 4.6.10.2 or 4.6.10.1.1 ?
On Jan 15, 2014, at 11:40 PM, Mike Shulman [email protected] wrote:
With the conventional scheme, we can't insert new theorems in between 4.6.10 and 4.6.11 without changing the latter to 4.6.12.
— Reply to this email directly or view it on GitHub.
Also, what will you do if you want to insert something between 4.6.10 and 4.6.10.1?
At that point it's just easier to understand 4.6.10½ and 4.6.10⅔. And also, this is way cool.
On Jan 16, 2014, at 10:05 AM, Andrej Bauer [email protected] wrote:
And also, this is way cool.
the real reason ...
There is some standard way which is used in libraries. I am away from the IAS at the moment so I can not check it out but it is probably the same or similar everywhere - they have the same problem to insert books without changing the call numbers of the existing ones.
V.
On Jan 16, 2014, at 9:48 AM, Andrej Bauer [email protected] wrote:
Also, what will you do if you want to insert something between 4.6.10 and 4.6.10.1?
— Reply to this email directly or view it on GitHub.
ah, good point — we are not the first people to face this problem, and librarians have probaby already solved it.
On Jan 16, 2014, at 9:41 PM, Vladimir Voevodsky [email protected] wrote:
There is some standard way which is used in libraries. I am away from the IAS at the moment so I can not check it out but it is probably the same or similar everywhere - they have the same problem to insert books without changing the call numbers of the existing ones.
V.
On Jan 16, 2014, at 9:48 AM, Andrej Bauer [email protected] wrote:
Also, what will you do if you want to insert something between 4.6.10 and 4.6.10.1?
— Reply to this email directly or view it on GitHub.
— Reply to this email directly or view it on GitHub.
That doesn't mean they've solved it in a good way, though. I, for one, would love to see fractional theorem numbers catch on throughout mathematical practice (in lieu of actual well-named identifiers, of course), and what better place to start than here? :)
