Hacker News Reader

Comment by beaconstudios | Hacker News Reader

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.

View on HN

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

For which the answer from the program is "I don't know".

Really? Even for "x is a prime number"?

How would you even express that as a piece of code? I'm not talking about magic blackbox functions.

Seriously? You don't know how to write a function that tests if a number is a prime?

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

computes a factorial expressed as a Church numeral. (See http://www.flownet.com/ron/lambda-calculus.html for some hints.)

And that's just what you get from elementary arithmetic. If you really want to blow your mind, look at:

http://www.mrob.com/pub/math/largenum.html

and the associated software:

http://www.mrob.com/pub/perl/hypercalc.html

Once you get to infinity you are only just getting started:

https://johncarlosbaez.wordpress.com/2016/06/29/large-counta...

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."

I'm not interested in trying to encode a proof that addition is commutative. I'm interested in the theory to the point where I'll enjoy (and have been enjoying) learning about the math, but in terms of implementation I just don't want or need to start that low.

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

    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 ):

    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 ;)

That is quite possibly one of the best comments ever posted to HN!

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 :)

Reply on news.ycombinator.com