Enum Exp 

pub enum Exp<T: Clone + Eq> {
    Var(Ident<T>),
    Abs(Ident<T>, Box<Exp<T>>),
    App(Box<Exp<T>>, Box<Exp<T>>),
}

Expression in Lambda Calculus.

T represents the type of indentifiers.

Formatting:

• use {} for simple format
• use {:#} for extra De Bruijn index information

use lambda macro to create lambda expression efficiently.

Variants

Var(Ident<T>)

Variable identifier

Abs(Ident<T>, Box<Exp<T>>)

Abstraction

App(Box<Exp<T>>, Box<Exp<T>>)

Application

Implementations

impl<T> Exp<T>

where T: Clone + Eq,

pub fn simplify(&mut self) -> Result<&mut Self, Error>

Simplify repeatedly using beta-reduction in normal order for at most SIMPLIFY_LIMIT times.

Examples found in repository

examples/church_encoding.rs (line 8)

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(())
}

examples/parser.rs (line 22)

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(())
}

examples/y_combinator.rs (line 12)

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(())
}

pub fn eval_normal_order(&mut self, eta_reduce: bool) -> bool

The leftmost, outermost redex is always reduced first. That is, whenever possible the arguments are substituted into the body of an abstraction before the arguments are reduced.

return false if nothing changes, otherwise true.

Examples found in repository

examples/y_combinator.rs (line 38)

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(())
}

impl<T: Clone + Eq> Exp<T>

pub fn for_each_var<F>(&mut self, f: F)

where F: Fn(&mut Exp<T>, u32) + Clone,

iterate over each variable the second parameter for f is depth: number of abstractions containing this variable.

pub fn subst_unbounded(&mut self, name: &T, exp: &Exp<T>) -> &mut Self

Substitute free variables (de bruijn index = 0) with expression

pub fn is_beta_redex(&mut self) -> bool

Check whether current expression is a beta reduction.

Examples found in repository

examples/beta_reduce.rs (line 11)

fn main() {
    let and = lambda!(x. y. (x y x));
    let tt = lambda!(x. (y. x));
    let ff = lambda!(x. (y. y));
    let mut exp = lambda!({and} {tt} {ff});

    eprintln!("exp = {}", exp); // ((λx. λy. (x y) x) λx. λy. x) λx. λy. y

    assert!(exp.into_app().unwrap().0.is_beta_redex());
    assert!(exp.into_app().unwrap().0.beta_reduce());
    eprintln!("exp = {}", exp); // (λy. ((λx. λy. x) y) λx. λy. x) λx. λy. y

    assert!(exp
        .into_app()
        .unwrap()
        .0 // λy. ((λx. λy. x) y) λx. λy. x
        .into_abs()
        .unwrap()
        .1 // ((λx. λy. x) y) λx. λy. x
        .into_app()
        .unwrap()
        .0 // (λx. λy. x) y
        .beta_reduce());
    eprintln!("exp = {}", exp); // (λy. (λy. y) λx. λy. x) λx. λy. y

    assert!(exp
        .into_app()
        .unwrap()
        .0 // λy. (λy. y) λx. λy. x
        .into_abs()
        .unwrap()
        .1 // (λy. y) λx. λy. x
        .beta_reduce());
    eprintln!("exp = {}", exp); // (λy. y) λx. λy. y

    assert!(exp.beta_reduce());
    eprintln!("exp = {}", exp); // λx. λy. y
}

pub fn beta_reduce(&mut self) -> bool

Try making beta reduction, return false if nothing changed.

Examples found in repository

examples/beta_reduce.rs (line 12)

fn main() {
    let and = lambda!(x. y. (x y x));
    let tt = lambda!(x. (y. x));
    let ff = lambda!(x. (y. y));
    let mut exp = lambda!({and} {tt} {ff});

    eprintln!("exp = {}", exp); // ((λx. λy. (x y) x) λx. λy. x) λx. λy. y

    assert!(exp.into_app().unwrap().0.is_beta_redex());
    assert!(exp.into_app().unwrap().0.beta_reduce());
    eprintln!("exp = {}", exp); // (λy. ((λx. λy. x) y) λx. λy. x) λx. λy. y

    assert!(exp
        .into_app()
        .unwrap()
        .0 // λy. ((λx. λy. x) y) λx. λy. x
        .into_abs()
        .unwrap()
        .1 // ((λx. λy. x) y) λx. λy. x
        .into_app()
        .unwrap()
        .0 // (λx. λy. x) y
        .beta_reduce());
    eprintln!("exp = {}", exp); // (λy. (λy. y) λx. λy. x) λx. λy. y

    assert!(exp
        .into_app()
        .unwrap()
        .0 // λy. (λy. y) λx. λy. x
        .into_abs()
        .unwrap()
        .1 // (λy. y) λx. λy. x
        .beta_reduce());
    eprintln!("exp = {}", exp); // (λy. y) λx. λy. y

    assert!(exp.beta_reduce());
    eprintln!("exp = {}", exp); // λx. λy. y
}

pub fn is_eta_redex(&mut self) -> bool

Check whether current expression is a eta reduction.

Examples found in repository

examples/eta_reduce.rs (line 14)

fn main() {
    let mut exp = lambda!(a. b. c. f a b c);

    eprintln!("exp = {}", exp);
    assert!(exp
        .into_abs()
        .unwrap()
        .1
        .into_abs()
        .unwrap()
        .1
        .is_eta_redex());

    assert!(exp.into_abs().unwrap().1.into_abs().unwrap().1.eta_reduce());
    eprintln!("exp = {}", exp);

    assert!(exp.into_abs().unwrap().1.eta_reduce());
    eprintln!("exp = {}", exp);

    assert!(exp.eta_reduce());
    eprintln!("exp = {}", exp);
}

pub fn eta_reduce(&mut self) -> bool

Eta reduce requires the function’s extensionality axiom, thus is not enabled by default.

Examples found in repository

examples/eta_reduce.rs (line 16)

fn main() {
    let mut exp = lambda!(a. b. c. f a b c);

    eprintln!("exp = {}", exp);
    assert!(exp
        .into_abs()
        .unwrap()
        .1
        .into_abs()
        .unwrap()
        .1
        .is_eta_redex());

    assert!(exp.into_abs().unwrap().1.into_abs().unwrap().1.eta_reduce());
    eprintln!("exp = {}", exp);

    assert!(exp.into_abs().unwrap().1.eta_reduce());
    eprintln!("exp = {}", exp);

    assert!(exp.eta_reduce());
    eprintln!("exp = {}", exp);
}

pub fn purify(&self) -> Exp<()>

Remove name of indentifiers, keeping just de bruijn code. If there are free variables, they will become the same thing.

Examples found in repository

examples/y_combinator.rs (line 27)

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(())
}

pub fn into_app(&mut self) -> Option<(&mut Self, &mut Self)>

return func and body for App.

Examples found in repository

examples/beta_reduce.rs (line 11)

fn main() {
    let and = lambda!(x. y. (x y x));
    let tt = lambda!(x. (y. x));
    let ff = lambda!(x. (y. y));
    let mut exp = lambda!({and} {tt} {ff});

    eprintln!("exp = {}", exp); // ((λx. λy. (x y) x) λx. λy. x) λx. λy. y

    assert!(exp.into_app().unwrap().0.is_beta_redex());
    assert!(exp.into_app().unwrap().0.beta_reduce());
    eprintln!("exp = {}", exp); // (λy. ((λx. λy. x) y) λx. λy. x) λx. λy. y

    assert!(exp
        .into_app()
        .unwrap()
        .0 // λy. ((λx. λy. x) y) λx. λy. x
        .into_abs()
        .unwrap()
        .1 // ((λx. λy. x) y) λx. λy. x
        .into_app()
        .unwrap()
        .0 // (λx. λy. x) y
        .beta_reduce());
    eprintln!("exp = {}", exp); // (λy. (λy. y) λx. λy. x) λx. λy. y

    assert!(exp
        .into_app()
        .unwrap()
        .0 // λy. (λy. y) λx. λy. x
        .into_abs()
        .unwrap()
        .1 // (λy. y) λx. λy. x
        .beta_reduce());
    eprintln!("exp = {}", exp); // (λy. y) λx. λy. y

    assert!(exp.beta_reduce());
    eprintln!("exp = {}", exp); // λx. λy. y
}

pub fn into_abs(&mut self) -> Option<(&mut Ident<T>, &mut Self)>

return body for Abs.

Examples found in repository

examples/eta_reduce.rs (line 8)

fn main() {
    let mut exp = lambda!(a. b. c. f a b c);

    eprintln!("exp = {}", exp);
    assert!(exp
        .into_abs()
        .unwrap()
        .1
        .into_abs()
        .unwrap()
        .1
        .is_eta_redex());

    assert!(exp.into_abs().unwrap().1.into_abs().unwrap().1.eta_reduce());
    eprintln!("exp = {}", exp);

    assert!(exp.into_abs().unwrap().1.eta_reduce());
    eprintln!("exp = {}", exp);

    assert!(exp.eta_reduce());
    eprintln!("exp = {}", exp);
}

examples/beta_reduce.rs (line 19)

fn main() {
    let and = lambda!(x. y. (x y x));
    let tt = lambda!(x. (y. x));
    let ff = lambda!(x. (y. y));
    let mut exp = lambda!({and} {tt} {ff});

    eprintln!("exp = {}", exp); // ((λx. λy. (x y) x) λx. λy. x) λx. λy. y

    assert!(exp.into_app().unwrap().0.is_beta_redex());
    assert!(exp.into_app().unwrap().0.beta_reduce());
    eprintln!("exp = {}", exp); // (λy. ((λx. λy. x) y) λx. λy. x) λx. λy. y

    assert!(exp
        .into_app()
        .unwrap()
        .0 // λy. ((λx. λy. x) y) λx. λy. x
        .into_abs()
        .unwrap()
        .1 // ((λx. λy. x) y) λx. λy. x
        .into_app()
        .unwrap()
        .0 // (λx. λy. x) y
        .beta_reduce());
    eprintln!("exp = {}", exp); // (λy. (λy. y) λx. λy. x) λx. λy. y

    assert!(exp
        .into_app()
        .unwrap()
        .0 // λy. (λy. y) λx. λy. x
        .into_abs()
        .unwrap()
        .1 // (λy. y) λx. λy. x
        .beta_reduce());
    eprintln!("exp = {}", exp); // (λy. y) λx. λy. y

    assert!(exp.beta_reduce());
    eprintln!("exp = {}", exp); // λx. λy. y
}

pub fn into_ident(&mut self) -> Option<&mut Ident<T>>

return identifer for Var.

Trait Implementations

impl<T: Clone + Clone + Eq> Clone for Exp<T>

fn clone(&self) -> Exp<T>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T: Debug + Clone + Eq> Debug for Exp<T>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Exp<()>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Exp<String>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T: PartialEq + Clone + Eq> PartialEq for Exp<T>

fn eq(&self, other: &Exp<T>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<T: Eq + Clone + Eq> Eq for Exp<T>

impl<T: Clone + Eq> StructuralPartialEq for Exp<T>