Leibniz

A Digital Scientific Notation based on rewriting

This page introduces Leibniz, a digital scientific notation developed by Konrad Hinsen and implemented on top of Glamorous Toolkit. Leibniz is not a programming language and not a computer algebra system. It is an experiment in how scientific knowledge itself can be written, inspected, and manipulated in a form that remains intelligible to humans while being executable by machines.

At its core, Leibniz is about rewriting.

## What Leibniz demonstrates Leibniz demonstrates the power of **small, special-purpose notations** for scientific work. Instead of embedding scientific models inside general-purpose programs, Leibniz expresses them directly as *terms, equations, and rewrite rules*. This makes it possible to: * write scientific models as readable artifacts, * manipulate them formally, * and inspect their behavior step by step. Leibniz is thus best understood as a **bridge between mathematical notation and executable computation**.

## The Leibniz environment The Leibniz interface is a combination of: * a **formal model** (terms, sorts, operators, rewrite rules), * a set of **annotations** that turn knowledge-management pages into scientific notations, * and several **inspector extensions** that expose internal structure and behavior. The environment supports three complementary modes of use: 1. **Use-mode** Express scientific notations directly in pages. 2. **Debug-mode** Inspect how rewrite rules apply: pattern matching, term replacement, and intermediate states. 3. **Engine-mode** Investigate the rewriting engine itself as a computational system.

## Rewriting as the core operation Leibniz is fundamentally a **rewriting system**, inspired primarily by **Maude**, which in turn belongs to a longer lineage of algebraic specification and rewriting systems (OBJ, etc.). While there is a rich theoretical literature on rewriting, much less attention has been paid to **practical development tools** for working with rewrite systems. Leibniz explores this gap. Its rewrite “debugger” is intentionally simple: it displays the individual rewrite steps and lets the user navigate them interactively. This has proven sufficient to make rewriting *visible* and *understandable* in practice.

## Tour and background

This session has Konrad Hinsen giving a tour of *Leibniz* github , a Digital Scientific Notation built on top of Glamorous Toolkit.

YOUTUBE f10NpsMmbis Hitchhiker #17: Using Glamorous Toolkit for Scientific Notation - Konrad Hinsen & Tudor Girba

HINSEN, Konrad, 2016. Scientific notations for the digital era. arxiv , github

> Computers have profoundly changed the way scientific research is done. > … an ever increasing part of today’s scientific knowledge is expressed, published, and archived exclusively in the form of software and electronic datasets. > … digital notations optimized for computerized processing are often an obstacle to scientific communication and to creative work by human scientists.

## Related materials

This book contains various Leibniz contexts, both as examples for studying and as foundations to build on.

~

gives a talk in the colloquium Journeys in Platonia: Celebrating 50 Years Since The End...

Leibniz and Wiki

## Local and published artifacts Local development and published versions include: * `leibniz.md`, `leibniz.pdf` * `rewriting.md`, `rewriting.pdf`

pages/leibniz

## How to read this page This page is an **entry point**, not a manual. To understand Leibniz in depth: * follow the **tour**, * study **rewriting** through the provided examples, * and treat the contexts as *living notations*, not static documents. Leibniz is best approached as an ongoing exploration of how scientific reasoning can be made **legible again** in a computational world.