Function lambda_calculus::reduction::beta

pub fn beta(term: Term, order: Order, limit: usize, verbose: bool) -> Term

Performs β-reduction on a Term with the specified evaluation Order, an optional limit on number of reductions (0 means no limit) and optional display of reduction steps; it returns the Term after reductions.

Example

use lambda_calculus::*;

let expression = parse(&"(λa.λb.λc.a (λd.λe.e (d b)) (λd.c) (λd.d)) (λa.λb.a b)", Classic);
let reduced    = parse(&"λa.λb.b", Classic);

assert!(expression.is_ok());
assert!(reduced.is_ok());
assert_eq!(beta(expression.unwrap(), NOR, 0, false), reduced.unwrap());