Topos theory can be added to type theory to provide a categorical semantics.
But even with Grothendieck topology (total and co-total categories) requires sets with least upper bound (join) and a greatest lower bound (meet).
The problem is that you get semi-algorthms, thus will only halt if true.
IMHO it is better to think of recursion as enabling realizability, and forcing fixed points. The ycombinator can be used for recursion because it is a fixed point combinator.
From descriptive complexity FO+LFP=SO+Krom=P, while FO by itself is AC^0 IIRC?
Using model logic+relations is another path.
The problem I have found is those paths tend to require someone to at least entertain intuitionistic concepts and that is a huge barrier.
Mostly people tend to use type theory to convert symantic properties to trivial symantic properties for convenience.
Blackburn/Rijke/Venema's “Modal Logic” is the most CS friendly book for that if you want to try.
Yes, it's interesting to see when coders start dealing with physical world problems and sensor systems and don't realize they are relying on constructivity to do anything at all. I've mostly only met other devs who have also worked in the CRDT space that grok intuitionistic reasoning.
Funny I fought for a good 5 min trying to convert everything to semantic on my phone, and finally gave up, figuring it also proved I wasn't a bot :) I have fixed it now.
But yes: semantic, run-time, extensional, etc... from Rice/Godel/etc...
There's no call stack in a tail-recursive function. It's equivalent to a loop.
And that, if you think about it a bit, might help you understand what recursion is, because your current understanding seems a bit off.
The only time you need a "call stack" with recursive calls is if the calls need to ultimately return to the call site and continue executing. It's still recursive.
By contrast, the model in which every function call pushes a return address, whether or not it's really needed, is a kind of mistake that comes from not understanding recursion.
Yes. This is correct, tail call optimized recursion is physically different than other types of recursion. It's much needed syntactic and structural sugar for goto.
Yes well we all have our pet theories about the world. Thankfully the people that think the natural numbers aren't "real" or that recursion isn't "real" haven't won out and destroyed our ability to make meaningful progress.
I'm curious about what you mean by recursion not being physically real? Do you mean it doesn't convert to CPU instructions, or something around occurence in nature?
Treating complex types, structure, arrangement, entanglement, etc. as if it has the same realness or priority as primitive types is a mistake.
It's like acting like recursion is physically real (it's not) when it smuggles in the call stack.