Generating scheme quines with prolog?

[cyclin...@gmail.com]

Hello

I'm very interested in logic programming and I was surprised when I learned minikanren (a prolog like language with occurs check and fair search) can produce quines by running the query (evalo q q) (find terms q which evaluate to themselves).

You can see the code for this here https://github.com/webyrd/quines/blob/master/q.scm and the paper here http://webyrd.net/quines/quines.pdf

As I said I was very surprised that this is possible. I assumed it was just the combination of occurs check and fair search - so I set out to rewrite the program in prolog with occurs check enabled and using tor for iterative deepening search. Also using dif/2 as =/=.

Here is my rewrite http://lpaste.net/7559243673339166720
It correctly evaluates the pre-written quine, it is able to fill in the blank for p1 but it cannot fill in the blank for p2 (it seems to infinite loop, while mk generates many quines in one second).

So I wanted to ask does anyone have any ideas why it is not possible to reproduce this in prolog?

[Jan Burse]

cyclin...@gmail.com schrieb:

> So I wanted to ask does anyone have any ideas why it is not possible to reproduce this in prolog?

symbolo(A) :- when(ground(A), (A=[]->true;atom(A))).

How about:

symbolo(A) :- when(nonvar(A), (A=[]->true;atom(A))).

Otherwise you might have A=f(_), and the constraint solver doesn't
detect that the constraint symbolo(A) is already violated.

Bye

[cycling fan]

Thank you!

This is a really nice improvement to the code.

And the question is still open!

[Markus Triska]

Jan Burse <janb...@fastmail.fm> writes:

> symbolo(A) :- when(ground(A), (A=[]->true;atom(A))).
>
> How about:
>
> symbolo(A) :- when(nonvar(A), (A=[]->true;atom(A))).

How about:

symbolo(A) :- freeze(A, atom(A)).

Unfortunately, in SWI-Prolog, [] is not an atom, so we need:

symbolo(A) :- freeze(A, (A=[]->true;atom(A))).

--
comp.lang.prolog FAQ: http://www.logic.at/prolog/faq/

[cycling fan]

this is a nice way to do it too! I've updated my code with that but it still doesn't generate quines yet - I guess we can rule out the implementation of symbolo/1 - there must be something else it needs.

Any ideas?

[Jan Burse]

cyclin...@gmail.com schrieb:
> Here is my rewritehttp://lpaste.net/7559243673339166720

If I compare with the q.scm code, I dont see not-in-envo (*)
realized in the Prolog code. This is to assure when for
example evaluating quote, that quote has not been redefined.

This could reduce further the search space. But this is only
a guess. There could be also other reasons that your seach
doesn't terminate.

Do you have some figures what is going on, lets say after a
minute or so? What was generated so far, how deep was the
search going? Or does it hang somewhere?

Bye

(*)
I find the same also in the paper, see
appendix A. An Extended Interpreter.

[cycling fan]

Thanks so much to everyone for your suggestions!

To run the code you can start the swipl repl and install the packages:

?- pack_install(tor).
?- pack_install(mutable_variables).

Sorry that I forgot to mention this before.

I got given a hint that made such a significant improvement I better post the updated code: http://lpaste.net/5489127788092850176

The main thing wrong was my use of dif/2 with clo/3, it was saying that the term wasn't this specific clo/3 term, instead of saying it wasn't any clo/3.

I have also added the things like not_in_envo and other small improvements.

It's now able to generate quines from a very very minimal template, but not quite completely yet. So I have more tinkering to do..

[cycling fan]

with just this change: evalo([lambda,X,B],clo(Env,X,B),Env) :- notspecialo(X),symbolo(X).

it is now able to generate quines from nothing!

?- search(id(evalo(Q,Q,[]))).
Q = [app, [lambda, _G8162, [cons, [quote, app], [cons, [var, _G8162], [cons, [cons, [quote, quote], [cons, [var, _G8162], [quote, []]]], [quote, []]]]]], [quote, [lambda, _G8162, [cons, [quote, app], [cons, [var, _G8162], [cons, [cons, [quote, quote], [cons, [var, _G8162], [quote, []]]], [quote, []]]]]]]],

Success!

[Markus Triska]

cycling fan <cyclin...@gmail.com> writes:

> Success!

I suppose you mean: Successo!

[j4n bur53]

Markus Triska schrieb:

> cycling fan <cyclin...@gmail.com> writes:
>
>> Success!
>
> I suppose you mean: Successo!
>

Next Challenge, use evalo and friends for:

Generating constraints to solve dependently-typed metavariables?
http://cs.stackexchange.com/questions/53555/generating-constraints-to-solve-dependently-typed-metavariables

Problem with my solution so far is that I currently don't
have a when/2 available in Jekejeke Prolog, as a result
the solution is a little crank. I am planning to introduce
a when/2 for the next release.

But SWI-Prolog could also show off here.

Bye

[web...@gmail.com]

> >> Success!
> >
> > I suppose you mean: Successo!

Successo indeed! Well done! I love this! :)

Would someone mind explaining to a non-Prologer like myself exactly what you had to do to extend/change Prolog to make this work?

Can you generate twines and thrines? How quickly can you generate quines, twines, thrines? I'm curious how the performance compares with that of miniKanren in Scheme. Your memory usage should be much better than with miniKanren's default interleaving search, I would think.

Of course, it is not really possible to compare the performance on quines when using different search strategies. I think the only fair comparison would be for those queries that have only finitely many queries, and for which the query is "refutationally complete" (that is, for which the query will terminate after producing a finite number of answers). Running the Scheme definition of 'append' inside the relational interpreter is one such example (and is shown in the PolyConf talk linked to below).

Dan Friedman and I implemented iterative deepening for miniKanren several years ago, but we didn't have much success running some of the larger queries. Our implementations weren't at all optimized, though. I wonder how well the arithmetic relations in chapters 7 and 8 of The Reasoned Schemer would run with your system.

> Next Challenge, use evalo and friends for:
>
> Generating constraints to solve dependently-typed metavariables?
> http://cs.stackexchange.com/questions/53555/generating-constraints-to-solve-dependently-typed-metavariables
>
> Problem with my solution so far is that I currently don't
> have a when/2 available in Jekejeke Prolog, as a result
> the solution is a little crank. I am planning to introduce
> a when/2 for the next release.
>
> But SWI-Prolog could also show off here.

If you can get this working, I'd love to back-port it to miniKanren! :)

Here's another challenge. We've been able to push the relational interpreter much further than the quine generating examples. I showed a number of the new examples in my PolyConf talk:

https://www.youtube.com/watch?v=eQL48qYDwp4

Here is the code for the talk:

https://github.com/webyrd/polyconf-2015

I'd *love* to see any of these examples using your Prolog interpreter!

Also, would you be interested in doing a Google Hangout to talk about this implementation, and perhaps play with some examples?

Thanks!

--Will

[Jan Burse]

web...@gmail.com schrieb:

> Can you generate twines and thrines? How quickly can you generate
> quines, twines, thrines? I'm curious how the performance compares
> with that of miniKanren in Scheme. Your memory usage should
> be much better than with miniKanren's default interleaving search,
> I would think.

If somebody has enough time on his hands and would add the
interleaving search to tor, we could compare 1-1. Maybe
fork the module tor and call it toro. :-)

The big advantage of iterative deepening is that you don't
need a unit clause store i.e. some tabling, since everything is
done with normal Prolog resolution, i.e. the stacks that are
usually used to implement a Prolog system.

An other option would be to go with explicit operators for
different search strategies, and introduce them also in Prolog.
Possibly there could be new implementation ways for example
using interactors, which are poping up for Prolog recently.

But according to this paper interleaving is a cludge, as long
as not some cost information is also incorporated in the
invokation of a predicate. See page 10 ff:
http://spivey.oriel.ox.ac.uk/~mike/silvija/seres_haskell99.pdf

Also when speeking of constraints, the quines solution uses
basically delayed goals, there is not much interaction between
the constraints, and last but not least there is no labeling
facility, which would apply further heuristics.

Maybe the interleaving is here the heuristics, but interleaving
doesn't seem to do what labeling does, namely labeling can
look at all variables so far in a model, and then try to
pick the best to continue search.

But it also begs the question whether for such examples as
the quine search really the labling view applies. Since the
interleaving search and also some of the domain rules are
productive in the sense that they create new variables.

I guess the practical applications could be less demanding
than the quines example, for example analysing a simple
WHILE program could work with a bounded number of variables.
So there would be less muddy waters.

[Jan Burse]

Jan Burse schrieb:

> Also when speeking of constraints, the quines solution uses
> basically delayed goals, there is not much interaction between
> the constraints, and last but not least there is no labeling
> facility, which would apply further heuristics.

By interaction between constraints I mean the following.
Assume in the course of solving a problem the following
happens:

?- ... when(C1, G1) ... when(C2, G2) ...

And both condition C1 and C2 are so far not satisfied.
Then the constraint store will have the following content:

when(C1, G1)
when(C2, G2)

There are constraint solver formalism where one can
posit further rules that allow recombination of constraints,
mostly to simplify them. So there could be a constraint
simplification rule that says:

(C1 & G1) & (C2 & G2) -> (C3 & G3)

The constraint solver would then remove the two constraints
and add a new constraint:

when(C1, G1) remove
when(C2, G2) remove
when(C3, G3) insert

So that when the simplification rule has been applied
the constraint solver and the program would
continue with:

when(C3, G3)

Most likely Kanren could do that, but the quest is to
define a logic language like Kanren itself is, that also
allows to define such rules, so that I don't have to pick
up scheme to do that.

Such a languages is for example CHR for Prolog.

Bye

[thecon...@gmail.com]

Hi!

I wrote a modified version that uses CHR for the constraints: http://lpaste.net/160468722731974656

I had to remove occurs check to get it to work with CHR, though it seems okay so far as I can still generate quines. I also made vars disjoint from the expressions and removed the app tag to try and speed things up.

I'm still new to prolog so if there's anything that can be fixed or improve I'd be happy to hear about it.

[Jan Burse]

Cool!

Just a side remark. Assume you have a web server,
and one thread finds a quine with id strategy
and another thread finds a thrine with ids strategy.

Can I use the tor library this way? Probably no.
The problem is the definition of the tor/2 predicate.
It reads:

G1 tor G2 :-
( b_getval(left,Left),
call(Left,G1)
; b_getval(right,Right),
call(Right,G2)
).

It uses a global variable, and not a thread local
variable. Also I am not sure whether call/2 is
a good solution. In my opinion hypothetical
reasoning would help.

For hypothetical reasoning we would first
define a thread local predicate tor/2:

:- thread_local tor/2.

And then when we start the search, from
within a thread, we can configure it via the
hypothetical reasoning operator (=>)/2:

search(...) :- ...
(tor(G1, G2) :- ...) => ...

Bye

P.S.: Further question, can CHR run in a thread?

thecon...@gmail.com schrieb:

[Jan Burse]

cyclin...@gmail.com schrieb:

Hi,

I gave it a try of the quince problem via DCG. The idea
is very simple, as a replacement for tor, I am using a DCG
definition of eval. There is a helper predicate step//0
which check the inference capacity:

step, [C] --> [D], {D > 0, C is D-1}.

The evaluation then goes as follows:

eval([quote,X], _, X) -->
{freeze(X, is_expr(X))}.
eval([cons,X,Y], E, [A|B]) -->
step,
eval(X, E, A),
eval(Y, E, B).
eval([lambda,X,B], E, [closure,X,B,E]) --> [].
eval([X,Y], E, R) -->
step,
{diff(X, quote)},
{sto(B)}, eval(X, E, [closure,Z,B,F]),
{sto(A)}, eval(Y, E, A),
eval(B, [Z-A|F], R).
eval(S, E, R) -->
{diff(S, [_|_])},
{freeze(E, lookup(S, E, R))}.

Conming from Jekejeke Prolog, the diff/1 equivalent
in SWI-Prolog is readily defined:

diff(X, Y) :- dif(X, Y).

I needed to find a sto/1 equivalent in SWI-Prolog,
and went with the following, which is an approximation,
since it is a little stronger than my sto/1:

sto(X) :- term_variables(X, L),
sto_vars(L).

sto_vars([X|Y]) :-
freeze(X, (acyclic_term(X), sto(X))),
sto_vars(Y).
sto_vars([]).

This sto/1 equivalent seems to work, at least I get:

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.16)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam

?- sto(X), X =f(X).
false.

?- sto(X), X=f(Y).
X = f(Y),
freeze(Y, (acyclic_term(Y), sto(Y))).

?- sto(X), X=f(Y), Y=g(X).
false.

Now if I try to find a quine, I get the following:

Jekejeke Prolog 2, Development Environment 1.1.2
(c) 1985-2016, XLOG Technologies GmbH, Switzerland

?- sto(Q), eval(Q, [], Q, [5], X).
Q = [[lambda,_A,[cons,_A,[cons,[cons,[quote,quote],
[cons,_A,[quote,[]]]],[quote,[]]]]],[quote,[lambda,_A,
[cons,_A,[cons,[cons,[quote,quote],[cons,_A,[quote,[]]]],
[quote,[]]]]]]],
X = [0],
diff(_A, [_B|_H]),
diff(_A, [_N|_V]),
freeze(_A, is_expr(_A)),
freeze(_A, is_expr(_A)),
freeze(_A, is_expr(_A))

When I do the same in SWI-Prolog, I get:

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.16)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam

?- sto(Q), eval(Q, [], Q, [5], X).
false.

Whats wrong?

P.S.: Source code is here, Jekejeke 1.1.2 is not yet out, sorry,
but still wonder why SWI is failing:

https://gist.github.com/jburse/c1e3c2051f1f724adcac

[Ulrich Neumerkel]

Jan Burse <janb...@fastmail.fm> writes:
>cyclin...@gmail.com schrieb:

>I needed to find a sto/1 equivalent in SWI-Prolog,
>and went with the following, which is an approximation,
>since it is a little stronger than my sto/1:
>
> sto(X) :- term_variables(X, L),
> sto_vars(L).
>
> sto_vars([X|Y]) :-
> freeze(X, (acyclic_term(X), sto(X))),
> sto_vars(Y).
> sto_vars([]).

?- X = s(X), sto(X).

succeeds, but obviously it should fail.

sto(X) :-
acyclic_term(X),
term_variables(X, Vs),
sto_vars(Vs).

sto_vars([]).
sto_vars([V|Vs]) :-
freeze(V, sto(V)),
sto_vars(Vs).

I suspect that this has worst case exponential runtime.
This is probably the worst case: With n functors you
get 2^n calls to acyclic_term/1.

?- sto(T0), T0 = T1+T1c, T1 = T1c, T1 = T2+T2c, T2 = T2c ...

A name like finite_term/1 might be preferable.

[j4n bur53]

Ulrich Neumerkel schrieb:

> ?- sto(T0), T0 = T1+T1c, T1 = T1c, T1 = T2+T2c, T2 = T2c ...

Not an example for exponential behaviour:

sto(T0)
After T0=T1+T1c: sto(T1) sto(T1c)
After T1=T1c: sto(T1c)
After T1=T2+T2c: sto(T2) sto(T2c)
After T2=T2c: sto(T2c)

At least in the current Jekejeke implementation (*),
since it uses ensure_hook/2, which adds the hook only
if necessary. So that each attribute variable has the
hook only once.

This leads also to the bit idea. A very light weight
form of sto/1 constraint. Each variable would have
this bit, and when it is set, the variable would act
upon instantiation, as if it were inside unify_with_occurs_check.

On the other hand when we use freeze/2 there could be
an explosion, since freeze/2 is missing interaction
between different suspended freeze/2 goals. freeze/2 is
blind to what it is delaying. There we might get
exponential behavior.

Bye

(*)
http://www.jekejeke.ch/idatab/doclet/blog/en/docs/15_min/02_reference/term/herbrand.html

[Ulrich Neumerkel]

Markus Triska <tri...@logic.at> writes:
>How about:
>
> symbolo(A) :- freeze(A, atom(A)).
>
>Unfortunately, in SWI-Prolog, [] is not an atom, so we need:
>
> symbolo(A) :- freeze(A, (A=[]->true;atom(A))).

Note that (A=[]->true;atom(A)) should rather read
(atom(A)->true;A==[]). In any case, this non-conforming
part will certainly be the source of many errors to come.

[cycling fan]

The step predicate is very interesting! Thank you for showing and nice to see that it worked with jekejeke!

[cycling fan]

It was not possible to generate twines...

?- search(id((dif(Q,P),(evalo(Q,P,[]),evalo(P,Q,[]))))).
[Thread 1] pl-prims.c:3285: unifiable: Assertion failed: ((((*((Word)((uintptr_t)(p)&~0x00000001L)))) & 0x00000007L) == 0x00000001L)
C-stack trace labeled "crash":
[0] PL_strtod() at ??:? [0x7f476f204c2c]
[1] __assert_fail() at ??:? [0x7f476f1ca7a1]
[2] pl_compound_name_arity3_va() at ??:? [0x7f476f19a2e3]
[3] PL_next_solution() at ??:? [0x7f476f16316a]
[4] pl_skip_list3_va() at ??:? [0x7f476f19f14e]
[5] pl_skip_list3_va() at ??:? [0x7f476f19f8db]
[6] PL_toplevel() at ??:? [0x7f476f15cb9d]
[7] swipl(main+0x2d) [0x4008ad]
[8] __libc_start_main() at ??:? [0x7f476eb8d610]
[9] swipl(_start+0x29) [0x4008f9]

I think append would be possible but this one might not work for much more of the advanced things - maybe the CHR and DCG version could pull it off!

Mainly what was changed was as expected: Using tor for fair search to stop the search getting sucked into an infinite fail black hole. Added checks that stop cyclic terms being generated.
It's very brittle though, one little thing missing (like notspecialo) and it wont terminate. Minikanren doesn't feel like that.

A hangout could be fun, I enjoyed the uncourse hangouts!

[Jan Burse]

I was switching to unicode for the atoms 'quote',
'cons' and 'lambda':

/* we are using
LEFT SINGLE QUOTATION MARK
LATIN LETTER LATERAL CLICK
GREEK SMALL LETTER LAMBDA
*/
:- encoding(utf8).


And then formulating the quine itself via DCG:

/**
* quine(Q):
* The quine test, as DCG.
*/
quine(Q) -->
{sto(Q), freeze(Q, is_expr(Q))},
eval(Q, [], Q).

This gives the following result:

?- between(1, 6, M), quine(Q, [M], [0]), copy_term_nat(Q, H),
numbervars(H, 0, _), write(H), nl, fail; true.
[[λ,A,[ǁ,A,[ǁ,[ǁ,[‘,‘],[ǁ,A,[‘,[]]]],[‘,[]]]]],[‘,[λ,A,[ǁ,A,[ǁ,[ǁ,[‘,‘],[ǁ,A,[‘,[]]]],[‘,[]]]]]]]
etc..
[[[λ,A,[λ,B,[ǁ,B,[ǁ,[ǁ,[‘,‘],[ǁ,B,[‘,[]]]],[‘,[]]]]]],[‘,C]],[‘,[[λ,A,[λ,B,[ǁ,B,[ǁ,[ǁ,[‘,‘],[ǁ,B,[‘,[]]]],[‘,[]]]]]],[‘,C]]]]
etc..

Unfortunately this doesn't work in a thread window in SWI-Prolog,
i.e. using the menu item "Run | New thread". When use listing(eval//3)
I don't see the result:

eval(['‘', A], _, A, B, B).
eval([ǁ, B, F], C, [D|G], A, I) :-
step(A, E),
eval(B, C, D, E, H),
eval(F, C, G, H, I).
eval([λ, A, B], C, [closure, A, B, C], D, D).

Instead I will see the below, although in the main console the listing
works correctly. So the new thread window and the main console
seem to use different widgets or somes uch:

eval(['‘', A], _, A, B, B).
eval([<black box here>, B, F], C, [D|G], A, I) :-
step(A, E),
eval(B, C, D, E, H),
eval(F, C, G, H, I).
eval([<black box here>, A, B], C, [closure, A, B, C], D, D).

Same problem on a 2K display even with the SWI-Prolog main console. :-(

Now I am heating the CPU with a DCG definition of twine:

?- between(1, 6, M), twine(Q, P, [M], [0]),
copy_term_nat(Q-P, H), numbervars(H, 0, _),
write(H), nl, fail; true.

No results so far, but also no crash.

Bye

cycling fan schrieb:

[j4n bur53]

cycling fan schrieb:

> It's very brittle though, one little thing missing (like notspecialo)
> and it wont terminate. Minikanren doesn't feel like that.

Was trying YAP Prolog 6.3.3, quine(Q, [5], X), killed my machine.
The cursor of YAP Prolog stopped blinking, then other windows
didn't react, then task-manager was not anymore accessible.

Bye

[Jan Burse]

cycling fan schrieb:

> It was not possible to generate twines...
>
> ?- search(id((dif(Q,P),(evalo(Q,P,[]),evalo(P,Q,[]))))).
> [Thread 1] pl-prims.c:3285: unifiable: Assertion failed: ((((*((Word)((uintptr_t)(p)&~0x00000001L)))) & 0x00000007L) == 0x00000001L)
> C-stack trace labeled "crash":
> [0] PL_strtod() at ??:? [0x7f476f204c2c]
> [1] __assert_fail() at ??:? [0x7f476f1ca7a1]
> [2] pl_compound_name_arity3_va() at ??:? [0x7f476f19a2e3]
> [3] PL_next_solution() at ??:? [0x7f476f16316a]
> [4] pl_skip_list3_va() at ??:? [0x7f476f19f14e]
> [5] pl_skip_list3_va() at ??:? [0x7f476f19f8db]
> [6] PL_toplevel() at ??:? [0x7f476f15cb9d]
> [7] swipl(main+0x2d) [0x4008ad]
> [8] __libc_start_main() at ??:? [0x7f476eb8d610]
> [9] swipl(_start+0x29) [0x4008f9]
>
> I think append would be possible but this one might not work for
> much more of the advanced things - maybe the CHR and DCG
> version could pull it off!

A further option would be to try ECLiPSe Prolog. I went
with the following definitions, link to source code at
the end of this post:

/* ECLiPSe Prolog specific freeze/2 definition */
delay freeze(X, _) if var(X).
freeze(_, G) :- call(G).

/* ECLiPSe Prolog specific dif/2 */
neq(X, Y) :- X ~= Y.

I get the following runtimes:

ECLiPSe Constraint Logic Programming System [kernel]
Version 6.1 #194 (x86_64_nt), Fri Oct 24 12:21 2014

?- quine(Q, [5], [0]).

Q = [[lambda, _443, [cons, _443, [cons, [cons, [quote, quote],
[cons, _443, [quote, []]]], [quote, []]]]], [quote, [lambda,
_443, [cons, _443, [cons, [cons, [quote, quote], [cons, _443,
[quote, ...]]], [quote, []]]]]]]

There are 17 delayed goals. Do you want to see them? (y/n)
Yes (0.90s cpu, solution 1, maybe more) ? ;

No (11.36s cpu)

Its faster for the first solution:
ECLiPSe: 0.9 sec SWI-Prolog: 1.4 sec

But slower for the redo:
ECLiPSe: 11.3 sec SWI-Prolog: 9.2 sec

Bye

quines3eclipse.p:
https://gist.github.com/jburse/c1e3c2051f1f724adcac#file-quines3eclipse-p

[Jan Burse]

Anybody figured out how to do the Quines example
in Picat or maybe B-Prolog? Does it run fast?

picat tutorial flops16 2
https://www.youtube.com/watch?v=dfJebzh62Jg

thecon...@gmail.com schrieb:

[cycling fan]

On Wednesday, 9 March 2016 09:46:09 UTC, Jan Burse wrote:
> Anybody figured out how to do the Quines example
> in Picat or maybe B-Prolog? Does it run fast?
>
> picat tutorial flops16 2
> https://www.youtube.com/watch?v=dfJebzh62Jg
>

> schrieb:
> > Hi!
> >
> > I wrote a modified version that uses CHR for the constraints: http://lpaste.net/160468722731974656
> >
> > I had to remove occurs check to get it to work with CHR, though it seems okay so far as I can still generate quines. I also made vars disjoint from the expressions and removed the app tag to try and speed things up.
> >
> > I'm still new to prolog so if there's anything that can be fixed or improve I'd be happy to hear about it.
> >

I was thinking about how this might be done in the language Curry which works differently to prolog and mk, but it does have fair search so it might well work there too.

http://www-ps.informatik.uni-kiel.de/currywiki/start

[R Kym Horsell]

If you're going to consider other languages or formalisms, perhaps
give von Thun's "Joy" a look.

Some of his papers are still around and there is a wikipedia entry.

At one point there was a "concatenative languages" group going somewhere
(a term von Thun first used for his language).

To give a flavor: all programs are written as a sequence of
atoms. The quoting operation is written as [P] where P is any program.
In simple terms programs appear to be Forth-like sequences of operators
that perform stack manipulations. But another way of looking at them
is as combinatory operators.

As for Scheme or other more (syntactically) complex languages you
can "solve" equations to derrive programs that have certain properties.

E.g. for quines you want a program P that when run produces a literal
copy of P i.e. [P].

So we have the equation to solve:
P == [P].

The actual "primitive" operators in Joy are left open to the
inventiveness of the implementor.

A couple basic ones might be dup and cons defined as:

[x] dup == [x] [x]
[x] [y] cons == [x y]

Ergo to solve for the self-replicator P we have a fairly speedy
Warplan-like search that almost immediately ends with
P == [[dup cons] dup cons]

It turned out dup cons appeared so often vT named it duco hence
P == [[duco] duco].

More interesting self-rep programs can be solved just as easily.
E.g. self-replicators that achieve some other effect as well as creating
a literal copy (or not literal copy) of themselves.

E.g. "genetic replicators" that have some internal state or memory
and when run create a literal copy with an updated state.
A simple example of course being a counter to record the number
of generations the replicator has "survived".

Adding in some glue to convert between e.g. Joy and Scheme is also
fairly straightforward if you insist on self-replicating Scheme with
certain additional proerties.


--
I argue very well. Ask any of my remaining friends. I can win an
argument on any topic, against any opponent. People know this, and
steer clear of me at parties. Often, as a sign of their great respect,
they don't even invite me.
-- Dave Barry

[j4n bur53]

R Kym Horsell schrieb:

> To give a flavor: all programs are written as a sequence of
> atoms. The quoting operation is written as [P] where P is any program.
> In simple terms programs appear to be Forth-like sequences of operators
> that perform stack manipulations. But another way of looking at them
> is as combinatory operators.

The eval flavor is currently more appealing to me. There
is a simple relationship of the quines example to other
examples in logic. For example asking for quines is
simply posing:

?- eval(Q, Q).

But you could also ask for:

?- eval(R, ~R).

Thus asking the interpreter for a russel paradox like instance.
Of course you would need some appropriate definition of
(~)/2. But such instance finders are actually used in proof
assistants, either to help you solve your problem or to
give you automatically a counter example.

For example the "blast" strategy of Isabelle/HOL seems to
easily find an f such that: exists a {x. x notin (f x)}
= (f a). Which is again a similar problem as the quines
example. If I remember well this is also done in a blink,
don't have the exact figures with me, could be in range
1 sec - 10 sec.

Just some guess, why the quines could be kind of
litmus test whether your constraint solver can only
juggle some numbers or do a little bit more symbolically.

Bye

[Mostowski Collapse]

We have tackled an old problem as a benchmark for
freeze/2 and when/2 in Prolog. Its an old problem because
we had an old solution, but gave it a new try with a slightly

different programming. Its based on this paper:

William E. Byrd, Eric Holk, Daniel P. Friedman, 2012
miniKanren, Live and Untagged
Quine Generation via Relational Interpreters

We get this result via Prolog:

?- dif(Q, []), quine(Q, 6, N).
Q = [[lambda, symbol(_Q), [cons, symbol(_Q), [cons, [cons,
[quote, quote], [cons, symbol(_Q), [quote, []]]], [quote,
[]]]]], [quote, [lambda, symbol(_Q), [cons, symbol(_Q), [cons,
[cons, [quote, quote], [cons, symbol(_Q), [quote, []]]],
[quote, []]]]]]],
N = 5

The source code is here:

Testing freeze/2 and dif/2:
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine-pl

Testing when/2 and dif/2:
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine2-pl

[Mostowski Collapse]

Here are the test results for freeze/2:

/* Jekejeke Prolog 1.4.7 */
?- time((dif(Q, []), quine(Q, 6, N))).
% Up 37,047 ms, GC 288 ms, Threads 36,688 ms (Current 12/30/20 23:22:42)

/* SWI-Prolog 8.3.15 */

?- dif(Q, []), quine(Q, 6, N).

ERROR: Stack limit (1.0Gb) exceeded

/* SICStus Prolog 4.6.0 */
?- statistics(walltime, [T|_]), dif(Q,[]), quine(Q,6,N),
statistics(walltime, [S|_]), D is S-T.
D = 5441

And here for when/2:

/* Jekejeke Prolog 1.4.7 */
?- time((dif(Q, []), quine(Q, 6, N))).
% Up 71,002 ms, GC 552 ms, Threads 70,438 ms (Current 12/30/20 23:37:20)

/* SWI-Prolog 8.3.15 */

?- dif(Q, []), quine(Q, 6, N).

ERROR: Stack limit (1.0Gb) exceeded

/* SICStus Prolog 4.6.0 */
?- statistics(walltime, [T|_]), dif(Q,[]), quine(Q,6,N),
statistics(walltime, [S|_]), D is S-T.
D = 21262

Remarkably SWI-Prolog cannot do it. We tried increasing the
memory 2GB and then 4GB, but it didn't help.

Also stunning, SICStus Prolog is quite fast, but it seems our
when/2 overhead is only 100% and not 300%.

[Mostowski Collapse]

Blame it on Corona that not fully occupied with some
partying. I just had a look at SWI-Prolog discourse. Jan W.
narrowed down the problem. I took his pair of terms P

and Q and could produce an even worse test case:

s1 :-
Q=[[lambda,symbol(_3026),[cons,[quote,_3434],[quote,_3514]]],[quote,_3206]],
P=[_3434|_3514],
freeze(_3434, (write(foo), nl)),
unify_with_occurs_check(P, Q).

s2 :-
Q=[[lambda,symbol(_3026),[cons,[quote,_3434],[quote,_3514]]],[quote,_3206]],
P=[_3434|_3514],
freeze(_3434, (write(foo), nl)),
freeze(_3514, (write(foo), nl)),
unify_with_occurs_check(P, Q).

And then I get:

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.16)

?- s1.
false.

?- s2.
foo
foo
true.

I think its a logical error that s2 succeeds. Seems that the
cycle test got lost.

[Mostowski Collapse]

Just out of curiousity I changed freeze/2 into dif/2. So I was
running these test cases:

s1 :-
Q=[[lambda,symbol(_3026),[cons,[quote,_3434],[quote,_3514]]],[quote,_3206]],
P=[_3434|_3514],

dif(_3434, foo),

unify_with_occurs_check(P, Q).

s2 :-
Q=[[lambda,symbol(_3026),[cons,[quote,_3434],[quote,_3514]]],[quote,_3206]],
P=[_3434|_3514],

dif(_3434, foo),
dif(_3514, foo),
unify_with_occurs_check(P, Q).
Now I get these results:

SWI-Prolog (threaded, 64 bits, version 8.3.16)

?- s1.
false.

?- s2.

true.

So it seem in SWI-Prolog, attributed variables in various incarnations
such as freeze/2, dif/2, etc… seem to interfer with unify_with_occurs_check/2.
I did not yet check bare bone attributed variables and unify hook.

[Mostowski Collapse]

One way out could be to roll your own unify_with_occurs_check/2. We can write it in Prolog itself, as was done in the past, for Prolog systems that did not have unify_with_occurs_check/2:

Mark Stickels unify/2:
https://formal.iti.kit.edu/beckert/leantap/unify.pl

Here is an alternative take that uses (=..)/2 and term_variables/2:

unify(X, Y) :- var(X), var(Y), !, X = Y.
unify(X, Y) :- var(X), !, notin(X, Y), X = Y.
unify(X, Y) :- var(Y), !, notin(Y, X), X = Y.
unify(X, Y) :- functor(X, F, A), functor(Y, G, B),
F/A = G/B,
X =.. [_|L],
Y =.. [_|R],
unify_list(L, R).

unify_list([X|L], [Y|R]) :-
unify(X, Y),
unify_list(L, R).
unify_list([], []).

notin(X, Y) :-
term_variables(Y, L),
notin_list(L, X).

notin_list([Y|L], X) :-
X \== Y,
notin_list(L, X).
notin_list([], _).

I now get the expected result:

?- s1.
false.

?- s2.

false.

[Mostowski Collapse]

With the help of unify/2 we can now benchmark SWI-Prolog as well:

With freeze/2:

/* SWI-Prolog 8.3.15 (using unify/2) */

?- time((dif(Q, []), quine(Q, 6, N))).

% 272,225,648 inferences, 18.301 CPU in 18.591 seconds (98% CPU, 14874585 Lips)

With when/2:

/* SWI-Prolog 8.3.15 (using unify/2) */

?- time((dif(Q, []), quine(Q, 6, N))).

% 318,001,853 inferences, 19.941 CPU in 20.090 seconds (99% CPU, 15947437 Lips)

Interestingly, SWI-Prolog doesn't beat SICStus freeze/2, but
it beats SICStus when/2, even with slowpoke unify/2. Woa!

[Mostowski Collapse]

Concerning the test cases s1 and s2. The outcome of s2 is wrong. The
outcome is wrong in two respects, first _3434 gets triggered and second
unify_with_occurs_check succeeds.

That _3434 shouldn't get triggered follows from 7.3.2 Herband Algorithm in
ISO core standard. According to clause 7.3.2 f) 1) an instantiation of variable
X to a term t is only propagated when it X does not occur in t.

That the unification should fail follows from clause 7.3.2 g).

[Mostowski Collapse]

The smallest test cases are probably these ones:

?- freeze(A,(write(A),nl)),freeze(B,(write(B),nl)),unify_with_occurs_check(B-A,n-s(A)).
false.

?- freeze(A,(write(A),nl)),freeze(B,(write(B),nl)),unify_with_occurs_check(A-B,s(A)-n).
@(S_1,[S_1=s(S_1)])
n
A = s(A),
B = n.

LoL

[Mostowski Collapse]

Woa! METUTL.P predates Mark Stickel. Anything older?

R.A.O'Keefe, 15 September 1984
http://www.picat-lang.org/bprolog/publib/metutl.html

Unfortunately the web document has a glitch.
subsumes/2 has multiple copies of clauses.

[Mostowski Collapse]

Lets assume SICStus Prolog is the benchmark for the implementation
of certain predicates, even ISO core standard predicates. Especially
in connection with attributed variables.

I then find these examples here. Its from SICStus 4 and not only SICStus 3:

?- when(nonvar(X), X=a), subsumes_term(X, b), X = a.
X = a ?
yes

?- when(nonvar(X), X=a), subsumes_term(X, b), X = b.
no
https://sicstus.sics.se/sicstus/docs/latest4/html/sicstus/mpg_002dref_002dsubsumes_005fterm.html

When do the same in SWI-Prolog I get different results:

?- when(nonvar(X), X=a), subsumes_term(X, b), X = a.
false.

?- when(nonvar(X), X=a), subsumes_term(X, b), X = b.
false.

How would one implement a workaround? ROKs METUTL.PL
probably doesn't help, since it uses normal unification.

[Mostowski Collapse]

Are there test cases where SWI-Prolog can determine subsumes_term/2 for cyclic terms? Can SICStus Prolog do that? What comes to mind and works in SWI-Prolog is the following. But did not yet check SICStus Prolog would do:

?- X = f(X), subsumes_term(Y, X).
X = f(X).

[Mostowski Collapse]

Propotypical I have adopted SICStus Prologs behaviour now. I have
specialized Java code for unifyWithOccursCheck() and subsumesTerm().
The later code was born yesterday, my system didn’t have subsumes_term/2
before yesterday. I don’t use this algorithm by SWI-Prolog:

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

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

I rather use this algorithm from METUTL.PL, but it is modified to completely
avoid calling term_variables/2:

subsumes(General, Specific, Vars) :-
/* ROKs algorithm from METUTL.PL but Vars is not a list,
but just a term, and var_member_chk/2 is just the occurs
check from unify_with_occurs_check. Also instead of
binAttr/2 just use bindUniv/2 , to avoid triggering */

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

The term_variables/2 variant could sometimes be faster, sometimes not.
Since my terms have a special variables string, so for example terms directly
fetched from a clause don’t need term_variables/2, the occurs check is faster.

GitHub source:
https://github.com/jburse/jekejeke-devel/blob/master/jekrun/headless/jekpro/reference/structure/SpecialUniv.java#L736

[Mostowski Collapse]

But maybe the SWI-Prolog algorithm is better, but it requires
unification in presence of cyclic terms, as this example shows.
It even requires a term_variables/2 that can deal with cyclic terms:

?- subsumes_term(g(X),g(f(X))).
false.

?- term_variables(g(f(X)), SVars).
SVars = [X].

?- term_variables(g(f(X)), SVars), g(X) = g(f(X)), term_variables(SVars, L).
X = f(X),
SVars = [X],
L = [].

The ROK algorithm doesn’t need cyclic terms, in particular no unify (=)/2
or term_variables/2 that could deal with cyclic terms, it blocks such a
case much earlier on, it is somehow closer to unify_with_occurs_check/2
works with acyclic terms.

[Mostowski Collapse]

I wonder what SICStus Prolog does in this example:

SWI-Prolog (threaded, 64 bits, version 8.3.16)

?- X=s(X), unify_with_occurs_check(Z-Z,X-s(Z)).
X = Z, Z = s(Z).
?- X=s(X), unify_with_occurs_check(Z-Z,s(Z)-X).
false.

By way of:
https://github.com/mthom/scryer-prolog/issues/101#issuecomment-487383444

And this is an old attempt of scryer to do subsumes_term/2:

subsumes_term(General, Specific) :-
\+ \+ (
term_variables(Specific, SVs1),
unify_with_occurs_check(General, Specific),
term_variables(SVs1, SVs2),
SVs1 == SVs2
).

Why not this? Would it also work?

subsumes_term(General, Specific) :-
\+ \+ (
term_variables(Specific, SVs1),
unify_with_occurs_check(General, Specific),
length(SVs1, N),
term_variables(SVs1, SVs2),
length(SVs2, M),
N == M
).

[Mostowski Collapse]

Oh, the irony:

SICStus 4.6.0 (x86_64-win32-nt-4):

?- X=s(X), unify_with_occurs_check(Z-Z,X-s(Z)).
no
| ?- X=s(X), unify_with_occurs_check(Z-Z,s(Z)-X).
no

[Mostowski Collapse]

Ok this idea, is a poop idea:

> subsumes_term(General, Specific) :-
> \+ \+ (
> term_variables(Specific, SVs1),
> unify_with_occurs_check(General, Specific),
> length(SVs1, N),
> term_variables(SVs1, SVs2),
> length(SVs2, M),
> N == M
> ).

Counter example by Ulrich Neumerkel, subsumes_term(-X, Y).

But lets see what TauProlog does concerning unify_with_occurs_check?
I find the following result:

TauProlog 0.3.0 (beta):

?- X=s(X), unify_with_occurs_check(Z-Z,s(Z)-X).
false.
?- X=s(X), unify_with_occurs_check(Z-Z,X-s(Z)).
false.

So it implements the SICStus Prolog semantics, and not the
SWI-Prolog semantics?

[Mostowski Collapse]

I guess I must retract my claim that TauProlog and SICstus
Prolog do the same. For example I now get the following
result, using Jan Ws minimal example:

?- X = f(X), unify_with_occurs_check(X, X).
X = f(X).

Not anymore “false”

[Mostowski Collapse]

Interesting find: One wont run into compatibility problems
concerning an OC flag with SICStus Prolog. It doesn’t have
an occurs check flag:

SICStus 4.6.0 (x86_64-win32-nt-4)

?- set_prolog_flag(occurs_check, true).
Domain error in argument 1 of set_prolog_flag/2
expected prolog_flag, but found occurs_check
goal: set_prolog_flag(occurs_check,true)

BTW: I am thinking of new promotional gifts. T-Shirt, Base-
ball Caps, and Coffee Mugs with "I ❤️ Prolog". Or maybe
"🚫 Cyclic Terms". LoL

[Mostowski Collapse]

We were again using some thinking time for an occurs_check
Prolog flag. But I guess abandoning such a Prolog flag gives
a speed advantage. One does not have to check this flag

all the time. The worst implementations check this flag all the
time before binding a variable. This costs memory bandwidth
to access the flag in the environmemt and precious CPU

time. Better implementations might do a branching more earlier
on. But since only few Prolog systems implement this Prolog
flag, it also leads to Prolog code that isn't portable.

On the other hand an interesting value of an occurs_check
Prolog flag is the value "error". How would one implement a
predicate unify_with_occurs_check_and_error/2 ?

Please note, the solution for unify_with_occurs_check_and_error/2
should behave like unify_with_occurs_check/2, i.e. not trigger
attributed variables.

[Mostowski Collapse]

The later seems to be rather trivial, if one accepts a Prolog solution:

unify_with_error(X, Y) :- var(X), var(Y), !, X = Y.
unify_with_error(X, Y) :- var(X), !, must_notin(X, Y), X = Y.
unify_with_error(X, Y) :- var(Y), !, must_notin(Y, X), X = Y.
unify_with_error(X, Y) :- functor(X, F, A), functor(Y, G, B),

F/A = G/B,
X =.. [_|L],
Y =.. [_|R],

maplist(unify_with_error, L, R).

must_notin(X, Y) :-
term_variables(Y, L),
maplist(\==(X), L), !.
must_notin(X, Y) :-
throw(error(occurs_check(X, Y),_)).

Seems to work and no interference with attributed variables:

/* SICStus 4.6.0 (x86_64-win32-nt-4) */

?- unify_with_error(X, f(X)).
error(occurs_check(_413,f(_413)),_409)

?- freeze(X, throw(ball)), unify_with_error(X, f(X)).
error(occurs_check(_413,f(_413)),_409)

[Mostowski Collapse]

Yesterday I closed all my occurs check flag tickets, and a particular
idea I had was abandoned. But I was testing the wrong thing. Now
reopening them, and working again on occurs check.

I now have a rather simple test case, which would allow a quantitative
assesment. Here is a simple example, with a more drastic impact,
Peano factorial:

add(n, X, X).
add(s(X), Y, s(Z)) :- add(X, Y, Z).

mul(n, _, n).
mul(s(X), Y, Z) :- mul(X, Y, H), add(Y, H, Z).

fac(n, s(n)).
fac(s(X), Y) :- fac(X, H), mul(s(X), H, Y).

I then get:

SWI-Prolog (threaded, 64 bits, version 8.3.16)

?- time(fac(s(s(s(s(s(s(s(s(s(s(s(n))))))))))),_)).
% 43,954,868 inferences, 2.576 CPU in 2.616 seconds (98% CPU, 17065822 Lips)
true.

?- set_prolog_flag(occurs_check, true).
true.

?- time(fac(s(s(s(s(s(s(s(s(s(s(s(n))))))))))),_)).
% 43,954,868 inferences, 5.627 CPU in 6.365 seconds (88% CPU, 7811022 Lips)
true.

Thats a ca. 150% slow down. LIPS go drastically down.