Set Theory
SET THEORY
Rosivaldo Fernandes Alves
September 23, 2017
Abstract
This software project, called set_theory (https://code.launchpad.net/~rosivaldo.fa/set-theory/trunk), aims to provide the Eiffel (programming language) Community with a rich and expressive library of classes modeled upon the concepts of set theory. Initially, the project is limited to present a specification of such a library, i.e. every class and feature is deferred, with no concrete implementation yet. Why to do so? The idea is to release the specification into public domain, as an open source project, and let the community use, correct, modify, enrich and implement the specification as they wish. It is also an exercise of the Eiffel method ability to allow the developer to use the Eiffel language as a tool from the very beginning of development cycle, namely the specification/analysis/design activity. Although no implementation has been done, every class and feature is completely specified, that is, nothing is left to a non-formal apprehension of the intended semantics. The specification is also minimal, avoiding as much as possible any redundancy: nothing is specified twice, there is no double check of any feature result or class invariant. This project is the first of three, the others being a set theory properties library, and a set theory implementation library. The properties library consists of a rich set of features that will allow developers to test their implementation, or others’, against the mathematical properties – or propositions – that set theory objects must bear – or conforms to. The implementation… well, it will be my implementation of the current specification-only library. Any help will be welcome.
Introduction
Motivation
The seed of this project came into my mind in my ancient days of a multi-language-then-Delphi-developer, in 1999. Yeah, eighteen years ago. I was frustrated for not having a tool able to incorporate OCL-written specifications into my Delphi code. Then I started to write a Delphi library of OCL-like classes and interfaces. Soon I heard of DbC as the most valuable contribution of Eiffel language to software development activity. After reading OOSC2, I “upgraded†my Delphi library in order to write my code along with DbC principles. None of my employers wanted to move to EiffelStudio, so buying it only for my personal use was a no way. No need to say that making DbC to fit into Delphi language/IDE on those days was a monstrously difficult task, and, despite interesting advances, my spare time was not enough to complete such a (Herculean) labor, and eventually I abandoned that goal. Anyway, my interest in Eiffel remained.
So in the 2000s EiffelStudio went open-source, and I finally could try it for real. Unfortunately, just during my spare time. Even so, I used Eiffel for academic projects and soon noted that some contracts were difficult to write thoroughly, due to the lack of a set theory library aimed to easing contract specifications. That was when I learned of MML, by Tobias Widmer and Bernd Schoeller. They were already doing what I needed, and more: MML was intended to allow validating contracts by static inspection. Great goal, great achievement. But one thing annoyed me: MML library was meant to make possible to write complete contracts for other classes but MML classes themselves lacked complete contracts.
Bernd Schoeller argued that MML classes should be treated as axiomatic ones, whose correctness should be implied by the underlying set theory. I don’t think so. Sure, MML was made to validate classes by means not applicable to MML classes themselves. But it does not imply that they could not be formally validated at all, let alone that they should not. They should. More than any other else, by the way, if they were meant to be reliable. With this in mind, I decided to develop my own set theory library.
Of course, all of that was many years ago. Why have I finished it just now? The best answer for this question is: Please, do not ask. :-)
Goals
Despite the OCL and MML roots of my decision to write this library, it is meant to mimic none of those. It has features that those do not have, but also lack others that those have. It is not difficult to equip set_theory with bags and richer sequences, for instance, but I prefer to let it to the (not so distant, I hope) future. The primary goal, for now, is to have a complete and multipurpose specification of a set theory library, fit to be implemented for any secondary purpose: writing an MML-like library for modeling and automated validation, creating higher-level libraries, e.g. those dealing with formal languages or graph theories, or just as the foundation for writing conventional, mutable, data structures like sets, trees and the like.
This is not a truly academic work, not even a professional one. It is just the result of my insistence in doing something that, I hope, may be useful to Eiffel community and that so far no one has done this way. It will be useful to me, at the very least.
Credits
This project, of course, was not born out of nothing, so I must credit those sources I relied on for inspiration, insights and knowledge. First of all, I credit to UML my initial interest on a more formal approach to software development. Then to OCL, the glimpse of how to make my own specification library. Object Oriented Software Construction, 2nd. Edition (OOSC2), by Prof. Bertrand Meyer, was a turning point on my learning history. I have no way to exaggerate the role of the already mentioned works of Tobias Widmer and Bernd Schoeller on providing me with plenty of stuff to study and learn.
I have got much help from sites like ProofWiki, nLab, planetmath.org, Wolfram MathWorld and the Wikipedia itself, which are priceless sources for finding terminology, alternative definitions, proofs and much more.
Nevertheless, no resource proved to be more valuable in this task than the book Teoria Elementar dos Conjuntos, by Edgard de Alencar Filho. Crystal-clear in presenting definitions, properties and theorems, almost every math expression written down on it lend itself to be effortlessly translated into computable code. It is a shame that such a book is out of print.
Some Considerations
My greatest fear about this project is that, working in almost complete isolation, I have produced a piece of software that definitely does not adhere to the coding conventions of Eiffel community. So they may get somewhat angry. I will try to justify my decisions.
Math symbols
First, I have made heavy use of math symbols, and was bold enough to render them in Unicode instead of some ASCII/ANSI mimicry of them. The price I have paid was somewhat high: EiffelStudio support to Unicode is poor still; I had little help from ES to deal with such alien characters, used mainly as operators. They disappear from Basic text view of Feature tool; they disappear from printing; they are replaced by question marks in generated documentation, whatever the filter I use; and so on. But I insist on them. Sure, Eiffel is not a domain-specific language, nor its syntax is meant to allow the creation of one. But Mathematics is a truly universal language, and I preferred to push the limits of ES instead of giving up using the venerable math symbols available in Unicode. Come on, we are no more in the nineteen-seventies. It is time for operating systems and IDEs to support Unicode decently for good.
For developers that may feel uncomfortable with those operators, the respective features may always be invoked by name. At worst, the developer may branch the original project and change it to get rid of Unicode operators at all. The library is open-source for things like that too.
An additional annoyance is that Courrier New, the font that ES uses by default fails to render several of those Unicode characters, and those that are shown get really ugly. Hence I preferred to use a font more Unicode-friendly, like Lucida Sans Unicode, which is not mono spaced, but, to my taste, renders Eiffel code, and Unicode characters too, very well. There are some mono spaced fonts good for Unicode rendering. Those who prefer these fonts may have a look at DejaVu Sans Mono, Noto Mono, or some other fonts available on the web.
Furthermore, Eiffel syntax does not allow to post-fix operators, so one cannot, for instance, invert a binary relation by writing R-1 or Râ†. So I have abused math notation by turning several post-fixed operators into prefixed ones. Out of syntax limitations, I also in-fixed operators that are usually prefixed or that have a math syntax totally alien to Eiffel, e.g. ∀.
At odds with EIS
The worst problem with using Unicode characters in ES is that they interact so badly with EIS (Eiffel Information System) up to the point to corrupt the Editor tool parsing, making the compiler to see syntax errors where there is none. The supposed errors disappear if the affected class is not opened in Editor tool. However, such a file gets uneditable in Editor tool, since any edition corrupts the file in memory, and trying to save the file corrupts it on disk too or makes ES to crash. It forces the developer to edit such classes externally. To workaround this, most classes had their EIS notes commented out.
Automatic class licensing defeated
ES automatic class licensing facility also gets defeated by the presence of Unicode characters in a class text; the license note clauses are inserted with varying degrees of corruption. So I had to copy and paste the license in most classes. If the license file is edited, when ES tries to update the license clause in a modified class, the license clause gets corrupted again. :-(
No prefixed class name
I have chosen not to prefix the class names, e.g. neither ST_SET nor ST_BIJECTION will be found here. I prefer to rely on ES capability of renaming a class or prefixing an entire library when needed. Some argue that it is not portable, that some Eiffel tool-chains cannot deal with such renaming. My appeal: improve those tools.
Unusual feature clauses
Although EiffelStudio offers a quasi-standard set of feature clauses, I preferred to use some additional ones. “Standard†or not, they are described below.
Definition
Features that define the concept represented by a class. Usually, such features are not defined, i.e. they lack an ensure clause, since they are the bare bones of their respective classes, whose other features and invariants are specified in terms of those in this clause.
Access
Features akin to those in Definition clause, but that are not primitives, being instead derived from those.
Notable element
Feature that access remarkable elements in structure-bearing sets.
Status report
Some few features inherited from EiffelBase.
Quality
This clause is akin to Status report. But, since every object in set_theory library is intended to be immutable, they have not true statuses, but qualities inherent to their internal structure.
Membership
This is a key aspect of elements and sets in set theory: every element is or is not a member of some set; oppositely, every set has or has not some element as their member.
Relationship
A special kind of membership, applicable to binary relations, that are sets of ordered pairs.
Quantifier
Some queries are specified in terms of universal or existential quantifiers of first-order predicate logic. They are gathered here.
Comparison
The usual comparative queries between objects of similar kind: equality, inclusion, ordering etc.
Relation
Queries upon how different objects are mutually related; they differ from Comparison by the fact of not fitting to establish an order among similar objects and by usually to apply to dissimilar ones.
Measurement
The usual kind of measurements: count, size, capacity etc.
Construction
Features aimed to build new objects by extending or decomposing previous ones.
Subset
This minor clause covers only the most trivial subsets of a set, which deserve to stand out from Operation features.
Interval
Operations that, from given lower and upper bounds, extract subsets from ordered sets.
Extremum
Operations that deal with extreme elements in ordered sets, e.g. minimum, maximum or infimum values.
Restriction
Operations that restrict well-known numeric sets to some of their specific subsets.
Operation
Mathematically well-established operations of set theory are put here.
Basic operations
Some few features inherited from EiffelBase.
Arithmetic
Features that provide some useful arithmetic operations.
Transformation
Features intended to provide somewhat complex operations upon sets and alike, e.g. mapping and reduction, which usually must be specified by means of recursion; keeping such operations here prevents, almost always, using recursion in ordinary features.
Conversion
Two kinds of feature occur here: those that change the type of an object without touching its mathematical value and those that embed an object into some kind of container.
Factory
Since every class in Set Theory library is deferred, none of them has a create clause, and the creation of new objects is delegated to factory features put here.
Predicate
Boolean queries written for the sole purpose of avoiding the use of in-line predicate agents, since the latter are stripped from Contract and Interface views of EiffelStudio.
Mapping
Features that provide agents for mapping transformations, since in-line agents are stripped from Contract and Interface views of EiffelStudio.
Reduction
Features that provide agents for reduction transformations, since in-line agents are stripped from Contract and Interface views of EiffelStudio.
Immutability
Every class in this library defines immutable objects, i.e. objects with no command feature at all. If one extends a set, or a sequence, for example, the original container stays untouched, and a brand new object is created for the extended container. One should keep in mind that “immutable†objects are immutable only if used as they were designed for. I did nothing to address the Frame Problem, as defined by Bernd Schoeller. AFAIK, it is an open problem to this date for imperative languages, and coping with it is far beyond my skills and immediate goals. If referential transparency is a must, perhaps the developer should have a look at Haskell. :-/
Renaming
In most cases, I have refrained myself from relying on renaming. Many operations in set theory have several names according to the context they are used in. It is tempting to follow these variations by renaming features wherever convenient; instead, in such cases I have defined new features as simply equal to their synonyms in ancestor classes. At once, this somewhat promotes uniformity and adherence to varying terminology. Those synonym features can even be written as such by an implementer, since Eiffel syntax allows it.
Most renaming in set_theory limits to resolve name clashes or to adjust the use of operators, replacing more general versions by more specific ones, or even to provide a kind of argument contravariance.
Documentation
The already mentioned problems with Unicode characters have been reported to Eiffel Software. But I do not know when they will manage to patch up those annoyances. Meanwhile, the ubiquity of Unicode operators in set_theory renders the documentation generated automatically by ES nearly useless. For the time being, I have used an external editor to convert the classes’ texts into PDF files, in order to make them readable by those that cannot deal with installing ES but are still interested on inspecting the library source code. Such PDF files are available here. Of course, they may get somewhat outdated and out of sync with the current sources, since hand-making such a big documentation is highly time-consuming.
Acknowledgments
Despite it is not an academic work, as I have already mentioned, I must thank some persons who helped me not to give up this little but relevant (to me, at the very least) project.
First of all, I thank my wife, Ivone, who knows for sure how much I wanted to get it done and gave me invaluable support without which I would have never – never! – got here. I also thank my daughter, Maria, who suffered and still suffers so much my prolonged absences due to tasks like this one.
I thank very, very much Maria Cristina Cavalcante, who, more than any other person in the world, urged me not to put aside my – then fading – interest and skills on software development, and computing in general, applied to scientific topics. I cannot forget to thank Celda Fontes, a common friend of ours, who always believed me even when I did it no more. On the same grounds, I thank Luana Shunk for his kind support when no one else was available. I heartily thank Dr. Tatiana Aiello, whose priceless care has made me capable of overcoming otherwise insurmountable obstacles along the years that mostly coincide with those that I have working this project through.
I would like to thank Prof. Giovanny Lucero, from UFS, who inspired me to increase my interest on topics related to theory of computation, formal languages, automata and their underlying math, from which set theory is only the very beginning. I am glad to thank Prof. Henrique Schneider, also from UFS, who gave me tremendous and undeserved encouragement when I was his student.
I must give special thanks to my great, incredibly goodhearted friend, Jadson Bitencourt, a privileged mind, superb professional and long-standing colleague who always shared with me the most rewarding ideas on computing, software development, technology, humanities and sciences in general, and whose generous enthusiasm with my then obscure efforts on this project renewed my resolution of getting it done for good.
I thank also Eiffel Software for making EiffelStudio open-source available to anyone willing to make awesome software. Thanks ES, I hope to be able to make useful contributions to Eiffel community and to software developers in general. By the way, I cannot forget to thank Eiffel Users group for their generous support along my many years as an always-asking-never-helping group member. By no means I could have this project done without their help. Thank them all very much.
Although my current job is totally unrelated to this project, I would like to thank those people under whose supervision I have worked through the last one and a half decade. First Adauton Borél, then Clilton Vieira, then Dannie Rosie Santos, then Adauton Borél again. All of them helped me to go through a lot of challenges, typical of a stressful IT department, without losing the motivation and energy necessary to accomplish my job duties and still be able to go along with personal affairs like the one presented here. More recently, Juvanilza Menezes proved not only to be a skillful manager, but also a great human being. I am very grateful by the time I have worked under her direction. Currently, LuÃs Carlos Cavalcante, a highly professional and committed manager, makes me proud of being where I am and honored of working under his guidance. My gratitude goes to him too.
Of course, I was lucky not only with my bosses. Many of my colleagues along those years also deserve my hearty thanks. Risking to make some unjust omission, I would like to thank Gilton Lobo, José Menezes Neto, Aldo Távora, Miriam Melo, Daykson da Cruz, João Paulo Andrade, Glaudiston Santos, Gerônimo Chagas, Carla Pitta, Tânia Souza, Eva de Fátima, Cláudia Neves and Débora Cristina Matos. I thank them all for their friendship, shared motivation, support in critical moments and persistent encouragement, not only on job-related matters, but frequently also on private ones.
Finally, I would like to thank another dear and long-standing friend, Soraia Sardeiro, professional translator, for her willingness on reviewing the present text, along with [''the still ongoing review of''] the pieces of text in natural language interwoven in the source code of set_theory. Without her work, my poor English would be shamefully evident. Obviously, I am the sole responsible for any remaining error.