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