Variable name ordering affects resulting MGU 'complexity'

[robertkleffner]

Lovely project, I am using it to confirm whether there is a bug in my own implementation of Boolean unification. Thank you!

I see some odd results depending on the ordering of variables in an equation. The equations are structurally the same, I just switched around which variable was which.

For instance, in both a = b || c and a = c || b, the following MGU is generated:

a --> b ∨ c
b --> b
c --> c

This is a pretty and comfortable-to-look-at MGU with a low intimidation factor.

When I input c = a || b however, I get the following MGU in the web portal:

a --> c ∧ (a ∨ ¬b)
b --> b ∧ c
c --> c

This one is much less intuitive despite being the same initial equation (at least for me) and seems like it could be a source of further complexity during unification-based type inference for Boolean types. The former MGU keeps the complexity of generated types lower.

[magnus-madsen]

@robertkleffner Hello Robert and welcome to our small community :)

I believe you are the only other person to have implemented Boolean Unification on GitHub! 🚀 (at least that was the case the last time I looked).

When you say web portal what specific site are we talking about? Do you mean the work bench?

As to your specific question:

• Yes, you are right.
• BU admits infinitely many MGUs (of different length and complexity).
• The fact that you get different MGUs is a byproduct of how SVE works (which you presumably already know).
• Presumably small MGUs are good.
• Other than that, its hard to define what a good MGU is. There is an aspect of software engineering and HCI to it.
• We are actively exploring (offline) several lines of attacks for computing small and good MGUs, but we still don't understand what it means to be "good".

In your example, you could argue that there are two problems: the asymmetry and the size of the substitution. How to deal with that, I don't know. We could of course use some uniform variable ordering, but that does not actually solve the problem. We can also reach for minimization (which we are doing), but minimal formulas are sometimes much harder to understand than say a formula in disjunctive normal form.

If you have any insights, we would be happy to hear!

[magnus-madsen]

Ah- I see now that the web portal is probably the workbench-- since this is the repository for that :)

I am curious, how did you find it?

[robertkleffner]

I found your papers a while back for the different ways you've been using Boolean-unifying types in PL type systems. Very creative! I found the workbench most recently by Googling 'Boolean unification online' and it was the third result for me. As soon as I saw the relation with the Flix project I knew it was exactly what I was looking for.

And indeed, by 'web portal' I meant the workbench. 2 AM when I wrote the initial message, hope everything was clear.

As far as insights, I don't have any groundbreaking suggestions. Perhaps there is a special case for equations like this, where the LHS is a single variable and the RHS does not contain the LHS in it's free variables. Something like:

X =~= EQN ---> [X -> simplify(EQN); (F -> F) ...]
    where X is a variable
          EQN is a boolean equation
          F ... are the variables in free(EQN)
          X not in free(EQN)
          [Ai -> EQNi; ...] is a substitution generated by unification

Of course I haven't done any deep formal thinking about this and whether it would cause problems. But if it doesn't, it seems like it could prevent some less intuitive inferred types in the cases of unification-based type inference.

[magnus-madsen]

I found your papers a while back for the different ways you've been using Boolean-unifying types in PL type systems. Very creative! I found the workbench most recently by Googling 'Boolean unification online' and it was the third result for me. As soon as I saw the relation with the Flix project I knew it was exactly what I was looking for.

Very cool! Feel free to link it somewhere. Maybe others will be able to find it and use it :)

As far as insights, I don't have any groundbreaking suggestions. Perhaps there is a special case for equations like this, where the LHS is a single variable and the RHS does not contain the LHS in it's free variables.

While I cannot say what technique we will end up with in Flix, we have been looking into Boolean minimization.

A few links that might be of interest:

https://research.swtch.com/boolean https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm

[robertkleffner]

Thank you for the links!

I have two quick updates wrt to this issue; the first is that the online workbench helped me solve a bug in my Boolean unification algorithm! Although it wasn't in unification per se, I had a simplification/minimization step implemented incorrectly.

The second is that I tried my idea above, and I can confirm it's promising but only really for the limited scenarios in which it applies. For instance, in the online workbench the equation c = a || b || d || e || f generates quite the complicated looking unifier, while my special-case detection just generates the substitution c --> a || b || d || e || f.

However, for most type inference scenarios I've run it on, it doesn't appear to result in much different types. The biggest value-add seemed to be that some intermediate unifiers were much smaller and thus didn't require as many minimization cycles.

Happy New Year!