|
|
|
|
|
|
by falsissime
1262 days ago
|
|
|
> 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. |
|
|