1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
//! 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`](enum.Term.html). 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`](fn.var.html), [`lam`](fn.lam.html), [`app`](fn.app.html) //! and the macro [`app!`](macro.app.html). //! //! ## the parser //! //! The parser of the library supports the classic notation. The parser is //! invoked by calling the function [`parse`](fn.parse.html). 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`](fn.parse_str.html). //! //! * 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 <br/>`((λ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`](fn.alpha.html) or the associated function //! [`Term::alpha`](enum.Term.html#method.alpha). We must tell those functions //! which strategy to use for renaming variables. The strategy is specified as //! a type parameter, <br/>e.g. `alpha::<Enumerate>(&expr)`. //! //! The trait [`AlphaRename`](trait.AlphaRename.html) defines the strategy for //! renaming variables in case of possible name clashes. The provided //! implementations are [`Enumerate`](struct.Enumerate.html) and //! [`Prime`](struct.Prime.html). //! //! ### β-reduction //! //! β-reduction evaluates function applications according a chosen strategy. //! //! To execute β-reduction on a term we use either the standalone function //! [`reduce`](fn.reduce.html) or the associated function //! [`Term::reduce`](enum.Term.html#method.reduce). We must tell those functions //! which strategy we want ot use for reduction. The strategy is specified as //! a type parameter, <br/>e.g. `reduce::<NormalOrder>(&expr)`. //! //! The trait [`BetaReduce`](trait.BetaReduce.html) defines the strategy //! applied when performing a β-reduction. The provided implementations are: //! //! * [`CallByName`](struct.CallByName.html): //! call-by-name reduction to weak head normal form //! * [`NormalOrder`](struct.NormalOrder.html): //! normal-order reduction to normal form //! * [`CallByValue`](struct.CallByValue.html): //! call-by-value reduction to weak normal form //! * [`ApplicativeOrder`](struct.ApplicativeOrder.html): //! applicative-order reduction to normal form //! * [`HybridApplicativeOrder`](struct.HybridApplicativeOrder.html): //! hybrid-applicative-order reduction to normal form //! * [`HeadSpine`](struct.HeadSpine.html): //! head-spine reduction to head normal form //! * [`HybridNormalOrder`](struct.HybridNormalOrder.html): //! hybrid-normal-order reduction to normal form //! //! [lambda calculus]: https://en.wikipedia.org/wiki/Lambda_calculus //! //! ## 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: //! //! ```text //! I => λa.a //! K => λa.λb.a //! AND => λp.λq.p q p //! ``` //! //! then we could write expressions like: //! //! ```text //! AND K (K I) //! ``` //! //! which during evaluation will be expanded to: //! //! ```text //! ((λ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`](combinator/index.html) //! : defines combinators, like those of the SKI and the BCKW system //! * module [`church_encoded`](church_encoded/index.html) //! : 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. #![doc(html_root_url = "https://docs.rs/lamcal/0.4.0")] #![warn( bare_trait_objects, missing_copy_implementations, missing_debug_implementations, missing_docs, trivial_casts, trivial_numeric_casts, //unsafe_code, unstable_features, unused_extern_crates, unused_import_braces, unused_qualifications, )] #[cfg(test)] #[macro_use] extern crate proptest; #[cfg(feature = "failure")] #[macro_use] extern crate failure; #[macro_use] mod term; mod reduction; #[macro_use] pub mod environment; pub mod church_encoded; pub mod combinator; pub mod inspect; pub mod parser; pub use self::environment::Environment; pub use self::parser::{parse, parse_str, ParseError}; pub use self::reduction::{ alpha, apply, evaluate, evaluate_inspected, expand, expand_inspected, reduce, reduce_inspected, substitute, AlphaRename, ApplicativeOrder, BetaReduce, CallByName, CallByValue, Enumerate, HeadSpine, HybridApplicativeOrder, HybridNormalOrder, NormalOrder, Prime, }; pub use self::term::{app, lam, var, Term, VarName}; impl Default for Environment { /// Creates an `Environment` containing predefined bindings to all the /// standard terms, combinators and data encoding terms that are provided /// by this crate. fn default() -> Self { let mut env = Environment::new(); env.extend(combinator::default_bindings()); env.extend(church_encoded::default_bindings()); env } }