Angel \”Java\” Lopez on Blog

February 25, 2009

Presenting AjLambda: Lambda calculus implementation in C#

Filed under: .NET, C Sharp, Functional Programming, Programming Languages — ajlopez @ 8:21 am

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

(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 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:


The short version with multiple parameters is supported:


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
; Natural numbers
0 = \fx.x
1 = \fx.fx
2 = \fx.f(fx)
3 = \fx.f(f(fx))
; Succesor
SUCC = \nfx.f(nfx)
; Add
ADD = \
; 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 = :

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

Lambda Calculus implementation from Fred’s Page

Angel “Java” Lopez


  1. […] sobre el Cálculo Lambda Presenting AjLambda, lambda calculus in C# Presentando AjLambda: implementación de Cálculo Lambda en […]

    Pingback by Computadoras aprendiendo música - Angel "Java" Lopez — May 18, 2009 @ 10:28 am

  2. gracias.

    una excelente informacion.

    es posible que me puedas enviar todo el proyecto a mi correo (

    por favor

    Comment by Alejandro — June 17, 2010 @ 4:58 pm

  3. gracias.

    una excelente informacion.

    es posible que me puedas enviar todo el proyecto a mi correo (

    por favor

    Comment by Alejandro — June 17, 2010 @ 5:00 pm

  4. […] Presenting AjLambda: Lambda Calculus Implementation in C# Presentando AjLambda: implementación de Cálculo Lambda en C# […]

    Pingback by Presentando Programación Funcional, AjLisp y Clojure - Angel "Java" Lopez — November 5, 2010 @ 3:10 pm

RSS feed for comments on this post. TrackBack URI

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Blog at

%d bloggers like this: