Crate lamcal[][src]

A lambda calculus parser and evaluator library.

This crate implements an untyped lambda calculus with the notation of a term as the main data type. A term is either a variable, a lambda abstraction or a function application.

the term

The lambda term is the main data type in lamcal. A lambda term is represented by the enum Term. Its variants are:

  • Term::Var for variables
  • Term::Lam for lambda abstractions
  • Term::App for function applications

We can construct lambda terms programmatically by using the convenient functions var, lam, app and the macro app!.

the parser

The parser of the library supports the classic notation. The parser is invoked by calling the function parse. The input of the parse method can be any data structure that provides an Iterator over char items. To parse a term from a str slice we can use the function parse_str.

  • Variables can be single unicode alphanumeric characters or names with multiple characters where the first character must be a unicode alphanumeric character. The characters following the first character can be unicode letters, digits, the underscore _ or the tick ' character.
  • Lambda abstractions start with the greek lowercase letter lambda λ or alternatively with a backslash \ for easier typing on traditional keyboards. Then follows a variable name as the parameter and a dot . that separates the parameter from the body.
  • Function applications are written as two terms side by side separated by whitespace.
  • Parenthesis can be used to group terms and clarify precedence. Outermost parenthesis can be omitted.
  • Function applications are left associative. This means the expression (λx.x) y z is equivalent to the expression
    ((λx.x) y) z.
  • Abstraction bodies are expanded to the right as far as possible. This means the expression λx.x y z is equivalent to the expression λx.(x y z). To apply this abstraction to a variable a we have to use parenthesis like so (λx.x y z) a.

the reduction system

The reduction system implements α-conversion and β-reduction.

The functions of the reduction system are provided in two variants: as standalone function and associated function on Term. The standalone function takes the input term by reference and returns the result in a new instance of Term while the input term remains unchanged. The functions associated on Term take the term by mutable reference and apply the reduction on the term in place.

As their are several possible ways (strategies) to implement the reduction rules for α- and β-reduction those strategies are defined as traits. The reduction system is designed based on these traits so that users of the crate can easily implement their own strategies and use them with all the functionality provided by this library.


α-conversion renames bound variables if the name conflicts with a free variable in a function application.

To execute α-conversion on a term we use either the standalone function alpha or the associated function Term::alpha. We must tell those functions which strategy to use for renaming variables. The strategy is specified as a type parameter,
e.g. alpha::<Enumerate>(&expr).

The trait AlphaRename defines the strategy for renaming variables in case of possible name clashes. The provided implementations are Enumerate and Prime.


β-reduction evaluates function applications according a chosen strategy.

To execute β-reduction on a term we use either the standalone function reduce or the associated function Term::reduce. We must tell those functions which strategy we want ot use for reduction. The strategy is specified as a type parameter,
e.g. reduce::<NormalOrder>(&expr).

The trait BetaReduce defines the strategy applied when performing a β-reduction. The provided implementations are:

the environment and bindings

The lambda calculus in this crate can evaluate terms in a given environment. The environment holds bindings of lambda terms to a name. During evaluation in an environment all free variables that have a name bound to a term defined in the environment are substituted with the bound term.

With the addon of an environment to the lambda calculus we can prepare a set of often used terms and bind them to meaningful names. Then we are able to write complex expression by using just the bound names instead of the whole terms. For example lets assume we have defined the following bindings in an environment:

I => λa.a
K => λa.λb.a
AND => λp.λq.p q p

then we could write expressions like:


which during evaluation will be expanded to:

((λp.λq.p q p) λ.a.λb.a) ((λa.λb.a) λa.a)

We see the first expression is much shorter. And this is just a very simple example. With more complex expressions the advantage can be huge.

predefined terms and the default environment

This crate provides predefined terms like combinators and encodings of data types, data structures and operators. Those predefined terms are bound to common names and added to the default environment.

The predefined terms are organized in the following modules:

  • module combinator : defines combinators, like those of the SKI and the BCKW system
  • module church_encoded : defines Church encodings of data types, data structures and operators.

The default environment instantiated by calling Environment::default() contains bindings for all predefined terms provided by this crate.


pub use self::environment::Environment;
pub use self::parser::parse;
pub use self::parser::parse_str;
pub use self::parser::ParseError;



Church encoding of data types, data structures and operations.


Standard terms and combinators


The environment is the context in which a lambda term is evaluated.


The inspection mechanism for tracing and interrupting reduction and evaluation functions.


The parser that transform expressions into a Term.



Constructs a Term from a sequence of function applications.


Constructs a Bindings from an identifier to a Term.


Constructs a set of Bindings from identifier to Term.



Applicative-Order β-reduction to normal form.


Call-By-Name β-reduction to weak head normal form.


Call-By-Value β-reduction to weak normal form.


Implementation of AlphaRename that appends an increasing number to the name.


Head-Spine β-reduction to head normal form.


Hybrid-Applicative-Order β-reduction to normal form.


Hybrid-Normal-Order β-reduction to normal form.


Normal-Order β-reduction to normal form.


Implementation of AlphaRename that appends a tick symbol ' at the end of a variable name.


A name of a variable.



A term in the lambda calculus.



Defines a strategy for renaming variables during α-conversion of terms.


Defines a strategy for β-reduction of terms.



Performs an α-conversion on a given lambda expression and returns the result as a new Term.


Constructs a function application with the lhs term to be applied to the rhs term.


Applies a given lambda abstraction to the given substitution term and returns the result as a new Term.


Evaluates a lambda expression in the given environment.


Evaluates a lambda expression with inspection in the given environment.


Replaces free variables in a term with the term that is bound to the variable's name in the given environment.


Replaces free variables in a term with the term that is bound to the variable's name in the given environment.


Constructs a lambda abstraction with given parameter and body.


Performs a β-reduction on a given lambda expression applying the given reduction strategy.


Performs a [β-reduction] on a given lambda expression with inspection applying the given reduction strategy and inspection.


Replaces all free occurrences of the variable var in the expression expr with the expression subst and returns the resulting expression.


Constructs a variable of the given name.