<div dir="ltr"><div>Thanks, John, with that patch I can also see a result, showing that zero and defective-natnum fail to unify, at the right place!</div><div><br></div>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:<br><div><div><br></div><div>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)"<br>[#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]] '<br><br>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)"<br>[#U[constraint 10 [NATNUM SUCC] ZERO-WITH-COPY ZERO ZERO-WITH-COPY -1] #U[type 9 [NATNUM SUCC RESULT] DEFECTIVE-NATNUM ZERO 10]] '<br><br>a_tag_path: [0]->(null)</div><div><br></div><div><br></div><div><br></div><div>Woodley, here's the command for a type with no features, along with the error again:<br></div><div><br></div><div>process_complete_command(): `avm 1 ZERO "zero - expanded"<br> '<br><br>YZLUI: Received unknown lkb-protocol top-level command: AVM</div><div><br></div><div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am Di., 10. Nov. 2020 um 17:51 Uhr schrieb Woodley Packard <<a href="mailto:sweaglesw@sweaglesw.org">sweaglesw@sweaglesw.org</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto"><div dir="ltr">Good sleuthing work, gentlemen.</div><div dir="ltr"><br></div><div dir="ltr">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?</div><div dir="ltr"><br></div><div dir="ltr">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.</div><div dir="ltr"><br></div><div dir="ltr">Guy, when displaying the atomic AVM and getting no window, is there a corresponding “process_complete_command” line in the log?</div><div dir="ltr"><br></div><div dir="ltr">Regards, Woodley</div><div dir="ltr"><br><blockquote type="cite">On Nov 10, 2020, at 9:30 AM, John Carroll <<a href="mailto:J.A.Carroll@sussex.ac.uk" target="_blank">J.A.Carroll@sussex.ac.uk</a>> wrote:<br><br></blockquote></div><blockquote type="cite"><div dir="ltr"> <div style="overflow-wrap: break-word;">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 <div><br> </div> <div>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?</div> <div><br> </div> <div>John</div> <div><br> <div><br> <blockquote type="cite"> <div>On 10 Nov 2020, at 12:07, John Carroll <<a href="mailto:J.A.Carroll@sussex.ac.uk" target="_blank">J.A.Carroll@sussex.ac.uk</a>> wrote:</div> <br> <div> <div style="overflow-wrap: break-word;">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/. <div><br> </div> <div>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. <div><br> </div> <div>Woodley, can you shed any light on this?</div> <div><br> <div>John</div> <div><br> <blockquote type="cite"> <div>On 10 Nov 2020, at 11:50, Guy Emerson <<a href="mailto:gete2@cam.ac.uk" target="_blank">gete2@cam.ac.uk</a>> wrote:</div> <br> <div> <div dir="ltr"> <div>After loading that file, instead of displaying the incorrect result, LUI now displays nothing. The log file (/tmp/yzlui.debug.ubuntu) says:</div> <div><br> </div> <div>process_complete_command(): `<br> avm 1 #D[natnum-with-copy-wrapper NATNUM: #D[natnum-with-copy RESULT: NATNUM]] "natnum-with-copy-wrapper - expanded"<br> '<br> <br> process_complete_command(): `avm 2 #D[defective-one-wrapper NATNUM: #D[defective-pos SUCC: ZERO]] "defective-one-wrapper - expanded"<br> '<br> </div> <div><br> </div> <div>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)"<br> [#U[constraint 1 [[NATNUM SUCC] ZERO-WITH-COPY ZERO ZERO-WITH-COPY -1] #U[type 0 [NATNUM SUCC RESULT] DEFECTIVE-NATNUM ZERO 1]] '<br> <br> Item in list is not homogeneous (list type 12, item type 3)<br> Path of failure was not a list of symbols (type 12)<br> Item in list is not homogeneous (list type 13, item type 3)<br> YZLUI: Received unknown lkb-protocol top-level command: AVM</div> <div><br> </div> </div> <br> <div> <div dir="ltr">Am Di., 10. Nov. 2020 um 08:29 Uhr schrieb John Carroll <<a href="mailto:J.A.Carroll@sussex.ac.uk" target="_blank">J.A.Carroll@sussex.ac.uk</a>>:<br> </div> <blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <div> <div>Dear Guy, <div><br> </div> <div>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> <br> 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><br> </div> <div>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><br> </div> <div>John</div> <div> <div><br> <blockquote type="cite"> <div>On 9 Nov 2020, at 15:12, Guy Emerson <<a href="mailto:gete2@cam.ac.uk" target="_blank">gete2@cam.ac.uk</a>> wrote:</div> <br> <div> <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" target="_blank"> 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> <span id="gmail-m_6823135890226962798x_gmail-m_1574554418353091205x_cid:f_khaonynj0"><unification-bug.tdl></span></div> </blockquote> </div> <br> </div> <div></div> </div> <div> <div></div> <div><br> </div> </div> </div> </blockquote> </div> </div> </blockquote> </div> <br> </div> </div> </div> </div> </blockquote> </div> <br> </div> <div></div> </div> <div style="overflow-wrap: break-word;"> <div></div> <div><br> </div> </div> <div><debug-unify2-patch.lsp></div></div></blockquote></div></blockquote></div>