Stream: Elpi users & devs

Topic: Reasoning about λProlog programs

Karl Palmskog (Aug 04 2023 at 12:16):

this may be obvious or already discussed somewhere, but is it possible (and could it be useful) to reason about λProlog programs in Coq, before implementing them in Elpi/Coq-Elpi? The algorithm(s) for typeclass resolution presented at the Coq Workshop seemed really tricky to get right.

Enrico Tassi (Aug 04 2023 at 12:37):

I have a few answers, which I think are all a bit weird ;-)

• if you take "pure λProlog" then you could use Abella, or, as I would have done if I had unlimited time, have an Abella mode in Coq (as we have an Iris mode)
• if you have a TC resolution program, I think it may be better to try to devise static checkers (after all you don't have "the program", the user writes instance by instance). In some sense you get the program (and a semantics) only after translation to Elpi. Before (I mean in Coq) I don't know what "Instance" means other than "the black box will use it".
• I've the impressions that what matters the most are "non functional" properties, like how long does it takes to fail in the worst case, which are not exactly easy to reason about. Maybe if @Davide F implements tabling (memoization) in the runtime of Elpi, some of these will become true for free, like no-loop, no-repetition.

The TC solver is an automatic prover and we check the output via Coq. We have (even formal) proofs about the calculus behind, say, E-prover. Would it make sense to prove that the code is OK? We have similar results for SLD or SLG (tabling) main loops. IMO we want to tell the user, statically, that his program will (always) loop in SLD or (always) fail in SLG, for example. Maybe this is what you had in mind, after all. But proving that the "compiler" @Davide F is "correct" is not so clear to me...

Karl Palmskog (Aug 04 2023 at 12:42):

Thanks. I meant both giving users static guarantees and proving algorithms for problems like typeclass resolution correct/fast in an abstract setting, divorced from Coq itself (but possibly inside Coq)

Paolo Giarrusso (Aug 04 2023 at 12:59):

In some sense you get the program (and a semantics) only after translation to Elpi.

Given unlimited time, one could still reason about the meta-program — compilation to elpi + elpi execution should be sound relative to a direct semantics — IF you have a simple enough semantics that the extra confidence is worthwhile.

Paolo Giarrusso (Aug 04 2023 at 13:08):

intuitively, any direct semantics should be a bit clearer than one involving a translation, but from outside I'd fear, with low confidence, the ratio between confidence gain and proof effort might be somewhat low?

Enrico Tassi (Aug 04 2023 at 21:02):

My problem in verifying the compilation is that one needs the semantics for the source language (Coq's Instance commands and TC solver) and the target one (Elpi's clauses, and the resolution strategy, e.g. depth-first aka SLD).

But I really don't know how to describe the semantics of Coq's TC search. Intuitively it is DFS, but it is really implemented calling apply, which uses the Coq's (legacy) unifier. I don't have a spec for that to begin with, while on the other end unification in Elpi is very very close to pattern-fragment, which one could define formally.

Davide and I are still discovering corner cases of the current TC engine, and sometimes we emulate it, sometimes we say it is wrong and we do differently. So even if we had the two semantics, it would not be the goal to be 100% faithful.

Gaëtan Gilbert (Aug 04 2023 at 21:04):

are you writing down somewhere the corner cases?

Enrico Tassi (Aug 04 2023 at 21:05):

At the same time having a semantics for the target language, and implement some static checks, is IMO very important. Actually, it was my starting point: I wanted to do static checking of TC "programs", and Dale convinced me I needed a language to express the whole business, and that turned out to be a dialect of lambdaProlog.

Enrico Tassi (Aug 04 2023 at 21:21):

Gaëtan Gilbert said:

are you writing down somewhere the corner cases?

I have notes, and they will end up in Davide's master report.

I can mention that the order is which goals are tackled depends on the caller, eg apply and rewrite (setoids) give goals in different order (one of the two does them in a clearly wrong order, as if the objective was maximizing backtracking).
Another thing which I believe Davide explained at the Coq workshop is that input/output modes are used to block the resolution of an ill-moded goal, but not to pick an order of goals which makes the i/o flow correct (or warn the user the order of premises is incompatible with the modes he is using).
The "cost" of an instance is, if I remember correctly, very complex to compute, at the point that we gave up trying to do exactly what Coq does (I thought it was the number of premises, but not quite).

Last updated: Oct 13 2024 at 01:02 UTC