Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unification failure in currying example #87

Open
GoogleCodeExporter opened this issue Mar 17, 2015 · 2 comments
Open

Unification failure in currying example #87

GoogleCodeExporter opened this issue Mar 17, 2015 · 2 comments

Comments

@GoogleCodeExporter
Copy link

@GoogleCodeExporter GoogleCodeExporter commented Mar 17, 2015

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
Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Mar 17, 2015

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
Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Mar 17, 2015

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

  • Changed state: Accepted

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
1 participant