Enum lamcal::Term

pub enum Term {
    Var(String),
    Lam(Var, Box<Term>),
    App(Box<Term>, Box<Term>),
}

A term in the lambda calculus.

Variants

Var(String)

A variable (x)

A character or string representing a parameter or mathematical/logical value.

Lam(Var, Box<Term>)

An abstraction (λx.M)

Function definition (M is a lambda term). The variable x becomes bound in the expression.

App(Box<Term>, Box<Term>)

An application (M N)

Applying a function to an argument. M and N are lambda terms.

Methods

impl Term

pub fn is_beta_redex(&self) -> bool

Returns whether this Term is a beta redex.

A beta redex is a term of the form (λx.A) M

The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules.

pub fn is_beta_normal(&self) -> bool

Returns whether this Term is a beta normal form.

A beta normal form is a term that does not contain any beta redex, i.e. that cannot be further reduced.

pub fn alpha<A>(&mut self) where     A: AlphaRename,

Performs an α-conversion on this Term.

pub fn substitute(&mut self, var: &VarT, rhs: &Term)

Substitutes all occurrences of var as free variables with the expression rhs recursively on the structure of this Term.

pub fn apply<A>(&mut self, rhs: &Term) where     A: AlphaRename,

Applies the expression rhs to the param of this lambda abstraction if this Term is of variant Term::Lam by recursively substituting all occurrences of the bound variable in the body of the lambda abstraction with the expression rhs.

If this Term is not a lambda abstraction this function does nothing.

To avoid name clashes this function performs α-conversions when appropriate. Therefore a strategy for α-conversion must be given as a type parameter.

Example

let mut expr = lam("x", app(var("y"), var("x")));

expr.apply::<Enumerate>(&var("z"));

assert_eq!(expr, app(var("y"), var("z")));

pub fn reduce<B>(&mut self) where     B: BetaReduce,

Performs a β-reduction on this Term.

The reduction strategy to be used must be given as a type parameter, like in the example below.

Example

let mut expr = app![
    lam("a", var("a")),
    lam("b", lam("c", var("b"))),
    var("x"),
    lam("e", var("f"))
];

expr.reduce::<NormalOrder<Enumerate>>();

assert_eq!(expr, var("x"));

Trait Implementations

impl Debug for Term

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

Formats the value using the given formatter.

impl Clone for Term

fn clone(&self) -> Term

Returns a copy of the value.

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

Performs copy-assignment from source.

impl PartialEq for Term

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

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

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

This method tests for !=.

impl Eq for Term

impl Hash for Term

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where     H: Hasher,

Feeds a slice of this type into the given [Hasher].

impl Display for Term

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

Formats the value using the given formatter.

impl<'a> From<&'a Term> for Term

fn from(expr: &Term) -> Self

Performs the conversion.

impl From<Var> for Term

fn from(var: Var) -> Self

Performs the conversion.