B. Sc. Thesis: Refactoring Theory Graphs

Back then on the 1^st July 2019 I handed in my B. Sc. thesis, which I subsequently “defended” on the 15^th July. My advisors were Prof. Dr. Michael Kohlhase and PD Dr. Florian Rabe.

• 📙 Title: Refactoring Theory Graphs in Knowledge Representation Systems

• 💬 Terse Summary:

  Based on the formal system and framework MMT for representing formal math, the thesis proposes a definition of behavior-preserving refactorings. It then focusses on refactorings to generalize and presents two such princniples. Importantly, one of the principles delivers a means of syntactical generalization along knowledge-translating morphisms (refinements) in MMT.

• 📃 Thesis PDF: latest revision

• 📽️ Presentation PDF: latest revision

• 💾 Source: _{… still figuring out on how to best publish this, please ping me if you want them.}

• 📜 License: Creative Commons Attribution-ShareAlike 4.0 International License

💬 Summary

The terse summary above is meant for people with a basic knowledge in MKM or formal systems. Usually when people ask me what my thesis was about, I rather present the following recipient-aware summaries:

• 2 minute summary for a total novice:

  Math is usually done with pen and paper and written in articles and text books. However, such math is inaccessible to computers since it’s written in natural language. Hence, there is a recent trend in formalization of math such that a computer can process it. One form of such processing is the act of “refactoring”, which means tidying up the knowledge.
  

  Similar to how you might tidy up your room regularly, say to separate papers from your studies from personal mails, you can do this with digital knowledge, which happens to be math here.

  My thesis discusses two tidying up processes for formalized math.

• 1 minute addendum for a programmer:

  So you know that one can do refactoring on code bases, at best while preserving some kind of, say, functional behavior. You can do similar techniques on code bases of formalized math.

  My thesis proposes a definition of behavior preservation and then goes on to defining two refactoring principles of an important class, namely refactorings to generalize knowledge.

  For example, your code might use LinkedList<Foo> everywhere as a type, but in fact it might as well be List<Foo>. Changing from the former to the latter would be a generalization. Or, say, going from List<Foo> to just Iterable<Foo>.

• 30 seconds addendum for people asking “so only theory??":

  No, in fact I also implemented my generalization refactoring algorithms and for one of them even devised a GUI.

  So the framework in which math can be formalized and which I used, is called MMT. To formalize mathematical documents with MMT there is an MMT plugin for IntelliJ IDEA. I extended that plugin with a simple GUI allowing you to select some knowledge items (theories) and automatically generalize them.

💡 Learnings

I learnt a lot during my thesis both technical as well as some non-technical skills. Here are is a probably incomplete list of them, which I’ll update every now and then:

• Let your thesis tell a (round about) complete story.

  There’s a reason why many publications have an introduction and a conclusion.

• Narration, i.e. writing of theses and publications, has real value and is not an easy task!

  Even if your work is novel and super great, you need a good narration to motivate, explain and reinforce that.

• Narration fosters accessibility and is part of mathematical knowledge management.

  Having much data in a consistent state in a datase is good, but useless without an adequate presentation. This in particular holds for mathematical knowledge. See also ¹ suggesting narration as an integral part of “big math” systems.