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

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.

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

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