cdgls
commented
8 years ago It occurs to me that if you use the current theorem function to create your definitions, then globular knows the desired link between them. [Is this how you are already making your definitions?] So possibly a single core change regarding the signature really does take care of both the definition and theorem issues. (But I maintain having them typed separately is useful for various reasons discussed (esp to allow the functionality of theorems without proofs) --- cf also you need the type distinction to ease the work of the auto paper generator.)
akissinger
jamievicary
semorrison
I know we've discussed this before, but yesterday Andre and I were attempting to make some headway on one of our globular projects, and it prompts us to raise it again ...
-- We think globular should have the functionality of Definitions and Theorems, not merely treat everything as just another cell of the appropriate dimension.
Let me first try to explain why this is so important, and then detail what it should be like (though exactly what might bear further discussion/revision). This is a substantial enough change to globular, that it would be worth discussing with other users whether they agree this would be worthwhile.
-- Why. One of the core purposes of globular, one might say the core purpose of globular, is to enable the machine certification of certain statements. We argue that it does not at present achieve this purpose, though it appears to for the simple kinds of examples that we all have so far used it for. The view that it does provide certification comes from looking at a globular worksheet, and seeing a statement cell and finding a cell of 1 higher dimension that "proves" the statement cell. But this involves a human belief or check that the "proof" cell actually does prove the statement cell, in terms of other cells which are "known" to be true. There is nothing in globular at present that checks this or confirms it. Indeed, you can just create a cell of the appropriate dimension that has the statement cell as source and any target you like, and it looks like a cell proving that statement. (Remark: it is possible that behind the scenes, globular keeps track of the connection between statements and proofs when they are created with the 'theorem' command, but if so, that isn't a connection that is visible to or usable by the end user at present.)
You might say, 'well, don't create random cells that looks like proofs but aren't! that's like writing "Proof. Ha ha, gotcha. QED" in a paper.' But aren't we not supposed to have to trust the author of a globular file? Isn't globular supposed to assure us that what was claimed was actually done? Of course in simple examples, you can kindof follow the globular signature and see that indeed everything has been done. But in larger or more complicated signatures, this can become difficult or impossible. It could even happen that the author genuinely thinks she has proven the statement, but actually somewhere in the middle used a cell that was not reducable to known cells. Globular could certify this has not happened, but at present it does not.
Here's another, closely related reason. When developing a globular proof, you sometimes know certain things are true, but haven't yet written down proofs of them. So you can't use the theorem function, you have to create the statements of the theorems by hand. But then you can't later use the theorem function to prove them, in fact you are stuck. And moreover, with a complicated signature, it can be unclear whether or not those 'theorem's even have proofs in the signature! (Recall there is no user visible difference between a cell that states a theorem but has no proof, and a cell that states a theorem but has a proof buried 20 scroll-pages of cells later in the signature. (Or even a cell that states a theorem but has a cell later that looks like a proof but isn't actually a proof, as mentioned earlier.)) You could say, 'well, don't do that, only use things you've actually proven!' In which case I ask you, 'have you ever written a research paper like that, linearly from start to finish? you often need to write a bunch of statements to figure out how they best fit together (or indeed which ones you will need in the end, or indeed which ones are true) before it makes sense to go back and write in the proofs.' In any case, this is the actual situation we are in, that we need to write a bunch of lemmas, and only once we've figured out that the lemmas fit together to prove the theorems, does it make any sense to go back and push through the proofs of the lemmas.
-- What. At present there is only a single type of thing that exists in the signature. We believe there should be at least five types of things: Postulates/Axioms, DefinedCells, Definitions, Theorems, Proofs. (Of course, one can alias to allow Theorems to be called also Lemmas or Propositions or Corollaries (with no functional change).) There are reasons we write papers with these headers that distinguish information types, and we think globular will benefit from them.
Postulates/Axioms. These are cells that are assumed to exist. "Assume there is a 0-cell Blue. Assume there is a 0-cell Red. Assume there is a 1-cell from Blue to Red." (I'll use http://globular.science/1512.007 as a reference point.) At present, every cell is treated as a postulate (from a user's viewpoint---we don't know if internally globular already makes some distinctions).
Definitions. There should be definition types. So for instance, in our reference worksheet, "New Cup" is a 2-cell, and then there is an invertible 3-cell "New Cup Definition". (Woe be you if you forgot to name this cell properly, or if the name is too long that you can't see the "Definition" part at the end.) But in reality, we don't ever want to think about or use that 3-cell except as a substitution mechanism, much less use any of the higher invertible structure. Instead of two things in the signature (one 2-cell and one 3-cell), there should be just a single item in the signature, listed at the level of 2-cells [But this item can have two parts, the thing being defined, and the definition]:
"DefinedItem: CupBeingDefined ____Definition: [CupBeingDefined] := [OldCup with bump]"
Note: for this item (Definitions), it may be that the internal structure of globular doesn't have to change at all --- maybe this is 'just a UI issue', in the sense that perhaps you still want to be able to click on the [CupBeingDefined] 2-cell and have it in its compressed form, and then click on the 'definition' to expand the compressed picture into the uncompressed picture, much as it does at present. So perhaps all the request amounts to is that there be a definite link between a cell that is being defined and the cell that is the definition. And the suggestion is that the link should be that they are either part of the same item of the signature, or adjacent in the signature (perhaps with the definition indented subordinately to the thing being defined, as displayed above).
Remark: To aim for minimal changes to the UI (since I can only imagine what a nightmare UI issues are to implement), perhaps the different cell types can be distinguished simply by adding a little "A" [Axiom], "C" [cell being defined], "D" [definition of a cell], "T" [theorem], "Pf" [proof] in the lower right corner of the cell box, or something.
Theorems & Proofs. There should be cells with type 'Theorem', and there are two subtypes 'Proven', 'Unproven'. So you can create a 3-cell of type Theorem, and by default it is unproven (perhaps there is a "Tu" in the corner, or if you prefer you can gloss unproven theorems as 'conjectures'). So in our example, you create a cell (type Theorem-unproven) from the snake to the identity and call it "Theorem 1". This is aspirational, and there are no 4-cells yet.
Then you can prove the theorem by creating a 3-cell with the features: 1. has source the source of the theorem, 2. has target the target of the theorem, 3. is built from other preexisting 3-cells in the signature (whatever the type of those cells). Once this 'Proof' 3-cell exists, the type of the theorem cell changes from 'Theorem-unproven' to 'Theorem-proven' "Tp". Of course, it is proven modulo earlier cells, which may themselves be unproven.
But crucially, globular should maintain a graph of the dependencies of the theorem cells, and then it's easy to ask globular whether the graph of dependencies of every theorem cell bottoms out into axiom cells, or if there are some leaves that have type 'Theorem-unproven'. This is the core verification that is missing in the situation discussed in the "Why" section above.
As with the 'Cell defined' and 'Definition' being linked and displayed adjacently, the Theorem and its Proof should be linked and displayed adjacently. Again, this could be done as
"Theorem 1 ____Proof 1"
ie the Proof is subordinately indented to the theorem [and it's easy to see if there is no proof there] [and they are part of the same item of the signature].
Again, you might say it is useful to have the proof still exist as an n+1 - cell (as it does now), and I can see that, and see that it would require less internal change to the structure of globular to have it be so. So maybe the [Theorem+Proof] item in the signature is a pair of an [n-cell + (n+1)-cell], just like the [Cell defined + Definition] pair. If so, maybe the globular core encoding doesn't have to change, other than having a way to keep track of the linkages between [Cell defined] and [Definition] and between [Theorem] and [Proof], and to change the UI to reflect these linkages, and to allow [Theorems] that don't yet have [Proofs], [and to give every cell one of the five types], [and to have a way to see or at least query the dependency tree among the theorems].
I can imagine objections to this proposal, but anyway, that's the thought to consider/discuss.
In conclusion: globular is super cool.