CHchriswarbo·Jul 5, 2018
> you could clearly change "x is even" to any "x is wholly divisible by <integer>"
The tricky thing is that it's not clear, since it depends entirely upon the formal system you're using!
As a simple example, let's say I have the following Java program:
if (2 < 3) { return "halt"; }
else { while (true) {}; return "never halts"; }
This program will halt, but what if we change it? We "could clearly change" the `3` to a `1` and the resulting program would not halt. What if we changed the `3` to `"hello world"`? The result would neither halt nor not-halt, since it wouldn't even be a valid Java program in the first place, due to a type mismatch. Hence it may not at all be clear whether it's valid to swap out parts of a statement or not, let alone whether that will/won't change some property of the statement.
That Java example failed du
Read the rest
e to type checking, but static analysis is very similar to type checking/inference, in the sense that it's calculating properties of code (or logical statements; they're equivalent via Curry-Howard) based entirely on the syntax. In this sense, we can think of any static analysis algorithm as being a (potentially very complicated and confusing) type system.
It's easy to see from the syntax above that the `2` and `"hello world"` have different types, and hence that this isn't valid code. When we start getting more powerful or complicated type systems, like dependent types, Goedel numbering, or some static analysis algorithm, then it can be arbitrarily difficult to figure out whether a particular arrangement of symbols is actually a valid statement or not.
This might seem petty, but consider your `is even` example, written in some dependently typed programming language (i.e. a powerful static analyser). We might say (in Agda, Idris, etc.):
halt : String
halt = "hello world"
f : Int -> String
f x = if isEven x then f (x + 1) else halt
Most type systems are "conservative", meaning that they treat "dunno" as failure. Since most dependently typed languages aren't smart enough to figure out that this halts, we would have to rewrite the program in a way that provides evidence that it halts. This can get very messy very quickly (e.g. see https://github.com/agda/agda-stdlib/blob/master/src/Relation... ). So the resulting program will be a massive pile of symbols, all carefully orchestrated such that the type checker is happy with the result.
In that situation, it is certainly not clear whether we can just replace one expression with another, even if they're the same type (e.g. replacing one integer with another), since that might break some of the surrounding proofs.
If we think of a static analyser as a complicated type inference algorithm, which can sometimes infer such proofs and coercions, then we can think of your example as being the 'tip of the iceberg', which the static analyser can "elaborate" into a much more complicated form (this is exactly how Idris works http://docs.idris-lang.org/en/latest/reference/elaborator-re... and "tactics" in Coq are similar https://coq.inria.fr/refman/proof-engine/ltac.html ).
It is this explosion of symbols which makes it difficult to talk about formal systems by using informal statements (like your example). It can be very difficult to even figure out how to represent an informal statement in a formal way, but it's only then that we can ask specific questions about algorithms (e.g. what can or can't be deduced). Often, the answers to such questions turn out to be trivial properties of the formalisation; but it may take many decades to actually come up with that formalisation!