Issue 91 in teyjus: odd behavior with unification

[tey...@googlecode.com]

Status: Accepted
Owner: dale.a.m...@gmail.com

New issue 91 by dale.a.m...@gmail.com: odd behavior with unification
https://code.google.com/p/teyjus/issues/detail?id=91

I was writing some code to translate lambda-normal terms into de Bruijn
syntax. The full program is attached. Just compile the bug.mod and call
the test goal.

There is a clause, written as

debe C (app M N) H ZZ :- (ZZ = (x\ Args (N'::x))), debi C N N', debe C M H
Args.

In this form, the "Heap overflow" error is generated. If we rewrite this
clause as (the logically equivalent clause)

debe C (app M N) H ZZ :- debi C N N', debe C M H Args, (ZZ = (x\ Args
(N'::x))).

then the program produces the correct answer. I don't see why the first
version leads to a looping error.

Notice that the unification problem above is not in the pattern fragment.



Attachments:
bug.mod 604 bytes
bug.sig 354 bytes

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