Simplee.Gama 1.0.1

Simplee.Gama

A functional language compiler using graph reduction technique. The sources can be found on github at this link. The unit tests and more examples can be found on github at this link.

Lambda Calculus Tree (constructor and infix functions)

Includes the defintions for the lambda calculus.

The library exposes several infix operator functions which construct lambda expressions. For example you can construct a lambda abstraction using the following infix operators (.>>., .>>, or >>.):

    let expr  = "x" .>>. "y"  // represents the <λx.x y> lambda expression
    let expr' = "y" .>> expr  // represents the <(λx.x) y> lambda expression
    let expr = "x" .>>. ("x" .<<. "y")    // represents the <λx.x y> lambda expression
    let expr' = ("x" .>>. "x") <<. "y"    // represents the <(λx.x) y> lambda expression

To and From String (g2str, g2strL, g2strH, gexpr, gsys)

The library provides several functions which conveniently convert a given lambda expression to a string. You can convert an expression to a string representation in lambda expression style (eg. λx.x) using g2str and its equivalent g2strL. For converting an expression to a string representation in Haskell style (eg. \x->x) using g2strH.

    "x" .>>. "x" |> g2str     // the result will be the 'λx.x' string
    "x" .>>. "x" |> g2strL    // the result will be the `λx.x` string
    "x" .>>. "x" |> g2strH    // the result will be the `\x->x` string

You can construct a lambda expression from a string using the gexpr or gsys functions. The first one returns a Result (Ok/Error) so the caller can catch the parsing errors. The gsys function is intended to be used when you are sure that the string is well formatted therefore it returns an GExpression or failswith if it encounters a parsing error. The input string could represent a lambda term in either Lambada Calculus or Haskell formats.

The parsing is using a search function which indicates the parser which identifiers are built-in functions. Here is an example where we have 2 built-in functions, HEAD and +:

    let srch = function
        | s when s = "HEAD" -> "HEAD" |> Some
        | s when s = "+"    -> "+"    |> Some
        | _                 -> None

Using the above srch function, you can parse the following strings into lambda expressions:

    // parsing a Lambda Calculus string
    "λx.x"    |> gexpr srch     // the result will be the identity lambda expression
    "λa b->a" |> gsys srch      // the result will be the Church True lambda expression

    // parsing a Haskell string
    "\x->x"   |> gexpr srch     // the result will be the identity lambda expression
    "\a b->a" |> gsys srch      // the result will be the Church True lambda expression

    // parsing built-in functions and constants
    "(+ 1 2)" |> gexpr srch     // the result will be a lambda application expression

Bound & Free Variables

To determine if a given variable is either bound or/and free in a given expression, you can use the provided patterns: FreeVariable and BoundVariable. Both functions in below exmple should return true.

    let ``y is free in λx.y`` () =
        let term = "x" .>>. "y"
        match "y" |> gid with
        | FreeVariable term -> true
        | _                 -> false

    let ``x is bound in λyx.x`` () =
        let term = "y" .>> ("x" .>>. "x")
        match "x" |> gid with
        | BoundVariable term -> true 
        | _                  -> false

Notice that a given variable can be both free and bound in the same expression:

    let ``y is both free and bound in (λx.xy) (λy.y)`` () =
        let term = ("x" .>> ("x" .<<. "y") ) << ("y" .>>. "y")
        match "y" |> gid, "y" |> gid with
        | FreeVariable term, BoundVariable term -> true
        | _                                     -> false

You can get the list of free variables in a given expression by using the freevs function. In the below example, the test function should return true since both y and z are free in the test expression.

    let ``the expression has two free vars, y and z`` () =
        let term = "x" .>> ("y" .<<. "z")
        (term |> freevs) = (["y"; "z"] |> List.map gid)

Evaluation

The library exposes two functions, geval and geval0 which evaluate a given expression to its normalize form, it the expression has one. The user can define a lookup function which replaces variables with expressions

    let lookup = function
        | (GIdentifier i) when i = "TST"  -> "tst" |> gvar  |> Some
        | (GIdentifier i) when i = "ID"   -> "x" .>>. "x"   |> Some
        | (GIdentifier i) when i = "HEAD" -> "HEAD" |> gkfn |> Some
        | (GIdentifier i) when i = "CONS" -> "CONS" |> gkfn |> Some
        | _                               -> None

This function can be passed as an argument to the geval function when an expression is evaluated. In the below example, the ID variable is replaced based on the defined lookup function with the Identity lambda abstraction which then is evaluated as part of the lambda application, the final expression being the expression represented by the y variable.

    // (ID y)  will be evaluated to y
    ("ID" .<<. "y") |> eval lookup

For the cases where there are no definition tables (eg. lookup function always returns None), you can use the convenience function geval0:

    // (λf.f 3) (λx.+ x 1) will be evaluated to (+ 3 1)
    ("f" .>> ("f" .<< (3 |> gkint))) 
    << ("x" .>> (("+" |> gkfn) <<. "x" << (1 |> gkint)))
    |> eval0