undesired side effect with modifiers associative and commutative on symbol

[NotBad4U]

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

// symbol to represent clause in Alethe format
associative commutative symbol ⟇: Prop → Prop → Prop; // ⟇ is \veedot 
notation ⟇ infix right 5;

symbol test_clause:  a ⟇ b ⟇ c;  // a,b,c defined with type Prop

The definition test is a formula of 3 litterals that looks like this clause in an Alethe step:

(step  (cl  a b  c) :rule xxxx)

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 a resolution with H1 and H2 with x as a pivot.

H1: x ⟇ a ⟇ b
H2: c ⟇ d ⟇ (¬ x)
-----------
a ⟇ b ⟇ c ⟇ d

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 the associative modifier is right associative).

opaque symbol resolution [x a b] : π (x ⟇ a) → π ((¬ x) ⟇ b) → π (a ⟇ b) ≔
begin
...
end;

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 modifier commutative 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:

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 H H2;  // (1)
    have H2_correct : π (((¬ x) ⟇ (c ⟇ d)) = (c ⟇ (d ⟇ (¬ x))) ) {
        reflexivity // automatic with modifier
    };
    // (2)
    apply resolution H (subst H2 H2_correct) // subst replace (c ⟇ (d ⟇ (¬ x)) ➡️  (¬ x) ⟇ (c ⟇ d)
end;

when I assume H2 at (1), I got the hypothesis:

H: π (x ⟇ (b ⟇ a))
H2: π (d ⟇ (c ⟇ ¬ x)) // I expect to have π (c ⟇ (d ⟇ (¬ x)))

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))) so apply 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?

[fblanqui]

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;

[NotBad4U]

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 👍

[fblanqui]

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.

[fblanqui]

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.

[fblanqui]

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.

[NotBad4U]

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 #843. So I invite you to use #843 instead for the moment.

Okay, I will have a look at this today.

[NotBad4U]

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.

[fblanqui]

No, that PR should work. It is less efficient but should work. Please add an example where type inference does not work.

[NotBad4U]

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.

[fblanqui]

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)

[NotBad4U]

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;

[fblanqui]

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.

[NotBad4U]

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?

[fblanqui]

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).

[NotBad4U]

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))?

[fblanqui]

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).