Crate lamcalc

LamCalc: An implementation for Lambda Calculus

LamCalc implements untyped Lambda Calculus, Inspired by Lambda Calculus: Basic Interpreter in Rust (Part 2).

Current status: stabalized v1.

Features

• lambda! macro for convenient definition.
• Implemented using De Bruijn index.
• Parser for expressions/definitions/files.
• WASM package for web application.

Quick View

use lamcalc::{lambda, Error, parser::parse_exp};

fn main () -> Result<(), Error> {
    // define using macro
    let tt = lambda!(x. y. x); // use macro to define lambda
    let ff = lambda!(x. (y. y)); // add parentheses for clarity
    let and = lambda!(x.y.x y x); // space between dots are not necessary

    // multiple printing format
    println!("and = {}", and);   // print lambda
    println!("and = {:#}", and); // lambda with De Bruijn index
    println!("and = {}", and.purify()); // De Bruijn encoding

    // use braces to refer to previously defined lambda
    let mut and_f_t = lambda!({and} {ff} {tt}); 
    and_f_t.simplify()?; // get simplified result
    assert_eq!(and_f_t, ff);

    // parse lambda expression string
    let y_combinator = lambda!(f.(x. f (x x)) (x. f (x x)));
    let y_str = r#"\f.(\x. f (x x)) (\x. f (x x))"#;
    let (y2, _) = parse_exp(y_str)?;
    
    assert_eq!(y2, y_combinator);

    Ok(())
}

See examples/ for more.

Example: Church Encoding

//! Church encoding

use lamcalc::{lambda, Error};

fn main() -> Result<(), Error> {
    let zero = lambda!(s. (z. z));
    let suc = lambda!(n. s. z. s (n s z));
    let plus = lambda!(n. m. n {suc} m).simplify()?.to_owned(); 

    let mut nats = vec![zero];
    for i in 1..10 {
        let sx = lambda!({suc} {nats[i - 1]}).simplify()?.to_owned();
        nats.push(sx);
    }

    let sum = lambda!({plus} {nats[4]} {nats[3]}).simplify()?.to_owned();
    assert_eq!(sum, nats[7]);

    Ok(())
}

Example: Parser

use lamcalc::{parser, Error, lambda};

fn main() -> Result<(), Error> {
    // parse single expression
    let (tt, _) = parser::parse_exp(r"\x. \y. x")?;

    // parse definition statement
    let (ident, ff, _) = parser::parse_def(r"ff = \x. \y. y")?;
    assert_eq!(ident, "ff");

    println!("ff = {}", ff);

    // parse multiple definitions
    let (map, _) = parser::parse_file(r##"
        // and
        and = \x. \y. x y x

        // or
        or = \x. \y. x x y
    "##)?;

    let and_t_f = lambda!({map["and"]} {tt} {ff}).simplify()?.to_owned();
    assert_eq!(and_t_f, ff);

    let or_t_f = lambda!({map["or"]} {tt} {ff}).simplify()?.to_owned();
    assert_eq!(or_t_f, tt);

    Ok(())
}

Example: Y Combinator

//! Y Combinator

use lamcalc::{lambda, Error};

fn main() -> Result<(), Error> {
    // prepare some nats
    let zero = lambda!(f. (x. x));
    let suc = lambda!(n. f. x. f (n f x));
    let prev = lambda!(n. f. x. n (g. h. h (g f)) (u. x) (u. u));
    let mut nats = vec![zero];
    for i in 1..10 {
        let sx = lambda!({suc} {nats[i - 1]}).simplify()?.to_owned();
        nats.push(sx);
        assert_eq!(
            lambda!({prev} {nats[i]}).simplify()?.to_string(),
            nats[i - 1].to_string()
        );
    }

    // utilities
    let mul = lambda!(n. m. f. x. n (m f) x);
    let if_n_is_zero = lambda!(n. n (w. x. y. y) (x. y. x));

    assert_eq!(
        lambda!({if_n_is_zero} {nats[0]} {nats[2]} {nats[1]} )
            .simplify()?
            .purify(),
        nats[2].purify()
    );

    // Y combinator
    let mut y = lambda!(f. (x. f (x x)) (x. f (x x)));

    // factorial
    let mut fact = lambda!(y. n. {if_n_is_zero} n (f. x. f x) ({mul} n (y ({prev} n))));

    eprintln!("simplify fact");
    while fact.eval_normal_order(true) { 
        eprintln!("fact = {}", fact);
    }

    let y_fact = lambda!({y} {fact});

    let res = lambda!({y_fact} {nats[3]}).purify().simplify()?.to_owned();
    eprintln!("{}", res);
    assert_eq!(res, nats[6].purify());

    // if you try to simplify Y combinator ...
    eprintln!("simplify y: {}", y.simplify().unwrap_err()); // lamcalc::Error::SimplifyLimitExceeded

    Ok(())
}

Modules

parser

Parse Lambda expressions in text. Support CJK characters.

wasm

feature: wasm interprete lambda expressions in browser

Macros

lambda

Build lambda expression with String identifier conveniently. Generally:

Structs

Ident

Identifier of variables.

Enums

Error

Error type.

Exp

Expression in Lambda Calculus.

Constants

SIMPLIFY_LIMIT

maximum number of reductions in a simplification