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)
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
F# is a functional language, created by Microsoft. Implemented under .NET CLR, it’s a typed language, with access to .NET framework. It inherits most of ML/OCaml features. 
