On the semantic of `tfilter` from the reif pack

After seeing Markus Triska’s work, I started paying more and more attention to preserve the generality of my predicates, so that they can answer correctly the most general query. I’m hitting a minor inconvenience when I try to filter away the elements of the form foo(_) from a list.

Conventionally, I’d do something like the following:

%?- length(X, _), exclude(=(foo(_)), X, Y).
%@ X = Y, Y = [] ;
%@ X = [foo(_5574)],
%@ Y = [] ;
%@ X = [foo(_5574), foo(_5574)],
%@ Y = [] ;
%@ X = [foo(_5574), foo(_5574), foo(_5574)],
%@ Y = [] .
...

but this is isn’t correct in the most general query.
Instead if I do:

%?- length(X, _), tfilter(dif(foo(_)), X, Y).
%@ X = Y, Y = [] ;
%@ X = [foo(_7124)],
%@ Y = [] ;
%@ X = Y, Y = [_7998],
%@ dif(_7998, foo(_8034)) ;
%@ X = [foo(_7124), foo(_7124)],
%@ Y = [] ;
%@ X = [foo(_8022), _8026],
%@ Y = [_8026],
%@ dif(_8026, foo(_8022)) ;
%@ X = [_8016, foo(_8028)],
%@ Y = [_8016],
%@ dif(_8016, foo(_8028)) ;
%@ X = Y, Y = [_8170, _8176],
%@ dif(_8170, foo(_8218)),
%@ dif(_8176, foo(_8218)) ;
...

I get a correct general solution (tfilter is from Ulrich Neumerkel’s library, available at https://github.com/meditans/reif/ as a pack).

The problem is now with a more concrete query:

%?- tfilter(dif(foo(_)), [bar, foo(a)], Y).
%@ Y = [bar] ;
%@ Y = [bar, foo(a)].

I would expect only the first solution here! I understand why it happens, after all foo(a) could be different from foo(X), depending on X; what would be a query that filters the terms of the form foo(_) from a list, while retaining correctness in the most general query?

1 Like

Not sure how the dif constraint works with the anonymous var but:

?-tfilter(dif(foo(X)), [bar, foo(a)], Y).
%@ X = a,
%@ Y = [bar] ;
%@ Y = [bar, foo(a)],
%@ dif(X, a).
2 Likes

Thanks @sam.neaves, the behavior you’re mentioning is the one I posted above; I’ll rephrase my question so that it’s slightly clearer: what would be a query that only returns the Y = [bar] solution, when I call it with [bar, foo(a)], and is correct in the most general query?

What I want is filter out the terms of the form foo(_), that’s why I don’t want foo(a) in the solution.

I guess you need to have a helper predicate, functor_dif/3 that works as you wish for

?- functor_dif(foo(_),frog(_),true).
true.
?- functor_dif(foo(_),foo(_),false).
true.

I would of thought univ =.. is the way to go, but that will error with insufficiently instantiated vars.