Stream: math-comp users

Topic: Implementing alternative TC resolution in a plugin


view this post on Zulip Karl Palmskog (Jan 14 2022 at 13:12):

but in theory one could do a plugin that starts from scratch and implements a more reasonable algo but is not backwards-compat?

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2022 at 13:13):

personally I don't understand how the Lean algo could be sound in the context of Coq

view this post on Zulip Enrico Tassi (Jan 14 2022 at 18:16):

Karl Palmskog said:

but in theory one could do a plugin that starts from scratch and implements a more reasonable algo but is not backwards-compat?

For TC resolution is it on my roadmap, the plugin is called Elpi and will feature tabling (at the language level). TC instances are just clauses.

view this post on Zulip Enrico Tassi (Jan 14 2022 at 18:32):

Of course I've noidea if it will work in practice, but I will try. After all it is why I got into logic programming in the first place.

view this post on Zulip Paolo Giarrusso (Jan 14 2022 at 20:28):

Isn't elpi for metaprogramming? Do you want to pregenerate instances or what?

view this post on Zulip Paolo Giarrusso (Jan 14 2022 at 20:29):

@Karl Palmskog also outside of Lean people mostly say that tabling is very hard to implement correctly IIUC (at least I heard so from the miniKanren author), but please correct me if I'm wrong

view this post on Zulip Enrico Tassi (Jan 14 2022 at 21:23):

Paolo Giarrusso said:

Isn't elpi for metaprogramming? Do you want to pregenerate instances or what?

Originally, it was to re-implement the elaborator. Then it seemed useful to extend te system, so I pushed that aspect. But the in the drawer I still have that "dream". A recent paper about lean says that the elaborator is essentially a lambda Prolog interpreter... so I m not alone :-)

view this post on Zulip Enrico Tassi (Jan 14 2022 at 21:26):

About TC, I want to synthesise instances on the fly. Tabling is just an alternative to SLD (depth first search). I'm implementing SLG in the runtime of Elpi, which is the most "operational" alternative to SLD, but memoizes success and failure. Very tricky but also neat.

view this post on Zulip Enrico Tassi (Jan 14 2022 at 21:29):

Once I have that I'll try to hijack TC instance declarations and turn them into Elpi clause declarations, and TC resolution queries into Elpi queries... and see how it goes.

view this post on Zulip Karl Palmskog (Jan 14 2022 at 22:15):

hmm, so theoretically, Elpi might also be used as a Prolog interpreter on top of regular Coq inductive predicates? (Like what Yves is talking about in this interview, switching from logic programming to Coq and not losing the former: https://www.typetheoryforall.com/2021/02/27/5-The-History-Of-CoqArt-Yves-Bertot.html)

view this post on Zulip Karl Palmskog (Jan 14 2022 at 22:17):

the hint modes in TC are driving me nuts, but it would be orthogonally helpful if I could play around with my inductive Prop relations (e.g., for PL operational semantics)

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2022 at 22:35):

@Enrico Tassi how would you memoize with universe constraints around? my understanding would be that caching with pointer equality would miss almost 100% of the time

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2022 at 22:36):

the only alternative I can think of is to be unsound, which is not much better

view this post on Zulip Enrico Tassi (Jan 15 2022 at 06:54):

for constraints you need to abstract them out (genetalize them) in the cache. The inspiration for the internal api is TCHR. In general a goal is solved in its generalized form, the solution is also generalized, and a cache hit requires to specialize the solution. You "unify", not pointer eq.

view this post on Zulip Enrico Tassi (Jan 15 2022 at 06:58):

Karl Palmskog said:

hmm, so theoretically, Elpi might also be used as a Prolog interpreter on top of regular Coq inductive predicates? (Like what Yves is talking about in this interview, switching from logic programming to Coq and not losing the former: https://www.typetheoryforall.com/2021/02/27/5-The-History-Of-CoqArt-Yves-Bertot.html)

Yes you already can, this is what eauto does. For elpi you would need some work to turn the type of each constructor into a clause. You can do that in Elpi itself but is not trivial.

view this post on Zulip Enrico Tassi (Jan 15 2022 at 07:02):

This "compilation" gives you some freedom, you could add rules which fail if some paramer is flexible, or suspend, impelenting hint modes in some sense. When the tabling engine will be ready, you will get a opt in cache.

view this post on Zulip Enrico Tassi (Jan 15 2022 at 07:03):

It is no different to TC resolution with these looking glasses.

view this post on Zulip Enrico Tassi (Jan 15 2022 at 07:03):

Just replace TC instance with inductive type constructor.

view this post on Zulip Karl Palmskog (Jan 15 2022 at 23:30):

I don't think eauto is a serious replacement for a Prolog toplevel to search in Prop inductive types. One wants to be able to enumerate solutions and so on.

view this post on Zulip Karl Palmskog (Jan 15 2022 at 23:31):

I think I would strongly prefer an "Elpi Inductive Prop Prolog mode/toplevel" (where exactly inductive Props are clauses) over eauto

view this post on Zulip Karl Palmskog (Jan 15 2022 at 23:36):

I think there would be some interesting synergies with other ecosystem tools, e.g., combine with QuickChick and its generators and you probably get close to PLT Redex for playing around with PL-style reduction relations

view this post on Zulip Enrico Tassi (Jan 16 2022 at 09:11):

I see, nice pointer. I was thinking at the engine behind the scenes, the "UI" is clearly not adapted for this use case. Ill keep this in mind.

view this post on Zulip Karl Palmskog (Jan 16 2022 at 10:48):

the background is that I have spent a ton of time using Ott to specify long and tedious PL typing and reduction relations and exporting them to Coq. However, there isn't really any good way of validating those relations (e.g., testing with "real" data) unless I make everything decidable/computable, which is a pain.

view this post on Zulip Paolo Giarrusso (Jan 16 2022 at 11:37):

So a bit like Twelf basically (minus HOAS)?

view this post on Zulip Paolo Giarrusso (Jan 16 2022 at 11:38):

(not sure on the relation between lambda Prolog and ELF)

view this post on Zulip Karl Palmskog (Jan 16 2022 at 11:40):

does Twelf really give you any testing facilities? I thought it was only for metatheory proofs

view this post on Zulip Paolo Giarrusso (Jan 16 2022 at 12:08):

I recall using it (a tiny bit) to enumerate solutions etc, as in usual Prolog toplevels.

view this post on Zulip Paolo Giarrusso (Jan 16 2022 at 12:09):

I haven't seen "metalevel" programmatic access to solutions but I'm not sure if you want/need that.

view this post on Zulip Paolo Giarrusso (Jan 16 2022 at 12:12):

(At a quick google) https://www.cs.cmu.edu/~twelf/guide-1-4/twelf_5.html#SEC26 mentions Twelf's interactive top-level. Of course it's a bit barebones :sweat_smile: — I was comparing it more to the "Elpi Prolog toplevel" part than to PLT Redex.

view this post on Zulip Paolo Giarrusso (Jan 16 2022 at 12:13):

But _if_ your typing relation is in algorithmic style, this is intended to be good enough to typecheck/infer programs/types.

view this post on Zulip Enrico Tassi (Jan 16 2022 at 12:50):

Yes, and when tabled the relations may work even if they are not syntax directed (they are not trivially algorithmic).

view this post on Zulip Enrico Tassi (Jan 16 2022 at 12:52):

BTW even today you can run a prolog query in Coq via Elpi, but it stops at the first result. Or you can ask all results, which may be too many. So the UI is a bit too rough.

view this post on Zulip Karl Palmskog (Jan 16 2022 at 12:55):

well, if you ever want to work on UI side, would be happy to help, have been collecting lots of PL relation examples as part of Ott and elsewhere.

view this post on Zulip Karl Palmskog (Jan 16 2022 at 12:56):

for example, we have a complete static and dynamic/operational semantics for an OCaml fragment called OCaml Light

view this post on Zulip Karl Palmskog (Jan 16 2022 at 12:57):

(the metatheory proofs were done in HOL4, though, but based on the same Ott definitions)


Last updated: Feb 08 2023 at 08:02 UTC