| >> 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! |
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.