CODEWITHSUNDEEP
javascriptfunctionhaskellclosurescompiler-theory
smoes
smoes

Reputation: 601

Formal defintion of function closures in computer science

at the moment I am writing a scientific expose. A part of the content is about the definition of closures in our developed DSL. However, I was not able to find references of how to formally describe function closures in computer programming. I must admit I have searched in only a handful of programming books. Without any success.

What I really need is the formal, precise and maybe mathematical definition of the concept of function closure in computer programming. Using a formal definition we may find a way to define our special kind of closures in a convenient and precise way.

Is there any standard notation/description out there? If not maybe one of you theorist can give me a hint, how to elegantly describe them ;)

Upvotes: 2

Views: 177

Answers (1)

smoes
smoes

Reputation: 601

So, since I already created a definition on my own, I want to share it with everyone, that is looking at this question.

The following definition is a short version and product of my own thoughts, so do not simply adopt it without thinking through it.

Closures are an implementation technique to implement lexically scoped name binding.

The operational view of a closure is the tuple of an environment E that binds free variables of the function f, and f itself: (E,f). Let E[in1] = x bind the value of in1 to an arbitrary x. The application foo(in2) of the closure (E, foo(in1, in2)) gets then evaluated to the same result, as foo(x, in2).

Other than partial evaluation, the functions source code is not duplicated. The environment is evaluated at run-time.

What do you think?

Upvotes: 1

Related Questions