# Is higher-order unification decidable for terms without abstractions within applications?

Consider the problem of higher order unification - that is, finding a substitution for the equation a = b, where a and b are open terms on the lambda calculus, such that a and b have the same alpha-beta normal form. That problem is undecidable in general. Now, consider the case where:

1. b is a closed term on the shape (λ t . (t Y0 Y1 Y2 ...)).
2. a is on the shape (λ t . (t (F X0) (F X1) (F X2) ... )), where F is the only variable.
3. Xn and Yn have no lambdas within applications.

For example, a valid instance of this problem is:

a = (λ t .
(F (λ a b c d . (a (c d) (a (c (c d)) (a (c (c (c d))) b)))))
(F (λ a b c d . (a (c (c d)) (a (c d) (a (c (c (c (c d)))) b)))))
(F (λ a b c d . (a (c (c d)) (a (c (c d)) b)))))

b = (λ t .
(λ a b . (a (a (a (a (a (a b)))))))
(λ a b . (a (a (a (a (a (a (a b))))))))
(λ a b . (a (a (a (a b))))))


The solution is the substitution:

F = (λ l f . (l (λ h t e . (h (t e))) (λ n . n) (λ p e . (f (p e))) (λ z . z)))


Is this problem decidable?

• I'm not sure this is an answer but If you eta-expand each instance of F into x -> F x then a and b are both higher order patterns. Higher order patterns not only have decidable unification but if a unifier exists there is a most general unifier. I'm not sure if the eta expansion will throw off beta equivalence however but my bet is that it will not. So not quite an answer but perhaps progress. – Jake Sep 29 '15 at 23:43
• It is a great progress, but I thought it was restricted to the simply typed lambda calculus? (Although that case probably has a simple type, now that I think about it.) – MaiaVictor Sep 30 '15 at 0:05
• Well I didn't think it had to be simply typed but the handbook of automated reasoning seems to assume simply typed lambda calculus for its terms. So perhaps you are right. Hopefully your specific case can fit into a simply typed setting. – Jake Sep 30 '15 at 0:50