BookofProofs starts as of 14th July 2020 a new collaborative subproject – the specification for FPL. Once it reaches a mature state, FPL will be integrated into BookofProofs so that it will be possible to enter FPL code instead of entering new content in English. Moreover, FPL will allow to translate FPL code into any natural language, not only back into English.
FPL, the Formal Proving Language, is a planned specification for an artificial language that is going to serve as a universal language to formulate mathematical definitions, theorems, and proofs independently from local natural languages.
While English is currently the de facto standard natural language for mathematical publications, FPL should further facilitate the dialog between mathematicians all over the world, providing a standard notation, a standard degree of details needed to write mathematical proofs, and a standard degree of details needed to formulate mathematical definitions, axioms, and theorems.
At the same time, as a formal language, FPL is going to facilitate creating automated tools serving different additional purposes, in particular:
to mention only some possible applications.
FPL is not yet another automated proof assistant or yet another automated theorem proving tool. It attempts to set a standard for writing mathematical definitions, theorems, and proofs while encouraging programming automated tools based on FPL.
The syntax of existing formal systems and automated tools is computer-friendly, i.e. primarily designed to be compiled and processed by automated tools, not by humans. Therefore, the language used by these tools is hard to read and to understand, even by mathematicians. The communities using these tools are small communities of specialists. Despite that, such automated tools provide many advantages. In particular, they help to write correct mathematical proofs and help to avoid errors.
Therefore, it would be great if there would be tools using a formal language that is readable, catchy, and easy to learn, even for non-programmers. Such tools could be (ideally) also used for educational purposes to teach mathematics.
FPL wants to close this gap. FPL is going to have a human-friendly syntax while being formal enough to develop tools based on it that can assist in writing and developing correct mathematical theories. In particular, FPL should be easy enough to be used in mathematical education.
Thus, FPL primarily aims at being human-readable and only then at being compiled and processed by computers. By this human-centric approach, FPL should enjoy a better user acceptance, while providing comparable advantages that automated formal language tools provide.
The repository for this subproject is hosted at Github and you are invited to join the contributing team. The FPL specification is published under the CC-BY-4.0 license, encouraging you to contribute and/or to use FPL as a reference for your own, FPL-related projects.
To be successful, the FPL specification has to follow some seemingly contradicting principles:
“Code written in FPL should be not only human-readable but also catchy, memorable, and easy to learn so that FPL can be learned even by non-programmers.”
This principle will be the most difficult to accomplish since a formal language can be human-readable but not always easy to learn and memorable. A memorable notation and simplicity of syntactical rules will be key for user acceptance.
“The syntax of FPL should be inspired by modern mathematical notation while preserving the readability principle.”
The richness of modern mathematical notation imposes at least two challenges for a specification of a formal language like FPL: one is its catchy readability, another it’s ambiguity.
x_i, x_{i_j}, x^{(k)}_j etc.)a_1,\ldots,a_n),\pmatrix{a_{11}&a_{12}\\a_{21}&a_{22}}),\sum), products $\prod$ (coded \prod), integrals $\int$ (coded \int), composition of functions $f(g(f(x))))$ (coded f(g(f(x))))),Because FPL is intended to be a formal language, its specification has to resolve the conflict between a notation that is catchy for humans and a notation that is computer-readable, while preserving the richness of notation. The FPL specification will have to make some concessions in both directions, i.e. keep the notation as simple as possible to allow a catchy result, while allowing complicated constructs to make it easy for computers to parse the code.
A feature of every formal language should be the lack of ambiguities. If a compiler encounters the symbol 1, it should collect enough information from the context to interpret the symbol in a manner it was meant by the author of the FPL code. On the other hand, avoiding ambiguities makes the syntax of many formal languages overloaded so that their readability suffers a lot.
So, how should FPL deal with notational ambiguities, without overloading the syntax? Again, the FPL specification will have to make some concessions in both directions, i.e. keep the notation as unambiguous as possible, while allowing context-based re-interpretation of the same symbols.
“FPL should be based on the axiomatic method i.e. every theory written in FPL should start with some definitions of mathematical concepts, axioms about these concepts asserting that they are true, and deriving new theorems based on given logical rules of inference while interpreting them also as true when they are derivable using the rules of inference.”
While the rules of inference have to be declared in FPL, to keep things simple, the semantics (i.e. interpretation) of any theory that was written in FPL should not have to be explicitly declared.
Thus, theories written in FPL simplify things by asserting that:
This approach is similar to the approach used in mathematics, in which axioms are variable but both, the rules of inference and interpretation, are not always explicitly apparent. The rules of inference are not explicitly given since mathematics is not formulated in a formal language. Interpretation is also not explicitly defined. There is a common sense that if something is “logically correctly derived from axioms” then it “is also true”. However, we should be aware that this is only one of many different possible interpretations and thus the theories of contemporary mathematics are not the only possible ones. They might even be false under different interpretations.
“While using the axiomatic method, FPL should not stick to a pre-defined set of axioms and rules of inference. Its meta syntax and semantics should allow developing any theory using the axiomatic method.”
FPL should allow formulating any new theory starting with a new set of axioms and rules of interference. This way, the scalability and extensibility of FPL should be ensured to anticipate future developments in mathematics and its evolution as a science.
“The FPL framework should encourage using some standard sets of axioms and rules of inference that were written in FPL to promote standard notation for widely agreed mathematical concepts and a common sense of what is currently perceived as a consistent mathematical theory. To facilitate using these standards, the FPL syntax should establish an explicit notation (or namespaces) for these standards, allowing to easily distinguish between a standard and non-standard FPL notation for widely agreed mathematical concepts.”
The “FPL framework”, in comparison to “FPL” itself as a pure language specification, should provide a public, open and freely accessible repository of pre-formulated theories in FPL with commonly agreed axioms and rules of inference, as well as notation that can be re-used for further purposes.
The usage of such pre-formulated theories can be compared to “including” the code of these theories as modules of own theories.
If a notation of an extended theory based on a standard module becomes commonly accepted by the community, the repository authorities may decide whether to add the extended theory as another module that can be re-used by others as a standard module.
The distinction between standard and non-standard modules of FPL should be made explicit, using reserved namespaces for standard modules.
“The syntax and semantics of FPL should enable the creation of automated aids and tools.”
While human readability remains important (see Principle 1), FPL should be formal enough to facilitate a rigid and unambiguous notation.
The syntax of FPL should be formal enough to develop automated tools capable to verify the correctness of FPL theories. Integrated Development Environments (IDEs) for FPL should assist users in writing correct mathematical proofs and in formulating mathematical definitions that meet modern standards.
Also, the syntax should make it possible to program automated tools translating a theory that was formulated in FPL into a given natural human language (possibly including LaTeX notation for mathematical formulae). With this respect, FPL should provide a means to formulate the same content independently from a given natural human language, while still enabling people to read the content even if they do not use or know FPL.
The main result of this specification is a syntax of FPL in the Extended Backus Naur Form (EBNF).
The above principles show a high complexity of reaching all of them at once by a language. The specification has to be developed using an agile method to be able to adapt to future requirements. The principles define high-level requirements that will be complemented by Additional Requirements of the language resulting from the following iterative agile process:
Ad Step 1.
The definition of the syntax should be done in EBNF or a variation of it. It makes sense to use a dialect of EBNF that can be used as the input for a tool generating a parser out of the grammar. Such a tool is, for instance, https://tatsu.readthedocs.io/en/stable/.
Ad Step 2.
If the parser can be recreated, the EBNF code is formally correct. Otherwise, the EBNF has to be corrected until the parser can be recreated.
Ad Step 3.
A repository of test cases is required for the agile process. A test case is a file containing code written in FPL (obviously with the file extension “*.fpl”). A test case addresses features of the FPL language that it has to fulfill. These features have to be defined in a list of Additional Requirements.
Some of the features might address not the syntax but also the semantics of the FPL language. Therefore, apart from the parser, also a compiler of FPL has to be implemented that addresses all requirements regarding the semantics. This compiler plays a role in step 5.
Ad Step 4.
The assessment of how FPL reaches the 6 pre-defined principles can be made only qualitatively. This will be accomplished using a qualitative ordinal scale. An ordinal scale has the advantage that it is possible to assess what’s is more important and significant, but the exact differences between each ordinal are not known.
A possible scale for assessing reaching each of the principles can be
Ad Step 5.
The Additional Requirements are a list of additional features FPL has to fulfill to meet the 6 pre-defined principles to a satisfactory degree (“quality gate”). In each iteration, in step 5 the Additional Requirements from the but-last iteration are used.
Ad Step 6.
Unlike the pre-defined principles, the Additional Requirements can be changed, enhanced, or adjusted in each iteration. Only those Additional Requirements should be added that help to meet the 6 pre-defined principles.
Initially, no Additional Requirements are defined. It should be documented, at which iteration an additional requirement was added and how meeting this requirement helps to meet the 6 pre-defined principles.
Ad Step 6.
A quality gate has to be defined to decide whether further repetitions of the agile process are required to improve the FPL specification. As of now, the quality gate consists of the following criteria:
to be created, see repo at Github
to be documented, see repo at Github
| 
| 
| 
| created: 2020-07-14 15:10:25 | modified: 2020-07-16 18:09:11 | by: bookofproofs | references: [1591]
[1591] Piotrowski, Andreas: “bookofproofs.org”, Own Work, 2014