# Enum lamcal::Term[−][src]

```pub enum Term {
Var(VarName),
Lam(VarName, Box<Term>),
App(Box<Term>, Box<Term>),
}```

A term in the lambda calculus.

## Variants

A variable (x)

A character or string representing a parameter or mathematical/logical value.

An abstraction (λx.M)

Function definition (M is a lambda term). The variable x becomes bound in the expression.

An application (M N)

Applying a function to an argument. M and N are lambda terms.

## Methods

### `impl Term`[src]

#### `pub fn free_vars(&self) -> HashSet<&VarName>`[src]

Returns a set of references to all free variables in this term.

### `impl Term`[src]

#### `pub fn is_beta_redex(&self) -> bool`[src]

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]

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]

Performs an α-conversion on this `Term`.

#### `pub fn substitute(&mut self, var: &VarName, rhs: &Term)`[src]

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]

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]

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]

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]

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]

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]

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]

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]

#### `fn fmt(&self, f: &mut Formatter) -> Result`[src]

Formats the value using the given formatter. Read more

### `impl Clone for Term`[src]

#### `fn clone(&self) -> Term`[src]

Returns a copy of the value. Read more

#### `fn clone_from(&mut self, source: &Self)`1.0.0[src]

Performs copy-assignment from `source`. Read more

### `impl PartialEq for Term`[src]

#### `fn eq(&self, other: &Term) -> bool`[src]

This method tests for `self` and `other` values to be equal, and is used by `==`. Read more

#### `fn ne(&self, other: &Term) -> bool`[src]

This method tests for `!=`.

### `impl Hash for Term`[src]

#### `fn hash<__H: Hasher>(&self, state: &mut __H)`[src]

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]

Feeds a slice of this type into the given [`Hasher`]. Read more

### `impl Display for Term`[src]

#### `fn fmt(&self, f: &mut Formatter) -> Result`[src]

Formats the value using the given formatter. Read more

### `impl<'a> From<&'a Term> for Term`[src]

#### `fn from(expr: &Term) -> Self`[src]

Performs the conversion.

### `impl From<VarName> for Term`[src]

#### `fn from(var: VarName) -> Self`[src]

Performs the conversion.

### `impl From<bool> for Term`[src]

#### `fn from(val: bool) -> Self`[src]

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]

#### `fn from(val: u8) -> Self`[src]

Performs the conversion.

### `impl From<u16> for Term`[src]

#### `fn from(val: u16) -> Self`[src]

Performs the conversion.

### `impl From<u32> for Term`[src]

#### `fn from(val: u32) -> Self`[src]

Performs the conversion.

### `impl From<u64> for Term`[src]

#### `fn from(val: u64) -> Self`[src]

Performs the conversion.

### `impl From<u128> for Term`[src]

#### `fn from(val: u128) -> Self`[src]

Performs the conversion.

### `impl From<usize> for Term`[src]

#### `fn from(val: usize) -> Self`[src]

Performs the conversion.