BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
hes
SUMMARY:Semi-automatic Algorithm Synthesis (Case Study: Sq
uare Root) - Madalina Erascu - Research Institute
for Symbolic Computation\, Johannes Kepler Univers
ity\, Linz\, Austria
DTSTART;TZID=Europe/London:20120621T130000
DTEND;TZID=Europe/London:20120621T140000
UID:TALK38374AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/38374
DESCRIPTION:We report a case study on semi-automatic synthesis
of optimal algorithms for square root problem: gi
ven the real number x and the error bound e\, find
the real interval such that it contains the radic
al of x and its width is less than e. As usual\, w
e begin by fixing an algorithm schema\, namely\, i
terative refining: the algorithm starts with an in
itial interval and repeatedly updates it by applyi
ng a refinement function\, say f\, on it until it
becomes narrow enough. Then the synthesis amounts
to finding a refinement function f that ensures th
at the algorithm is correct (loop invariant)\, ter
minating (contraction)\, and optimal. All these ca
n be formulated as quantifier elimination over the
real numbers. Hence\, in principle\, they can be
all carried out automatically. However the computa
tional requirement is so huge\, making the automat
ic synthesis practically impossible with the curre
nt general quantifier elimination software. Hence\
, we did some hand derivations and were able to sy
nthesize semi-automatically an optimal algorithm u
nder suitable assumptions. We hope that the ideas
behind the hand derivations could be eventually tu
rned into an algorithm. Then we would have an auto
matic synthesis of optimal square-root algorithm.
This is joint work with Hoon Hong.
LOCATION:Computer Laboratory\, William Gates Building\, Roo
m SS03
CONTACT:William Denman
END:VEVENT
END:VCALENDAR