trs - a term rewriting system

A C++ implementation of a Term Rewriting System (TRS) with Breadth-First Search (BFS) rewrite exploration and symbolic pattern matching.

Features

• Symbolic Representation: Supports variables, constants, and functions.
• Pattern Matching & Substitution: Unifies patterns with free variables and applies substitutions to generate new terms.
• Infinite-Depth BFS Exploration: Explores the entire reachable space of term rewrites via BFS, ensuring all possible rewritings are discovered (terminating when no new terms are found).
• Input Database Parsing: Loads declarations and inference rules from human-readable .trs files.
• Memory Safety: Clean resource management validated via AddressSanitizer (ASAN) and Valgrind.

---

You can define symbols and rewriting rules directly in a .trs file:

# algebra
neg([0])          -> [0]
neg(neg(x))       -> x
sub(x, [0])       -> x
sub([0], x)       -> neg(x)

sum(x, [0])       -> x
sum(x, y)         -> sum(y, x)          # commutativity
sum(sum(x, y), z) -> sum(x, sum(y, z))  # associativity
sum(x, x)         -> mul([2], x)

sin(sum(x, mul([2], PI))) -> sin(x)
cos(sum(x, mul([2], PI))) -> cos(x)

der([c], x) -> [0]
der(x, x) -> [1]
der(y, x) -> [0]

• Comments can appear at the beginning or at the end of a line, and begin with #.
• Logical implications are defined with an arrow ->, where on the left is the implicant and on the right the implication.
• Functions are defined as they first appear in the database. Writing a function with a different parameter count will result in an error.
• Natural numbers are written between [] square brackets. A variable natural number (and not a symbol) can be referenced writing a name between brackets, like [n].
• Constants are written in caps, like PI.
• Functions with different parameters are matched only by applications of different symbols. Functions with same parameters are matched only by applications of same symbols. The rule der(x, x) -> [1] is matched when two same symbols are found, while der(y, x) -> [0] is matched with two symbols that are necessarily different.

---

Project Structure

• src/: Core C++ source files
  • main.cpp: Executable entry point, demonstrates rewriting.
  • rewriting.cpp / rewriting.hpp: Rewriting logic, binding maps, and BFS exploration.
  • symbol.cpp / symbol.hpp: Symbol representations, matching, and cloning.
  • database.cpp / database.hpp: Symbol and rule repository singleton.
  • userdb.cpp / userdb.hpp: Parser interfaces to populate the database.
• lib/spl/: Simple Parser Library.
• res/: Configurations and databases

---

Getting Started

Prerequisites

Ensure you have the following installed on your system:

• A C++17 compatible compiler (e.g., GCC or Clang)
• Meson Build System
• Ninja Build System
• make (optional, for shortcut commands)
• entr (optional, for file watching and automation in developer mode)

Compilation

You can compile the project using Meson/Ninja or the provided Makefile helper:

make compile

This compiles the executable under the build/ directory.

Development mode

Simply run make dev to enter a development mode loop, with file watching:

• the project gets recompiled if some change to the code is detected, and the main database gets re-run.
• the executable is restarted if a change to one of the databases is detected.

Running the TRS

To run the program with the default calculus rules defined in res/calculus.json:

make run

Or execute it directly with a custom JSON configuration file:

./build/trs path/to/your/rules.json

Running Tests

Run the test suite using Meson:

meson test -C build

Debugging & Memory Safety

To compile and run the project under AddressSanitizer (ASAN):

make sanitize

To run under Valgrind memory leak checks:

make check

To clean build directories:

make clean