Function lamcal::evaluate[][src]

pub fn evaluate<B>(expr: &Term, env: &Environment) -> Term where
    B: BetaReduce

Evaluates a lambda expression in the given environment.

This function takes the given expression by reference and returns a new Term with the evaluation applied. The given Term remains unchanged.

Evaluation comprises the following steps in the given order:

  • expand all named constants with their bound terms found in the environment recursively
  • perform β-reduction on the expression
  • perform α-conversion where needed to avoid name clashes

For the β-reduction step a reduction strategy is required. Therefore the reduction strategy must be specified as the type parameter B.

The expansion of named constants step as done by this function is equivalent to calling the expand function. Similar the β-reduction step performed by this the function is equivalent to calling the reduce function.

Examples

let env = Environment::default();

let expr = app![
    var("C"),
    lam("x", lam("y", app(var("x"), var("y")))),
    var("e"),
    var("f")
];

let result = evaluate::<NormalOrder<Enumerate>>(&expr, &env);

assert_eq!(result, app(var("f"), var("e")));