Conversation

Notices

1. Embed this notice
   julesh (julesh@mathstodon.xyz)'s status on Wednesday, 06-Nov-2024 21:26:30 JST julesh

   Basic question but I'm not 100% sure: it's not possible to have a "reasonable" syntax that captures exactly the total computable functions N → N, right?

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Wednesday, 06-Nov-2024 21:28:33 JST julesh

     in reply to

     There's a canonical way to overshoot, namely the partial computable functions, and multiple very interesting ways to undershoot, such as the primitive recursive functions

   • Embed this notice
     Philip Trettner (artificialmind@fosstodon.org)'s status on Wednesday, 06-Nov-2024 23:29:45 JST Philip Trettner

     in reply to

     @julesh I think that's basically what the Calculus of Inductive Constructions (as used in Coq / Lean) provides.

     The syntax only allows recursion on structurally smaller arguments.

     Recursion on inductive types is always well-founded and you can define inductive types for a well-foundedness relation, which basically means that all provably total functions are definable.

     The syntax ranges from "reasonable" (any obviously structural recursion requires no annotiation) to "custom proof required".

   • Embed this notice
     Philip Trettner (artificialmind@fosstodon.org)'s status on Wednesday, 06-Nov-2024 23:29:45 JST Philip Trettner

     in reply to

     @julesh There is still a gap as far as I understand it: there exist functions that are computable and total but where the totatily cannot be proven inside the same system. This should be a consequence of Gödel's incompleteness.

     However, the CIC can represent almost all of math, so I don't know if such functions can exist in practice. How do you "know" that it is total while being unable to prove it?

     Like, I think you can prove their existence but never provide an example. (I'm fuzzy on this)

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Wednesday, 06-Nov-2024 23:29:45 JST julesh

     in reply to

     • Philip Trettner

     @artificialmind I know of one way to construct a total computable function that is not structurally recursive (bar recursion is the best known example), but it's for functions with a type like (N -> N) -> N, I don't remember how it adapts to N -> N computability

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Wednesday, 06-Nov-2024 23:51:35 JST julesh

     in reply to

     In this sense, Turing completeness is a *really bad* property of a programming language because it's such a gigantic over-approximation of the thing you actually want, which is the total computable functions. In this sense the thing that languages like Agda and Idris do is much better: "by default" (ie. using the obvious type signature Nat -> Nat) supply as big a possible under-approximation of total computable functions that contains everything you need it to contain except for 1 in a million cases, and for the remaining 1 in a million cases let you get back to the standard over-approximation by partial computable functions by using a different type signature (like Nat -> Delay Nat or whatever)

   • Embed this notice
     CubeRootOfTrue (cuberootoftrue@mathstodon.xyz)'s status on Thursday, 07-Nov-2024 00:28:40 JST CubeRootOfTrue

     in reply to

     @julesh binary logic proves too much
     a -> (b -> a) is BS but binary logic thinks it's fine

   • Embed this notice
     John Carlos Baez (johncarlosbaez@mathstodon.xyz)'s status on Thursday, 07-Nov-2024 00:49:46 JST John Carlos Baez

     in reply to

     @julesh - "Basic question but I'm not 100% sure: it's not possible to have a "reasonable" syntax that captures exactly the total computable functions N → N, right?"

     I'm pretty sure that's true, but we should phrase it in theorems so we can spot loopholes. Here's what I know. The set of total computable functions is not computably enumerable: there's no total computable function f: ℕ²→ℕ such that every total computable function ℕ→ℕ is one of the f(i, -): ℕ→ℕ. The proof is an easy diagonal argument.

     So then the question is whether "a reasonable syntax that captures exactly the total computable functions ℕ→ℕ" must give a way to computably enumerate these functions.