7

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've been looking at both meaning theory and metaphysics as possible frameworks for giving a more detailed account. (I work as an engineer but have an interest in philosophy).

When we specify something, we're really just giving a description of some possible kind of (desired) object. The process of implementing is then to find such an object, possibly by arranging other objects into a new whole (i.e. building something).

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. This seems like a precise way of doing specifications.

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 spec, and the assigned objects as the implementation).

However, we frequently build systems up in layers. As an example:

  • Propositional logic gives the rules for the connectives /\, \/, -> and ~
  • Boolean algebra gives a mathematical model of propositional logic
  • Claude Shannons "Switching circuits" give a mechanical model of boolean algebra
  • Transistor circuits give a model of switching circuits

Is model theory a good place to look at formalizing "implementing a specification"? How might I give an account of building up these layers of implementations?

Edit:

I think what I'm really looking for with the layer example is a composition of scientific theories, as discussed in this article:

https://plato.stanford.edu/entries/structure-scientific-theories/

14

4 Answers 4

1

To implement a specification is to optimize a function. The specification corresponds to a function across all possible objects, which for each object gives a number that indicates how well that object fits the specification.

When the function has a binary output ("does implement" or "does not implement"), we can also say that it is a constraint satisfaction problem. In practice the function often involves degrees of fit. For example, an engineering diagram might specify that a certain pipe should have a circular cross-section. The physical object will never have an exactly circular cross-section, so the function can say how close it comes. The diagram might give a precise tolerance, to make the function output binary again - but there are still likely to be vague border cases where it's hard to say if it's exactly in tolerance or not. In any case, we'd often like to distinguish between a pipe that is slightly warped (slightly out of spec) and a pipe that is completely non-functional, and the way to represent this is with degrees of fit.

The specification corresponds to a function that we optimize, but the specification itself is not that function. The specification is a document that must be interpreted to obtain the function. To do this we must have an interpreter, such as a human being or perhaps an automated verifier. The interpreter can be modeled as a function of two parameters: I(S, O), where S is the specification document and O is the object, and the output is the degree of fit. Holding S constant (currying I) gives us the specification function of O described above. The specification function is the meaning of the specification.

The interpreter themselves has internal variables, which influence the interpretation; humans have neurons with connections of varying strengths. So really we might say that I is a function of 3 parameters: I(V, S, O), where V is the internal state of the interpreter.

Interpretation is not a singular, instantaneous act. It occurs over a period of time. If there is a two-hundred-page engineering document, it will take a human interpreter a long time to decide how well a given object implements it. And on two different occasions, the interpreter might give two different results. This can be partially represented with variation in V between the two occasions. But it may also be due to random factors, or to outside influences that might distract the interpreter. To make sense of this we'd like to think of the interpreter as an ideal, that ideally would be always consistent. I(V, S, O) is a simplified, idealized model of messy reality. We may approach the ideal by asking what result the interpreter would give if they had unlimited time to study S and O and access outside resources, so they would give the most well-thought out possible answer.

A human interpreter of such a document would give, not just one number, but a description of how well the object fits the specification for each of the many sections of the specification. So we might think about making I(V, S, O) a multidimensional score, with one score for each section. But we don't need this because this information is already contained within the scalar output of I(V, S, O) as it varies across O. Suppose that the specification has a pipe, a valve, and a pump. Suppose the pipe is the component that's out of spec and the other two are fine. Then, by altering only the pipe part of O, we could improve I(V, S, O), whereas by altering the valve or pump we can't improve the score. That fact gives us our subscore for the pipe.

3
  • This seems like a good formalization of the relation between a specification and an implementation but it doesn't to me seem to explain the layering at the end of my post. Commented Oct 23 at 14:13
  • 1
    @RasmusKällqvist Well, you could have specifications for specifications. Then you could have like I(V, S1, S2) saying specification S2 is an implementation of specification S1, and then I(V, S2, S3) saying specification S3 is an implementation of specification S2, and so on.
    – causative
    Commented Oct 23 at 17:01
  • Hm, how would that work in the other direction? Usually we might start with some high-level theory, and then iteratively "reify" it, like I did in the example in the opening post, with propositional logic being step-by-step implemented down to transistor circuits Commented Oct 23 at 23:39
1

Implementing a specification is the common task in software engineering.

A typical example is the implementation of an accounting system for a business company. E.g., an automotive company starts a project for an IT-system which computes and distributes each month all invoices for the cars they selled.

  1. After the company has made a requirements analysis for the accounting system a group of business consultants in cooperation with the accountants of the company design the accounting system in a domain specific language using concepts like customer, order, car, invoice, price list, etc.
  2. IT-consultants transform this textual specification into a formal language like UML (Unified Modeling Language) which uses several formal models like datamodel or class model, usecases, and process models like BPMN (Business Process Model and Notation).
  3. Eventually, a group of programmers generates and codes the UML-specification into a programming language like java: They implement the specification as the required IT-system.

One may call the method scetched above a model theoretic approach. Its degree of formalization depends on the problem under consideration. For a real world problem like above I consider the approach semi-formal: Its degree of formalization depends on how much final code can be generated from the UML model.

1

Vocational phrases are rarely simple to convert into philosophical ones.

Based on my engineering experience, I would say that capturing the concept of a specification is a good match for model theory. The spec defines a model such that all implementation of that model can be used in a way consistent with that model. However, actually implementing is an action, and there's some ambiguity based on context. In some situations, one might say that an implementation is written according to a specification, just implying that the author claims it is an implementation. However, in other situations, an author who implements a specification may be obliged to prove that their implementation is indeed an implementation of that model. Such a proof is typically more in line with proof theory than it is with model theory.

0
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?

lemon-meringue-pie

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

  1. 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.
  2. 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.
  3. 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.

1
  • Thanks for the very insightful commentary! You are correct about the technicalities of languages and theories etc., and probably I should just bite the bullet and study model theory proper. (I already am familiar with both propositional and first order logic) Commented Oct 23 at 15:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .