lamb 0.1.0

Pure untyped lambda calculus in safe Rust.
Documentation 
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

//! Standard [Term]s and combinators.

use crate::Term;

/// The function composition combinator `B`.
///
/// This is α-equivalent to `λf g x. f (g x)`.
pub fn compose() -> Term<&'static str> {
    lambda!(λ f g x. f (g x))
}

/// The argument flipping combinator `C`.
///
/// This is α-equivalent to `λf x y. f y x`.
pub fn flip() -> Term<&'static str> {
    lambda!(λ f x y. f y x)
}

/// The identity combinator `I`.
///
/// This is α-equivalent to `λx. x`.
pub fn id() -> Term<&'static str> {
    lambda!(λ x. x)
}

/// The constant or discarding combinator `K`.
///
/// This is α-equivalent to `λx y. x`.
pub fn constant() -> Term<&'static str> {
    lambda!(λ x y. x)
}

/// The diverging combinator `Ω`.
///
/// This is α-equivalent to `ω ω`, where `ω` is the self-applying combinator (see [app_self]).
pub fn omega() -> Term<&'static str> {
    app!(app_self(), app_self())
}

/// The reverse application combinator `R`.
///
/// This is α-equivalent to `λx y. y x`.
pub fn app_rev() -> Term<&'static str> {
    lambda!(λ x y. y x)
}

/// The substitution combinator `S`.
///
/// This is α-equivalent to `λx y z. x z (y z)`.
pub fn sub() -> Term<&'static str> {
    lambda!(λ x y z. x z (y z))
}

/// Turing's fixed-point combinator `Θ`.
///
/// This is α equivalent to `(λx y. y (x x y)) (λx y. y (x x y))`.
pub fn fix_turing() -> Term<&'static str> {
    lambda!((λ x y. y (x x y)) (λ x y. y (x x y)))
}

/// The duplicating combinator `W`.
///
/// This is α-equivalent to `λf x. f x x`.
pub fn dup() -> Term<&'static str> {
    lambda!(λ f x. f x x)
}

/// The lazy fixed-point combinator `Y`.
///
/// This is α-equivalent to `λf. (λx. f (x x)) (λx. f (x x))`.
pub fn fix_lazy() -> Term<&'static str> {
    lambda!(λ f. (λ x. f (x x)) (λ x. f (x x)))
}

/// The strict fixed-point combinator `Z`.
///
/// This is α-equivalent to `λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))`.
pub fn fix_strict() -> Term<&'static str> {
    lambda!(λ f. (λ x. f (λ y. x x y)) (λ x. f (λ y. x x y)))
}

/// The universal combinator `i`.
///
/// This is α-equivalent to `λx. x S K`, where `S` is the substitution combinator (see [sub]) and `K` is the constant combinator (see [constant]).
pub fn universal() -> Term<&'static str> {
    abs!(x. app!(var!(x), sub(), constant()))
}

/// The self-application combinator `ω`.
///
/// This is α-equivalent to `λx. x x`.
pub fn app_self() -> Term<&'static str> {
    lambda!(λ x. x x)
}