Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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?
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.)
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.
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.
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?
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.
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.
1 to 9 of 9