[developers] Bug in interactive unification

[Guy Emerson]

After loading that file, instead of displaying the incorrect result, LUI
now displays nothing.  The log file (/tmp/yzlui.debug.ubuntu) says:

process_complete_command(): `
avm 1 #D[natnum-with-copy-wrapper NATNUM: #D[natnum-with-copy RESULT:
NATNUM]] "natnum-with-copy-wrapper - expanded"
 '

process_complete_command(): `avm 2 #D[defective-one-wrapper NATNUM:
#D[defective-pos SUCC: ZERO]] "defective-one-wrapper - expanded"
 '

process_complete_command(): `avm 3 #D[natnum-with-copy-wrapper NATNUM:
#D[defective-pos-with-copy RESULT: #D[pos SUCC: <0>= DEFECTIVE-NATNUM]
SUCC: #D[zero-with-copy RESULT: <0>]]] "Unification Failures (2)"
[#U[constraint 1 [[NATNUM SUCC] ZERO-WITH-COPY ZERO ZERO-WITH-COPY -1]
#U[type 0 [NATNUM SUCC RESULT] DEFECTIVE-NATNUM ZERO 1]] '

Item in list is not homogeneous (list type 12, item type 3)
Path of failure was not a list of symbols (type 12)
Item in list is not homogeneous (list type 13, item type 3)
YZLUI: Received unknown lkb-protocol top-level command: AVM


Am Di., 10. Nov. 2020 um 08:29 Uhr schrieb John Carroll <
J.A.Carroll at sussex.ac.uk>:

> Dear Guy,
>
> 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.
>
> 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...
>
> 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")
>
> John
>
> On 9 Nov 2020, at 15:12, Guy Emerson <gete2 at cam.ac.uk> wrote:
>
> 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
> <unification-bug.tdl>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.delph-in.net/archives/developers/attachments/20201110/1a57cf2f/attachment.html>