[developers] Bug in interactive unification

[Guy Emerson]

Thanks, John, with that patch I can also see a result, showing that zero
and defective-natnum fail to unify, at the right place!

I find the display a little counter-intuitive, because it gives a different
result depending on which direction I do the unification.  But that might
be a matter of taste.  It displays the failure and I can now use LKB+LUI to
debug my code!  For completeness, here is the log file for the two
unifications:

process_complete_command(): `avm 20 #D[defective-one-wrapper NATNUM:
#D[defective-pos-with-copy RESULT: #D[pos SUCC: DEFECTIVE-NATNUM] SUCC:
#D[zero-with-copy RESULT: ZERO]]] "Unification Failures (2)"
[#U[constraint 8 [NATNUM] DEFECTIVE-POS-WITH-COPY NATNUM-WITH-COPY
DEFECTIVE-POS-WITH-COPY -1] #U[type 7 [NATNUM SUCC RESULT] ZERO
DEFECTIVE-NATNUM 8]] '

process_complete_command(): `avm 9 #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 10 [NATNUM SUCC] ZERO-WITH-COPY ZERO ZERO-WITH-COPY -1]
#U[type 9 [NATNUM SUCC RESULT] DEFECTIVE-NATNUM ZERO 10]] '

a_tag_path: [0]->(null)



Woodley, here's the command for a type with no features, along with the
error again:

process_complete_command(): `avm 1 ZERO "zero - expanded"
 '

YZLUI: Received unknown lkb-protocol top-level command: AVM



Am Di., 10. Nov. 2020 um 17:51 Uhr schrieb Woodley Packard <
sweaglesw at sweaglesw.org>:

> Good sleuthing work, gentlemen.
>
> The name of the first constraint sounds like it’s being truncated somehow,
> as I would hypothesize that “vi” is part of “violation”?  Is that
> consistent with what is displayed?
>
> John, it does look like for whatever reason I did not set maclui up to
> open a log file — an unfortunate oversight.  I will fix that.
>
> Guy, when displaying the atomic AVM and getting no window, is there a
> corresponding “process_complete_command” line in the log?
>
> Regards, Woodley
>
> On Nov 10, 2020, at 9:30 AM, John Carroll <J.A.Carroll at sussex.ac.uk>
> wrote:
>
> 
> Aha, the constraint object in your LUI log has unbalanced brackets.
> Guessing which bracket is wrong, I've changed another LKB robust unifier
> function, and attach a new version of the file debug-unify2-patch.lsp
>
> With this new patch file, LUI now displays a "Unification Failures" window
> with 2 failures: "GLB Type Constraint Vi" and "No GLB Exists". Are these
> correct?
>
> John
>
>
> On 10 Nov 2020, at 12:07, John Carroll <J.A.Carroll at sussex.ac.uk> wrote:
>
> I noticed that LUI didn't display anything in response to the unification
> failure, but didn't know why since I don't get a file in /tmp/.
>
> I can't see anything else obviously wrong with the LKB code concerned, but
> I don't know whether it's sending the right thing to LUI since I haven't
> found any documentation on the LKB-LUI interface.
>
> Woodley, can you shed any light on this?
>
> John
>
> On 10 Nov 2020, at 11:50, Guy Emerson <gete2 at cam.ac.uk> wrote:
>
> 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>
>
>
>
>
>
>
> <debug-unify2-patch.lsp>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.delph-in.net/archives/developers/attachments/20201110/0d087a54/attachment-0001.html>