Hi Saveliy, The current implementation not only performs matches (that it, unifications), but also allows you to capture the unification results in new variables, which can later be reused.
One of the reason I thought about a scripting language is that I wanted the core (the language interpreter) to be database agnostic, while the script themselves could be tailored to a database. But that might also be realized with a multilayered library (for example, one specific library using services from another, agnostic, library). A scripting language also has the advantage that it can be used as an external, without the need to e.g. recompile for each use. In the end, the language in which I specify how the tactics are used, can also be used for writing the tactics themselves. Any such tactics language should definitely allow one to implement operations as developing or simplifying formulas. That's valid for first and second order logic formulas, but also for algebraic formulas in the complex numbers, and the abstract level of generic algebraic structures like groups, rings and fields. Working on numerical expressions, performing long additions and multiplications, or for example connecting to an SMT solver, might require the ability to use some custom code. Maybe I'll have another go at implementing the tactics directly in an (existing) programming language rather than designing a scripting language, and see where this leads me. I'd probably use metamath-knife as a basis for that. _ Thierry On 17/12/2023 18:00, savask wrote:
Thierry, that's a cool project, I had no idea it exists. I took a brief look at the syntax and the currently implemented tactics. The "equality" tactic looks very useful, others are a bit too technical for me to understand. Correct me if I'm wrong, but it should be possible to write a tactic for expanding polynomial expressions, and maybe to port Mario's tactic for long addition and multiplication. I agree that one would need a more powerful language to implement some of the more interesting tactics. The "improve" tactic from metamath exe seems as one example. I'm not sure if it's beneficial to come up with your own scripting language for tactics, but if I were to use a library to write a tactic, I would certainly prefer to have functions from your language like matching patterns etc.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fc7bfcd1-4915-4103-8bae-41991a574bcf%40gmx.net.
