Enum lamcal::Term [−][src]
A term in the lambda calculus.
Variants
Var(VarName)
A variable (x)
A character or string representing a parameter or mathematical/logical value.
Lam(VarName, Box<Term>)
An abstraction (λx.M)
Function definition (M is a lambda term). The variable x becomes bound in the expression.
App(Box<Term>, Box<Term>)
An application (M N)
Applying a function to an argument. M and N are lambda terms.
Methods
impl Term
[src]
impl Term
pub fn free_vars(&self) -> HashSet<&VarName>
[src]
pub fn free_vars(&self) -> HashSet<&VarName>
Returns a set of references to all free variables in this term.
impl Term
[src]
impl Term
pub fn is_beta_redex(&self) -> bool
[src]
pub fn is_beta_redex(&self) -> bool
Returns whether this Term
is a beta redex.
A beta redex is a term of the form (λx.A) M
The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules.
Examples
let expr1 = app(lam("a", var("a")), var("x")); assert!(expr1.is_beta_redex()); let expr2 = app(var("x"), lam("a", var("a"))); assert!(!expr2.is_beta_redex()); let expr3 = app(var("x"), app(lam("a", var("a")), var("y"))); assert!(expr3.is_beta_redex());
pub fn is_beta_normal(&self) -> bool
[src]
pub fn is_beta_normal(&self) -> bool
Returns whether this Term
is a beta normal form.
A beta normal form is a term that does not contain any beta redex, i.e. that cannot be further reduced.
pub fn alpha<A>(&mut self, names: &HashSet<&VarName>) where
A: AlphaRename,
[src]
pub fn alpha<A>(&mut self, names: &HashSet<&VarName>) where
A: AlphaRename,
Performs an α-conversion on this Term
.
pub fn substitute(&mut self, var: &VarName, rhs: &Term)
[src]
pub fn substitute(&mut self, var: &VarName, rhs: &Term)
Substitutes all occurrences of var
as free variables with the
expression rhs
recursively on the structure of this Term
.
pub fn apply<A>(&mut self, rhs: &Term) where
A: AlphaRename,
[src]
pub fn apply<A>(&mut self, rhs: &Term) where
A: AlphaRename,
Applies the expression rhs
to the param of this lambda abstraction if
this Term
is of variant Term::Lam
by recursively substituting all
occurrences of the bound variable in the body of the lambda abstraction
with the expression rhs
.
If this Term
is not a lambda abstraction this function does nothing.
To avoid name clashes this function performs α-conversions when
appropriate. Therefore a strategy for α-conversion must be given as the
type parameter A
.
Examples
let mut expr = lam("x", app(var("y"), var("x"))); expr.apply::<Enumerate>(&var("z")); assert_eq!(expr, app(var("y"), var("z")));
pub fn reduce<B>(&mut self) where
B: BetaReduce,
[src]
pub fn reduce<B>(&mut self) where
B: BetaReduce,
Performs a β-reduction on this Term
.
The reduction strategy to be used must be given as the type parameter
B
, like in the example below.
If the reduction of the term diverges it can go through an infinite
sequence of evaluation steps. To avoid endless loops, a default limit
of u32::MAX
reduction steps is applied. Thus this method returns
when either no more reduction is possible or the limit of u32::MAX
iterations has been reached.
Examples
let mut expr = app![ lam("a", var("a")), lam("b", lam("c", var("b"))), var("x"), lam("e", var("f")) ]; expr.reduce::<NormalOrder<Enumerate>>(); assert_eq!(expr, var("x"));
pub fn reduce_inspected<B, I>(&mut self, inspect: &mut I) where
B: BetaReduce,
I: Inspect,
[src]
pub fn reduce_inspected<B, I>(&mut self, inspect: &mut I) where
B: BetaReduce,
I: Inspect,
Performs a [β-reduction] on this Term
with inspection.
The given inspection is called before each contraction (reduction step).
See the documentation of the inspect
module for
information on how to define an inspection and the implementations that
are provided.
The reduction strategy to be used must be given as the type parameter
B
.
pub fn expand(&mut self, env: &Environment)
[src]
pub fn expand(&mut self, env: &Environment)
Replaces free variables with the term bound to the variable's name in the given environment.
This method walks through the whole term and replaces any free variable with the term bound to the variable's name in the given environment. Bound variables are not replaced.
This method modifies this Term
in place. If you want to expand named
constants and get the result as a new Term
while keeping the original
Term
unchanged use the standalone function expand
instead.
Examples
let env = Environment::default(); let mut expr = app![ var("C"), lam("a", app(var("K"), var("I"))), var("e"), var("f") ]; expr.expand(&env); assert_eq!( expr, app![ lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))), lam("a", app(lam("a", lam("b", var("a"))), lam("a", var("a")))), var("e"), var("f") ] );
pub fn expand_inspected(
&mut self,
env: &Environment,
inspect: &mut impl Inspect
)
[src]
pub fn expand_inspected(
&mut self,
env: &Environment,
inspect: &mut impl Inspect
)
Replaces free variables with the term bound to the variable's name in the given environment with inspection.
This method walks through the whole term and replaces any free variable with the term bound to the variable's name in the given environment. Bound variables are not replaced.
Before each substitution of a variable with its bound term from the
environment the given inspection is called. See the documentation
of the inspect
module for information on how to
define an inspection and the implementations that are provided.
This method modifies this Term
in place. If you want to expand named
constants and get the result as a new Term
while keeping the original
Term
unchanged use the standalone function
expand
instead.
Examples
let env = Environment::default(); let mut expr = app![ var("C"), lam("a", app(var("K"), var("I"))), var("e"), var("f") ]; let mut collected = Collect::new(); expr.expand_inspected(&env, &mut collected); assert_eq!( collected.terms(), &vec![ app![ var("C"), lam("a", app(var("K"), var("I"))), var("e"), var("f") ], app![ lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))), lam("a", app(var("K"), var("I"))), var("e"), var("f") ], app![ lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))), lam("a", app(lam("a", lam("b", var("a"))), var("I"))), var("e"), var("f") ], ][..], ); assert_eq!( expr, app![ lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))), lam("a", app(lam("a", lam("b", var("a"))), lam("a", var("a")))), var("e"), var("f") ] );
pub fn evaluate<B>(&mut self, env: &Environment) where
B: BetaReduce,
[src]
pub fn evaluate<B>(&mut self, env: &Environment) where
B: BetaReduce,
Evaluates this lambda expression in the given environment.
Evaluation comprises the following steps in the given order:
- expand all named constants with their bound terms found in the environment recursively
- perform β-reduction on the expression
- perform α-conversion where needed to avoid name clashes
For the β-reduction step a reduction strategy is required. Therefore the
reduction strategy must be specified as the type parameter B
.
The expansion of named constants step as done by this function is
equivalent to calling the
Term::expand
method. Similar the
β-reduction step performed by this the function is equivalent to calling
the Term::reduce
method.
Examples
let env = Environment::default(); let mut expr = app![ var("C"), lam("x", lam("y", app(var("x"), var("y")))), var("e"), var("f") ]; expr.evaluate::<NormalOrder<Enumerate>>(&env); assert_eq!(expr, app(var("f"), var("e")));
pub fn evaluate_inspected<B, I>(&mut self, env: &Environment, inspect: &mut I) where
B: BetaReduce,
I: Inspect,
[src]
pub fn evaluate_inspected<B, I>(&mut self, env: &Environment, inspect: &mut I) where
B: BetaReduce,
I: Inspect,
Evaluates this lambda expression with inspection in the given environment.
For the β-reduction step a reduction strategy is required. Therefore the
reduction strategy must be specified as the type parameter B
.
The given inspection is called before each substitution of a free
variable with its bound term and before each contraction (reduction
step). See the documentation of the inspect
for information on how to define an inspection and the implementations
that are provided.
Examples
let env = Environment::default(); let mut expr = app![ var("C"), lam("x", lam("y", app(var("x"), var("y")))), var("e"), var("f") ]; let mut collected = Collect::new(); expr.evaluate_inspected::<NormalOrder<Enumerate>, _>(&env, &mut collected); assert_eq!( collected.terms(), &vec![ app![ var("C"), lam("x", lam("y", app(var("x"), var("y")))), var("e"), var("f") ], app![ lam("a", lam("b", lam("c", app![var("a"), var("c"), var("b")]))), lam("x", lam("y", app(var("x"), var("y")))), var("e"), var("f") ], app![ lam( "b", lam( "c", app![ lam("x", lam("y", app(var("x"), var("y")))), var("c"), var("b") ] ) ), var("e"), var("f") ], app![ lam( "b", lam("c", app![lam("y", app(var("c"), var("y"))), var("b")]) ), var("e"), var("f") ], app![ lam("b", lam("c", app(var("c"), var("b")),)), var("e"), var("f") ], app![lam("c", app(var("c"), var("e"))), var("f")], ][..], ); assert_eq!(expr, app(var("f"), var("e")));
Trait Implementations
impl Debug for Term
[src]
impl Debug for Term
fn fmt(&self, f: &mut Formatter) -> Result
[src]
fn fmt(&self, f: &mut Formatter) -> Result
Formats the value using the given formatter. Read more
impl Clone for Term
[src]
impl Clone for Term
fn clone(&self) -> Term
[src]
fn clone(&self) -> Term
Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)
1.0.0[src]
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read more
impl PartialEq for Term
[src]
impl PartialEq for Term
fn eq(&self, other: &Term) -> bool
[src]
fn eq(&self, other: &Term) -> bool
This method tests for self
and other
values to be equal, and is used by ==
. Read more
fn ne(&self, other: &Term) -> bool
[src]
fn ne(&self, other: &Term) -> bool
This method tests for !=
.
impl Eq for Term
[src]
impl Eq for Term
impl Hash for Term
[src]
impl Hash for Term
fn hash<__H: Hasher>(&self, state: &mut __H)
[src]
fn hash<__H: Hasher>(&self, state: &mut __H)
Feeds this value into the given [Hasher
]. Read more
fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
1.3.0[src]
fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
Feeds a slice of this type into the given [Hasher
]. Read more
impl Display for Term
[src]
impl Display for Term
fn fmt(&self, f: &mut Formatter) -> Result
[src]
fn fmt(&self, f: &mut Formatter) -> Result
Formats the value using the given formatter. Read more
impl<'a> From<&'a Term> for Term
[src]
impl<'a> From<&'a Term> for Term
impl From<VarName> for Term
[src]
impl From<VarName> for Term
impl From<bool> for Term
[src]
impl From<bool> for Term
fn from(val: bool) -> Self
[src]
fn from(val: bool) -> Self
Converts a value of type bool
into the Church encoding of its value.
Examples
use lamcal::church_encoded::boolean::{False, True}; use lamcal::{lam, var, Term}; let term: Term = true.into(); assert_eq!(term, True()); assert_eq!(Term::from(false), False()); let term: Term = false.into(); assert_eq!(Term::from(true), lam("a", lam("b", var("a")))); assert_eq!(term, lam("a", lam("b", var("b"))));
impl From<u8> for Term
[src]
impl From<u8> for Term
impl From<u16> for Term
[src]
impl From<u16> for Term
impl From<u32> for Term
[src]
impl From<u32> for Term
impl From<u64> for Term
[src]
impl From<u64> for Term
impl From<u128> for Term
[src]
impl From<u128> for Term
impl From<usize> for Term
[src]
impl From<usize> for Term