<p>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".</p>

CC BY-SA 3.0
2018-01-19T05:24:40.640Z
2018-01-19T05:24:40.640Z
John Lasseter
<p>To be as clear and concise as possible, I'd try saying this</p>

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

CC BY-SA 3.0
2018-01-18T22:20:32.490Z
2018-01-18T22:20:32.490Z
cody
<p>At <a href="https://cstheory.stackexchange.com/questions/19538/what-is-the-goal-behind-abstract-interpretation-in-programming-languages">this question</a>, 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?</p>

CC BY-SA 3.0
2018-01-18T21:45:05.873Z
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.
Mikolas
<pl.programming-languages><decidability>
How can you state how abstract interpretation gets around Rice's Theorem succinctly?
CinchBlue
# How can you state how abstract interpretation gets around Rice's Theorem succinctly?

(Asked by: username_0 on 2018-01-18)

At [this question](https://cstheory.stackexchange.com/questions/19538/what-is-the-goal-behind-abstract-interpretation-in-programming-languages), 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?

**Tags:** pl.programming-languages, decidability
> **Comments:**
> **username_1**: 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.  

---

## 2 answers

### Answer by username_3 on 2018-01-18. Score: 7 | Accepted answer

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).


---

### Answer by username_2 on 2018-01-19. Score: 1

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".


---

