Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorSam Staton
   • CommentTimeMay 26th 2019
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexComment about Ackermann function. I don't know what Ackermann originally wrote, but most texts use A_0(m)=m+1, if I understand correctly. <a href="https://ncatlab.org/nlab/revision/diff/partial+recursive+function/18">diff</a>, <a href="https://ncatlab.org/nlab/revision/partial+recursive+function/18">v18</a>, <a href="https://ncatlab.org/nlab/show/partial+recursive+function">current</a>

   Comment about Ackermann function. I don’t know what Ackermann originally wrote, but most texts use A_0(m)=m+1, if I understand correctly.

   diff, v18, current

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 26th 2019
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks, Sam. The definition I wrote comes from the lecture notes of Stephen Simpson that I put in the references. Let's see: if $A_0(m) = m+1$, then I seem to get $A_1(m) = A_0^m(1) = m+1$ as well. So maybe those other references use a slightly different recursive rule?

   Thanks, Sam. The definition I wrote comes from the lecture notes of Stephen Simpson that I put in the references.

   Let’s see: if $A_0(m) = m+1$, then I seem to get $A_1(m) = A_0^m(1) = m+1$ as well. So maybe those other references use a slightly different recursive rule?

3. • CommentRowNumber3.
   • CommentAuthorSam Staton
   • CommentTimeMay 27th 2019
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexThanks, you're right, they put an extra f in the inductive step. This is the version I learnt as a student, and also the version on wikipedia. I don't know a case for using one or the other, though. <a href="https://ncatlab.org/nlab/revision/diff/partial+recursive+function/19">diff</a>, <a href="https://ncatlab.org/nlab/revision/partial+recursive+function/19">v19</a>, <a href="https://ncatlab.org/nlab/show/partial+recursive+function">current</a>

   Thanks, you’re right, they put an extra f in the inductive step. This is the version I learnt as a student, and also the version on wikipedia. I don’t know a case for using one or the other, though.

   diff, v19, current

4. • CommentRowNumber4.
   • CommentAuthorSam Staton
   • CommentTimeMay 27th 2019
   • (edited May 27th 2019)
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexIncidentally, my understanding of the fact that Ackermann is not definable in the free category with products and a natural numbers object, but is definable in the free ccc with a natural numbers object, is that the former category contains functions with termination ordinal $\lt \omega^\omega$, whereas the latter contains functions with termination ordinal $ \lt \epsilon_0$. (In the sense of [[https://ncatlab.org/nlab/show/ordinal+analysis|ordinal analysis]].)

   Incidentally, my understanding of the fact that Ackermann is not definable in the free category with products and a natural numbers object, but is definable in the free ccc with a natural numbers object, is that the former category contains functions with termination ordinal $\lt \omega^\omega$, whereas the latter contains functions with termination ordinal $\lt \epsilon_0$. (In the sense of ordinal analysis.)

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 27th 2019
   • (edited May 27th 2019)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexYes, thanks. I don't know if you looked carefully at the nLab article, but I did record a detailed proof there that Ackermann cannot live in the standard category whose objects are finite powers $\mathbb{N}^n$ in $Set$ and whose morphisms are primitive recursive maps between them. If it lived in the initial category with products and a *parametrized* NNO, then you could transfer it along the product-preserving map over to the standard category. Meanwhile, at the Café I explicitly wrote down a definition of Ackermann in the free CCC with NNO, which I assume you saw (because otherwise, it'd be quite a coincidence that you started this thread just now), but in case not, it's [here](https://golem.ph.utexas.edu/category/2019/05/polyadic_boolean_algebras.html#c055900). Meanwhile, I've added another Café comment [here](https://golem.ph.utexas.edu/category/2019/05/polyadic_boolean_algebras.html#c055903).

   Yes, thanks. I don’t know if you looked carefully at the nLab article, but I did record a detailed proof there that Ackermann cannot live in the standard category whose objects are finite powers $\mathbb{N}^n$ in $Set$ and whose morphisms are primitive recursive maps between them. If it lived in the initial category with products and a parametrized NNO, then you could transfer it along the product-preserving map over to the standard category. Meanwhile, at the Café I explicitly wrote down a definition of Ackermann in the free CCC with NNO, which I assume you saw (because otherwise, it’d be quite a coincidence that you started this thread just now), but in case not, it’s here.

   Meanwhile, I’ve added another Café comment here.

6. • CommentRowNumber6.
   • CommentAuthorSam Staton
   • CommentTimeMay 27th 2019
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexSorry, yes, I came from the café, and your nice definition of Ackermann in the free ccc! That was indeed the context of my comment #4, which should perhaps have gone on the cafe instead.

   Sorry, yes, I came from the café, and your nice definition of Ackermann in the free ccc! That was indeed the context of my comment #4, which should perhaps have gone on the cafe instead.

7. • CommentRowNumber7.
   • CommentAuthorDavidRoberts
   • CommentTimeOct 3rd 2019
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI think the claim ([here](https://ncatlab.org/nlab/show/partial+recursive+function#Lawvere)) that partial recursive functions give a Lawvere theory is incorrect, as the cartesian product $\mathbb{N}^k$ is not the product in any category whose objects are finite powers of $\mathbb{N}$ and whose morphisms are some class of partial functions closed under composition and including projections and diagonals. There is a unique partial function $\mathbb{N}^m \to \mathbb{N}^{k+l}$ induced from a pair of partial functions $\mathbb{N}^m \to \mathbb{N}^k$ and $\mathbb{N}^m \to \mathbb{N}^l$, but the usual triangles don't commute! The cartesian product here is only a 'restriction product', namely a lax product in the locally posetal 2-category determined by the given category of partial functions. Since the primitive recursive functions are total and include projections, that's not a problem. I'm not sure what I want to put in place of the current statement: a disclaimer? an explanation of what goes wrong? An attempt at outlining a generalisation of a Lawvere theory?

   I think the claim (here) that partial recursive functions give a Lawvere theory is incorrect, as the cartesian product $\mathbb{N}^k$ is not the product in any category whose objects are finite powers of $\mathbb{N}$ and whose morphisms are some class of partial functions closed under composition and including projections and diagonals. There is a unique partial function $\mathbb{N}^m \to \mathbb{N}^{k+l}$ induced from a pair of partial functions $\mathbb{N}^m \to \mathbb{N}^k$ and $\mathbb{N}^m \to \mathbb{N}^l$, but the usual triangles don’t commute! The cartesian product here is only a ’restriction product’, namely a lax product in the locally posetal 2-category determined by the given category of partial functions.

   Since the primitive recursive functions are total and include projections, that’s not a problem.

   I’m not sure what I want to put in place of the current statement: a disclaimer? an explanation of what goes wrong? An attempt at outlining a generalisation of a Lawvere theory?

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeOct 3rd 2019
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexInteresting point. I notice, though, that the claim as stated only says that > a morphism $k \to 1$ of the Lawvere theory is a function $\mathbb{N}^k \to \mathbb{N}^1$ belonging to the class [of partial recursive functions] whereas you seem to be objecting to a version of this statement with $k$ replaced by an arbitrary $n$. It seems to me that we would get a Lawvere theory if we take this statement as written, only applying to the morphisms $k\to 1$, and then *define* the morphisms $k\to n$ to be what they have to be to make it a Lawvere theory, namely $n$-tuples of partial recursive functions $\mathbb{N}^k \to \mathbb{N}^1$ --- which, as you note, are not the same as single partial recursive functions $\mathbb{N}^k \to \mathbb{N}^n$. Put differently, partial recursive functions "naturally" form a cartesian operad, which we can then make into its equivalent Lawvere theory.

   Interesting point. I notice, though, that the claim as stated only says that

   a morphism $k \to 1$ of the Lawvere theory is a function $\mathbb{N}^k \to \mathbb{N}^1$ belonging to the class [of partial recursive functions]

   whereas you seem to be objecting to a version of this statement with $k$ replaced by an arbitrary $n$. It seems to me that we would get a Lawvere theory if we take this statement as written, only applying to the morphisms $k\to 1$, and then define the morphisms $k\to n$ to be what they have to be to make it a Lawvere theory, namely $n$-tuples of partial recursive functions $\mathbb{N}^k \to \mathbb{N}^1$ — which, as you note, are not the same as single partial recursive functions $\mathbb{N}^k \to \mathbb{N}^n$.

   Put differently, partial recursive functions “naturally” form a cartesian operad, which we can then make into its equivalent Lawvere theory.

9. • CommentRowNumber9.
   • CommentAuthorDavidRoberts
   • CommentTimeOct 4th 2019
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexOh, I see, defining the problem away! Neat. (I think you mean "with $1$ replaced by an arbitrary $n$") I will edit the entry to make this more clear.

   Oh, I see, defining the problem away! Neat. (I think you mean “with $1$ replaced by an arbitrary $n$”)

   I will edit the entry to make this more clear.