4 ms·

> 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

> 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!

beaconstudios 8y ago
a dependent typing engine is exactly how I was thinking of representing this - i.e "x: int => x + 1" would have a type signature of "x: int => x + 1". Further compositions would stack. If I e.g. converted the Collatz conjecture to a function I would get the following signatures: - collatz(x: 1) => halt - collatz(x: int where x > 0 && x % 2 = 0) => collatz(x / 2) - collatz(x: int where x > 0 && x % 2 = 1) => collatz(x * 3 + 1) I figure that if I extract out recursion like this (as recursion seems to be the only thing that makes a computation potentially undecidable) and bubble the branching up to the signature as a form of pattern matching, then the signature becomes something you could potentially use to figure out if it is decidable. The issue I'm stuck on is what approach to take to build a deduction system for calculating whether continuing such a sequence from any value in the allowed input space would halt - obviously at this point in time the collatz conjecture is an open question but we can also construct functions using the same notation that we can intuitively determine will either always halt or only sometimes halt, so there is surely room for the existence of such a deductive system. I just don't want to spend a year learning about e.g. category theory or natural deductive logic just to find out that this problem cannot be effectively expressed in such a system.
- chriswarbo 8y ago
  A dependently typed system (or presumably anything else) which allows non-halting definitions is unsound. The classic example is an infinite loop: loop = loop What is the type of `loop`? We can infer it by starting with a completely generic type variable, e.g. `forall t. t`: loop : forall t. t loop = loop Then we can look at the type of the body to see which constraints it must satisfy, and perform unification with that and the `t` we have so far. In this case the body is `loop` which has type `forall t. t` (i.e. which is completely unconstrained). Unifying `forall t. t` with `forall t. t` gives (unsurprisingly) `forall t. t`. Hence that is the type of `loop`. Yet this claims to hold for all types `t`, which must include empty types like `Empty`, which should have no values! data Empty where -- This page intentionally left blank loop : forall t. t loop = loop myEmptyValue : Empty myEmptyValue = loop In particular, this lets us "prove" (in an invalid way) things like the Collatz conjecture. Here's a quick definition of the Collatz sequence, in Agda/Idris notation (untested): -- Peano arithmetic data Natural where Zero : Natural Succ : Natural -> Natural one = Succ Zero halve : Natural -> Natural halve Zero = Zero halve (Succ Zero) = Succ Zero -- Should never reach this; included for completeness halve (Succ (Succ n)) = Succ (halve n) threeTimes : Natural -> Natural threeTimes Zero = Zero threeTimes (Succ n) = Succ (Succ (Succ (threeTimes n))) data Boolean where True : Boolean False : Boolean not : Boolean -> Boolean not True = False not False = True ifThenElseNat : Boolean -> Natural -> Natural -> Natural ifThenElseNat True x y = x ifThenElseNat False x y = y isEven : Natural -> Boolean isEven Zero = True isEven (Succ n) = not (isEven n) collatzStep : Natural -> Natural collatzStep Zero = one -- Again, only for completeness collatzStep (Succ n) = ifThenElseNat (isEven (Succ n)) (halve (Succ n)) (Succ (threeTimes (Succ n))) -- This won't be allowed by Agda/Idris since it may or may not halt ;) collatzLoop : Natual -> Natural collatzLoop Zero = collatzLoop (collatzStep Zero) -- For completeness collatzLoop (Succ Zero) = Succ Zero -- Halt collatzLoop (Succ (Succ n)) = collatzLoop (collatzStep (Succ (Succ n))) We can then define the Collatz conjecture, using a standard encoding of equality: data Equal : Natural -> Natural -> Type where reflexivity : (n : Natural) -> Equal n n CollatzConjecture : Type CollatzConjecture = (n : Natural) -> Equal (collatzLoop n) one proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = ? disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture purportedProof = ? The disproof basicallys says "if you give me a proof of `CollatzConjecture`, I can give you a value which doesn't exist"; since that's absurd, the only way it can hold is if there are no proofs of `CollatzConjecture` to give it (this is a form of proof by contradiction: give me a supposed proof, and I'll show you why it must be wrong). The problem with allowing non-terminating recursion is that we can use `loop` to fill in either of these proofs, or even both of them! proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = loop disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture purportedProof = loop The type of `loop` is `forall t. t`, which can unify with either of these types, so the language/logic will allow us to use it in these definitions (or anywhere else, for that matter). For this reason, we have to make sure our language isn't Turing-complete, which we can do using a "totality checker" (a static analyser which checks if our definitions halt: if they definitely do, they're permitted; if they don't or we can't tell, they're forbidden). That stops us from writing things like `loop`, but unfortunately it stops us from writing `collatzLoop` as well. One way to get around this is to use "corecursion". This lets an infinite loop pass the totality checker, as long as it's definitely producing output data as it goes (e.g. like a stream which is forbidden from getting "stuck"). We can use this to make a `Delayed` type, which is just a stream of dummy data which might or might not end (a polymorphic version of this is described in more detail at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html ): data Delayed : Type where Now : Natural -> Delayed Later : Delayed -> Delayed collatzLoop : Natural -> Delayed collatzLoop Zero = Later (collatzLoop (collatzStep Zero)) -- For completeness collatzLoop (Succ Zero) = Now (Succ Zero) -- Halt collatzLoop (Succ (Succ n)) = Later (collatzLoop (collatzStep (Succ (Succ n)))) This will pass the totality checker since each step is guaranteed to produce some data (either the `Now` symbol or the `Later` symbol); even though the contents of a `Later` value may be infinite! If we run this version of `collatzLoop` on, say, 6 (ignoring the `Zero`/`Succ` notation for brevity), we get: collatzLoop 6 Later (collatzLoop 3) Later (Later (collatzLoop 10)) Later (Later (Later (collatzLoop 5))) Later (Later (Later (Later (collatzLoop 16)))) Later (Later (Later (Later (Later (collatzLoop 8))))) Later (Later (Later (Later (Later (Later (collatzLoop 4)))))) Later (Later (Later (Later (Later (Later (Later (collatzLoop 2))))))) Later (Later (Later (Later (Later (Later (Later (Later (collatzLoop 1)))))))) Later (Later (Later (Later (Later (Later (Later (Later (Now 1)))))))) We can rephrase the Collatz conjecture as saying that the return value of `collatzLoop` will always, eventually, end with `Now one`. This is an existence proof: there exists an `n : Natural` such that after `n` layers of `Later` wrappers there will be a `Now one` value. Since we're dealing with constructive logic, to prove this existence we must construct the number `n` (e.g. using some function, which I'll call `boundFinder`): unwrap : Natural -> Delayed -> Delayed wrap Zero x = x wrap (Succ n) (Now y) = Now y wrap (Succ n) (Later y) = unwrap n y data DelayEqual : Delayed -> Delayed -> Type where delayedReflexivity : (d : Delayed) -> DelayEqual d d -- The notation `(x : y *** z)` is a dependent pair, where the first element has -- type `y` and the second element has type `z` which may refer to the first -- value as `x` CollatzConjecture : Type CollatzConjecture = (boundFinder : Natural -> Natural *** (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = ? disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture (boundFinder, purportedProof) = ? With this definition, a value of type `CollatzConjecture` will be a proof of the Collatz conjecture. Since we can't use tricks like `loop`, we're forced to actually construct a value of the required type. This value will be a pair: the first element of the pair is a function of type `Natural -> Natural`, which we call `boundFinder`. The second element of the pair is also a function, but it has type: (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) This says that given any `n : Natural`, we can return a proof that: DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) This says that `unwrap (boundFinder n) (collatzLoop n)`, i.e. removing `boundFinder n` layers of `Later` wrappers from `collatzLoop n`, is equal to the value `Now one`. To disprove this form of the Collatz conjecture, we're given a supposed proof: i.e. we're given some `boundFinder` function and a value supposedly proving the equation described above. We need to find a contradiction to that supposed proof, which might be an `n : Natural` which reduces to `Now x` where `x` is not 1; or which we can show doesn't reduce at all. Either way this would contradict the claim made by `purportedProof`, and we could use that contradiction to prove anything ("ex falso quodlibet") including the `Empty` return value we need (just as if we had `loop`!). The thing is, even if we set up all of this machinery, there is an unfortunate fact staring us in the face: compare the definition of `Natural` to the definition of `Delayed`. They're almost identical! The only difference is that `Now` takes an argument but `Zero` doesn't. If we think about what `Succ` is doing, it's just adding a wrapper around a `Natural` to represent "one more than" (e.g. `Succ Zero` is 1, `Succ (Succ Zero)` is 2, etc.). If we think about what `Later` is doing, it's just adding a wrapper around a `Delayed` to represent "one more step". In essence we've just traded one form of counting for another! It doesn't actually get us any closer to solving the Collatz conjecture, other than giving us something to plug a proof attempt into, such that it will be verified automatically. It's like setting up a Wordpress blog: it lets us say anything we like to the world, but doesn't help us figure what we want to say ;)

beaconstudios 8y ago

a dependent typing engine is exactly how I was thinking of representing this - i.e "x: int => x + 1" would have a type signature of "x: int => x + 1". Further compositions would stack. If I e.g. converted the Collatz conjecture to a function I would get the following signatures: - collatz(x: 1) => halt - collatz(x: int where x > 0 && x % 2 = 0) => collatz(x / 2) - collatz(x: int where x > 0 && x % 2 = 1) => collatz(x * 3 + 1) I figure that if I extract out recursion like this (as recursion seems to be the only thing that makes a computation potentially undecidable) and bubble the branching up to the signature as a form of pattern matching, then the signature becomes something you could potentially use to figure out if it is decidable. The issue I'm stuck on is what approach to take to build a deduction system for calculating whether continuing such a sequence from any value in the allowed input space would halt - obviously at this point in time the collatz conjecture is an open question but we can also construct functions using the same notation that we can intuitively determine will either always halt or only sometimes halt, so there is surely room for the existence of such a deductive system. I just don't want to spend a year learning about e.g. category theory or natural deductive logic just to find out that this problem cannot be effectively expressed in such a system.

chriswarbo 8y ago
A dependently typed system (or presumably anything else) which allows non-halting definitions is unsound. The classic example is an infinite loop: loop = loop What is the type of `loop`? We can infer it by starting with a completely generic type variable, e.g. `forall t. t`: loop : forall t. t loop = loop Then we can look at the type of the body to see which constraints it must satisfy, and perform unification with that and the `t` we have so far. In this case the body is `loop` which has type `forall t. t` (i.e. which is completely unconstrained). Unifying `forall t. t` with `forall t. t` gives (unsurprisingly) `forall t. t`. Hence that is the type of `loop`. Yet this claims to hold for all types `t`, which must include empty types like `Empty`, which should have no values! data Empty where -- This page intentionally left blank loop : forall t. t loop = loop myEmptyValue : Empty myEmptyValue = loop In particular, this lets us "prove" (in an invalid way) things like the Collatz conjecture. Here's a quick definition of the Collatz sequence, in Agda/Idris notation (untested): -- Peano arithmetic data Natural where Zero : Natural Succ : Natural -> Natural one = Succ Zero halve : Natural -> Natural halve Zero = Zero halve (Succ Zero) = Succ Zero -- Should never reach this; included for completeness halve (Succ (Succ n)) = Succ (halve n) threeTimes : Natural -> Natural threeTimes Zero = Zero threeTimes (Succ n) = Succ (Succ (Succ (threeTimes n))) data Boolean where True : Boolean False : Boolean not : Boolean -> Boolean not True = False not False = True ifThenElseNat : Boolean -> Natural -> Natural -> Natural ifThenElseNat True x y = x ifThenElseNat False x y = y isEven : Natural -> Boolean isEven Zero = True isEven (Succ n) = not (isEven n) collatzStep : Natural -> Natural collatzStep Zero = one -- Again, only for completeness collatzStep (Succ n) = ifThenElseNat (isEven (Succ n)) (halve (Succ n)) (Succ (threeTimes (Succ n))) -- This won't be allowed by Agda/Idris since it may or may not halt ;) collatzLoop : Natual -> Natural collatzLoop Zero = collatzLoop (collatzStep Zero) -- For completeness collatzLoop (Succ Zero) = Succ Zero -- Halt collatzLoop (Succ (Succ n)) = collatzLoop (collatzStep (Succ (Succ n))) We can then define the Collatz conjecture, using a standard encoding of equality: data Equal : Natural -> Natural -> Type where reflexivity : (n : Natural) -> Equal n n CollatzConjecture : Type CollatzConjecture = (n : Natural) -> Equal (collatzLoop n) one proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = ? disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture purportedProof = ? The disproof basicallys says "if you give me a proof of `CollatzConjecture`, I can give you a value which doesn't exist"; since that's absurd, the only way it can hold is if there are no proofs of `CollatzConjecture` to give it (this is a form of proof by contradiction: give me a supposed proof, and I'll show you why it must be wrong). The problem with allowing non-terminating recursion is that we can use `loop` to fill in either of these proofs, or even both of them! proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = loop disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture purportedProof = loop The type of `loop` is `forall t. t`, which can unify with either of these types, so the language/logic will allow us to use it in these definitions (or anywhere else, for that matter). For this reason, we have to make sure our language isn't Turing-complete, which we can do using a "totality checker" (a static analyser which checks if our definitions halt: if they definitely do, they're permitted; if they don't or we can't tell, they're forbidden). That stops us from writing things like `loop`, but unfortunately it stops us from writing `collatzLoop` as well. One way to get around this is to use "corecursion". This lets an infinite loop pass the totality checker, as long as it's definitely producing output data as it goes (e.g. like a stream which is forbidden from getting "stuck"). We can use this to make a `Delayed` type, which is just a stream of dummy data which might or might not end (a polymorphic version of this is described in more detail at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html ): data Delayed : Type where Now : Natural -> Delayed Later : Delayed -> Delayed collatzLoop : Natural -> Delayed collatzLoop Zero = Later (collatzLoop (collatzStep Zero)) -- For completeness collatzLoop (Succ Zero) = Now (Succ Zero) -- Halt collatzLoop (Succ (Succ n)) = Later (collatzLoop (collatzStep (Succ (Succ n)))) This will pass the totality checker since each step is guaranteed to produce some data (either the `Now` symbol or the `Later` symbol); even though the contents of a `Later` value may be infinite! If we run this version of `collatzLoop` on, say, 6 (ignoring the `Zero`/`Succ` notation for brevity), we get: collatzLoop 6 Later (collatzLoop 3) Later (Later (collatzLoop 10)) Later (Later (Later (collatzLoop 5))) Later (Later (Later (Later (collatzLoop 16)))) Later (Later (Later (Later (Later (collatzLoop 8))))) Later (Later (Later (Later (Later (Later (collatzLoop 4)))))) Later (Later (Later (Later (Later (Later (Later (collatzLoop 2))))))) Later (Later (Later (Later (Later (Later (Later (Later (collatzLoop 1)))))))) Later (Later (Later (Later (Later (Later (Later (Later (Now 1)))))))) We can rephrase the Collatz conjecture as saying that the return value of `collatzLoop` will always, eventually, end with `Now one`. This is an existence proof: there exists an `n : Natural` such that after `n` layers of `Later` wrappers there will be a `Now one` value. Since we're dealing with constructive logic, to prove this existence we must construct the number `n` (e.g. using some function, which I'll call `boundFinder`): unwrap : Natural -> Delayed -> Delayed wrap Zero x = x wrap (Succ n) (Now y) = Now y wrap (Succ n) (Later y) = unwrap n y data DelayEqual : Delayed -> Delayed -> Type where delayedReflexivity : (d : Delayed) -> DelayEqual d d -- The notation `(x : y *** z)` is a dependent pair, where the first element has -- type `y` and the second element has type `z` which may refer to the first -- value as `x` CollatzConjecture : Type CollatzConjecture = (boundFinder : Natural -> Natural *** (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = ? disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture (boundFinder, purportedProof) = ? With this definition, a value of type `CollatzConjecture` will be a proof of the Collatz conjecture. Since we can't use tricks like `loop`, we're forced to actually construct a value of the required type. This value will be a pair: the first element of the pair is a function of type `Natural -> Natural`, which we call `boundFinder`. The second element of the pair is also a function, but it has type: (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) This says that given any `n : Natural`, we can return a proof that: DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) This says that `unwrap (boundFinder n) (collatzLoop n)`, i.e. removing `boundFinder n` layers of `Later` wrappers from `collatzLoop n`, is equal to the value `Now one`. To disprove this form of the Collatz conjecture, we're given a supposed proof: i.e. we're given some `boundFinder` function and a value supposedly proving the equation described above. We need to find a contradiction to that supposed proof, which might be an `n : Natural` which reduces to `Now x` where `x` is not 1; or which we can show doesn't reduce at all. Either way this would contradict the claim made by `purportedProof`, and we could use that contradiction to prove anything ("ex falso quodlibet") including the `Empty` return value we need (just as if we had `loop`!). The thing is, even if we set up all of this machinery, there is an unfortunate fact staring us in the face: compare the definition of `Natural` to the definition of `Delayed`. They're almost identical! The only difference is that `Now` takes an argument but `Zero` doesn't. If we think about what `Succ` is doing, it's just adding a wrapper around a `Natural` to represent "one more than" (e.g. `Succ Zero` is 1, `Succ (Succ Zero)` is 2, etc.). If we think about what `Later` is doing, it's just adding a wrapper around a `Delayed` to represent "one more step". In essence we've just traded one form of counting for another! It doesn't actually get us any closer to solving the Collatz conjecture, other than giving us something to plug a proof attempt into, such that it will be verified automatically. It's like setting up a Wordpress blog: it lets us say anything we like to the world, but doesn't help us figure what we want to say ;)