<p>Let me amend Damiano's answer with more specific comments.</p>
<p>Terms of type <code>bool</code> are <em>not</em> logical statements. Expressions like <code>not (3 &lt; x) or (x == y)</code> have the exact same status as expressions like <code>3 + 5 * x</code>, i.e., they are <em>term</em> formers. Also, equality is just a term former (yielding a term of type <code>bool</code>).</p>
<p>In fact, there are no logical symbols whatsoever in a programming language. A programming language is a calculus of <em>terms</em>. Its model theory is more like universal algebra than first-order model theory.</p>
<p>There is of course plenty of logic, but it is not part of the programming language itself. It's built <em>around</em> the language, in more than one way.</p>
<p>There are <em>equational theories</em> of programming languages which describe how a language behaves in terms of equations only (hence comparison with universal algebra). A typical equation is <code>(if True then A else B) = A</code>.</p>
<p>There are <a href="https://xavierleroy.org/CdF/2020-2021/" rel="noreferrer"><em>program logics</em></a> which are custom-made formal systems with which we can state and prove properties of programs. Ordinary first-order logic is not appropriate, because it does not directly account for various phenomena, such as computational effects (intput-output, mutable state, exceptions) and non-termination. A typical example is <a href="https://en.wikipedia.org/wiki/Hoare_logic" rel="noreferrer">Hoare logic</a> in which formulas take the form <span class="math-container">$\{P\} \; c \; \{Q\}$</span>, read it &quot;if assertion <span class="math-container">$P$</span> holds (in current state) and command <span class="math-container">$c$</span> terminates, then assertion <span class="math-container">$Q$</span> will hold (in the resulting state)&quot;.</p>
<p>There are still other approaches that mix and match algebra, topology, category theory, and logic. It's a rich area.</p>
<p>Knowing first-order logic and model theory is very helpful as background knowledge, but they do not appear directly in programming language theory. You have to modify and generalize in various directions, and place emphasis elsewhere.</p>

CC BY-SA 4.0
2023-05-23T18:36:28.063Z
Thanks for this answer! One question: if we take, e.g., an equational theory of programming languages, then that theory has to account for how to evaluate expressions like ''3 + 5 * x''. That's fine if these are all natural numbers, but what if 3, 5, and x live in some arbitrary ring? It would seem like the equational theory of this programming language would have to encode the entire atomic diagram of the ring in question. So we'd need as many equations as the size of the ring itself, in general. Do I understand you correctly?
Siddharth
CC BY-SA 4.0
2023-05-23T19:50:46.603Z
I am not aware of anyone creating a programming language with an arbitrary ring. Presumably you would want one that is finitely presented. Also, an equational theory need not account for all aspects of the language – usually it is used as a reasoning tool. Evaluation can be described in some other way, in terms of operational semantics. One then checks that the equational theory is sound with respect to the operational semantics.
Andrej Bauer
CC BY-SA 4.0
2023-05-23T22:54:35.017Z
OK, an arbitrary ring is admittedly weird. Let's consider a simple nondeterministic program that recognizes if there is a path from vertex u to vertex v. Let vertex w be u; while w is not v, replace w by any neighbor of w. This program halts iff there is a path from u to v. It works over *any* graph. When we endow this program with an operational semantics, say, there seems to be a clear distinction between the "logical" steps (independent of the graph) and the "nonlogical" steps (picking a neighbor of the given vertex, dependent on the graph). Is this distinction not meaningful?
Siddharth
CC BY-SA 4.0
2023-05-24T12:00:35.000Z
Yes, the distinction you are making is precisely the distinction between "pure" computation steps and the computational effect (the non-deterministic choice of a vertex). This is all well established in the mathematical treatment of computational effects. But where are you going with all this?
Andrej Bauer
CC BY-SA 4.0
2023-05-24T19:33:01.517Z
(1/2) Basically I'm interested in when the recursion theory of a structure looks "classical" and when it's different. For example, if we consider first-order programs over the natural numbers taking the increment (S, successor) and decrement (P, predecessor) operations plus equality tests as primitive, we get a normal Turing-complete model of computation. But if we lose S we get a drastically different model of computation (looks more like a complexity class). From a FOL perspective these structures are the same, as S is a definitional expansion of P. But their computation theories differ.
Siddharth
CC BY-SA 4.0
2023-05-24T19:38:11.957Z
(2/2) Similar work has been done in the past, for example on the notion of "adequacy" by Lynch and Blum (https://groups.csail.mit.edu/tds/papers/Lynch/mst80.pdf). A collection of binary string primitives is adequate if all PTIME queries can be computed by programs making a polynomial number of calls to the primitives. In any case, I'm interested in programs operating over arbitrary first-order structures, and on classifying structures by how expressive these programs are. This naturally leads me to the questions I asked originally.
Siddharth
CC BY-SA 4.0
2023-05-24T21:06:33.080Z
As far as I can tell there is a rather large divide between your interests and experience on one hand, and what we're trying to convey on the other. But it's hard to pin it down. Practically all programming languages are Turing-complete – but that is a very *un*intersting observation from the PL perspective. (Of course there are studies on how to design a PL that matches precisely a given complexity class, etc., but overall that's not the sort of thing that PL design and semantics is about.)
Andrej Bauer
CC BY-SA 4.0
2023-05-21T09:33:50.290Z
2023-05-23T08:05:37.797Z
2023-05-23T08:05:37.797Z
Andrej Bauer
<p>Models in some semantic framework are essentially a mapping from synthetic objects to some other domain of object. In the sematic domain we typically identify or take as equivalent a bunch of synthetic objects. We do this because we know things about the sematic domain that we can use to learn things about the synthetic objects.</p>
<p>At the one extreme, one can map a program to the function that it computes over the standard model. Two programs are the same if they compute the same function. That is not a very useful semantics, we are often interested in also how they compute it. (I assume we at least care about what function the program is computing.)</p>
<p>At the other extreme, we can take the synthetic objects themselves as the semantic domain. That is not a very useful semantics.</p>
<p>Between these two there are many possibly semantic domains that one can use. Denotational semantics (with emphasize on s) are some very useful semantic domains. Note that we don't just care about the objects themselves but the relationships between them.</p>
<p>However, keep in mind that things are not as clean as they may look at first. Denotational semantics works great for languages that are nice (functional programming), but you will see someone taking about the denotational semantics of a common programming language like Go or C or Java or JavaScript or Python. Similarly for languages like Prolog.</p>
<p>Having a semantic domain also is not sufficient for model <em>theory</em> in the sense of logic. We can construct models but model theory cares more about nonstandard models typically than standard model, because that is what is related to provablity in theories. We don't need just a syntax with construction rules, we need axioms about what can be said about those objects that are inherently incomplete. I want to go to the nonstandard model of reals with infinitesimals and show something holds there and then transfer that back to standard reals using the fact that the language and the theory cannot distinguish between these two. In programming the languages are typically too powerful. The typical model theory deals with relatively simple cases that are not strong enough to express computation. Almost all interesting programming language are expressive enough to write a Turing machine simulator. The model theory of arithmetic theories like PA might be more inline from the perspective of complexity they have. Even there, one needs to not use the True Arithmetic theory but some limited set of axioms. When taking about programming language, the theory people typically use is all of mathematics. These are I think partly responsible for why we don't have a model theory of programming languages in the sense of logic.</p>

CC BY-SA 4.0
2023-05-25T04:33:03.300Z
2023-05-25T04:33:03.300Z
Kaveh
<p>Thanks to everyone! I'm just going to summarize my takeaway from the helpful responses and comments above targeted towards someone in mathematical logic wondering the same thing as I did. Please let me know if anything here is inaccurate. <strong>Update:</strong> Seems like it is, please see the comments below!</p>
<p><strong>(1) There is no distinction between logical and nonlogical symbols.</strong> That is because programming languages come with a <em>fixed</em> set of data, and moreover, the semantics for the functions and relation symbols over that data is tied into the semantics of the whole programming language. E.g., if your programming language contains the symbol <span class="math-container">$+$</span>, then your semantics has to account for <span class="math-container">$+$</span>.</p>
<p>This is not to say that <em>in principle</em> you could not study programs in an arbitrary signature <span class="math-container">$L$</span> which take semantics over any <span class="math-container">$L$</span>-structure. It's just not part of the enterprise of the theory of programming languages.</p>
<p><strong>(2) Programs, not structures, are first-class citizens.</strong> Since we don't consider <span class="math-container">$L$</span>-programs operating over arbitrary <span class="math-container">$L$</span>-structures, we don't tend to define properties of, or otherwise classify, structures themselves.</p>
<p><strong>(3) The semantics of programs and first-order formulas have a common generalization.</strong> Despite the differences in attitude and orientation between PL theory and model theory, they share a common categorical setting. (See Damiano's answer for an elaboration of this.)</p>

CC BY-SA 4.0
2023-05-24T21:03:39.980Z
I only agree with (3). The other two are ... strange?
Andrej Bauer
CC BY-SA 4.0
2023-05-25T05:01:21.447Z
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.
Damiano Mazza
CC BY-SA 4.0
2023-05-25T05:05:04.303Z
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.
Damiano Mazza
CC BY-SA 4.0
2023-05-25T05:10:39.070Z
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!
Damiano Mazza
CC BY-SA 4.0
2023-05-25T05:13:48.383Z
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...
Damiano Mazza
CC BY-SA 4.0
2023-05-25T12:46:11.530Z
Thanks @DamianoMazza! I am hopeful that understanding this example will get to the core of my misconception. Why must the third argument to $f$ be an nno? Indeed, I was imagining $f : A^3 \to A$, *not* $A^2 \times \text{nat} \to A$. The definition of $f$ is not by primitive recursion on $z$.
Siddharth
CC BY-SA 4.0
2023-05-25T12:58:50.537Z
Yes, you are right, the definition is not by primitive recursion.  My understanding of it was that you were using the usual inductive definition of the type $\mathsf{nat}$ of natural numbers, so your definition is by cases (you test for zero and then you do something based on that test).  Primitive recursion uses the inductive structure of $\mathsf{nat}$, but it was a mistake for me to mention it.
Damiano Mazza
CC BY-SA 4.0
2023-05-25T13:10:29.010Z
The fundamental point remains: you are just considering an equational theory over the signature of semirings.  That's *not* a programming language.  No one who studies programming languages takes a random equational theory and calls it a "programming language", referring to its terms as "programs".  Programming languages must, in one way or another, have to do with computable functions, you must be able to represent computation with them.  In which programming language is your example written, and how does this programming language compute?
Damiano Mazza
CC BY-SA 4.0
2023-05-25T13:29:48.343Z
In fact, now that I look at it, your definition of $g$ and $f$ does not even seem to be representable as an equational theory.  I don't know how to make your definition by cases fit into an equational theory.  It can certainly fit a more elaborate kind of theory (certainly a first-order theory, for example).  But then, again, you are just doing usual logic and model theory, so all of a sudden I don't understand your question anymore...
Damiano Mazza
CC BY-SA 4.0
2023-05-25T16:01:03.183Z
The semantics of this specific example: given any structure $M$ in the signature of semirings, consider the family $X$ of partial functions $M^3 \to M$ partially ordered by extension ($\sqsubseteq$). The right-hand-side of the definition of $f$ defines a monotone operator on $(X,\sqsubseteq)$. Take its least fixed point; that is your definition of $f$.
Siddharth
CC BY-SA 4.0
2023-05-25T16:03:35.913Z
In general, given any system of recursive equations in the signature of semirings, where the right-hand-sides are terms built up from the semiring operations, cases, and recursive calls, we can endow it with a least fixed-point semantics in a similar way. In what sense does this fail to be a programming language?
Siddharth
CC BY-SA 4.0
2023-05-25T18:20:08.703Z
Unfortunately, there is no formal definition of "programming language", so it's impossible to say why this isn't one :-D  If I have to point out a reason, it would be that the syntax of this system is devoid of an operational semantics:  given a "program", how do you evaluate it, independently of the semantics?  Another, related reason: I do not see how to encode in this "programming language" usual computation on some kind of finite structure (integer, strings), directly in terms of the syntax, as one may always do with usual programming languages.
Damiano Mazza
CC BY-SA 4.0
2023-05-25T18:24:23.223Z
This doesn't mean that what you do is meaningless!  It just means that it's difficult, if not impossible, to relate/adapt what people usually do in PL theory to your setting, also for what concerns denotational semantics.
Damiano Mazza
CC BY-SA 4.0
2023-05-26T01:52:04.440Z
I can certainly give a big-step semantics, and I am pretty sure there is no obstacle to a small-step semantics, but I'd have to think about that. (Both, of course, depend on the structure $M$!) But certainly we don't automatically have integers, strings, etc Anyway, thanks for the clarification, this was very helpful!
Siddharth
CC BY-SA 4.0
2023-05-24T20:02:08.850Z
2023-05-25T12:29:32.977Z
2023-05-25T12:29:32.977Z
Siddharth
<p>The model theory of programming languages is called <em>denotational semantics</em>.  You can google the term to find out more about it, I'll give an extreme synthesis of it.</p>
<p>Denotational semantics is a special case of &quot;categorical logic&quot;, which is itself a generalization (introduced in the 1960s by Bill Lawvere) of the usual model theory of first-order logic.  The idea is that a programming language may be seen as a (syntactic) category whose objects are combinations of basic types (Booleans, natural numbers, etc.) and whose arrows are equivalence classes of programs depending on a finite number of arguments.  When I say &quot;combinations of basic types&quot; I mean that usually the syntactic category has at least products and a terminal object, the rest depends on the language. I am not going to explain what it means for two programs to be &quot;equivalent&quot; (and therefore to represent the same arrow in the syntactic category), but intuitively it means that they &quot;evaluate to the same thing&quot;.</p>
<p>For example, for your program <span class="math-container">$f$</span>, if the multiplication you use in its definition has type <span class="math-container">$A\times A\to A$</span>, then <span class="math-container">$f$</span> would be an arrow of the syntactic category of type <span class="math-container">$A\times A\times\mathsf{nat}\to A$</span>.  (Programs that do not return anything are typed with the terminal object).</p>
<p>Now, depending on your programming language, its syntactic category <span class="math-container">$\mathcal C$</span> will have a certain structure and properties (like I said, it will have at least finite products).  Then, your language will have (denotational) models in any category with that structure and properties.  Given such a category <span class="math-container">$\mathbf D$</span>, a model is just a structure-and-property-preserving functor <span class="math-container">$F:\mathcal C\to\mathbf D$</span>.  For example, <span class="math-container">$\mathbf D$</span> could be <span class="math-container">$\mathbf{Set}$</span>, so your types will be interpreted by sets and your programs by functions.  More often, <span class="math-container">$\mathbf D$</span> will be a category with the property that every arrow has a (least) fixpoint, because fixpoints are needed to interpret recursion.  A famous example is <span class="math-container">$\mathbf{Cpo}$</span>, the category of complete partial orders and Scott-continuous maps.</p>
<p>The fact that the category <span class="math-container">$\mathcal C$</span> is &quot;syntactic&quot; means, a bit more technically, that it is sort of the &quot;free category&quot; with such and such structure/properties built from the syntax of the programming language.  Therefore, the functor <span class="math-container">$F$</span> corresponding to the denotational model will be defined as soon as you define it on the basic types and on the basic pieces of the syntax of your programming language.  This is precisely what happens in the usual model theory for first-order logic, where a model is defined as soon as you fix a set (more generally, an object of a category) interpreting the universe where your individuals live, and a function/relation (more generally, a morphism/subobject) for every function/relation symbol of your logical language.  The fact that the model must verify the axioms of the theory correponds, in denotational semantics, to the fact that the arrows of the syntactic category are equivalence classes of programs, so your denotational model must equate equivalent programs.</p>
<p>A final word of warning: in many expository texts on programming languages, denotational semantics is presented directly as an interpretation of the basic pieces of syntax into a certain category, without any reference to the functorial perspective or the construction of the syntactic category, so don't be surprised if you do not see that appearing explicitly.</p>
<p><strong>Addendum:</strong> let me clarify how categorical logic is able unify traditional model theory (of first-order logic) and denotational semantics.</p>
<p>The categorical viewpoint on traditional model theory is that every first-order theory <span class="math-container">$\mathbb T$</span> induces a <em>Boolean pretopos</em> <span class="math-container">$\mathrm{Syn}(\mathbb T)$</span>, the <em>syntactic category</em> of <span class="math-container">$\mathbb T$</span>.  It doesn't matter what a Boolean pretopos is exactly, all it matters for the sake of this answer is that the category <span class="math-container">$\mathbf{Set}$</span> of sets and functions is a Boolean pretopos, and that we may define a (very large) category of Boolean pretoposes and <em>morphisms</em> between them, which are functors preserving all the properties that make a category into a pretopos.</p>
<p>One of the pillars of categorical logic (the observation originally due to Lawvere) is that a model of <span class="math-container">$\mathbb T$</span> in the traditional sense is exactly the same thing as a morphism of Boolean pretoposes</p>
<p><span class="math-container">$$\mathrm{Syn}(\mathbb T)\to\mathbf{Set}.$$</span></p>
<p>As I said in the comments, one may take another Boolean pretopos as <span class="math-container">$\mathbf{Set}$</span>, and get models in that pretopos. For example, if <span class="math-container">$\mathbf{FinSet}$</span> is the category of finite sets, then a morphism <span class="math-container">$\mathrm{Syn}(\mathbb T)\to\mathbf{FinSet}$</span> is a finite model of <span class="math-container">$\mathbb T$</span>.</p>
<p>As Andrej pointed out, the theory of programming languages is more similar to universal algebra at this level, in the sense that a programming language may be seen as an <em>equational theory</em>: there are no logical operators, quantifiers, or anything like that, only terms (representing programs), built out of function symbols (or &quot;term-formers&quot;), and equalities between them (representing the so-called &quot;operational semantics&quot; of the programming language).  Also, with respect to first-order logic, there are <em>types</em>, that is, the equational theory is <em>multisorted</em> (in traditional model theory, every first-order theory implicitly has only one sort).</p>
<p>However, the idea of (denotational) model is exactly the same as that of first-order model.  For example, the theory <span class="math-container">$\mathbb G$</span> of groups is a (single-sorted) equational theory, and a group in the traditional sense is just a product-preserving functor</p>
<p><span class="math-container">$$\mathrm{Syn}(\mathbb G)\to\mathbf{Set}.$$</span></p>
<p>Here, changing the target category is very useful, and you have even more freedom than in (classical) first-order logic because you have less properties to preserve (equational logic is much simpler than first-order logic--in fact, in this case all you need is a category with finite products, which is <em>way</em> less than a (Boolean) pretopos).  For example, product-preserving functors <span class="math-container">$\mathrm{Syn}(\mathbb G)\to\mathbf{Top}$</span> are <em>topological groups</em>, product-preserving functors <span class="math-container">$\mathrm{Syn}(\mathbb G)\to\mathbf{Sch}$</span> are <em>algebraic groups</em>, etc., all objects which naturally come up in mathematics. Categorical logic gives a uniform account of all this variety of structures.</p>
<p>Similarly, when one defines a denotational model of a programming language <span class="math-container">$\mathbb P$</span> in which types and programs are interpreted as objects and arrows of some category <span class="math-container">$\mathbf D$</span>, one is implicitly defining the syntactic category <span class="math-container">$\mathrm{Syn}(\mathbb P)$</span> and a structure/property-preserving functor</p>
<p><span class="math-container">$$\mathrm{Syn}(\mathbb P)\to\mathbf{D}.$$</span></p>
<p>The big difference with model theory, pointed out by Martin Berger in his comment, is that, in the theory of programming languages, there is no canonical class of categories, fixed once and for all, such that <span class="math-container">$\mathbf{D}$</span> and <span class="math-container">$\mathrm{Syn}(\mathbb P)$</span> belong to that class.  This is in sharp contrast with first-order logic (where we have (Boolean) pretoposes) or algebraic theories like <span class="math-container">$\mathbb G$</span> (where we have finite-product categories).  In other words, there is no canonical &quot;logical structure&quot; that we know <span class="math-container">$\mathbb P$</span> must have (unlike first-order theories or algebraic theories): it all depends very much on the kind of programming language that <span class="math-container">$\mathbb P$</span> is. This is ultimately due to the lack of a formal definition of &quot;programming language&quot;.</p>
<p>That being said, there are some important cases, encompassing many useful situations.  For example, a typical categorical structure for programming languages is that of a Cartesian closed category with a natural number object and a fixpoint operator, which is enough to define a Turing-complete programming language. (This shows, in particular, that you cannot take <span class="math-container">$\mathbf D=\mathbf{Set}$</span>, because <span class="math-container">$\mathbf{Set}$</span> does <em>not</em> have a fixpoint operator. So being able to vary the target of the intepretation functor is a generalization which is absolutely fundamental to programming languages!).</p>
<p>Another big difference with traditional model theory is that, usually, people do not study the relationship between various models <span class="math-container">$F:\mathrm{Syn}(\mathbb P)\to\mathbf D$</span> for a fixed <span class="math-container">$\mathbf D$</span>, because they differ in uninteresting ways.  For example, when <span class="math-container">$\mathbb P$</span> is the simply-typed <span class="math-container">$\lambda$</span>-calculus, the only choice you have in defining <span class="math-container">$F$</span> is to pick an object of <span class="math-container">$\mathbf D$</span> for each atomic type, and the specific choice is often irrelevant.  So, contrarily to first-order logic, it is interesting to change <span class="math-container">$\mathbf D$</span> rather than pick a <span class="math-container">$\mathbf D$</span> and then let <span class="math-container">$F$</span> vary.  In fact, when people say that they have a &quot;model&quot; of a programming language, usually they mean that they have a <span class="math-container">$\mathbf D$</span> with the desired structure/properties, not that they have fixed one specific <span class="math-container">$F$</span>. This is another reason why denotational semantics has a different flavor than usual model theory, even though technically they are related via categorical logic.</p>
<p>By the way, all this (long!) digression was only to drive my point home: <em>denotational semantics is to programming languages what model theory is to first-order theories</em> (with all the necessary caveats).  You do <strong>not</strong> need to know categorical logic in order to understand or study denotational semantics!</p>

CC BY-SA 4.0
2023-05-21T10:06:46.053Z
At this level of abstraction, is this characterisation of model theory in PL saying anything more than:
*we map syntax to something else*? (Yes, you get a bunch of coherence conditions from the categorical language, but they are trivial in general.)
The beauty of (20th century) model theory is that the righthand side
of the map from mathematical structures was fixed (ZF(C) set
theory)! Moreover, on both sides we have first-order logic as
unproblematic background.

So really, (20th century) model theory has been a study of ZF(C). PL has nothing comparably canonical, as of 2023.
Martin Berger
CC BY-SA 4.0
2023-05-21T13:52:46.053Z
Beauty is in the eye of the beholder, but the fact that, in traditional model theory, the target of the interpretation functor is fixed to the category $\mathbf{Set}$ is seen by many (starting from Lawvere) as an unnecessary limitation.  Mathematics is full of structures which are not bare sets, and allowing the target category of logical interpretations to vary is a very nice (or should I say very beautiful?) way of incorporating this into model theory.
Damiano Mazza
CC BY-SA 4.0
2023-05-21T14:08:39.607Z
Anyhow, more to the point that (I think) you are trying to make: I am (painfully) aware that there is no canonical definition of "programming language".  In the terms of my answer, *we do not have a canonical class of categories such that all programming languages induce categories of that class*.  This is in contrast with first-order classical logic, where we have, for example, Boolean pretoposes.  But this doesn't invalidate my answer: from Lawvere's functoral viewpoint, denotational semantics and traditional model theory are literally *the same thing*.
Damiano Mazza
CC BY-SA 4.0
2023-05-21T14:18:24.110Z
One last, side remark: characterizing model theory as the "study of ZF(C)" is at best debatable, and quite misleading if you ask me.  Maybe you are confusing with *set theory*?  Model theory uses set theory (and ZF/ZFC) as a foundation, just like any other branch of mathematics.  The important theorems of model theory do not say *anything* about ZF(C), albeit they might of course depend on it (like the compactness theorem, which uses choice).  But then again, lots of theorems of other branches of mathematics depend on ZF(C). PL theory too is ultimately based on ZFC...
Damiano Mazza
CC BY-SA 4.0
2023-05-21T16:18:20.163Z
I don't wish to start a normative discussion about what model theory is, let alone should be.
In  my experience with mathematicians, when they learn about model theory, they do so
from books like Hodges, Chang/Keisler, or Shelah, and those are, for better or worse, ZF(C)-centric.
I'm sure Siddharth can clarify what he means.
Martin Berger
CC BY-SA 4.0
2023-05-22T12:08:24.117Z
I think the situation is even more dire (please correct me if I'm wrong), the problem isnt just that we need to define the syntactic category Syn(ℙ) for each new language ℙ, but rather that for many (most) ℙ of interest, we don't really know *how* to define the very concept of  Syn(ℙ) in a categorical language. (Or, on the upside: there are plenty of interesting open research questions! And they have immediate practical relevance: as soon as you can express language properties to be preserved in a nice way, you get a recipe for program verification and tooling.)
Martin Berger
CC BY-SA 4.0
2023-05-23T08:15:58.017Z
@MartinBerger Yes, it's true.  Otherwise stated, there are tons of interesting programming languages for which it is not clear what it means to define a denotational semantics.  What I say in my answer makes technical sense only for the more "traditional" languages (which are mostly $\lambda$-calculus based).  In fact, I personally think that, for programming languages, the denotational approach is less useful than the operational approach!
Damiano Mazza
CC BY-SA 4.0
2023-05-23T18:16:27.000Z
(1/2) Thank you @DamianoMazza for your comprehensive answer! I understand (at a high level) that a "denotational model" is a functor from the appropriate syntactic category to **Set**, **Cpo**, or otherwise, and this generalizes the notion of a model of a first-order theory.

However, one of the lessons of first-order model theory is that it's the *structures*, not the formulas, that are first-class citizens. For example, by asking simple questions like *how many models are there of a given theory?*, we get, roughly, classification theory---a deep and subtle taxonomy of first-order theories.
Siddharth
CC BY-SA 4.0
2023-05-23T18:27:41.163Z
(2/2) So--what can programs tell us about denotational structures?

Let also push back on the assertion that denotational models "in the same signature" differ in uninteresting ways. Take a first-order programming language in the signature of rings, with 0, 1, +, *, and =. If we interpret these operations in the natural numbers we get a Turing-complete programming language.

However, let us instead interpret these operations in, say, the algebraic closure of the finite field F_2 (an infinite field), Then we get a radically different model of computation (e.g., no universal program).
Siddharth
CC BY-SA 4.0
2023-05-24T12:32:16.757Z
@DamianoMazza I agree that operational semantics has absolute priority, but I don't see an antagonism, I think of denotational semantics as being a research methodology
for better understanding operational semantics, and, in particular, for developing reasoning principle (aka logics) for programming languages: the algebraic spirit makes us think in a certain direction, which is sometimes very successful, but has been failing for some forms of computation (e.g. parallel and timed computation), pointing to an incomplete understanding.
Martin Berger
CC BY-SA 4.0
2023-05-24T12:45:23.523Z
**(1/2)** @Siddharth 
Taking the natural numbers and operations on them as given is, in general, not what we study in computer science.                                                                                                                        
Instead, we assume that operations like addition or multiplication is something to be defined in the model of computation, not something already given *ex cathedra*.
Martin Berger
CC BY-SA 4.0
2023-05-24T12:45:47.463Z
**(2/2)** For example the Church numerals you mentioned up-thread
are essentially unary encodings of numbers, leading to computationally inefficient arithmetic operations. In addition, Church numerals are not typable in, for example, the simply-typed form of the $\lambda$-calculus,
you need something more powerful (e.g. System F).
While the questions you suggest by analogy with classical model theory are natural, I'd say, they don't fit with the spirit of contemporary studies of computation: mathematical structures like rings, fields, etc should be explained
as computation, not assumed.
Martin Berger
CC BY-SA 4.0
2023-05-24T19:44:35.450Z
Thanks. These last two comments really clarify things for me!
Siddharth
CC BY-SA 4.0
2023-05-24T20:31:48.250Z
@Siddharth as I underlined, beside the formal similarity given by the functorial perspective, model theory and denotational semantics are developed in very different ways and for very different purposes.  I don't know what kind of answer you are expecting for your question ("what can programs tell us about denotational structures"), but for sure you can't expect to transport your knowledge of model theory directly on denotational semantics.
Damiano Mazza
CC BY-SA 4.0
2023-05-24T20:39:34.417Z
@Siddarth about your second comment, you are misunderstanding what a "model of computation" is.  A programming language/model of computation doesn't change because you change its interpretation.  I don't know exactly what you have in mind with "a first-order programming language in the signature of rings", but either it will be Turing-complete or it won't, it's not a matter of how you interpret it.  And if it is Turing-complete, then your interpretation in the algebraic closure of $\mathbb F_2$ probably does not even exist (I can't say for sure without a precise definition).
Damiano Mazza
CC BY-SA 4.0
2023-05-21T09:18:29.330Z
2023-05-23T08:20:01.243Z
2023-05-23T08:20:01.243Z
Damiano Mazza
<p>I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between <em>logical</em> and <em>nonlogical</em> symbols. For example in the sentence <span class="math-container">$(\forall x)(\exists y)(x = y+1)$</span>, <span class="math-container">$+$</span> and <span class="math-container">$1$</span> are nonlogical symbols whereas <span class="math-container">$\exists$</span>, <span class="math-container">$x$</span>, <span class="math-container">$y$</span>, and <span class="math-container">$=$</span> are logical. The denotation of the sentence depends on the <em>interpretation</em> of those nonlogical symbols.</p>
<p>We could make exactly the same distinction in the syntax of programming languages. For example, the denotation of the program
<span class="math-container">$$ g(x) = f(x,x,1) \text{ where } f(x,y,z) = \begin{cases} y &amp; \text{if } z =0 \\ f(x,x\cdot y,z + 1)  &amp; \text{otherwise} \end{cases} $$</span>
depends on the interpretation of the nonlogical symbols <span class="math-container">$+$</span>, <span class="math-container">$\cdot$</span>, <span class="math-container">$0$</span>, and <span class="math-container">$1$</span>. In a ring of finite characteristic <span class="math-container">$n$</span>, <span class="math-container">$g$</span> computes the function <span class="math-container">$x \mapsto x^n$</span>. In a ring of characteristic 0, it computes the everywhere-divergent function.</p>
<p>My first question is, <strong>why is the distinction between logical and nonlogical symbols not fundamental in programming language theory?</strong> It doesn't appear in the beginning of (or, as far as I can tell, at all) in most introductory textbooks. Instead, programming languages seem to come with a <em>fixed</em> set of data that seems to include, at a minimum, booleans, natural numbers, and some mechanism for lists. (In other words, the interpretations of the nonlogical symbols are fixed.) My guesses are:</p>
<ol>
<li><strong>Definability is not the point.</strong> Rather, the point is to learn about various &quot;program constructs,&quot; i.e., the purely logical fragment of the syntax. These are much richer in PL theory than, say, first-order logic. The data are just the vehicle for that.</li>
<li><strong>Everything is founded on the lambda calculus,</strong> where we get a rich set of data for free via, e.g., Church numerals.</li>
<li>Possibly <strong>it is fundamental,</strong> and I just don't know it.</li>
</ol>
<p>Why should we care about varying the interpretation of nonlogical function symbols? One of the lessons of first-order logic is that it is more interesting to make structures, rather than formulas, first-class citizens. (<em>Structures</em> refers to interpretations of the nonlogical symbols.) For example, we say two structures are <em>elementarily equivalent</em> if they are satisfied by exactly the same formulas. This equivalence relation on structures turns out to be much more interesting than, say, logical equivalence of formulas, and gives rise to the whole field of model theory.</p>
<p>So my second question is, <strong>where is the model theory of programming languages?</strong> In other words, where are the properties <em>of structures</em> that come from studying programs that operate over them? Are they simply less interesting? Or, have they attracted less attention?</p>

CC BY-SA 4.0
2023-05-21T08:35:00.080Z
A suggestion, the higher-order nature of lambda calculus (as a logic) in programming languages has the tendency to blur the logical/non-logical distinction that's clear-cut in first-order case. Functions and datypes become the primitive. Logic can be recovered and thought in terms of functions via Curry-Howard correspondence. This is not so clear cut though, we still need axioms/inference rules for datatypes. We still need models for the polymorphic datatypes, most models pass through category theory.
Ilk
CC BY-SA 4.0
2023-05-21T08:37:43.530Z
Also note on church encoding, this is quite dependent on the way you turn the lambda calculus into logic and the flavor of predicativity, whether and what form of power sets you have. Depending on the flavor you might want to bake in the primitives or look for new ways to re-allow the encodings. In predicative setting church encodings end up increasing universe levels (roughly equivalent to bumping up one inaccessible cardinal), so primitive datatypes are the preferred style.
Ilk
CC BY-SA 4.0
2023-05-21T09:32:37.663Z
Unlike (first-order and propositional) logic with negation, conjunction, quantifiers etc, PL does not have canonical syntax that is beyond debate.                                                    
Moreover, a guiding assumption in CS is the Church-Turing thesis which says that, simplifying a bit, syntax doesn't matter as all (reasonable) PLs formalise the same                                      
notion of mechanical computation anyway. In addition, model theory is really based  (ZFC) set theory being the unproblematic background theory. PL theory currently lacks such a background.
Martin Berger
CC BY-SA 4.0
2023-05-21T09:33:48.550Z
**(1/2)** Elementary equivalence is used in the theory of programming languages.
It is well-known that program logics induce a notion of program
equality as follows: Define for $P, Q$ being arbitrary programs $P
\equiv_{ee} Q$ iff for any (Hoare logic) formulae we have: $\{A\} P \{B\}$
iff $\{A\} Q \{B\}$.  (Note that in model theory, one can prove that
two structures are elementary equivalent with the Ehrenfeucht–Fraïssé
games, i.e. bisimulation, a core notion of program equivalence.)
Martin Berger
CC BY-SA 4.0
2023-05-21T09:33:57.917Z
**(2/2)** We can then ask how
$\equiv_{ee}$ relates to other natural notions of program equivalence, in particular
the contextual congruence induced by the operational semantics. A
Hoare logic is called "observationally complete" if the latter coincides with
$\equiv_{ee}$. This has been fruitful in calibrating axiomatic semantics against the (typically more foundational) operational semantics.
Martin Berger
CC BY-SA 4.0
2023-05-21T09:37:39.370Z
@MartinBerger: that was simplifying more than a bit. I dare you to stand up at at a PL conference and shout "syntax doesn't matter, it's all equivalent to Turing machines". I'll bring popcorn.
Andrej Bauer
CC BY-SA 4.0
2023-05-21T09:41:24.543Z
@AndrejBauer Steve Vickers once said: *a truth is deep if its negation is also true.*
Martin Berger
CC BY-SA 4.0
2023-05-23T18:42:07.390Z
What does PL theory say about non-Turing complete programming languages, e.g., those used in implicit computational complexity?
Siddharth
CC BY-SA 4.0
2023-05-24T13:04:03.213Z
@Siddharth Much  implicit complexity
comes from PL theory, in particular logic and typing systems (which PL theory considers (almost) the same by the Curry-Howard correspondene),
since typing systems amount to language restrictions, here in particular restricing forms of recursion, to  enforce resource bounds on
programs. A lot of this work relates back to linear logic.
Martin Berger
CC BY-SA 4.0
2023-05-25T02:56:03.957Z
I would suggest also taking a look at the book "Foundations of Constructive Mathematics" by Michael Beeson.
Kaveh
CC BY-SA 4.0
2023-05-25T02:56:46.723Z
Another interesting read I think is Jean-Yves Girard's book.
Kaveh
CC BY-SA 4.0
2023-05-25T04:54:51.463Z
@Siddharth I don't understand your question.  PL theory may "say" the same things about any kind of language, Turing-complete or not, in the sense that its tools/ideas may be applied, to certain extents and with varying degree of pertinence, to *any* programming language.  Maybe you should tell us what you think PL theory "says" about Turing-complete languages, and then, maybe, we'll be able to tell you if it "says" the same of the non-Turing complete ones...
Damiano Mazza
CC BY-SA 4.0
2023-05-25T12:24:39.853Z
My comment in this thread was just in response to Martin's comment that "all (reasonable) PLs formalise the same notion of mechanical computation anyway." This seems to exclude non Turing-complete languages. I might have taken that comment too literally? Apologies if so.
Siddharth
<lo.logic><soft-question><type-theory><pl.programming-languages>
Where is the model theory in programming language theory?
Siddharth
# Where is the model theory in programming language theory?

(Asked by: username_0 on 2023-05-20)

I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between *logical* and *nonlogical* symbols. For example in the sentence $(\forall x)(\exists y)(x = y+1)$, $+$ and $1$ are nonlogical symbols whereas $\exists$, $x$, $y$, and $=$ are logical. The denotation of the sentence depends on the *interpretation* of those nonlogical symbols.

We could make exactly the same distinction in the syntax of programming languages. For example, the denotation of the program
$$ g(x) = f(x,x,1) \text{ where } f(x,y,z) = \begin{cases} y & \text{if } z =0 \\ f(x,x\cdot y,z + 1) & \text{otherwise} \end{cases} $$
depends on the interpretation of the nonlogical symbols $+$, $\cdot$, $0$, and $1$. In a ring of finite characteristic $n$, $g$ computes the function $x \mapsto x^n$. In a ring of characteristic 0, it computes the everywhere-divergent function.

My first question is, **why is the distinction between logical and nonlogical symbols not fundamental in programming language theory?** It doesn't appear in the beginning of (or, as far as I can tell, at all) in most introductory textbooks. Instead, programming languages seem to come with a *fixed* set of data that seems to include, at a minimum, booleans, natural numbers, and some mechanism for lists. (In other words, the interpretations of the nonlogical symbols are fixed.) My guesses are:

1. **Definability is not the point.** Rather, the point is to learn about various "program constructs," i.e., the purely logical fragment of the syntax. These are much richer in PL theory than, say, first-order logic. The data are just the vehicle for that.
2. **Everything is founded on the lambda calculus,** where we get a rich set of data for free via, e.g., Church numerals.
3. Possibly **it is fundamental,** and I just don't know it.

Why should we care about varying the interpretation of nonlogical function symbols? One of the lessons of first-order logic is that it is more interesting to make structures, rather than formulas, first-class citizens. (*Structures* refers to interpretations of the nonlogical symbols.) For example, we say two structures are *elementarily equivalent* if they are satisfied by exactly the same formulas. This equivalence relation on structures turns out to be much more interesting than, say, logical equivalence of formulas, and gives rise to the whole field of model theory.

So my second question is, **where is the model theory of programming languages?** In other words, where are the properties *of structures* that come from studying programs that operate over them? Are they simply less interesting? Or, have they attracted less attention?

**Tags:** lo.logic, soft-question, type-theory, pl.programming-languages

> **Comments:**
> **username_1**: A suggestion, the higher-order nature of lambda calculus (as a logic) in programming languages has the tendency to blur the logical/non-logical distinction that's clear-cut in first-order case. Functions and datypes become the primitive. Logic can be recovered and thought in terms of functions via Curry-Howard correspondence. This is not so clear cut though, we still need axioms/inference rules for datatypes. We still need models for the polymorphic datatypes, most models pass through category theory.  
> **username_1**: Also note on church encoding, this is quite dependent on the way you turn the lambda calculus into logic and the flavor of predicativity, whether and what form of power sets you have. Depending on the flavor you might want to bake in the primitives or look for new ways to re-allow the encodings. In predicative setting church encodings end up increasing universe levels (roughly equivalent to bumping up one inaccessible cardinal), so primitive datatypes are the preferred style.  
> **username_2**: Unlike (first-order and propositional) logic with negation, conjunction, quantifiers etc, PL does not have canonical syntax that is beyond debate.                                                     Moreover, a guiding assumption in CS is the Church-Turing thesis which says that, simplifying a bit, syntax doesn't matter as all (reasonable) PLs formalise the same                                       notion of mechanical computation anyway. In addition, model theory is really based  (ZFC) set theory being the unproblematic background theory. PL theory currently lacks such a background.  
> **username_2**: **(1/2)** Elementary equivalence is used in the theory of programming languages. It is well-known that program logics induce a notion of program equality as follows: Define for $P, Q$ being arbitrary programs $P \equiv_{ee} Q$ iff for any (Hoare logic) formulae we have: $\{A\} P \{B\}$ iff $\{A\} Q \{B\}$.  (Note that in model theory, one can prove that two structures are elementary equivalent with the Ehrenfeucht–Fraïssé games, i.e. bisimulation, a core notion of program equivalence.)  
> **username_2**: **(2/2)** We can then ask how $\equiv_{ee}$ relates to other natural notions of program equivalence, in particular the contextual congruence induced by the operational semantics. A Hoare logic is called "observationally complete" if the latter coincides with $\equiv_{ee}$. This has been fruitful in calibrating axiomatic semantics against the (typically more foundational) operational semantics.  
> **username_3**: @MartinBerger: that was simplifying more than a bit. I dare you to stand up at at a PL conference and shout "syntax doesn't matter, it's all equivalent to Turing machines". I'll bring popcorn.  
> **username_2**: @AndrejBauer Steve Vickers once said: *a truth is deep if its negation is also true.*  
> **username_0**: What does PL theory say about non-Turing complete programming languages, e.g., those used in implicit computational complexity?  
> **username_2**: @username_0 Much  implicit complexity comes from PL theory, in particular logic and typing systems (which PL theory considers (almost) the same by the Curry-Howard correspondene), since typing systems amount to language restrictions, here in particular restricing forms of recursion, to  enforce resource bounds on programs. A lot of this work relates back to linear logic.  
> **username_4**: I would suggest also taking a look at the book "Foundations of Constructive Mathematics" by Michael Beeson.  
> **username_4**: Another interesting read I think is Jean-Yves Girard's book.  
> **username_5**: @username_0 I don't understand your question.  PL theory may "say" the same things about any kind of language, Turing-complete or not, in the sense that its tools/ideas may be applied, to certain extents and with varying degree of pertinence, to *any* programming language.  Maybe you should tell us what you think PL theory "says" about Turing-complete languages, and then, maybe, we'll be able to tell you if it "says" the same of the non-Turing complete ones...  
> **username_0**: My comment in this thread was just in response to Martin's comment that "all (reasonable) PLs formalise the same notion of mechanical computation anyway." This seems to exclude non Turing-complete languages. I might have taken that comment too literally? Apologies if so.  

---

## 4 answers

### Answer by username_5 on 2023-05-21. Score: 15 | Accepted answer

The model theory of programming languages is called *denotational semantics*. You can google the term to find out more about it, I'll give an extreme synthesis of it.

Denotational semantics is a special case of "categorical logic", which is itself a generalization (introduced in the 1960s by Bill Lawvere) of the usual model theory of first-order logic. The idea is that a programming language may be seen as a (syntactic) category whose objects are combinations of basic types (Booleans, natural numbers, etc.) and whose arrows are equivalence classes of programs depending on a finite number of arguments. When I say "combinations of basic types" I mean that usually the syntactic category has at least products and a terminal object, the rest depends on the language. I am not going to explain what it means for two programs to be "equivalent" (and therefore to represent the same arrow in the syntactic category), but intuitively it means that they "evaluate to the same thing".

For example, for your program $f$, if the multiplication you use in its definition has type $A\times A\to A$, then $f$ would be an arrow of the syntactic category of type $A\times A\times\mathsf{nat}\to A$. (Programs that do not return anything are typed with the terminal object).

Now, depending on your programming language, its syntactic category $\mathcal C$ will have a certain structure and properties (like I said, it will have at least finite products). Then, your language will have (denotational) models in any category with that structure and properties. Given such a category $\mathbf D$, a model is just a structure-and-property-preserving functor $F:\mathcal C\to\mathbf D$. For example, $\mathbf D$ could be $\mathbf{Set}$, so your types will be interpreted by sets and your programs by functions. More often, $\mathbf D$ will be a category with the property that every arrow has a (least) fixpoint, because fixpoints are needed to interpret recursion. A famous example is $\mathbf{Cpo}$, the category of complete partial orders and Scott-continuous maps.

The fact that the category $\mathcal C$ is "syntactic" means, a bit more technically, that it is sort of the "free category" with such and such structure/properties built from the syntax of the programming language. Therefore, the functor $F$ corresponding to the denotational model will be defined as soon as you define it on the basic types and on the basic pieces of the syntax of your programming language. This is precisely what happens in the usual model theory for first-order logic, where a model is defined as soon as you fix a set (more generally, an object of a category) interpreting the universe where your individuals live, and a function/relation (more generally, a morphism/subobject) for every function/relation symbol of your logical language. The fact that the model must verify the axioms of the theory correponds, in denotational semantics, to the fact that the arrows of the syntactic category are equivalence classes of programs, so your denotational model must equate equivalent programs.

A final word of warning: in many expository texts on programming languages, denotational semantics is presented directly as an interpretation of the basic pieces of syntax into a certain category, without any reference to the functorial perspective or the construction of the syntactic category, so don't be surprised if you do not see that appearing explicitly.

**Addendum:** let me clarify how categorical logic is able unify traditional model theory (of first-order logic) and denotational semantics.

The categorical viewpoint on traditional model theory is that every first-order theory $\mathbb T$ induces a *Boolean pretopos* $\mathrm{Syn}(\mathbb T)$, the *syntactic category* of $\mathbb T$. It doesn't matter what a Boolean pretopos is exactly, all it matters for the sake of this answer is that the category $\mathbf{Set}$ of sets and functions is a Boolean pretopos, and that we may define a (very large) category of Boolean pretoposes and *morphisms* between them, which are functors preserving all the properties that make a category into a pretopos.

One of the pillars of categorical logic (the observation originally due to Lawvere) is that a model of $\mathbb T$ in the traditional sense is exactly the same thing as a morphism of Boolean pretoposes

$$\mathrm{Syn}(\mathbb T)\to\mathbf{Set}.$$

As I said in the comments, one may take another Boolean pretopos as $\mathbf{Set}$, and get models in that pretopos. For example, if $\mathbf{FinSet}$ is the category of finite sets, then a morphism $\mathrm{Syn}(\mathbb T)\to\mathbf{FinSet}$ is a finite model of $\mathbb T$.

As Andrej pointed out, the theory of programming languages is more similar to universal algebra at this level, in the sense that a programming language may be seen as an *equational theory*: there are no logical operators, quantifiers, or anything like that, only terms (representing programs), built out of function symbols (or "term-formers"), and equalities between them (representing the so-called "operational semantics" of the programming language). Also, with respect to first-order logic, there are *types*, that is, the equational theory is *multisorted* (in traditional model theory, every first-order theory implicitly has only one sort).

However, the idea of (denotational) model is exactly the same as that of first-order model. For example, the theory $\mathbb G$ of groups is a (single-sorted) equational theory, and a group in the traditional sense is just a product-preserving functor

$$\mathrm{Syn}(\mathbb G)\to\mathbf{Set}.$$

Here, changing the target category is very useful, and you have even more freedom than in (classical) first-order logic because you have less properties to preserve (equational logic is much simpler than first-order logic--in fact, in this case all you need is a category with finite products, which is *way* less than a (Boolean) pretopos). For example, product-preserving functors $\mathrm{Syn}(\mathbb G)\to\mathbf{Top}$ are *topological groups*, product-preserving functors $\mathrm{Syn}(\mathbb G)\to\mathbf{Sch}$ are *algebraic groups*, etc., all objects which naturally come up in mathematics. Categorical logic gives a uniform account of all this variety of structures.

Similarly, when one defines a denotational model of a programming language $\mathbb P$ in which types and programs are interpreted as objects and arrows of some category $\mathbf D$, one is implicitly defining the syntactic category $\mathrm{Syn}(\mathbb P)$ and a structure/property-preserving functor

$$\mathrm{Syn}(\mathbb P)\to\mathbf{D}.$$

The big difference with model theory, pointed out by username_2 in his comment, is that, in the theory of programming languages, there is no canonical class of categories, fixed once and for all, such that $\mathbf{D}$ and $\mathrm{Syn}(\mathbb P)$ belong to that class. This is in sharp contrast with first-order logic (where we have (Boolean) pretoposes) or algebraic theories like $\mathbb G$ (where we have finite-product categories). In other words, there is no canonical "logical structure" that we know $\mathbb P$ must have (unlike first-order theories or algebraic theories): it all depends very much on the kind of programming language that $\mathbb P$ is. This is ultimately due to the lack of a formal definition of "programming language".

That being said, there are some important cases, encompassing many useful situations. For example, a typical categorical structure for programming languages is that of a Cartesian closed category with a natural number object and a fixpoint operator, which is enough to define a Turing-complete programming language. (This shows, in particular, that you cannot take $\mathbf D=\mathbf{Set}$, because $\mathbf{Set}$ does *not* have a fixpoint operator. So being able to vary the target of the intepretation functor is a generalization which is absolutely fundamental to programming languages!).

Another big difference with traditional model theory is that, usually, people do not study the relationship between various models $F:\mathrm{Syn}(\mathbb P)\to\mathbf D$ for a fixed $\mathbf D$, because they differ in uninteresting ways. For example, when $\mathbb P$ is the simply-typed $\lambda$-calculus, the only choice you have in defining $F$ is to pick an object of $\mathbf D$ for each atomic type, and the specific choice is often irrelevant. So, contrarily to first-order logic, it is interesting to change $\mathbf D$ rather than pick a $\mathbf D$ and then let $F$ vary. In fact, when people say that they have a "model" of a programming language, usually they mean that they have a $\mathbf D$ with the desired structure/properties, not that they have fixed one specific $F$. This is another reason why denotational semantics has a different flavor than usual model theory, even though technically they are related via categorical logic.

By the way, all this (long!) digression was only to drive my point home: *denotational semantics is to programming languages what model theory is to first-order theories* (with all the necessary caveats). You do **not** need to know categorical logic in order to understand or study denotational semantics!

> **Comments:**
> **username_2**: At this level of abstraction, is this characterisation of model theory in PL saying anything more than: *we map syntax to something else*? (Yes, you get a bunch of coherence conditions from the categorical language, but they are trivial in general.) The beauty of (20th century) model theory is that the righthand side of the map from mathematical structures was fixed (ZF(C) set theory)! Moreover, on both sides we have first-order logic as unproblematic background.  So really, (20th century) model theory has been a study of ZF(C). PL has nothing comparably canonical, as of 2023.  
> **username_5**: Beauty is in the eye of the beholder, but the fact that, in traditional model theory, the target of the interpretation functor is fixed to the category $\mathbf{Set}$ is seen by many (starting from Lawvere) as an unnecessary limitation.  Mathematics is full of structures which are not bare sets, and allowing the target category of logical interpretations to vary is a very nice (or should I say very beautiful?) way of incorporating this into model theory.  
> **username_5**: Anyhow, more to the point that (I think) you are trying to make: I am (painfully) aware that there is no canonical definition of "programming language".  In the terms of my answer, *we do not have a canonical class of categories such that all programming languages induce categories of that class*.  This is in contrast with first-order classical logic, where we have, for example, Boolean pretoposes.  But this doesn't invalidate my answer: from Lawvere's functoral viewpoint, denotational semantics and traditional model theory are literally *the same thing*.  
> **username_5**: One last, side remark: characterizing model theory as the "study of ZF(C)" is at best debatable, and quite misleading if you ask me.  Maybe you are confusing with *set theory*?  Model theory uses set theory (and ZF/ZFC) as a foundation, just like any other branch of mathematics.  The important theorems of model theory do not say *anything* about ZF(C), albeit they might of course depend on it (like the compactness theorem, which uses choice).  But then again, lots of theorems of other branches of mathematics depend on ZF(C). PL theory too is ultimately based on ZFC...  
> **username_2**: I don't wish to start a normative discussion about what model theory is, let alone should be. In  my experience with mathematicians, when they learn about model theory, they do so from books like Hodges, Chang/Keisler, or Shelah, and those are, for better or worse, ZF(C)-centric. I'm sure username_0 can clarify what he means.  
> **username_2**: I think the situation is even more dire (please correct me if I'm wrong), the problem isnt just that we need to define the syntactic category Syn(ℙ) for each new language ℙ, but rather that for many (most) ℙ of interest, we don't really know *how* to define the very concept of  Syn(ℙ) in a categorical language. (Or, on the upside: there are plenty of interesting open research questions! And they have immediate practical relevance: as soon as you can express language properties to be preserved in a nice way, you get a recipe for program verification and tooling.)  
> **username_5**: @MartinBerger Yes, it's true.  Otherwise stated, there are tons of interesting programming languages for which it is not clear what it means to define a denotational semantics.  What I say in my answer makes technical sense only for the more "traditional" languages (which are mostly $\lambda$-calculus based).  In fact, I personally think that, for programming languages, the denotational approach is less useful than the operational approach!  
> **username_0**: (1/2) Thank you @DamianoMazza for your comprehensive answer! I understand (at a high level) that a "denotational model" is a functor from the appropriate syntactic category to **Set**, **Cpo**, or otherwise, and this generalizes the notion of a model of a first-order theory.  However, one of the lessons of first-order model theory is that it's the *structures*, not the formulas, that are first-class citizens. For example, by asking simple questions like *how many models are there of a given theory?*, we get, roughly, classification theory---a deep and subtle taxonomy of first-order theories.  
> **username_0**: (2/2) So--what can programs tell us about denotational structures?  Let also push back on the assertion that denotational models "in the same signature" differ in uninteresting ways. Take a first-order programming language in the signature of rings, with 0, 1, +, *, and =. If we interpret these operations in the natural numbers we get a Turing-complete programming language.  However, let us instead interpret these operations in, say, the algebraic closure of the finite field F_2 (an infinite field), Then we get a radically different model of computation (e.g., no universal program).  
> **username_2**: @DamianoMazza I agree that operational semantics has absolute priority, but I don't see an antagonism, I think of denotational semantics as being a research methodology for better understanding operational semantics, and, in particular, for developing reasoning principle (aka logics) for programming languages: the algebraic spirit makes us think in a certain direction, which is sometimes very successful, but has been failing for some forms of computation (e.g. parallel and timed computation), pointing to an incomplete understanding.  
> **username_2**: **(1/2)** @username_0  Taking the natural numbers and operations on them as given is, in general, not what we study in computer science.                                                                                                                         Instead, we assume that operations like addition or multiplication is something to be defined in the model of computation, not something already given *ex cathedra*.  
> **username_2**: **(2/2)** For example the Church numerals you mentioned up-thread are essentially unary encodings of numbers, leading to computationally inefficient arithmetic operations. In addition, Church numerals are not typable in, for example, the simply-typed form of the $\lambda$-calculus, you need something more powerful (e.g. System F). While the questions you suggest by analogy with classical model theory are natural, I'd say, they don't fit with the spirit of contemporary studies of computation: mathematical structures like rings, fields, etc should be explained as computation, not assumed.  
> **username_0**: Thanks. These last two comments really clarify things for me!  
> **username_5**: @username_0 as I underlined, beside the formal similarity given by the functorial perspective, model theory and denotational semantics are developed in very different ways and for very different purposes.  I don't know what kind of answer you are expecting for your question ("what can programs tell us about denotational structures"), but for sure you can't expect to transport your knowledge of model theory directly on denotational semantics.  
> **username_5**: @Siddarth about your second comment, you are misunderstanding what a "model of computation" is.  A programming language/model of computation doesn't change because you change its interpretation.  I don't know exactly what you have in mind with "a first-order programming language in the signature of rings", but either it will be Turing-complete or it won't, it's not a matter of how you interpret it.  And if it is Turing-complete, then your interpretation in the algebraic closure of $\mathbb F_2$ probably does not even exist (I can't say for sure without a precise definition).  

---

### Answer by username_3 on 2023-05-21. Score: 14

Let me amend Damiano's answer with more specific comments.

Terms of type `bool` are *not* logical statements. Expressions like `not (3 < x) or (x == y)` have the exact same status as expressions like `3 + 5 * x`, i.e., they are *term* formers. Also, equality is just a term former (yielding a term of type `bool`).

In fact, there are no logical symbols whatsoever in a programming language. A programming language is a calculus of *terms*. Its model theory is more like universal algebra than first-order model theory.

There is of course plenty of logic, but it is not part of the programming language itself. It's built *around* the language, in more than one way.

There are *equational theories* of programming languages which describe how a language behaves in terms of equations only (hence comparison with universal algebra). A typical equation is `(if True then A else B) = A`.

There are [*program logics*](https://xavierleroy.org/CdF/2020-2021/) which are custom-made formal systems with which we can state and prove properties of programs. Ordinary first-order logic is not appropriate, because it does not directly account for various phenomena, such as computational effects (intput-output, mutable state, exceptions) and non-termination. A typical example is [Hoare logic](https://en.wikipedia.org/wiki/Hoare_logic) in which formulas take the form $\{P\} \; c \; \{Q\}$, read it "if assertion $P$ holds (in current state) and command $c$ terminates, then assertion $Q$ will hold (in the resulting state)".

There are still other approaches that mix and match algebra, topology, category theory, and logic. It's a rich area.

Knowing first-order logic and model theory is very helpful as background knowledge, but they do not appear directly in programming language theory. You have to modify and generalize in various directions, and place emphasis elsewhere.

> **Comments:**
> **username_0**: Thanks for this answer! One question: if we take, e.g., an equational theory of programming languages, then that theory has to account for how to evaluate expressions like ''3 + 5 * x''. That's fine if these are all natural numbers, but what if 3, 5, and x live in some arbitrary ring? It would seem like the equational theory of this programming language would have to encode the entire atomic diagram of the ring in question. So we'd need as many equations as the size of the ring itself, in general. Do I understand you correctly?  
> **username_3**: I am not aware of anyone creating a programming language with an arbitrary ring. Presumably you would want one that is finitely presented. Also, an equational theory need not account for all aspects of the language – usually it is used as a reasoning tool. Evaluation can be described in some other way, in terms of operational semantics. One then checks that the equational theory is sound with respect to the operational semantics.  
> **username_0**: OK, an arbitrary ring is admittedly weird. Let's consider a simple nondeterministic program that recognizes if there is a path from vertex u to vertex v. Let vertex w be u; while w is not v, replace w by any neighbor of w. This program halts iff there is a path from u to v. It works over *any* graph. When we endow this program with an operational semantics, say, there seems to be a clear distinction between the "logical" steps (independent of the graph) and the "nonlogical" steps (picking a neighbor of the given vertex, dependent on the graph). Is this distinction not meaningful?  
> **username_3**: Yes, the distinction you are making is precisely the distinction between "pure" computation steps and the computational effect (the non-deterministic choice of a vertex). This is all well established in the mathematical treatment of computational effects. But where are you going with all this?  
> **username_0**: (1/2) Basically I'm interested in when the recursion theory of a structure looks "classical" and when it's different. For example, if we consider first-order programs over the natural numbers taking the increment (S, successor) and decrement (P, predecessor) operations plus equality tests as primitive, we get a normal Turing-complete model of computation. But if we lose S we get a drastically different model of computation (looks more like a complexity class). From a FOL perspective these structures are the same, as S is a definitional expansion of P. But their computation theories differ.  
> **username_0**: (2/2) Similar work has been done in the past, for example on the notion of "adequacy" by Lynch and Blum (https://groups.csail.mit.edu/tds/papers/Lynch/mst80.pdf). A collection of binary string primitives is adequate if all PTIME queries can be computed by programs making a polynomial number of calls to the primitives. In any case, I'm interested in programs operating over arbitrary first-order structures, and on classifying structures by how expressive these programs are. This naturally leads me to the questions I asked originally.  
> **username_3**: As far as I can tell there is a rather large divide between your interests and experience on one hand, and what we're trying to convey on the other. But it's hard to pin it down. Practically all programming languages are Turing-complete – but that is a very *un*intersting observation from the PL perspective. (Of course there are studies on how to design a PL that matches precisely a given complexity class, etc., but overall that's not the sort of thing that PL design and semantics is about.)  

---

### Answer by username_4 on 2023-05-25. Score: 2

Models in some semantic framework are essentially a mapping from synthetic objects to some other domain of object. In the sematic domain we typically identify or take as equivalent a bunch of synthetic objects. We do this because we know things about the sematic domain that we can use to learn things about the synthetic objects.

At the one extreme, one can map a program to the function that it computes over the standard model. Two programs are the same if they compute the same function. That is not a very useful semantics, we are often interested in also how they compute it. (I assume we at least care about what function the program is computing.)

At the other extreme, we can take the synthetic objects themselves as the semantic domain. That is not a very useful semantics.

Between these two there are many possibly semantic domains that one can use. Denotational semantics (with emphasize on s) are some very useful semantic domains. Note that we don't just care about the objects themselves but the relationships between them.

However, keep in mind that things are not as clean as they may look at first. Denotational semantics works great for languages that are nice (functional programming), but you will see someone taking about the denotational semantics of a common programming language like Go or C or Java or JavaScript or Python. Similarly for languages like Prolog.

Having a semantic domain also is not sufficient for model *theory* in the sense of logic. We can construct models but model theory cares more about nonstandard models typically than standard model, because that is what is related to provablity in theories. We don't need just a syntax with construction rules, we need axioms about what can be said about those objects that are inherently incomplete. I want to go to the nonstandard model of reals with infinitesimals and show something holds there and then transfer that back to standard reals using the fact that the language and the theory cannot distinguish between these two. In programming the languages are typically too powerful. The typical model theory deals with relatively simple cases that are not strong enough to express computation. Almost all interesting programming language are expressive enough to write a Turing machine simulator. The model theory of arithmetic theories like PA might be more inline from the perspective of complexity they have. Even there, one needs to not use the True Arithmetic theory but some limited set of axioms. When taking about programming language, the theory people typically use is all of mathematics. These are I think partly responsible for why we don't have a model theory of programming languages in the sense of logic.


---

### Answer by username_0 on 2023-05-24. Score: 1

Thanks to everyone! I'm just going to summarize my takeaway from the helpful responses and comments above targeted towards someone in mathematical logic wondering the same thing as I did. Please let me know if anything here is inaccurate. **Update:** Seems like it is, please see the comments below!

**(1) There is no distinction between logical and nonlogical symbols.** That is because programming languages come with a *fixed* set of data, and moreover, the semantics for the functions and relation symbols over that data is tied into the semantics of the whole programming language. E.g., if your programming language contains the symbol $+$, then your semantics has to account for $+$.

This is not to say that *in principle* you could not study programs in an arbitrary signature $L$ which take semantics over any $L$-structure. It's just not part of the enterprise of the theory of programming languages.

**(2) Programs, not structures, are first-class citizens.** Since we don't consider $L$-programs operating over arbitrary $L$-structures, we don't tend to define properties of, or otherwise classify, structures themselves.

**(3) The semantics of programs and first-order formulas have a common generalization.** Despite the differences in attitude and orientation between PL theory and model theory, they share a common categorical setting. (See Damiano's answer for an elaboration of this.)

> **Comments:**
> **username_3**: I only agree with (3). The other two are ... strange?  
> **username_5**: 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.  
> **username_5**: 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.  
> **username_5**: 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!  
> **username_5**: 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...  
> **username_0**: Thanks @DamianoMazza! I am hopeful that understanding this example will get to the core of my misconception. Why must the third argument to $f$ be an nno? Indeed, I was imagining $f : A^3 \to A$, *not* $A^2 \times \text{nat} \to A$. The definition of $f$ is not by primitive recursion on $z$.  
> **username_5**: Yes, you are right, the definition is not by primitive recursion.  My understanding of it was that you were using the usual inductive definition of the type $\mathsf{nat}$ of natural numbers, so your definition is by cases (you test for zero and then you do something based on that test).  Primitive recursion uses the inductive structure of $\mathsf{nat}$, but it was a mistake for me to mention it.  
> **username_5**: The fundamental point remains: you are just considering an equational theory over the signature of semirings.  That's *not* a programming language.  No one who studies programming languages takes a random equational theory and calls it a "programming language", referring to its terms as "programs".  Programming languages must, in one way or another, have to do with computable functions, you must be able to represent computation with them.  In which programming language is your example written, and how does this programming language compute?  
> **username_5**: In fact, now that I look at it, your definition of $g$ and $f$ does not even seem to be representable as an equational theory.  I don't know how to make your definition by cases fit into an equational theory.  It can certainly fit a more elaborate kind of theory (certainly a first-order theory, for example).  But then, again, you are just doing usual logic and model theory, so all of a sudden I don't understand your question anymore...  
> **username_0**: The semantics of this specific example: given any structure $M$ in the signature of semirings, consider the family $X$ of partial functions $M^3 \to M$ partially ordered by extension ($\sqsubseteq$). The right-hand-side of the definition of $f$ defines a monotone operator on $(X,\sqsubseteq)$. Take its least fixed point; that is your definition of $f$.  
> **username_0**: In general, given any system of recursive equations in the signature of semirings, where the right-hand-sides are terms built up from the semiring operations, cases, and recursive calls, we can endow it with a least fixed-point semantics in a similar way. In what sense does this fail to be a programming language?  
> **username_5**: Unfortunately, there is no formal definition of "programming language", so it's impossible to say why this isn't one :-D  If I have to point out a reason, it would be that the syntax of this system is devoid of an operational semantics:  given a "program", how do you evaluate it, independently of the semantics?  Another, related reason: I do not see how to encode in this "programming language" usual computation on some kind of finite structure (integer, strings), directly in terms of the syntax, as one may always do with usual programming languages.  
> **username_5**: This doesn't mean that what you do is meaningless!  It just means that it's difficult, if not impossible, to relate/adapt what people usually do in PL theory to your setting, also for what concerns denotational semantics.  
> **username_0**: I can certainly give a big-step semantics, and I am pretty sure there is no obstacle to a small-step semantics, but I'd have to think about that. (Both, of course, depend on the structure $M$!) But certainly we don't automatically have integers, strings, etc Anyway, thanks for the clarification, this was very helpful!  

---

