2020-05-26 12:57:41 (GMT)
Currently, in the "Sup with Lambdas" submission, ExtInf is defined so that an extra NegExt needs to be applied. Shouldn't we always apply it automatically and never generate the clause without it?
2020-05-26 12:58:33 (GMT)
(There's also an @PETAR in the text saying the same.)
2020-05-26 14:52:6 (GMT)
It is hard an inelegant to combine those two inferences with the current architecture of Zip
2020-05-26 14:52:41 (GMT)
The effect can be made if you choose the option --neg-ext-as-simpl=true which is going to turn neg-ext into simplification rule
2020-05-26 14:54:22 (GMT)
OK, I see. What's your experience with that option?
2020-05-26 15:3:33 (GMT)
Ext-Inst is waay worse than Ext-* rules
2020-05-26 15:3:54 (GMT)
It afaik never helps, whereas Ext-* rule is more useful
2020-05-26 15:9:18 (GMT)
There's a misunderstanding. I was talking about ExtInf, not ExtInst. ExtInf is the official name of Ext-*, because the latter was ambiguous. So what's your experience with --neg-ext-as-simpl in conjunction with ExtInf?
2020-05-26 15:13:4 (GMT)
(Maybe ExtCore would be a better name than ExtInf? Since we're talking about the three core rules.)
2020-05-26 15:33:4 (GMT)
Sorry I mistaken ExtInf and ExtInst
2020-05-26 15:34:24 (GMT)
I have not played much with neg-ext-as-simpl.
It is on by default in only one configuration
2020-05-26 16:53:30 (GMT)
Petar Vukmirovic said:
Ext-Inst is waay worse than Ext-* rules
Is that so? In the JAR submission, ExtInst is as good as ExtInf (or ExtCore? what do you prefer?) on TPTP problems, but indeed not so good in Sledgehammer problems.
Which terms do you use with it? All possible terms from the active set? What about polymorphism? The reason why I'm asking is that I think I can make ExtInst complete and get rid of (Ext) once and for all.
2020-05-26 17:19:37 (GMT)
We have a really small set of TPTP problems in that submission, on larger TPTP sets it is as bad as on SH :frown:
This rule does not work with Boolean extensionality, which makes it worse than Ext*
As for the second point, anything that will kick out Ext axiom in complete mode is for sure better than the axiom
2020-05-26 17:19:49 (GMT)
But I do not think it is going to help on SH/competition problems
2020-05-26 17:25:10 (GMT)
No, but the complete mode is going to be closer to the pragmatic mode. That's a step in the right direction, don't you think?
2020-05-26 17:33:6 (GMT)
I should have explained my goal more clearly from the start: I'm trying to kick out the extensionality axiom and replace it by ExtInst.
2020-05-26 18:46:26 (GMT)
I think it is the step in a perfect direction :slight_smile:
2020-05-26 18:47:47 (GMT)
we were just today discussing with @Sophie, @Alexander Bentkamp and @Visa how having ext axioms was the major drawback of the previous calculus
2020-05-27 8:12:46 (GMT)
The bad news is, it's more difficult than I thought and/or less precise. I had (I believe) everything worked out for the ground HO layer but when I looked at the lifting, then I realized that that's where the real difficulty is. Now I remember that @Alexander Bentkamp pointed that out last year. The trouble, roughly, is that any applied variable appearing at the wrong place in a clause (and there are many possible wrong places) forces the generation of axiom (Ext) in its full glory.
2020-05-27 8:35:22 (GMT)
But maybe restricted to a certain type? Or really the full polymorphic Ext axiom?
2020-05-27 9:0:54 (GMT)
Full glory. ;)
2020-06-02 6:57:26 (GMT)
The more I think about the names ExtSup etc., the less I like them. These rules don't perform any extensionality and don't depend on (Ext) for their soundness. I understand that they create opportunities for extensionality, but that's a weak connection; rule names should describe what the rules do, not what other rules might or might not do on their conclusion. We have enough rules with Ext in their names that actually perform extensional reasoning without having to muddle things further (and I'm planning to introduce some more).
I'm not sure what to call them, though. EagerSup etc. (since they apply earlier than Sup etc., even when the terms are not unifiable), or OptimisticSup etc. (not a serious proposal, but no idea is too silly when brainstorming), or KeenSup etc., or ...? What we have is that unification is performed by "constraints" encoded as literals. Then we could talk about the Eager or whatever rules collectively, not the (simply confusing) Ext-* rules nor the ExtInf or (right now in the draft) ExtCore (the "ext" version of the core calculus rules).
In terms of meaning, I like "optimistic"; it's reminescent of optimistic vs. pessimistic locking in databases. (Pessimistic: you check whether terms are unifiable before performing the rewrite; optimistic: you check afterwards.) But it's quite of a mouthful. OptSup suggests "optional", OptimSup suggests "optimal", ...
2020-06-02 8:16:32 (GMT)
How about AbsSup etc.? That would also be more in line with Ahmed and Giles's terminology.
2020-06-02 8:22:15 (GMT)
As a name surface/shallow superposition would hint that the terms are superposed only partially.
I agree that optimistic gives a better idea of the behavior than eager/keen which I'd connect to some scheduling things.
2020-06-02 8:26:34 (GMT)
We have "deep variables" already so we shouldn't use "shallow" except as the opposite. "Surface" goes in the right direction. We could have MockSup etc. It would be nice to have a really short prefix (ideally 3-4 letters).
2020-06-02 11:5:16 (GMT)
In our IJCAR submission, we have called the equivalent rules in Vampire *-wA where "wA" stands for "with abstraction".
2020-06-02 11:23:54 (GMT)
I like AbsSup the best