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?

  • 1
    $\begingroup$ 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. $\endgroup$
    – Jake
    Sep 29, 2015 at 23:43
  • $\begingroup$ 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.) $\endgroup$
    – MaiaVictor
    Sep 30, 2015 at 0:05
  • $\begingroup$ 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. $\endgroup$
    – Jake
    Sep 30, 2015 at 0:50


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.