Monthly Archives: February 2014

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:

((位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.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%)

JavaScript NodeJS and Browser Modules

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

I want galojs to work on the browser and nodejs.

So I started to rewrite the galojs modules to work on nodejs. Apparently there is two types/specifications of modules in JS the CommonJS modules and AMD (Asynchronous Module Definition)

I think nodejs uses a improved version of CommonJS modules and a module can be something like this:

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

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

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


One of the nice features of modules is that you can export only the important parts and
keep other functions/variables as “private”.

module.exports = {
	Variable: Variable,
	Abstraction: Abstraction,
	Application: Variable,
	parse: parse,
	bind: bind,
	std_lib: std_lib,
	std_rename: std_rename

After the module is defined you can import it like this:

var Lambda = require ("lambda.js");

And you simple use it like this:

var myvar = new Lambda.Variable("myvar");

How to use modules in the browser?

There is probably more than one way to use nodejs modules in the browser, my favorite is to “compile” the modules to the browser, most of this “compilers” put all the code in only one file witch is great because you only need to include it once.

There is a few compilers out there the most popular is browserify and webmake, I prefer the last one (webmake) because the generated code is much more clear to me.

After js code is compiled you include it as a normal js script:

The other cool thing is that using webmake you can use require(…) and modules to code to the browser. In my case I made a few modules to node and main.js file to run with node, and then I made other js file to just work in the browser, it looks something like this:

var Lambda = require("../node/lib/lambda.js");
var AST = require("../node/lib/ast.js");

function print (msg) {
	if (msg !== undefined) { 
	  msg = msg.toString(); 
	else {
		msg = '#undef'
'); } $(document).ready(function() { print("start"); function updateCode() { var code = $("#code").val(); try { $("#output").html(""); eval(code); } catch (e) { print(e); throw e; } }; $("#code").bind('input propertychange', function () { updateCode(); }); updateCode(); });

I am using jquery that I included in my html page, and using require to import my node modules. When compiling this with webmake all dependencies are solved and put in only one file to be included in my html page like this.


Using modules on nodejs and the browser is very simple and it makes the code much more clean.
I am really enjoying the webmake, its great to be able to import js files in js, I had tried other ways, jslibs/functions, to include files with js but I always found some issues when debugging in the browser, I didn’t debug anything (yet) with webmake generated files but since they are really clean I think that wouldn’t be a problem…

Anyway even if you are not thinking about writing modules to nodejs webmake is still a great tool if you are thinking in writing js as modules in the browser.

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