Patrick Nicodemus (Mar 14 2023 at 04:23): Patrick Nicodemus (Mar 14 2023 at 04:23):https://github.com/theoremprover-museum/lambdaclam
https://www.semanticscholar.org/paper/System-Description%3A-Proof-Planning-in-Higher-Order-Richardson-Smaill/707283b85199bd61ce1e4eb5f0b686acfe79d393
This is really cool! I guess this is no longer maintained but if Elpi is going to be a big part of Coq in the long run it might be worth dusting this off and getting it back up and running.
system_description_lambda_clam.djvu
Does anybody have examples of theorem proving projects based on this?
Patrick Nicodemus (Mar 14 2023 at 04:25):I am very sympathetic to the idea of proof-planning. It seems like a sensible way to organize automated theorem proving, in theory.
Patrick Nicodemus (Mar 14 2023 at 04:32):I also have been ruminating on the idea that the user could write methods or tactics where one of the preconditions of the method would be given by a pattern to match on the hypotheses and/or goal.
The pattern could serve as a key in a discrimination tree, and at each deduction step, the methods whose pattern keys match the hypotheses or goal will be retrieved.
In this way the user could write very many methods each of which is specific to a narrow circumstance without bogging down proof search too much.
Patrick Nicodemus (Mar 14 2023 at 04:39):You can already do something like this in ordinary ltac with a long match goal statement.
But a match goal statement is not a data structure which can be added to progressively over time.
You can also add Hint Externs to an auto database but these only allow you to pattern match on the goal, not the hypotheses. I wish you could write Hint Externs with pattern matching on the goal!
Patrick Nicodemus (Mar 14 2023 at 05:46):https://drops.dagstuhl.de/opus/volltexte/2019/11118/pdf/LIPIcs-COSIT-2019-26.pdf
Wow, I didn't know inductive logic programming had been extended to higher order logic! This is all very new to me.
Enrico Tassi (Mar 14 2023 at 09:05):Patrick Nicodemus said:
I also have been ruminating on the idea that the user could write methods or tactics where one of the preconditions of the method would be given by a pattern to match on the hypotheses and/or goal.
The pattern could serve as a key in a discrimination tree, and at each deduction step, the methods whose pattern keys match the hypotheses or goal will be retrieved.
In this way the user could write very many methods each of which is specific to a narrow circumstance without bogging down proof search too much.
I'm not familiar with this line of research, but it actually looks pretty nice and for sure one could base it on Elpi.
Elpi is quite compatible with Teyjus, you can load .mod files directly, if you want to experiment with some piece of code from the first project you link.
Paolo Giarrusso (Mar 14 2023 at 11:58):(does elpi restrict to pattern Higher-order unification like Teyjus 2, or support the full thing like Teyjus 1?)
Enrico Tassi (Mar 14 2023 at 12:27):It does only pattern (like teyjus 2, and it does support automatic delay of problems outside the fragment, but it is off by default).
But it also lets you take over a term outside the fragment, e.g. extract the variable "cell" and arguments, and generate yourself a
solution for it, for example by abstracting a term over arbitrary terms (and not just names). You cannot take over unification globally, but you can implement your own unify predicate without reifying the notion of unification variables. I do it in a prototype here
Patrick Nicodemus (Mar 17 2023 at 23:03): Patrick Nicodemus (Mar 17 2023 at 23:03):The docs in the github repo build successfully. :D
Patrick Nicodemus (Mar 18 2023 at 05:10):@Enrico Tassi I installed Teyjus but I am having some problems. Is it possible that some of the Elpi builtin constants declared in coq-elpi/elpi-builtin.elpi might be visible to the Teyjus installation and prevent other code from compiling that shares the same constants? I got an error message saying
Patrick Nicodemus (Mar 18 2023 at 05:11):none(0,0) : Error : constant 'abs' declared with incompatible type 'int -> int'
See constant declaration with type '(osyn -> osyn) -> osyn -> osyn' at syntax.sig(20,5)
I think this is a strange error because nowhere in the Lambda Clam code can I find the constant abs of type (int -> int), and I don't know where to look for it because it says "none." I can find the constant abs of type '(osyn -> osyn) -> osyn -> osyn' in the Lambda Clam code in the file syntax.sig, but the only place I can find abs : int -> int is in coq-elpi/elpi-builtin.elpi
Enrico Tassi (Mar 18 2023 at 06:27):I need more context. What are you trying to do exactly? Running lambdaclam using elpi from the command line? Fom Coq? From teyjus?
Patrick Nicodemus (Mar 18 2023 at 11:30):Running the teyjus compiler tjcc on the command line on lambda clam files. Theoretically as far as I know, Coq or elpi do not come into the picture, but I do not know where the "abs : int -> int" is coming from if not that.
Enrico Tassi (Mar 18 2023 at 20:46):It can't be that, just uninstall elpi if you want to be sure.
Patrick Nicodemus (Mar 18 2023 at 21:30):My apologies, I see.
Patrick Nicodemus (Mar 18 2023 at 21:30):https://github.com/teyjus/teyjus/issues/90
Patrick Nicodemus (Mar 18 2023 at 21:31):The issue is that a few years ago Teyjus appropriated `abs' for the absolute value function.
Patrick Nicodemus (Mar 18 2023 at 21:31):So it can no longer be used to mean 'abstraction.'
I replaced all occurrences of "abs" with a new token "abst" , hopefully that fixes the conflict.
Patrick Nicodemus (Mar 19 2023 at 03:49):Teyjus has gone through some changes over the past 20 years. Currently it has a separate compiling and linking phase, while it appears that earlier it was just monolothic. I am hoping that the code still works as long as I can rewrite the makefiles appropriately for the current version of Teyjus.
Patrick Nicodemus (Mar 19 2023 at 03:49):I don't know Make though so anybody who wants to help, I would appreciate it.
Patrick Nicodemus (Mar 19 2023 at 03:51):I emailed Louise Dennis, the last academic who was in charge of this project, and she was responsive, but I don't expect her to want to work hard to rescuscitate long dead software.
Paolo Giarrusso (Mar 19 2023 at 07:08):Might be easier to build it against earlier Teyjus — a while ago I managed to install Teyjus 1
Enrico Tassi (Mar 19 2023 at 19:46):Hum, in Elpi the same symbol can have multiple types, so that problem would not be blocking.
Last updated: Apr 19 2024 at 04:02 UTC