[DAW, sorry for double sending, this is meant for the mailing list] Il 04/11/19 18:52, David A. Wheeler ha scritto: > There's no way to know for certain without trying, but I expect that > an automated tool could simplify a number of these expressions. The > result might be a smaller monster.
Looking quickly at the proof, it seems that a substantial amount of steps apply either mergeconj or selconj. The first is used to merge together two lists of conjuncts in the antecedent of a ND clause, and the second to select one of the conjuncts in the antecedent of a ND clause. Currently the Metamath proof synthesisation algorithm is forced to represent ND clauses invariably in this form: ( ( ph /\ ( ps /\ ( ch /\ T. ) ) ) -> th ) although in line of principle much more freedom could be use to represent the antecedent. When to lists are merged they won't be in this form, so mergeconj has to be repeatedly called to fix it. Also, ND manipulation lemmata, which are called by the proof generated by my code, expect conjuncts to be removed from the antecedent to appear in the first (outermost) place(s). Therefore repeated application of selconj is required to fix the shape of the antecedent before applying some ND steps. Probably many such calls could be saved by allowing more freedom in how the antecedent is represented. mergeconj could be dropped altogether and fewer selconj applications might be required if the antecedent is shallower. Unfortunately, this means complicating the code, because the conjunct selection process needs to accept any tree of conjuncts instead of a rigid right-associated list. Alternatively I could try to follow the idea of Mario's style for ND. In that case selecting conjuncts becomes free, because selecting hypotheses in Metamath is already free. The problem I see is that some ND steps, like ex (implication introduction) require a reified inference operator (i.e., an implication), that is not available with Mario's style. It is available with mine, though, which is the reason I am using it. Therefore it seems that I would still need to use both my and Mario's style in the proof, with a lot of additional complication, as I would have to track for each antecedent which type it is, and with much less advantage because I still would have implications. I don't know if there is an easy way out (other than using purely my style, with the disadvantage of size). Another frequently used lemma is csbcom2fi, which applies an explicit substitution to another one. Substitutions are frequently used in ND proofs, for example in quantifier introduction and elimination. Also, when I convert a FOF predicate or functor to Metamath, I represent it using one substitution for each of its arguments. For example, ph(x, y) is represented as [. x / w ]. [. y / z ]. ph where w and z are two fresh variables chosen for ph. Furthermore, I assume that w and z are the only free variables in ph. A similar thing happens for functors, where in addition I also assume that it can be proved that they are sets. This is necessary because there is mismatch between Metamath and standard FOFs: in FOFs arguments are explicit and order-based, while in Metamath they are implicit and name-based. As a result, it is not easy in Metamath to distinguish the two FOFs ph(x,y) and ph(y,x), and even less ph(x,y) and ph(A(y),y), unless one resorts to the trick I am using. If we stipulate that the arguments to ph are internally called w and z and the argument to A is internally called u, then we can write: [. y / w ]. [. x / z ]. ph [. [_ y / u ]_ A / w ]. [. y / z ]. ph and everything is fine, except for the readability of the notation and the fact that we have to commute a lot of explicit substitutions. I don't see an easy way out here. It might be possible to save a few variables on some proof where there is no need to perform excessively complicated substitutions, but it is something difficult to generalize and which complicates a lot the logic of the generator. Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/e5498452-2f99-ec7a-ed60-831b2b89eaeb%40gmail.com.
signature.asc
Description: OpenPGP digital signature
