|
boxes_def : THEORY
BEGIN
IMPORTING util,
structures@listn[real],
reals@product_below
Box(n:posnat) : TYPE = [#
vars_lb : listn(n),
vars_ub : listn(n)
#]
setnth_box(v:nat,f:[real->real],n:posnat)(box:Box(n)) : Box(n) = (#
vars_lb := setnth(box`vars_lb,v,f),
vars_ub := setnth(box`vars_ub,v,f)
#)
map_box(n:posnat,f:[listn(n)->listn(n)])(box:Box(n)) : Box(n) = (#
vars_lb := f(box`vars_lb),
vars_ub := f(box`vars_ub)
#)
unitbox(n:posnat) : Box(n) = (#
vars_lb := array2list(n)(zeroes),
vars_ub := array2list(n)(ones)
#)
Boxes(n:posnat) : TYPE = [#
inside,
outside,
unknown : list[Box(n)]
#]
mk_boxes(n:posnat,inside,outside,unknown:list[Box(n)]) : Boxes(n) = (#
inside := inside,
outside := outside,
unknown := unknown
#)
volume(n:posnat,box:Box(n)): real =
product[below(n)](0,n-1,LAMBDA(i:below(n)):nth(box`vars_ub,i)-nth(box`vars_lb,i))
END boxes_def
[ zur Elbe Produktseite wechseln0.2Quellennavigators
Analyse erneut starten
]
|
