Found an alarming counterexample to my expectations about the termination of higher-order unification. I hope I'm just being really stupid here and missing something obvious.

Suppose the signature is
o : type.
f : o -> o.

Imagine everything lives in a (deBruijn-indexed) context that consists of two variables of type o.

Consider the unification equations

(X = f (Y[Z])) ∧ (Y = X[Z])

where all the existential variables X, Y, Z are variables in contextual-modal-type-theory style, of type (o ⊦ o).

Say the algorithm looks at the first equation. It can't push the inverse of  all the way through Y[Z] (since it knows only that at least one of Y or Z must project out its argument, but it doesn't know which one(s) will) so it tries to make progress by at least using the information that X starts with an application of f. It makes up a new variable X', instantiates

X := f (X'[id])

X' = Y[Z]

After eliminating the equation with X on the left, carrying out the substitution and conjoining the new constraint onto the right, we get

(Y = f (X'[Z])) ∧ (X' = Y[Z])

which is just an alpha-rewrite (X ↦ Y, Y ↦ X') of the original set of equations, so we haven't made any progress.

Below is some twelf code that illustrates the problem, with a %query not terminating, despite a %terminates check. I feel like I should be able to twist this into a simple type-checking problem, but my brain hasn't coughed it up yet.

```o : type.
k : o.
f : o -> o.

eq : o -> o -> o -> type.
eq/refl : eq DUMMY M M.

test : o -> type.

test/ : {X : o -> o} {Y : o -> o} {Z : o -> o}
test DUMMY <- ({a} {b} eq DUMMY (X a) (Y (Z b)))
<- ({a} {b} eq DUMMY (Y a) (f (X (Z b)))).

%mode eq +DUMMY *A *B.
%terminates DUMMY (eq DUMMY A B).
%mode test +DUMMY.
%terminates DUMMY (test DUMMY).

%query 1 1 D : test k.```

Another update: Frank's reply to my twelf-bearing email contains the word "Oops", so I guess I have found a real bug in the implementation and am not discovering known problems. I've mixed feelings: finding bugs is good, but bugs being there to be found is bad.
Tags:
• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic