ExMaude Quick Start

app_root = Path.expand("..", __DIR__)

if File.exists?(Path.join(app_root, "mix.exs")) do
  # Running from a clone of the repository: use the local checkout,
  # which bundles the Maude interpreter under priv/.
  Mix.install(
    [{:ex_maude, path: app_root, env: :dev}],
    config_path: :ex_maude,
    lockfile: :ex_maude,
    config: [ex_maude: [use_pty: false]]
  )
else
  # Running standalone (e.g. via the "Run in Livebook" badge): use the
  # released package. This needs a `maude` binary on your PATH, or the
  # MAUDE_PATH env var set — see https://github.com/futhr/ex_maude#installation
  Mix.install(
    [{:ex_maude, "~> 0.4"}],
    config: [ex_maude: [use_pty: false]]
  )
end

{:ok, _pool_supervisor} =
  Supervisor.start_link([ExMaude.Pool.child_spec()], strategy: :one_for_one)

Introduction

ExMaude is an Elixir client for Maude, a language and system for rewriting logic. Where Elixir programs describe how to compute, a Maude specification describes what is true about a system: which expressions are equal, and which state transitions are possible. Maude can then compute with those facts — simplifying expressions, running state machines, and exhaustively exploring every reachable state to prove properties.

That last part is the superpower. Maude excels at:

• Term rewriting — reducing expressions to their simplest form
• Equational reasoning — computing with algebraic laws instead of hand-written algorithms
• State space exploration — searching every possible execution of a system
• Formal verification — proving that bad states can never be reached

This notebook covers the basic ExMaude API. The Term Rewriting notebook then builds up the Maude concepts step by step, and Advanced Usage applies them to real rule-conflict detection.

Running this notebook — the easiest path is to open it from a clone of the ex_maude repository, where the Maude interpreter is bundled and nothing else needs installing. Opened standalone (for example via the Run in Livebook badge), the setup cell falls back to the released package, which needs a maude binary on your PATH — see the installation guide.

Your First Reduction

Maude code lives in modules — named collections of types (sorts), operators, and laws. Maude ships with built-in modules like NAT (natural numbers), INT (integers), and STRING.

The most fundamental operation is reduce: give Maude a module and a term (an expression), and it applies the module's equations until nothing more can change. The stable result is called the normal form.

ExMaude.reduce("NAT", "1 + 1")

Every ExMaude call returns {:ok, result} or {:error, reason} — the result of a reduce is the normal form as a string:

ExMaude.reduce("NAT", "2 * 3 + 4")

Other built-in modules work the same way. INT adds negative numbers:

ExMaude.reduce("INT", "-5 + 10")

Even large computations are fast — Maude is a mature interpreter with decades of optimization behind it:

ExMaude.reduce("NAT", "2 ^ 64")

Parsing Without Evaluating

parse checks that a term is syntactically valid in a module — without evaluating it. Maude answers with the term's most specific sort (its inferred type):

ExMaude.parse("NAT", "1 + 2 * 3")

The NzNat: prefix is Maude telling you the term's sort is non-zero natural number — inferred from the operators alone, before any evaluation. Invalid terms return an error that pinpoints the bad token:

ExMaude.parse("NAT", "invalid syntax here")

Equations vs Rules: a Teaser

Maude has two kinds of laws. Equations state that two things are equal — reduce applies them. Rules state that one state can transition to another — rewrite applies those. Here is a two-state system, loaded from a string:

coffee = """
mod COFFEE is
  sort State .
  ops tired caffeinated : -> State [ctor] .

  rl [drink] : tired => caffeinated .
endm
"""

ExMaude.load_module(coffee)

The rule [drink] says a tired state can become caffeinated. rewrite runs the transition:

ExMaude.rewrite("COFFEE", "tired")

State transitions are where Maude gets interesting — the Term Rewriting notebook explores them properly, including how to search every reachable state.

Working with Strings

Maude has a built-in STRING module. Maude string literals use double quotes, so the examples below use Elixir's ~s{...} sigil to avoid escaping. (Note the {} delimiters — with ~s(...), the parentheses inside the Maude expression would end the sigil early.)

ExMaude.reduce("STRING", ~s{"Hello" + " " + "World"})

ExMaude.reduce("STRING", ~s{length("ExMaude")})

ExMaude.reduce("STRING", ~s{substr("Hello World", 0, 5)})

Error Handling

Everything returns tagged tuples, so the usual Elixir patterns apply:

case ExMaude.reduce("NAT", "1 + 1") do
  {:ok, result} -> "Result: #{result}"
  {:error, error} -> "Error: #{inspect(error)}"
end

Referencing a module that isn't loaded:

ExMaude.reduce("NONEXISTENT-MODULE", "1 + 1")

A syntax error inside a term:

ExMaude.reduce("NAT", "1 + + 1")

Inspecting Modules

To see what a module actually contains, ask for its definition. Here is the real NAT — note the op declarations and their attributes:

ExMaude.show_module("NAT")

List everything currently loaded (your COFFEE module is in there now):

ExMaude.list_modules()

And for anything the high-level API doesn't cover, send raw Maude commands directly — note the trailing . that ends every Maude command:

ExMaude.execute("reduce in NAT : 10 * 10 .")

Under the Hood

ExMaude runs Maude as a pool of separate OS processes, so a Maude crash can never take down the BEAM, and concurrent callers each get their own interpreter:

ExMaude.Pool.status()

ExMaude.version()

Where to Next

Follow the notebooks in this order for a gradual introduction:

1. Term Rewriting — equations vs rules, writing your own modules, and search: the exhaustive state exploration that makes verification possible
2. Advanced Usage — custom modules in practice, IoT rule-conflict detection, pooling, telemetry
3. AI Rules — conflict detection for AI agent policies: capabilities, approval gates, sovereignty
4. Benchmarks — what performance to expect, and how verification cost scales