2

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 ;)

Aadit M Shah
  • 72,912
  • 30
  • 168
  • 299
smoes
  • 591
  • 2
  • 17
  • 1
    Would this Wikipedia [article](http://en.wikipedia.org/wiki/Closure_(computer_programming)) be a good start? – Alexander Kogtenkov Oct 23 '14 at 21:02
  • Thank you for your hint. I already stumbled across the article. And the answer to your question is "barely". It describes by examples what it means for specific languages and not how the concept can be described in general. – smoes Oct 24 '14 at 07:36
  • Perhaps this answer would be helpful: http://stackoverflow.com/a/12931785/783743 – Aadit M Shah Apr 20 '15 at 17:45
  • 1
    I don't think there's a mathematical definition of the concept. In Haskell, you'd just use a partial application of a function to create a "closure". It all comes down to scoping rules, which are very much language-specific. – Bergi Apr 20 '15 at 18:11

1 Answers1

1

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?

smoes
  • 591
  • 2
  • 17
  • 2
    Closures are an implementation technique. They are not a language feature or a theoretical construct. They may come and go in the course of optimization. It's not clear to me, therefore, what purpose a formal definition could serve, or whether a formal definition could properly capture the right ideas. – dfeuer Apr 21 '15 at 17:46
  • 1
    Thank you for your answer dfeuer. You are completely right. I changed my answer and laid the focus on the operational view of a closure. I used the terminus from https://en.wikipedia.org/wiki/Closure_%28computer_programming%29. In my opinion it is important to have a straight forward theoretical definition of the mechanics behind closures, to reason in a scientific context. – smoes Apr 22 '15 at 08:40