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.

Modules

church_encoded	Church encoding of data types, data structures and operations.
combinator	Standard terms and combinators

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.
Binding	A binding definition.
CallByName	Call-By-Name β-reduction to weak head normal form.
CallByValue	Call-By-Value β-reduction to weak normal form.
CharPosition	Represents a position in a stream of `char`s.
Enumerate	Implementation of `AlphaRename` that appends an increasing number to the name.
Environment	The environment in which lambda terms get evaluated.
HeadSpine	Head-Spine β-reduction to head normal form.
Hint	A hint how to avoid an error.
HybridApplicativeOrder	Hybrid-Applicative-Order β-reduction to normal form.
HybridNormalOrder	Hybrid-Normal-Order β-reduction to normal form.
NormalOrder	Normal-Order β-reduction to normal form.
ParseError	An error that occurs during parsing of expressions.
Prime	Implementation of `AlphaRename` that appends a tick symbol `'` at the end of a variable name.
VarName	A name of a variable.

Enums

ParseErrorKind	The kind of a parse error.
Term	A term in the lambda calculus.
Token	A token in a lambda expression.

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`.
bind	Constructs a new `Binding` with the given term bound to the given name.
evaluate	Evaluates a lambda expression 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.
hint	Constructs a `Hint` from a type that can be converted into a `String`.
lam	Constructs a lambda abstraction with given parameter and body.
parse	Parses the input into a `Term`.
parse_str	Parses a `str` slice into `Term`.
parse_tokens	Parses a list of `Token`s into a `Term`.
pos	Constructs a `CharPosition` from line and column.
reduce	Performs a β-reduction on a given lambda expression applying the given reduction strategy.
substitute	Replaces all free occurrences of the variable `var` in the expression `expr` with the expression `subst` and returns the resulting expression.
tokenize	Converts a stream of `char`s into a list of `Token`s.
tokenize_str	Converts a `str` slice into a list of `Token`s.
var	Constructs a variable of the given name.