Crate lamcal[−][src]

A lambda calculus parser and evaluator library.

This crate implements a pure 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 with its variants Term::Var for variables, Term::Lam for lambda abstractions and 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 lower case letters or names with multiple characters where the first character must be a lower case letter. The characters following the first character can be lower case 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 parser fully supports unicode characters.

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

Macros

app	The app! macro can be used to conveniently construct an sequence of function applications.

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.
CharPosition	Represents a position in a stream of `char`s.
Enumerate	Implementation of `AlphaRename` that appends an increasing number to the name.
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.
Var	A variable with a given name.

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`.
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 `repl` 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.