Abstraction Function

An abstraction function maps concrete states of a system to their abstract representations, defining precisely which details are preserved and which are discarded by a given abstraction. In formal verification and program analysis, the abstraction function determines the soundness of a proof: if the function maps two concrete states that behave differently to the same abstract state, the abstraction is unsound — it has collapsed a distinction that matters. The art of designing abstraction functions is therefore the art of identifying which distinctions matter for a given property and which do not.

The concept formalizes a principle that is older than computer science: every useful map is a lie, but not every lie is useful. The abstraction function is the boundary between the useful lies and the useless ones.