A Category of Systems

 Exploring the consequences of Systems & Cybernetics in Engineering
Author Tom Westbury License Creative Commons Licence

Type theory as a basis for MBSE
Date 2020-11-29
Tags

This post is a re­sponse to a flurry of ac­tiv­ity in sys­tems en­gi­neer­ing acad­e­mia around us­ing cat­e­gory the­ory as a the­o­ret­i­cal ba­sis for SysML. A num­ber of pa­pers ex­plor­ing this idea have ap­peared in th lit­er­a­ture re­cently and as some­one who is pas­sion­ate about cat­e­gory the­ory and sys­tems en­gi­neeer­ing, I can’t help but con­tribute my thoughts on the mat­ter. In this post I’d like to ex­plore the ba­sics of cat­e­gory the­ory and the closely re­lated type the­ory and ex­plain the power that this the­o­ret­i­cal ba­sis could bring to model based sys­tems en­gi­neer­ing.

What is Cat­e­gory The­o­ry?

Cat­e­gory the­ory is a field of math­e­mat­i­cal study that has re­ceived a lot of at­ten­tion in re­cent times (and the in­spi­ra­tion for this blog’s ti­tle). It is, fun­nily enough, the study of cat­e­gories. Math­e­mati­cians have used cat­e­gory the­ory to dis­cover many ab­stract the­o­rems about the un­der­ly­ing struc­ture of maths; cat­e­gory the­ory is one of the most ab­stract fields of math­e­mat­i­cal study, so prov­ing a the­o­rem in cat­e­gory the­ory means that the­ory is now proven across many other fields of math­e­mat­ics.

So what is a cat­e­go­ry? Let’s ex­plore that now. A cat­e­gory is a col­lec­tion of two types of thing: ob­jects and mor­phisms. Ob­jects are points with an iden­ti­fi­er. Mor­phisms are ar­rows that go be­tween two ob­jects. Ob­jects have no struc­ture what­so­ev­er; they’re ba­si­cally just la­bels for the ends of mor­phisms. On top of these things there are also a few rules:

By play­ing within these rules and con­struct­ing var­i­ous cat­e­gories, math­e­mati­cians have found ways to con­struct cat­e­gory the­ory ana­logues of many dif­fer­ent fields of maths which has en­abled them to dis­cover sur­pris­ing links be­tween sup­pos­edly un­re­lated fields. For more on the ins and outs of cat­e­gory the­o­ry, see Bar­tosz Milewski’s Cat­e­gory The­ory for Pro­gram­mers. Hold this sec­tion in your head for now as we’re go­ing to ex­plore the cur­rent state of spec­i­fi­ca­tion in UM­L/SysML.

Prov­abil­ity in mod­els

UML (and there­fore SysML) are not com­plete spec­i­fi­ca­tion lan­guages. This point is made by the re­searcher Jordi Cabot in his OCL tu­to­r­ial. Tl­dr; UML and SysML can only de­fine the struc­ture of the sys­tem you’re de­sign­ing. A con­straint lan­guage is re­quired to rea­son about a UML model and to give a com­plete spec­i­fi­ca­tion of a sys­tem. For ex­am­ple, we could “prove” a model through ex­haus­tively test­ing the mod­el. Though this is still a valid ap­proach to ‘prov­ing’ a mod­el, it is some­what time con­sum­ing and of­ten in­com­plete; their may be a set of con­di­tions that you may not have tried that would con­tra­vene the con­straints. As Eds­gar Dijk­stra said:

Pro­gram test­ing can be used to show the pres­ence of bugs, but never to show their ab­sence!

This is­n’t just a prob­lem with UML though, it ac­tu­ally cov­ers pretty much all pro­gram­ming lan­guages. To solve this prob­lem, it has been a goal for many years in in­dus­try to use the lan­guage of logic to rea­son about pro­grammes. The holy grail has been to pro­duce code that is math­e­mat­i­cally proven to not be able to fail in cer­tain ways. If you can en­code the con­cept of ‘For All’ into a true state­ment about your code, you can prove that cer­tain prop­er­ties hold for all pos­si­ble in­puts for ex­am­ple. The ben­e­fits to such tech­niques to func­tional safety and cy­ber se­cu­rity are ob­vi­ous. Lan­guages that al­low pro­gram­mers to for­mally rea­son about code have been avail­able for a while. No­table ex­am­ples are VD­M-SL, Z no­ta­tion, OCL and Spark Ada. These lan­guages have one thing in com­mon that may have led to their lim­ited adop­tion in in­dus­try: they’re all based on set the­o­ry.

Sets and Logic

Set the­ory (or more for­mally Zer­melo-Frankel Set The­ory with Choice (ZFC)) is a foun­da­tional the­ory of maths; that is to say that all proven maths can be proven within the ax­ioms and ob­jects pre­sented by ZFC. The base ob­jects of ZFC are sets and pred­i­cates. A set is a unique col­lec­tion of ob­jects that can be rea­soned with us­ing logic and a pred­i­cate is a log­i­cal state­ment that rea­sons about sets and other pred­i­cates. There­fore set the­ory has two parts, sets and log­ic. Z and OCL are good ex­am­ples of lan­guages that are based on ZFC log­ic. There­fore, ZFC set the­ory has this ba­sic di­chotomy built into it, the con­struc­tion of sets and rea­son­ing in ZFC logic are two dif­fer­ent lan­guages. This is also com­pounded by the fact that OCL has been found to be log­i­cally in­con­sis­tent. To use these lan­guages, first you must write your code or build your model and then you must use a seper­ate lan­guage to rea­son about it.

Cor­rect by con­struc­tion

To find our­selves an al­ter­na­tive to ZFC based lan­guages, we’re go­ing to have to ex­plore a dif­fer­ent in­ter­pre­ta­tion of the idea of proof and truth. For this, we will turn to con­struc­tivism. Con­struc­tivism is a school of math­e­mat­i­cal thought that states that to prove a the­o­rem, you must pro­duce ev­i­dence of that the­o­rem. In par­tic­u­lar, you can­not use the law of the ex­cluded mid­dle in a con­struc­tivist proof. This is be­cause a con­struc­tivist proof will only al­low you to state some­thing as true if you can pro­vide an ex­am­ple that sat­is­fies your pred­i­cate.

Con­struc­tivism was seen as a bit of a fringe idea un­til Haskell Curry dis­cov­ered a cor­re­spon­dence be­tween con­struc­tivist logic and pro­gram­ming. Curry dis­cov­ered that the stan­dard op­er­a­tors of con­struc­tivist logic had ana­logues in the typed lambda cal­cu­lus. This meant that any con­struc­tive log­i­cal propo­si­tion can be con­verted into an equiv­a­lent com­puter pro­gramme and vice-ver­sa. This ef­fec­tively showed that con­struc­tivist maths cor­re­sponds with maths that is com­putable; if you can prove a the­o­rem con­struc­tive­ly, you can also com­pute all things that sat­isfy that the­o­rem. A few cor­re­spond­ing con­cepts be­tween logic and pro­gram­ming are shown in the ta­ble be­low:

Log­i­cal Con­cept Sym­bol Pro­gram­ming Con­cept Sym­bol
Im­pli­ca­tion ⇒ Func­tion Ar­row ->
Con­junc­tion ∧ Prod­uct Type (tu­ple) (a,b)
Dis­junc­tion ∨ Sum Type Ei­ther
Truth ⊤ An in­hab­ited type e.g. Int
False­hood ⊥ The empty type Void

This means that any type de­c­la­ra­tion in a pro­gram­ming lan­guge with a com­pat­i­ble type sys­tem (such as Haskell or Idris) can be read as a log­i­cal propo­si­tion. The type sig­na­ture of a generic func­tion a -> b can be read as “If you can give me proof of a, I can give you back a proof of b. Here are some func­tion de­c­la­ra­tions and their mean­ings to il­lus­trate the point:

 im : Ei­ther a b -> c

If you can give im proof of a or proof of b, im can give you proof of c

 con : (a, b) -> c

If you can give con a proof of a and a proof of b, con can give you a proof of c. In­ter­est­ing­ly, this is equiv­a­lent to the type a -> b -> c:

 curry : ((a, b) -> c) -> a -> b -> c
 un­curry : (a -> b -> c) -> (a,b) -> c

This process of us­ing this equiv­a­lence is known as cur­ry­ing af­ter Haskell Cur­ry. It be­comes in­cred­i­bly use­ful for reuse pur­pos­es. I’ll ex­plore us­ages of cur­ry­ing in SysML in a fu­ture blog post. For now, we can ap­pre­ci­ate that it is some­what of a tau­tol­ogy; the log­i­cal in­ter­pre­ta­tion of a -> b -> c is: If you can give me a proof of a, I can give you a proof of b -> c.

 efq : Void -> a

If you can give efq a mem­ber of the Void type, efq can give you any­thing. The log­i­cal prin­ci­ple of ex­plo­sion. Ef­fec­tive­ly, this state­ment means that you can prove any­thing true if you start from a lie.

not : a -> Void

If you can give not a value of a, not will give you a value of Void. Since this is is im­pos­si­ble, not rep­re­sents the log­i­cal Not op­er­a­tor: be­ing able to ob­tain a value of a -> Void (find a map­ping from an in­hab­ited type to the empty type) is an ab­surd propo­si­tion. There­fore, if a con­tains val­ues, Not a will not.

Some pro­gram­ming lan­guages (Such as Idris, Coq and Ag­da) give you a re­ally use­ful type called equal­ity that al­lows you to prove that two propo­si­tions are equal:

Equal­ity : a -> b -> Type where
  re­flex : Equal­ity x x

This state­ment uses a new no­ta­tional se­man­tic, the where key­word, that tells us that re­flex is a con­struc­tor func­tion for Equal­ity. Equal­ity it­self is a type that states: If you can give me two val­ues one of type a and one of type b, I can give you back a new type, but only if the two val­ues that you give me are the same (The re­flex con­struc­tor is only de­fined for val­ues that are the same). There­fore, type the­ory gives us a way to ex­press equal­ity in type sig­na­tures within pro­grammes! You may have al­ready no­ticed the use of equal­ity (in its sym­bolic guise ‘=’) in the ear­lier rules for cat­e­gories.

We al­ready know that UML (e­spe­cially the ex­e­cutable sub­set fUML) gives us a spec­i­fi­ca­tion for struc­ture and be­hav­iour, adding the ad­di­tional abil­ity to ex­press propo­si­tions in UML with­out hav­ing to re­sort to the com­plex­i­ties of OCL would mean that we would­n’t have to learn two lan­guages to fully spec­ify our de­signs and do­main spe­cific lan­guages in MB­SE.

A type the­o­ret­i­cal ba­sis would mean that a mod­el­ling lan­guage could spec­ify both struc­ture and con­straints in one uni­fied pack­age!

In­ter­est­ing­ly, whilst re­search­ing this post, I stum­bled across a pa­per on­line where re­searchers had used Haskell to en­code both the struc­ture of UML mod­els but also a con­straints lan­guage. The pa­per can be found here. Al­though this pa­per does not touch on the points in this post, it does show the power of a lnguage like Haskell to en­code both lan­guages.

So where does cat­e­gory the­ory fit into all of this?

It just so turns out that there is a strong cor­re­spon­dence be­tween type the­ory and cat­e­gory the­o­ry: type the­o­ries are the in­ter­nal lan­guages of cat­e­gories. This means that the ob­jects of a cer­tain cat­e­gory cor­re­spond to the types in a cer­tain type the­o­ry. The keen-eyed reader will prob­a­bly have no­ticed how the no­ta­tion that I used for mor­phisms in the sec­tion on the rules for cat­e­gory the­ory was the same no­ta­tion used for type sig­na­tures in the logic sec­tion; that’s be­cause they are the same thing!

Cat­e­gory the­ory is miss­ing a key part of what makes type the­ory though: the abil­ity to work with el­e­ments of types. Tech­ni­cal­ly, there is a way in cat­e­gory the­ory of in­spect­ing which el­e­ments ex­ist in which types but its far eas­ier to play with these el­e­ments within a type the­o­ry.

The holy trin­ity

The ap­proach to maths and com­puter sci­ence of us­ing propo­si­tions as types, pro­grammes as proofs and us­ing cat­e­gory the­ory & type the­o­ries to­gether is known as com­pu­ta­tional trini­tar­i­an­ism. Cat­e­gory the­ory can only give us the “propo­si­tions as types” part of the equa­tion but once we get type the­ory in­volved, we can ex­press pro­grammes that can act as proofs!

There­fore, fo­cussing solely on cat­e­gory the­ory for the ba­sis of MBSE is not see­ing the wood for the trees. Cat­e­gory the­ory may be the study of math­e­mat­i­cal ab­strac­tion but type the­ory is the fire that breathes truth and in­ter­pre­ta­tion into a cat­e­go­ry.

So here is where I state the man­i­festo in­her­ent in the ti­tle of this blog: I am call­ing for an end to the di­chotomy be­tween struc­ture and proof; an end to the re­liance on set the­ory as the ba­sis of “truth” in the MBSE world. Let’s re­place our logic with judge­ments and ev­i­dence. I am call­ing for the con­struc­tion of a cat­e­gory of sys­tems!

If you’ve stuck with me this far, you’re prob­a­bly the sort who’s in­ter­ested in learn­ing fur­ther. I whole­heart­edly rec­om­mend div­ing into the Haskell and Idris pro­gram­ming lan­guages which ig­nited my in­ter­est in this area of study. If you feel that you’re ready for the bleed­ing edge of maths, I rec­om­mend the Ho­mo­topy Type The­ory book. It’s a free down­load and I’m cur­rently work­ing my way through it (de­ter­minedly but slow­ly, I must ad­mit) to see what trea­sures can be found in­side for the fu­ture of sys­tems en­gi­neer­ing.

Con­clu­sion: what needs to change?

First of all, its my be­lief that we could use a lan­guage like Idris to ex­press our sys­tems mod­els com­pletely and con­her­ently in a way that could be eas­ily val­i­dat­ed. With a suit­able base li­brary (or a pre­lude as is called in Haskell de­scen­dents), Idris could eas­ily be used as a spec­i­fi­ca­tion lan­guage with math­e­mat­i­cal proofs built in. The prob­lem, of course, is that en­gi­neers like pic­tures, so Idris would need a graph­i­cal no­ta­tion on top of it that could be some­thing very UML or SysML like.

UML and SysML, de­spite be­ing sup­pos­edly lan­guage ag­nos­tic, are heav­ily Java ori­ented lan­guages. A lot of the more im­per­a­tive parts of UML could be trans­formed into a type the­o­retic set­ting but UML is so bloated with dis­con­nected con­cepts that it might not be worth it. The con­structs of UML and SysML mean that there are many ways to rep­re­sent a sin­gle con­cept and this fact leads to huge dis­par­i­ties in mod­el­ling philoso­phies and prac­tices across the MBSE world even within in­di­vid­ual teams! A fu­ture lan­guage would en­sure that you could ex­press any­thing that you’d want to de­sign but with min­i­mal over­lap of con­cepts.

Func­tional pro­gram­ming lan­guages since early LISPs have taught us that many com­plex con­structs can be ex­pressed in a clean sim­ple syn­tax. This point has def­i­nitely been reached with Haskell and its de­scen­dants. UML, like Java, has a bloated syn­tac­ti­cal struc­ture, re­quir­ing you to in­di­vid­ual cre­ate and name loads of el­e­ments to ex­press sim­ple ideas. A sim­ple test of this is see­ing how many el­e­ments you have to cre­ate and name if you were to cre­ate a sim­ple ob­ject flow based ac­tiv­ity di­a­gram. Every sin­gle pin on every func­tion re­quires cre­ation, a name and a type. There has to be a bet­ter way.

There­fore, as sys­tems en­gi­neers, we should start ex­plor­ing the ex­cit­ing world that a type the­o­retic ba­sis to MBSE could be. There are many bonuses to us­ing a type the­o­retic and func­tional ap­proach to mod­el­ling lan­guages that I hope to ex­plore in fu­ture blog posts. For now, I hope that I have put for­ward a con­vinc­ing enough ar­gu­ment to en­tice you into want­ing to know more about type the­ory and func­tional pro­gram­ming. If you have any thoughts your­self on the mat­ter, please pop them in the com­ments be­low. If you’ve made it this far, thank you for read­ing!