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 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

α-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

β-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:

CallByName: call-by-name reduction to weak head normal form
NormalOrder: normal-order reduction to normal form
CallByValue: call-by-value reduction to weak normal form
ApplicativeOrder: applicative-order reduction to normal form
HybridApplicativeOrder: hybrid-applicative-order reduction to normal form
HeadSpine: head-spine reduction to head normal form
HybridNormalOrder: hybrid-normal-order reduction to normal form

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:

AND K (K I)

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.

Re-exports

pub use self::environment::Environment;

pub use self::parser::parse;

pub use self::parser::parse_str;

pub use self::parser::ParseError;

Modules

church_encoded	Church encoding of data types, data structures and operations.
combinator	Standard terms and combinators
environment	The environment is the context in which a lambda term is evaluated.
inspect	The inspection mechanism for tracing and interrupting reduction and evaluation functions.
parser	The parser that transform expressions into a `Term`.

Macros

app	Constructs a `Term` from a sequence of function applications.
bind	Constructs a `Binding`s from an identifier to a `Term`.
binds	Constructs a set of `Binding`s from identifier to `Term`.

Structs

ApplicativeOrder	Applicative-Order β-reduction to normal form.
CallByName	Call-By-Name β-reduction to weak head normal form.
CallByValue	Call-By-Value β-reduction to weak normal form.
Enumerate	Implementation of `AlphaRename` that appends an increasing number to the name.
HeadSpine	Head-Spine β-reduction to head normal form.
HybridApplicativeOrder	Hybrid-Applicative-Order β-reduction to normal form.
HybridNormalOrder	Hybrid-Normal-Order β-reduction to normal form.
NormalOrder	Normal-Order β-reduction to normal form.
Prime	Implementation of `AlphaRename` that appends a tick symbol `'` at the end of a variable name.
VarName	A name of a variable.

Enums

Term	A term in the lambda calculus.

Traits

AlphaRename	Defines a strategy for renaming variables during α-conversion of terms.
BetaReduce	Defines a strategy for β-reduction of terms.

Functions

alpha	Performs an α-conversion on a given lambda expression and returns the result as a new `Term`.
app	Constructs a function application with the `lhs` term to be applied to the `rhs` term.
apply	Applies a given lambda abstraction to the given substitution term and returns the result as a new `Term`.
evaluate	Evaluates a lambda expression in the given environment.
evaluate_inspected	Evaluates a lambda expression with inspection in the given environment.
expand	Replaces free variables in a term with the term that is bound to the variable's name in the given environment.
expand_inspected	Replaces free variables in a term with the term that is bound to the variable's name in the given environment.
lam	Constructs a lambda abstraction with given parameter and body.
reduce	Performs a β-reduction on a given lambda expression applying the given reduction strategy.
reduce_inspected	Performs a [β-reduction] on a given lambda expression with inspection applying the given reduction strategy and inspection.
substitute	Replaces all free occurrences of the variable `var` in the expression `expr` with the expression `subst` and returns the resulting expression.
var	Constructs a variable of the given name.