[falsissime]

> [3] What does the DEC10 Prolog manual say about the occurs check?

See I.2.1. Occur Check of https://userweb.fct.unl.pt/~lmp/publications/online-papers/D...

A recent related discussion: https://stackoverflow.com/questions/65600226/what-occurs-che...

In general, we do agree on the observation that Prolog profits from both the theoretical and the practical side. But still even today I have the impression that the highly theoretically leaning side does not appreciate the fundamental contribution errors have on ensuring correctness properties. At least this was my impression of November 10th in Paris.

Just one personal recollection (from memory) which probably also influences my view on the Kowalski-Colmerauer relation. At a META 90 tutorial/talk about meta interpreters, Sterling attributed the origin of meta interpreters to Warren and the DEC10 manual. Kowalski responded (publicly during the talk) that this was well known to Colmerauer, well before Warren ever got into Prolog.

As to the lady you are referring to she is his widow, a linguist.

[falsissime]

Just to note one error in I.2.1:

> ... whereas unification without the occur check is linear on the size of the smallest of the terms being unified.

This claim is incorrect, it goes far beyond what is possible. To see its incorrectness consider the unification problem X = Y. And just for illustrative purposes, think of them both as being very big and evolved. Now, consider a related unification problem Z-Z = X-Y with Z just a variable. According to above claim, the cost would be now independent of X and Y which cannot be.

[YeGoblynQueenne]

Yes, I see, that doesn't make sense.

I wonder if all that was more of a consideration in an older time, with weaker hardware. Anyway where I come from (ILP research, again) "polynomial time" is synonymous to "efficient" and the bigger problem is proofs failing to terminate.

I might actually try some learning experiments with the occurs check flag set to "true" just to see what happens. I mean, I wonder. I'm so used to leaving the flag to default false that I wonder if I haven't formed a completely wrong model about the execution of Prolog programs. I've been coding in Prolog for more than ten years now and it still catches me off-guard at times.

[falsissime]

Consider to set the flag to "error" to see if there are any cases where infinite terms would be created.

[YeGoblynQueenne]

>> See I.2.1. Occur Check of https://userweb.fct.unl.pt/~lmp/publications/online-papers/D...

>> A recent related discussion: https://stackoverflow.com/questions/65600226/what-occurs-che...

Thanks! I'll have a look.

It's funny but my go-to reference for unification (Foundations of Inductive Logic Programming, 1997) says that the occurs check is crucial for the performance of the algorithm (because without it unification can go on forever, whereas with the occurs check unification will terminate and find an mgu if one exists). That's exactly the opposite argument than the one in the PDP-11 and Sicstus manuals.

I confess it's been a while since I've looked at the matter. Thanks for reminding me to refresh on it. Just in case it comes up in some internet conversation and I come across as clueless :P

>> Just one personal recollection (from memory) which probably also influences my view on the Kowalski-Colmerauer relation. At a META 90 tutorial/talk about meta interpreters, Sterling attributed the origin of meta interpreters to Warren and the DEC10 manual. Kowalski responded (publicly during the talk) that this was well known to Colmerauer, well before Warren ever got into Prolog.

Wow, that's a really interesting historical tidbit. My specific research in ILP is on an approach called "meta-interpretive learning". Doesn't quite roll of the tongue but it's basically what it says on the tin: a Prolog meta-interpreter used for induction (i.e. learning). Without the idea of meta-interpreters that wouldn't have been possible. And meta-interpreters themselves, btw, would not have been possible with strict adherence to logic programming formalisms. What I mean is, Prolog programs can take as arguments Prolog programs so Prolog programs can't be first-order. And they're not! But that opens up entire avenues of possibility, like representing second and higher-order logics.

>> As to the lady you are referring to she is his widow, a linguist.

Ah, thanks. A linguist. That figures!

[falsissime]

> the occurs check is crucial for the performance of the algorithm (because without it unification can go on forever, whereas with the occurs check unification will terminate and find an mgu if one exists).

Many current systems perform rational tree unification. Like SICStus, SWI by default, Scryer by default etc. This claim that unification going on forever only holds for rather the minority of systems today.