1 people like it.

A Lambda Calculus AST

A work-in-progress implementation of Lambda Calculus - Alpha and Beta reduction is buggy

  1: 
  2: 
  3: 
  4: 
  5: 
  6: 
  7: 
  8: 
  9: 
 10: 
 11: 
 12: 
 13: 
 14: 
 15: 
 16: 
 17: 
 18: 
 19: 
 20: 
 21: 
 22: 
 23: 
 24: 
 25: 
 26: 
 27: 
 28: 
 29: 
 30: 
 31: 
 32: 
 33: 
 34: 
 35: 
 36: 
 37: 
 38: 
 39: 
 40: 
 41: 
 42: 
 43: 
 44: 
 45: 
 46: 
 47: 
 48: 
 49: 
 50: 
 51: 
 52: 
 53: 
 54: 
 55: 
 56: 
 57: 
 58: 
 59: 
 60: 
 61: 
 62: 
 63: 
 64: 
 65: 
 66: 
 67: 
 68: 
 69: 
 70: 
 71: 
 72: 
 73: 
 74: 
 75: 
 76: 
 77: 
 78: 
 79: 
 80: 
 81: 
 82: 
 83: 
 84: 
 85: 
 86: 
 87: 
 88: 
 89: 
 90: 
 91: 
 92: 
 93: 
 94: 
 95: 
 96: 
 97: 
 98: 
 99: 
100: 
101: 
102: 
103: 
104: 
105: 

//namespace Demo.Lambda

open Microsoft.FSharp.Quotations
open Microsoft.FSharp.Quotations.Patterns

type var = string
type term = 
  | Lambda of Variable:var * Body:term
  | Var of Variable:var
  | App of Left:term * Right:term

type Fn = delegate of Fn -> Fn

module Lambda =
  let lambdaSymbol = System.Char.ConvertFromUtf32(0x000003BB)
  let rec ToString this = 
    match this with
    | Lambda(var, body) -> 
        sprintf "%s%s.%s" lambdaSymbol var (ToString body)
    | Var(var) -> var
    | App(left,right) -> 
        sprintf "(%s %s)" (ToString left) (ToString right)
  let rec fromExpr (e:Microsoft.FSharp.Quotations.Expr) =
    match e with
    | Patterns.Lambda(v, e) -> Lambda(v.Name, fromExpr e)
    | Patterns.Application(left, right) -> App(fromExpr left, fromExpr right)
    | Patterns.Var(var) -> Var(var.Name)
    | Patterns.Call(Some(left), methodInfo, [right]) when methodInfo.Name = "Invoke" -> 
        App(fromExpr left, fromExpr right)
    | e -> 
        let typeName = e.Type.ToString()
        raise (System.Exception(sprintf "Cannot convert %s to lambda" typeName))
  let rec substitute (varName:var) (withExpr:term) (expr:term) =
    let doSubRec = substitute varName withExpr 
    match expr with
    | Var(name) when varName = name -> withExpr
    | App(left, right) -> App(doSubRec left, doSubRec right)
    | Lambda(var, body) when var <> varName -> Lambda(var, doSubRec body)
    | x -> x
  let (|NonShadowingLamda|_|) varName expr = 
    match expr with
    | Lambda(var, body) when var <> varName -> Some(NonShadowingLamda(var, body))
    | _ -> None
  let rec substitute2 (varName:var) (withExpr:term) (expr:term) =
    let doSubRec = substitute varName withExpr 
    match expr with
    | Var(name) when varName = name -> withExpr
    | App(left, right) -> App(doSubRec left, doSubRec right)
    | NonShadowingLamda varName (var, body) -> Lambda(var, doSubRec body)
    | x -> x

  let alphaNormalize (expr:term) =
    let rec normalizeRec (n:int) (expr:term) =
      let newVarName = sprintf "v%i" n
      let newVar = Var(newVarName)
      let normalize = normalizeRec (n + 1)
      match expr with
      | Lambda(var, body) as l -> 
        let newBody = normalize body
        let subbedVar = substitute var newVar newBody
        Lambda(newVarName, subbedVar)
      | App(left, right) -> App(normalize left, normalize right)
      | x -> x
    normalizeRec 0 expr
  let rec evalStep expr = 
    match expr with
    | App(Lambda(var, expr), right) -> substitute var right expr
    | App(left, right) -> App(evalStep left, evalStep right)
    | Lambda(var, body) -> Lambda(var, evalStep body)
    | x -> x

  let rec eval (maxSteps:int) (term:term) =
    seq {
      yield term
      let last = ref term
      let next = ref (evalStep term)
      while next.Value <> last.Value do
        yield next.Value
        last := next.Value
        next := evalStep next.Value
    } |> Seq.truncate maxSteps |> Seq.toList
  let printEval max term =
    let steps = term |> eval max
    for step in steps do
      printfn "%s" (ToString step)
    let last = steps |> List.rev |> List.head
    last

module BooleanLogic =
  let Id = <@@ fun x -> x @@> |> Lambda.fromExpr 
  let True = <@@ fun x y -> x @@> |> Lambda.fromExpr 
  let False = <@@ fun x y -> y @@> |> Lambda.fromExpr 
  let Not = <@@ fun p a b -> p b a @@> |> Lambda.fromExpr 
  let And = <@@ fun (p:Fn) (q:Fn) -> p.Invoke(q).Invoke(p) @@> |> Lambda.fromExpr 

  let ex1 = App(And, True) |> Lambda.printEval 10

  let Zero = <@@ fun f x -> x @@> |> Lambda.fromExpr 
  let One = <@@ fun f x -> f x @@> |> Lambda.fromExpr
  let Two = <@@ fun f x -> f (f x) @@> |> Lambda.fromExpr
  let Succ = <@@ fun n f x -> f (n f x) @@> |> Lambda.fromExpr
  let Plus = <@@ fun m n f x -> m f (n f x) @@> |> Lambda.fromExpr

  let ZeroSucc = App(Succ, Zero) |> Lambda.printEval 10
  let OnePlus = App(App(Succ, One),One) |> Lambda.printEval 10
namespace Microsoft
namespace Microsoft.FSharp
namespace Microsoft.FSharp.Quotations
module Patterns

from Microsoft.FSharp.Quotations
type var = string

Full name: Script.var
Multiple items
val string : value:'T -> string

Full name: Microsoft.FSharp.Core.Operators.string

--------------------
type string = System.String

Full name: Microsoft.FSharp.Core.string
type term =
  | Lambda of Variable: var * Body: term
  | Var of Variable: var
  | App of Left: term * Right: term

Full name: Script.term
Multiple items
union case term.Lambda: Variable: var * Body: term -> term

--------------------
active recognizer Lambda: Expr -> (Var * Expr) option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Lambda|_| )
Multiple items
union case term.Var: Variable: var -> term

--------------------
active recognizer Var: Expr -> Var option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Var|_| )

--------------------
type Var =
  interface IComparable
  new : name:string * typ:Type * ?isMutable:bool -> Var
  member IsMutable : bool
  member Name : string
  member Type : Type
  static member Global : name:string * typ:Type -> Var

Full name: Microsoft.FSharp.Quotations.Var

--------------------
new : name:string * typ:System.Type * ?isMutable:bool -> Var
union case term.App: Left: term * Right: term -> term
type Fn =
  delegate of Fn -> Fn

Full name: Script.Fn
union case term.Lambda: Variable: var * Body: term -> term
val lambdaSymbol : string

Full name: Script.Lambda.lambdaSymbol
namespace System
type Char =
  struct
    member CompareTo : value:obj -> int + 1 overload
    member Equals : obj:obj -> bool + 1 overload
    member GetHashCode : unit -> int
    member GetTypeCode : unit -> TypeCode
    member ToString : unit -> string + 1 overload
    static val MaxValue : char
    static val MinValue : char
    static member ConvertFromUtf32 : utf32:int -> string
    static member ConvertToUtf32 : highSurrogate:char * lowSurrogate:char -> int + 1 overload
    static member GetNumericValue : c:char -> float + 1 overload
    ...
  end

Full name: System.Char
System.Char.ConvertFromUtf32(utf32: int) : string
val ToString : this:term -> string

Full name: Script.Lambda.ToString
val this : term
Multiple items
val var : var

--------------------
type var = string

Full name: Script.var
val body : term
val sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
Multiple items
union case term.Var: Variable: var -> term

--------------------
type Var =
  interface IComparable
  new : name:string * typ:Type * ?isMutable:bool -> Var
  member IsMutable : bool
  member Name : string
  member Type : Type
  static member Global : name:string * typ:Type -> Var

Full name: Microsoft.FSharp.Quotations.Var

--------------------
new : name:string * typ:System.Type * ?isMutable:bool -> Var
val left : term
val right : term
val fromExpr : e:Expr -> term

Full name: Script.Lambda.fromExpr
val e : Expr
Multiple items
type Expr =
  override Equals : obj:obj -> bool
  member GetFreeVars : unit -> seq<Var>
  member Substitute : substitution:(Var -> Expr option) -> Expr
  member ToString : full:bool -> string
  member CustomAttributes : Expr list
  member Type : Type
  static member AddressOf : target:Expr -> Expr
  static member AddressSet : target:Expr * value:Expr -> Expr
  static member Application : functionExpr:Expr * argument:Expr -> Expr
  static member Applications : functionExpr:Expr * arguments:Expr list list -> Expr
  ...

Full name: Microsoft.FSharp.Quotations.Expr

--------------------
type Expr<'T> =
  inherit Expr
  member Raw : Expr

Full name: Microsoft.FSharp.Quotations.Expr<_>
active recognizer Lambda: Expr -> (Var * Expr) option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Lambda|_| )
val v : Var
property Var.Name: string
active recognizer Application: Expr -> (Expr * Expr) option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Application|_| )
val left : Expr
val right : Expr
active recognizer Var: Expr -> Var option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Var|_| )
Multiple items
val var : Var

--------------------
type var = string

Full name: Script.var
active recognizer Call: Expr -> (Expr option * System.Reflection.MethodInfo * Expr list) option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Call|_| )
union case Option.Some: Value: 'T -> Option<'T>
val methodInfo : System.Reflection.MethodInfo
property System.Reflection.MemberInfo.Name: string
val typeName : string
property Expr.Type: System.Type
System.Type.ToString() : string
val raise : exn:System.Exception -> 'T

Full name: Microsoft.FSharp.Core.Operators.raise
Multiple items
type Exception =
  new : unit -> Exception + 2 overloads
  member Data : IDictionary
  member GetBaseException : unit -> Exception
  member GetObjectData : info:SerializationInfo * context:StreamingContext -> unit
  member GetType : unit -> Type
  member HelpLink : string with get, set
  member InnerException : Exception
  member Message : string
  member Source : string with get, set
  member StackTrace : string
  ...

Full name: System.Exception

--------------------
System.Exception() : unit
System.Exception(message: string) : unit
System.Exception(message: string, innerException: exn) : unit
val substitute : varName:var -> withExpr:term -> expr:term -> term

Full name: Script.Lambda.substitute
val varName : var
val withExpr : term
val expr : term
val doSubRec : (term -> term)
val name : var
val x : term
union case Option.None: Option<'T>
val substitute2 : varName:var -> withExpr:term -> expr:term -> term

Full name: Script.Lambda.substitute2
active recognizer NonShadowingLamda: var -> term -> (var * term) option

Full name: Script.Lambda.( |NonShadowingLamda|_| )
val alphaNormalize : expr:term -> term

Full name: Script.Lambda.alphaNormalize
val normalizeRec : (int -> term -> term)
val n : int
Multiple items
val int : value:'T -> int (requires member op_Explicit)

Full name: Microsoft.FSharp.Core.Operators.int

--------------------
type int = int32

Full name: Microsoft.FSharp.Core.int

--------------------
type int<'Measure> = int

Full name: Microsoft.FSharp.Core.int<_>
val newVarName : string
val newVar : term
val normalize : (term -> term)
val l : term
val newBody : term
val subbedVar : term
val evalStep : expr:term -> term

Full name: Script.Lambda.evalStep
val eval : maxSteps:int -> term:term -> term list

Full name: Script.Lambda.eval
val maxSteps : int
Multiple items
val term : term

--------------------
type term =
  | Lambda of Variable: var * Body: term
  | Var of Variable: var
  | App of Left: term * Right: term

Full name: Script.term
Multiple items
val seq : sequence:seq<'T> -> seq<'T>

Full name: Microsoft.FSharp.Core.Operators.seq

--------------------
type seq<'T> = System.Collections.Generic.IEnumerable<'T>

Full name: Microsoft.FSharp.Collections.seq<_>
val last : term ref
Multiple items
val ref : value:'T -> 'T ref

Full name: Microsoft.FSharp.Core.Operators.ref

--------------------
type 'T ref = Ref<'T>

Full name: Microsoft.FSharp.Core.ref<_>
val next : term ref
property Ref.Value: term
module Seq

from Microsoft.FSharp.Collections
val truncate : count:int -> source:seq<'T> -> seq<'T>

Full name: Microsoft.FSharp.Collections.Seq.truncate
val toList : source:seq<'T> -> 'T list

Full name: Microsoft.FSharp.Collections.Seq.toList
val printEval : max:int -> term:term -> term

Full name: Script.Lambda.printEval
val max : int
val steps : term list
val step : term
val printfn : format:Printf.TextWriterFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.printfn
val last : term
Multiple items
module List

from Microsoft.FSharp.Collections

--------------------
type List<'T> =
  | ( [] )
  | ( :: ) of Head: 'T * Tail: 'T list
  interface IEnumerable
  interface IEnumerable<'T>
  member Head : 'T
  member IsEmpty : bool
  member Item : index:int -> 'T with get
  member Length : int
  member Tail : 'T list
  static member Cons : head:'T * tail:'T list -> 'T list
  static member Empty : 'T list

Full name: Microsoft.FSharp.Collections.List<_>
val rev : list:'T list -> 'T list

Full name: Microsoft.FSharp.Collections.List.rev
val head : list:'T list -> 'T

Full name: Microsoft.FSharp.Collections.List.head
module BooleanLogic

from Script
val Id : term

Full name: Script.BooleanLogic.Id
val x : obj
Multiple items
union case term.Lambda: Variable: var * Body: term -> term

--------------------
module Lambda

from Script
val True : term

Full name: Script.BooleanLogic.True
val y : obj
val False : term

Full name: Script.BooleanLogic.False
val Not : term

Full name: Script.BooleanLogic.Not
val p : (obj -> obj -> obj)
val a : obj
val b : obj
val And : term

Full name: Script.BooleanLogic.And
val p : Fn
val q : Fn
abstract member Fn.Invoke : Fn -> Fn
val ex1 : term

Full name: Script.BooleanLogic.ex1
val Zero : term

Full name: Script.BooleanLogic.Zero
val f : obj
val One : term

Full name: Script.BooleanLogic.One
val f : (obj -> obj)
val Two : term

Full name: Script.BooleanLogic.Two
val Succ : term

Full name: Script.BooleanLogic.Succ
val n : ((obj -> obj) -> obj -> obj)
val Plus : term

Full name: Script.BooleanLogic.Plus
val m : (obj -> obj -> obj)
val n : (obj -> obj -> obj)
val ZeroSucc : term

Full name: Script.BooleanLogic.ZeroSucc
val OnePlus : term

Full name: Script.BooleanLogic.OnePlus
Raw view Test code New version

More information

Link:http://fssnip.net/oj
Posted:9 years ago
Author:Steve Goguen
Tags: theory

This web site is created using F# and Suave web server. It is hosted on Azure and the source code is on GitHub. Contributions are welcome!

The first version of fssnip.net has been created by @tomaspetricek back in 2010. This web site is a new, open-source and contribution-friendly version.