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);Sourcepub fn max_depth(&self) -> u32
pub fn max_depth(&self) -> u32
Returns the maximum depth of lambda abstractions
in the given Term.
§Example
use lambda_calculus::*;
assert_eq!(abs(Var(1)).max_depth(), 1);Sourcepub fn is_isomorphic_to(&self, other: &Term) -> bool
pub fn is_isomorphic_to(&self, other: &Term) -> bool
Returns true if self is structurally isomorphic to other.
§Example
use lambda_calculus::*;
let term1 = abs(Var(1)); // λ 1
let term2 = abs(Var(2)); // λ 2
let term3 = abs(Var(1)); // λ 1
assert_eq!(term1.is_isomorphic_to(&term2), false);
assert_eq!(term1.is_isomorphic_to(&term3), true);
Sourcepub fn has_free_variables(&self) -> bool
pub fn has_free_variables(&self) -> bool
Returns true if self has any free vairables.
§Example
use lambda_calculus::*;
let with_freevar = abs(Var(2)); // λ 2
let without_freevar = abs(Var(1)); // λ 1
assert!(with_freevar.has_free_variables());
assert!(!without_freevar.has_free_variables());Sourcepub fn max_free_index(&self) -> usize
pub fn max_free_index(&self) -> usize
Calculates the maximum index of any free variable in the term.
The result corresponds to the number of names Context must supply to bind them all.
Sourcepub fn with_context<'a>(&'a self, ctx: &'a Context) -> impl Display + 'a
pub fn with_context<'a>(&'a self, ctx: &'a Context) -> impl Display + 'a
Returns a helper struct that allows displaying the term with a given context.
§Example
use lambda_calculus::{*, term::Context};
let term = abs(Var(2)); // λa.b
let ctx = Context::new(&["x"]); // Predefine "x" as a free variable
// The context defines `Var(2)` as "x" instead of the default "b"
assert_eq!(term.with_context(&ctx).to_string(), "λa.x");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 Abstraction.
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);