What benefits are obtained by allowing the occurrence of free variables and open terms in lambda calculus?

Question

Because of the existence of free variables in lambda calculus, the evaluation of open terms (at least as outlined here) is more complicated relative to the evaluation of closed terms since the evaluator must ensure that the beta-reduction step uses capture-avoiding substitution, i.e., that the variables it substitutes into a term are not free variables of that term.

Combinatory logic can be seen as a subset of lambda calculus that only allows closed terms. Despite this, it is still Turing-complete, and can thus be used to compute everything that lambda calculus can. As such, what are the benefits of allowing free variables and open terms, and the disadvantages of disallowing them? On a related note, why does lambda calculus seem to be a more popular topic of study than combinatory logic despite the apparent shortcoming mentioned? Is the former somehow more relevant and useful to a larger variety of topics than the latter?

Answer 1

A subterm of a closed term is not necessarily a closed term. A calculus of closed terms would have to model open terms as well anyway. Pretty much any definition on terms relies on induction over the structure of the terms, and to define something for closed terms of the form $\lambda x. M$, you need to define that thing for the open term $M$.

There are plenty of models of computation. What's the benefit of using combinator calculus when you can use Turing machines or Conway's game of life? Combinator calculus is a natural model of function application, but doesn't capture function definition. The lambda calculus, with variable names, models function definitions with variable names, which a core concept of most programming languages. For this reason, it's a more useful model of programming languages than combinator calculus.

The point of a theory is not just to be internally simple, it's also to be useful for reasoning.