Monthly Archives: April 2013

Lambda-calculus is Fun!

What do you think of this post?
  • Awesome (16.7%)
  • Interesting (16.7%)
  • Useful (33.3%)
  • Boring (16.7%)
  • Sucks (16.7%)

In my last post I talked about a way to get the Abstract Syntax Tree (AST) from a JavaScript function.

So today I decided to make some experiments with AST manipulation. As an exercise I choose to make pure lambda-calculus logical expressions.

First lets define some nice namespaces so that the code doesn’t get confused with normal JS code and generated code:

var lambda = {}
lambda.logic = {}

Next we define the true and false values as lambda abstractions/functions:

lambda.logic.True = function(a,b) {return a;};
lambda.logic.False = function(a,b) {return b;};

And now the all necessary logical connectives:

lambda.logic.nand = function(a,b) {return (a(b, lambda.logic.False))(lambda.logic.False, lambda.logic.True);};

Yep, thats it NAND its all we need ๐Ÿ˜€ because its functional complete meaning all other logical connectors can be constructed with NAND.

For example a NOT can be defined by:

lambda.logic.not = function(a) {return lambda.logic.nand(a, a);};

This may seems a little confusing but actually is very simple and clever, the True and False functions are the actually boolean values, so the NOT function is called like this:

console.log('not(True) = ' + (lambda.logic.not(lambda.logic.True) === lambda.logic.True?"True":"False"));
console.log('not(False) = ' + (lambda.logic.not(lambda.logic.False) === lambda.logic.True?"True":"False"));

This will print to log console:

not(True) = False 
not(False) = True 

Now lambda-calculus functions are lot of fun for small examples, but not so much when writing an entire program. Therefor I have write a small experimental code to do it for me:

lambda.program = function(prg) {
  var AST = esprima.parse(prg.toString());
  console.log(JSON.stringify(AST, null, 4));

  var str = lambda.gen(AST);
  console.log(str);
  
  return str;
};

lambda.gen = function(prg){
  switch (prg.type) {
    case 'Program':
      var result = '';
      for (var i in prg.body) {
        result += lambda.gen(prg.body[i]) + ';n';
      } 
      return result;
      
    case 'FunctionDeclaration':
      var body = prg.body.body;
      var f = 'function lambda_' + prg.id.name +
        '(' + lambda.genParams(prg.params) + ') {';

      for (i in body) {
        f += lambda.genFuncBody(body[i]);
      }
        
      f += '}';

      return f;
  }

  return "";
  
};

lambda.genParams = function(params) {
  var result, name;
  
  for (i in params) {
    name = params[i].name;
    result = result? result +','+ name : name;
  }
  
  return result; 
};

lambda.genFuncBody = function(body) {
  switch (body.type) {
    case "ReturnStatement":
      return 'return ' + lambda.genFuncBody(body.argument) + ';';
        
    case "UnaryExpression":
      switch (body.operator) {
        case '!':
          return 'lambda.logic.not('+ lambda.genFuncBody(body.argument)+')';
      }
      break;    
        
    case "Identifier":
      return body.name; 
  }

  return "";
};

Now I can write the following test functions in JavaScript:

function not(a) {return !a;}
function not_not(a) {return !(!a);}

And call my lambda.program to convert it to lambda functions:

eval(lambda.program(not));
eval(lambda.program(not_not));

lambd.program(not) will return a string with new function definition and eval will make it executable, the following are the generated functions:

function lambda_not(a) {return lambda.logic.not(a);};
function lambda_not_not(a) {return lambda.logic.not(lambda.logic.not(a));};

To avoid name clashing I used the lambda_ prefix in all generated functions.

And now they can be called like this:

console.log('lambda_not(True) = ' + (lambda_not(lambda.logic.True) === lambda.logic.True?"True":"False"));
console.log('lambda_not(False) = ' + (lambda_not(lambda.logic.False) === lambda.logic.True?"True":"False"));

console.log('lambda_not_not(True) = ' + (lambda_not_not(lambda.logic.True) === lambda.logic.True?"True":"False"));
console.log('lambda_not_not(False) = ' + (lambda_not_not(lambda.logic.False) === lambda.logic.True?"True":"False"));

console output:

lambda_not(True) = False
lambda_not(False) = True
lambda_not_not(True) = True
lambda_not_not(False) = False

Conclusions

Transversing the AST and generating different outputs and functions seems possible and not very difficult but handle all JavaScript possibilities seems a lot of work.
Another thing is that I want to use JS as a proof assistance and simple converting JS functions to pure lambda will not going to help, but generating property or auxiliary functions may prove to be useful.
Other options would probably be creating a tree representing the lambda conversion and apply validation tactics to it.

Well thats it for today, see you soon ๐Ÿ˜€

What do you think of this post?
  • Awesome (16.7%)
  • Interesting (16.7%)
  • Useful (33.3%)
  • Boring (16.7%)
  • Sucks (16.7%)

Javascript Introspection!

What do you think of this post?
  • Awesome (0.0%)
  • Interesting (0.0%)
  • Useful (0.0%)
  • Boring (0.0%)
  • Sucks (0.0%)

For a long time I had been interested in formal proof’s and software validation, mainly because of my librfa project that is a experimental recursive finite automata’s library.

I try to study Coq, but I find it a little difficult to learn and I was unable to convert some of the more complex recursive functions. I started to think in other options more suitable to my capabilities and that would allow me to learn the basic concepts.
Since I mostly work with symbols lambda calculus seems simple enough for me to use.

If I wanted to be able to make a proof of any program I would have to know everything that the program is doing. First I thought on doing a language based on lambda calculus that I could parse and have control over it, also I would need to make available a representation of the language so that it could analyses itself (introspection).
But I got to the conclusion that was a lot of work that I didn’t want to do ๐Ÿ˜€ and start searching for existing solutions:

and off-course JavaScript won ๐Ÿ˜€ …

Something that I learn recently (by repeatably doing the same mistake) is that a function keeps its human representation and can be converted to a string.

Ex.

function add(x, y) {return x+y};
alert(add);

Will display a alert with the message “function add(x, y) {return x+y};” this is because the function object ‘add’ is converted to a string by alert function.

So a more clear example would be:

function add(x, y) {return x+y};
console.log(add.toString());

This code prints “function add(x, y) {return x+y};” to console.

Now that I have a string I can analyze it, but a string is not very convenient for this, fortunately there is great libs to construct JavaScript Abstract Syntax Tree (AST), I have choose the esprima for the job.

Applying esprima parser (code: “esprima.parse(add.toString())”) on the previews add function we get the following json object:

{
    "type": "Program",
    "body": [
        {
            "type": "FunctionDeclaration",
            "id": {
                "type": "Identifier",
                "name": "add"
            },
            "params": [
                {
                    "type": "Identifier",
                    "name": "x"
                },
                {
                    "type": "Identifier",
                    "name": "y"
                }
            ],
            "defaults": [],
            "body": {
                "type": "BlockStatement",
                "body": [
                    {
                        "type": "ReturnStatement",
                        "argument": {
                            "type": "BinaryExpression",
                            "operator": "+",
                            "left": {
                                "type": "Identifier",
                                "name": "x"
                            },
                            "right": {
                                "type": "Identifier",
                                "name": "y"
                            }
                        }
                    }
                ]
            },
            "rest": null,
            "generator": false,
            "expression": false
        }
    ]
}

Off-course changing the AST tree doesn’t affect the real JavaScript code, but its possible to convert the AST back to JavaScript and run it (I hope there is a lib for this ๐Ÿ˜€ ).

This gives a lot of possibilities in run time:

  • Code Analyzes,
  • Code injection,
  • Code transformations/conversions,

Well for now this is pretty much what I have, I hope to write more about this subject.

What do you think of this post?
  • Awesome (0.0%)
  • Interesting (0.0%)
  • Useful (0.0%)
  • Boring (0.0%)
  • Sucks (0.0%)