FlexiForms

We will use the word flexiform as an adjective to describe the fact that a representation is of flexible formality, i.e. can contain informal (i.e. appealing to a human reader) and formal (i.e. supporting syntax-driven reasoning processes) components or both.

A good example for a flexiform document is a mathematical text, which contains informal representations - e.g. historical remarks or proof sketches as well as formal definitions. Note that we understand the term flexiform in an inclusive sense, in particular, we include fully formal representations like algebraic specifications of software properties and in principle also fully informal documents like e-mails into the set of flexiform documents. We are also interested in

• flexiform theories: i.e. mathematical theories that are represented with flexible formality. Flexiform theories tend to be formal objects that make use of informal representations for documentation or migration.
• flexiform libraries: i.e. collections of flexiform documents whose relations may be marked up with flexible degrees of formality, ranging from the Dublin Core source relation or to theory morphisms.
• flexiform fragments: i.e. the self-contained fragments that make up the flexiform objects or collections above.
• … the list goes on … exploring this will be one of the purposes of MathHub.info.

We will use the noun flexiform to denote an arbitrary flexiform object or collection as exemplified above. This concept of the class of flexiforms is useful, since it has very good closure properties: flexiform fragments can be composed to flexiform documents, which can be collected to flexiform libraries, which in turn can be formalized to flexiform theory graphs or excerpted to flexiform documents. All of these knowledge management processes can now be described in terms of flexiforms.

Note that as defined here, the class of flexiforms is very broad, it includes arbitrary (informal) documents, datasets, and logical axiomatizations. We will pragmatically restrict the set of completely informal representations to those that are intended to or could in principle be (semi)-formalized, excluding e.g. poetry, which are outside our interest for MathHub.info. In particular, we include completely informal documents that are written with eventual flexiformalization in mind as the starting points of a step-wise formalization process, first adding methodical and mathematical rigor, and then marking up formal elements.

Concretely, the class of flexiforms includes specifications from program verification, semantically annotated course materials, textbooks in the “hard sciences”, etc.

In MathHub.info, Flexiforms are usually realized as documents in representation formats that flexibly support both formal and informal modes of representation.