search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
270 stars 35 forks source link

Inferring implicit parameters of binders is too slow #941

Open cstolze opened 1 year ago

cstolze commented 1 year ago

The following code takes 0.4 seconds to get typechecked:

constant symbol T : TYPE;
constant symbol τ : T → TYPE;
constant symbol A : T;

constant symbol U : TYPE;
constant symbol ∀ [t] : (τ t → U) → U;
notation ∀ quantifier;
constant symbol TRUE : U;

symbol foo : U ≔ `∀ (x1 : τ A), `∀ (x2 : τ A), `∀ (x3 : τ A), `∀ (x4 : τ A), `∀ (x5 : τ A), `∀ (x6 : τ A), `∀ (x7 : τ A), `∀ (x8 : τ A), `∀ (x9 : τ A), `∀ (x10 : τ A), `∀ (x11 : τ A), `∀ (x12 : τ A), `∀ (x13 : τ A), `∀ (x14 : τ A), `∀ (x15 : τ A), `∀ (x16 : τ A), `∀ (x17 : τ A), `∀ (x18 : τ A), `∀ (x19 : τ A), `∀ (x20 : τ A), `∀ (x21 : τ A), `∀ (x22 : τ A), `∀ (x23 : τ A), `∀ (x24 : τ A), `∀ (x25 : τ A), `∀ (x26 : τ A), `∀ (x27 : τ A), `∀ (x28 : τ A), `∀ (x29 : τ A), `∀ (x30 : τ A), `∀ (x31 : τ A), `∀ (x32 : τ A), `∀ (x33 : τ A), `∀ (x34 : τ A), `∀ (x35 : τ A), `∀ (x36 : τ A), `∀ (x37 : τ A), `∀ (x38 : τ A), `∀ (x39 : τ A), `∀ (x40: τ A), `∀ (x41 : τ A), `∀ (x42 : τ A), `∀ (x43 : τ A), `∀ (x44 : τ A), `∀ (x45 : τ A), `∀ (x46 : τ A), `∀ (x47 : τ A), `∀ (x48 : τ A), `∀ (x49 : τ A), `∀ (x50 : τ A), `∀ (x51 : τ A), `∀ (x52 : τ A), `∀ (x53 : τ A), `∀ (x54 : τ A), `∀ (x55 : τ A), TRUE;

Adding explicitely the implicit parameter, it gets reduced to 0.02 seconds:

constant symbol T : TYPE;
constant symbol τ : T → TYPE;
constant symbol A : T;

constant symbol U : TYPE;
constant symbol ∀ [t] : (τ t → U) → U;
notation ∀ quantifier;
constant symbol TRUE : U;

symbol foo : U ≔ ∀ [A] (λ (x1 : τ A), ∀ [A] (λ (x2 : τ A), ∀ [A] (λ (x3 : τ A), ∀ [A] (λ (x4 : τ A), ∀ [A] (λ (x5 : τ A), ∀ [A] (λ (x6 : τ A), ∀ [A] (λ (x7 : τ A), ∀ [A] (λ (x8 : τ A), ∀ [A] (λ (x9 : τ A), ∀ [A] (λ (x10 : τ A), ∀ [A] (λ (x11 : τ A), ∀ [A] (λ (x12 : τ A), ∀ [A] (λ (x13 : τ A), ∀ [A] (λ (x14 : τ A), ∀ [A] (λ (x15 : τ A), ∀ [A] (λ (x16 : τ A), ∀ [A] (λ (x17 : τ A), ∀ [A] (λ (x18 : τ A), ∀ [A] (λ (x19 : τ A), ∀ [A] (λ (x20 : τ A), ∀ [A] (λ (x21 : τ A), ∀ [A] (λ (x22 : τ A), ∀ [A] (λ (x23 : τ A), ∀ [A] (λ (x24 : τ A), ∀ [A] (λ (x25 : τ A), ∀ [A] (λ (x26 : τ A), ∀ [A] (λ (x27 : τ A), ∀ [A] (λ (x28 : τ A), ∀ [A] (λ (x29 : τ A), ∀ [A] (λ (x30 : τ A), ∀ [A] (λ (x31 : τ A), ∀ [A] (λ (x32 : τ A), ∀ [A] (λ (x33 : τ A), ∀ [A] (λ (x34 : τ A), ∀ [A] (λ (x35 : τ A), ∀ [A] (λ (x36 : τ A), ∀ [A] (λ (x37 : τ A), ∀ [A] (λ (x38 : τ A), ∀ [A] (λ (x39 : τ A), ∀ [A] (λ (x40 : τ A), ∀ [A] (λ (x41 : τ A), ∀ [A] (λ (x42 : τ A), ∀ [A] (λ (x43 : τ A), ∀ [A] (λ (x44 : τ A), ∀ [A] (λ (x45 : τ A), ∀ [A] (λ (x46 : τ A), ∀ [A] (λ (x47 : τ A), ∀ [A] (λ (x48 : τ A), ∀ [A] (λ (x49 : τ A), ∀ [A] (λ (x50 : τ A), ∀ [A] (λ (x51 : τ A), ∀ [A] (λ (x52 : τ A), ∀ [A] (λ (x53 : τ A), ∀ [A] (λ (x54 : τ A), ∀ [A] (λ (x55 : τ A), ∀ [A] (λ (x56 : τ A), ∀ [A] (λ (x57 : τ A), ∀ [A] (λ (x58 : τ A), ∀ [A] (λ (x59 : τ A), ∀ [A] (λ (x60 : τ A), TRUE))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
fblanqui commented 1 year ago

In the second case, no unification problems are generated. Moreover a metavariable depends on all the bound variables occurring before. So we probably have a quadratic complexity here.