// This implementation support evaluation of anonymous recursion through Y Combinator (ex. Y Factorial)

type exp = | Var of string

| Lambda of string * exp

| Apply of exp * exp

let rec subst x v a =

match a with

| Var y ->

if x = y then v else a

| Lambda(y, a') ->

if x = y then a else Lambda(y, subst x v a')

| Apply(a', a'') ->

Apply(subst x v a', subst x v a'')

let rec reduce e =

let rec reduce' e =

match e with

| Var _ -> e

| Lambda (s, e') -> Lambda(s, reduce' e')

| Apply(e1, e2) ->

match e1 with

| Lambda(s, e3) -> subst s e2 e3

| _ -> Apply(reduce' e1, reduce' e2)

reduce' e

let rec loop f x =

let x' = f x

if x = x' then x' else loop f x'

let normalOrderReducer = loop reduce

## Saturday, 8 August 2009

### Lambda Calculus Normal Order Reducer

Subscribe to:
Post Comments (Atom)

## 5 comments:

Now how can I reduce the lambda expression using this feature in F# Interactvie?

1) Paste the reducer code in F# Interactive

2) Type the following (This example shows that: (\x.x) (\y.y) reduces to (\y.y))

> normalOrderReducer (Apply(Lambda("x", Var "x"), Lambda("y", Var "y")));;

val it : exp = Lambda ("y",Var "y")

thanks man.

When I want to reduce expression with number f.e. ( (/x . x) 3 )

How do this with F#?

Numbers in the lambda calculus can be encoded using Church Encoding (http://http://en.wikipedia.org/wiki/Church_encoding)

where:

3 ≡ \f.\x. f (f (f x))

hi, i'm trying to bulid applicative order reducer. I'm thinking i've to change a

Applypart inreducefunction, right?Post a Comment