Unification between two symbolic expressions involves finding substitutions for variables (if any) in the expressions such that the expressions match after applying the substitutions. This is a powerful idea and is quite common in logic programming languages such as Prolog.
Interestingly, “newLisp” has a buil-in function called “unify” that can be used for unifying two expressions. In this article, let us go over several examples of this function.
Let us start with a simple case involving atomic elements:
Unifying “atomic” expressions
The “unify” function returns a “bindings” list, that is, a list of possible substitutions for the variables, if any. If the two expressions cannot be unified, it returns nil.
In the above case, there is a match only when the two expressions are identical. Since there are no variables in the expressions, if the match is successful, an empty list is returned.
It gets interesting when we introduce one or more variables in the expressions. Variables start with an uppercase letter in order to distinguish them from other elements of the expression.
Expressions with Variables
In the first case above, the variable “X” can be directly unified with the literal “Hi”. The third case shows that we can have variables in both expressions. The next four cases involve only variables, no literals. The reason the last case fails is because of mismatch between the number of elements in each expression.
We can use the special symbol “_” as a variable to match any single element, but it does not get bound to what it matches. See the following examples:
Using Underscore
As you can guess, the last two expressions fail because of mismatch in the number of elements.
The “unify” function optionally takes a third parameter – a binding list. This is used as needed when unifying the first two expressions.
Passing an Optional Bindings List
If the binding list includes variables other than those present in the first two expressions, then those are also included in the final list of bindings:
Extra Variables in the Bindings List
Here are some examples with “_” in the binding list (not a common scenario):
Bindings List Contains “_”
The first fails because of inconsistent bindings. When the first two arguments unify, the bindings will be ‘((A 1) (B 2)). However, the third parameter forces ‘(A 10), which is different from ‘(A 1). This cannot be true and hence the unification fails.
The remaining cases use “_” and hence there is no inconsistency. In the last case, the extra binding ‘(C _) is ignored because the variable “C” does not occur in the first two expressions and “_” is just a place holder with no concrete value.
In practice, the third argument is often another “unify” expression, in which case, its result will be used as the binding list for the main “unify”.
Nested “unify”
Do you see why the second case fails? It forces “P” and “Y” to take different bindings (due to the nested “unify”), and this cannot satisfy the unification of the first two expressions.
I hope the functionality of “unify” in “newLisp” is reasonably clear from the discussion so far. Do check it out when you get time.
Have a wonderful Thanksgiving weekend!
Recent Comments