Functional programming and the closure term birth

Question

I'm studying functional programming and lambda calculus but I'm wondering if the closure term is also present in the Church's original work or it's a more modern term strictly concerned to programming languages.

I remember that in the Church's work there were the terms: free variable, closed into..., and so on.

Answer 1

Consider the following function definition in Scheme:

(define (adder a)
  (lambda (x) (+ a x)))

The notion of explicit closure is not required in the pure lambda calculus, because variable substitution takes care of it. The above code snippet can be translated

λa λx . (a + x)

When you apply this to a value z, it becomes

λx . (z + x)

by β-reduction, which involves substitution. You can call this closure over a if you want.

(The example uses a function argument, but this holds true for any variable binding, since in the pure lambda calculus all variable bindings must occur via λ terms.)

Answer 2

It is a more modern term, due to (as many things in modern FP are), P. J. Landin (1964), The mechanical evaluation of expressions

Also we represent the value of a λ-expression by a bundle of information called a "closure," comprising the λ-expression and the environment relative to which it was evaluated.