Unexpected semantics of library(ordsets) for ordered _lists_ (not sets)

[stassa.p]

@peter.ludemann

Ah, that’s why you want the “undefined” behaviour to be defined. Given that the code is old, doesn’t seem to be buggy, and does what you want, documenting that it works for multi-sets seems reasonable – you’d want to add list_to_ord_multiset(List, MSet):-msort(List,MSet) (also ord_set_to_ord_multiset/2 for completeness); add some comments to the various predicates; and add some multi-set tests to tests/library/test_ordsets.pl.

That’s right! Sorry, I think I confused the point in my first comments, but then I was confused myself and still am unsure. I think those are good suggestions and I’ll see if I can find the time to follow them.

@anon37422618

Yeah somehow min, max from multisets is a lattice and min, sum
from multisets is a semiring. You can do a kind of fuzzy logic
Datalog construction all the time.

Heh. I am a category theory illiterate, sorry. What does it mean, in practical terms, that something is a semiring?

The connection to tabling sounds really interesting.

[jan]

@peter.ludemann

Given that the code is old, doesn’t seem to be buggy, and does what you want, documenting that it works for multi-sets seems reasonable

I am inclined to disagree. ordsets is a nice consistent library that could be optimized a lot further, even completely rewriting it using low-level primitives. I’d rather keep this option open. Then, multisets are probably best represented as a list of pairs Term-Count and supported by a proper library.

Of course, anyone can take the risk and use the ordsets library beyond its documentation. A simple assertion/1 call in a directive could be enough to warn that things changed.

[stassa.p]

@jan

I am inclined to disagree. ordsets is a nice consistent library that could be optimized a lot further, even completely rewriting it using low-level primitives. I’d rather keep this option open. Then, multisets are probably best represented as a list of pairs Term-Count and supported by a proper library.

What would change in that case? I still think (but I still need to check also) that the reason the library works both ways (on ordered lists with either unique elements or with duplicates) is its efficient implementation that exploits list ordering.

What I mean is that the natural way to walk through a pair of ordered lists efficiently is the same whether the lists have duplicates or not. “Natural” is a bit hard to define, but what I mean is that it would take extra code to force a predicate to only accept a list with unique elements (for example, you’d have to keep track of the last element seen and check it’s different than the current element).

I think this extra code is missing from the library because it is not necessary to ensure the library works correctly on lists with unique elements, and it’s hard to justify writing extra code to make an implementation less general, let alone to notice that it is (usually we check that the code does what its spec says, not that it doesn’t do a bit of extra stuff that doesn’t get in the way of the main purpose of the code).

On the other hand, I now seem to remember an older discussion, probably not on this incarnation of the mailing list, about representing multisets as key-value pairs, like you say and like @anon37422618 suggested. I wonder where I saw this before. It may even have been in a textbook. Craft of Prolog? Not sure.

@jan

Of course, anyone can take the risk and use the ordsets library beyond its documentation. A simple assertion/1 call in a directive could be enough to warn that things changed.

Well, if you’re saying the implementation can change then I guess the best thing for me is to keep a local copy of the library to make sure I don’t lose the functionality. It sucks a little, but at least I think I can distribute it with my code if I respect the license? Not that I’m currently planning to distribute the code, but I may put it on github at some point.

Anyway the main reason I’ve raised this is that I think it’s an interesting quirk of Prolog: sometimes you write a bit of code in the way that feels natural and is most efficient and it turns out to not only solve your immediate problem but also the generalisation of your immediate problem. Kind of like the way append/3 doesn’t just append lists but also splits them. I suppose that’s what you get for having a language where relations, rather than functions, are the first-class citizens. I’d like to be able to point to library(ordsets) as an example of this peculiarity of Prolog.

[stassa.p]

Thanks for taking the time to write that, but I don’t understand the terminology at all

[jan]

@stassa.p

Well, if you’re saying the implementation can change then I guess the best thing for me is to keep a local copy of the library to make sure I don’t lose the functionality

That is the ultimate safe way. Just relying on the current implementation is fairly safe, but not guaranteed.

@stassa.p

Kind of like the way append/3 doesn’t just append lists but also splits them

That is IMO a different thing. append/3 describes a relation. Here we are talking about how some piece of code acts on unanticipated input. Consider phrase/2,3. Once upon a time that could be used with non-lists and was used for general threaded variables occasionally. The introduction of strings in SWI-Prolog made unintended calls that would just fail too likely, so now phrase/2,3 does a type check. Likewise, the ordset library could be implemented differently, or static checking could be added that would validate that the input is indeed a valid ordset.

[stassa.p]

@jan

That is IMO a different thing. append/3 describes a relation. Here we are talking about how some piece of code acts on unanticipated input. Consider phrase/2,3. Once upon a time that could be used with non-lists and was used for general threaded variables occasionally. The introduction of strings in SWI-Prolog made unintended calls that would just fail too likely, so now phrase/2,3 does a type check. Likewise, the ordset library could be implemented differently, or static checking could be added that would validate that the input is indeed a valid ordset.

append/3 is not a great example, sorry. A better example is when I want to add or subtract a number to or from another. One way to do that is to write something like:

% Version 1
add_or_subtract(+,X,Y,Z):-
  Z is X + Y.
add_or_subtract(-,X,Y,Z):-
  Z is X - Y.

But I can also do it like this:

% Version 2
add_or_subtract(S,X,Y,Z):-
  Op =.. [S,X,Y]
  ,Z is Op.

And now, suddenly, my predicate works not only on addition and subtraction but also on every other arity-2 arithmetic function. Here, I didn’t make my code more efficient, but I made it shorter and more general, and it turns out to be in a sense maximally general. That’s the kind of quirk of Prolog I was trying to point to.

Now, if I don’t want that maximal generality I have to explicitly restrict S to be in {+,-}, for example like this:

% Version 3
add_or_subtract(S,X,Y,Z):-
  must_be(oneof([+,-]),S)
  ,Op =.. [S,X,Y]
  ,Z is Op.

But, now, what have I achieved and what was my motivation? I’ve made my predicate more special, by adding extra code, or in other words I’ve done extra work to take away its generality.

But, why? I’m sure there are use cases where restricting the value of S to {+,-} maybe be necessary. But there are also cases where it’s not. If I go with Version 2, I can add that predicate to a library and reuse it in both kinds of use cases.

Whenever I need strict type-checking, I can do it before calling add_or_subtract/4 and in fact, this type-checking can restrict the values of S to a different set of values than {+,-} For instance, for one project I might call add_or_subtract/4 like this:

... 
,must_be(oneof([+,-]),S)
,add_or_subtract(S,X,Y,Z)
, ... 

And for another I might call it like this:

... 
,must_be(oneof([arc,tan,cos]),S)
,add_or_subtract(S,X,Y,Z)
, ... 

At that point, the only problem that remains is that the predicate is misnamed: it should be named something like apply_arithmetic_function or something like that.

So my argument is that I can’t see the utility of modifying code to take away useful behaviour. If the motivation is to make the code agree with the documentation, it makes more sens to me (in this particular case and not as a general rule) to update the documentation to better describe the behaviour of the code, if we can agree that the code is not doing something that nobody wants it to do. If the code turns out to behave in a way that there are use cases for (and I think in this case it does) then I think it makes more sense to keep the code the way it is, or improve it without breaking its undocumented behaviour, and instead document that behaviour.

And, again, what’s the alternative, if one wants the multiset behaviour found in library(ordsets) like I do? Copy the library, and rename it. But… why duplicate code like that? Or write a new library from scratch, that will end up looking just like the old library. That’s not great either.

[stassa.p]

@anon37422618

Me neither, but the WAM Book author recently layed hands on it:

Thanks for the reference.

@anon37422618

The fancy thing is how type script infered types are annotated.

That’s …fancy indeed. Reminds me more of C# than javascript.

@anon37422618

BTW: The paper has some taxonomy graphs, can one trust them?

Honestly, I’ve no idea. I’ve kept well away from category theory. It reminds me a bit of collecting Pokemon. Too much work -and for what?

[stassa.p]

@anon37422618

But it doesn’t automatically translate to meaningfull error
messages, a little dilemma, like the common instantiation
error or the common type error list:

This hadn’t occurred to me but the use of =>/2 implies that the library is not as old as I thought, it must have been re-worked more recently. I guess I could have a look at the repo. I thought this was an ancient library that nobody would touch anymore, kind of like the Cobol code running on banks’ mainframes (don’t ask). I guess I was wrong.

[stassa.p]

I guess my knowledge stops at FOL. I have a very vague idea even about ZFC. You could argue I’m stuck somewhere in the 1920’s, between Hilbert and Gödel, in terms of my outlook on mathematics. If asked, I say that I just like to play it safe

[stassa.p]

That, I can work with. But what is the relation with e.g. semirings? FOL functions don’t really work like algebraic functions.

[stassa.p]

@anon37422618

∀x ∀y ∀z (x * (y + z) = x * y + x * y)

Well, that’s not FOL, or it’s not a WFF anyway. It’s Prolog I think, and it won’t be done automatically either in FOL or in Prolog. In Prolog it will fail because the two sides of the = don’t unify. In FOL, I don’t know how to interpret the equality symbol.

@anon37422618

* : D x D -> D

+ : D x D -> D

I think what this means is that * and + are mapped to functions over objects in the domain of discourse, as would be done by a pre-interpretation according to some authors? Is that right?

@anon37422618

But every day mathematics is more flexible.

Right. And Prolog, too. Prolog is not FOL

[stassa.p]

@anon37422618

Its not purely relational, it has function symbols. It is a well
formed formula WFF or sentence.

I think it depends on the author because in my sources that would not be a WFF, but I can see what you mean.

@anon37422618

@anon37422618

But distributivity is exactly an axiom about equality =.

So how translate such an axiom into Prolog? Try this:

?- ord_union([a,b,c], [c,d,e], X), 
   ord_union([a,b,c], [a,e,f], Y), 
   ord_intersection(X, Y, Z).
Z = [a, b, c, e].

?- ord_intersection([c,d,e], [a,e,f], S), 
   ord_union([a,b,c], S, T).
T = [a, b, c, e].

So its quite useful to shorten programs and queries.

So there’s a definition of “distributivity” in terms of set operations?

[peter.ludemann]

@stassa.p

the use of =>/2 implies that the library is not as old as I thought

The use of =>/2 was introduced 5 years ago: History for library/ordsets.pl - SWI-Prolog/swipl-devel · GitHub but the change was quite minor.

[jan]

@anon37422618

But it doesn’t automatically translate to meaningfull error
messages

Yes and no. A non-matching rule is a cheap and implicit message that typically translates to a domain, type or instantiation error. You have to get used to it but in most cases it is quite obvious what is wrong if you get such an exception. We might event try to be smart, look at the arguments and clauses and try to figure out why there is no match and come up with a better error message if we can.

[stassa.p]

@anon37422618

You don’t find it in propositional logic (zero order logic). Since zero
order has anyway no domain of discourse. But in predicate logic
(first order logic) you find it:

"The next step is to define the atomic formulas.

1. If t1 and t2 are terms then t1=t2 is an atomic formula
2. If R is an n-ary predicate symbol, and t1,…,tn are terms,
   then R(t1,…,tn) is an atomic formula"

I mean my sources for FOL. As you say FOL with equality is not the same as FOL. The definition of t1=t2 above makes = a predicate symbol which is what I always expected of FOL with equality, but to be honest I’ve never really looked into that because it never seems to crop up in logic programming or inductive logic programming work.

To be honest I’m not sure why it is important to define new logics whose whole schtick is that they have a special definition of a predicate, or more. Like all the modal logics for example, AFAIU them. That kind of specialisation seems to only serve the interest of having a subject to publish papers on.

You’ll find I’m a bit hardcore with sticking to FOL though, perhaps not completely reasonably so. For example I have never seen the point of any work in logic starting with Church and beyond. All of that seems like unnecessary over-engineering to me, and while I sorta see the motivation, my head just hurts every time I try to get it around e.g. the labmda calculus, or temporal logic, or whatever, and I keep thinking “I don’t need all this special notation, I can just do that with higher-order predicate logic”.

[stassa.p]

@anon37422618

The difference between FOL with equality =, and standard Prolog
is that Prolog equality is not FOL equality. Because you
cannot write axioms about equality = in standard Prolog.

Yes! Unification is not equality. It’s really just a way to avoid grounding the entire Herbrand base of a predicate before a proof can be completed. In fact, it lets you postpone the grounding until the proof is complete. The alternative is … ASP. And while I’m fine with ASP, it’s got limitations that I wouldn’t want to see in Prolog (e.g. no lists or at least no natural notation for lists, although you can always hack in a sort of “list” representation).

Prolog always gets a bad rep for being inefficient with backtracking etc, but the grounding problem that has to be solved before executing an ASP problem is NP-complete. Oh and it doesn’t work with infinite Herbrand bases. I’m guessing that Robinson was well aware of that and was looking for a way to avoid the hassle.

EDIT: if I understand correctly the ASP “list” representation is as a set of dyadic atoms, where the first argument is an index and the second an element. So e.g. the list [a,b,c,d] becomes:

el(1,a).
el(2,b).
el(3,c).
el(4,d)

For a base-one list.

[stassa.p]

You know, I always forget the sources are on github and I can just look at them in my browser

[jan]

@anon37422618

But I didn’t win in a lottery. Also it would not always be that simple with (=>)/2 rules.

It doesn’t need to be perfect. We can figure out for each argument which rules match and if a head matches which guard does not succeed. From there you could create a much more detailed report on why the predicate has no matching rules. Next, there are cases where this argument generalizes quite easily to a type/domain/instantiation error. I find myself quite often forgetting that => rules can not bind values in the head. Now I get no rule matching. It would be quite easy to say that what is intended to be an output argument suffers from an instantiation error. So, the idea would be

• Figure out the most likely/minimal cause of mismatch
• Try to abstract this to a type/domain/instantiation error
• On failure, just describe the minimal mismatch.

The benefit is clear: no pollution of your code and usable error messages.

[jan]

@anon37422618

P.P.S.: Was using this, the if-then-else uses (->)/2, but an
if-then-else with (=>)/2 is also somehow conceivable.

That has been discussed when talking about => rules. It was never implemented. In part because of the now rather simple minded way => rules are implemented: they basically use normal unification and, after the head unification completes, it verifies that nothing is trailed, Using single-sided unification instructions would be more efficient, but also more complicated and adding more instructions tends to reduce performance (probably due to cache behaviour). Implementing => choice would be a lot easier using such instructions though.

@anon37422618

C = (<) ->

Use C == (<) -> for speed. If-then-else condition evaluation is optimized for conditions that use no stack space and have no side effects such as a (partial) unification. In that case we do not need a choicepoint and we can simply evaluate the condition and jump (or not).