Enum lambda_calculus::term::Term
source · pub enum Term {
Var(usize),
Abs(Box<Term>),
App(Box<(Term, Term)>),
}
Expand description
A lambda term that is either a variable with a De Bruijn index, an abstraction over a term or an applicaction of one term to another.
Variants§
Implementations§
source§impl Term
impl Term
sourcepub fn lhs_mut(&mut self) -> Result<&mut Term, TermError>
pub fn lhs_mut(&mut self) -> Result<&mut Term, TermError>
Returns a mutable reference to the left-hand side term of an application.
Example
use lambda_calculus::*;
assert_eq!(app(Var(1), Var(2)).lhs_mut(), Ok(&mut Var(1)));
sourcepub fn is_supercombinator(&self) -> bool
pub fn is_supercombinator(&self) -> bool
Returns true
if self
is a
supercombinator.
Example
use lambda_calculus::*;
let term1 = abs(app(Var(1), abs(Var(1)))); // λ 1 (λ 1)
let term2 = app(abs(Var(2)), abs(Var(1))); // (λ 2) (λ 1)
assert_eq!(term1.is_supercombinator(), true);
assert_eq!(term2.is_supercombinator(), false);
source§impl Term
impl Term
sourcepub fn apply(&mut self, rhs: &Term) -> Result<(), TermError>
pub fn apply(&mut self, rhs: &Term) -> Result<(), TermError>
Applies a Term
to self
via substitution and variable update.
Example
use lambda_calculus::*;
let mut term1 = parse(&"λλ42(λ13)", DeBruijn).unwrap();
let term2 = parse(&"λ51", DeBruijn).unwrap();
let result = parse(&"λ3(λ61)(λ1(λ71))", DeBruijn).unwrap();
term1.apply(&term2);
assert_eq!(term1, result);
Errors
Returns a TermError
if self
is not an Abs
traction.
sourcepub fn reduce(&mut self, order: Order, limit: usize) -> usize
pub fn reduce(&mut self, order: Order, limit: usize) -> usize
Performs β-reduction on a Term
with the specified evaluation Order
and an optional limit
on the number of reductions (0
means no limit) and returns the number of performed
reductions.
Example
use lambda_calculus::*;
let mut expression = parse(&"(λa.λb.λc.b (a b c)) (λa.λb.b)", Classic).unwrap();
let reduced = parse(&"λa.λb.a b", Classic).unwrap();
expression.reduce(NOR, 0);
assert_eq!(expression, reduced);
Trait Implementations§
source§impl PartialEq<Term> for Term
impl PartialEq<Term> for Term
impl Eq for Term
impl StructuralEq for Term
impl StructuralPartialEq for Term
Auto Trait Implementations§
impl RefUnwindSafe for Term
impl Send for Term
impl Sync for Term
impl Unpin for Term
impl UnwindSafe for Term
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more