14
$\begingroup$

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?

$\endgroup$
13
  • 2
    $\begingroup$ 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. $\endgroup$
    – Ilk
    May 21, 2023 at 8:35
  • 3
    $\begingroup$ 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. $\endgroup$ May 21, 2023 at 9:32
  • 3
    $\begingroup$ (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. $\endgroup$ May 21, 2023 at 9:33
  • 4
    $\begingroup$ @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. $\endgroup$ May 21, 2023 at 9:37
  • 3
    $\begingroup$ @AndrejBauer Steve Vickers once said: a truth is deep if its negation is also true. $\endgroup$ May 21, 2023 at 9:41

4 Answers 4

13
$\begingroup$

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 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 $\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!

$\endgroup$
15
  • $\begingroup$ 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. $\endgroup$ May 21, 2023 at 10:06
  • 1
    $\begingroup$ 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. $\endgroup$ May 21, 2023 at 13:52
  • 1
    $\begingroup$ @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. $\endgroup$ May 24, 2023 at 12:32
  • 1
    $\begingroup$ (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. $\endgroup$ May 24, 2023 at 12:45
  • 1
    $\begingroup$ (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. $\endgroup$ May 24, 2023 at 12:45
14
$\begingroup$

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 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 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.

$\endgroup$
7
  • $\begingroup$ 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? $\endgroup$
    – Siddharth
    May 23, 2023 at 18:36
  • $\begingroup$ 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. $\endgroup$ May 23, 2023 at 19:50
  • $\begingroup$ 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? $\endgroup$
    – Siddharth
    May 23, 2023 at 22:54
  • $\begingroup$ 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? $\endgroup$ May 24, 2023 at 12:00
  • 2
    $\begingroup$ 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 unintersting 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.) $\endgroup$ May 24, 2023 at 21:06
2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.)

$\endgroup$
14
  • 1
    $\begingroup$ I only agree with (3). The other two are ... strange? $\endgroup$ 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$ 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$ 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$ 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$ May 25, 2023 at 5:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.