> ... 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.
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.
>> A recent related discussion: https://stackoverflow.com/questions/65600226/what-occurs-che...
Thanks! I'll have a look.
>> As to the lady you are referring to she is his widow, a linguist.
Ah, thanks. A linguist. That figures :)
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.
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.