The School of Athens. Raffaello Sanzio da Urbino. 1509-1511

1.1. Types to Tensors

This chapter provides a historical introduction to the tension between continuous and discrete descriptions of reality, providing context for programmers that need to change gears in the way they model reality from the types of software 1.0 to the tensors of software 2.0.

Contents

• Philosophers: Propositions to Probability
• Physicists: Action to Free Energy
• Programmers: Types to Tensors

Aristotle and Euclid to Kolmogorov and Laplace

Programming as a discipline shares the same dream with that of the philosophers of Ancient Greece. That is, to describe continuous, and fuzzy reality with a discrete language called mathematics. Mathematics is like a universal code library that has been maintained for millenia, without version management, a unified namespace, central maintainers, nor a code of conduct! Programmers are heir to a great tradition in describing reality with discrete utterances.

To better understand the zeitgeist of these Greek Mathematicians¹, a good first approximation is picturing the excitement they felt upon realizing that the geometry of the planet and the stars can be reduced to number, as nodifferent than that of the programmer's thrill when diving into the source of kernels, and compilers, understanding how these complex systems are all reduced down to two specific numbers: 0 and 1.

The canonical path taken by the Greeks to learn the mathematics that describe various fidelities of reality² was to attend schools of thought which were dedicated to educate civilization. Of the many mathematicians and philosophers depicted above in Raffaello's School of Athens, the two that are of concern with respect to computation are Aristotle and Euclid. Aristotle, the compiler writer, who developed logic. And Euclid, the

-> merge stepanov and harper/wadler. aristotle's species, genus, and differentia church/turing's tape(TM)/copy-paster(lambda calculus)

PROBLEM OF INDUCTION

H: "All ravens are black" O: "I've only seen black ravens" H=>O: "if all ravens are black, then we will only see black ravens"

H O

T T F T F F T F

enumerate the truth states of H and O, in order to see that O is T does not uniquely determine H.

#![allow(unused)]
fn main() {
enum Nat {
    Zero,
    Succ(Box<Self>)
}

fn gcd(n: Nat) -> Nat {
    todo!()
}

fn pred(n: Nat) -> Option<Nat> {
    match n {
        Nat::Zero => None,
        Nat::Succ(n) => Some(*n),
    }
}
}

#![allow(unused)]
fn main() {
enum List<T> {
    None,
    Some((T, Box<Self>))
}
fn classify_text(in: List<List<Nat>>) -> bool {
    let pos = hs(["good","great","love","amazing","awesome","nice","cool","fantastic","wonderful","happy"]);
    let neg = hs(["bad","terrible","hate","awful","horrible","worse","worst","angry","sad","disappointing"]);
    let mut score: f32 = 0.0;

    for t in tokens.iter() {
        // simple state machine: handle negators/intensifiers/softeners
        if negators.contains(t) { negate_window = 3; continue; }
        if intens.contains(t)   { intensity *= 1.5; continue; }
        if soften.contains(t)   { intensity *= 0.5; continue; }

        let mut val = 0.0;
        if pos.contains(t) { val += 1.0; }
        if neg.contains(t) { val -= 1.0; }

        if negate_window > 0 {
            val = -val;
            negate_window -= 1;
        }

        score += val * intensity;
        intensity = 1.0; // one-shot boost
    }

    let mut score: f32 = 0.0;
}
}

bayes and laplace - Binomial Inference of the Sunrise - Gaussian Inference of Height

one of the first algorithm's was euclid's algorithm. algorithm is a terminating procedure -> today algorithms are evaluated by turing machine or lambda calculus using a computer -> we compute algorithms

what's the algorithm for computing sentiment analysis, speech recognition, or face detection? impossible to enumerate everything.

• aristotle -> laplace
• wittgenstein LT -> PI logic program minsky -> connectionist program rosenblatt types -> tensors (rosenblatt)

Minsky to Rosenblatt

(early wittgenstein to late wittgenstein)

Nat

#![allow(unused)]
fn main() {
#[derive(Debug)]
enum Nat {
    Z,
    S(Box<Self>)
}

fn succ(x: Nat) -> Nat {
    Nat::S(Box::new(x))
}

fn pred(x: Nat) -> Option<Nat> {
    match x {
    Nat::Z => None,
    Nat::S(n) => Some(*n),
    }
}

fn plus(x: Nat, y: Nat) -> Nat {
    match x {
    Nat::Z => y,
    Nat::S(n) => Nat::S(Box::new(plus(*n, y))),
    }
}
}

Correctness

#![allow(unused)]
fn main() {
#[cfg(test)]
mod test_nat {
    use super::*;
    use proptest::prelude::*;
    
    #[test]
    fn test_succ() -> () {
        let two = Nat::S(Box::new(Nat::S(Box::new(Nat::Z))));
        let output = succ(two);
        println!("{:?}", output);
    }

    #[test]
    fn test_pred() -> () {
        let two = Nat::S(Box::new(Nat::S(Box::new(Nat::Z))));
        let output = pred(two);
        println!("{:?}", output);
    }

    #[test]
    fn test_plus() -> () {
        let two = Nat::S(Box::new(Nat::S(Box::new(Nat::Z))));
        let one = Nat::S(Box::new(Nat::Z));
        let output = plus(one, two);
        println!("{:?}", output);
    }
}
}

Performance