Jan Wielemaker schrieb:
> - Provide partial evaluation to deal with (in particular)
> meta-predicates based on call/N.
>
> Ultimately, I'd like the last option ...

I call my solutions "dirty" HOL, since I am using the same
variable one time abstracted in the body of a clause and one
time non-abstracted in the head of a clause. So as to make
the iterators also binders. I guess a "clean" HOL solution
would look more complex.

At the moment not a lot of bad things can happend if
abstracted terms are not too much swirled around. But
since the iterators are binders they influence the notion
of a free variable, and thus the use of copy_term and
the like.

The local-by-default semantics are here better off. But
for the global-by-default semantics I guess there are
some counter examples that break the copy_term and the
like. Thus it would eventually also break my (^)/2 even
without binder terms, since I am using the weak witness.

Did not yet have time to figure out the counter examples,
but I guess there should be some...

Bye