How to write max_member/2 with =>

Help! Predicate
1

Looking at the new code for max_member/2:

max_member(Max, [H|T]) :-
    max_member_(T, H, Max).

max_member_([], Max0, Max) =>
    Max = Max0.
max_member_([H|T], Max0, Max) =>
    (   H @=< Max0
    ->  max_member_(T, Max0, Max)
    ;   max_member_(T, H, Max)
    ).

I’m wondering about writing it like this:

max_member_([], Max0, Max) =>
    Max = Max0.
max_member_([H|T], Max0, Max), H @=< Max0 =>
    max_member_(T, Max0, Max).
max_m_([H|T], _Max0, Max) =>
    max_member_(T, H, Max).

and if the two cases of [H|T] bother you:

max_member_([], Max0, Max) =>
    Max = Max0.
max_member__([H|T], Max0, Max) =>
    max_member__(H, T, Max0, Max).

max_member__(H, T, Max0, Max), H @=< Max0 =>
    max_member_(T, Max0, Max).
max_member__(H, T, _Max0, Max) =>
    max_member_(T, H, Max).

All of these raise an exception if they’re not given a proper list.

Also, how well does => play with lazy lists? (In the particular case of max_member/2, the older definition works with a lazy list, whereas the new definition throws an error.)

2 Likes
2

Correction: the old definition of max_member/2 does work with lazy lists; the new definition throws an error.
(I had a typo in my copy&paste of the old max_member/2 code)
(I’ve edited my previous post)

5 
:- use_module(library(lazy_lists)).

ll(State0, State1, Head) :-
    State0 =< 5,
    State1 is State0 + 1,
    Head is State0.

?- lazy_list(ll, 0, List), lazy_list_materialize(List).
List = [0, 1, 2, 3, 4, 5].

?- List = [1,2,3,4,5], subsumes_term([_|_], List).
List = [1, 2, 3, 4, 5].

?- lazy_list(ll, 0, List), subsumes_term([_|_], List).
false.

?- lazy_list(ll, 0, List), lazy_list_materialize(List), subsumes_term([_|_], List).
List = [0, 1, 2, 3, 4, 5].

So, the answer seems to be that subsumes_term/2 doesn’t work with attributed variables, at least not if unification would cause any variable in it to change its attribute value.

2 Likes
6

Very good. I like that. Ideally the double unwind of the [H|T] should be done using source-to-source translation by the compiler.

Thanks for that observation. That is surely an unintended modification. This requires some thought. Ideas?

1 Like
7

The interaction of attributed variables and Picat-style will require some thought. In the meantime, I’ve found a problem with uninstantiated variables and the new implementation of ord_union/2, which has me scratching my head (my code shouldn’t be trying to do ord_union/2 with variables; but it’s not clear to me why the new definition of ord_union/2 fails rather than throwing an error). Figuring this out will probably take me a few days. :clown_face:

2 Likes
8

As currently defined, max_member/2 still has surprises.

?- max_member(a, [X,Y]).
Y = a.

?- _ = Y-X, max_member(a, [X,Y]).
X = a.

The second query is there just to show that the “maximum member” of the list argument to max_member/2 is correctly determined based on the variable age, but by the time max_member/2 is done with the list, its maximum member is no longer a variable.

I am not sure what is the correct behavior here. The docs say, as is tradition:

True when Max is the largest member in the standard order of terms.

Which is technically true. But still, consider these three queries:

?- max_member(b, [a,b]).
true.

?- max_member(b, [X,Y]).
Y = b.

?- max_member(B, [X,Y]).
B = Y.

The first one correctly confirms that b is the largest atom in the list [a, b].

The last one correctly unifies B with the “youngest” variable in the list. (I faintly remember that there was discussion about a use case for this behavior?)

The middle one correctly finds the youngest, “max” variable in the list, but then unifies it with b. Before the unification, and after it, this element is the “max member” since unifying a variable with anything won’t make it compare “less than” any other variable (right?) But is there a reasonable use case for this behavior?

That has been revisited endless times, I know, but it still confuses me a bit. I know what happens but I still don’t know why would I use it like this on purpose.

9

This all looks very much like the long discussion on sort/2 we had here before. Output arguments (mode -) do their work as expected, but if you instantiate them this counts as unification after the core operation. Ordering of variables is not stable under unification. Thus, this is the same as

?- sort([X,Y], [z,a]).

producing an unsorted list.

You don’t. I also see no way to avoid this except for making standard order of terms undefined for terms for which the final order cannot yet be defined or adding constraints to ensure the derived relation remains valid. Prolog is not a logical language. Only some subsets are …

11

This vaguely reminds me of a key limitation of horn clauses.

In full first order logic you can specify an disjunctive in the head, to mean one or the other, without committing to any one – although, i am not sure about the details here.

So, the result might need to be something like this, leading to some kinds of case analyses when such a result is fed into further reasoning.

?- max_member(b, [X,Y]).
(X or Y) = b.

Edit:

Here is the early paper by Brachman and Levesque that discussed something link that:

image