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

<ol>
<li><code>b</code> is a closed term on the shape <code>(λ t . (t Y0 Y1 Y2 ...))</code>.</li>
<li><code>a</code> is on the shape <code>(λ t . (t (F X0) (F X1) (F X2) ... ))</code>, where <code>F</code> is the only variable.</li>
<li><code>Xn</code> and <code>Yn</code> have no lambdas within applications.</li>
</ol>

<p>For example, a valid instance of this problem is:</p>

<pre><code>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))))))
</code></pre>

<p>The solution is the substitution:</p>

<pre><code>F = (λ l f . (l (λ h t e . (h (t e))) (λ n . n) (λ p e . (f (p e))) (λ z . z)))
</code></pre>

<p>Is this problem decidable?</p>

CC BY-SA 3.0
2015-09-29T23:43:15.350Z
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
CC BY-SA 3.0
2015-09-30T00:05:19.947Z
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
CC BY-SA 3.0
2015-09-30T00:50:41.257Z
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
<ds.algorithms><lambda-calculus>
Is higher-order unification decidable for terms without abstractions within applications?
MaiaVictor
# Is higher-order unification decidable for terms without abstractions within applications?

(Asked by: username_0 on 2015-09-29)

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:

b is a closed term on the shape (λ t . (t Y0 Y1 Y2 ...)).
a is on the shape (λ t . (t (F X0) (F X1) (F X2) ... )), where F is the only variable.
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?

**Tags:** ds.algorithms, lambda-calculus
> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.)  
> **username_1**: 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.  

---

## 0 answers

