Comment by _a_a_a_ | Hacker News Reader

Comment by _a_a_a_ | Hacker News Reader

It's the kind of thing that might make sense if you understood it, but that's hardly going to help a newbie. I also have some real doubt whether it's actually accurate or helpful. For instance

"If an execution is represented by a curve showing the evolution of the vector x(t) of values of the input, state and output variables of the program as a function of the time t, this concrete semantics can be represented by a set of curves (with continuous time for short): x(t)"

To call these curves is just weird, and suggest this could be plotted on a two-dimensional graph is hugely misleading (And 'continuous time'???)

"The concrete semantics of a program is an "infinite" mathematical object which is not computable: it is not possible to write a program able to represent and to compute all possible executions of any program in all its possible execution environments"

Really? Let's determine if a program halts, that can't be trivial can it. Here's my program:

    HALT;

"In formal methods the abstract semantics must be chosen as a superset of the concrete semantics since otherwise reasonings in the abstract might not be correct in the concrete"

By 'superset' I think he means a subset, or more restrictive, because otherwise you could have abstract semantics that allow more behaviour than the programming language. Or maybe it doesn't, but it's so bloody unclear that even I'm getting confused.

etc.

Abstract interpretation is an interest of mine (doesn't mean I know much about it though) and I think this post is a bloody mess.

I will look at the references he's provided and also at the other links people here have posted (thanks). I hope his books are better than his blog.

(Also AFAICT from the linked coures, this is circa 2005)

> Really? Let's determine if a program halts, that can't be trivial can it.

I don’t know if you are trolling, but the halting problem is the problem of an algorithm to detemine whether any arbitrary program halts.

Curves need not be smooth, for example we may consider elliptic curves over finite fields [1] or space-filling curves [2]. In general, there are various ways to generalize the notion of curvature to discrete structures like graphs and programs [3] which reflects our intuitive understanding about local curvature on smooth manifolds. For example, one way to view discrete curvature is to grow a ball around a point and look at how quickly its volume deviates from a ball of the same radius embedded in a uniformly connected graph approximating a “flat” or Euclidean space.

[1]: https://en.wikipedia.org/wiki/Elliptic_curve#Elliptic_curves...

[2]: https://en.wikipedia.org/wiki/Space-filling_curve

[3]: https://www.maths.dur.ac.uk/users/norbert.peyerimhoff/peyeri...

This article is by one of the two inventors of abstract interpretation. Maybe you didn't find it helpful but it is definitely accurate.

I decided to do some more reading on the site that agumonkey provided. In particular this link, also by Patrick Cousot:

https://www.di.ens.fr/~cousot/publications.www/Cousot-LNCS20... [pdf] - Abstract Interpretation Based Formal Methods and Future Challenges, 2000

> All abstractions considered in this paper are “from above” so that the abstract semantics describes a superset or logical consequence of the concrete semantics. Abstractions “from below” are dual and consider a subset of the concrete semantics. An example of approximation “from below” is provided by debugging techniques which consider a subset of the possible program executions or by existential checking where one wants to prove the existence of an execution trace prefix fulfilling some given specification. In order to avoid repeating two times dual concepts and as we do usually, we only consider approximations “from above”, knowing that approximations “from below” can be easily derived by applying the duality principle (as found e.g. in lattice theory).

This is where he's getting the "superset" part. The abstraction describes many possible concrete implementations and so is a superset of all of them. Finding a particular concrete implementation or following a particular trace of a particular concrete implementation in a particular environment would be finding a subset (or particular element) of the set.

Relatedly, consider the idea of an "abstract data type" like a stack. We can describe a stack's abstract behavior (last in/first out collection with push/pop/peek operations) without describing any particular concrete details or environments. That abstract description is applicable to all stack implementations, though when we get to concrete implementations they may have further restrictions (an array-based stack has a maximum stack depth set at the start if we don't allow reallocation, a linked-list based stack has a size limit as well but it's limited by system memory instead of an initial fixed number, etc.).

This ADT of a stack is describing a superset of all concrete implementations in that it is describing something common to all of them. If it were a subset of all concrete implementations then it would only describe the behavior of some concrete implementations of a stack, which means we would have concrete implementations which are not compliant with our abstract notion of stack. That would be odd. In OO or type terms this is a superclass or supertype of all concrete stack implementations, and the actual concrete implementations are subclasses or subtypes of the stack ADT. Subclasses/subtypes are subsets of the superclass or supertype.

EDIT: Stacks are last in/first out. Needed coffee to catch that mistake.

Reply on news.ycombinator.com