6 ms·

you're right, my phrasing wasn't ideal there. I'll try to clarify: what I want to do is to create a static analyser based on a set of axioms/deductions that ca

you're right, my phrasing wasn't ideal there. I'll try to clarify: what I want to do is to create a static analyser based on a set of axioms/deductions that can determine which of the "always halts/does not always halt/don't know" categories a program fits into. (I'm rephrasing the categories because a program like "(x: int) => x == 1 ? halt : loop" fits into the second category). What I'm wanting to figure out is the mathematical field in which these types of axioms reside. My naive assumption was that computability theory is the answer but in researching the various branches of similar fields it seems to me that there is a lot of crossover and similarities between concepts in different fields. So I wasn't sure if there was a field that covers what I would describe as "given a sequence of transformations of typed values, representing those transformations as relationships between inputs and an output, can we definitively prove that the program halts, or does not always halt". For example, given the function "f(x: int) => x is even ? f(x + 1) : halt" I can know from looking at it that it will halt on any valid input because for any int x, recursing on x + 1 has to reach a value where x is not even. I just don't know how I would formalise such knowledge into a system that can actually deduce such conclusions as you could clearly change "x is even" to any "x is wholly divisible by <integer>" and the conclusion would hold.

lisper 8y ago
> you could clearly change "x is even" to any "x is wholly divisible by <integer>" Or... "x is a prime number" "x is a counterexample to the Goldbach conjecture" "x is an encoding of a planar map that cannot be four-colored" "x is the encoding of an algorithm that solves the traveling salesman problem in polynomial time" "x is the encoding of a formal proof of the Riemann hypothesis"
- beaconstudios 8y ago
  For which the answer from the program is "I don't know".
  - lisper 8y ago
    Really? Even for "x is a prime number"?
    - beaconstudios 8y ago
      How would you even express that as a piece of code? I'm not talking about magic blackbox functions.
      - lisper 8y ago
        Seriously? You don't know how to write a function that tests if a number is a prime?
        beaconstudios 8y ago
        of course I do - I misspoke after I missed your reference to prime numbers in the list of open/hard problems. I get why you're including it, but if we're just deciding whether the program halts then "f(x: int) => x is prime ? halt : loop" is clearly resolvable to "doesn't always halt" so I don't see your point.
        lisper 8y ago
        > if we're just deciding whether the program halts then "f(x: int) => x is prime ? halt : loop" is clearly resolvable to "doesn't always halt" Yes, that's right. But that was not your original example. Your original example was: f(x: int) => x is even ? f(x + 1) : halt which is a much more interesting case. But the real point (as I am now repeating for the third time) is that the halting problem is equivalent to proving arbitrary theorems. "f(x: int) => x is prime ? halt : loop" is equivalent to the (very uninteresting) theorem "X is prime" for whatever X you happen to put in. Your original example is equivalent to "there are an infinite number of even numbers", which is slightly more interesting. Replace "even" with "prime" and it gets even more interesting. Replace "prime" with one of the other examples, then it gets more interesting still.
chriswarbo 8y ago
> 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 due 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/Binary/PropositionalEquality.agda 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-reflection.html 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 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!

lisper 8y ago

> you could clearly change "x is even" to any "x is wholly divisible by <integer>" Or... "x is a prime number" "x is a counterexample to the Goldbach conjecture" "x is an encoding of a planar map that cannot be four-colored" "x is the encoding of an algorithm that solves the traveling salesman problem in polynomial time" "x is the encoding of a formal proof of the Riemann hypothesis"

beaconstudios 8y ago
For which the answer from the program is "I don't know".
- lisper 8y ago
  Really? Even for "x is a prime number"?
  - beaconstudios 8y ago
    How would you even express that as a piece of code? I'm not talking about magic blackbox functions.
    - lisper 8y ago
      Seriously? You don't know how to write a function that tests if a number is a prime?
      - beaconstudios 8y ago
        of course I do - I misspoke after I missed your reference to prime numbers in the list of open/hard problems. I get why you're including it, but if we're just deciding whether the program halts then "f(x: int) => x is prime ? halt : loop" is clearly resolvable to "doesn't always halt" so I don't see your point.
        lisper 8y ago
        > if we're just deciding whether the program halts then "f(x: int) => x is prime ? halt : loop" is clearly resolvable to "doesn't always halt" Yes, that's right. But that was not your original example. Your original example was: f(x: int) => x is even ? f(x + 1) : halt which is a much more interesting case. But the real point (as I am now repeating for the third time) is that the halting problem is equivalent to proving arbitrary theorems. "f(x: int) => x is prime ? halt : loop" is equivalent to the (very uninteresting) theorem "X is prime" for whatever X you happen to put in. Your original example is equivalent to "there are an infinite number of even numbers", which is slightly more interesting. Replace "even" with "prime" and it gets even more interesting. Replace "prime" with one of the other examples, then it gets more interesting still.

chriswarbo 8y ago

> 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 due 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/Binary/PropositionalEquality.agda 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-reflection.html 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 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!