Skip to main content
Theoretical Computer Science

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

Required fields*

14
  • 1
    $\begingroup$ I only agree with (3). The other two are ... strange? $\endgroup$ Commented May 24, 2023 at 21:03
  • $\begingroup$ I agree with @AndrejBauer :-) It seems that you have your own understanding of what a programming language is, and that this does not exactly match the one that PL people have. Maybe we should just look at concrete examples. Now that I look closer at it, the example you give in your question (the definition of $g$ and $f$) already shows, in my eyes, a misconception. You are obviously treating $f$ and $g$ as function symbols of an equational theory over the language of semirings. That is not a programming language. $\endgroup$ Commented May 25, 2023 at 5:01
  • $\begingroup$ The interpretation that I had in mind of your example when I wrote my answer was that you were working in some kind of programming language with primitive recursion (for loops). That's why I wrote that the type of your $f$ is $A^2\times\mathsf{nat}\to A$. Notice that, crucially, this is not $A^3\to A$ unless $A=\mathsf{nat}$ (the type of natural numbers). The standard operational semantics of primitive recursion will result in the type $\mathsf{nat}$ being a natural number object (nno). Therefore, denotational models must interpret $\mathsf{nat}$ as a nno in the target category. $\endgroup$ Commented May 25, 2023 at 5:05
  • $\begingroup$ Now, I challenge you to exhibit a finite-product category $\mathbf C$ with a nno which, externally, may be seen as a ring of finite characteristic. I'd be amazed if you found it. It certainly isn't $\mathbf{Set}$, in which you seem to be taking your interpretation. So, your interpretation of your "program" $f$ as a function $R^3\to R$ where $R$ is a ring of finite characteristic simply does not exist in the world of denotational semantic! $\endgroup$ Commented May 25, 2023 at 5:10
  • 1
    $\begingroup$ Finally, it is not true that you may make your $f$ converge by changing its interpretation. As a program (of type $A^2\times\mathsf{nat}\to A$), your $f$ will always diverge, regardless of how you interpret $A$! This is what I told you in another comment: the behavior of programs does not depend on how you interpret them! At this point, your whole question appears to be based on a rather big misconception... $\endgroup$ Commented May 25, 2023 at 5:13