Module lambda_calculus::reduction [−] [src]

β-reduction for lambda Terms

Enums

The evaluation order of β-reductions. Applicative order will fail to fully reduce expressions containing functions without a normal form, e.g. the Y combinator (they will expand forever). CallByName, HeadSpine and CallByValue orders don't always normalize fully. The default is Normal.

Constants

SHOW_REDUCTIONS

Set to true to see all the steps of β-reductions. The default is false.

Functions

apply	Applies two `Term`s with substitution and variable update, consuming the first one in the process. It produces an `Error` if the first `Term` is not an `Abs`traction.
beta	Performs β-reduction on a `Term` with the specified evaluation `Order` and an optional limit on number of reductions (`0` means no limit).