Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

### The abstract of the Mizar article:

### A Compiler of Arithmetic Expressions for SCM

**by****Grzegorz Bancerek, and****Piotr Rudnicki**- Received December 30, 1993
- MML identifier: SCM_COMP

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_3, FINSEQ_1, AMI_1, INT_1, SCM_1, FUNCT_1, RELAT_1, ARYTM_1, BINTREE1, DTCONSTR, LANG1, AMI_2, TDGROUP, BOOLE, TREES_4, QC_LANG1, CAT_1, NAT_1, TREES_2, MCART_1, FUNCT_2, SQUARE_1, SCM_COMP; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1, MCART_1, FUNCT_1, FUNCT_2, TREES_2, TREES_4, STRUCT_0, AMI_1, AMI_2, AMI_3, FRAENKEL, SCM_1, FINSEQ_1, FINSEQ_2, LANG1, BINTREE1, DTCONSTR, LIMFUNC1; constructors NAT_1, AMI_2, SCM_1, BINTREE1, DTCONSTR, FINSOP_1, LIMFUNC1, MEMBERED, XBOOLE_0; clusters SUBSET_1, INT_1, TREES_3, DTCONSTR, BINTREE1, AMI_1, AMI_3, RELSET_1, STRUCT_0, AMI_2, XBOOLE_0, NAT_1, FRAENKEL, MEMBERED, ZFMISC_1, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Auxiliary theorems about SCM theorem :: SCM_COMP:1 for I1, I2 being FinSequence of the Instructions of SCM, D being FinSequence of INT, il, ps, ds being Nat, s being State-consisting of il, ps, ds, I1^I2, D holds s is State-consisting of il, ps, ds, I1, D & s is State-consisting of il, (ps+len I1), ds, I2, D; theorem :: SCM_COMP:2 for I1, I2 being FinSequence of the Instructions of SCM, il, ps, ds, k, il1 being Nat, s being State-consisting of il, ps, ds, I1^I2, <*>INT, u being State of SCM st u = (Computation s).k & il.il1 = IC u holds u is State-consisting of il1, (ps + len I1), ds, I2, <*>INT; definition func SCM-AE -> binary with_terminals with_nonterminals with_useful_nonterminals strict (non empty DTConstrStr) means :: SCM_COMP:def 1 Terminals it = SCM-Data-Loc & NonTerminals it = [:1, 5:] & for x, y, z being Symbol of it holds x ==> <*y, z*> iff x in [:1, 5:]; end; definition mode bin-term is Element of TS SCM-AE; end; definition let nt be NonTerminal of SCM-AE; let tl, tr be bin-term; redefine func nt-tree (tl, tr) -> bin-term; end; definition let t be Terminal of SCM-AE; redefine func root-tree t -> bin-term; end; definition let t be Terminal of SCM-AE; func @t -> Data-Location equals :: SCM_COMP:def 2 t; end; theorem :: SCM_COMP:3 for nt being NonTerminal of SCM-AE holds nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4]; theorem :: SCM_COMP:4 [0,0] is NonTerminal of SCM-AE & [0,1] is NonTerminal of SCM-AE & [0,2] is NonTerminal of SCM-AE & [0,3] is NonTerminal of SCM-AE & [0,4] is NonTerminal of SCM-AE; definition let t1, t2 be bin-term; func t1+t2 -> bin-term equals :: SCM_COMP:def 3 [0,0]-tree(t1, t2); func t1-t2 -> bin-term equals :: SCM_COMP:def 4 [0,1]-tree(t1, t2); func t1*t2 -> bin-term equals :: SCM_COMP:def 5 [0,2]-tree(t1, t2); func t1 div t2 -> bin-term equals :: SCM_COMP:def 6 [0,3]-tree(t1, t2); func t1 mod t2 -> bin-term equals :: SCM_COMP:def 7 [0,4]-tree(t1, t2); end; theorem :: SCM_COMP:5 :: PRE_COMP_5: for term being bin-term holds (ex t being Terminal of SCM-AE st term = root-tree t) or ex tl, tr being bin-term st term = tl+tr or term = tl-tr or term = tl*tr or term = tl div tr or term = tl mod tr; definition let o be NonTerminal of SCM-AE, i, j be Integer; func o-Meaning_on (i, j) -> Integer equals :: SCM_COMP:def 8 i+j if o = [0,0], i-j if o = [0,1], i*j if o = [0,2], i div j if o = [0,3], i mod j if o = [0,4]; end; definition let s be State of SCM; let t be Terminal of SCM-AE; redefine func s.t -> Integer; end; definition let D be non empty set; let f be Function of INT, D; let x be Integer; redefine func f.x -> Element of D; end; definition let s be State of SCM; let term be bin-term; func term @ s -> Integer means :: SCM_COMP:def 9 ex f being Function of TS SCM-AE, INT st it = f.term & (for t being Terminal of SCM-AE holds f.(root-tree t) = s.t) & (for nt being NonTerminal of SCM-AE, tl, tr being bin-term, rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of INT st xl = f.tl & xr = f.tr holds f.(nt-tree (tl, tr)) = nt-Meaning_on (xl, xr)); end; theorem :: SCM_COMP:6 for s being State of SCM, t being Terminal of SCM-AE holds (root-tree t)@s = s.t; theorem :: SCM_COMP:7 for s being State of SCM, nt being NonTerminal of SCM-AE, tl, tr being bin-term holds (nt-tree(tl, tr))@s = nt-Meaning_on(tl@s, tr@s); theorem :: SCM_COMP:8 :: PRE_COMP_8: for s being State of SCM, tl, tr being bin-term holds (tl+tr)@s = (tl@s)+(tr@s) & (tl-tr)@s = (tl@s)-(tr@s) & (tl*tr)@s = (tl@s)*(tr@s) & (tl div tr)@s = (tl@s) div (tr@s) & (tl mod tr)@s = (tl@s) mod (tr@s); definition let nt be NonTerminal of SCM-AE, n be Nat; func Selfwork(nt, n) -> Element of ((the Instructions of SCM) qua set)* equals :: SCM_COMP:def 10 <*AddTo(dl.n, dl.(n+1))*> if nt = [0,0], <*SubFrom(dl.n, dl.(n+1))*> if nt = [0,1], <*MultBy(dl.n, dl.(n+1))*> if nt = [0,2], <*Divide(dl.n, dl.(n+1))*> if nt = [0,3], <*Divide(dl.n, dl.(n+1)), dl.n:=dl.(n+1)*> if nt = [0,4]; end; definition let term be bin-term, aux be Nat; func SCM-Compile(term, aux) -> FinSequence of the Instructions of SCM means :: SCM_COMP:def 11 ex f being Function of TS SCM-AE, Funcs(NAT, ((the Instructions of SCM) qua set)*) st it = (f.term qua Element of Funcs(NAT, ((the Instructions of SCM) qua set)*)).aux & (for t being Terminal of SCM-AE ex g being Function of NAT, ((the Instructions of SCM) qua set)* st g = f.(root-tree t) & for n being Nat holds g.n = <*dl.n:=@t*>) & for nt being NonTerminal of SCM-AE, t1, t2 being bin-term, rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl, rtr*> ex g, f1, f2 being Function of NAT, ((the Instructions of SCM) qua set) * st g = f.(nt-tree (t1, t2)) & f1 = f.t1 & f2 = f.t2 & for n being Nat holds g.n = (f1.n)^(f2.(n+1))^Selfwork(nt, n); end; theorem :: SCM_COMP:9 for t being Terminal of SCM-AE, n being Nat holds SCM-Compile(root-tree t, n) = <* dl.n:=@t *>; theorem :: SCM_COMP:10 for nt being NonTerminal of SCM-AE, t1, t2 being bin-term, n being Nat, rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl, rtr*> holds SCM-Compile(nt-tree(t1,t2), n) = SCM-Compile(t1, n)^SCM-Compile(t2, n+1)^Selfwork(nt, n); definition let t be Terminal of SCM-AE; func d".t -> Nat means :: SCM_COMP:def 12 dl.it = t; end; definition let term be bin-term; func max_Data-Loc_in term -> Nat means :: SCM_COMP:def 13 ex f being Function of TS SCM-AE, NAT st it = f.term & (for t being Terminal of SCM-AE holds f.(root-tree t) = d".t) & (for nt being NonTerminal of SCM-AE, tl, tr being bin-term, rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Nat st xl = f.tl & xr = f.tr holds f.(nt-tree (tl, tr)) = max(xl, xr)); end; theorem :: SCM_COMP:11 for t being Terminal of SCM-AE holds max_Data-Loc_in root-tree t = d".t; theorem :: SCM_COMP:12 for nt being NonTerminal of SCM-AE, tl, tr being bin-term holds max_Data-Loc_in(nt-tree(tl, tr)) = max(max_Data-Loc_in tl, max_Data-Loc_in tr); theorem :: SCM_COMP:13 for term being bin-term, s1, s2 being State of SCM st for dn being Nat st dn <= max_Data-Loc_in term holds s1.dl.dn = s2.dl.dn holds term @ s1 = term @ s2; theorem :: SCM_COMP:14 for term being bin-term for aux, n, k being Nat, s being State-consisting of n, n, k, SCM-Compile(term, aux), <*>INT st aux > max_Data-Loc_in term ex i being Nat, u being State of SCM st u = (Computation s).(i+1) & i+1 = len SCM-Compile(term, aux) & IC (Computation s).i = il.(n+i) & IC u = il.(n+(i+1)) & u.dl.aux = term@s & for dn being Nat st dn < aux holds s.dl.dn = u.dl.dn; theorem :: SCM_COMP:15 for term being bin-term, aux, n, k being Nat, s being State-consisting of n, n, k, SCM-Compile(term, aux)^<*halt SCM*>, <*>INT st aux > max_Data-Loc_in term holds s is halting & (Result s).dl.aux = term@s & Complexity s = len SCM-Compile(term, aux);

Back to top