2020-07-02 16:12:1 (GMT)
I just want to say that the slides are super cool.
2020-07-02 16:19:23 (GMT)
So this is the Matryoshka philosophy, applied to HO unification, heh? I lost count of the number of times "graceful" was uttered :upside_down:
2020-07-02 16:20:47 (GMT)
Are solid terms those where substituting HO variables will not trigger any reduction?
2020-07-02 16:22:26 (GMT)
I thought that unification would be more of a factor in SH
2020-07-02 16:22:51 (GMT)
but maybe the gains you would have from that are in a previous paper...
2020-07-02 16:32:34 (GMT)
I suspect it's hard to have a clear picture of SH until we have native support for the Booleans.
2020-07-02 16:33:16 (GMT)
Simon Cruanes said:
Are solid terms those where substituting HO variables will not trigger any reduction?
Hm.. they will trigger basic reductions
2020-07-02 16:33:17 (GMT)
Actually, let me retract that. Petar has added it already on an ad hoc basis and reran the evaluation after that.
2020-07-02 16:33:59 (GMT)
Congrats on your talk, Petar! And on the other day's talk as well. It was very nice and understandable. A great advertisement for the paper.
2020-07-02 16:34:0 (GMT)
I think it is what Tobias Nipkow calls reductions
2020-07-02 16:34:13 (GMT)
Thanks a lot to everyone :slight_smile:
2020-07-02 16:35:18 (GMT)
Haniel Barbosa said:
I thought that unification would be more of a factor in SH
As soon as you support some forms of FO unification
2020-07-02 16:35:35 (GMT)
IT no longer matters
2020-07-02 16:36:11 (GMT)
THe difference would be much bigger if JP did not implement a FO oracle
2020-07-02 16:36:31 (GMT)
so the HOL part of the SH problems are a non-issue?
2020-07-02 16:37:23 (GMT)
I think they're an issue, but they were an issue and they remain an issue.
2020-07-02 16:37:28 (GMT)
Not quite sure. They can be such an issue that they are not solvable by any configuration
2020-07-02 16:37:29 (GMT)
This will require more investigation.
2020-07-02 16:37:47 (GMT)
Jasmin Blanchette said:
I think they're an issue, but they were an issue and they remain an issue.
Exactly what I wanted to say
2020-07-02 16:37:54 (GMT)
For example, there's an old joke that if your goal has a set comprehension over tuples, SH will always fail.
2020-07-02 16:37:58 (GMT)
I'm probably wrong, but the SH problems are also encoded and selected in a way that FO-ish provers can tackle them.
2020-07-02 16:38:18 (GMT)
One thing Jasmin told me before is that a bunch require induction
2020-07-02 16:38:21 (GMT)
So a new crop of HO problems from SH would be good for future research?
2020-07-02 16:38:25 (GMT)
The THF0 problems, no. There's only monomorphization.
2020-07-02 16:38:41 (GMT)
Well it just so happens that Zipperposition supports induction… :upside_down:
2020-07-02 16:38:42 (GMT)
Yes, next year there will be a "Slammer" division at CASC with TF0 problems.
2020-07-02 16:38:44 (GMT)
Yeah, there are some strange things in SH HO problems (such as inclusion of ), but not as nearly as in Mizar exports
2020-07-02 16:39:5 (GMT)
It'd "just" need the same kind of tune-up and improvements that were applied to everything else in Zipperposition.
2020-07-02 16:39:11 (GMT)
Induction could be useful but I think we really need to exploit the fact that it's a bidirectional rule.
2020-07-02 16:39:26 (GMT)
Jasmin Blanchette said:
Induction could be useful but I think we really need to exploit the fact that it's a bidirectional rule.
In what sense?
2020-07-02 16:39:31 (GMT)
Also in the output: A partial proof, with some missing cases, is better than no proof at all.
2020-07-02 16:40:6 (GMT)
If the original conjecture was provable, the unproven cases will be provable.
2020-07-02 16:40:18 (GMT)
And you can "sorry" them (or "Admit" or whatever).
2020-07-02 16:40:32 (GMT)
The user can then call SH "recursively" if they want.
2020-07-02 16:41:52 (GMT)
In the prover itself, I don't know enough about how it's done today in Zip, but exploiting bidirectionality might simply mean that once you commit to a proof by induction, you don't look back. I.e. you don't try in parallel to prove the problem by induction and directly. (No idea if that helps, though.)