lambda_calculus 3.0.0

A simple, zero-dependency implementation of pure 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
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

//! [Church right fold list](https://ifl2014.github.io/submissions/ifl2014_submission_13.pdf)

use crate::term::{Term, abs, app, UD};
use crate::term::Term::*;
use crate::data::boolean::{tru, fls};
use crate::data::pair::{pair, fst, snd};

/// Produces a `nil`, the last link of a Church-encoded list; equivalent to `boolean::tru`.
///
/// NIL ≡ λab.a ≡ λ λ 2 ≡ TRUE
pub fn nil() -> Term { tru() }

/// Applied to a Church-encoded list it determines if it is empty.
///
/// IS_NIL ≡ λl.l TRUE (λax.FALSE) ≡ λ 1 TRUE (λ λ FALSE)
///
/// # Example
/// ```
/// use lambda_calculus::data::list::church::{is_nil, nil};
/// use lambda_calculus::*;
///
/// assert_eq!(beta(app(is_nil(), nil()), NOR, 0), true.into());
/// ```
pub fn is_nil() -> Term {
    abs(app!(Var(1), tru(), abs!(2, fls())))
}

/// Applied to two terms it returns them contained in a Church-encoded list.
///
/// CONS ≡ λaxnc.c a ((λl.l) x n c) ≡ λ λ λ λ 1 4 ((λ 1) 3 2 1)
///
/// # Example
/// ```
/// use lambda_calculus::data::list::church::{nil, cons};
/// use lambda_calculus::*;
///
/// let list_consed =
///     app!(
///         cons(),
///         1.into_church(),
///         app!(
///             cons(),
///             2.into_church(),
///             app!(
///                 cons(),
///                 3.into_church(),
///                 nil()
///             )
///         )
///     );
///
/// let list_into = vec![1, 2, 3].into_church();
///
/// assert_eq!(
///     beta(list_consed, NOR, 0),
///     list_into
/// );
/// ```
pub fn cons() -> Term {
    abs!(4, app!(
        Var(1),
        Var(4),
        app!(
            abs(Var(1)),
            Var(3),
            Var(2),
            Var(1)
        )
    ))
}

/// Applied to a Church-encoded list it returns its first element.
///
/// HEAD ≡ λl.l UD (λht.h) ≡ λ 1 UD (λ λ 2)
///
/// # Example
/// ```
/// use lambda_calculus::data::list::church::head;
/// use lambda_calculus::*;
///
/// let list = vec![1, 2, 3].into_church();
///
/// assert_eq!(
///     beta(app(head(), list), NOR, 0),
///     1.into_church()
/// );
/// ```
pub fn head() -> Term {
    abs(app!(Var(1), UD, abs!(2, Var(2))))
}

/// Applied to a Church-encoded list it returns a new list with all its elements but the first one.
///
/// TAIL ≡ λl.FST (l (PAIR UD NIL) (λap. PAIR (SND p) (CONS a (SND p))))
///      ≡ λ FST (1 (PAIR UD NIL) (λ λ PAIR (SND 1) (CONS 2 (SND 1))))
///
/// # Example
/// ```
/// use lambda_calculus::data::list::church::tail;
/// use lambda_calculus::*;
///
/// let list = vec![1, 2, 3].into_church();
///
/// assert_eq!(
///     beta(app(tail(), list), NOR, 0),
///     vec![2, 3].into_church()
/// );
/// ```
pub fn tail() -> Term {
    abs(app!(
        fst(),
        app!(
            Var(1),
            app!(pair(), UD, nil()),
            abs!(2, app!(
                pair(),
                app(snd(), Var(1)),
                app!(
                    cons(),
                    Var(2),
                    app(snd(), Var(1))
                )
            ))
        )
    ))
}