Talk:Remainder is Primitive Recursive

Can be slightly simpler

If I’m not mistaken, then when using a convention $a\bmod 0 = a$ (more on justification of that at SE), it’s possible to omit $\map \sgn m$ from the final expression. Analogously it allows removing that same subexpression from the final result at Quotient is Primitive Recursive. (I don’t think it’s essential enough for the potential controversy of this convention (though I myself think it’s more useful than any other), and I’m inexperienced with the traditions here, so I won’t edit these pages, but maybe someone would decide it’s woth the candle?) --Arseniiv (talk) 20:20, 10 June 2019 (EDT)

The development of this subject on $\mathsf{Pr} \infty \mathsf{fWiki}$ has not at this point defined $\bmod$ as a primitive recursive function, so it cannot be used in a proof of primitive recursion. --prime mover (talk) 01:28, 11 June 2019 (EDT)

Oops, I should have written $\rem$, of course. --Arseniiv (talk) 07:25, 11 June 2019 (EDT)

Yes I see your point. But there's a specifically-crafted structure to the whole exposition of the primitive recursive functions whose aim is to lead up to Godel's things. It's probably because the URM encoding of $\rem$ is simpler when you return zero for the zero-divisor case than the alternative. However, unless we are prepared to go through the whole of the pages downstream from here to make them consistent with that alternative definition (which at the moment I am not) it would be better to leave it as it is. Long time since I put these pages together and I'm not immediately certain where the source material is (somewhere in the loft I believe). --prime mover (talk) 09:54, 11 June 2019 (EDT)