Towards a verifiable topology of data

Towards a verifiable topology of data Laureano Lambán (U. La Rioja) Francisco J. Martín-Mateos (U. Sevilla) Julio Rubio (U. La Rioja) José L. Ruiz-Reina (U. Sevilla) Schedule •Mathematical background. •Persistent homology over a field. an elementary divisor ring. •Formalisation in ACL2. Mathematical backgroud Simplicial Complex V ordered set Simplicial Complex (over V) •K  Pfin (V), K closed under the subset relation •Sn(K), “simplices whose cardinality is n+1” •σ in : Sn(K)  Sn-1(K), σ in(v0,..,vn)=(v0,..,vi-1,vi+1,..vn) Mathematical backgroud Chain Complex R ring Chain Complex (over R) C*= {(Cn,dn) / nϵZ} •Cn , R-module •dn: Cn Cn-1, morphism of R-modules, n •dn dn+1=0, n Mathematical backgroud Chain Complex associated with a simplicial complex K K simplicial complex. C*(K) is given by: •Cn(K), free R-module over Sn(K) •dn = −1 𝑖 σ in 𝑛 𝑖=0 Mathematical backgroud Homology K simplicial complex. The n-th homology group of K Hn(K) = Zn Bn (d2= 0 implies Im dn+1= Bn≤ Zn= Ker dn) Mathematical backgroud Filtration  Filtration of a simplical complex K K1  K2 ….  Kd =K (K is a filtered simplicial complex) Filtration of chain complexes f0 f1 f2 C0 *  C1 *  C* 2 … (fi is a morphism of chain complexes) Mathematical backgroud Induced filtration induces A filtration of simplicial complexes K0K1K2…Kd = K C*(K0)  C*(K1) … C*(Kd) a filtration of chain complexes (arrows are inclusion maps) Mathematical backgroud Persistent homology A filtration of simplicial complexes K0K1K2…Kd = K The p-persistent n-dimensional homology group of K j is given by Hn j, p = Zn j Bn p ∩ Zn j (j≤ p) (Znj ≤ Znp ≤ Cn( Kp) and Bnp ≤ Cn( Kp) ) Computing persistent homology (over an ED-ring R) Existence of echelon form R is an effecctive Bezout domain. Th1: Existence of echelon form (A ∈ M(nxm,R)) “There exists P invertible s.t. echelonForm(AP)” (P is a sequence of Bezout and permutation “elementary operations”) Computing persistent homology (over an ED-ring R) Generalized echelon form s≥n s<n A1 0 A1 * 0 a echelonForm(A,s) A ∈ M(nxm,R) true (a≠0) and echelonForm(A1,s) Computing persistent homology (over an ED-ring R) Generalized echelon form echelonForm (A,s) A1 A2 A = Computing persistent homology (over an ED-ring R) Graded matrices Graded matrix A ∈ M(nxm,R) 0 ≤ j1≤j2≤….. ≤jd= 𝑛 0 ≤ i1≤ i2≤….. ≤ id= 𝑚 Computing persistent homology (over an ED-ring R) Graded matrices A filtration of simplicial complexes K0  K1  K2… Kd = K The standard matrix representation of the differential map dn={dn i:Cn(Ki) → Cn-1(Ki)} is a graded matrix. Computing persistent homology (over an ED-ring R) Graded matrices A = i=1,2,…,p represent the filtration index Computing persistent homology (over an ED-ring R) Graded echelon form R is an effecctive Bezout domain. Th2: “Existence of graded echelon form” Input: (A,s,t) A ∈ M(nxm,R), graded matrix 0≤s ≤ t ≤ d Computing persistent homology (over an ED-ring R) Graded echelon form R is an effecctive Bezout domain. Th2: “Existence of graded echelon form” Input: (A, s, t) Output: (Ps, Ps+1,..,Pt) Pi are invertible matrices echelonForm(Ei , s), where Ei = Ai Pi , and… Computing persistent homology (over an ED-ring R) Graded echelon form Ei= E i 1 E i 2 Ei = Ai Pi Ei1∈ M(_x bi , R) Pi-1 1..b(i-1) * 0 Pi = Computing persistent homology (over an ED-ring R) Smith normal form R is an elementary divisor ring. Th3: “Existence of Smith normal form” Input: A (A ∈ M(nxm,R) ) Output: ((d1,…,dr), P, R) P, Q invertible matrices di|di+1 (i=1..r-1) PAQ=DiagonalMatrix (d1,…,dr,0,..,0) Formalisation in ACL2 •Our goal: implement and formally verify this algorithm in the ACL2 Theorem Prover •This means to implement and verify Echelon form Graded echelon form Smith normal form Formalisation in ACL2 One of our main concerns is efficiency Advantage of using ACL2: we verify Common Lisp code. But ACL2 is an applicative subset of CL. In principle, we have not CL arrays, only lists. Fortunately, we can use stobjs (single-threaded objects), which alllows destructive updates and constant-time accesses, without losing the applicative semantic. Formalisation in ACL2 What we have now: An array-based version of echelon form algorithm (“efficient” but unverified). A list-based version of echelon form and Smith form algorithms (still unverified). Infrastructure proving operational equivalence between both approaches. Our goal: reasoning using the second approach and executing using the first one.