Bug in interactive unification

There were some previous threads suggesting that interactive unification wasn’t working properly with append lists:

I’ve done a bit more digging, and I think interactive unification has the following bug: 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 the following small example to illustrate the problem, where the following code is the entire grammar. Note that there is no parsing involved here, just compilation of this file and interactive unification.

; The following types implement the natural numbers,
; using simplest kind of recursion (a single feature SUCC).
; A fully specified natural number is a chain of feature structures,
; with the last feature structure of type "zero",
; and all other feature structure of type "pos".
natnum := *top*.
zero := natnum.
pos := natnum &
  [ SUCC natnum ].

; The following types implement an identity function on the natural numbers,
; in the sense that, for any feature structure compatible with "natnum",
; unifying that feature structure with "natnum-with-copy"
; will produce the original feature structure under RESULT.
natnum-with-copy := natnum &
  [ RESULT natnum ].
zero-with-copy := zero & natnum-with-copy &
  [ RESULT zero ].
pos-with-copy := pos & natnum-with-copy &
  [ SUCC.RESULT #diagonal,
    RESULT.SUCC #diagonal ].

; The following types implement a defective subtype of "natnum",
; in the sense that "defective-natnum" has no common subtype with "zero".
defective-natnum := natnum.
defective-pos := defective-natnum & pos.

; The following types extend the copying function to the defective type.
; However, note that defectiveness is shifted along the number by one:
; "defective-natnum-with-copy" has a RESULT that is just "natnum";
; "defective-pos-with-copy" enforces defectiveness on its RESULT.SUCC.
defective-natnum-with-copy := defective-natnum & natnum-with-copy.
defective-pos-with-copy := defective-natnum-with-copy & defective-pos & pos-with-copy &
  [ RESULT.SUCC defective-natnum ].

; The following are wrapper types, holding a natural number under NATNUM.
; "natnum-with-copy-wrapper" holds the copy operation.
; "defective-one-wrapper" holds the number one (it has one SUCC),
; but where the "pos" is defective.
natnum-wrapper := *top* &
  [ NATNUM natnum ].
natnum-with-copy-wrapper := natnum-wrapper &
  [ NATNUM natnum-with-copy ].
defective-one-wrapper := natnum-wrapper &
  [ NATNUM defective-pos & [ SUCC zero ]].

; The following type would apply the copy operation to the defective number one.
; This would cause a unification failure:
; NATNUM.RESULT.SUCC must be of type "defective-natnum";
; NATNUM.SUCC.RESULT must be of type "zero";
; the above two paths must be re-entrant;
; and there is no common subtype of "defective-natnum" and "zero".
; (Intuitively, the operation pushes the defectiveness along by one,
; but defectiveness is not allowed at the end of the number.)
; Note that neither of the above paths exist in the parent types
; "natnum-with-copy-wrapper" and "defective-one-wrapper".
;fail-wrapper := natnum-with-copy-wrapper & defective-one-wrapper.

; If the above type is uncommented, the LKB correctly throws an error when compiling.
; However, leaving the above type commented out,
; interactive unification of the values of NATNUM
; from "natnum-with-copy-wrapper" and "defective-one-wrapper"
; displays an incorrect result (it does not enforce all the constraints).

; When there is a well-defined result, interactive unification
; does not seem to have a problem with recursive type constraints.
; For example, we can fix the defective type by adding the following two types:
;defective-zero := defective-natnum & zero.
;defective-zero-with-copy := defective-natnum-with-copy & defective-zero & zero-with-copy.

; If these two types are uncommented, interactive unification produces the correct result.
; Similarly, if all three types ("fail-wrapper", "defective-zero", "defective-zero-with-copy")
; are uncommented, the LKB correctly compiles.

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.

1 Like

Thank you for tracking this down, Guy! It sounds like it might be of interest to @sweaglesw, @johnca, and others. It may also be of interest to folks who are on developers but don’t follow this site (like Glenn, Stephan, maybe others).

Good idea, I’ve now posted it to the developers list!

Thank you, Guy!

And you found this bug in interactive unification generally, not in how LUI visualizes it? I remember being able to see a unification failure without LUI but not with it, in cases like you are quoting above.

Could you explain to use interactive unification without LUI?

With the LKB-FOS: start it from the terminal:


and then in the same terminal:


To start it back:



Without LUI, it says unification failed. So it seems the problem is how LUI is integrated with the LKB.

Thanks for the report. Can you post / attach /tmp/yzlui.debug.* after the unexpected behavior? Or it might be hiding in ~/tmp/ or other logon-related tmp directory; and it might be named pangolui.debug.* instead. That should help illuminate whether the issue is LUI failing to display it properly or LKB failing to communicate the failure properly.

Best, Woodley

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

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

process_complete_command(): `avm 3 #D[defective-one-wrapper NATNUM: #D[defective-pos-with-copy RESULT: #D[pos SUCC: DEFECTIVE-NATNUM] SUCC: #D[zero-with-copy RESULT: ZERO]]] "Unification Result"

process_complete_command(): `avm 4 #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 Result"

Depending on which direction I do the interactive unification, a different piece of information gets lost. In the first case, the re-entrancy is missing; in the second case, the “zero” type is missing.

That appears to be a message from LKB indicating unification success rather than failure.

I’ve reproduced this: 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 collects 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 do).

I’m running maclui, and unfortunately I’m not getting a log file in any tmp directory - so I can’t show any diagnostic messages.

1 Like