Extending Unification 2

General
1

Hello everybody,
After doing some side projects, I encountered the same kind of problematic multiple times and I wanted to discuss with the community the topic.
Let me start with use-cases which I hope will explain the topic:

  1. Imprecise geometry

For a graphical grammar project, I needed to unify coordinates as long as their difference is smaller than an epsilon.
I managed to do it using clpBNR by using the following formula:

abs(A - B) =< Eps.

But what I really would have liked to write is this: A = B.
Although in this case, we still need to deal with Eps, maybe as a global config or as an implicit state.

  1. unit with aliases

With my recent units pack, I needed to implement the concept of unit aliases.
So for example, kilogram is an alias of the unit kilo(gram).
Dealing with aliases adds a lot of complexity in the code since I can’t use unification anymore.
Basically, I would want this to work kilogram = kilo(gram).

  1. probabilistic logic programming ?

I have never actually used probabilistic logic programming, but I believe it could be a relevant use case.
When doing A=B, it would automatically associate a probability to that unification.
If that probability turns out to be 0, then the unification fails.
If the probability is 1, then it is a classic unification.

What solution can we imagine facilitating these patterns ?

  1. the current status quo

A pure Prolog solution is to stop using unification and make helper predicate that wrap the new type of unification.
For example, wrapping the earlier clpBNR formula in a predicate like eps(Eps, A, B) and use it everywhere it is needed.
The cons of this method are that we loose unification and all its benefits:

  • syntactical clarity: A=B is a very clear and beautiful syntax
  • unification in the head of a clause
  • Argument indexing in the head of a clause
  1. constrained variables

One could image using only variables, and attach constrains to these variables and never instantiate them.
This allows us to “overload” unification with the attr_unify_hook and redefine the unification there.
Although it could work for my geometry use case where I already use constraints with clpBNR, it would be very annoying with the aliases in my unit library.

  1. generalize attr_unify_hook to any type of data

Imagine we could say that we want to customize unification for every term of the type unit(U).
Then, we could deal with aliases inside the hook.
Maybe even write a very fast unification function for optimization ?

Has anyone worked on something like this ?
What are your thought on this ?

This type of question was already discussed a bit in this thread

2 Likes
2

I saw people doing this:

:- op(700,xfx, ~=).

A ~= B :- abs(A - B) =< 1e-6.

It doesn’t change unification, but it gives an alternative to (=:=)/2:

?- pi ~= 3.14159.
false.

?- pi ~= 3.141592.
true.
1 Like
3

Unification is the fundamental mechanism underlying Prolog. Not only must the syntax be “very clear and beautiful”, the semantics must be (and currently is) equally clear. I don’t think you want to mess with that.

But you can define other forms of equivalence. Every Prolog also supports arithmetic equivalence (=:=) and term equivalence (==). @j4n_bur53 provides another example: approximate arithmetic equivalence. Presumably the units pack implements another for unit equivalence (i.e., alias). But I’m not sure why you would want to conflate these other forms of equivalence with unification - they don’t mean the same (“sin(0) = 0.0” is false).

You also suggest that modifying the unification semantics would permit new equivalence relations to be enforced in the head of a clause. If this had significant benefits, it probably would have already be done somehow for the existing equivalence relations supported in the system.

Just my 2¢.

2 Likes
4

Thank you, I quite like this operator :slight_smile:

@ridgeworks Of course, you are right.
One subtlety of my first post is that we could maybe change the type of unification based on the type/shape of data we want to compare ?
Something like operator overloading, but for unification ^^

I suppose we could use ~= as a customization point to implement different type of unification, based on shape of data given to it ?
In a sense, it is a bit similar to your work on customizing arithmetic function ?

5

I think you should call it comparison, not unification. Unification is a precise term that establishes a unified version of two terms, i.e., the two terms become equal.

Attributed variables are the only entry point for extending unification. In their “proper” use the attributes represent constraints on the instantiation that the variable is allowed to get and unification determines the intersection of the two involved constraints. This can result in failure (intersection is empty), a concrete value (one of them is a concrete value and it is allowed by the constraint or the intersection of two constraints allows for only one specific value) or both variables are aliased and have the intersection as new constraint.

Of course, attributed variables allow for some hacking :slight_smile: Even more so in systems that follow SICStus model of attributed variables which allows for not unifying the variables, i.e., ==/2 does not need to hold after the “unification”. SWI-Prolog’s model does not support that. It executes the unification and allows the hook to veto the unification or combine the attributes if the unified result is still a variable.

I guess you can implement unit handing using attributed variables. With a bit of macro expansion and some write hooking that could all look pretty neat. Like clpBNR, you can represent intervals/fuzziness as well.

1 Like
6

Yeah, I’m currently thinking about how to do a pure interface to unit.
As an example, let’s say we want to have a distance, time, speed relationship that can be applied with any units of distance, time and speed. I suppose it would look something like this ?

?- distance_time_speed(Distance, Time, Speed).
Distance = A * kind_of(length)[U1],
Time     = B * kind_of(time)[U2],
Speed    = C * kind_of(speed)[U3],
% where constraints
U3 = U1/U2
C = A/B

Was this what you thought about ?

7

I don’t know. I guess there are several steps

  • How do you create a variable with value and unit?
  • What can be unspecified? Seems you hint the value can and it seems you also have some notion of unit abstracting and specify that something is e.g., a length without specifying the exact unit.
  • How do you compute with these?
  • How do you print them?
  • How do you make the unit and value accessible as normal Prolog terms?
8

So this is the design of the original mp-units library which is based on the international standard of quantity (isq).
This standard defines hierarchy of quantities and how quantities can be converted to each other.
Then every unit is associated with a group of quantities (metre is a kind of length).
This is all quite complicated but it works really well in practice.

Anyway, thank you for all your questions, it will give me some directions when trying to implement something.

9

By the way, what did you have in mind when you wrote this ?

10

You notably want some comfortable way to create a variable with a value and unit. E.g., somehow you want to write 10*kg and you want this to create a variable with attributes. One way of doing that could be leverage SWI-Prolog’s functional syntax support to create turn

load :- add(10*kg).

into

load :- unit_var(Var, 10*kg), add(Var).

There is an undocumented hack for doing that by adding clauses to '$expand':function/2. See boot/expand.pl Alternatively, you can achieve similar results using term/goal expansion.

:- multifile '$expand':function/2.

'$expand':function(A*B, Module) :-
    <verify this is a something you want to turn into a function>

*(A,B,Var) :-
    <create attributed Var from A and B>

Eventually this should have a public documented interface …

11

Wow, thanks, I didn’t know this.
I’ll think about it for the next version of the library.

12

FYI, This (goal expansion) is the support mechanism used by library(arithmetic) and pack(arithmetic_types) to extend SWIP’s functional arithmetic.

13

The problem of extending unification to reals is this:
1.0 = 1.00000000000001 will fail. You can’t get past this.

So instead you need a new function properties like

% unify over terms involving 'real' numbers.  (actually float/rational/etc.)
really_unify(X, Y) :- 
    X == Y -> true
;  X ~= Y -> true
;   X = Y -> true.
;  X =..Xs, Y =..Ys, maplist(Xs, Ys, really_unify).

I would inject into this support for unit structures so really_unify(2.54*mm, inch) passes. OR I would write the code so whatever units I have are first reduced to a unique normal form for that unit. Then all numeric calculations don’t have to do a lot of multiplying of constants.