lambdapi

lambdapi copied to clipboard

While working on https://github.com/dwarfmaster/ett-in-lambdapi/blob/recursive-let/ETT/rr.lp, I got strange unification errors, and sometimes lambdapi would not terminate even after consuming all my RAM. It turns out this was linked to my extensive use of the let in construct. Indeed, after inlining almost all the let in, it worked as expected.

I havent managed to create a smaller example of the behaviour, but I have managed to reproduce it again. There (on the recursive-let branch), there are three file, rr.lp, failing.lp and ram_out.lp that are almost the same, and only differ by more or less inlining of let ... in in the very last rewriting rule.

• ram_out.lp : This one was the original code, with many constructs factorised into variables. When running lambdapi check ram_out.lp, it consumes all my RAM (~15Go) without either succeeding or failing, until I interrupt it.
• failing.lp : I inlined most of the definition, and in this situation it terminates with the following error :

[/data/luc/repos/ett-in-dedukti/ETT/failing.lp, 173:5-186:105] Cannot solve τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA ≡ ?78[a]
Cannot solve τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA ≡ ?78[a]
Cannot solve τ_T (TPush ETT.failing.$v0_Γ ETT.failing.$v5_s ETT.failing.$v8_A ETT.failing.$v11_dA (transport (τ_s ETT.failing.$v5_s) ?78[a] (τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s ETT.failing.$v11_dA) (convert_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA ETT.failing.$v11_dA) a)) ETT.failing.$v10_B ETT.failing.$v6_s' ETT.failing.$v13_dB ≡ τ_T (TPush ETT.failing.$v0_Γ ETT.failing.$v5_s ETT.failing.$v8_A ETT.failing.$v11_dA (transport (τ_s ETT.failing.$v5_s) (τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA) (τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s ETT.failing.$v11_dA) (convert_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA ETT.failing.$v11_dA) a)) ETT.failing.$v10_B ETT.failing.$v6_s' ETT.failing.$v13_dB
Cannot solve ITT.eq (ITT.snext (ITT.smax (τ_s ETT.failing.$v5_s) (τ_s ETT.failing.$v6_s'))) (ITT.u (ITT.smax (τ_s ETT.failing.$v5_s) (τ_s ETT.failing.$v6_s'))) (ITT.S (τ_s ETT.failing.$v5_s) (τ_s ETT.failing.$v6_s') (τ_T ETT.failing.$v0_Γ
ETT.failing.$v8_A ETT.failing.$v5_s udA) (λ a, τ_T (TPush ETT.failing.$v0_Γ ETT.failing.$v5_s ETT.failing.$v8_A udA a) ETT.failing.$v10_B ETT.failing.$v6_s' ETT.failing.$v13_dB)) (ITT.S (τ_s ETT.failing.$v5_s) (τ_s ETT.failing.$v6_s') (τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s ETT.failing.$v11_dA) (λ a, τ_T (TPush ETT.failing.$v0_Γ ETT.failing.$v5_s ETT.failing.$v8_A ETT.failing.$v11_dA a) ETT.failing.$v10_B ETT.failing.$v6_s' ETT.failing.$v13_dB)) ≡ ?175
Cannot solve ?173 ≡ τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA
Cannot solve ?173 ≡ τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA
Cannot solve ?175 ≡ ITT.eq (ITT.snext (ITT.smax (τ_s ETT.failing.$v5_s) (τ_s ETT.failing.$v6_s'))) (ITT.u (ITT.smax (τ_s ETT.failing.$v5_s) (τ_s ETT.failing.$v6_s'))) (ITT.S (τ_s ETT.failing.$v5_s) (τ_s ETT.failing.$v6_s') (τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA) (λ a, τ_T (TPush ETT.failing.$v0_Γ ETT.failing.$v5_s ETT.failing.$v8_A udA a) ETT.failing.$v10_B ETT.failing.$v6_s' ETT.failing.$v13_dB)) (ITT.S (τ_s ETT.failing.$v5_s) (τ_s ETT.failing.$v6_s') (τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s ETT.failing.$v11_dA) (λ a, τ_T (TPush ETT.failing.$v0_Γ ETT.failing.$v5_s ETT.failing.$v8_A ETT.failing.$v11_dA a) ETT.failing.$v10_B ETT.failing.$v6_s' ETT.failing.$v13_dB))
Cannot solve ?173 ≡ τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA
Cannot solve ?173 ≡ τ_T ETT.failing.$v0_Γ ETT.failing.$v8_A ETT.failing.$v5_s udA

• rr.lp : In this case I inlined one more variable, and lambdapi succeeds on this one.

I would have expected lambdapi to succeed on all of those, or at least to have the same behaviour.

$ lambdapi --version
30b1f60e

Remark: with the current master version of LP (commit 405c9fe3), I get the same behavior for all these files (and no performance issue):

[/home/blanqui/src/lambdapi/ett-in-lambdapi/ETT/failing.lp, 54:0-55:98] Some metavariables could not be solved: a proof must be given

Γ: TContext
T: ETT.Term
s: ETT.Sort
d1: ETT.der (τ_Γ Γ) T (ETT.tsort s) (ETT.snext s)
d2: ETT.der (τ_Γ Γ) T (ETT.tsort s) (ETT.snext s)
S: ITT.Sort ≔ τ_s s
--------------------------------------------------------------------------------
0. τ_s s ≡ S
1. τ_s s ≡ S

I will try again with the master version then. Still, even in this case, it is strange it fails to unify τ_s s ≡ S since it has as hypothesis S: ITT.Sort ≔ τ_s s.

This seems to be a performance problem in Bindlib at the following line in LP (call to bind_mvar): https://github.com/Deducteam/lambdapi/blob/4cdd818a7d4a8b214e5ac904a14e8b959ad0ec0a/src/tool/sr.ml#L151 So I don't know whether it can be fixed quickly...

Is it really the bind_mvar that never returns? Or is it the unbox?

I'm a bit sceptical that the problem comes from Bindlib: I think it is more likely that some (infinitely looping) computation can make its way into a boxed term (through a bad lifting somewhere), and it is unleashed on the call to unbox.

Moreover, the that is pointed to in the above message is only executed if !log_enabled is true. Does this mean that the problem only arises when some level of logging is enabled?

Ah, my mistake: this is not on master that I have this problem but on a working branch. Sorry.

@rlepigre Wait, I really have a problem with bind_mvar but this is a few lines later, not in a log_enabled section: https://github.com/fblanqui/lambdapi/blob/249b81fadc16b6c24b829d44290422ee57ea161a/src/tool/sr.ml#L171-L175 When running this branch on ram_out.lp with "debug +s;" added just before the last rule (with 6 let's in the rhs), "a" and "b" get printed but not "c".

@rlepigre In term.ml, you mentioned in a comment that _Meta_full is harmful for efficiency and the last rule of ram_out.lp contains many metavariables. Could this be an explanation? Or there is something wrong in rule scoping as this problem happens just after scoping. Your help is welcome!

@dwarfmaster If you want, you can try my branch "let" in https://github.com/fblanqui/lambdapi. It improves the handling of let's so that failing.lp does not fail anymore. But there is still a problem with ram_out.lp which seems related to scoping.

@rlepigre In term.ml, you mentioned in a comment that _Meta_full is harmful for efficiency and the last rule of ram_out.lp contains many metavariables. Could this be an explanation? Or there is something wrong in rule scoping as this problem happens just after scoping. Your help is welcome!

I don't think this could be the problem. The worst that could happen is that you end up with a free variables in the term.

I can try to have a look to the problem, but it would be nice if someone could first minimise the example (so that it fits in one file, and has the least number of definitions, of the least possible size).

I did try to minimize it, but for some reason I couldn't reproduce the explosion on small terms. Maybe I'll give it another go next week.

I did try to minimize it, but for some reason I couldn't reproduce the explosion on small terms. Maybe I'll give it another go next week.

That's be great! If at least the example is in a single file that would already help quite a bit. If you get around to doing that then could you also tell me what command dune exec -- ... I need to run in the repo to check the file without installing.

Thank you @rlepigre and @dwarfmaster for your help.

Hello @dwarfmaster . Did you succeed in putting every thing in a single file and minimize it?

I'm sorry, I haven't taken the time yet to do it. I'll try to do it before the end of july.