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 rename(&self, old: &Variable, new: &Variable) -> Self

α-conversion

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

β-reduction small-step semantics.

η: Local completeness in natural deduction.

Local reducibility in natural deduction.

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

Big-step natural semantics.

η: Global completeness in natural deduction.

Global reducibility in natural deduction.

let parser = lalrpop_lambda::parse::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(false));

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

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

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

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

let env = map! {
    variable!(id) => abs!{x.x},
//     variable!(a) => app!(id,"a".into()),
    variable!(x) => 1.into(),
};
assert_eq!(None, var!(q).resolve::<u64>(&env));
assert_eq!(Some(1), var!(x).resolve::<u64>(&env));
// assert_eq!(Some("a"), var!(a).resolve::<String>(&env));
// assert_eq!(Some((1,2)), var!(id).resolve::<(u64,u64)>(&env)(1,2));
// assert_eq!(None, abs!{x.x}.resolve::<Fn()>(&env));

Trait Implementations

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<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 From<u64> for Expression

Church encoded natural numbers

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

type Output = Self

The resulting type after applying the + operator.

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

Performs the + operation.

impl Mul<Expression> for Expression

type Output = Self

The resulting type after applying the * operator.

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

Performs the * operation.