Karl Palmskog (Jan 14 2022 at 13:12): 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?
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
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.
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.
Paolo Giarrusso (Jan 14 2022 at 20:28):Isn't elpi for metaprogramming? Do you want to pregenerate instances or what?
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
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 :-)
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.
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.
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)
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)
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
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
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.
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.
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.
Enrico Tassi (Jan 15 2022 at 07:03):It is no different to TC resolution with these looking glasses.
Enrico Tassi (Jan 15 2022 at 07:03):Just replace TC instance with inductive type constructor.
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.
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
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
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.
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.
Paolo Giarrusso (Jan 16 2022 at 11:37):So a bit like Twelf basically (minus HOAS)?
Paolo Giarrusso (Jan 16 2022 at 11:38):(not sure on the relation between lambda Prolog and ELF)
Karl Palmskog (Jan 16 2022 at 11:40):does Twelf really give you any testing facilities? I thought it was only for metatheory proofs
Paolo Giarrusso (Jan 16 2022 at 12:08):I recall using it (a tiny bit) to enumerate solutions etc, as in usual Prolog toplevels.
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.
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.
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.
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).
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.
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.
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
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