For a code similarity detection framework I need to eliminate references to non-local variables, for example having the following closure:
{ var a; var b; var f = function() { a = 5; b = 6; } f(); }
would be converted into something like:
{ var a; var b; var f = function() { var a = 5; var b = 6; return tuple(a, b); } a, b = f(); }
Another approach would be:
{ var world; var a; var b; var f = function(world) { world = update_world(world, "a", 5); world = update_world(world, "b", 6); return world; } world = f(world); a = get_world(world, "a"); b = get_world(world, "b"); }
Basically, convert a stateful program to a purely functional one. The goal is then to transform the resulting program into the lambda calculus, normalize and look for isomorphic subtrees.
Is there a formalization of what I'm trying to do?
Asked By : Philip Kamenarsky
Answered By : babou
Denotational Semantics was an answer almost intended for your question
There is a huge collection of techniques that may be applicable, since the proposed task is basically a compilation process, possibly partial / incremental compilation. The target language is domain extended λ-calculus, which imply some standard transformations such as continuations or passing state as parameter and (part of) result of functions. So it can be described by piecemeal compiler and functional programming bibliography.
But the systematic view of compiling programming languages to λ-calculus is precisely one of the purposes of defining denotational semantics of programming languages, though it is a consequence of the original aim: defining a compositional semantics. Compositionality is precisely what is naturally given by λ-calculus. This is illustrated by the fact that the first environment for building systematically the denotational semantics of a language, P. Mosses'SIS, was also considered the first complete compiler-compiler.
Denotational semantics offers a systematic framework for the stated goal, with a strong and fairly unified theoretical basis.
Basically, convert a stateful program to a purely functional one. The goal is then to transform the resulting program into the lambda calculus, normalize and look for isomorphic subtrees.
Is there a formalization of what I'm trying to do?
Yes, there is a formalization of what you are trying to do, and it has been existing for 35 years, though some techniques may have evolved, It was for example applied to the very imperative language Ada around 1980.
What you want is very precisely and formally what is done by using denotational semantics: transform your stateful program, or program fragment, into a lambda expression. It does use many compiling and functional programming techniques, such as continuations and other higher order functions.
Indeed the structure of the last example in the question, introducing a memory environment called world
is typical of denotational semantics. In denotational semantics world
is a "state mapping" $S:\mathrm{State}$ representing the memory state. This state is passed as argument to all functions, so that functions can access global memory (by whatever means), and returned by function to be available in the calling environment. Of course the $\mathrm{State}$ value returned may differ from the one received as parameter, exactly as the world
value returned by function f
is not the one it received.
For some simple examples, you may look at the question: Denotational semantics of expressions with side effects.
If you have a reference denotational semantics for the language you are considering, then you are sure that no language feature is forgotten in the translation process that could invalidate what you are trying to do.
If you do it on an ad hoc basis for a specific program fragment, you get no garantee that you are taking all you should into consideration.
If you do not have a denotational semantics definitions for your language, you may get ideas from looking at how it handles specific features for other existing languages., or look at the denotational semantics literature in general.
I know denotational semantics does not seem very popular these days. But it was developed and used for that purpose, in addition to more theoretical and abstract aims.
The idea of thus using denotational semantics was pionneered by Peter Mosses with his Semantics Implementation System (SIS)1 developed in the late 1970s. It was doing just that: transform (compile) programs into big lambda expressions according to the denotational semantics of the programming language, which had first to be entered in the system.
There is considerable literature and books on denotational semantics, which you can easily find by searching the web.
Not surprisingly, many of the techniques used are compiler writing techniques, and the system SIS is considered as the first compiler-compiler. Hence much of the literature on compilers can be relevant too, as shown by the important bibliography in the previous answer by Wandering Logic.
The fact is that a denotational semantics specification of a programming language can be read as high-level code for a compiler of the language into lambda calculus, up to some predefined domains of values.
1 Peter Mosses, "SIS: A Compiler-Generator System Using Denotational Semantics," Report 78-4-3, Dept. of Computer Science, University of Aarhus, Denmark, June 1978
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/44454
0 comments:
Post a Comment
Let us know your responses and feedback