Functional programming and the closure term birth -

Functional programming and the closure term birth -

i'm studying functional programming , lambda calculus i'm wondering if closure term nowadays in church's original work or it's more modern term strictly concerned programming languages.

i remember in church's work there terms: free variable, closed into..., , on.

consider next function definition in scheme:

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

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

λa λx . (a + x)

when apply value z, becomes

λx . (z + x)

by β-reduction, involves substitution. can phone call closure on a if want.

(the illustration uses function argument, holds true variable binding, since in pure lambda calculus variable bindings must occur via λ terms.)

functional-programming closures lambda-calculus