lambda_calculus

lambda_calculus is a simple implementation of the untyped lambda calculus in Rust.

The data and operators follow the Church encoding and the terms are displayed using De Bruijn indices.

The library contains:

• Church numerals and arithmetic operations
• Church booleans
• Church pairs
• Church lists
• standard lambda terms and combinators
• a parser for lambda expressions with De Bruijn indices
• normal order β-reduction with optional display of reduction steps

The implementation tries to find a compromise between the spirit of the lambda calculus and Rust's best practices; the lambda Terms implemented by the library are produced by functions (in order to allow arbitrary application), but they are not Copyable and the methods they provide allow memory-friendly disassembly and referencing their internals.

Documentation

Status

The library is already usable, but it is still a work in progress.

TODO

• classic notation mode ( variable names instead of De Bruijn indices )
• additional reduction strategies
• function optimization