// 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
Useful snippets of F# code, formatted in a way that makes it easy to copy and paste the snippet in the F# Interactive editor.
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 Apply part in reduce function, right?
Post a Comment