Deducteam
Taking types into account when checking local confluence is not sound
This is a counterexample to the technique of taking typability constraints into account when checking local confluence. This technique apparently had been implemented by this PR but I had seen not theoretical justification for it. Now this shows that this is indeed unsound.
Consider the following Lambdapi file (tested with version 2.4.1).
constant symbol Set : TYPE;
constant symbol List (A : Set) : TYPE;
constant symbol nil (A : Set) : List A;
symbol concat (A : Set) (l l' : List A) : List A;
rule concat $A (nil $B) $l ↪ $l;
rule concat $A $l (nil $B) ↪ $l;
constant symbol bool : Set;
constant symbol nat : Set;
constant symbol list : Set → Set;
symbol c : Set;
symbol F : Set → Set → Set;
rule F $x $x ↪ nat;
rule F $x (list $x) ↪ bool;
rule c ↪ list c;
The only critical pair is the following, which is unjoignable on untyped terms.
nil $A' <-- concat $A (nil $A') (nil $A'') --> nil $A''
The typing constraints, together with the (supposed) injectivity of List, would ensure that A' and A'' are convertible, so once could think that this is ok. Apparently, Lambdapi thinks this as it does not report this critical pair. However, we have
nat <-- F c c --> F c (list c) --> bool
and thus we can type nil bool : List nat. Therefore the term concat nat (nil nat) (nil bool) is well typed, but it reduces to both nil nat and nil bool, which are irreducible. Therefore, the rewrite system restricted to well-typed terms is not locally confluent.
This is a counter-example to what exactly? Lambdapi just tries to check that, when adding new rules, the typable critical pairs are joinable (which is not decidable). If it finds such a critical pair, then it prints a warning. It would be unsound if it were printing a wrong warning. When checking the rules of concat, it is true that there is no typable critical pairs that are unjoinable in the theory with concat only. Then, you had (well known) rules that have no critical pair and so are locally confluent, but are non confluent and non terminating. What do you expect from Lambdapi here?
What this shows is that it is unsound to deduce that nil A' and nil A'' have a common reduct just because A' and A'' are convertible by typing constraints. To have this you would need to apply confluence, but this is a circular reasoning because you are in the middle of the proof of local confluence. To answer your question, I would expect that Lambdapi should only apply techniques that we have proven to be correct, and this shows that the technique implemented here does not seem to be correct, or in any case I can see no clear reason why you can deduce that nil A' and nil A'' are joinable from the convertibility of A' and A''.