[developers] Bug in interactive unification

[Guy Emerson]

Dear all,

I found a bug in interactive unification, which I posted about here:
https://delphinqa.ling.washington.edu/t/bug-in-interactive-unification/592

The bug is the following: if there is no possible type for a feature path,
but that path does not exist in either of the two input feature structures,
then interactive unification does not enforce all constraints (i.e. it
produces an incorrect result, rather than reporting unification failure).

I wasn’t sure where to report this bug.

This is admittedly a rare situation (which is probably why it hasn’t been
an issue until now).  But it happens when recursive computation types lead
to a unification failure.  I’ve written a small example to illustrate the
problem (see attached file).  Note that there is no parsing involved here,
just compilation of this file and interactive unification.

In more positive news, I can report that when there is no failure, the LKB
and interactive unification are both robust to extremely recursive type
constraints. I implemented the untyped lambda calculus as a type system,
and I tested it using the Ackermann function as a lambda expression on
Church numerals (the Ackermann function is non-primitive-recursive, so I
thought this would be a good test case). With 10,570 re-entrancies (no that
is not a typo), it correctly evaluated A(2,1)=5.

Best,
Guy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.delph-in.net/archives/developers/attachments/20201109/f3aadb2f/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: unification-bug.tdl
Type: application/octet-stream
Size: 3569 bytes
Desc: not available
URL: <http://lists.delph-in.net/archives/developers/attachments/20201109/f3aadb2f/attachment.obj>