Enum Term 

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

An untyped lambda calculus term using de Bruijn indices.

Variants

Var(usize)

de Bruijn variable (0 = innermost binder).

Lam(Box<Term>)

Lambda abstraction: λ.body.

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

Application: (f arg).

Implementations

impl Term

pub fn shift(&self, d: isize, cutoff: usize) -> Term

Shift all free variables by d when entering a context of depth cutoff.

pub fn subst(&self, j: usize, sub: &Term) -> Term

Substitute sub for de Bruijn index j in self.

pub fn beta_step_normal(&self) -> Option<Term>

Perform one step of β-reduction (normal order: leftmost-outermost). Returns Some(reduced) if a redex was found, None if already normal.

pub fn normalize(&self, limit: usize) -> (Term, usize)

Fully normalize by normal-order β-reduction (with a step limit to avoid divergence).

pub fn is_normal(&self) -> bool

Check if the term is in beta-normal form.

pub fn size(&self) -> usize

Count the number of nodes in the term tree.

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Term

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

Formats the value using the given formatter.

impl PartialEq for Term

fn eq(&self, other: &Term) -> 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 Eq for Term

impl StructuralPartialEq for Term