# 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

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

## Macros

app |
Constructs a |

bind |
Constructs a |

binds |
Constructs a set of |

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

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 |

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 |

app |
Constructs a function application with the |

apply |
Applies a given lambda abstraction to the given substitution term and
returns the result as a new |

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 |
Constructs a variable of the given name. |