Lambda-calculus using javascript

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

Until now I have been loosely using JavaScript to represent lambda-calculus, but to get things right I have to define a strict lambda-calculus JavaScript API.

Everything that follows is from my understanding of lambda-calculus, if anything is wrong please fell free to contact me by email or comment on this post.

JavaScript Lambda Definitions

Variables (I think its called term’s but: We call it variables out here!)

The most basic lambda-expression is a variable, in the context of lambda-calculus a variable is a value that can be replaced by other value. Normally a variable is represented by a letter but with JavaScript I will represent it like this:

Lambda.Variable = function (varname) {
  this.varname = varname;
};

Where varname its a string with the name of my variable.

All Lambda.Variable’s are lambda-expressions.

Abstractions

An abstraction is represented like this {lambda}x.M where x is a variable and M is a lambda-expression.
Abstractions are similar to functions, example: {lambda}x.x is the same as f(x) = x.

An abstraction can only have one variable as argument, example’s:

  • f(x,y) = xy is the same as {lambda}x.{lambda}y.xy
    , don’t assume that xy is the same as x*y because that is wrong;
  • Lets assume that binary math operator * (multiplication) is defined as a lambda-abstraction that can take two arguments and multiply them. The function f(x,y) = x*y can be written as {lambda}x.{lambda}y.* x y.

Notation:
There are some conventions to abbreviate lambda-expression, for example {lambda}x.{lambda}y.* x y can be abbreviated as {lambda}xy.* x y, but for learning I think its better to use the extended version to avoid mistakes and to have a better understanding of what is going on.

With JavaScript I represent lambda-abstraction like this:

Lambda.Abstraction = function (x, M, name) {
  this.x = x;
  this.M = M;
  this.name = name;
};

The name is not needed for lambda-calculus, I use it here to bind a human name to an abstraction.

All Lambda.Abstractions are lambda-expressions.

Applications

Let M and N be lambda-expressions, then (M N) is a lambda-application. All lambda-applications are lambda-expressions.

You can think of applications as a function call, or something like that, examples:

  • ({lambda}x.{lambda}y.xy) a is an application and can be reduced to the abstraction {lambda}y.ay
  • ({lambda}x.{lambda}y.xy) a b is an application and can be reduced to the application {(lambda}y.ay) b, that can also be reduced to the application (a b).

With JavaScript I represent lambda-application like this:

Lambda.Application = function (M, N) {
  this.M = M;
  this.N = N;
};

All Lambda.Applications are lambda-expressions.

Parentheses ()

In lambda-calculus parentheses () can be used to express or force lambda-expressions order. In my code I don’t need them because order is implicit in my JS Lambda objects hierarchy.

Usage

The following examples demonstrates how to use the above definitions.

  1. {lambda}x.{lambda}y.x (Lambda Logic True):
    1. Create variables x and y,
          var x = new Lambda.Variable ('x');
          var y = new Lambda.Variable ('y');
         
    2. Create the inner most abstraction,
          abstraction_y = new Lambda.Abstraction (y, x); 
      
    3. Create the final abstraction,
          True = new Lambda.Abstraction (x, abstraction_y, 'True'); 
      

      The ‘True’ string will be used only for displaying purposes.

    4. Final code,
          var x = new Lambda.Variable ('x');
          var y = new Lambda.Variable ('y');
      
          abstraction_y = new Lambda.Abstraction (y, x); 
          True = new Lambda.Abstraction (x, abstraction_y, 'True'); 
      

      The Lambda.Variable varname will be used only for displaying purposes so varname is never used in code to identify a variable.

    5. True.toString(): True={lambda}x.{lambda}y.x
  2. ({lambda}x.{lambda}y.x) ({lambda}x.{lambda}y.x) ({lambda}x.{lambda}y.x) (Application)
    1. To make things easier this ({lambda}x.{lambda}y.x) will be defined as:

      function True () {
          var x = new Lambda.Variable ('x');
          var y = new Lambda.Variable ('y');
          return new Lambda.Abstraction (x, new Lambda.Abstraction (y, x), 'True'); 
      }
      
    2. The application ({lambda}x.{lambda}y.x) ({lambda}x.{lambda}y.x) ({lambda}x.{lambda}y.x)

         var app = new Application (new Application (True, True), True);
        
    3. All code,

      function True () {
          var x = new Lambda.Variable ('x');
          var y = new Lambda.Variable ('y');
          return new Lambda.Abstraction (x, new Lambda.Abstraction (y, x), 'True'); 
      }
         var app = new Application (new Application (True, True), True);
        
    4. app.toString(): ((True={lambda}x.{lambda}y.x True={lambda}x.{lambda}y.x) True={lambda}x.{lambda}y.x)

Variables Scope

There is no real scope mechanism in my api, I just assume that the lambda-expressions are constructed correctly.

For example:

var x = new Lambda.Variable ('x');
var y = new Lambda.Variable ('y');
var True = new Lambda.Abstraction (x, new Lambda.Abstraction (y, x), 'True'); 

The variables x is bound to True.

But in this case:

var x = new Lambda.Variable ('x');
var y = new Lambda.Variable ('y');

var x1 = new Lambda.Variable ('x');
True = new Lambda.Abstraction (x, new Lambda.Abstraction (y, x1), 'True'); 
}

The variable x and x1 are not the same and so x1 is a free variable on True.

Free and Bound Variables (Extending API)

“The abstraction operator (lambda) is said to bind its variable wherever it occurs in the body of the abstraction. Variables that fall within the scope of an abstraction are said to be bound. All other variables are called free”

The algorithm is very simple:

  1. All functions keep track of two array’s free and bound and free and bound variables are inserted to the corresponding array,
  2. Abstraction and Application call the function “variables” on their own children’s passing the free and bound arrays as argument,
  3. The variable argument (x) of an Abstraction is always bound,
  4. If a variable is in bound array than it’s bound else it’s free.

The following code extends Lambda.Variable, Lambda.Abstraction and Lambda.Application with a variables function, this function returns all bound and free variables.

Lambda.Variable.prototype.variables = function (vars) {

  vars = vars || {bound: [], free: []};

  if (vars.bound.indexOf (this) === -1) {
    if (vars.free.indexOf (this) === -1) {
      vars.free.push (this);
    }
  }

  return vars;
};

Lambda.Abstraction.prototype.variables = function (vars) {
  vars = vars || {bound: [], free: []};

  vars.bound.push (this.x);

  return this.M.variables (vars);
};

Lambda.Application.prototype.variables = function (vars) {
  vars = this.M.variables (vars);
  vars = this.N.variables (vars);

  return vars;
};

Alpha-Conversion (Extending API)

“Alpha-conversion, sometimes known as alpha-renaming, allows bound variable names to be changed.”

Actually I will just ignore renaming and will implement a more replacing function, so renaming would be more like replacing a variable with other variable.

And the code for this is very simple:

Lambda.Application.prototype.alphaConversion = function (variable, value) {
  this.M = this.M.alphaConversion (variable, value);
  this.N = this.N.alphaConversion (variable, value);

  return this;
};

Lambda.Abstraction.prototype.alphaConversion = function (variable, value) {
  this.x = this.x.alphaConversion (variable, value);
  this.M = this.M.alphaConversion (variable, value);

  return this;
};

Lambda.Variable.prototype.alphaConversion = function (variable, value) {
  return (this === variable)?value: this;
};

Beta-Reduction (Extending API)

“Beta-reduction captures the idea of function application. Beta-reduction is defined in terms of substitution”

In this case I choose not to implement a recursive beta-reduction algorithm instead I implemented a some kind of step-by-step algorithm. So the following code will not
completely reduce a lambda-expression but every time betaReduction is called part of the lambda expression will be reduced.

The algorithm that I use and hopefully correct is like this:
Application: if M is an abstraction apply application argument N, else if is an application try to reduce it, else just return itself.

Lambda.Application.prototype.betaReduction = function () {
  if (this.M instanceof Lambda.Abstraction) {
    return this.M.betaReduction(this.N);
  }
  else if (this.M instanceof Lambda.Application) {
    this.M = this.M.betaReduction();
  }

  return this;
}

Abstraction: If a value is passed then replace the Abstraction argument (x) on the abstraction body (M) and return the result else return itself:

Lambda.Abstraction.prototype.betaReduction = function (value) {
  var r = this;

  if (value) {
    r = this.M.alphaConversion (this.x, value);
  }

  return r;
}

Variables: are irreducible and beta-reduction will always return variable itself:

Lambda.Variable.prototype.betaReduction = function () {
  return this;
};

Clone (Extending API)

Some functions like Alpha-Conversion and Beta-Conversion are destructive.
The simplest way to avoid a lambda-expression to be changed by this functions its to apply them to a clone.

And the code to clone a lambda-expression is like this:

Lambda.Variable.prototype.clone = function (vars) {
  vars = vars || {original: [], replace: []};
  
  var index = vars.original.indexOf(this);
  if (index === -1) {
     var x = new Lambda.Variable (this.varname);
     vars.original.push(this);
     vars.replace.push(x);
     return x;
  }
  else {
    return vars.replace[index];
  }
};

Lambda.Abstraction.prototype.clone = function (vars) {
  vars = vars || {original: [], replace: []};
  
  var v = this.x.clone(vars);
  this.M.clone(vars).alphaConversion (this.x, v);
  return new Lambda.Abstraction (v, this.M.clone(vars).alphaConversion (this.x, v));
};

Lambda.Application.prototype.clone = function (vars) {
  return new Lambda.Application (this.M.clone(vars), this.N.clone(vars));
};

Some Tests

To test it I choose a interesting example, a lambda tuples implementation:
pair = {lambda}abf.fab
first = {lambda}p.p({lambda}ab.a)
second = {lambda}p.p({lambda}ab.b)

So this is done like this:

Lambda.Container = {};
Lambda.Container.Pair = function () {
  var a = new Lambda.Variable ('a');
  var b = new Lambda.Variable ('b');
  var f = new Lambda.Variable ('f');

  return new Lambda.Abstraction (
    a,
    new Lambda.Abstraction (
      b,
      new Lambda.Abstraction (
        f,
        new Lambda.Application (
          new Lambda.Application (f, a),
          b
        )
      )
    ),
    'Pair'
  );
};


Lambda.Container.First = function () {
  var a = new Lambda.Variable ('a');
  var b = new Lambda.Variable ('b');
  var p = new Lambda.Variable ('p');

  return new Lambda.Abstraction (
    p,
    new Lambda.Application (
      p,
      new Lambda.Abstraction (
        a, new Lambda.Abstraction (b,a)
      )
    ),
    'First'
  );
};

Lambda.Container.Second = function () {
  var a = new Lambda.Variable ('a');
  var b = new Lambda.Variable ('b');
  var p = new Lambda.Variable ('p');

  return new Lambda.Abstraction (
    p,
    new Lambda.Application (
      p,
      new Lambda.Abstraction (
        a, new Lambda.Abstraction (b,b)
      )
    ),
    'Second'
  );
};

And can be used like this:

  function pair (a, b) {
    return new Lambda.Application (new Lambda.Application (Lambda.Container.Pair(), a) , b);
  };

  function first (a) {
    return new Lambda.Application (Lambda.Container.First(), a);
  };

  function v(a) {
    return new Lambda.Variable (a);
  };
  
  var fruits1 = pair(v("morangos"), v("abacaxi"));
  print ("fuits1: " + fruits1.toString());

  fruits1 = fruits1.betaReduction()
  print ("fuits1: " + fruits1.toString());

  fruits1 = fruits1.betaReduction()
  print ("fuits1: " + fruits1.toString());

  var beta = first(fruits1);
  print ("beta: " + beta.toString());

  beta = beta.betaReduction();
  print ("beta: " + beta.toString());

  beta = beta.betaReduction();
  print ("beta: " + beta.toString());

  beta = beta.betaReduction();
  print ("beta: " + beta.toString());

  beta = beta.betaReduction();
  print ("beta: " + beta.toString());

The output would be:

  1. fuits1: ((Pair={lambda}a.{lambda}b.{lambda}f.((f a) b) morangos) abacaxi)
  2. fuits1: ({lambda}b.{lambda}f.((f morangos) b) abacaxi)
  3. fuits1: {lambda}f.((f morangos) abacaxi)
  4. beta: (First={lambda}p.(p {lambda}a.{lambda}b.a) {lambda}f.((f morangos) abacaxi))
  5. beta: ({lambda}f.((f morangos) abacaxi) {lambda}a.{lambda}b.a)
  6. beta: (({lambda}a.{lambda}b.a morangos) abacaxi)
  7. beta: ({lambda}b.morangos abacaxi)
  8. beta: morangos

Conclusion

Lambda Calculus is a lot of fun and this post is too big, yet to small ;).

I think this representations is pretty simple and uses some JavaScript features making it good to compile JavaScript to this representation.

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

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>