search

mattiasw2 / teyjus

Automatically exported from code.google.com/p/teyjus
GNU General Public License v3.0
0 stars 0 forks source link

Unification failure in currying example #87

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
At least since revision 658 [1], unification does not complete in the currying 
example, as shown by examples/handbook/progs/script2 [2] (I've reproduced the 
same problem with release 2.0-b2 and with the latest release). Yet, the comment 
still says that this example "demonstrates the power/usefulness of higher-order 
unification".

I am interested in using Teyjus only if this example works, since I'm 
interested in writing more complex rewrite rules relying on higher-order 
unification.

Links:
[1] https://code.google.com/p/teyjus/source/detail?spec=svn1133&r=658
[2] 
https://code.google.com/p/teyjus/source/browse/trunk/examples/handbook/progs/scr
ipt2

Original issue reported on code.google.com by p.giarrusso on 18 May 2014 at 1:06

GoogleCodeExporter commented 9 years ago 
Is this change a consequence of the restriction to pattern unification?

After reading 
http://www.cs.nmsu.edu/ALP/2010/03/teyjus-a-lprolog-implementation/ and 
skimming Xiaochu Qi's PhD thesis (at the end of Sec. 9.3), I guess that 
"[Teyjus 2] is oriented around a special form of higher-order unification known 
as pattern unification" probably means "it only supports pattern unification".

Teyjus 1 seems to manage this example successfully, once I build it on a 32bit 
machine (it's almost certainly possible to make it build a 32bit executable on 
64bit machines).

If that's the case, I might not be interested in using Teyjus 2 after all, as 
long as you don't implement higher-order unification. Moreover, I'm 
disappointed by the fact that this restriction is not clearly explained.

Original comment by p.giarrusso on 18 May 2014 at 1:53

GoogleCodeExporter commented 9 years ago 
Hi,

Indeed Teyjus 2 is restricted to pattern unification that's why you don't have 
the expected result. There are reasons to do that: pattern unification has good 
algorithmic properties whereas the general higher-order case is undecidable.
Furthermore, pattern unification is most of the time enough for applications.
Well of course, it is not enough for this example which should be removed 
because this does not illustrate anything...

I agree that should be stated more clearly that Teyjus 2 cannot handle the full 
case.

Fabien

Original comment by fafounet@gmail.com on 19 May 2014 at 7:59