Overview of Leibniz

Leibniz is designed to be embedded into documents written for human readers, much like traditional mathematical notation. Leibniz code consists of declarations , of which there are several types which will be explained below. The main unit of code in Leibniz is called a context , and consists of all the declarations contained in a Wiki page. The name of the context is simply the page title.

To get a better idea of how this works, please have a look at the Context definitions that are part of this book. A quick introduction to reading Leibniz code:

1. Everything shown in blue is a declaration that contributes to the definition of a context: a-new-sort, a-new-operator : a-new-sort.

2. Everything shown in brown is example or explanatory code that does not contribute to the context definition: a-new-sort, a-new-operator : a-new-sort.

3. Computed results are shown in green : 2 + 3 ⇒ 5. To make this computation work, we have to include the Integers context, as nothing in Leibniz is built in and always there.

In addition to its main context, a page can define subcontexts . They consist of all the declarations in the main context plus all declarations that include a subcontext name. Subcontext names are shown as a purple label before declarations: _a-subcontext a-new-sort-in-a-subcontext. Subcontexts exist mainly to allow examples to be included right in the page, but without cluttering the context with non-essential definitions. Many of the contexts in this book contain an example section that illustrates how this works in practice.

A good starting point for exploration is the context Integers, which shows how to express in Leibniz some basic mathematics that you are probably familiar with. Next, have a look at Heron's algorithm for computing square roots, which explains a simple numerical algorithm, and at Lotka-Volterra equations, which illustrates differential equations and in particular how Leibniz code can be used by a solver for differential equations written in a traditional programming language.

Clicking on any declaration opens a data inspector for it. For now, many of these inspectors are very basic and provide little added value, but they are expected to become the main user interface for working with mathematical and scientific models in Leibniz.

Note: If you are reading this book on the Web, you are looking at a static export that has none of the interactive facilities. Install the software on your computer for the full interactive experience.

An important principle is that the order of declarations in the page does not matter. This means that the semantics of the declarations do not impose any restrictions on the organization of the explanations. For the same reason, Leibniz allows declarations to be repeated multiple times in the page. The code adapts to the prose.

Leibniz' data model

The main inspiration for the data model used in Leibniz is the specification language Maude. The introductory material on Maude is a useful guide to how Leibniz works, though the syntax is very different. A Leibniz context corresponds roughly to a functional module in Maude.

All data in Leibniz is represented by Terms, which are tree structures composed of Operators with optional arguments (which are terms as well). Terms are classified by Sorts. Terms cannot be modified (they are immutable ), but other terms can be derived from them via Rewriting. A context defines:

1. a signature , which defines the operators and their sorts that in turn define which terms can be constructed in the context.

2. equality axioms for these terms

3. rewrite rules applicable to these terms