Issue 87 in teyjus: Unification failure in currying example

[tey...@googlecode.com]

Status: New
Owner: ----

New issue 87 by p.giarrusso: Unification failure in currying example
http://code.google.com/p/teyjus/issues/detail?id=87

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/script2

--
You received this message because this project is configured to send all
issue notifications to this address.
You may adjust your notification preferences at:
https://code.google.com/hosting/settings

[tey...@googlecode.com]

Comment #1 on issue 87 by p.giarrusso: Unification failure in currying
example
http://code.google.com/p/teyjus/issues/detail?id=87

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.

[tey...@googlecode.com]

Updates:
Status: Accepted

Comment #2 on issue 87 by fafo...@gmail.com: Unification failure in
currying example
http://code.google.com/p/teyjus/issues/detail?id=87

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