On Thursday, October 31, 2019 at 1:38:28 PM UTC-4, ookami wrote: > > Now that Christmas is approaching, I would love to come up with my personal > wish list, that I slowly gathered over the past years. Okay, I am not > going to > command others here to fulfil my needs. But maybe, one or the other point > has > been silently pondered by others as well. So lets see whether this > results in a > discussion, or even, finally, something more. >
I'll make a few comments mostly related to current software. Others can comment on some of your more visionary ideas. > 1. The user interface > > It is common practice nowadays to separate the UI from the so called > backend. > The backend is responsible for carrying out commands issued by the user. > The > UI should present the user with an overview of his/her options, and perhaps > allow focussing on particular fields of interest. > > Why do you want to have these separated? There are people fantastic at > creating > intuitive interfaces. Others are more into abstract thinking, and can > provide > fast and reliable libraries. Or incorporate third-party software like > search > engines. > > The current structure of set.mm has UI elements (in form of htmldef > entries), > theorem signatures (i.e hypotheses and statement), and proofs in one single > document, which I consider not optimal. > The $t comment where htmldefs are stored (about 250K in size or 0.7% of set.mm) is currently produced as a separate module 'set-typeset.mm' when you use 'write source set.mm /split', and like other modules it can be worked on independently from the rest of set.mm. (BTW 'help verify markup' has a link to the modularization tag spec for /split.) > > Here's an existing example, where a separation has been successfully > carried out: > chess! See http://www.playwitharena.de/ > <http://www.google.com/url?q=http%3A%2F%2Fwww.playwitharena.de%2F&sa=D&sntz=1&usg=AFQjCNGQQFjRUarK_xLxBWnT07Rbjp25Ow> > > for a screen shot of an UI. To really play > a game you still need an engine like https://stockfishchess.org/. Both UI > and > engine are exchangeable. > > If we want to go into this direction, we need to standardize the interface > between > frontend and backend. And before we can do that, we need to get an > overview of > what capabilities are requested by the users -- that are you! > > 2. Proof templates > > At least in the area where I have worked so far, I more than once > encountered a > situation, where I needed a specific instance out of a theorem family, that > wasn't provided. The usual action to get around this deficiency was by > looking out for a nearby solution and introduce otherwise unnecessary > administrative proof steps. A good example is the > deduction/immediate/closed form > of a theorem. Wouldn't it be nice to have these forms at hand without > much ado? > For most new theorems in set theory and beyond, the convention has become to use Mario's deduction form. The closed and inference forms can be obtained from these almost immediately inside of a proof, so usually there is no need to state them as separate theorems. For a heavily-used theorem, a separate form might be justified if there is sufficient proof size savings, but that could be done as a separate maintenance activity for theorems with high usage. > > Apart from this convenience aspect, I would really love to extend parts of > FOL to > arbitrary dimensions, as applies to substitution [ z / x ] [ w / y ]... , > for example. > The current Metamath language has no means of expressing a proof concept, > or template, > that contains instructions how to create a proof for a concrete theorem > instance. > I really miss such an abstraction layer. > > There are some pitfalls here to note: One should keep a compiled form of a > theorem > database, where all these abstract notions are collapsed into instances as > needed, > instead of interpreting them over and over again. C++ is an example of a > computer > language that follows this idea. The executable is stripped of any helper > constructs > the programer might have employed in his working process. > > Anyway, is there an idea of how to create a meta language/grammar that > fits into this > field? > > 3. Specialization > > The gource video from DAW shows in how many different fields of mathematics > set.mm has put its foot into. These are only the traditional fields, > others might > want to use ZFC in future to create abstract graph structures like trees, > maps. I am > pretty sure, there is much more than that conceivable. > > For me it is time to break set.mm up into dedicated subunits. > 'write source ... /split' produces modules as specialized as you care to make them. Each module can be read by itself and include only those previous modules that are needed. Creating a complete > HTML site of all theorems is already a matter of an hour or so on my > computer. > You can specify a statement range to create a portion of the site; e.g., 'show statement ax-1~df-ex /alt_html' will produce all of propositional calculus (and a couple of predicate calculus statements). Should't there be some support of specialization? Don't get me wrong > here. I think > this is difficult, as it needs some sort of linking process, with all > kinds of > conflicts lurking (link against classic or intuitionistic logic? Use > theorem A or > B out of different units, one using the axiom of choice, the other not?). > > I would love to hear from you how you see the future here. > > Kind regards > > Wolf > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6428f01f-2ab1-476d-a7a6-17be5e68fa69%40googlegroups.com.
