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

//! Church-encoded boolean [Term]s and operations.

use crate::Term;

/// The Church-encoded boolean `false`.
/// 
/// This is α-equivalent to `λt f. f`.
pub fn fls() -> Term<&'static str> {
    lambda!(λ t f. f)
}

/// The Church-encoded boolean value `true`.
/// 
/// This is α-equivalent to `λt f. t`.
pub fn tru() -> Term<&'static str> {
    lambda!(λ t f. t)
}

/// The `if-then-else` function.
/// 
/// This is α-equivalent to `λc t e. c t e`.
/// Since Church booleans encode this functionality in themselves, this is technically redundant.
pub fn if_then_else() -> Term<&'static str> {
    lambda!(λ c t e. c t e)
}

/// The boolean `not` function.
/// 
/// This is α-equivalent to `λb. if-then-else b fls tru` (see [fls], [tru], and [if_then_else]).
pub fn not() -> Term<&'static str> {
    abs!(b. app!(if_then_else(), var!(b), fls(), tru()))
}

/// The boolean `and` function.
/// 
/// This is α-equivalent to `λl r. l r fls`, where `fls` is the Church-encoded boolean value `false` (see [fls]).
pub fn and() -> Term<&'static str> {
    abs!(l r. app!(var!(l), var!(r), fls()))
}

/// The boolean `or` function.
/// 
/// This is α-equivalent to `λl r. l tru r`, where `tru` is the Church-encoded boolean value `true` (see [tru]).
pub fn or() -> Term<&'static str> {
    abs!(l r. app!(var!(l), tru(), var!(r)))
}