2
$\begingroup$

At this question, abstract interpretation has a nice in-depth look. However, I'd like someone to clearly and very precisely state how abstract interpretation takes the result of Rice's Theorem over the Turing-complete programming languages/Turing machines, and uses abstract interpretation to get similar results for decidability for non-trivial program properties; or, rather, how does abstract interpretation get around Rice's Theorem/the Halting Problem?

$\endgroup$
  • 2
    $\begingroup$ It's unclear what you're asking. Any abstract interpretation will be sucessful only on a subset of programs, never on all. Therefore there's no conflict with undecidability. $\endgroup$ – Mikolas Jan 18 '18 at 21:45
6
$\begingroup$

To be as clear and concise as possible, I'd try saying this

Abstract interpretation may only over-approximate properties of programs: the most precise abstract value of a program $P$ may be $a$, but any algorithm for computing an abstract value will in general compute some value $a'\geq a$ for $P$ (possibly $\top$ in the worst case).

$\endgroup$
1
$\begingroup$

This is logically redundant with the answers already given by Cody and Mikolas, but here's an intuition that might help. The property that any abstract interpretation proves about a program is guaranteed to be correct, but sometimes this is because the answer it brings back is "I don't know". That answer may be useless, but it isn't wrong. Basically, if you want a decidable version of a decision problem, you have to add this third option, so that the possible results are not "yes"/"no", but "yes"/"no"/"I give up".

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.