2020-03-23 15:51:21 (GMT)
Does anyone (@Ahmed B @Alexander Bentkamp @Jasmin Blanchette ) have the latest version of Combinator ordering and calculus papers
2020-03-23 15:51:42 (GMT)
I am getting ready to continue working on this topic and would like to get back in the game :)
2020-03-23 16:8:23 (GMT)
The versions submitted at IJCAR link to reports. These keep on evolving AFAIK.
2020-03-23 16:10:52 (GMT)
2020-03-23 16:11:26 (GMT)
2020-03-23 17:9:34 (GMT)
Thanks @Jasmin Blanchette for linking to the papers. Those are indeed the latest versions of the reports.
2020-03-23 17:15:42 (GMT)
Petar Vukmirovic said:
Does anyone (Ahmed B Alexander Bentkamp Jasmin Blanchette ) have the latest version of Combinator ordering and calculus papers
You should have access to the repository.
2020-03-23 17:54:24 (GMT)
I have reinstalled the system recently and lost it :(
2020-03-23 17:58:9 (GMT)
Ahmed, I have some questions about SubVarSup
2020-03-23 18:12:29 (GMT)
In its definition it is said that it uses the condition 3 of Sup inferences
2020-03-23 18:12:42 (GMT)
However, then it uses a different sigma
2020-03-23 18:13:15 (GMT)
Can you explain me which substitution should be used? And with what is t unified? There is no u in the definiton of SubVarSup
2020-03-23 20:5:49 (GMT)
Sorry, the paper should say "conditions 4-8" not "conditons 3-8". The unifier is the one stated in the rule. It unifies z t with y. Very similar to the FluidSup rule. Let me know if that makes sense.
2020-03-27 19:52:1 (GMT)
Here is the outline of the Combinators vs Lambdas paper
2020-03-27 19:52:2 (GMT)
2020-03-27 19:53:26 (GMT)
@Ahmed B , you can edit if you have any more ideas what we can add and which other experiments we can perform
2020-03-27 19:53:51 (GMT)
Also, we should agree on whether we will use only Zipperposition for evaluation of calculi or Vampire as well
2020-03-27 19:55:3 (GMT)
Petar Vukmirovic said:
Also, we should agree on whether we will use only Zipperposition for evaluation of calculi or Vampire as well
To use Vampire we'd have to implement Lambda sup in it. I don't think that is happening any time soon.
We could use Vampire for a separate combinator-options-amongst-themselves test
2020-03-27 19:55:57 (GMT)
OK.
2020-03-27 19:56:18 (GMT)
In that case, we should be certain my implementation of combinators is correct, not to be biased towards lambdas
2020-03-31 15:39:2 (GMT)
For the last two days I have been going through every single problem that could not be solved by lambdas/combs
2020-03-31 15:39:32 (GMT)
2020-03-31 15:41:13 (GMT)
There is a discussion of every proof, with the time, configuration that solved it and the reason why one calculus solves and the other does not
2020-03-31 15:42:10 (GMT)
There are many cases where it is simply the case that heuristics steered the prover one way or the other
but also many interesting proofs
2020-03-31 15:42:24 (GMT)
I will systemize the list in the coming days
2020-04-01 9:2:59 (GMT)
@Ahmed B Do you have any ideas for heuristics that would help combinators?
I have ideas for a few for lambdas
2020-04-01 10:36:27 (GMT)
Petar Vukmirovic said:
Ahmed B Do you have any ideas for heuristics that would help combinators?
I have ideas for a few for lambdas
Sorry, I've been busy preparing IJCAR sumissions, so haven't yet had time to look into your very thorough problem lists more closely. I'll take a look this afternoon and get back to you.
2020-04-01 10:56:26 (GMT)
Sure, of course :) Take your time :)
2020-04-01 13:59:13 (GMT)
Petar Vukmirovic said:
At the link https://docs.google.com/spreadsheets/d/1MEyQJ33Jrp6604HUIAtmVK1B3ADWgqfz7GBCxjGfETA/edit?usp=sharing
The timings in this spreadsheet, are they the best times achieved by any strategy on that problem? Or is it how long the schedule took until a solution was found?
2020-04-01 14:15:26 (GMT)
It is the time a particular configuration in the schedule took to solve the problem
2020-04-01 14:25:31 (GMT)
One idea that comes to mind looking through these problems is to unleash limited higher-order unification (I know that is a bit of a cheat!). Alex has suggested using HO unification for simplifications. What about using it for Equality Resolution on single negative literal clauses that pass certain tests? The terms could be first translated to lambda syntax and then standord HO unif called. If no unifier returned after a certain amount of time/depth give up and continue?
2020-04-01 14:26:5 (GMT)
That would potentially help with SYO219 for example.
2020-04-01 14:35:8 (GMT)
I mean, you can have a lambda-unification-based calculus that converts unifiers to combinators on the fly before instantiating, I imagine? :)
2020-04-01 16:20:18 (GMT)
Ahmed B said:
One idea that comes to mind looking through these problems is to unleash limited higher-order unification (I know that is a bit of a cheat!). Alex has suggested using HO unification for simplifications. What about using it for Equality Resolution on single negative literal clauses that pass certain tests? The terms could be first translated to lambda syntax and then standord HO unif called. If no unifier returned after a certain amount of time/depth give up and continue?
Oke. I will add a rule that does EqRes using unification to combinators
2020-04-01 18:44:37 (GMT)
SYO219^5 was solved using such a rule :)
2020-04-01 18:49:18 (GMT)
You surely know that but there's a paper on how to do HO unification directly with combinators, btw.
2020-04-01 19:22:32 (GMT)
Dougherty: HO unification via combinators? It's not that great. For example, it doesn't terminate for X a =?= a.
2020-04-01 19:25:10 (GMT)
But Ahmed has his own variant of it (https://link.springer.com/chapter/10.1007%2F978-3-030-29436-6_5) implemented in Vampire.
2020-04-01 19:29:29 (GMT)
Oh, neat.
2020-04-01 19:30:16 (GMT)
I did implement that back in 2017, but Zipperposition did have polymorphism already…
2020-04-01 19:33:24 (GMT)
(and it did get drowned in the inferences, I think I had a limit on the depth of unifiers?)
2020-04-02 11:43:47 (GMT)
Dougherty is horrible. It enumerates all terms that ou can create
2020-04-02 11:44:15 (GMT)
*you