Improve performance #17

New issue

Closed

opened 2024-12-08 20:41:09 -08:00 by wball · 1 comment

wball commented

2024-12-08 20:41:09 -08:00

Owner

We're getting to the point where poor performance is starting to be a problem. A useful benchmark to measure against is the proof initial_uniq in category.pg, which on my machine takes about 4s to type check, about 4 times as long as all of peano.pg, so whatever bottleneck we're having, it is very present in initial_uniq. For reference, in case it changes, here's initial_uniq:

def initial_uniq (A B : Obj) (hA : initial A) (hB : initial B) : isomorphic A B :=
    exists_uniq_t_elim (Hom A B) (isomorphic A B) (hA B) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) =>
    exists_uniq_t_elim (Hom B A) (isomorphic A B) (hB A) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) =>
    exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) =>
    exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) =>
        exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f
            (exists_intro (Hom B A) (inv A B f) g
                (and_intro (inv_l A B f g) (inv_r A B f g)
                    (eq_trans (Hom A A) (comp A B A f g) a (id A)
                        (eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g)))
                        (a_uniq (id A)))
                    (eq_trans (Hom B B) (comp B A B g f) b (id B)
                        (eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f)))
                        (b_uniq (id B)))))))));

Potential bottlenecks to investigate:

Redundant type checks in findType
Evaluating unnecessarily far in findBeta (consider not unwrapping Free in head position unless necessary)

We're getting to the point where poor performance is starting to be a problem. A useful benchmark to measure against is the proof `initial_uniq` in `category.pg`, which on my machine takes about 4s to type check, about 4 times as long as all of `peano.pg`, so whatever bottleneck we're having, it is very present in `initial_uniq`. For reference, in case it changes, here's `initial_uniq`: ```perga def initial_uniq (A B : Obj) (hA : initial A) (hB : initial B) : isomorphic A B := exists_uniq_t_elim (Hom A B) (isomorphic A B) (hA B) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) => exists_uniq_t_elim (Hom B A) (isomorphic A B) (hB A) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) => exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) => exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) => exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f (exists_intro (Hom B A) (inv A B f) g (and_intro (inv_l A B f g) (inv_r A B f g) (eq_trans (Hom A A) (comp A B A f g) a (id A) (eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g))) (a_uniq (id A))) (eq_trans (Hom B B) (comp B A B g f) b (id B) (eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f))) (b_uniq (id B))))))))); ``` Potential bottlenecks to investigate: - Redundant type checks in `findType` - Evaluating unnecessarily far in `findBeta` (consider not unwrapping `Free` in head position unless necessary)