Anybody got a short Prolog program for computing terms that are alpha variants? i.e. identical up to the choice of variable names. That is by uniformly renaming variables the two terms can be made identical.

Mark

variant(C, D) :- \+ \+ (numbervars(C, 0, _), numbervars(D, 0, _), C == D).

Strangely numbervars/3 is not defined in the ISO core standard,
but the ISO core standard points to it, since it talks about
writing '$VAR'(N) in a special way.

Mark Tarver schrieb am Donnerstag, 1. September 2022 um 02:21:09 UTC+2:
> Anybody got a short Prolog program for computing terms that are alpha variants? i.e. identical up to the choice of variable names. That is by uniformly renaming variables the two terms can be made identical.
>
> Mark

On Thursday, 1 September 2022 at 12:51:52 UTC+2, burs...@gmail.com wrote:
> Mark Tarver schrieb am Donnerstag, 1. September 2022 um 02:21:09 UTC+2:
> > Anybody got a short Prolog program for computing terms that are alpha
> > variants? i.e. identical up to the choice of variable names. That is by uniformly
> > renaming variables the two terms can be made identical.
>
> variant(C, D) :- \+ \+ (numbervars(C, 0, _), numbervars(D, 0, _), C == D).

Structural equivalence (=@=) does exactly that.

> Strangely numbervars/3 is not defined in the ISO core standard,

At least, term_variables/2 is ISO, you lucky one...

HTH,

Julio

I recently made a test, numbervars/3 bootstrapped
from term_variables/2. It turns out that it is slower.

For example Scryer Prolog does bootstrap numbervars/3
like that, but the classical implementation is faster,

since it doesn't need to create a list first. So this here is slow:

https://github.com/mthom/scryer-prolog/blob/master/src/lib/terms.pl#L5

I had to rethink the implementation for Dogelog Player,
and ended with the classical way to do it.

ju...@diegidio.name schrieb am Donnerstag, 1. September 2022 um 21:22:57 UTC+2:
> On Thursday, 1 September 2022 at 12:51:52 UTC+2, burs...@gmail.com wrote:
> > Mark Tarver schrieb am Donnerstag, 1. September 2022 um 02:21:09 UTC+2:
> > > Anybody got a short Prolog program for computing terms that are alpha
> > > variants? i.e. identical up to the choice of variable names. That is by uniformly
> > > renaming variables the two terms can be made identical.
> >
> > variant(C, D) :- \+ \+ (numbervars(C, 0, _), numbervars(D, 0, _), C == D).
> Structural equivalence (=@=) does exactly that.
> > Strangely numbervars/3 is not defined in the ISO core standard,
> At least, term_variables/2 is ISO, you lucky one...
>
> HTH,
>
> Julio

On Friday, 2 September 2022 at 00:44:50 UTC+2, burs...@gmail.com wrote:
> I recently made a test, numbervars/3 bootstrapped
> from term_variables/2. It turns out that it is slower.

I'm all for a RISC-like specification and a solid one, I rather find
the present situation a total mess, the standard we got to begin
with. That said, I can't in fact imagine a case where numbervars
is not just used for printing/serialization, where the performance
of the predicate makes no significant difference: can you?

> I had to rethink the implementation for Dogelog Player,
> and ended with the classical way to do it.

(By which I take you mean implemented natively/VM-level.)

Julio

A case where performance of numbervars/3 makes
a dent is this case. In case you bootstrap (=@=)/2
via numbervars/3:

Mark Tarver schrieb:
> Anybody got a short Prolog program for computing
terms that are alpha variants?

Mostowski Collapse schrieb:
> variant(C, D) :- \+ \+ (numbervars(C, 0, _),
numbervars(D, 0, _), C == D).

You can try yourself. Write some code that
needs (=@=)/2. Compare different versions
of it, implemented with different versions

of numbervars/2. Also numbervars/2 could
serve as a starting point to implement (=@=)/2,
by parallel unfolding the two numbervars/2

in the definition of variant/2.

Julio Di Egidio schrieb:
> On Friday, 2 September 2022 at 00:44:50 UTC+2, burs...@gmail.com wrote:
>> I recently made a test, numbervars/3 bootstrapped
>> from term_variables/2. It turns out that it is slower.
>
> I'm all for a RISC-like specification and a solid one, I rather find
> the present situation a total mess, the standard we got to begin
> with. That said, I can't in fact imagine a case where numbervars
> is not just used for printing/serialization, where the performance
> of the predicate makes no significant difference: can you?
>
>> I had to rethink the implementation for Dogelog Player,
>> and ended with the classical way to do it.
>
> (By which I take you mean implemented natively/VM-level.)
>
> Julio
>

Currently these Prolog system do not have (=@=)/2:
- Scryer Prolog
- Tau Prolog
- Jekejeke Prolog
- Dogelog Player
- Ciao Prolog
- What else?

But they have all have numbervars/3. You can make
some benchmarking now with a numbervars/3 bootstrapped
variant/2. For example using pocket unit resolution

theorem prover:

---------------- begin pocket unit resolution ----------------

next(C, S, S) :- member(D, S), variant(C, D), !.
next(C, S, T) :- apply(C, S, H), many(H, [C|S], T).

variant(C, D) :- \+ \+ (numbervars(C, 0, _),
numbervars(D, 0, _), C == D).

many([], S, S).
many([C|S], T, R) :- next(C, T, H), many(S, H, R).

apply(C, S, T) :-
findall(E, (member(D, S), resolvent(C, D, E)), T).

resolvent(C, D, _) :-
\+ C = [_], \+ D = [_], !, fail.
resolvent(C, D, E) :-
select(A, C, C2),
select(B, D, D2),
opposite(A, B),
append(C2, D2, E).

opposite(pos(A), neg(A)).
opposite(neg(A), pos(A)).

---------------- end pocket unit resolution ----------------

Mostowski Collapse schrieb:
> A case where performance of numbervars/3 makes
> a dent is this case. In case you bootstrap (=@=)/2
> via numbervars/3:
>
> Mark Tarver schrieb:
> > Anybody got a short Prolog program for computing
> terms that are alpha variants?
>
> Mostowski Collapse schrieb:
> > variant(C, D) :- \+ \+ (numbervars(C, 0, _),
> numbervars(D, 0, _), C == D).
>
> You can try yourself. Write some code that
> needs (=@=)/2. Compare different versions
> of it, implemented with different versions
>
> of numbervars/2. Also numbervars/2 could
> serve as a starting point to implement (=@=)/2,
> by parallel unfolding the two numbervars/2
>
> in the definition of variant/2.
>
> Julio Di Egidio schrieb:
>> On Friday, 2 September 2022 at 00:44:50 UTC+2, burs...@gmail.com wrote:
>>> I recently made a test, numbervars/3 bootstrapped
>>> from term_variables/2. It turns out that it is slower.
>>
>> I'm all for a RISC-like specification and a solid one, I rather find
>> the present situation a total mess, the standard we got to begin
>> with.  That said, I can't in fact imagine a case where numbervars
>> is not just used for printing/serialization, where the performance
>> of the predicate makes no significant difference: can you?
>>
>>> I had to rethink the implementation for Dogelog Player,
>>> and ended with the classical way to do it.
>>
>> (By which I take you mean implemented natively/VM-level.)
>>
>> Julio
>>
>

I tend to use numbervars/3 to implement variant/2, since
spinning it a step further, you can also use it to implement
a subsumption check. But I just noticed that you

can also implement variant, for two Prolog terms with
distinct variables, as follows. Right?

variant(C, D) :- \+ \+ (term_variables(C, L), term_variables(D, L), C == D).

But didn't try yet, could be slower or could be faster? here is some
benchmarking of the numbervars/2 implemented variant/2, also
a comparison to the SWI-Prolog (=@=)/2 builtin:

SWI-Prolog 8.5.14, =@=: 310 ms
SWI-Prolog 8.5.14, variant: 568 ms
Jekejeke Prolog 1.5.4, JDK 1.8: 982 ms
Trealla Prolog 2.1.16: 2'440 ms
Scryer Prolog 0.9.0: 97'752 ms

So Scryer Prolog , with some must_be/2 nonsense due to
Ulrich Neumerkel and Markus Triska really botched it. Made
Scryer Prolog totally unusable.

The test case was this:

% ?- findall(C, rule(C), S), many(S, [], T), member([], T).
% ...

% ?- findall(C, rule(C), S), time((between(1,75,_), many(S, [], _), fail; true)).
% ...

With this unit resolution problem, path search:

--------------------- path search problem --------------------------

rule([neg(edge(X,Y)),pos(path(X,Y))]).
rule([neg(path(X,Z)),neg(path(Z,Y)),pos(path(X,Y))]).

rule([pos(edge(1,2))]).
rule([pos(edge(2,3))]).
rule([pos(edge(3,1))]).
rule([pos(edge(3,4))]).

rule([neg(path(1,4))]).

--------------------- path search problem --------------------------

Mostowski Collapse schrieb am Freitag, 2. September 2022 um 22:14:42 UTC+2:
> Currently these Prolog system do not have (=@=)/2:
> - Scryer Prolog
> - Tau Prolog
> - Jekejeke Prolog
> - Dogelog Player
> - Ciao Prolog
> - What else?
>
> But they have all have numbervars/3. You can make
> some benchmarking now with a numbervars/3 bootstrapped
> variant/2. For example using pocket unit resolution
>
> theorem prover:
>
> ---------------- begin pocket unit resolution ----------------
>
> next(C, S, S) :- member(D, S), variant(C, D), !.
> next(C, S, T) :- apply(C, S, H), many(H, [C|S], T).
> variant(C, D) :- \+ \+ (numbervars(C, 0, _),
> numbervars(D, 0, _), C == D).
> many([], S, S).
> many([C|S], T, R) :- next(C, T, H), many(S, H, R).
>
> apply(C, S, T) :-
> findall(E, (member(D, S), resolvent(C, D, E)), T).
>
> resolvent(C, D, _) :-
> \+ C = [_], \+ D = [_], !, fail.
> resolvent(C, D, E) :-
> select(A, C, C2),
> select(B, D, D2),
> opposite(A, B),
> append(C2, D2, E).
>
> opposite(pos(A), neg(A)).
> opposite(neg(A), pos(A)).
>
> ---------------- end pocket unit resolution ----------------
>
> Mostowski Collapse schrieb:
> > A case where performance of numbervars/3 makes
> > a dent is this case. In case you bootstrap (=@=)/2
> > via numbervars/3:
> >
> > Mark Tarver schrieb:
> > > Anybody got a short Prolog program for computing
> > terms that are alpha variants?
> >
> > Mostowski Collapse schrieb:
> > > variant(C, D) :- \+ \+ (numbervars(C, 0, _),
> > numbervars(D, 0, _), C == D).
> >
> > You can try yourself. Write some code that
> > needs (=@=)/2. Compare different versions
> > of it, implemented with different versions
> >
> > of numbervars/2. Also numbervars/2 could
> > serve as a starting point to implement (=@=)/2,
> > by parallel unfolding the two numbervars/2
> >
> > in the definition of variant/2.
> >
> > Julio Di Egidio schrieb:
> >> On Friday, 2 September 2022 at 00:44:50 UTC+2, burs...@gmail.com wrote:
> >>> I recently made a test, numbervars/3 bootstrapped
> >>> from term_variables/2. It turns out that it is slower.
> >>
> >> I'm all for a RISC-like specification and a solid one, I rather find
> >> the present situation a total mess, the standard we got to begin
> >> with. That said, I can't in fact imagine a case where numbervars
> >> is not just used for printing/serialization, where the performance
> >> of the predicate makes no significant difference: can you?
> >>
> >>> I had to rethink the implementation for Dogelog Player,
> >>> and ended with the classical way to do it.
> >>
> >> (By which I take you mean implemented natively/VM-level.)
> >>
> >> Julio
> >>
> >

On Friday, 2 September 2022 at 22:05:07 UTC+2, burs...@gmail.com wrote:

> A case where performance of numbervars/3 makes
> a dent is this case. In case you bootstrap (=@=)/2
> via numbervars/3:

Well well, of course I wouldn't do that. But then again,
I am not the one who wrote the standard...

Have fun,

Julio

Sometimes you don't make any sense. You
write you wouldn't bootstrap (=@=)/2
from numbervars/2, you said "I wouldn't

do that" And then you say "I am not the
one who wrote the standard...".

Are you aware that a) "I wouldn't do that"
implies that you wouldn't need numbervars/2.
And that b) numbervars/2 is not in the standard.

There is no numbervars/2 in the standard!!!
So what does it have to do with the standard?
Sometimes you don't make any sense.

Julio Di Egidio schrieb:
> On Friday, 2 September 2022 at 22:05:07 UTC+2, burs...@gmail.com wrote:
>
>> A case where performance of numbervars/3 makes
>> a dent is this case. In case you bootstrap (=@=)/2
>> via numbervars/3:
>
> Well well, of course I wouldn't do that. But then again,
> I am not the one who wrote the standard...
>
> Have fun,
>
> Julio
>

Corr.: numbervars/2 --> numbervars/3

Maybe you are confused because you believe
numbervars/3 is part of the ISO core standard?
numbervars/3 is official declared an extension

by the ISO core standard. You find this footnote.
Maybe the usefullness of numbervars/3 is
wrongly judged, but the note and the predictae

index of the ISO core standard implies that it
would be a Prolog processor extension:

NOTE The current operators do not affect
output when there is a write-option numbervars (true).
This write-option is provided so that the built-in
predicates write/1 and writeq/1 (8.14.2) are
compatible with existing practice, but this
write-option is more useful when the processor
provides the built-in predicate numbervars/ 3 as an extension.
Page 59 - ISO/IEC 13211-1 First Edition 1995-06-01

So the ISO core standard is already RISC like, i.e.
reduced instruction set like. The ISO core standard
is basically already a Novacore, only nobody has

worked yet on defining all the extensions in a
systematic way, so that there would be some PEPs.
Or such work in the past has died out.

Mostowski Collapse schrieb am Samstag, 3. September 2022 um 18:03:16 UTC+2:
> Sometimes you don't make any sense. You
> write you wouldn't bootstrap (=@=)/2
> from numbervars/2, you said "I wouldn't
>
> do that" And then you say "I am not the
> one who wrote the standard...".
>
> Are you aware that a) "I wouldn't do that"
> implies that you wouldn't need numbervars/2.
> And that b) numbervars/2 is not in the standard.
>
> There is no numbervars/2 in the standard!!!
> So what does it have to do with the standard?
> Sometimes you don't make any sense.
>
> Julio Di Egidio schrieb:
> > On Friday, 2 September 2022 at 22:05:07 UTC+2, burs...@gmail.com wrote:
> >
> >> A case where performance of numbervars/3 makes
> >> a dent is this case. In case you bootstrap (=@=)/2
> >> via numbervars/3:
> >
> > Well well, of course I wouldn't do that. But then again,
> > I am not the one who wrote the standard...
> >
> > Have fun,
> >
> > Julio
> >

On Saturday, 3 September 2022 at 18:03:16 UTC+2, burs...@gmail.com wrote:

> Sometimes you don't make any sense.

I simply don't bother that you are an imbecille.

> So the ISO core standard is already RISC like

That is utter nonsense: as most of your drivel.

> There is no numbervars/2 in the standard!!!

There is no =@= either... idiot.

*Plonk*

Julio

> > So the ISO core standard is already RISC like
> That is utter nonsense: as most of your drivel.

What does the ISO core standard not make RISC?

ju...@diegidio.name schrieb am Samstag, 3. September 2022 um 19:57:05 UTC+2:
> On Saturday, 3 September 2022 at 18:03:16 UTC+2, burs...@gmail.com wrote:
>
> > Sometimes you don't make any sense.
> I simply don't bother that you are an imbecille.
> > So the ISO core standard is already RISC like
> That is utter nonsense: as most of your drivel.
> > There is no numbervars/2 in the standard!!!
> There is no =@= either... idiot.
>
> *Plonk*
>
> Julio

It doesn't have (=@=)/2 it doesn't have
numbervars/3, so it must be RISC, right?

LoL

Or what do you understand by RISC?
You can compare:

- ISO core standard, without the Annex,
which isn't very useful anyway:

ISO/IEC 13211-1:1995(E) = 124 Pages

- On the other hand the Ruby standard:

ISO/IEC 30170:2012(E) = 313 Pages

Mostowski Collapse schrieb am Samstag, 3. September 2022 um 21:22:12 UTC+2:
> > > So the ISO core standard is already RISC like
> > That is utter nonsense: as most of your drivel.
> What does the ISO core standard not make RISC?
> ju...@diegidio.name schrieb am Samstag, 3. September 2022 um 19:57:05 UTC+2:
> > On Saturday, 3 September 2022 at 18:03:16 UTC+2, burs...@gmail.com wrote:
> >
> > > Sometimes you don't make any sense.
> > I simply don't bother that you are an imbecille.
> > > So the ISO core standard is already RISC like
> > That is utter nonsense: as most of your drivel.
> > > There is no numbervars/2 in the standard!!!
> > There is no =@= either... idiot.
> >
> > *Plonk*
> >
> > Julio

Whats your RISC metric Culio?

*Plonk* per year?

Mostowski Collapse schrieb am Samstag, 3. September 2022 um 21:29:03 UTC+2:
> It doesn't have (=@=)/2 it doesn't have
> numbervars/3, so it must be RISC, right?
>
> LoL
>
> Or what do you understand by RISC?
> You can compare:
>
> - ISO core standard, without the Annex,
> which isn't very useful anyway:
>
> ISO/IEC 13211-1:1995(E) = 124 Pages
>
> - On the other hand the Ruby standard:
>
> ISO/IEC 30170:2012(E) = 313 Pages
> Mostowski Collapse schrieb am Samstag, 3. September 2022 um 21:22:12 UTC+2:
> > > > So the ISO core standard is already RISC like
> > > That is utter nonsense: as most of your drivel.
> > What does the ISO core standard not make RISC?
> > ju...@diegidio.name schrieb am Samstag, 3. September 2022 um 19:57:05 UTC+2:
> > > On Saturday, 3 September 2022 at 18:03:16 UTC+2, burs...@gmail.com wrote:
> > >
> > > > Sometimes you don't make any sense.
> > > I simply don't bother that you are an imbecille.
> > > > So the ISO core standard is already RISC like
> > > That is utter nonsense: as most of your drivel.
> > > > There is no numbervars/2 in the standard!!!
> > > There is no =@= either... idiot.
> > >
> > > *Plonk*
> > >
> > > Julio

Imagine a PEP that also defines a Native API for
certain dynamic host programming languages. A slim
and fast native API with very few wrappers, so

that you don't need to wrap DOM Objects, Integers,
etc.. unlike Tau Prolog which wraps everything. Sounds
futuristic? Here you got it`! I made a test via barell

architecture, to provide a public native API, numbervars2/3,
is implemented via the prototype public native API, whereas
numbervars/3 is the current local private implementation:

:- ensure_loaded('numbervars2.mjs').

?- numbervars(f(X,g(Y,X),Y), 0, N).
X = '$VAR'(0), Y = '$VAR'(1), N = 2.

?- numbervars2(f(X,g(Y,X),Y), 0, N).
X = '$VAR'(0), Y = '$VAR'(1), N = 2.

?- time((between(1,1000000,_), numbervars(f(X,g(Y,X),Y), 0, N),
fail; true)).
% Wall 1941 ms, gc 12 ms, 2060906 lips
true.

?- time((between(1,1000000,_), numbervars2(f(X,g(Y,X),Y), 0, N),
fail; true)).
% Wall 2062 ms, gc 12 ms, 1939970 lips
true.

http://www.xlog.ch/izytab/doclet/docs/18_live/20_novacore/example64/package.html

Dogelog Player is the avant-garde of logic programming!

LoL

Mostowski Collapse schrieb am Samstag, 3. September 2022 um 22:00:37 UTC+2:
> Whats your RISC metric Culio?
>
> *Plonk* per year?

Things that are not in the ISO core standard are more
likely to behave differently across Prolog systems?

GNU Prolog behaves already differently to SWI-Prolog in
numbervars/3. I find this discrepancy:

/* GNU Prolog 1.5.0 */
?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl.
_24
cannot display cyclic term for X

/* SWI-Prolog 9.1.16 */
?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl.
'$VAR'(0)
X = f(A, X),
A = A.

LoL

So what goodies are there in library(compat) as well?

Check this out:

/* SWI-Prolog 9.1.16 */
?- numlist(1,100000,A), numlist(1,100000,B),
time((between(1,1000,_), subsumes((f(_),X,X),(_,A,B)),
fail; true)), fail.
% 2,999 inferences, 2.375 CPU in 2.498 seconds (95% CPU, 1263 Lips)
false.

/* Dogelog Player 1.1.3 for Java (new!) */
?- numlist(1,100000,A), numlist(1,100000,B),
time((between(1,1000,_), subsumes((f(_),X,X),(_,A,B)),
fail; true)), fail.
% Zeit 2 ms, GC 0 ms, Lips 1550000, Uhr 18.10.2023 17:40
fail.

Dogelog Player for Java came out a few days ago. To get
subsumes/2 you have to use ensure_loaded(library(compat)).
I am using Richard O’Keefes algorithm from 1984 for subsumes/2.

Mild Shock schrieb am Mittwoch, 18. Oktober 2023 um 14:59:26 UTC+2:
> Things that are not in the ISO core standard are more
> likely to behave differently across Prolog systems?
>
> GNU Prolog behaves already differently to SWI-Prolog in
> numbervars/3. I find this discrepancy:
>
> /* GNU Prolog 1.5.0 */
> ?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl.
> _24
> cannot display cyclic term for X
>
> /* SWI-Prolog 9.1.16 */
> ?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl.
> '$VAR'(0)
> X = f(A, X),
> A = A.
>
> LoL

I am not extremly convinced by Richard O'Keefes approach
for subsumes/2. Especially how I have implemented it in
Dogelog Player, avoiding term_variables/2 all togtether!

Possibly I can produce some drastic test cases where it
doesn't run very well. On the other hand Jan W. is conceptually
promoting this bootstrapping of subsumes/2:

subsumes(General, Specific) :-
term_variables(Specific, SVars),
General = Specific,
term_variables(SVars, SVars).

The above cannot fast fail like Richard O'Keefes approach
can do. The further boostrapping is identical:

subsumes_term(General, Specific) :-
\+ \+ subsumes(General, Specific).

Mild Shock schrieb am Mittwoch, 18. Oktober 2023 um 17:56:52 UTC+2:
> So what goodies are there in library(compat) as well?
>
> Check this out:
>
> /* SWI-Prolog 9.1.16 */
> ?- numlist(1,100000,A), numlist(1,100000,B),
> time((between(1,1000,_), subsumes((f(_),X,X),(_,A,B)),
> fail; true)), fail.
> % 2,999 inferences, 2.375 CPU in 2.498 seconds (95% CPU, 1263 Lips)
> false.
>
> /* Dogelog Player 1.1.3 for Java (new!) */
> ?- numlist(1,100000,A), numlist(1,100000,B),
> time((between(1,1000,_), subsumes((f(_),X,X),(_,A,B)),
> fail; true)), fail.
> % Zeit 2 ms, GC 0 ms, Lips 1550000, Uhr 18.10.2023 17:40
> fail.
>
> Dogelog Player for Java came out a few days ago. To get
> subsumes/2 you have to use ensure_loaded(library(compat)).
> I am using Richard O’Keefes algorithm from 1984 for subsumes/2.
> Mild Shock schrieb am Mittwoch, 18. Oktober 2023 um 14:59:26 UTC+2:
> > Things that are not in the ISO core standard are more
> > likely to behave differently across Prolog systems?
> >
> > GNU Prolog behaves already differently to SWI-Prolog in
> > numbervars/3. I find this discrepancy:
> >
> > /* GNU Prolog 1.5.0 */
> > ?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl.
> > _24
> > cannot display cyclic term for X
> >
> > /* SWI-Prolog 9.1.16 */
> > ?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl.
> > '$VAR'(0)
> > X = f(A, X),
> > A = A.
> >
> > LoL

But Jan W. conceptualization can be used to develop
a funny variant/2 predicate. If we start from this here,
we will have two unifications, in each subsumes_term/2:

variant2(A,B) :-
subsumes_term(A,B),
subsumes_term(B,A).

We can also use only one unification:

equalizer(A, B) :-
term_variables(A, L),
term_variables(B, R),
A = B,
term_variables(L, L),
term_variables(R, R).

variant3(A, B) :-
\+ \+ equalizer(A, B).

Seems to work:

A B variant2(A,B) variant3(A,B)
f(X,g(Y,X),Y) f(Z,g(T,Z),T) true true
f(X,g(Y,X),Y) f(Z,g(Z,Z),T) false false
f(X,g(Y,X),X) f(Z,g(T,Z),T) false false
f(A,A,B) f(B,A,A) false false
X+Y Y+Z false false

Mild Shock schrieb am Donnerstag, 19. Oktober 2023 um 19:02:23 UTC+2:
> I am not extremly convinced by Richard O'Keefes approach
> for subsumes/2. Especially how I have implemented it in
> Dogelog Player, avoiding term_variables/2 all togtether!
>
> Possibly I can produce some drastic test cases where it
> doesn't run very well. On the other hand Jan W. is conceptually
> promoting this bootstrapping of subsumes/2:
>
> subsumes(General, Specific) :-
> term_variables(Specific, SVars),
> General = Specific,
> term_variables(SVars, SVars).
>
> The above cannot fast fail like Richard O'Keefes approach
> can do. The further boostrapping is identical:
>
> subsumes_term(General, Specific) :-
> \+ \+ subsumes(General, Specific).