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.