[developers] Bug in interactive unification

[Guy Emerson]

I also get this behaviour (no LUI window appearing) if I try to display a
type that has no features (obviously, this isn't a useful display on its
own, but it would be helpful for interactive unification to be able to drag
and drop the type).  The log file says:

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

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

> 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>
>>
>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.delph-in.net/archives/developers/attachments/20201110/6b8c4079/attachment-0001.html>