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

You can ask about the predefined names. I defined the first natural numbers, including zero:

Names are words that begin with upper case letter. Variable names are lower letter (from ‘a’ thru ‘z’, only one letter per variable).

As usual, I defined SUCC and PRED (succesor and predecessor functions):

Each reduction step is printed, until no more reduce is possible.

You can define new functions using Name = <expression>:

More information about Lambda Calculus at:

Lecture Notes on the Lambda Calculus (pdf) (excellent paper to learn Lambda Calculus)

Peter Selinger- Papers

Lambda calculus – Wikipedia, the free encyclopedia

A Tutorial Introduction to the Lambda Calculus

http://delicious.com/ajlopez/lambda

Lambda Calculus implementation from Fred’s Page

Angel “Java” Lopez

http://www.ajlopez.com/


http://twitter.com/ajlopez