Proposal: Allow bottom-up prover to unify work variables more broadly (long-term) #77
Comments
|
Thanks for the detailed explanations. I will analyze the issue and return with some response. |
|
Thanks, and as always, thanks for your time. I did an experiment with a surprising result, which may be helpful to you. I expected that the problem was that "&W1" would only match a wff variable (which would be an understandable limitation). So I modified "Variables" to say: I then modified my "statement 3" to delete its justification & changed the first wff variable to a work variable, resulting in this: Even with this change, a bottom-up proof didn't find ax-2. |
|
In case it's relevant, it'd also be awesome if the tool could automatically replace work variables on unification. The review posted on May 27, 2023, at 10:17 AM, by Alexander van der Vekens on the Metamath mailing list (metamath@googlegroups.com) said:
I'm not sure this is related, but since it might be, I thought I'd note it. |
|
I analyzed this issue and yes indeed this is not a bug, this is a limitation of the mm-lamp unifier. This case is special because of the following reason. What it can do is: given two expressions exprA and exprB, it can find a substitution subsUni such that by applying subsUni to exprA we are obtaining exprB, i.e.: What the case described in this issue requires is to find a substitution subsBi such that (using similar notation): In my notation, Uni stands for "unidirectional" and Bi stands for "bidirectional". Let me demonstrate this on real expressions. exprA = A substitution subsBi (such that subsBi(exprA) = subsBi(exprB) ) exists, and it is as follows: But mm-lamp searches only for subsUni, such that subsUni(exprA) = exprB. Obviously it doesn't exist because length(exprB) < length(exprA). The workaround you've described in the guide, when you manually substitute I would like to share another possible solution. It uses more logical steps, but it demonstrates that such a "bidirectional" substitution may be achieved by two "unidirectional" substitutions. I recorded a video because it would be difficult to write (and probably to read) an explanation - (no sound) https://drive.google.com/file/d/1KIr0eOEmH4VoIHOHFhqXwBn08h-xGicV/view?usp=sharing To fix this issue, I plan to use the fact that a "bidirectional" substitution may be achieved by two "unidirectional" substitutions. Sorry if my explanation is difficult to understand because of unusual terminology. I am ready to answer clarifying questions if you have any. |
|
@expln - thanks for the explanation! I also appreciate you pointing out that it's possible to select two expressions to make replacements easier. For now, I think the solution is to document both approaches in the guide, given the current limitations in the unification algorithm. That said, I hope we don't stop there, see my next comment here... |
|
In the longer term, it'd be great if the unifier could handle this more general case, at least as an enable-able option. Unification has been studied to death, I bet there are some awesome algorithms that do much with decent performance. @digama0 - any suggestions on how to improve the metamath-lamp unification algorithm, given the discussion above? In particular, any pointers to some of the most relevant literature? |
|
There is a canonical algorithm for what @expln calls "bidirectional unification" (normally this is called "unification" and the unidirectional version is called "matching") which can be done purely recursively. There is a description on wikipedia, although I think the version I have implemented for MM1 is both more executable and simpler. I will summarize it:
|
|
@digama0 - thank you so much for your wonderfully clear & specific reply! Now things make much more sense. Alexander van der Vekens earlier complained of problems using metamath-lamp, and while I'm sure part of the problem was a lack of documentation, this difference is almost certainly part of the issue as well. I don't know how long it would take to implement full unification instead. I suspect that once it is, the tool would become much more capable AND would be easier to use for those who've used other tools like mmj2. Full unification might be slower than matching; I can see selecting matching vs. unification as a possible option in the search dialogue. That said, I suspect "full unification" would be the preferred setting, as that would greatly increase the likelihood of finding solutions. |
|
Thank you @digama0 for your detailed answer and especially for providing the summary of the algorithm. I would not understand it from the Rust code without that summary. In this notation
Sure, I already have one idea what I can do to handle this and other similar cases. But yeah, that's not a simple change, so it will need some time for implementation. Thank you for posting this issue with detailed description and explanations how it is handled in mmj2. Currently this is the only way how I can discover such non-trivial uses cases commonly used during creation of proofs. |
Yes, I would say that not doing parsing would be a big misstep for any MM proof assistant - you gain the ability to read some unusual metamath databases at the cost of not being able to reason about the proof at a high enough level to perform useful automation activities. |
|
If it's not too hard, I suggest leaving the old unifier as an option, at least for bottom-up search. If the bottom up prover is too powerful, it's hard to make simple examples in the guide to explain how to deal with cases where the automation doesn't work. So having ways to disable the automation can help. That said, I expect that the default should be full unification. |
|
FYI, I looked for some more resources about implementing Unification, especially in OCaml, Rescript, or JavaScript. My hope is that this would help in addition to the awesome info from Mario above. Unification is a really old well-studied problem; Robinson's unification algorithm dates from 1965. Here are some things I found that might be useful:
BTW, there's a nice video of the Curry-Howard Correspondence here (I found it while looking for examples): https://cs3110.github.io/textbook/chapters/adv/curry-howard.html |
|
Thanks David and Mario for the detailed explanations! The unification algorithm described by Mario looks really easy. I will analyze everything and return with my feedback. |
|
I totally understand if that's deferred, but I think this one is key. I think there are two parts to this:
|
|
Supporting full unification in the global substitution dialog is also an excellent idea. I will implement this. But I think it should be optional too. Currently I am thinking of the following design for the global substitution dialog :
|
|
My 2 cents: Users don't care what algorithm you are using (unless it fails to do its job), and unless there are situations where each beats out the other on some axis (quality or performance) there is no reason to surface this implementation detail to the user. If you want to keep the matching algorithm around, just put it behind a dev option in the code. Unification is very much a "behind the scenes" kind of algorithm. It is very important, but people just expect it to do its job and not pay much attention to it. |
|
It's hard to imagine a case where global substitution (the "substitution" icon) shouldn't use full unification. I can't think of any use cases. I like options, but only in the case where there's a reason to use it. It'll change my syl example in the tutorial, though. I'll probably have to wait to record that until we know what it looks like and I can adjust to match. |
|
It is not so clear for me. I can imagine many different substitutions depending on the algorithm and additional settings. However, I have not yet studied different unification algorithms mentioned in this issue. Probably it will become clearer to me after I study them. But for now, I see that results may be different, that's why I wrote about allowing users to select from two options. Assume we have the following symbols: Example 1 (not possible in set.mm due to ambiguity of the syntax in the example 1, but demonstrates my current understanding better): All the below algorithms use same two expressions:
(all other not mentioned in the substitution variables also get substituted with themselves, i.e.
Example 2 (should be possible in set.mm): All the below algorithms use same two expressions:
(all other not mentioned in the substitution variables also get substituted with themselves, i.e.
As you can see, found substitutions may be different depending on the algorithm used. Probably, under the conditions when syntax is unambiguous, as in set.mm, the full unification may replace matching. But I am trying to keep mm-lamp as general as possible (that's what inspires me), and in that case matching cannot be skipped. Please provide your thoughts and/or ask questions if any. |
I don't know what the distinction you are making between "local" and "global" variables is. Do you have an example? In mmj2 there are variables like To give this consistent terminology, I will call variables of the first two kinds "local constants" to emphasize that while these are variables from the perspective of the overall database, within the context of the proof they cannot be substituted and hence they are just as constant as actual constants like The third kind are what I would call "metavariables"; these are being instantiated by the prover and are what we actually want to be assigning in this algorithm. When you are doing proof search and want to apply a theorem, or a theorem is used in the worksheet, the first thing you do is pull the theorem statement and replace all the variables in the theorem's frame by fresh metavariables. For example if the theorem is Now, given your description my interpretation is that both We want to unify
Note that there is no branching in this algorithm. Only one result is produced. (The ambiguous grammar version of this algorithm does have branching.) There is no need to consider alternative unifications like What I just described is your unification (1), this is the mgu. (2) is also the mgu. (3) and (4) are not correct, they are unifiers but not most general unifiers. (Actually, (3) and (4) are not even proper simultaneous substitutions, since The key property of an mgu is that any unification must be a substitution instance of the mgu. If you assign
FWIW I think this should not be considered as part of the design at all. Ambiguous grammars are worth supporting only insofar as they can be supported without impacting the unambiguous grammar case, since that's what matters in practice. The algorithm I gave for unification does not work in the presence of grammar ambiguity. You can plausibly extend the algorithm to handle it by considering all possible parses (or something along those lines), but it is more complex and frankly exceeds my personal budget for complication for niche use cases. Getting a correct result here is tricky. This algorithm would look a lot more like a string diffing algorithm: you must match up all the constants and variables on the left and right, considering all possible interleavings of the constants. I will leave off a precise description of the algorithm, but in this case you would end up with the following results:
There are no additional results. Note that for larger expressions this list grows pretty fast, and most cases are not possible because of syntactic constraints. You probably want to use a bracket matching heuristic here. |
|
Whups, I forgot a third case where full unification would make sense, the "unify" icon (!). Correction, I think there are 3 cases where full unification makes sense (please let me know if I'm mistaken):
I'm guessing a single full unification implementation could be used in all of these cases. Agreed? What am I missing? |
|
Notes for me. Check this comments when the full unification is implemented: |
|
I am sorry for the late response. I needed some time to read, understand and think of different cases.
Unlike mmj2, mm-lamp doesn't have metavariables. Mm-lamp uses only usual variables and constants, and it can substitute usual variables with expressions if mm-lamp can prove the expression is of the same type as the variable. "Local" and "global" have similar meaning as in other programming languages. Internally, mm-lamp uses a context with three levels of nesting: Mm-lamp can emulate the mmj2 approach by allowing to replace only local variables. Currently, it doesn't do that. But most probably I will do that for the full unification to make it simple.
Mm-lamp does the same, but it adds usual local variables instead of the metavariables.
That was not a typo, mm-lamp allows not proper simultaneous substitutions. Here is a video demonstration https://drive.google.com/file/d/1VOjVKDHQ6S2X7Ylb-vG1-LZDpua094bO/view?usp=sharing I suppose there is a chance that not proper simultaneous substitutions result in invalid proofs, but I have not done a deep analysis of this. I implemented this only based on my intuition.
Thanks for the explanation. I plan to implement the recursive algorithm you've explained earlier. A single result is fine.
How does mmj2 unify more than 2 statements? I suppose it applies the unification algorithm to different pairs of statements. But then the result may depend on the order in which statements were selected for the unification. For example: stmt1: &A ~ &B If I first unify stmt1 with stmt2, then I get:
I am not sure. The full unification for the global substitution and in the bottom-up prover are more or less simple. But for the third case (when pressing the "unify" icon) it doesn't look as simple for me. Anyway, I will start implementing the first two cases and I will look into the third one later. |
One such scenario is when there are global essential statements (i.e. loaded from external sources). If such an improper simultaneous substitution tries to replace a variable in one or few global essential statements this may lead to errors because global essential statements are read-only, mm-lamp doesn't modify them during the global substitution. But this is a bug, and I will fix it by prohibiting such scenarios. |
…stitution #77 full unification in substitution
|
I implemented the full unification during global substitution (the "substitution" icon), and automatic merging of similar steps. It is available on dev https://expln.github.io/lamp/dev/index.html With these two new features the example from my first demo becomes more simple - https://drive.google.com/file/d/1YM3EAbJeWJglWITkEZ-FxCJpDgnbkzt1/view?usp=sharing Here are some explanations of decisions I made. Automatic merging of similar steps is optional. There is a global setting "Merge similar steps automatically". It is On by default. It can merge only in simple cases: 1) both similar steps must be P or G (not H); 2) one of them must have a non-empty justification and another must have an empty justification. Only in that case the one with empty justification will be removed and all references to it will be replaced with the label of the remaining step. If automatic merging is not possible then the manual merging is still available and works as before (the Merge icon). After I composed this comment I realised that I have to tweak the "auto merge" feature to not remove the G step. I will do this. The full unification during global substitution is also optional. But the choice remains for the next invocation of the substitution dialog. So if you always prefer to use the full unification you don't have to change anything each time. During implementation of the full unification algorithm I understood the importance of separating variables into "local constants" and metavariables. It was not so obvious to me from just reading the algorithm Mario explained. Because of that I introduced another new global setting "Prefix of metavariables in unification". By default, it is Another thing which I understood during implementation of the full unification algorithm is that maybe the name of the "Unify all" button (the Hub icon) is misleading. Initially I thought that unification means connecting all the steps by finding appropriate justifications. But now I understand that unification might mean the very specific process of finding the mgu. So maybe it worth renaming the "Unify all" button to something else? For example, "Justify all" with the tooltip "Justify all steps or justify selected provable bottom-up"? |
|
By the way, regarding metavariable prefixes, my personal preference is to use names like
The "unify" operation in mmj2 is indeed quite overloaded. I would describe it more generally as "make everything coherent and conformant": If steps are notated with an abbreviated syntax, use the canonical syntax; if steps are missing a formula, fill it in; if steps are missing a justification (and the settings are such that we should try to fill it in), fill it in if we can; if formulas have metavariables which can be nontrivially unified, assign and rewrite the metavariables; if all the steps are done, add the final proof block. |
|
I agree that
I don't want to change defaults to this because there are already videos and documentation with
Good to know. Thanks. |
How did that happen? Didn't you just implement this a few hours ago? In previous versions I only see regular variables, you yourself said that mm-lamp has no concept of metavariables (until now, I guess). I don't think visual similarity to mmj2 should be treated as a goal FWIW. |
|
I am not sure what you are asking about. But I have not changed anything since my announcement of the readiness of the full unification on dev. If you are asking about how that happened that the old setting works together with the new one, then I think this is just a coincidence. These settings are "independent" and "don't know each other". But the way how they are implemented produces this overall result. The setting The new setting "Prefix of metavariables in unification" is used only in the new unification algorithm. When I was implementing it, I faced a problem that it worked similar to matching - it was finding substitutions only in one direction. Then I noticed your explanation "all other equality checks should be performed modulo this assignment...". So I implemented "you should rewrite the whole state to replace occurrences of mv with e". This is the place where I had to distinguish "local constants" and metavariables. I decided to distinguish them by name and introduced this setting "Prefix of metavariables in unification". I cannot say that I introduced the concept of metavariables to the entire mm-lamp. The concept of metavariables is used only inside the new function which unifies two expressions. When that new unify() function finds a substitution, its work ends and the further processing is done by the old code. The old code takes this substitution, performs disjoint checks and type checks. When a user presses "Apply" button, then again the old code which knows nothing about metavariables applies the substitution as a simultaneous substitution of all the variables. The variables not shown in the substitution dialog are substituted with themselves (the same way as it worked prior this last change). For example, By saying "I don't want to change defaults" I didn't mean any big change. I meant that I plan to use the symbol |
Great, this is definitely a step forward. I tried it out. Starting from this state I can use "search" to add a use of ax-2, select the new step 4 and step 3, click on "substitute", and (after selecting unify mode) unify. I can then use a bottom-up proof on step 2 to complete the proof. So it definitely does work. I think there are many other opportunities to use the full unification algorithm. If I start over and search to add an instance of Perhaps more importantly, I can't edit a statement where the justification is known, and cause full unification. That's something many mmj2 users depend on. E.g., after starting over and adding an instance of ax-2, I can't edit the statement in the new step 4, to replace just one E.g., if I change the step 4 statement to this and then unify: I see this error: Whereas I expect it to produce: |
|
Thank you for testing the new feature.
Merge can only eliminate one of two identical statements. Unification of two statements is done how you described previously - select the new step 4 and step 3, click on "substitute"... If you mean that I can add such feature to the merge button, then I will think on that. But this causes overloading of buttons. The approach with "substitute" dialog is not much harder.
This could be achieved with the "substitute" dialog. Click on |
Yes, but IIUC that was the status quo before this feature. I would consider it an important case of unification that it can handle unifying (two variables replaced) or (replacing |
|
I think mm-lamp is already able to handle all these cases. However, it does it in a bit different way. Could you please verify if the below sequence of steps is functionally equal to what you described?
You may use this link to load the state to use for the verification (the important part is to stop before bj-0, otherwise some statements will be incorrectly parsed by mm-lamp) Here are screenshots showing how I reproduced all the tree cases you described: two variables replaced: replacing &W4 with &W3 and &W3 with ph, thus unifying both to ph:
|
|
Yes, that is what I mean. The main difference is that mmj2 would infer the "unify what" field from the theorem label, by replacing all the variables in the theorem statement by fresh metavariables. More generally, I think there is much to like about the way in which unification can be used as a zero-configuration tool. In mmj2, it's literally just one "do everything" button that users are quickly trained to press frequently. The dialog here would require two copy pastes, an edit, and three button presses (to open the dialog, press "find substitution" and then "apply") instead of an edit and a key command "unify all". |
Yes, in mm-lamp one additional step is required - adding an assertion to the editor by clicking the "Search" button. I am not trying to replace mmj2 by mm-lamp or to compete with it :) But I will try to do such kind of actions more effortless in mm-lamp. Thanks for the feedback! |
Yes, please. If I click on 2 statements and click on merge. I think users would expect the tool to do it if it's possible.
I agree with @digama0 - unification is a powerful general-purpose algorithm that can do a number of actions automatically, and I'd really like to see it used so that a single change in one place can cause automatic replacements like this. |
|
Hi Mario, Can you explain how MM1 builds syntax trees? Currently, I have performance problems with the algorithm I use in mm-lamp. My algorithm of building a syntax tree for an expression, for example
Transforming a proof into a syntax tree is a straightforward process because the proof is already a tree. Finding a proof is much more expensive process. I am using the same algorithm as in mm-lamp's bottom-up prover to find syntax proofs, which tries to apply all possible assertions to build a proof bottom-up. If needed I can provide more details on this algorithm, but I think this should be enough to understand why it is not very fast. This algorithm works sufficiently well for a small amount of statements. But now I want to build syntax trees for all assertions in set.mm, and that will be very slow. |
|
The process of building syntax trees from expressions is called parsing. There are a few ways you can do it, but the simplest is to put the syntax axioms into a trie and do a general backtracking algorithm. This can perform poorly on highly ambiguous grammars, but set.mm is unambiguous by design, and even though some backtracking is still needed because things might only be resolved after a while, it's not so bad in practice on set.mm. A trie node has the following data:
The top level of the trie is a map from typecodes to trie nodes. Every path through the tree represents a sequence of constants and variables, and during grammar initialization (which you can do either up front or as you encounter syntax axioms) you travel down the tree and add the syntax axiom. For example, starting from the empty tree: we can insert axiom If we insert Having prepared a data structure for parsing, now suppose we have a string of constants and variables we want to parse. Here's a rendering of the algorithm as lean code: inductive Node where
| mk (const : String → Option Node)
(var : List (String × Node))
(done : Option String)
def Trie := String → Option Node
def Node.empty : Node := ⟨fun _ => none, [], none⟩
inductive Sym where
| const (_ : String)
| var (_ : String)
inductive Expr where
| var (_ : String)
| app (_ : String) (_ : Array Expr)
-- Given a variable symbol like "v", returns ("setvar", "wv"),
-- i.e. the typecode and the variable hypothesis for the symbol
def getVarHyp : String → String × String := sorry
variable (p : Trie) (input : Array Sym) in
mutual
partial def parseC (q : Trie) (c : String) (pos : Nat) (args : Array Expr)
(k : Expr → Nat → Option Expr) : Option Expr :=
parsePT pos args k ((q c).getD .empty)
partial def parseV (pos : Nat)
(args : Array Expr) (k : Expr → Nat → Option Expr) :
List (String × Node) → Option Expr
| [] => none
| (s', q) :: vs =>
(parse s' pos fun v f' => parsePT f' (args.push v) k q)
<|> parseV pos args k vs
partial def parsePT (pos : Nat) (args : Array Expr)
(k : Expr → Nat → Option Expr) : Node → Option Expr
| ⟨cs, vs, d⟩ =>
(match input[pos]? with
| some (.const c) => parseC cs c (pos + 1) args k
| _ => none)
<|> parseV pos args k vs
<|> (d.bind fun a => k (.app a args) pos)
partial def parse (tc : String) (pos : Nat) (k : Expr → Nat → Option Expr) : Option Expr :=
(match input[pos]? with
| some (.var v) =>
let (tc', v') := getVarHyp v
if tc == tc' then k (.var v') (pos + 1) else none
| _ => none)
<|> parseC p tc pos #[] k
end
def parseFmla (s : String) (t : Trie) (input : Array Sym) : Option Expr :=
parse t input s 0 fun e pos => if pos == input.size then some e else noneDescribed in more detail:
Each individual case is fairly straightforward given the data structure; I can explain in more detail if required. This is also a transcription of the algorithm https://github.com/digama0/mm0/blob/master/mm0-hs/src/MM0/FromMM/Parser.hs#L575-L612 , although that one assumes lazy evaluation and so hopefully this one is more suitable to be adapted to your context. |
|
Thank you so much, Mario!
Thanks, I need some time to understand this and probably then I will ask additional questions. |
|
@digama0 - as always, thanks so much for your help!! |
I understood the algorithm. But I have not implemented it yet because it will take some time. I am wondering how much time could this algorithm take to parse all assertion statements in set.mm (only the resulting statements of axioms and theorems without hypotheses). Do you have any statistics from your implementation of how much time it takes to parse set.mm? I've done some improvements to my current algorithm in mm-lamp, so now it takes about 40 seconds to parse set.mm (previously it was about an hour). |
|
The lower bound of this parsing algorithm is definitely sub-second if done well. I doubt knowing that will be useful to you though. |
|
Metamath-lamp has gown into a very useful tool. I personally think this issue is now of the most important issues holding it back. While there is always room for better auto.ation, full unification would automate much (compared to the current state) and is 100% general. |
|
Having this would certainly simplify the tutorial! :-) |
|
I started working on full unification a few months ago. But it turned out to be much harder than I imagined. I needed to change the parts of the code which I don't want to change (at least for now). So, I postponed this activity. Currently I am implementing automation. My current results in automation are promising, so I want to release it first. After that, I will try to do another attempt to implement full unification. Probably I will use that new automation to implement the full unification. |
I have an idea - it'd be great if the unifier/bottom-up prover could unify on work variables more aggressively, at least optionally. This is an area where mmj2 can currently do more than metamath-lamp can.
I'm trying to re-prove
sylwhen loading set.mm and stopped afterax-3(that is, I only have the axioms in the context).I want to prove, using ax-2, the following step which was created earlier by a backwards application of ax-mp:
However, when I select this statement and unify (prove bottom-up), ax-2 doesn't appear as an option. That's true even if I allow "everything" by changing the Length restriction to "No", allow root statements at all levels, and enable everything else. If I try to enter
ax-2directly as a label, the backwards prover won't offer ax-2 as an option - it clearly thinks this statement cannot matchax-2.Follow this link to see the state. The full situation is also captured by this json:
{"srcs":[{"typ":"Web","fileName":"","url":"https://us.metamath.org/metamath/set.mm","readInstr":"StopAfter","label":"ax-3","resetNestingLevel":true,"allLabels":[]}],"descr":"Reprove syllogism (\"syl\"), using only axioms.","varsText":"var1 wff &W1","disjText":"","stmts":[{"label":"syl.1","typ":"e","cont":"|- ( ph -> ps )","jstfText":""},{"label":"syl.2","typ":"e","cont":"|- ( ps -> ch )","jstfText":""},{"label":"3","typ":"p","cont":"|- ( &W1 -> ( ( ph -> ps ) -> ( ph -> ch ) ) )","jstfText":""},{"label":"2","typ":"p","cont":"|- &W1","jstfText":""},{"label":"1","typ":"p","cont":"|- ( ( ph -> ps ) -> ( ph -> ch ) )","jstfText":"2 3 : ax-mp"},{"label":"syl","typ":"p","cont":"|- ( ph -> ch )","jstfText":"syl.1 1 : ax-mp"}]}The desired state is to be able to unify it with ax-2.
It also won't unify through merging. I can search for ax-2 and insert it, which is fine, and the instance has a bunch of metavariables as expected. But "merge" will not merge the original statement and the instance of ax-2, no matter what the order is.
I can replace the work variable
&W1with( ph -> ( ps -> ch ) )and apply "unify". Then bottom-up proving immediately unifies to that result.This is unfortunate. If the backwards prover could handle this case (even optionally) I bet it could automatically prove a lot more. In fact, if it noticed these matches, it could probably prove some things that mmj2 struggles with (because in mmj2 you can't really control the search of just one statement very well).
I tested on this, but I don't think the version matters: https://expln.github.io/lamp/dev/index.html
This is in contrast to mmj2, which can unify some work variables and lets you specify an assertion like
ax-2to be used on such a statement. A "before" and "after" should clarify things. For example, here's an example of "syllogism" where I just typed inax-2in the analogous situation (the "*" comments are hints to myself of where I'm going):In mmj2, after pressing control-U, I get a unification which helps me to keep going:
The text was updated successfully, but these errors were encountered: