One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus

Investigations concerned with anti-unification (AU) over $\lambda$-terms have focused on developing algorithms that produce generalizations residing within well-studied fragments of the simply-typed $\lambda$-calculus. These fragments forbid the nesting of generalizations variables, restrict the structure of their arguments, and are \textit{unitary}. We consider the case of nested generalization variables and show that this AU problem is \textit{nullary}, even when the arguments to free variables are severely restricted.