Enum lamcal::Term

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

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

pub fn free_vars(&self) -> HashSet<&VarName>

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

impl Term

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

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,

Performs an α-conversion on this Term.

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,

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,

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,

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)

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 )

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,

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,

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

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Clone for Term

fn clone(&self) -> Term

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl PartialEq for Term

fn eq(&self, other: &Term) -> bool

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

fn ne(&self, other: &Term) -> bool

This method tests for !=.

impl Eq for Term

impl Hash for Term

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where     H: Hasher,

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

impl Display for Term

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.

impl<'a> From<&'a Term> for Term

fn from(expr: &Term) -> Self

Performs the conversion.

impl From<VarName> for Term

fn from(var: VarName) -> Self

Performs the conversion.

impl From<bool> for Term

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

fn from(val: u8) -> Self

Performs the conversion.

impl From<u16> for Term

fn from(val: u16) -> Self

Performs the conversion.

impl From<u32> for Term

fn from(val: u32) -> Self

Performs the conversion.

impl From<u64> for Term

fn from(val: u64) -> Self

Performs the conversion.

impl From<u128> for Term

fn from(val: u128) -> Self

Performs the conversion.

impl From<usize> for Term

fn from(val: usize) -> Self

Performs the conversion.