Category Archives: lambda-calculus

JavaScript to Lambda-Calculus: GaloJS

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

Good news everyone 馃榾 …

The GaloJS is now able to convert a simple JavaScript function to lambda-calculus and can execute alpha conversion and beta (normal) reduction.

As a test I use the factorial function:

 function fac(n) {
   if (n === 0) {
     return 1;
   }
   else {
     return n * fac(n-1);
   }
 }

Well the function is not well defined because it doesn’t guarantee that n is a positive integer, but I want to keep things simple.

So GaloJS is now capable to convert the function to lambda-calculus and it looks like this:

 fixpoint 位fac.位n. (
     (=== n (位f.位x.x)) 
        (位f.位x.f (x)) 
        (* n (fac (- n (位f.位x.f (x))))))

You are probably thinking that I am cheating with the === and * and fixpoint, but no I actually defined a “std lib” for it, and it goes like this:

((位fixpoint.((位false.((位true.((位nand.((位!.((位&&.((位||.
((位isZero.((位pred.((位*.((位+.((位-.((位< =.((位===.

(fixpoint (位fac.(位n.((((=== n) (位f.(位x.x))) (位f.(位x.(f x)))) 
((* n) (fac ((- n) (位f.(位x.(f x))))))))))

) (位m.(位n.((&& ((<= m) n)) ((<= n) m)))))
) (位m.(位n.(isZero ((- m) n)))))) 
(位m.(位n.((n pred) m))))) (位m.(位n.((n succ) m))))) 
(位m.(位n.(位f.(m (n f))))))) 
(位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u))))))) 
(位n.((n (位x.false)) true)))) (位p.(位q.((nand (! p)) (! q)))))) 
(位p.(位q.(! ((nand p) q)))))) 
(位p.((nand p) p)))) 
(位p.(位q.((((p q) false) false) true))))) 
(位x.(位y.x)))) 
(位x.(位y.y)))) (位f.((位x.(f (x x))) (位x.(f (x x))))))

Seems complicated but it isn't, its just messy, basically what I do is "bind" a "function" to a name by nesting "functions", for example the fixpoint is defined here as a Y combinator (can you find it in the above lambda expression? lol):

(位fixpoint.body) (位f.(位x.f (x x)) (位x.f (x x)))

So on beta reduction all fixpoint occurrences in the body will be replaced by the Y combinator, so if the body is:

 fixpoint 位fac.位n. (
     (=== n (位f.位x.x)) 
        (位f.位x.f (x)) 
        (* n (fac (- n (位f.位x.f (x))))))

It will became:

 (位f.(位x.f (x x)) (位x.f (x x))) 位fac.位n. (
     (=== n (位f.位x.x)) 
        (位f.位x.f (x)) 
        (* n (fac (- n (位f.位x.f (x))))))

Alpha Conversion

Alpha conversion is basically variable rename, like this:

(位x.(位y.x)) => rename x to a => (位a.(位y.a))
(位x.(位y.x)) => rename y to a => (位a.(位a.x))

Alpha conversion has been a pain to implement, not that its incredible difficult its just tricky and because I want to use it in beta reduction I am still fuzzy on how should my alpha conversion behave in some cases.

Variable Capture

I think variable capture is when a substitution of a free variable results in a bound variable (the free variable is captured).

For example: (位x.(位y.x f)) alpha conversion x to f will result in the capture of free variable f as a bound variable (位f.(位y.f f)).

Other example can be:
(位x.(位y.x)) alpha conversion x to y, x is a bound variable but is free where the alpha conversion will occur (位y.x) ,so the conversion will result in (位y.(位y.y)).

The problem with variable capture is that if the substitution is made it will change the
meaning of the original expression.

for example: (位x.(位y.x f)) 1 => (位y.1 f) but renaming x to f => (位f.(位y.f f) and then do the same as before (位f.(位y.f f) 1 => (位y.1 1) =/= (位y.1 f).

In this cases, by definition, alpha conversion is not possible but we can avoid variable capture by renaming bound variables:

(位x.(位y.x)) => rename y to y1 => (位x.(位y1.x)) 
=> rename x to y => (位y.(位y1.y))

Beta Reduction

There is a couple of beta reduction strategy’s, I think beta normal reduction is
guarantied to find a lambda-expression that cant be reduced no more if such expression
exists, for example if I try beta normal reduction on my factorial example without arguments it will expand to infinity because it will always be able to apply Y combinator but if I give it a argument (a church numeral) it will reduce to factorial result (a church numeral),
this is because the Y combinator will disappear when the stop condition (n===0) is true.

Variable Capture

Variable capture can occur in beta reduction and must avoided (using bound variable renaming) to complete beta reduction.

For example:

 
(位x.(位y.x)) y a 
=> (位y.y) a 
=> a 

witch is wrong, the reduction should be like this:

(位x.(位y.x)) y a 
=> (位y1.y) a 
=> y 

A more complex example:

(位x.(位y.x)) (位x.(位y.y)) (位x.(位y.x)) 
=> (位y.(位x.(位y.y))) (位x.(位y.x)) 
=> (位x.(位y.y))

In this case I think there is no need to rename variables, because there is no variable
capture, all substitutions have bound variables.

One last example:

(位x.(位y.x)) (x y) z
=> (位y.x y) z
=> x z

witch is wrong, it should be:

(位x.(位y.x)) (x y) z
=> (位y1.x y) z
=> x y

GaloJS: factorial beta normal reduction

The following are some examples of beta reduction of factorial:

fac (位f.位x.x) // (位f.位x.x) church numeral 0, fac 0
=> (位f.位x.f x) // result 1  
fac (位f.位x.f x) // fac 1 
=> * (位f.位x.f x) (fac 0) 
=> * (位f.位x.f x) (位f.位x.f x) 
=> (位f.位x.f x)  // result 1
fac (位f.位x.f (f x)) // fac 2 
=> * (位f.位x.f (f x)) (fac 1) 
=> * (位f.位x.f x) (位f.位x.f x) 
=> (位f.位x.f (f x))  // result 2
fac (位f.位x.f (f (f x))) // fac 3 
=> * (位f.位x.f (f (f x))) (fac 2) 
=> * (位f.位x.f x) (位f.位x.f (f x)) 
=> (位f.位x.f (f (f (f (f (f x))))))  // result 6

Unfortunately GaloJS doesn’t produce such easy to read outputs,
a intermediate step looks more like this mess:

=> fac 3
...
(位f.(位x.(f (f (f (f (f (f ((位u.x) ((((位x.((位fac.(位n.(((((位m.(位n.(((位p.(位q.((位p.(((位p.(位q.((((p q) (位x.(位y.y))) (位x.(位y.y))) (位x.(位y.x))))) p) p)) (((位p.(位q.((((p q) (位x.(位y.y))) (位x.(位y.y))) (位x.(位y.x))))) p) q)))) (((位m.(位n.((位n.((n (位x.(位x.(位y.y)))) (位x.(位y.x)))) (((位m.(位n.((n (位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u)))))) m))) m) n)))) m) n)) (((位m.(位n.((位n.((n (位x.(位x.(位y.y)))) (位x.(位y.x)))) (((位m.(位n.((n (位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u)))))) m))) m) n)))) n) m)))) n) (位f.(位x.x))) (位f.(位x.(f x)))) (((位m.(位n.(位f.(m (n f))))) n) (fac (((位m.(位n.((n (位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u)))))) m))) n) (位f.(位x.(f x))))))))) (x x))) (位x.((位fac.(位n.(((((位m.(位n.(((位p.(位q.((位p.(((位p.(位q.((((p q) (位x.(位y.y))) (位x.(位y.y))) (位x.(位y.x))))) p) p)) (((位p.(位q.((((p q) (位x.(位y.y))) (位x.(位y.y))) (位x.(位y.x))))) p) q)))) (((位m.(位n.((位n.((n (位x.(位x.(位y.y)))) (位x.(位y.x)))) (((位m.(位n.((n (位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u)))))) m))) m) n)))) m) n)) (((位m.(位n.((位n.((n (位x.(位x.(位y.y)))) (位x.(位y.x)))) (((位m.(位n.((n (位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u)))))) m))) m) n)))) n) m)))) n) (位f.(位x.x))) (位f.(位x.(f x)))) (((位m.(位n.(位f.(m (n f))))) n) (fac (((位m.(位n.((n (位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u)))))) m))) n) (位f.(位x.(f x))))))))) (x x)))) (((位m.(位n.((n (位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u)))))) m))) (((位m.(位n.((n (位n.(位f.(位x.(((n (位g.(位h.(h (g f))))) (位u.x)) (位u.u)))))) m))) (位f.(位x.(f (f (f x)))))) (位f.(位x.(f x))))) (位f.(位x.(f x))))) f))))))))))
...
=> (位f.(位x.(f (f (f (f (f (f x))))))))

Not very pretty, but it works :D.

GaloJS: Future work

GaloJS only converts very simple functions, it doesn’t support imperative programming,
this means it doesn’t know how to deal with statements.

So this will be a challenging and interesting problem to solve, I think it can be
done with monoids or monads.

Other thing that I want to do is investigate what useful things can be done with what I already have, bottom line is that it will be a nice lambda-calculus teaching tool :D.

What do you think? Let me now in the comments.

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

Lambda-calculus recursion with factorial example (Part 2, anonymous recursive function – fixpoint)

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

On my last post I presented a solution to write the recursive factorial function with anonymous recursive function, but there is a better and more general way to write recursive functions, it is called fix-point combinator and one well-known (and perhaps the simplest) fixed-point combinator in the untyped lambda-calculus is called the Y combinator. It was discovered by Haskell B. Curry, and is defined as:

Y = {lambda}f.({lambda}x.f (x x)) ({lambda}x.f (x x))

Translating lambda-calculus to JavaScript is not a easy task because they do not operate in the same way. JavaScript is a practical programming language and lambda-calculus is a theoretical language that is much more close to a simple mechanical operation.

Example:

function add (a, b) { return a + b;}

In lambda-calculus this should be written in JavaScript as:

function add (a) {
   return function (b) {
        return (a+b)
   }
}

And execution is like this:

add (1) (2);

Everything in lambda-calculus is mostly functions, and all function are lazy evaluated, this is important when we want to translate lambda-calculus to JavaScript because JavaScript evaluates most of expression early.

Fixpoint Y-Combinator in JavaScript

This is one of does examples that are much more simple in lambda-calculus that are in JavaScript or maybe I am just misunderstanding the Y fix-point combinator…
Anyway this is what I got:

function Y (f) 
  {return function (x) {
    return function () { 
      return f (
	function () {return x (x);}
      )
      (
        function (x) {
	  return function () {
	    return f (
	      function (x) {return x(x);}
	    );
	}
      }
    );
   }
  }
}

You can see that all functions return a function as result but this is mostly because we don’t want the function to be executed right away, we want to return a function as result and then apply it if necessary, otherwise we will make a infinity function call that would result in stack overflow.

Writing Factorial with Fixpoint Y-Combinator in JavaScript

The factorial function,

function factorial (n) {
  if (n === 0) {
     return 1;
  }
  else if (n > 0) {
     return factorial (n-1) * n;
  }
}

Now I need to change the function to work with the Y combinator, something like this:

function fact (self) {
	return function () {
        // I think this dummy function is unnecessary 
        // but this is executed with no argument at 
        // initialization and I don't know why...
		return function (n) {
			if (n === 0) {
				return 1;
			}
			else if (n > 0) {
				return (self () (self) (n-1)) * n;
			}
		}
	};
}

Once again I return functions to avoid early execution. The function self is not really the function itself but the function constructed with the Y combinator.

The recursive function is initialized like this:

var factorial = Y (fact) (Y (fact)) ();

console.log (factorial (0)); // print 1
console.log (factorial (4)); // print 24

Putting it all together!

Next code is kind of messy thats why I am wondering if this is the correct way to do it, but it works…

console.log (

function (
  Y
) {
  return function (fact) {
    return function (factorial) {
      return "factorial (0) = " + factorial(0) + "n" +
	     "factorial (1) = " + factorial(1) + "n" +
	     "factorial (2) = " + factorial(2) + "n" +
	     "factorial (3) = " + factorial(3) + "n" +
	     "factorial (4) = " + factorial(4) + "n" +
	     "factorial (5) = " + factorial(5) + "n" ;
    } (
      Y (fact) (Y(fact)) ()
    )
 } (
   function (self) {
     return function () {
       return function (n) {
	 if (n === 0) {
	   return 1;
	 }
	 else if (n > 0) {
	     return (self () (self) (n-1)) * n;
      	 }
       }
     };
   }
   );
}
(
  function (f) {
    return function (x) {
      return function () { 
	return f (
	  function () {return x (x);}
	)
	(
	  function (x) {
	    return function () {
	      return f (
		function (x) {return x (x);}
	      );
	    }
	  }
	);
      }
    }
})

);

The output would be

factorial (0) = 1
factorial (1) = 1
factorial (2) = 2
factorial (3) = 6
factorial (4) = 24
factorial (5) = 120

Other way

When I was playing with fix-points I made a code prototype that actually works, but is much more simple than the code above so something must be wrong,
anyway the code is very simple,

function (
  fixpoint	
) {
  return function (
    factorial
  ) {
    // execute factorial  
    return factorial (4); // return 24
  } (
    fixpoint (function (fact) {
      return function (n) {
	if (n === 0) {
	  return 1;
        }
	else if (n > 0) {
	  return fact (fact) (n-1) * n;
	}
      }
    })
  );
} (
	function fixpoint (f) {
		return function (x) {
			return x (x);
		} (
			function (x) {
				return f (x);	
			}
		)
	}
};
)
What do you think of this post?
  • Awesome (0.0%)
  • Interesting (0.0%)
  • Useful (0.0%)
  • Boring (0.0%)
  • Sucks (0.0%)

Lambda-calculus recursion with factorial example (Part 1, Recursive anonymous functions)

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

Hi,

My last post about lambda-calculus just sucks, I know that because most of my readers (almost 3 people) voted that it sucks. So this time I will try to write a more interesting and fun post :) and whats better than recursive functions, especially if they are anonymous.

First lets write a nice factorial function in JavaScript:

function factorial (n) {
    if (n === 0) {
        return 1;
    }
    else if (n > 0) {
        return factorial (n-1) * n;
    }
};

Recursive anonymous functions

Now the interesting part is that lambda-calculus only uses anonymous functions, so the
above function must be rewritten, the next section is a solution that I came up with:

  1. A function parameter can be used to “name” a function like this,

    function (factorial, n) { ... }
    
  2. Since we added a new argument to the function we need to modify the call to reflect the changes,

    function (factorial, n) {
        if (n === 0) {
            return 1;
        }
        else if (n > 0) {
            return factorial (factorial, n-1) * n;
        }
    };
    
  3. now we only need a function to call the recursive process,

    function (factorial, n) {
        return factorial(factorial, n);
    }
    (
        function (factorial, n) {
            if (n === 0) {
                return 1;
            }
            else if (n > 0) {
                return factorial (factorial, n-1) * n;
            }
        },
        3 // Calculate 3!, result 6
    );
    
  4. and just for convenience we can use parameters to give a function “name” instead of applying values directly to the definition,

    alert (
    function (factorial) {
       return " => " + factorial (0) + ", " + factorial (1) + ", " + factorial (3);
    } (
        function (n) {
            return function (factorial, n) {
                return factorial (factorial, n);
            }
            (
                function (factorial, n) {
                    if (n === 0) {
                        return 1;
                    }
                    else if (n > 0) {
                        return factorial (factorial, n-1) * n;
                    }
                },
                n
            )
        }
    )
    );

Using a mix of JavaScript and lambda-calculus the previews function will look like this:

(
  {lambda}factorial.factorial 3 // calculate 3!
)(
  // function (n)
  {lambda}n.
    // function (factorial, n) {return factorial(factorial,n)}
    ({lambda}factorial n.factorial factorial n)
    // and finally the actual factorial function,
    (
       {lambda}factorial n.
           if (n === 0) {lbrace} 1 {rbrace} 
           else if (n > 0) {lbrace} (factorial factorial n-1) * n {rbrace}
    )
)

And thats it, on next parts I will talk about lambda-calculus logical expression like if-then-else and natural numbers representation and handling.

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

GaloJs – A JavaScript Proof Assistence Project.

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

For sometime I had been publishing a few toughs about JavaScript as a proof assistance, all my posts have a code base that I test and experiment before I post anything.

So I decided to release this experimental code (https://github.com/fsvieira/galojs), it is still incomplete but it maybe interesting for some people, a example can be accessed here: http://fsvieira.com/beta/galojs/.

Enjoy!

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

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

JavaScript lambda-tree generation (or something like that).

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

Hi,
In my previous posts I talked about generating an Abstract Syntax Tree (AST) from JavaScript functions using the great lib Esprima and manipulated it to create pure lambda functions. The simple examples that I used were simple logic formulas using only the ‘not’ operator. Executing this simple converted lambda functions would return a Value (True or False).
I also concluded that it would be more useful to my goal of using JavaScript as a proof assistance for software validation if it was possible to build a lambda-tree representation of the function to enable a deeper analysis.

Firstly, to make this post more interesting than the last one, I will implement the new operators ‘and’ and ‘or':

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

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

// new logic operators 
lambda.logic.and = function(a, b) {return lambda.logic.not(lambda.logic.nand(a, b));};
lambda.logic.or = function(a, b) {return lambda.logic.nand(lambda.logic.not(a), lambda.logic.not(b));};

As you can see in the code above I use nand to define ‘not’, ‘and’ and ‘or’, so I will only need to change the function lambda.logic.nand to return a tree, defined as:

function lambda(application, variables) {
  this.application = application;
  this.variables = variables;
}

where the application is like a function and the variables are the function’s arguments.
Now that we have a nice representation the nand definition would be like this:

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

For the test function I chose this logic formula ‘p / (q / r) -> (p / q / (p / r))’ that I found in the Internet and have no idea what it means :D.
JavaScript doesn’t have the logic operator -> (implication), but ‘p -> q’ can be easily written with not/or operators: ‘!p || q’ and the whole formula be written like this:

function pqr(p,q,r) {
  // p / (q / r) -> (p / q / (p / r))
  return !(p || (q && r)) || ((p || q) && (p || r));
}

To convert the above formula the following code is executed:

eval(lambda.program(pqr));

Which will result in this function:

function lambda_pqr(p,q,r) {return lambda.logic.or(lambda.logic.not(lambda.logic.or(p,lambda.logic.and(q,r))),lambda.logic.and(lambda.logic.or(p,q),lambda.logic.or(p,r)));}; 

Executing the lambda_pqr (I chose to pass string arguments because I wanted to name the variables, but I could have passed the values as True or False).

var r = lambda_pqr('p', 'q', 'r');

will return the lambda tree:

r = ((((((((((p p False) False True) ((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False) False True) ((((p p False) False True) ((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False) False True) False) False True) ((((((p p False) False True) ((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False) False True) ((((p p False) False True) ((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False) False True) False) False True) False) False True) ((((((((((p p False) False True) ((q q False) False True) False) False True) ((((p p False) False True) ((r r False) False True) False) False True) False) False True) ((((((p p False) False True) ((q q False) False True) False) False True) ((((p p False) False True) ((r r False) False True) False) False True) False) False True) False) False True) ((((((((p p False) False True) ((q q False) False True) False) False True) ((((p p False) False True) ((r r False) False True) False) False True) False) False True) ((((((p p False) False True) ((q q False) False True) False) False True) ((((p p False) False True) ((r r False) False True) False) False True) False) False True) False) False True) False) False True) False) False True)

I made two functions in lambda ‘class’. One is ‘replace’, that receives a dictionary and replaces all matching keys in the lambda tree with the corresponding value. The other is the ‘solve’ function that will apply arguments to any application on the tree that can be applied.

Ex.

r_replace = r.replace({'p': lambda.logic.True});

/* Result:
r_replace = ((((((((((True True False) False True) ((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False) False True) ((((True True False) False True) ((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False) False True) False) False True) ((((((True True False) False True) ((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False) False True) ((((True True False) False True) ((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False) False True) False) False True) False) False True) ((((((((((True True False) False True) ((q q False) False True) False) False True) ((((True True False) False True) ((r r False) False True) False) False True) False) False True) ((((((True True False) False True) ((q q False) False True) False) False True) ((((True True False) False True) ((r r False) False True) False) False True) False) False True) False) False True) ((((((((True True False) False True) ((q q False) False True) False) False True) ((((True True False) False True) ((r r False) False True) False) False True) False) False True) ((((((True True False) False True) ((q q False) False True) False) False True) ((((True True False) False True) ((r r False) False True) False) False True) False) False True) False) False True) False) False True) False) False True)
*/

As you can see in the result, all occurrences of ‘p’ are replaced by the True value, if we try to solve it we get:

 
r_replace.solve();

// Result: True.  

From the original formula it’s easy to see that the result is actually right: p / (q / r) -> (p / q / (p / r)) => replace p with True => True / (q / r) -> (True / q / (p / r)) => True -> True => True.

But it’s more interesting when p is False:

r_replace = r.replace({'p': lambda.logic.False});
r_replace.solve();

/* Result:
r_replace = (((((((((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False True) (((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False True) False) False True) (((((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False True) (((((((q r False) False True) ((q r False) False True) False) False True) ((((q r False) False True) ((q r False) False True) False) False True) False) False True) False True) False) False True) False) False True) (((((((((q q False) False True) False True) (((r r False) False True) False True) False) False True) (((((q q False) False True) False True) (((r r False) False True) False True) False) False True) False) False True) (((((((q q False) False True) False True) (((r r False) False True) False True) False) False True) (((((q q False) False True) False True) (((r r False) False True) False True) False) False True) False) False True) False) False True) False) False True)
*/

The tree is partially solved because there isn’t anything else to replace. q and r are not defined so the result can’t be reduced any more.

Conclusions

The idea of this post was to experiment with the tree representation of a function. The chosen example is a logical formula because it is easier to experiment with.
There are some limitations in the code regarding the use of propositional logic. One is that I have to use the values True and False and it isn’t possible to say, instead of p=True, just say that p exists and apply some elimination rules.
I don’t know if in the current state of the tree representation it would be possible to somehow apply the propositional logic techniques and rules, but even if is possible (I think) a very handy feature would be to keep different levels of representation, being the lambda calculus the base and lowest level.
With representation levels it would be much easier to maintain a human representation and in the case of propositional logic it would be great to deal with the normal logic symbols ->, /, / … and use what is already in the field, for example the method of analytic tableaux.

So I guess in the next post about this subject I will try to add different levels of representation to the tree.

See you soon…

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

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

12 Balls game release for caanoo.

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

I ported my javascript game ‘The 12 Balls Game’ to caanoo and made a new web page for it, The 12 Balls Game.

Also I have made a new download section and add it the latex source of my CV and the 12 Balls game page as a template.

I Should start to clean a little my dev blog…

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