Explaining "Implementing a specification"
I'm currently looking into the notion of "implementing according to a specification" in engineering, and in particular in software development and what we engineers might mean with that phrase explained in some formal way.
I personally have been seeking a fundamental definition of "data" or "information" in order to define certain mathematical notions pertaining how different structures relate in terms of their "information". But a recurrent theme in my study of logic has been that there is no "one formal system to rule them all". This is a view espoused by some people, at least, but not by everyone. It can be given as a reminder to not get carried away by seeking the "best" definition, but instead, allow yourself to work with frameworks that you know of, and explore how they reflect the subject matter differently. Hence, the common phrase "all models are wrong, but some models are useful."
I've been looking at both meaning theory
Commonly referred to as 'semantics'?
and metaphysics as possible frameworks. When we specify something, we're really just giving a description of some possible kind of (desired) object.
So far, this reminds me of type theory and of formal logic, as formal languages we use to specify the properties of a structure or object. The specifications, or "theories", we write, do not have to determine a structure uniquely. They can describe a class of structures/objects. We may also not know in advance if the theory has a model, hence, if the described thing exists.
The process of implementing is then to find such an object, possibly by arranging other objects into a new whole (i.e. building something).
In mathematics, I think this would be called constructing such an object. But when you talk about "arranging other objects", I think of "compositionality", which some say is the central idea in category theory: just as groups are the canonical structure for modeling symmetry, category theory is the canonical structure for studying compositional phenomena; which happen to be very common. Just as Awodey says, "Just as group theory is the abstraction of the idea of a system of permutations of a set or symmetries of a geometric object, category theory arises from the idea of a system of functions among some objects... category theory was invented as a way of studying and characterizing different kinds of mathematical structures in terms of their “admissible transformations"... Functions are everywhere! And everywhere that functions are, there are categories. Indeed, the subject might better have been called abstract function theory.” (Steve Awodey, "Category Theory", 2010).
Similarly, Spivak says, "Category theory is unmatched in its ability to organize and layer abstractions, to find commonalities between structures of all sorts... modern human intuition seems to include a pre-theoretical understanding of monoidal categories that is just waiting to be formalized. Is there anyone who wouldn’t correctly understand the basic idea being communicated in the following diagram?
(David Spivak, "Seven Sketches in Compositionality", 2018)
Here is a book about categorical systems theory:
"Categorical Systems Theory". David Jaz Myers. 2023. http://davidjaz.com/Papers/DynamicalBook.pdf
Model theoretic approach?
In the semantics of logic and in model theory, it's my understanding that we can define some theory as a language that extends first order logic with some new symbols, and give the theorems of that theory, and then find models of that theory by assigning what actual objects are being talked about.
That sounds accurate to me. I similarly had my first inkling of the idea of model theory when I considered that a fundamental definition of what a "language" is (coming from a background in linguistics) is simply any "representational system" where the elements of one system are used to "represent" the elements of some other system. And this is what model theory does.
However, to be precise, we do not "define a theory as a language", but rather, we define a language, and a theory in that language is a subset of the well-formed formulae of that language.
And when you say "and give the theorems of that theory", I'm also inclined to mention some common intuitions that turn out to be inaccurate when one studies model theory on a technical level. When you present a signature, a structure, a map from a signature to a structure, and then select a set of formulae, you determine a theory. The deduction rules immediately imply all of the formulae which are deducible from the axioms you chose.
I mention this, because I have found it to be an important detail to be aware of, because I am also considering the exact same question as you: first-order theories appear to lack a dynamism that reflects how humans think, procedurally and sequentially. There is no formal mechanism in the deduction rules to "introduce a new symbol into a signature and provide it with a definition", during the process of deriving theorems. Instead, as you said, we extend the signature; and there are ways of showing how one theory contains another. So, these ideas are expressible, but on a conceptual level, they feel different than the human intuition of "defining something ad hoc, on the spot".
It seems like this kind of assignment of objects to the variables and constants of a theory in model theory (or just an interpretation of a first order logic formula) is a precise way to describe what happens when we "implement according to a specification" (with the theory as the specification, and the assigned objects as the implementation).
Yes, to an extent. The word "implement" has an active, creative connotation. What is philosophically interesting about model theory is that (I think) we often do not actually "create" things when we define them - we specify things which are taken to already exist, in the ambient set theory. This is a paradigm that I am in the midst of acclimatizing to myself. Kristian Berry exposed me to the philosophical terminology in re / ante rem, regarding this question: when we define mathematical structures, are we "generating" something new, on the spot - or are we simply specifying something that already exists?
It is quite important to remember this; when defining functions, for example. Up until recently, I always thought of functions as being inherently "constructive" phenomena. I thought that there were "rules", which took things, operated on them, and suddenly, produced "new things". In fact, this is the common analogy people are given, in elementary school mathematics.
But in set theory, functions don't "create" anything. They can't. We can only "define" a function if the elements in its image already exist, as elements in its codomain, in our world of sets. These leads to a quite noteworthy paradigm shift, when we see the common way of definition a function. When one says,
Let f be a function from X to Y,
such that f(x) = x + 2.
one might commonly think the second statement, the equation, is what gives the function its "mechanism of action", and the first statement, the domain and codomain, is possibly contextual information. Actually, the converse is true: for any two sets, we can claim something "is a function on those sets", so long as it holds under the definitional properties of "a function". When we add an equation like "f(x) = 2" to the set of formulae describing "some set", we are further constraining the possible models. Sometimes this determines a unique set, and sometimes it still has a class of functions as its model - i.e., the class of functions with a certain property. So, when we identify a function with an equation, like f(x) = x2, this is just because that collection of formulas happens to determine a unique model. Thus we say "the function such that f(x) = ...", rather than "a function such that...".
This relates to concepts like "inductive definitions" and constructive mathematics, which relates to your question of what we mean by "instantiating a specification", that I won't go into right now.
However, we frequently build systems up in layers. As an example:
- Propositional logic gives the rules for the connectives ∧, ∨ →, and ¬.
Yes, or, in order to be more precise (since this helps so much, once you start grappling with these questions): "Propositional logic" can be defined as a set of equations (an "equational theory") written in a language L with those symbols in its signature. (And to be fair, the choice of symbolic representative is not the important part, but the system of equations governing their mutual interrelationships.)
- Boolean algebra gives a mathematical model of propositional logic
Yes, sort of. A "Boolean algebra" can be defined as any model of the theory of Boolean algebras. I think it is true to say that the theory of Boolean algebras and the theory of propositional theories are logically equivalent (i.e., a theory of a single proposition is isomorphic to a Boolean algebra with one generator).
- Claude Shannons "Switching circuits" give a mechanical model of boolean algebra
- Transistor circuits give a model of switching circuits
This I have not learned anything about.
Is model theory a good place to look at formalizing "implementing a specification"?
Yes, because it will teach you how to think with mathematical precision! After studying logic for a year, I feel I have developed a kind of "mathematical literacy" where learning new mathematical concepts is much easier, because I can break down new concepts into fundamental definitions. Trying to learn machine learning algorithms is much easier when you can write a complete theory of them from scratch, and understand important nuances of how "functions", "real numbers" and "infinite sets" are actually defined. I learned from this textbook:
"Mathematical Logic". Heinz-Dieter Ebbinghuas, et al. 2021. https://link.springer.com/book/10.1007/978-3-030-73839-6
First-order logic, and set theory, have helped give me a foundation from which to learn other mathematical concepts. However, type theory is paradigmatically different, yet can define the same concepts. I am currently studying type theory.
How might I give an account of building up these layers of implementations?
This is a bigger question.
I currently recommend a practical method of writing out your thoughts on something in natural language, and then repeatedly rewriting the sentences in more and more precise form, and breaking them apart into separate assertions.
For example, here's a random sentence from the front page of Wikipedia:
The stonework of its pointed arcades and fluted piers bears pronounced mouldings and carved capitals in a foliate, "stiff-leaf" style.
I will "iteratively" try to translate and decompose this sentence into a theory in first-order logic.
- The stonework of something's pointed arcades and fluted piers bore at time t pronounced moulding and carved capitals, which were in a foliate and "stiff-leaf" style.
- There is something. At time t, it had stonework. Its stonework had pointed arcades. Its stonework had fluted piers. Its pointed arcades and fluted piers bore pronounced mouldings, and they bore carved capitals. Those carved capitals were in a foliate and stiff-leaf style.
- Let there be a thing X. X has stonework. (
hasStonework(X)). "Stonework" means something is made of carved stone.madeOfCarvedStone(X). "Made of carved stone" means it was made of stone. Carved stone is a subtype of stone. Let's say "madeOf()" is a relation between a thing, and a material. Then we can say madeOf() is a relation on a set of Things and a set of Materials. Therefore madeOf is a subset or equal to the set-theoretic product of the set Things and the set Materials. Furthermore, everything is made of something (left-totality); but not everything is made of only one thing (which would be right-uniqueness). Thus, madeOf is not a functional relationship. Instead, it is many-to-many.
We can go on like this. Then we can code it up in a programming language. I am currently learning Haskell and Coq, but since the logic I know best is first-order logic, I may have to research which proof assistant is best for first-order theories. However, it turns out that different logics have different properties regarding how they can be automated. Right now, I am learning about how "regular logic is the most expressive logic" for which you can "compute an initial model" (I think). This means that, if we want to take advantage of very useful computational automation, construction, and inference over a "specification", we have to find a way to force our specification into regular logic - where the only permissible expressions are existential Horn clauses, of the form ∀ x, y, z, ... [φ0(...) ∧ ψ1(...) ∧ ...] → ∃ p [ψ(...)].
Yes, model theory is a good starting point to study the relation between "specifications" and "structures",
but especially with the help of categorical logic, which gives us a broad view on the relationships between different kinds of logic - for example, what they can and cannot express - and different kinds of structures.
Category theory actually subsumed model theory, in a way. Model theory divided the world, in quite a metaphysical, even Platonist way, into the realm of human thought, and the realm of mathematical truth; where we use the metalanguage of natural language to define:
- a formal system we take as our formal language
- an envisioned world of "inherent mathematical structures"
and then we study the interaction between these two things.
As one increasingly formalizes and abstracts, of course, the formal language itself becomes just another mathematical structure: now we are just studying structural relationships between different structures. However, in a way that I am still learning, sets still play an important role in category theory: very often, one "represents" a category, as a description of a structure, via a functor into the category of sets. In the context of categorical data science, an "instance" of a "schema" (which sounds highly analogous to your "implementation" of a "specification") is a functor from a category into the category of sets.
More broadly, I think your question is just about mathematical modeling. And this is a wide, active field. If you want to try your hand on mathematical modeling, I suggest you begin to study logic. There are many different types of logic, which are used in formal specification, such as regular logic, and computer programs used to implement them, such as TLA+, Prolog, and others.