[Turkmath:5137] Symbolic Computation Istanbul Meetings (SCIM)

[Zafeirakis Zafeirakopoulos]

Dear colleagues,

on Friday 24 September 2021 (tomorrow) at 17:00 we will have the first talk
(see details below) in the Symbolic Computation Istanbul Meetings (SCIM)
series.

For more information about the meetings, please visit
https://alcyon-lab.gitlab.io/lab/scim
To register for SCIM, please visit https://tinyurl.com/symbolicmeetings
The meetings take place in IMBM (http://www.imbm.org.tr), but we plan to
broadcast in zoom as well.
To receive the zoom link, for this talk and future talks, you should
register in the form above.

Students are very welcome to join SCIM.
Please let interested parties know about SCIM.

Apologies for multiple postings.

================
Speaker: Dr. Madalina Erascu (Faculty of Mathematics & Informatics, West
University of Timisoara, Romania)
Title: Using Real Quantifier Elimination for Synthesizing Optimal Numerical
Algorithms
Abstract:
Various problems in mathematics, science and engineering can be reduced to
real quantifier elimination (quantifier elimination over real closed
fields). Around 1930, Alfred Tarski showed that real quantifier elimination
can be carried out algorithmically. In 1975, George Collins provided a
dramatically more efficient algorithm. Since then, there has been intensive
research to make further improvement of efficiency for a certain important
class of formulas (inputs). In our research, we consider formulas arising
in the synthesis of optimal numerical algorithms. In this talk, we present
a case study on the square root problem: given the real number x and the
error bound eps, find a real interval such that it contains sqrt(x) and its
width is less than eps. As usual, we begin by fixing an algorithm schema,
namely, iterative refining: the algorithm starts with an initial interval
and repeatedly updates it by applying a refinement function, say R on it
until it becomes narrow enough. Then the synthesis amounts to finding a
refinement function R that ensures that the algorithm is correct (loop
invariant), terminating (contraction), and optimal. All these can be
formulated as quantifier elimination over the real numbers. Hence, in
principle, they can be all carried out automatically. However the
computational requirement is so huge, making the automatic synthesis
practically impossible with the current general quantifier elimination
software. Hence, we did some hand derivations and were able to synthesize
semi-automatically optimal algorithms under suitable assumptions.

This is joint work with Hoon Hong.
================

Sincerely,
Zafeirakis Zafeirakopoulos
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://yunus.listweb.bilkent.edu.tr/pipermail/turkmath/attachments/20210923/68135c85/attachment.html>