• Toes♀@ani.social
    link
    fedilink
    arrow-up
    4
    arrow-down
    6
    ·
    edit-2
    4 days ago

    By god they are right, this might change the future of mathematics!

    
    // 2024‑edition Rust
    use std::rc::Rc;
    
    /// Church numeral: given a successor `s: fn(u32) -> u32`,
    /// returns a function that applies `s` n times.
    type Church = Rc<dyn Fn(fn(u32) -> u32) -> Rc<dyn Fn(u32) -> u32>>;
    
    /// 0 ≡ λs.λx.x
    fn zero() -> Church {
        println!("Define 0");
        Rc::new(|_s| Rc::new(|x| {
            println!("  0 applied to {}", x);
            x
        }))
    }
    
    /// succ ≡ λn.λs.λx. s (n s x)
    fn succ(n: Church) -> Church {
        // `label` is printed *before* the closure is created, so the closure
        // does not capture any non‑'static reference.
        println!("Build successor");
        Rc::new(move |s| {
            // `inner` is the predecessor numeral applied to the same successor
            let inner = n(s);
            Rc::new(move |x| {
                // first run the predecessor
                let y = inner(x);
                println!("  predecessor applied to {} → {}", x, y);
                // then apply the extra successor step
                let z = s(y);
                println!("  +1 applied to {} → {}", y, z);
                z
            })
        })
    }
    
    /// Convert a Church numeral to a Rust integer, printing each step.
    fn to_int(n: &Church) -> u32 {
        let inc: fn(u32) -> u32 = |k| {
            println!("    inc({})", k);
            k + 1
        };
        let f = n(inc);               // f: Rc<dyn Fn(u32) -> u32>
        println!("  evaluate numeral starting at 0");
        f(0)
    }
    
    /// Even ⇔ divisible by 2
    fn is_even(n: &Church) -> bool { to_int(n) % 2 == 0 }
    fn is_odd(n: &Church) -> bool  { !is_even(n) }
    
    fn main() {
        // ---- build the numerals step‑by‑step ----
        let zero = zero();                     // 0
        let one  = succ(zero.clone());         // 1 = succ 0
        let two  = succ(one.clone());          // 2 = succ 1
    
        // ---- show the numeric values (trace) ----
        println!("\n--- evaluating 0 ---");
        println!("0 as integer → {}", to_int(&zero));
    
        println!("\n--- evaluating 1 ---");
        println!("1 as integer → {}", to_int(&one));
    
        println!("\n--- evaluating 2 ---");
        println!("2 as integer → {}", to_int(&two));
    
        // ---- parity of 2 (the proof) ----
        println!("\n--- parity of 2 ---");
        println!("Is 2 even? {}", is_even(&two)); // true
        println!("Is 2 odd?  {}", is_odd(&two));  // false
    
        // Proof: “divisible by 2” ⇔ “even”.
        // Since `is_odd(&two)` is false, no odd number can satisfy the
        // divisibility‑by‑2 condition.
        assert!(!is_odd(&two));
        println!("\nTherefore, no odd number is divisible by 2.");
    }