<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div class="" style="word-wrap:break-word; line-break:after-white-space">Dear Guy,
<div class=""><br class="">
</div>
<div class="">Thanks for this example showing the problem. I’ve reproduced it: unification failure at SUCC.RESULT with LKB native graphics, but successful unification with LUI.<br class="">
<br class="">
What gets executed is very different between the two cases. The LKB is content to find the first failure path, whereas for LUI the LKB runs a completely different ‘robust’ unifier which records all failure paths. I’ve found a bug in the latter which I think
accounts for the problem. In debug-unify2 in src/glue/dag.lsp, (nconc %failures% failures) does not get assigned back to %failures% as it should. This means that currently a failure in applying a constraint is only recorded if it's not the first unification
failure. Hmm...</div>
<div class=""><br class="">
</div>
<div class="">I attach a patch for the LKB (any version) which fixes the problem you observed with LUI interactive unification. I hope it fixes the bug completely, but I haven't tested on other examples. Since it's Lisp code, you can load it by typing the following
at the command line in a running LKB: (load "path-to/debug-unify2-patch.lsp")</div>
<div class=""><br class="">
</div>
<div class="">John</div>
<div class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On 9 Nov 2020, at 15:12, Guy Emerson <<a href="mailto:gete2@cam.ac.uk" class="">gete2@cam.ac.uk</a>> wrote:</div>
<br class="x_Apple-interchange-newline">
<div class="">
<meta content="text/html; charset=utf-8" class="">
<div dir="ltr" class="">
<div class="">Dear all,</div>
<div class=""><br class="">
</div>
<div class="">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" class="">
https://delphinqa.ling.washington.edu/t/bug-in-interactive-unification/592</a></div>
<div class=""><br class="">
</div>
<div class="">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 class="">
<br class="">
I wasn’t sure where to report this bug.<br class="">
<br class="">
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 class=""><br class="">
</div>
<div class="">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 class=""><br class="">
</div>
<div class="">Best,</div>
<div class="">Guy<br class="">
</div>
</div>
<span id="x_cid:f_khaonynj0"><unification-bug.tdl></span></div>
</blockquote>
</div>
<br class="">
</div>
<div class=""></div>
</div>
<div class="" style="word-wrap:break-word; line-break:after-white-space">
<div class=""></div>
<div class=""><br class="">
</div>
</div>
</body>
</html>