I'm not familiar with directly, but if you're more familiar with comp-sci: based on my understanding of Curry-Howard correspondence, I would think it's the logic equivalent of the halting problem. I could be way off-base though, I'd appreciate a mathematician chiming in on whether my intuition is accurate here.
(Caveat: I'm a computer scientist, not a mathematician)
The halting problem, and universal computation itself, came directly out of work on incompleteness. Incompleteness is about being unable to prove statements in a particular system; it leaves open the possibility that a more powerful system might be able to prove that statement (but that more powerful system will have its own incompleteness, and so on).
Turing got involved after attending a series of lectures on Goedel's incompeteness theorem. He came up with turing machines, showed that they cannot decide their own halting problem, and proved that they're equivalent to lambda calculus. Goedel tried to make a more powerful alternative to lambda calculus, called general recursive functions, but it also turned out to be equivalent to turing machines and lambda calculus.
This lead to the Church-Turing thesis, which claims that any effective/physical/realisable system of logic cannot be more powerful than turing machines/lambda calculus/general recursive functions. In this sense, we can still "solve" the halting problem by using a more powerful logical system (e.g. oracle machines), but the Church Turing thesis says that we can never carry out those calculation to get a true/false answer.
I like to think of incompleteness as a mathematical property, applying to all systems but allowing the "escape hatch" of switching to a more powerful system; and I like to think of the Church Turing thesis as a law of physics, that there is a limit to the logical power of any physical system (i.e. Turing completeness).
Being like a law of physics makes the Church-Turing thesis really unique in computer science. Most of the things we work with are theorems but the Church-Turing thesis is distinctly non-provable. The evidence we have for it is that no one ever managed to observe a counterexample.
the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into some interesting implications when I incorporate dependent typing, but it feels like there must be something theoretical that's already out there.
> what is the property of a program that makes it undecidable?
That is itself an undecidable question!
There are a lot of programs for which you can tell that they halt (programs with no loops, for example). Likewise there are a lot of programs for which you can tell that they do not halt (any program whose main body is a WHILE TRUE loop in a language that does not have exceptions, for example.) And then there are lots of more complicated cases for which the answer can be found. But there are some cases where we just don't know. The best known is this:
Not only do we not know the answer, but we don't know if it is even possible to find the answer! We know (because Turing) that there exist programs for which we cannot find the answer, but we don't know whether the Collatz problem is one of them. And in general we cannot know, because if we could then we could use that knowledge to solve the halting problem itself! (We might be able to prove undecidability for particular programs, just as we can prove halting or non-halting for particular programs, but deciding undecidability for any particular program is in general undecidable!)
but that's exactly my point - there are clear-cut halting, clear-cut non-halting, and "we don't know yet" programs. My interest is in delineating the properties that separate the 3. The collatz conjecture is exactly the example I use when explaining the "we don't know yet" programs. If I could build a logic system that can positively prove halting, and one that can positively prove non-halting, then anything that remains is "dunno".
The halting problem is basically showing that you can never prove the category of "dunno" to be empty. Which is pretty self-evident given there are unsolved bounding problems like the collatz conjecture in mathematics.
For a minimal example, if I create a program that takes an AST and runs it through two truth functions, one that checks if the AST === "return;" and prints "it halts" and one that checks if the AST === "while(true) {}" and prints "it never halts", then we've already created such an application, just with a "dunno" space containing the majority of programs. Adding practical axioms to a logic system could grow the "halts" and "never halts" spaces to the point where only a subset of applications cannot be excluded from the "dunno" space, and my question is: what are the unique properties of those applications?
But that is exactly my point: what separates these three classes is the state of our current mathematical knowledge, and that obviously changes over time.
> Which is pretty self-evident
No, that is not at all self-evident. (If it were, someone would have proven it long before Turing, and he wouldn't be famous for it.) I don't know what you mean by a "bounding" problem, but we can prove a lot of things about programs with a structure similar to Collatz. For example, we can prove that a program that searches for a prime larger than its input will always halt for any input.
I think op's problem is different than the one normally studied - he wants to design a halting program and find the class of programs for which it works.
This is typically not very popular as these statements depend a lot on the program, and the representations of programs unlike the halting problem computability statement.
Yes, I understand that. And what I'm saying is: you can't do that. The halting problem is formally equivalent to proving arbitrary mathematical theorems. For every program, there is a corresponding theorem which is true IFF the program halts, and for every theorem there is a corresponding program that halts IFF the theorem is true. So the question: for what programs can the halting problem be decided? is formally equivalent to the question: what theorems can we prove? And we can't prove any useful theorems about that because if we could, we could solve the halting problem!
[UPDATE] I want to revise my claim that if we could prove interesting theorems about which programs have decidable halting properties that we could solve the halting problem itself. That's not true, because the word "interesting" is too poorly defined. But what is true is that if we could do this then we could prove theorems that we could not previously prove (that has to be true for any reasonable definition of "interesting"). Furthermore, we could now prove these theorems in a purely mechanistic way with no need for human creativity. By any stretch of the imagination that would be a major breakthrough.
>> he wants to design a halting program and find the class of programs for which it works.
> Yes, I understand that. And what I'm saying is: you can't do that.
Not sure if it's relevant, but it's certainly possible to define an approximate halting-problem-decider, then figure out what it does and doesn't work for.
For example, a trivial implementation which checks if the given program is equal to `42`, outputs "halts" if it is, outputs "don't know" if it isn't. The space of programs it works for is { `42` }, the space of programs it doesn't work for is `remove(42, enumerateAllPrograms)`
Thank you, this is the space I'm wanting to work in - maximising the number of programs that can be decided. I'm just not sure what kind of logic I could use for such a system.
it's self-evident _at this point in time_, given you could feed such a machine the collatz conjecture as an algorithm and we just don't know if any arbitrary input will halt. I'm not claiming it is self-evident in perpetuity. By bounding problem I guess I mean the mathematical equivalent of knowing it can halt. I'm not a mathematician as I previously stated so I don't know the terminology.
I don't think the space I'm talking about is equivalent to the state of all of our mathematical knowledge, as AFAIK not all problems relate directly to this space. But a subset of all mathematics, sure (perhaps computability, or logic in general although of a higher kind than first-order). My interest is in creating a static analyser based on the set of axioms or deductions that can be derived from that space.
No, it's not. Just because you and I don't know the answer is not proof that no one knows the answer. Someone may have discovered the answer in the last five minutes. (In fact, for any mathematical discovery there is always necessarily a period time when only one person knows the answer.)
> AFAIK not all problems relate directly to this space
And I am telling you that you are wrong about that. If you think that there is anything about computation that does not relate to math then you have a deep misunderstanding of either computation or math (possibly both).
Let me rephrase that to hopefully make it sound a little less insulting: if you are able to identify an aspect of computation that cannot be described mathematically then you will be remembered alongside Turing, Godel and von Neuman as one of the greatest thinkers humanity has ever produced. (But a priori, the odds of your being able to do that seem pretty low to me.)
well you've just gone and been inaccurate yourself - I said that I didn't believe all mathematical discoveries had an impact on computability, but you just suggested I was saying that not all computation is based in mathematics. Which is absurd and it's clear you think I'm stupid, where to me it's pretty clear you are misinterpreting what I'm saying, whether that's poor communication on my part or uncharitable interpretation on yours.
I've been friends with academics before who had an unyielding desire to interpret lay speak as an attempt to be rigorous and then criticise it as such, as you have done with me saying "self-evident", but surely you realise I'm not trying to say "self-evident" in some kind of rigorous mathematical sense? I mean if you're just trying to be obtuse it's working well but it comes off like you're trying to hold my conversational and largely intuition-based ideas to a much higher standard than I am trying to meet. I don't understand the impulse at all. If I were trying to be totally rigorous with my thoughts rather than just conversationally trying to communicate an idea that is still taking shape, I would be learning the correct syntax to write a paper and sharing that instead.
> I said that I didn't believe all mathematical discoveries had an impact on computability, but you just suggested I was saying that not all computation is based in mathematics. Which is absurd
No, that's not what I said. What I said was that this statement:
"I don't think the space I'm talking about is equivalent to the state of all of our mathematical knowledge, as AFAIK not all problems relate directly to this space."
is false. This is not a matter of opinion. There is a formal equivalence between math and computability. For every theorem, there is a corresponding program that halts IFF the theorem is true, and for every program, there is a corresponding theorem that is true IFF the program halts. Therefore, it is necessarily the case that all mathematical discoveries have an impact on our knowledge of computability because there is in fact no distinction between math and computability. They are the exact same field of study, just with different window-dressing.
> and it's clear you think I'm stupid
No, I don't think you're stupid, merely ignorant (and a bit defensive). And this has nothing to do with your lack of rigor, it has to do with your intuition that there might be something worthwhile to be discovered by trying to examine the structure of known halting and non-halting programs. This is a well understood problem. It is possible that you could discover something that everyone else has overlooked. But if you do, it would be a breakthrough of the highest order, a major revolution in both computability theory and mathematics.
If you think I'm trying to discover something then you've completely missed my point. I was never looking to discover some new concept, but to find an existing model of looking at computability and implement it as software. I know its possible to decide computability for at least some subset of programs because we can do it by eye, I'm just looking to do the same thing programmatically in a way that is theoretically sound.
Yes, I understand that. And what I'm trying to tell you is that this problem you have set for yourself is formally equivalent to the problem proving mathematical theorems. They are the same problem. Any substantial progress on one is necessarily also substantial progress on the other.
not quite - I'm trying to implement existing proofs into an axiomatic system. All unproven theorems can be classified as the "don't know" outcome. But I don't know what approach to use to implement a system that can look at "f(x: int) => x is cleanly divisible by 2 ? f(x + 1) : halt" and tell me that this recursive function all halt under all valid inputs. Because that would require that it be able to derive such a fact from a core understanding of what addition and division mean.
> that would require that it be able to derive such a fact from a core understanding of what addition and division mean
Yes, and that's the part that's not possible in general, only for specific cases. For example, you can prove that:
f(P: int -> boolean, x: int) => P(x) ? f(x + 1) : halt
will halt for any x IFF there are an infinite number of integers that have the property P, so f will halt if P is "is an even integer" because there are an infinite number of even integers (which, obviously, you can also prove).
And with that in mind, you might want to go take another look at:
> My interest is in creating a static analyser based on the set of axioms or deductions that can be derived from that space.
From the sound of it, I think this might be a little backwards: axioms and deductions give rise to a space of possible proofs, and those can be used for things like static analysis. One example of going the other way is "reverse mathematics", where we try to find a set of axioms that give rise to some statement. I'm not sure if that could be applied to a (perhaps informal) "space" of theorems rather than some particular theorem.
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.
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.
> 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.
yeah I'm aware that I'm trying to build a platform that proves arbitrary theorems. I think where we're butting heads is that I'm wanting to approach such a platform from a constructive angle - starting with simple axioms and building up from there. The initial system may only be capable of interpreting natural number equality and addition.
My original question was around what theoretical approach best matches that goal - whether it's an axiomatic system based on Peano arithmetic, or a natural deductive system, or something based on type theory. From a non-academic perspective these fields all seem very similar and there seems to be a lot of crossover so I didn't know what best suited the problem I'm trying to solve. Of course even when the system is complete some functions will remain undecidable, but I'm totally OK with that. It may even be that something like a deductive classifier better suits the problem than a mathematical representation.
> I'm aware that I'm trying to build a platform that proves arbitrary theorems.
OK, well, that was far from clear. Here's your original question:
> the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into some interesting implications when I incorporate dependent typing, but it feels like there must be something theoretical that's already out there.
You're right, there is "something theoretical that's already out there", and that "something theoretical" is Turing-equivalence (and a vast literature on automated theorem proving).
> My original question was around what theoretical approach best matches that goal - whether it's an axiomatic system based on Peano arithmetic, or a natural deductive system, or something based on type theory. From a non-academic perspective these fields all seem very similar and there seems to be a lot of crossover so I didn't know what best suited the problem I'm trying to solve.
You're right. All of those fields are very similar. In fact, they are equivalent because they are all Turing-complete. It is really hard to avoid Turing-completeness, and even there all of the possible options are well understood.
The bottom line is that you (AFAICT) are at the very beginning of an extremely well-worn path. Actually, not just one path, but many, many paths, all of which lead to the same place: undecidability (and meta-undecidability and meta-meta-undecidability...) No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found (though of course that can't be proved because undecidability!) The best you can hope for is to make reasonable engineering tradeoffs that work for some domain of interest. But at the end of the day, you're just doing math, and math is hard. Nowadays it's really, really hard because all the low-lying fruit was picked a long, long time ago.
But if you're really serious about this, the first step is to get a stack of textbooks on computability theory and automated theorem proving and read them.
> OK, well, that was far from clear. Here's your original question:
Yeah, sorry about that - not being an academic myself makes it hard to put it across in the correct way.
> No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found
That's absolutely fine by me - I'm not looking to break through the undecidability barrier, only to implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories).
The numerous branching and totally equivalent fields is the thing I'm wary of - I don't want to have to invest 6 months learning category theory, only to find out that what I want to do is better expressed by type theory or second order logic or something else entirely. I guess in my mind it's similar to building a complex application in one programming language just to discover certain patterns can't be idiomatically expressed in that language, so you have to write horrible hacks to compensate for that lacking where you could have chosen a different language in the first place. From my own research I'm leaning towards axiom systems, perhaps utilising Zermelo-Fraenkel set theory as a basis. I don't know, it's early days yet. I'll keep reading and get a rough grasp on the principal fields before I make a definitive decision.
> I'm not looking to break through the undecidability barrier
That, too, was far from clear. You said you were tackling this problem:
> what is the property of a program that makes it undecidable?
and I told you:
> That is itself an undecidable question!
and explained why (at least three times). And AFAICT you still don't get it because you still say you want to:
> implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories)
and that is the problem of automated theorem proving, which is an open research issue, and (provably) always will be.
If you want to get a small taste of what you're up against, try proving that this program always halts:
f(x:int, y:int) = ( x+y == y+x ? halt : loop )
In other words, try proving the commutative law of addition.
If you get that, try to prove that this lambda-calculus expression
(λ (n f) (n (λ (c i) (i (c (λ (f x) (i f (f x))))))(λ x f) (λ x x)))
And even all that is just what you get from discrete math! Then there's calculus, topology, algebraic varieties (of which elliptic curves are one example, and even that is a whole field of study). And even here we've not even begun to scratch the surface of what is possible. The world of math is (provably!) richer than you -- or anyone -- can possibly imagine! That's what "undecidable" means.
Your only reasonable hope of making any kind of non-trivial progress is to focus on one domain, and then use the constraints imposed by the properties of that domain to shrink the problem down to something potentially manageable.
See, I'm not an academic - proving that addition is commutative is not in scope for what I'm wanting to do. It is not a big leap for me to make that an axiom in my system, I'm almost entirely disinterested in trying to innovate in the pure theory of foundational mathematics. I find the theory itself extremely interesting but that's just not my path. I thought I was clear about what I was wanting to build - a practical system for categorising functions that can be shown to halt or not always halt, lumping everything else into a third category. Academia and pure maths just isn't for me, this is so I can build a language with minimal bugs.
Yes, you were very clear. But saying "I want to build a practical system for categorising functions that can be shown to halt or not always halt, but I'm not interested in theory" is kind of like saying, "I want to build a practical warp drive, but I'm not interested in physics."
> 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... ). 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!
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.
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!
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 ):
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:
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 ;)
hey, just so you're aware I am working my way through your answer. I appreciate the depth of your comment and will be coming back to reply once I've fully understood your answer. I don't know how long it takes for HN to lock a thread for replies, but if you want to discuss this further would you mind dropping me an email (my address is in my profile)? It might take a couple more days for me to formulate a response.
hey Chris, I've read through your argument a few times and completely see your point - I've encountered this kind of second-system loop myself while trying to whiteboard a way to map a function to a representation that can be treated more like an algebra. Now my angle of approach is - I would be delighted for my system to not permit the collatzLoop function to be declared without constraining the range of natural numbers allowed!
From the sounds of it a totality checker may be what I'm actually wanting to write, rather than a type system - to be honest, I wanted to avoid explicit type notation within this language anyway, I'd much rather treat the functions included as a mapping where the output type inherently contains the relationship it shares with the inputs. I see two approaches I could proceed with: one fairly simple but not ideal, and one that is more optimal but that I do not know how to approach.
Scenario 1: What I'm imagining is a checker that, given a specific recursive function, can determine the exact input type that is required in order to terminate in 1 execution, 2 executions, and so on up until a defined limit. So for the collatz conjecture, it could determine that only the input `1` would halt on a single execution, `2` on two executions, etc but then would open up to either `32` or `5` after five executions. That seems simple enough to implement by converting branches into multiple function signatures and "solving for x" with substitution. However, I would love to be able to ensure that a function halts after an unrestricted number of recursions, and it seems as though it would be possible - because we can intuitively know that, for example, a function `f(n: Nat) => n is even ? f(n / 2) : f(n + 1)` will always halt on valid input.
Scenario 2: If we can intuitively know the fact noted above then surely that intuition could be encoded into a program? It seems like more of a meta concept in that I don't believe it would be possible to show such a fact using simple algorithmic substitutions (although I would welcome being wrong on this, makes my life easier!). From reading about the history of various mathematical fields over the past couple of weeks it seems like this pattern has shown up in maths on numerous occasions and appears to be basically a fundamental trait of logic - that any closed system that is permitted to contain references to the whole system suddenly gains a whole new set of behaviours that cannot be understood from the "meta-level" of the system itself. I mean, that's what GEB seems to be partially about too. A set containing sets that does not contain itself, the proof of the halting problem including an oracle that can call itself with itself as input, that kind of thing. And there's often a new system "on top of" the self-referential system that basically takes the self-reference out and provides a new meta-level for reasoning about the lower system, but with extra added self-reference. I guess what I'm trying to get to is - this scenario #2 seems like it must match up to some theory or another that is perhaps one of these meta-theories atop something like category theory or deductive logic - not looking at the relationships between input and output directly, but the relationship between the relationships, to determine whether it eventually resolves down. Something that could tell that the above-mentioned function halts, from base principles. I've found something that seems comparable in axioms and axiom schemata, but being able to build an axiomatic system seems pretty deep down the logic rabbit-hole and I don't want to dive in head-first without knowing I'm at least looking in the right direction, y'know?
Anyways, whether you respond to this comment or not, I want to thank you for your comment. You've described in a much more comprehensive way, something that I've been bumping into while researching this topic and that helps a great deal to verify to me that going down the lower meta-level route (damn you, lack of relevant terminology!) of trying to convert the logic into a different representation and solve that way is a fruitless exercise - though I still don't know if it is possible to move to a higher meta-level and make some progress from there; I guess that's why I'm asking :)
It does sound like you might be after something closer to totality checking. I'm not as familiar with that, but I can maybe give a few pointers and a bit of terminology:
One easy way to guarantee termination, even for functions with input/output spaces that are infinite, is using "structural recursion". This is when we only make recursive calls on a 'smaller piece' of our input. The classic example is the `Natural` type, where we can do:
f Zero = somethingNonRecursive
f (Succ n) = somethingInvolving (f n)
We can tell just from the syntax that the argument will always get smaller and smaller for each recursive call. Note that structural recursion is syntactic: we cannot do something like `f n = f (n - 1)` since the syntactic form `n - 1` is not a 'smaller piece' of the syntactic form `n`; whereas `x` is a smaller piece of `Succ x`. This makes structural recursion pretty limited. As an example, the "Gallina" language of the Coq language/proof assistant does totality checking via structural recursion, and it very quickly becomes unusable (more on Coq below!).
There's actually a subtlety here: if `Natural` is defined inductively then all of its values are finite (it is the least fixed point of its constructors, sometimes written as a "μ" or "mu" operator; similar to the Y combinator). In particular its values are `Zero`, `Succ Zero`, `Succ (Succ Zero)`, and so on. This means that structural recursion on `Natural` will eventually stop, either by hitting `Zero` or some other "base case" (e.g. functions involved in the Collatz conjecture might stop at `Succ Zero`, etc.).
We could instead decide to use the greatest fixed point (sometimes written as a "ν" or "nu" operator); we call such definitions coinductive, and a coinductive `Natural` type would contain values `Zero`, `Succ Zero`, `Succ (Succ Zero)`, and so on and an infinite value `Succ (Succ (Succ ...))` (sometimes written as "ω" or "omega"; not to be confused with the non-terminating program omega `(λx. x x) (λx. x x)`!). Structural recursion on values defined coinductively might not terminate; but it does coterminate, which is the idea of being "productive" like I showed with `Delayed`. (Note that in my Collatz examples I was assuming that `Natural` was defined inductively and `Delayed` was defined coinductively). Note that all datatypes in Haskell are coinductive. Also note that a type may contain many different infinite values, for example if we define trees like:
data Tree : Type where
Leaf : Tree
Node : Tree -> Tree -> Tree
If this is coinductive we can have any arrangement of finite and infinite branches we like. Another interesting example is `Stream t` which is like `List t` but only contains infinite values (there is no base case!):
data Stream (t : Type) : Type where
Cons : t -> Stream t -> Stream t
We can extend structural recursion a little to get "guarded recursion". In this case when we define a function like `f(arg1, arg2, ...)` which makes recursive calls like `f(newArg1, newArg2, ...)` we must also specify some function, say `s`, such that `s(newArg1, newArg2, ...) < s(arg1, arg2, ...)`. The function `s` effectively calculates a "size" for each set of arguments, and if we can prove that the "size" of the recursive arguments is always less than the "size" of the original arguments, then we guarantee termination/cotermination. This would allow things like `f n = f (n - 1)`, given a suitable "size" function (which could be the identity function in this case) and a proof (manual or inferred) that it always decreases. The Isabelle proof assistant does totality checking in this way, and I think it's also how Agda works (but Agda tries representing this using "sized types", which confuses me ;) ).
Talking about meta levels, proof assistants can provide an "escape hatch". The way Coq works is that proofs are represented in the "Gallina" language, which is total. We can write Gallina terms directly, but it can be painful. Instead, we can use a meta-language called "Ltac", which is a (rather awful) untyped Turing-complete imperative programming language. We can use Ltac to construct Gallina terms in whichever way we like; when we "compile" or check a Coq program/proof, that Ltac is executed and, crucially, it might not halt! We don't actually need such a large separation between object level and meta level: there's a really nice Coq plugin called "Mtac" which extends the Gallina language with a `Delay t` type (a polymorphic version of my `Delayed` example; we could say `Delayed = Delay Natural`), and the only "meta" operation it defines is converting a value of `Delay t` to a value of `t`, which it does by unwrapping any `Later` constructors at compile/check time. Just like Ltac, this might not halt (since there could be infinitely many `Later` wrappers).
Another thing to keep in mind with totality checking is "strictly positive types". Types are called "positive" or "negative" depending on whether they contain functions which return or accept values of that type. I've never looked into this in much depth (since languages like Coq will tell you when it's not allowed), but it seems like types which aren't "strictly positive" allow us to define infinite values, which shouldn't be allowed for inductive types.
Another thing to look at regarding self-reference is predicative vs impredicative definitions. Impredicative definitions are like "lifting yourself up by your bootstraps" (see e.g. http://wadler.blogspot.com/2015/12/impredicative-images.html ;) ).
I don't follow research in totality checking too closely, only where it overlaps my interests in programming language design and theorem proving. One memorable paper I've come across is https://dl.acm.org/citation.cfm?id=2034680 but whilst it's a nice application of language and representation, it's not clear to me if it's much of an advance in totality checking (i.e. it's a neater way of doing known things). I also see a steady trickle of work on things like "parameterised coinduction" and "circular coinduction" which seem related to totality, but they're slightly above my ability to tell whether they're brilliant new insights or just niche technical results. At least I hope they lead to better support for coinduction in Coq. You can tell how long someone's worked with this stuff based on how much they joke about the name (although I couldn't resist laughing when someone seriously remarked that "well of course everyone loves Coq" ;) ) versus how much they joke about "lol lack of subject reduction".
Thanks for coming back to me! Totality checking sounds exactly like what I was looking for; because your examples of structural and guarded recursion closely match parts of the algorithm I had already figured out through playing around with logical structures.
You've given me a lot to look into and I sincerely appreciate the effort you've put into opening up these fields to me. There's a few concepts you've mentioned that are still a little hazy to me (particularly coinductive types and the "Delayed" concept - which sounds somewhat like a generator function?) but now I know the terminology I can begin to research these topics myself in earnest. I always that find with the sciences, the hardest part of diving into a new field is simply knowing what you're looking for, followed shortly by building an accurate mental model of the concepts. You've helped a great deal with both, so thank you :)
Turing machines output yes/no or indefinitely go on, so that might be like your possible outputs of halts/doesn't halt/don't know. I'm not really sure how much to assume you know, so the [wiki page](https://en.wikipedia.org/wiki/Halting_problem) might help
> what is the property of a program that makes it undecidable?
It's important to keep in mind that undecidability and the halting problem only apply in general, not for some particular input or program.
With that said, I think it's to do with program length. The Busy Beaver numbers tell us the maximum number of steps a turing machine can take before halting, when given a program of a certain length. No matter how clever we try to make our static analyser, we ultimately have to write it down as a program (e.g. a turing machine tape, or something more sane ;) ) and this will have a particular, finite size. Hence there is an upper bound on the number of steps that any static analyser can take (the Busy Beaver number for its program length), unless it runs forever without giving us an answer.
Consider a particularly simple static analyser: it reads in a program, executes that program for N steps, and checks to see if it halted yet. If it halted, the static analyser halts with the answer "halts"; if it didn't halt, the static analyser halts with the answer "dunno". This static analyser can be improved by using a larger value of N; yet that necessarily requires a longer static analyser program (to contain the larger N value). That's what the Busy Beaver numbers tell us: calculating a number larger than BusyBeaver(X) requires a program more than X bits long; so we can't use a value of N that's larger than the Busy Beaver number of our static analyser's program length. If we want a bigger N, we will eventually need to make our program longer, since that's the only way to increase this bound caused by the Busy Beaver.
Note that there is another way we could "improve" such a static analyser: we could remove the cutoff completely, and just run the given program until it halts. In this case, the static analyser itself may not halt, so we're back to square one ;)
Now consider that there are infinitely many programs we might feed into a static analyser. These input programs can be arbitrarily long (much longer than our static analyser), and hence the limits imposed on them by the Busy Beaver numbers can be arbitrarily higher than the limits of the static analyser. In particular, their control flow can be arbitrarily complex, such that figuring out whether or not it halts can require an arbitrary amount of calculation steps. Since the number of steps any particular static analyser can perform is bounded by its Busy Beaver number, there will be infinitely many programs which that static analyser can't figure out; even though the same algorithm could figure them out, if given a larger limit to work with.
In this sense, we can think of all static analysis algorithms as being like Busy Beaver approximators: they're trying to calculate the largest number they can, in order to reach the number of steps required to analyse whatever program they've been given. They can do this in two ways: by bloating out their codebase to be much bigger than the programs they analyse, or by making their code more complex than the programs they analyse.
From a practical point of view, most human-written programs are incredibly simple and verbose; so these Busy Beaver limits aren't really a problem. Yet they're the reason that certain problems cannot be solved in the general case.
