2020-06-09 18:58:8 (GMT)
Hi all,
Do you have an idea how I can delay open flex-flex pairs (the ones with loosely bound free variables)?
Does it suffice to convert the constraint into constraint between lambdas that closes all variables?
2020-06-09 19:4:3 (GMT)
Do you mean something like this: Preunifying λx. f (Y x) =?= λx. f (Z a) will yield the flex-flex pairY x =?= Z a. And then you are wondering what to do with the unbound x?
2020-06-09 19:5:34 (GMT)
Yes, I think you can just convert it into λx. Y x =?= λx. Z a. Some descriptions of unification algorithms do this anyway to distinguish free and loose bound variables, right?
2020-06-09 19:7:30 (GMT)
Or, alternatively, you could put Skolems with the free variables as arguments in there. That would be correspond to applying NegExt to the lambdas.
2020-06-09 19:45:30 (GMT)
Indeed... I will convert it into lambda to have a more modular implementation :slight_smile:
2020-06-09 19:45:42 (GMT)
Thanks... I just wanted to check whether my intuition is right
2020-06-10 10:58:46 (GMT)
I tested the idea of delaying flex-flex pairs and it makes more or less no difference on solvability of the problems
because most flex-flex pairs are solved using some oracle
2020-06-10 11:26:17 (GMT)
What does "delaying flex-flex pairs" mean exactly? E.g. if a clause contains two positive literals, one of which is a flex-flex equality, do you only focus on the other literal, even though the flex-flex pair is (surely) maximal? Is that what you mean?
2020-06-10 11:43:20 (GMT)
No. This means that when unification procedure gets a flex-flex pair, it is going to store it as a constraint instead of solving it
2020-06-10 11:43:30 (GMT)
That is, it is going to be hoisted to the literal level
2020-06-10 11:46:35 (GMT)
Is the flex-flex constraint just an ordinary literal or does it have some kind of special status in the clause?
2020-06-10 11:48:13 (GMT)
it is just an ordinary literal
2020-06-10 11:48:57 (GMT)
and it is hoisted only if it is not at the top-level of unification (i.e., if the original problem is the flex-flex pair, at least one step of unif algorithm will be done on it)
2020-06-10 12:20:5 (GMT)
Ah, I see. Just make sure not to do that in the complete mode. ;)
2020-06-10 13:30:1 (GMT)
of course ... I am not doing it in the pragmatic mode either since it does not work well :slight_smile:
2020-06-10 14:0:19 (GMT)
BTW provers like the Leo's work this way for all unification constraints, not just flex-flex. It's part of their calculus.
2020-06-10 17:35:42 (GMT)
Zipperposition used to do that too, and may still do it for arithmetic and boolean pairs if @Petar Vukmirovic didn't remove that. Some unification constraints are just postponed and turned into negative equality literals.