Open NotBad4U opened 1 year ago
Hi Alessio. I am afraid this won't be possible since the way AC symbols are handled in Lambdapi is crucially based on the fact that terms are always in AC-canonical form. By construction, there cannot exists terms not in AC-canonical form. You should really try to reason modulo AC: the order of elements should not be relevant. But we then get problems with unification that could perhaps be solved by a simple change: allowing AC symbols to be declared as constant (and injective?). I will try to implement this today.
symbol Prop:TYPE;
symbol -:Prop → Prop; notation - prefix 10;
associative commutative symbol +: Prop → Prop → Prop; notation + infix right 5;
injective symbol π:Prop → TYPE;
symbol resolution x a b : π (x + a) → π (- x + b) → π (a + b);
opaque symbol test a b c d x :
π (x + a + b) → π (c + d + - x) → π (a + b + c + d) ≔
begin
assume a b c d x h1 h2;
apply resolution x (b + a) (d + c) h1 h2
/* We get unification goals that Lambdapi cannot solve like:
(d + c) + (b + a) ≡ d + (c + (b + a))
(Strangely, the LHS is not in AC-canonical form.)
Lambdapi cannot solve it because + is not constant or injective.
Currently, it cannot be declared so when it is AC.
Shouldn't we allow this though? */
{ }
{ }
{ };
end;
the order of elements should not be relevant. But we then get problems with unification
yes, I have a unification error, and I agree that the order should not be relevant.
allowing AC symbols to be declared as constant (and injective?).
That could be very nice if we could have this! Because without the AC feature, we will need to depend on some tool (like Archsat, Zenon-modulo or any prologue-like?) that will tell us how to move the pivot at the correct position and I think it will be heavy for nothing. I also think that being able to declare a symbol
AC + constant
and injective
is an interesting feature.
I will try to implement this today.
Thank you very much! This problem is a little bit blocking my progress.
Thank you 👍
There is an unexpected bug in Lambdapi in the handling of AC symbols, perhaps related to Bindlib. It will probably take me more time than expected to fix this.
No, we shouldn't in unification allow decomposition of AC symbol applications; this is wrong. The problem is that some terms are not put in AC canonical form as expected. Actually, I just realized that Bindlib is unsound when using private data types. This can be fixed by recanonizing terms after each Bindlib substitution, which would be very inefficient. This is another argument to abandon Bindlib and merge #843.
https://github.com/fblanqui/lambdapi/blob/db/tests/OK/991.lp works with #843. So I invite you to use #843 instead for the moment.
This can be fixed by recanonizing terms after each Bindlib substitution, which would be very inefficient.
Yes, it sounds not a very desirable solution, especially in my case where a formula could have tens of literals.
https://github.com/fblanqui/lambdapi/blob/db/tests/OK/991.lp works with https://github.com/Deducteam/lambdapi/pull/843. So I invite you to use https://github.com/Deducteam/lambdapi/pull/843 instead for the moment.
Okay, I will have a look at this today.
The reconstruction of resolution
seems to work https://gist.github.com/NotBad4U/47eeda2d489fd595a368a509d3bde7a5. I just lost the type inference but I guess it is because the PR is a WIP.
No, that PR should work. It is less efficient but should work. Please add an example where type inference does not work.
The reconstruction of resolution seems to work
Yes, I said it worked 😄 : "The reconstruction of resolution seems to work..."
Please add an example where type inference does not work.
Sorry, In the end, the type inference works. I just forgot that my disjunction has the modifier associative commutative symbol ∨ ...
so it is normal that unification failed in some cases.
Thanks for your solution! I think we should keep the issue open until #843 is merged. I will report any further problems here in case I am facing other bugs.
symbol Prop:TYPE;
associative commutative symbol +: Prop → Prop → Prop;
constant symbol p:Prop;
constant symbol q:Prop;
symbol T: Prop → TYPE;
symbol a x y: T(+ x y);
type a p q; // T (+ q p) -- this is wrong! it should be T(+ p q)
Please add an example where type inference does not work.
In this case, the inference does not work, and the problem does not come from the modifier associative commutative
because it sounds to still not work if you remove it.
symbol Prop: TYPE;
injective symbol π: Prop → TYPE;
symbol ¬: Prop → Prop; notation ¬ prefix 10;
associative commutative symbol ⟇: Prop → Prop → Prop; notation ⟇ infix right 5;
constant symbol not_not [x] : π (¬ ( ¬ ( ¬ x)) ⟇ x);
opaque symbol test x : π (¬ ( ¬ ( ¬ x)) ⟇ x) ≔
begin
assume x;
apply not_not ;
// apply @not_not x; work with explicit parameter
end;
In the case where ⟇ is not declared associative commutative, the problem is that ⟇ is declared as definable (there is no modifier) and not constant or injective and thus lambdapi does not know how to solve a problem of the form a ⟇ b = c ⟇ d (there may be many different solutions depending on the rules defining ⟇). This is a common mistake... And, of course, if ⟇ is declared associative commutative then it is not constant and not injective.
But in this case, the symbol ⟇ will not have a definition and just exists at the syntactic level.
An interesting solution will be to be able to define ⟇ as constant commutative associative symbol ⟇: ...;
,
and then the unification will work. But why constant
is declared as incompatible with modifiers commutative associative
?
It is a feature we can add when the symbol does not have a definition?
If ⟇ is commutative then ⟇ cannot be constant nor injective: a ⟇ b = c ⟇ d has 2 solutions: (a,b)=(c,d) and (a,b)=(d,c).
Okay thx for the answer,
If ⟇ is commutative then ⟇ cannot be constant nor injective: a ⟇ b = c ⟇ d has 2 solutions: (a,b)=(c,d) and (a,b)=(d,c).
So that means being constant
implies having a unique solution whereas commutative implies at least two?
Just to understand, here in my case with not_not
I have this error
Missing subproofs (0 subproofs for 2 subgoals):
x: Prop
--------------------------------------------------------------------------------
0. ¬ (¬ (¬ ?7.[x])) ⟇ ?7.[x] ≡ x ⟇ ¬ (¬ (¬ x))
1. ?7: Prop
because ¬ (¬ (¬ ?7.[x])) ⟇ ?7.[x]
has two solutions: x ⟇ ¬ (¬ (¬ x))
and ¬ (¬ (¬ x)) ⟇ x
and Lambdapi do not know which one it should use to unify? Or he knows how to unify for ¬ (¬ (¬ x)) ⟇ x
but it does not know for x ⟇ ¬ (¬ (¬ x))
?
To understand what unification tries to do, add debug +u;
just before.
An equation of the form f t1 .. tn = f u1 .. un can be simplified to the set of equations t1 = u1, .., tn = un only if f is injective (constant is a particular case of injectivity).
Hi!
When I apply the modifiers
associative commutative
on a symbol, and if I have a term with this symbol in the hypothesis of a proof, Lambdapi automatically puts it in its normal form. Where I would prefer that it just keep the term as it is and just apply the normal form for unification when I need it.Let me illustrate to you why I would like this because of Alethe's reconstruction.
Problem with Alethe
I defined a symbol to represent the clauses in a step of the Alethe format
The definition
test
is a formula of 3 litterals that looks like this clause in an Alethe step:Problem for reconstructing CNF resolution step
When Alethe does
resolution
CNF, the pivot can be anywhere in a formula. For example, here, you want to do aresolution
with H1 and H2 withx
as a pivot.The problem is that my
resolution
lemma is not flexible in syntax. It attempted to have the pivot at the left side of the term (of course, I can also have the dual with a lemma that put the pivot on the right side but theassociative
modifier is right associative).So with H2, the
¬ x
is at the right of the expression. To overcome the problem of the undefined position of the pivot in Alethe clauses, I wanted to use the modifiercommutative associative
to have a normal form and reorder the pivot in a sublemma when the pivot is not placed correctly. I expect that the proof is immediate by unification. The problem is the term is reordered automatically in their normal form:when I
assume H2
at (1), I got the hypothesis:and I would prefer that Lambdapi does not change the order. At (2), I tried to reorder H2 by putting the pivot at the left, but Lambdapi automatically rewrites the
H2_correct
asπ ((d ⟇ (c ⟇ ¬ x)) = (d ⟇ (c ⟇ ¬ x)))
soapply resolution H (subst H2 H2_correct)
failed because the pivot is still at the wrong position.Conclusion
Could we remove this undesired rewrite because it will make the reconstruction of the resolution step easier?