<div dir="ltr"><div>Dear all,</div><div><br></div><div>I found a bug in interactive unification, which I posted about here: <a href="https://delphinqa.ling.washington.edu/t/bug-in-interactive-unification/592">https://delphinqa.ling.washington.edu/t/bug-in-interactive-unification/592</a></div><div><br></div><div>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).<br><br>I wasn’t sure where to report this bug.<br><br>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.</div><div><br></div><div>
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.</div><div><br></div><div>Best,</div><div>Guy<br>

</div></div>