Function lambda_calculus::reduction::beta

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

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 reduced Term.

Example

use lambda_calculus::*;

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

assert_eq!(beta(expr, NOR, 0), reduced);