Quelle bernstein_minmax.pvs Sprache: PVS

bernstein_minmax : THEORY
BEGIN

  IMPORTING vardirselector,
     structures@for_iterate,
            multi_bernstein,
     minmax

  bspoly,
  bspolz      : VAR MultiBernstein
  bsdegmono   : VAR DegreeMono
  nvars,terms : VAR posnat
  cf          : VAR Coeff
  f           : VAR CoeffMono
  intendpts   : VAR IntervalEndpoints
  depth,v     : VAR nat
  e           : VAR posreal
  a,b         : VAR real
  rf       : VAR [real->real]
  l           : VAR list[real]
  ep          : VAR bool
  varselect   : VAR VarSelector
  omm,
  omm1,omm2   : VAR Outminmax

  unit_box_lb?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm): bool =
    cons?(omm`lb_var) IMPLIES
      (length(omm`lb_var) = nvars AND
       LET lb_varlam  = list2array(0)(omm`lb_var) IN
         (FORALL (iup:below(nvars)):
    interval_between?(0,1,intendpts(iup),(true,true))(lb_varlam(iup)))
    AND
           multibs_eval(bspoly,bsdegmono,cf,nvars,terms)(lb_varlam) = omm`lb_max)

  unit_box_lb_id : LEMMA
    (FORALL(t:below(terms),v:below(nvars),i:upto(bsdegmono(v))):
       bspoly(t)(v)(i) = bspolz(t)(v)(i)) IMPLIES
    unit_box_lb?(bspoly,bsdegmono,nvars,terms,cf,intendpts) =
    unit_box_lb?(bspolz,bsdegmono,nvars,terms,cf,intendpts)

  unit_box_ub?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm): bool =
    cons?(omm`ub_var) IMPLIES
      (length(omm`ub_var) = nvars AND
      LET ub_varlam  = list2array(0)(omm`ub_var) IN
         (FORALL (iup:below(nvars)):
    interval_between?(0,1,intendpts(iup),(true,true))(ub_varlam(iup))) AND
           multibs_eval(bspoly,bsdegmono,cf,nvars,terms)(ub_varlam) = omm`ub_min)

  unit_box_ub_id : LEMMA
    (FORALL(t:below(terms),v:below(nvars),i:upto(bsdegmono(v))):
       bspoly(t)(v)(i) = bspolz(t)(v)(i)) IMPLIES
    unit_box_ub?(bspoly,bsdegmono,nvars,terms,cf,intendpts) =
    unit_box_ub?(bspolz,bsdegmono,nvars,terms,cf,intendpts)

  sound?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm) : bool =
    forall_X_between(omm`lb_min,omm`ub_max)(bspoly,bsdegmono,cf,nvars,terms) AND
    unit_box_lb?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm) AND
    unit_box_ub?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm) AND
    length_eq?(nvars)(omm)

  sound_id : LEMMA
    (FORALL(t:below(terms),v:below(nvars),i:upto(bsdegmono(v))):
       bspoly(t)(v)(i) = bspolz(t)(v)(i)) IMPLIES
    sound?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm) =
    sound?(bspolz,bsdegmono,nvars,terms,cf,intendpts)(omm)

  sound_lb_le_ub: LEMMA
    sound?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm)
    IMPLIES
    lb_le_ub?(omm)

  combine_sound: LEMMA
    (EXISTS (VPr:[Vars->bool]): FORALL (X:(unitbox?(nvars))): (VPr(X)
    IMPLIES eval_X_between(omm1`lb_min,omm1`ub_max)(bspoly,bsdegmono,cf,nvars,terms)(X))
    AND ((NOT VPr(X))
    IMPLIES eval_X_between(omm2`lb_min,omm2`ub_max)(bspoly,bsdegmono,cf,nvars,terms)(X)))
    AND
    unit_box_lb?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm1) AND
    unit_box_ub?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm1) AND
    unit_box_lb?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm2) AND
    unit_box_ub?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm2) AND
    length_eq?(nvars)(omm1) AND length_eq?(nvars)(omm2)
    IMPLIES
    sound?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(combine(omm1,omm2))

  Bern_coeffs_minmax_rec(bspoly,bsdegmono,cf,nvars,terms,f,
                         depth,intendpts,v,
    (ep:(edge_point?(bsdegmono,nvars,f,intendpts,v)))):
    RECURSIVE {omm:Outminmax |
      (FORALL (nf:CoeffMono): (FORALL (i:below(nvars)): nf(i)<=bsdegmono(i) AND
                                      (v <= i IMPLIES f(i)=nf(i)))
                     IMPLIES
         omm`lb_min <= multibscoeff(bspoly,bsdegmono,cf,nvars,terms)(nf)  AND
                              multibscoeff(bspoly,bsdegmono,cf,nvars,terms)(nf) <= omm`ub_max) AND
      unit_box_lb?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm) AND
      unit_box_ub?(bspoly,bsdegmono,nvars,terms,cf,intendpts)(omm) AND
      length_eq?(nvars)(omm) AND
      omm`max_depth = depth} =
    IF v = 0 THEN
      LET coefffun      = multibscoeff(bspoly,bsdegmono,cf,nvars,terms),
          thiscoeff     = coefffun(f),
     thisvar       = IF ep THEN corner_to_point(f,nvars) ELSE null ENDIF,
          thisachval    = IF ep THEN thiscoeff ELSE 0 ENDIF IN
        single_outminmax(thiscoeff,thisachval,thisvar,depth)
    ELSE
      LET iepts = intendpts(v-1) IN
        iterate_left(0,bsdegmono(v-1),
         LAMBDA(d:upto(bsdegmono(v-1))):
           LET nf    = f WITH [(v-1) := d],
               nep   = ep AND (d=0 AND iepts`1 OR
                               bsdegmono(v-1)/=0 AND
                               d=bsdegmono(v-1) AND iepts`2) IN
           Bern_coeffs_minmax_rec(bspoly,bsdegmono,cf,nvars,terms,nf,depth,intendpts,v-1,nep),
         combine)
    ENDIF
    MEASURE v

  Bern_coeffs_minmax(bspoly,bsdegmono,cf,nvars,terms,depth,intendpts) :
    (sound?(bspoly,bsdegmono,nvars,terms,cf,intendpts)) =
    Bern_coeffs_minmax_rec(bspoly,bsdegmono,cf,nvars,terms,zeroes,depth,intendpts,nvars,true)

  Bern_coeffs_minmax_length: LEMMA
    LET omm = Bern_coeffs_minmax(bspoly,bsdegmono,cf,nvars,terms,depth,intendpts) IN
    length_eq?(nvars)(omm)

  Bern_coeffs_minmax_maxdepth: LEMMA
    LET omm = Bern_coeffs_minmax(bspoly,bsdegmono,cf,nvars,terms,depth,intendpts) IN
    omm`max_depth = depth

  Bern_coeffs_minmax_var: LEMMA
   LET omm = Bern_coeffs_minmax(bspoly,bsdegmono,cf,nvars,terms,depth,intendpts),
       bseval = multibs_eval(bspoly, bsdegmono, cf, nvars, terms)
   IN
     (cons?(omm`lb_var) OR cons?(omm`ub_var)) IMPLIES
       bseval(list2array(0)(omm`lb_var)) = omm`lb_max AND
       bseval(list2array(0)(omm`ub_var)) = omm`ub_min

  localexit  : VAR [Outminmax -> bool]

  globalexit : VAR [Outminmax->bool]

  %%%% BEGIN 3M: used to close TCC obligations
  list2array_sound_pi : LEMMA
    FORALL(l:list[real],t:real) :
      list2array(t)(l) = LAMBDA(i: nat):
        IF i < length(l) THEN nth(l,i)
        ELSE t
      ENDIF
  %%%% END 3M

  Bernstein_minmax_rec(bspoly,bsdegmono,nvars,terms,cf,depth,(level:upto(depth)),
                       localexit,globalexit,intendpts,varselect,omm) :
    RECURSIVE (sound?(bspoly,bsdegmono,nvars,terms,cf,intendpts)) =
    LET bp     = translist(polylist(bspoly,bsdegmono,nvars,terms)),
        minmax = Bern_coeffs_minmax(bp,bsdegmono,cf,nvars,terms,level,intendpts)
    IN
      IF level = depth OR localexit(minmax) OR between?(omm,minmax) OR globalexit(minmax) THEN
        minmax
      ELSE
        LET
   varsel       = varselect(bp,bsdegmono,nvars,terms,cf,level),
          v            = mod(varsel`2,nvars),
   spleft       = Bern_split_left_mpoly(bp,bsdegmono)(mod(varsel`2,nvars)),
   spright      = Bern_split_right_mpoly(bp,bsdegmono)(mod(varsel`2,nvars)),
   ipleft       = intendpts WITH [(v)`2 := true],
   ipright      = intendpts WITH [(v)`1 := true],
   (LR1,LR2)    = IF varsel`1 THEN (spleft,spright) ELSE (spright,spleft) ENDIF,
   LR1intendpts = IF varsel`1 THEN ipleft ELSE ipright ENDIF,
   LR2intendpts = IF varsel`1 THEN ipright ELSE ipleft ENDIF,
   combine_this = IF varsel`1 THEN combine_l ELSE combine_r ENDIF,
   newmm1       = combine(omm,minmax),
          level        = level + 1,
          bslr1        = Bernstein_minmax_rec(LR1,bsdegmono,nvars,terms,cf,depth,level,
                                              localexit,globalexit,LR1intendpts,varselect,newmm1)
IN
          IF globalexit(bslr1) THEN
            combine_this(v,bslr1,minmax)
          ELSE
            LET
       newmm2   = combine(newmm1,bslr1),
              bslr2    = Bernstein_minmax_rec(LR2,bsdegmono,nvars,terms,cf,depth,level,
                                              localexit,globalexit,LR2intendpts,varselect,newmm2),
       bslrleft = IF varsel`1 THEN bslr1 ELSE bslr2 ENDIF,
       bslrright = IF varsel`1 THEN bslr2 ELSE bslr1 ENDIF
            IN
              combine_lr(v,bslrleft,bslrright)
   ENDIF
      ENDIF
      MEASURE depth-level

  Bernstein_minmax(bspoly,bsdegmono,nvars,terms,cf,depth,localexit,globalexit,
                   intendpts,varselect) : (sound?(bspoly,bsdegmono,nvars,terms,cf,intendpts)) =
    Bernstein_minmax_rec(bspoly,bsdegmono,nvars,terms,cf,depth,0,
                         localexit,globalexit,intendpts,varselect,empty_minmax)

END bernstein_minmax

quality85%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.