Calculates the "unified bound" of the for metamath theorem reference access sequence

key-dist.rs

// [dependencies]
// metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", tag = "v0.3.7" }
// rand = "0.8"

use metamath_knife::{statement::StatementAddress, verify::ProofBuilder, Database, StatementType};
use rand::Rng;
use std::collections::{hash_map::RandomState, HashMap, HashSet};
use std::ops::Range;

struct Pass<'a>(&'a HashMap<StatementAddress, u32>, &'a mut AccessSeq);

impl ProofBuilder for Pass<'_> {
    type Item = ();
    type Accum = ();

    fn push(&mut self, _: &mut (), _: ()) {}

    fn build(&mut self, addr: StatementAddress, _: (), _: &[u8], _: Range<usize>) {
        if let Some(&i) = self.0.get(&addr) {
            self.1.push(i)
        }
    }
}

#[derive(Default)]
struct AccessSeq {
    seq: Vec<u32>,
    temp: HashSet<u32>,
    sum_score: f64,
    sum_log_score: f64,
    sum_sqrt_score: f64,
}

impl AccessSeq {
    fn push(&mut self, i: u32) {
        let mut best = u32::MAX;
        for &j in self.seq.iter().rev() {
            self.temp.insert(j);
            if self.temp.len() as u32 > best {
                break;
            }
            best = best.min(self.temp.len() as u32 + j.abs_diff(i));
        }
        self.temp.clear();
        if best != u32::MAX {
            let score = best as f64;
            self.sum_score += score;
            self.sum_log_score += score.log2();
            self.sum_sqrt_score += score.sqrt();
        }
        self.seq.push(i)
    }
}

fn main() {
    let mut db = Database::default();
    db.parse("../mm/set.mm".into(), vec![]);
    db.scope_pass();
    let mut map = HashMap::new();
    let mut acc = AccessSeq::default();
    for (i, stmt) in db
        .statements()
        .filter(|stmt| stmt.is_assertion())
        .enumerate()
    {
        map.insert(stmt.address(), i as u32);
    }
    // uncomment to shuffle
    // for (k, (_, v)) in map.iter_mut().enumerate() {
    //     *v = k as u32;
    // }
    let mut acc = AccessSeq::default();
    for stmt in db.statements().filter(|stmt| stmt.is_assertion()) {
        if stmt.statement_type() == StatementType::Provable {
            db.verify_one(&mut Pass(&map, &mut acc), stmt).unwrap();
        }
    }
    // replace the above for loop with this for a comparable completely random access sequence
    // let mut rand = rand::thread_rng();
    // for _ in 0..3075357 {
    //     acc.push(rand.gen_range(0..map.len() as u32));
    // }
    let n = acc.seq.len();
    let AccessSeq { sum_score, sum_log_score, sum_sqrt_score, .. } = acc;
    let avg_score = sum_score / n as f64;
    let avg_log_score = sum_log_score / n as f64;
    let avg_sqrt_score = sum_sqrt_score / n as f64;
    println!("avg score: {sum_score} / {n} = {avg_score:.1}");
    println!("avg lg(score): \
        {sum_log_score:.1} / {n}) = {avg_log_score:.4} = lg({:.4})", avg_log_score.exp2());
    println!("avg sqrt(score): \
        {sum_sqrt_score:.1} / {n} = {avg_sqrt_score:.4} = sqrt({:.4})", avg_sqrt_score.powi(2));
}

// Results on https://github.com/metamath/set.mm/blob/3de3ae5/set.mm
// number of theorems: 42879
//
// avg score: 75178012 / 3075357 = 24.4
// avg lg(score): 10750001.8 / 3075357) = 3.4955 = lg(11.2787)
// avg sqrt(score): 12640434.2 / 3075357 = 4.1102 = sqrt(16.8940)
// 
// shuffled 1:
// avg score: 157481709 / 3075357 = 51.2
// avg lg(score): 12857460.5 / 3075357) = 4.1808 = lg(18.1362)
// avg sqrt(score): 17549817.2 / 3075357 = 5.7066 = sqrt(32.5652)
// 
// shuffled 2:
// avg score: 157220284 / 3075357 = 51.1
// avg lg(score): 12861417.8 / 3075357) = 4.1821 = lg(18.1524)
// avg sqrt(score): 17552661.4 / 3075357 = 5.7075 = sqrt(32.5758)
//
// completely random 1:
// avg score: 565223103 / 3075357 = 183.8
// avg lg(score): 22394511.3 / 3075357) = 7.2819 = lg(155.6242)
// avg sqrt(score): 40151474.7 / 3075357 = 13.0559 = sqrt(170.4559)
// 
// completely random 2:
// avg score: 565104301 / 3075357 = 183.8
// avg lg(score): 22394838.4 / 3075357) = 7.2820 = lg(155.6357)
// avg sqrt(score): 40149999.7 / 3075357 = 13.0554 = sqrt(170.4433)

It's really nice to see a direct application of metamath-knife!

For the record, the required API change will go into v0.3.7:

metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", tag = "v0.3.7" }