Enum lalrpop_lambda::Expression

pub enum Expression {
    Var(Variable),
    Abs(Abstraction),
    App(Application),
}

A mutually recursive definition for all lambda expressions

let parser = lalrpop_lambda::parse::ExpressionParser::new();

assert!(parser.parse("λx.(x x)").is_ok());

Variants

Var(Variable)Abs(Abstraction)App(Application)

Methods

impl Expression

pub fn apply(&self, η: bool) -> Self

β-reduction small-step semantics (→)

Represents local reducibility in natural deduction.

• η: λx.(e1 x) -> e1 whenever x does not appear free in e1

  Represents local completeness in natural deduction.

pub fn normalize(&self, strategy: &Strategy) -> Self

Big-step natural semantics (⇓)

Represents global reducibility in natural deduction.

TODO: Reduction strategy.

• η: (see Expression::apply)

use lalrpop_lambda::Strategy;
use lalrpop_lambda::parse::ExpressionParser;

let parser = ExpressionParser::new();
let expression = parser.parse("((λx.(λy.x y) b) a)").unwrap();
let normal = parser.parse("a b").unwrap();

assert_eq!(normal, expression.normalize(&Strategy::Applicative(true)));
assert_eq!(normal, expression.normalize(&Strategy::HeadSpine(false)));

impl Expression

pub fn rename(&self, old: &Variable, new: &Variable) -> Self

α-conversion

pub fn variables(&self) -> HashSet<Variable>

pub fn free_variables(&self) -> HashSet<Variable>

FV(M) is the set of variables in M, not closed by a λ term.

use std::collections::HashSet;
use lalrpop_lambda::Variable;

let parser = lalrpop_lambda::parse::ExpressionParser::new();

let mut free = HashSet::new();
free.insert(Variable("y".into(), None));

let expression = parser.parse("λx.(x y)").unwrap();

assert_eq!(free, expression.free_variables());

pub fn resolve(&self, env: &HashMap<Variable, Expression>) -> Expression

use std::collections::HashMap;

let mut env = HashMap::new();
env.insert(variable!(id), abs!{x.x});
env.insert(variable!(ad), abs!{x.y});
env.insert(variable!(x), 1.into());

assert_eq!(var!(q), var!(q).resolve(&env));
assert_eq!(1u64, var!(x).resolve(&env).into());

// Works with functions too!
let id: fn(u64) -> u64 = var!(id).resolve(&env).into();
assert_eq!(1, id(1));
let ad: fn(u64) -> u64 = var!(ad).resolve(&env).into();
assert_eq!(u64::from(var!(y)), ad(0));
assert_eq!(u64::from(var!(y)), ad(1));

impl Expression

pub fn build_abs(
    lambs: usize,
    ids: Vec<Variable>,
    body: Option<Expression>
) -> Self

Trait Implementations

impl<T> FnOnce(T) for Expression where
    T: Into<Expression> + From<Expression>, 

Function call support for an Expression.

assert_eq!(0u64, λ!{x.x}(0).into());
assert_eq!(γ!(γ!(a,b),0), γ!(a,b)(0));

type Output = Expression

The returned type after the call operator is used.

extern "rust-call" fn call_once(self, t: (T,)) -> Expression

🔬 This is a nightly-only experimental API. (fn_traits)

Performs the call operation.

impl Eq for Expression

impl PartialEq<Expression> for Expression

fn eq(&self, other: &Expression) -> bool

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl Clone for Expression

fn clone(&self) -> Expression

Returns a copy of the value.

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

Performs copy-assignment from source.

impl From<Expression> for fn(_: u64) -> u64

fn from(e: Expression) -> Self

Performs the conversion.

impl From<fn(u64) -> u64> for Expression

fn from(_f: fn(_: u64) -> u64) -> Self

Performs the conversion.

impl From<bool> for Expression

Church encoded booleans

use lalrpop_lambda::Expression;

assert_eq!(λ!{a.λ!{b.a}}, Expression::from(true));
assert_eq!(λ!{a.λ!{b.b}}, Expression::from(false));

fn from(p: bool) -> Self

Performs the conversion.

impl From<Expression> for bool

Convert λ term back to native Rust type

assert_eq!(true , bool::from(λ!{a.λ!{b.a}}));
assert_eq!(false, bool::from(λ!{a.λ!{b.γ!(b,b)}}));

fn from(e: Expression) -> bool

Performs the conversion.

impl From<u64> for Expression

Church encoded natural numbers

use lalrpop_lambda::Expression;

assert_eq!(λ!{f.λ!{x.x}}, Expression::from(0));
assert_eq!(λ!{f.λ!{x.γ!(f,x)}}, Expression::from(1));
assert_eq!(λ!{f.λ!{x.γ!(f,γ!(f,γ!(f,x)))}}, Expression::from(3));

fn from(n: u64) -> Self

Performs the conversion.

impl From<Expression> for u64

Convert λ term back to native Rust type

assert_eq!(0, u64::from(λ!{f.λ!{x.x}}));
assert_eq!(1, u64::from(λ!{f.λ!{x.γ!(f,x)}}));
assert_eq!(3, u64::from(λ!{f.λ!{x.γ!(f,γ!(f,γ!(f,x)))}}));

fn from(e: Expression) -> u64

Performs the conversion.

impl Debug for Expression

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

Formats the value using the given formatter.

impl Display for Expression

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

Formats the value using the given formatter.

impl Add<Expression> for Expression

let one = λ!{f.λ!{x.γ!(f,x)}};
let two = one.clone() + one.clone();
assert_eq!(2, u64::from(two.clone()));
assert_eq!(4, u64::from(two.clone() + two.clone()));

type Output = Self

The resulting type after applying the + operator.

fn add(self, other: Self) -> Self

Performs the + operation.

impl Mul<Expression> for Expression

let one = λ!{f.λ!{x.γ!(f,x)}};
let two = one.clone() + one.clone();
assert_eq!(1, u64::from(one.clone() * one.clone()));
assert_eq!(4, u64::from(two.clone() * two.clone()));

type Output = Self

The resulting type after applying the * operator.

fn mul(self, other: Self) -> Self

Performs the * operation.

impl Not for Expression

let t = λ!{a.λ!{b.a}};

assert_eq!(false, bool::from(!t.clone()));
assert_eq!(true, bool::from(!!t.clone()));

Evaluation Strategy

Note that there are two version of not, depending on the evaluation strategy that is chosen. We currently only evaluate using application order, so we choose the first option.

• Applicative evaluation order: λp.λa.λb.p b a
• Normal evaluation order: λp.p (λa.λb.b) (λa.λb.a)

type Output = Self

The resulting type after applying the ! operator.

fn not(self) -> Self

Performs the unary ! operation.

impl BitAnd<Expression> for Expression

let t = λ!{a.λ!{b.a}};
let f = λ!{a.λ!{b.b}};

assert_eq!(true,  bool::from(t.clone() & t.clone()));
assert_eq!(false, bool::from(t.clone() & f.clone()));
assert_eq!(false, bool::from(f.clone() & t.clone()));
assert_eq!(false, bool::from(f.clone() & f.clone()));

type Output = Self

The resulting type after applying the & operator.

fn bitand(self, other: Self) -> Self

Performs the & operation.

impl BitOr<Expression> for Expression

let t = λ!{a.λ!{b.a}};
let f = λ!{a.λ!{b.b}};

assert_eq!(true,  bool::from(t.clone() | t.clone()));
assert_eq!(true,  bool::from(t.clone() | f.clone()));
assert_eq!(true,  bool::from(f.clone() | t.clone()));
assert_eq!(false, bool::from(f.clone() | f.clone()));

type Output = Self

The resulting type after applying the | operator.

fn bitor(self, other: Self) -> Self

Performs the | operation.

impl BitXor<Expression> for Expression

let t = λ!{a.λ!{b.a}};
let f = λ!{a.λ!{b.b}};

assert_eq!(false, bool::from(t.clone() ^ t.clone()));
assert_eq!(true, bool::from(t.clone() ^ f.clone()));
assert_eq!(true, bool::from(f.clone() ^ t.clone()));
assert_eq!(false, bool::from(f.clone() ^ f.clone()));

type Output = Self

The resulting type after applying the ^ operator.

fn bitxor(self, other: Self) -> Self

Performs the ^ operation.