Jason (jcreed) wrote,
Jason
jcreed

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[1] = f (Y[Z[2]])) ∧ (Y[1] = X[Z[2]])

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 [1] all the way through Y[Z[2]] (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])

and adds the constraint

X'[1] = Y[Z[2]]

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

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

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: math
Subscribe

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 10 comments