Presenting AjLambda: Lambda calculus implementation in C#

I was working on my “code kate” AjLambda, a Lambda Calculus implementation, written using C#:

http://code.google.com/p/ajcodekatas/source/browse/#svn/trunk/AjLambda

(If you are new to Lambda Calculus notation, there are tutorial links at the end of this post)

Yes! It’s the geeky project I wrote this year…;-).. The solution is simple, it contains three projects,

It has a core library, AjLambda, a test project AjLambda.Tests and an AjLambda.Console program to run. The core library has few main classes.

Expression is the base abstract class. .Reduce is the method that implements the reduction of an expression. .Replaces is used to change a variable by other. Sometimes, it’s needed to choose a new name for a variable, that it doesn’t collides with another free variable name. .FreeVariables is the method to obtain the list of free variables in an expression. For example, in the lambda expression:

\x.xy

x and y are variables, but y is a free variable, and x is a bound parameter.

Variable express the variable (a lower-case letter in this implementation). Lambda is the lamba (parameter plus body). The lambda is entered using:

\x.x

The short version with multiple parameters is supported:

\xy.yx

This is the .Reduce implementation for Pair (a pair of expression, left and right):

public override Expression Reduce() { if (this.left is Lambda) return ((Lambda)this.left).Apply(this.right); Expression newLeft = this.left.Reduce(); if (newLeft != this.left) return new Pair(newLeft, this.right); Expression newRight = this.right.Reduce(); if (newRight == this.right) return this; return new Pair(newLeft, newRight); }

Running AjLamnda.Console with a parameter:

AjLambda.Console Boot.l

loads the auxiliary file Boot.l, where I defined some predefined functions:

; True
T = \xy.x
; False
F = \xy.y
; And
AND = \ab.abF
; If Then Else
IFTHENELSE = \x.x
; Natural numbers
0 = \fx.x
1 = \fx.fx
2 = \fx.f(fx)
3 = \fx.f(f(fx))
; Succesor
SUCC = \nfx.f(nfx)
; Add
ADD = \nmfx.nf(mfx)
; Multiply
MULT = \nmf.n(mf)
; Is Zero
ISZERO = \nxy.n(\z.y)x
; Predecessor
PRED = \nfx.n(\gh.h(gf))(\u.x)(\u.u)
; Pair Functions
PAIR = \xyf.fxy
FIRST = \p.pT
SECOND = \p.pF
NIL = \x.T
NULL = \p.p(\xy.F)
; Fixed Point
A = \xy.y(xxy)
Y = A A
; Factorial
FACT = Y (\f.\n.IFTHENELSE (ISZERO n) (1) (MULT n (f (PRED n)))))