Crate lalrpop_lambda

This project started as just the parse.lalrpop and AST, but grew into a bit more.

Evaluation of λ-expressions is currently done in a single big-step semantics Expression::normalize function. The reduction strategy is so far only configurable by η.

See the impl From items under Expression. These define conversions between Rust and λ-expressions. These are all defined in mod encode.

use lalrpop_lambda::Expression;
use lalrpop_lambda::parse::ExpressionParser;

// Define an expression parser, for shortest lambda term strings.
let parser = ExpressionParser::new();

// The successor Church numeral function.
let add1 = parser.parse("λn.λf.λx.f (n f x)").unwrap();

// The first two church numerals.
let zero = Expression::from(0u64);
let one = app!({add1},{zero}).normalize(false);
assert_eq!(Expression::from(1u64), one);

// Use a parsed identity function with other `Experssion`s.
let id = parser.parse("λx.x").unwrap();
let id_one = id(Expression::from(1u64)).normalize(false);
assert_eq!(one, id_one);

// Use a parsed identity function with Rust `u64` numbers!
// NOTE: This is a WIP.
let id = parser.parse("λx.x").unwrap();
let u64_id = <fn(u64) -> u64>::from(id.clone());
assert_eq!(1, u64_id(1));

Modules

parse

Parse λ-expressions

Macros

abs	An abstraction (Abs) expression
app	An application (App) expression
map	A HashMap macro like vec!
set	A HashSet macro like set!
var	A variable (Var) expression
variable	A raw Variable
γ	Theory is nothing without application.
λ	The all-powerful λ

Structs

Abstraction	An abstraction over a bound variable
Application	An application of two expressions
Variable	A potentially free variable

Enums

Expression

A mutually recursive definition for all lambda expressions