Bug in higher-order matching

[francoisthire]

I am sorry, I don't have time to minimize the example. I am aware of a type checking issue in Lambdapi which is probably related to Higher-Order matching. The error can be found in the Librairies repository. There are two files in play. The first one encodes Cedille's core theory: cedille.dk . The second one encodes a basic example with it: nat.dk.

The first file type checks but not the second in Lambdapi (but it does in Dedukti and Dedukti is right on this one). I know that the error commes from either this rule or this rule which are both Higher-Order rules. One of these rules is not applied while it should.

[gabrielhdt]

The issue might come from the matching of an abstraction against an applied pattern variable. The current lambdapi rejects it as line 176 of eval.ml suggests.

[GuillaumeGen]

This issue suggests that even in the old syntax, LambdaPi performs syntactic matching rather than matching modulo beta.

[francoisthire]

Does your PR @gabrielhdt fixes this issue?

[gabrielhdt]

Hum for now it fails to build a tree, precisely because of this case. It should be easy to fix though.

[gabrielhdt]

The decision trees branch now behave like the master branch, that is, it raises

[cedille.dk, 46:0-51] Term [mk_iota cnat cz inat iz I] does not have type [Term star nat].

[francoisthire]

Alright, but the file is well-typed, so there is still a bug.

[GuillaumeGen]

The error message is weird, since the line which raises the problem is the line 46 of nat.dk, not of cedille.dk.
The "file is well-typed" depends on the definition of matching. I think refusing this file could have been a reasonable choice, but both implementations must agree.

[francoisthire]

@GuillaumeGen Can you detail your comment? Why do you think it depends on the definition of "matching"?

[rlepigre]

I can try to have a look later, but you should definitely try to make the example more minimal (just inline nat.dk at the end of cedille.dk), and also convert it to Lambdapi syntax. The legacy syntax may not be translated accurately, and it would be easier to debug this way.

[GuillaumeGen]

As far as I understand, LambdaPi implements AFSM (or something close to it). Hence there are two kind of application, the usual one x y and the metavariable one X[y].
The metavariable one comes with arity constraint and in the lhs of a rule you have the pattern restriction (only distinct bound variables). Matching is performed syntactically on usual application and "modulo beta" on meta-variable application.
I put "modulo beta" between quotes since the metavariables have a fixed arity, so it does not really create lambdas.

[francoisthire]

@rlepigre Here you go

symbol const Sort : TYPE

symbol const star : Sort

symbol const box : Sort

symbol Rule : Sort ⇒ Sort ⇒ Sort

rule Rule _ &s → &s

symbol const Univ : Sort ⇒ TYPE

symbol Term : ∀ (s : Sort), Univ s ⇒ TYPE

symbol const ustar : Univ box

rule Term _ ustar → Univ star

symbol prod :
  ∀ (s1 : Sort), ∀ (s2 : Sort), ∀ (A : Univ s1), (Term s1 A ⇒ Univ
  s2) ⇒ Univ (Rule s1 s2)

rule Term _ (prod &s1 &s2 &A &B) → ∀ (x : Term &s1 &A), Term &s2 (&B x)

symbol iprod :
  ∀ (s1 : Sort), ∀ (s2 : Sort), ∀ (A : Univ s1), (Term s1 A ⇒ Univ
  s2) ⇒ Univ (Rule s1 s2)

rule Term _ (iprod &s1 &s2 &A &B) → ∀ (x : Term &s1 &A), Term &s2 (&B x)

definition forall :
  ∀ (t : Univ star), (Term star t ⇒ Univ star) ⇒ Univ star ≔
  λ A, λ B, prod star star A B

definition iforall :
  ∀ (t : Univ star), (Term star t ⇒ Univ star) ⇒ Univ star ≔
  λ A, λ B, iprod star star A B

definition arrow : Univ star ⇒ Univ star ⇒ Univ star ≔
  λ A, λ B, forall A (λ __, B)

definition iforallk :
  ∀ (K : Univ box), (Term box K ⇒ Univ star) ⇒ Univ star ≔
  λ A, λ B, iprod box star A B

definition pi :
  ∀ (t : Univ star), (Term star t ⇒ Univ box) ⇒ Univ box ≔
  λ A, λ B, prod star box A B

symbol const True : TYPE

symbol const I : True

symbol const pure : TYPE

symbol const lam : (pure ⇒ pure) ⇒ pure

symbol Eq : pure ⇒ pure ⇒ TYPE

rule Eq &x &x → True

symbol code : ∀ (s : Sort), ∀ (t : Univ s), Term s t ⇒ pure

symbol uncode : ∀ (s : Sort), ∀ (t : Univ s), pure ⇒ Term s t

rule code _ (prod &s1 &s2 &A &B) (λ x, &f[x])
   → lam (λ (x : pure), code &s2 (&B (uncode &s1 &A x)) &f[uncode &s1 &A
         x])

symbol const dummy : pure

rule code _ (iprod &s1 &s2 &A &B) (λ x, &f[x])
   → code &s2 (&B (uncode &s1 &A dummy)) &f[uncode &s1 &A dummy]

rule code _ _ (uncode _ _ &x) → &x

symbol const iota :
  ∀ (t : Univ star), (Term star t ⇒ Univ star) ⇒ Univ star

symbol mk_iota :
  ∀ (t1 : Univ star), ∀ (t : Term star t1),
  ∀ (t2 : Term box (pi t1 (λ __, ustar))), ∀ (t' : Term star (t2 t)), Eq
  (code star t1 t) (code star (t2 t) t') ⇒ Term star (iota t1 t2)

definition cnat : Univ star ≔
  iforallk ustar (λ X, arrow X (arrow (arrow X X) X))

definition cz : Term star cnat ≔ λ X, λ z, λ s, z

definition cs : Term star (arrow cnat cnat) ≔
  λ n, λ X, λ z, λ s, s (n X z s)

definition inat : Term box (pi cnat (λ __, ustar)) ≔
  λ (x : Term star cnat),
  iforallk (pi cnat (λ __, ustar)) (λ P, arrow (P cz) (arrow (iforall cnat
    (λ m, arrow (P m) (P (cs m)))) (P x)))

definition iz : Term star (inat cz) ≔ λ P, λ pz, λ __, pz

definition nat : Univ star ≔ iota cnat inat

definition Z : Term star nat ≔ mk_iota cnat cz inat iz I

[francoisthire]

Maybe I should mention also that this example comes from the encoding of a type system called Cedille from Aaron Stump. It features mainly:

• Dependent intersection types
• Curry style type theory
• Untyped equality

The original file I have provided in this issue aims to encode this logic. Nat is an example that this encoding seems to work. The main benefit of Cedille is to be able to derive inductive types. This is the theorem I proved in Nat.dk.

From my understanding, PML is not that far from Cedille. Maybe it is possible to have an encoding of PML in Dedukti then.

[fblanqui]

Remark: the file is checked if we replace the first rule defining code by

rule code _ (prod &s1 &s2 &A &B) &f
   → lam (λ (x : pure), code &s2 (&B (uncode &s1 &A x)) (&f (uncode &s1 &A x)))

[francoisthire]

So it is indeed a Higher-Order issue. In my case though, I don't want to use this rule since it does an eta-expansion.

[fblanqui]

No.

[fblanqui]

And this rule is more general since it applies even if the argument is not a lambda.

[francoisthire]

In Cedille it does ^^ .

[fblanqui]

How?

[francoisthire]

Because using this rule, you maybe have two terms f and \x. f~x which are not equal in Cedille, but their encoding will be because the encoding of f will match the left pattern, and hence, the encoding of both terms will be convertible.

[fblanqui]

The "normal form" computed by LP for code star cnat cz is:

lam (λx,
       code
         star
         (prod
           star
           star
           (prod
             star
             star
             (uncode box ustar dummy)
             (λ__, uncode box ustar dummy))
           (λ__, uncode box ustar dummy))
         (λs, uncode star (uncode box ustar dummy) x))

This is not a normal form. It seems that (λs, uncode star (uncode box ustar dummy) x) does not match λs,&f[s]. I propose the following explanation: λs, uncode star (uncode box ustar dummy) x is not recognized as a closed term since it contains the free variable x. What do you think @rlepigre ?

[fblanqui]

This is indeed the case as shown by the following example:

symbol T:TYPE
symbol a:T
symbol f:(T⇒T)⇒T
rule f (λx,&F[x]) → a
compute λx,f(λy,x) // does not return λx,a !

[rlepigre]

@fblanqui you are right about that, your explanation is correct. The environment [s] in &f[s] says that the only variable that can appear in a matching term is s.

[fblanqui]

Will it be easy to fix? It seems that we cannot use is_closed. Instead we need to check that some variables do not occur. Is it possible to do this efficiently with Bindlib?

[rlepigre]

But is that really a bug though? For me this looks like some variable is gonna escape its scope here.

[francoisthire]

If you have a rule

rule foo &x &y --> &x

it matches the term foo z z. The fact that z is free is not a problem right? You don't expect that the term that matches the variable &x is closed.

When you encounter the rule

rule foo (\x. &f[x]) --> f[0].

You cannot assume, for the same reason that any term which matches f[x] has only x has as a free variable. At least, this is not what it is intended when Miller's presented its restriction. And the current behavior implemented by Dedukti is the one implemented by every other languages supporting the Miller's pattern fragment I know.

[gabrielhdt]

I have a branch with dtrees that solves Frederic subproblem, but not Francois'

[fblanqui]

@rlepigre , this is the difference between programming languages and proof assistants: in proof assistants, we want to compute strong normal forms, hence reduce under lambda's.

[fblanqui]

Will be fixed by merging #172.

[rlepigre]

Let's not close until the bug has been fixed in master (I'll take care of that now), especially since #172 is not ready to be merged in my opinion. I'll review it right after I fix master.

[fblanqui]

Could you please explain why Gabriel's branch does not solve the problem? Do you have an example?

[rlepigre]

In fact I'm not sure, I'm still trying to understand what is happening. There are several issues going on at the same time. Solving the issue naively may lead to free variables escaping their scope if we are not careful. For instance, consider the following example.

symbol const T : TYPE
symbol const e : T

symbol get : (T ⇒ T) ⇒ T
rule get (λx, &f) → &f

// Should give [e]
compute get (λx, (λ _, e) x)

What used to happen here was that &f was set to be (λ _, e) x, which was obviously wrong since x escaped its scope, even though the result was still correct in the end (x eventually disappears through computation).

With the approach that I am considering now, this issue is solved. However, I now run into the problem that (λ _, e) x cannot match &f unless we first evaluate it to e. In general, we may need an arbitrary number of reduction steps, at arbitrary places, to ensure that "forbidden" variables disappear (and weak head normalization is not enough). I'm not sure what is the desired approach here. One solution would be to compute the (strong) normal form before matching, which would guarantee that every variable that can disappear does disappear. But that that's probably not "lazy" enough, is it?

Does Dedukti do anything special to enforce that free variables do not escape their scope @francoisthire?
And is anything special done for that kind of case in your branch @gabrielhdt?

[francoisthire]

Maybe @barras or @Gaspi will give a better answer than mine. But in Dedukti you cannot write your rule. We have a restriction that the arity of every variable on the righ-hand side of the rule should be greater than any occurence of this symbol on the left-hand side.

But here, I think we try also to solve this problem by computing the snf of the argument if the matching failed beforehand.

[gabrielhdt]

In my branch, &f would be (\lambda _ e) x as you said. But I don't see why it is wrong. On the other hand, indeed unless we beta normalise, the term won't match since &f must contain no free variable.

[rlepigre]

@gabrielhdt it is very wrong because reducing get (λx, (λ _, e) x) (which is closed) will produce (λ _, e) x (which is open) as an intermediate step. The fact that x will here be erased after a step of beta-reduction is a pure coincidence, and if it would be very much possible that a variable escapes through this mechanism.

[rlepigre]

@francoisthire my example comes from a simplification of the ho_bug1.dk file (see here) that is used in our unit tests. The problem with this example (under my attempted fix) is essentially the same, so I don't understand why Dedukti would reject the above example and still allow the example in ho_bug1.dk.

[fblanqui]

Rodolphe, I believe that there is a misunderstanding about what Gabriel said. Gabriel, correct me if I am wrong but I think that you said that, currently, in your branch, get (λx, (λ _, e) x) does not reduce because (λ _, e) x contains x. If we were reducing (λ _, e) x before testing variables, we would get e and then, indeed, get (λx, (λ _, e) x) would be reducible to e because e does not contain x. So, you are right Rodolphe, this reduction strategy is not complete. But free variables are preserved: no bound variable will escape its scope. To fix this new problem (strategy completeness), we need to strongly normalize the argument before testing variables. Note however that this is necessary only when there are forbidden variables indeed, and this is very rare in practice. So, Gabriel, I am thinking that, in your decision trees, you should have a variable test only if there are forbidden variables like in Rodolphe's example. For instance, in f (λx,g(F[x])) → r, there is no check to do. Is it what you implemented?

[gabrielhdt]

That is indeed what I meant. However, this is what I thought I implemented, and in fact, I just found a bug in some auxiliary function. I'm fixing this.

Regarding the conditional test, I intended to do this, but some tests failed, namely the miller ones, because I had to check that variables are swapped in this test. Otherwise, decision on whether a test has to be done is done at compile time and takes into account the bracketed variables and the traversed lambda; it is done here.

[gabrielhdt]

So as of commit 4e458b7, the expected behaviour announced by Frederic operates.

Additionally, I've made clearer what I stated above, see here and there. In both lines, one condition translates "check for free variables if some are forbidden", the other part forces the variable check in case of permutation of free variables as shown there.

[rlepigre]

@gabrielhdt What about efficiency in your branch? Have you tested make matita and the likes?

[francoisthire]

@francoisthire my example comes from a simplification of the ho_bug1.dk file (see here) that is used in our unit tests. The problem with this example (under my attempted fix) is essentially the same, so I don't understand why Dedukti would reject the above example and still allow the example in ho_bug1.dk.

I made a mistake in my answer. I thought that f was applied to x in the pattern. Since it is not the case, you need to take into account the second part of my answer, not the first part.

[gabrielhdt]

@rlepigre on verine, performance does not change, but I haven't fixed the issue as you have done, using snf (i.e. my branch is still buggish)

[rlepigre]

@gabrielhdt OK, no worries. I started to give comments on your PR, but I'll do that in several waves. It would be nice to merge it soon, and solve the problems at the same time. I don't want to spend time optimizing the version I fixed, it is probably better to finish the work on decision trees.

[francoisthire]

Is it possible to get a behavior similar to the current one once @gabrielhdt PR will be merged?

[gabrielhdt]

wdym?

[fblanqui]

@gabrielhdt I don't understand why you have to check variable occurrences when there is a permutation. In abstractions.lp there should be no test on variables.

[gabrielhdt]

@fblanqui in fact it is a trivial variable check, but I need to remap the right variables into the term, and this is done by a variable check.

[fblanqui]

I don't understand. If you take f (λx, λy, &F[x,y]) → r, there is nothing to do whatever r is. Idem for f (λx, λy, &F[y,x]) → r. Assume that you try to match λx, λy, t against λx, λy, &F[x,y], then F will be set to λx, λy, t. If you try to match against λx, λy, &F[y,x] then F will be set to λy, λx, t because abstractions are done in the order of the arguments of F. And all this does not depend on r. If r contains F[a,b] then it will be replaced by t{x=a,y=b} in the first case, and t{x=b,y=a} in the second case. But this is taken care by the substitution mechanism.

[gabrielhdt]

I was mistaken, it has nothing to do with permutation. However, during evaluation, I unbind terms using variables created at compile time. In the end, I must gather the free variables introduced and bind them into right hand side. This is currently done by a variable check, which performs a lift to get the variables, and then a bind_mvar. It is possible to do it outside the free variable check though, if you want to separate things.

[fblanqui]

Yes, it would be better to separate the two.

[gabrielhdt]

Commit 2494410 separates the two, and no free var check is done in abstractions.lp.