Leibniz - a digital scientific notation

Leibniz is an attempt to define a digital scientific notation, i.e. a formal language for writing down scientific models in terms of equations and algorithms. Such models can be published, cited, and discussed, in addition to being manipulated by software.

Although Leibniz can express algorithms, it is not a programming language. It is more similar to a specification language in that it allows to express what some program is supposed to compute.

Leibniz is named after Gottfried Wilhelm Leibniz, who made important contributions to science, mathematics, formal logic, and computation, topics that are all relevant to this project. He also invented a widely used notation for calculus.

If you are interested in the development of digital scientific notations, even if your ideas are very different from what I envisage with Leibniz, please consider joining my Open Science project at Guaana.

Status

The support code for Leibniz is now sufficiently advanced that first examples for digital scientific knowledge can be developed. They are located (no surprise) under examples. For a first contact with Leibniz, I suggest looking at examples/quantities/mass.rkt, which shows how physical quantities and units can be defined. For a much more elaborate example, see examples/mechanics/solar-system.rkt, which defines gravitational interactions in a system of celestial bodies. In examples/quick-guide.md you can find essential background information for understanding the examples.

Readers interested in the implementation should start by looking at the file notes.md for an overview of the code structure.

I will announce any significant progress on my Guaana project.

Background

The following articles are helpful to understand the context in which this code is developed:

• My essay Scientific notations for the digital era explains the concept of digital scientific notations, in particular as opposed to scientific software.

• Mark Buchanan wrote an excellent one-page summary of this essay for Nature Physics, under the title Digital Science.

• I have written two short essays on related topics: Scientific communication in the digital age and Verifiable research: The missing link between replicability and reproducibility

Leibniz is based on equational logic and term rewriting. This seems an appropriate choice for scientific models that are traditionally written as mathematical equations. Algorithms are expressed by giving a direction to certain equations, indicating that the left-hand side is supposed to be replaced by the right-hand side in simplifying an expression. Term rewriting has been used for a long time in computer algebra, notably by Mathematica.

Leibniz differs from Mathematica and most other computer algebra systems in using an order-sorted term algebra, in which each term is assigned a sort, which is similar to what is called a type in programming languages. For a detailed discussion of order-sorted algebra, see

• Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations by J. A. Goguen and J. Meseguer

Term rewriting in order-sorted algebras has been implemented in the specification languages OBJ and its modern offshoot Maude. For readers familiar with these languages, a Leibniz "context" is roughly the same as an "object" in OBJ or a "functional module" in Maude. Reading the Maude documentation is currently the best preparation for understanding Leibniz.

However, Leibniz is much simpler than Maude, lacking both Maude's flexible syntax and its support for non-functional modules. This is due to a very different focus: Maude is a language for writing specifications for complex software, whereas Leibniz is a notation for scientific models. Scientific models are much simpler than most software, but they can be processed by a wide range of software. Leibniz must therefore be easy to implement in a wide range of software packages, whereas reimplementing Maude is of little interest, given that its source code is open.

Required software

This first implementation of Leibniz is written in Racket, whose support for implementing languages and language extensions is particularly useful for this project. In addition to Racket itself, Leibniz depends on the following libraries:

• threading
• chk (or rather my slightly modified fork that fixes an installation problem on recent Racket versions)

The examples also use

• sweet-exp

for better readability.

To install Leibniz and its dependencies, type:

   raco pkg install git://github.com/khinsen/leibniz\?path=leibniz

To run the Leibniz test suite, type

   raco test -c leibniz

You can run an individual library module's tests by typing

   raco test -l leibniz/sorts

etc.

License

I expect to properly document and release this code at some time, under a meaningful license. But for now, it is research code covered by the CRAPL license.

Branch notes

Most branches of this repository contain experiments that test the utility and feasibility of ideas for improvements and new features. Each branch has a short note in this place that explains its reason for being. This branch (master) always contains the version currently considered most useful.

Note that all branches except master may be rebased, or modified in other ways. If you want to fork this repository, please don't rely on any branch other than master.