Computation issue with huge binary trees with sharing

[Gaspi]

The following file typechecks in less than one second in Dedukti 2.7 but is stuck in lambdapi when computing the second #EVAL command:

N : Type.
z : N.
s : N -> N.

def x2 : N -> N.
[ ] x2 z --> z
[n] x2 (s n) --> s (s (x2 n)).

def pw2 : N -> N.
[ ] pw2 z     --> s z
[n] pw2 (s n) --> x2 (pw2 n).

def 1  := pw2 z.
def 2  := pw2 1.
def 4  := pw2 2.
def 16 := pw2 4.
def 32 := x2 16.
def 65536 := pw2 16.

T : Type.
t : T.
c : T -> T -> T.

def bin : T -> T.
[X] bin X --> c X X.

def f : N -> T.
[ ] f z     --> t.
[n] f (s n) --> bin (f n).

def test : T -> N.
[ ] test t --> z.
[X] test (c (c X X) (c X X)) --> test X.

#EVAL test (f 16).
#EVAL test (f 32).
#EVAL test (f 65536).

The reason is that the term f n is meant to compute a full binary tree of depth n and therefore of size O(2^n) whose SNF doesn't (usually) fit in memory. The test function is then defined to be z on leaves and is recursively defined for trees that match the non-linear pattern c (c X X) (c X X).

This is handled in Dedukti 2.7 thanks to a syntactical check performed before computing WHNFs in the convertibility check: f 32 reduces to c (c (f 30) (f 30)) (c (f 30) (f 30)) which matches c (c X X) (c X X) without having to fully compute f 30 since all occurrences are syntactically equal.

In lambdapi there is no syntactical check but only a physical equality check which should be enough if there were enough sharing when computing f 32. For instance the following cases work:

• Replacing [n] f (s n) --> bin (f n). with [n] f (s n) --> (x => c x x) (f n).. This computes the same huge tree but using beta-redexes instead of the duplicating bin symbol.
• Replacing [X] test (c (c X X) (c X X)) --> test X. with [X] test (c X X) --> test X.. In the case where bin only needs to be unfolded once, it seems there is enough sharing to quickly perform the non-linearity convertibility check.

Is this acceptable ? If not: should lambdapi also check for syntactical equality before performing reduction ? should it better enforce sharing for non-right-linear rewrite rules ?

Side note: when defining f with all three rules:

def test : T -> N.
[ ] test t --> z.
[X] test (c X X) --> test X.
[X] test (c (c X X) (c X X)) --> test X.

lambdapi is still stuck, even when using the --keep-rule-order flag and whatever the order of the rules definitions. As explained above, removing the last rule fixes the example.