Variables cannot unify with themselves

[CatsAreFluffy]

If I try to unify R with R (using unification and not matching), I get an error, even though they should trivially unify.

[expln]

Thanks for reporting this. I will take a look.

[expln]

Hi @CatsAreFluffy. I am sorry for the long delay in response.
Looks like this is not a bug. The Unification mode works with meta variables only. Check the Prefix of metavariables in unification setting on the Settings tab.

That symbol defines meta variables. By default, it is &. For example, R is not a meta variable, but &R is a meta variable.

You can create a local variable &R and try to unify it with itself. You should see Found substitutions: 1 valid, 0 invalid.. However, you will not see &R -> &R. This is a bit confusing, but this is done intentionally.

The way how mm-lamp is implemented, is that it includes all variables present in the editor to the list of found substitutions. It could be a big number of variables. Usually, only a few variables get substituted with something else, and others are substituted with itself. Mm-lamp shows only "useful" substitutions, where a variable is substituted with something different from itself. For example:

Currently, this distinction between meta variables and usual variables is used in the Unification mode of the Find substitutions feature only. In all other places all variables are treated equally. This is done because of how the unification algorithm works. In some sense, the unification algorithm divides all symbols into two groups: symbols not to replace and placeholders. The algorithm will try to find substitutions for placeholders only. The issue here is that, firstly, symbols not to replace include not only Metamath constants but also Metamath variables. Secondly, placeholders include Metamath variables only, but not all of them. So, Metamath variables can be in both symbols not to replace and placeholders. Therefore, the Prefix of metavariables in unification setting was introduced, and only variables prefixed with this prefix will be considered as placeholders in the unification algorithm. There is another issue with some interesting discussions related to this topic #77 (comment)

All of this might be too complicated. Even I didn't recognize this problem by its description. I had to dive into the code to find out that this is not a bug. Maybe it makes sense to add some hints to the Unification dialog. I will think on that.