lambda_types/
math.rs

1use crate::{
2    boolean::{And, False, True},
3    define,
4    primitives::{Composed, Constant, Identity},
5    Function,
6};
7
8/// Church numeral for zero.
9pub type Zero = crate::primitives::SecondOf;
10
11define! {
12    /// Successor function. Returns a number plus one.
13    /// ```text
14    /// λn.λf.λx.f(nfx)
15    /// ```
16    pub fn Successor ::= {
17        N. F. X. { F, { N, F, X }}
18    } where
19        N: F,
20        {N, F}: X,
21        F: {N, F, X};
22
23    /// Adds two church numerals.
24    /// ```text
25    /// S ::= Successor
26    /// λm.λn.mSn
27    /// ```
28    pub fn Add ::= { M. N. { M, Successor, N }} where
29        M: Successor,
30        {M, Successor}: N;
31
32    /// Multiplies two church numerals - this is simply composition.
33    pub fn Multiply ::= { X. Y. (Composed<X, Y>) };
34
35    /// Predecessor function. Gets the number below a given church numeral.
36    /// ```text
37    /// λn.λf.λx. n (λg.λh. h (g f)) (λu.x) (λu.u)
38    /// ```
39    pub fn Predecessor ::= { N. F. X. { N, Pred_1<F>, Constant<X>, Identity }} where
40        N: (Pred_1<F>),
41        {N, Pred_1<F>}: (Constant<X>),
42        {N, Pred_1<F>, Constant<X>}: Identity;
43
44    fn Pred_1<F> ::= { G. H. { H, { G, F }}} where
45        H: {G, F},
46        G: F;
47    
48    /// Subtracts two church numerals.
49    /// ```text
50    /// P ::= Predecessor
51    /// λm.λn.nPm
52    /// ```
53    pub fn Subtract ::= { M. N. { N, Predecessor, M }} where
54        N: Predecessor,
55        {N, Predecessor}: M;
56    
57    /// Raises a numeral to the power of another.
58    /// ```text
59    /// λm.λn.nm
60    /// ```
61    pub fn Exponent ::= { M. N. { N, M }} where N: M;
62
63
64    /// Returns whether a number is zero.
65    /// ```text
66    /// F ::= False
67    /// T ::= True
68    /// λn.n(λx.F)T
69    /// ```
70    pub fn IsZero ::= { N. { N, Constant<False>, True }} where
71        N: (Constant<False>),
72        {N, Constant<False>}: True;
73    
74    
75    /// Returns whether one number is less than or equal to another.
76    /// ```text
77    /// ? ::= IsZero
78    /// - ::= Subtract
79    /// λm.λn.?(-mn)
80    /// ```
81    pub fn Leq ::= { M. N. { IsZero, { Subtract, M, N }}} where
82        Subtract: M,
83        {Subtract, M}: N,
84        IsZero: { Subtract, M, N };
85    
86    
87    /// Returns whether two numbers are equal.
88    /// ```text
89    /// & ::= And
90    /// ≤ ::= Leq
91    /// λm.λn.&(≤mn)(≤nm)
92    /// ```
93    pub fn Eq ::= { M. N. { And, { Leq, M, N }, { Leq, N, M }}} where
94        Leq: M, Leq: N,
95        {Leq, M}: N, {Leq, N}: M,
96        And: {Leq, M, N},
97        {And, { Leq, M, N }}: { Leq, N, M };
98
99    /// Converts a church numeral to a constant number. See [`ConstNumber`].
100    /// ```text
101    /// λn.n(λ{X}.{X + 1}){0}
102    /// ```
103    @[cfg(any(doc, feature = "const-numeral"))]
104    pub fn ToNumber ::= { N. { N, ConstIncrement, ConstNumber<0> }} where
105        N: ConstIncrement,
106        ConstIncrement: (ConstNumber<0>),
107        {N, ConstIncrement}: (ConstNumber<0>);
108
109
110}
111
112// Due to const generics, this has to be explicitly declared.
113/// Increments a [`ConstNumber`] by one. Used to define [`ToNumber`].
114/// ```text
115/// λ{X}.{X + 1}
116/// ```
117#[cfg(any(doc, feature = "const-numeral"))]
118pub struct ConstIncrement;
119/// Constant number returned by converting a church numeral.
120#[cfg(any(doc, feature = "const-numeral"))]
121pub struct ConstNumber<const N: u64>;
122
123#[cfg(any(doc, feature = "const-numeral"))]
124impl<const N: u64> Function<ConstNumber<N>> for ConstIncrement
125where
126    ConstNumber<{ N + 1 }>: Sized,
127{
128    type Output = ConstNumber<{ N + 1 }>;
129}
130
131#[cfg(any(doc, feature = "const-numeral"))]
132impl<const N: u64> ConstNumber<N> {
133    /// Extracts the number argument from a constant number.
134    #[inline]
135    pub const fn value() -> u64 { N }
136}
137
138#[cfg(test)]
139mod test {
140    #![allow(dead_code)]
141    use crate::prelude::*;
142
143    type Two = call!{Successor, { Successor, Zero }};
144    type Three = call!{Successor, Two};
145
146    #[test]
147    fn main() {
148        let _: call!{
149            Eq, {Multiply, Two, Three}, {Add, Three, Three}
150        } = <True>::default();
151    }
152}
lambda_types/math.rs

lambda_types/
math.rs
