Newn 1.0.1

Newn — define new mathematical systems through properties, categories, and axioms. Symbolic reasoning, bidirectional backtracking, and multi-format export.

Newn

Define new mathematical systems in plain text. Reason over them bidirectionally.

pip install newn

Newn is a Python library for building custom symbolic rule systems — algebras, type systems, abstract number domains, game logic, formal grammars — using a clean declarative file format called .nn. You state what is true. Newn enforces it, inverts it, and exports it.

---

Why Newn?

Most languages let you compute. Newn lets you declare what a system is — and then query that system from any direction.

• No imperative code. Every op is defined by axioms, not procedures.
• Bidirectional by default. Every rule system is automatically reversible — find what inputs produce a given output without writing inverse functions.
• Multi-result by design. When multiple axioms match, you get all results. Ambiguity is data, not a bug.
• Semantically typed values. Props wrap values with meaning, not just types — absent(5) and star(5) are different objects in your system's algebra even though both contain 5.
• Export to four formats. The same system runs in Python, exports to Prolog, Z3, and PDDL with no rewriting.

Installation

pip install newn

Requires Python 3.8 or later. No mandatory dependencies — pure Python.

---

Main Concepts

Props — semantic wrappers

A prop wraps a value and gives it a named identity within your system. Two props with the same inner value are different objects — the prop name is part of the identity, not just metadata.

prop absent: None
prop star:   None
prop quantum: None

a = absent(5)    # PropValue('absent', 5)
b = star(5)      # PropValue('star', 5)
c = quantum(5)   # PropValue('quantum', 5)

# a, b, and c are three different values in your system

Props can nest:

deep = absent(star(3))   # PropValue('absent', PropValue('star', 3))

---

Ops — operations defined entirely by axioms

An op has no built-in meaning. It only does what its axioms say. With no matching axiom, it raises NewnError.

op combine: None
op scale:   None
op project: None

Binary ops use infix notation.

result = absent(3) combine star(4)   # infix

---

Axioms — the rules of your system

Axioms define what ops do. Each axiom fires when its pattern matches the call's arguments.

axiom plain_add:  [for all x, for all y],           x add y         = x + y
axiom absent_add: [for all x, for all absent(y)],   x add absent(y) = absent(x + y)
axiom star_add:   [for all x, for all star(y)],     x add star(y)   = star(x + y)

---

Categories — named domains

A category is a named set of values defined by a condition. Use it to scope axioms to a subset of inputs.

category small:   [for all x in range(0, 10)], absent(x)

Then constrain axiom variables to categories:

axiom discount: [for all x in small, for all y], x add y = absent(y)

Prop-union categories combine multiple props:

category typed_val: [for all x], absent(x) and star(x)   # values that are absent OR star wrapped

Unresolved categories — categories defined by the output of an op, enabling higher-order dispatch:

axiom double: [for all x, for all y], double(x) add y = y add double(x)

category result_of_double: [for all x], double(x) add y

#Arguments of the unresolved can be accessed through x.1 (1st arg) - x.n

---

Multiple matching axioms — MultiResult

When two or more axioms all match the same call, Newn returns a MultiResult — a list of all results in axiom-definition order. A single match returns the value directly, no wrapping.

op classify: None
axiom zero: [for all x], classify(0) = "zero"   # matches literal 0
axiom any:  [for all x], classify(x) = "other"  # matches everything

r = classify(0)    # MultiResult(['zero', 'other']) — both axioms fired
s = classify(99)   # 'other' — only one axiom fired, plain value returned

Use first() inside .nn to extract only the first matching result (explicit first-match-wins):

r = first(classify(0))   # 'zero'

Use op.all() from Python to get all results with their axiom names:

results = ns['classify'].all(0)
# [('zero', 'zero'), ('any', 'other')]

---

Ground axioms — constant facts

A ground axiom fires only for exact inputs. No variables. Auto-recorded at definition time.

axiom base_case: [None], fact(0) = 1
axiom next_case: [None], fact(1) = 1
axiom two:       [None], fact(2) = 2
axiom six:       [None], fact(6) = 720

---

Prop-family axioms

An axiom can fire for an entire family of props at once using a numeric index variable:

op lift: None
axiom gen: [for all n, for all pn(x)], lift(pn(x)) = pn(x + 1)

This fires for p0(3) → p0(4), p7(1) → p7(2), and any pN(x) — one axiom covers the whole family. The n variable must be consistent across both sides.

---

Recursion guard — symbolic expressions

When an axiom's RHS would recursively call itself with the same pattern, the engine records the call as an UnresolvedExpr instead of looping. This is how Newn produces symbolic unevaluated expressions you can inspect and pattern-match later.

axiom hold: [for all absent(x), for all y], absent(x) add y = absent(x) add y

result = absent(5) add 7
print(result)         # absent(5) add 7
print(type(result))   # UnresolvedExpr

---

DotAccessPat — deconstructing unresolved categories

Access the inner components of an UnresolvedExpr using .N notation:

axiom new2: [for all x, for all y], x add absent(y) = absent(y) add x
category nop: [for all x, for all y], absent(y) add x
axiom futnew: [for all x in nop, for all y], x cube y = (x.2 + y) add x.1
coq = 6 add absent(7)
print(coq cube 7)

---

Prop-family ops via Python-backed definitions

Import any Python callable as a Newn op:

from_python: math.sqrt as sqrt_op
from_python: operator.add as py_add

result = sqrt_op(16)    # 4.0
result2 = 3 py_add 4    # 7

---

Multi-file support

include "base_domain.nn"
include "extensions/extra.nn"

axiom my_extension: ...

Paths resolve relative to the file containing the include directive.

---

Bind — language translation boundaries

Map Newn values to and from external representations:

prop fib: None
bind f5: fib(5) == [21]   # fib(5) displays and exports as 21

result = translate_out(fib(5))   # 21
back   = translate_in(21)        # fib(5)

Bind tables are included in all export formats.

---

VisualDict — readable prop representations

Control how PropValues print for human-readable output:

prop degree: None
vd = VisualDict({0: "none", 1: "low", 2: "medium", 3: "high"})
prop degree: vd

d = degree(2)
print(d)   # degree(medium)

---

Backtracking

Structural backtracking — the default

Given a pattern, find all axioms whose LHS or RHS structurally matches it — then return the opposite side. No execution needed.

op add: None
axiom plain: for all x, for all y, x add y = x + y

hits = {[for all x, for all y], x add y}

hits is a BacktrackResult containing the RHS pattern x + y — found by matching the LHS structurally.

Going the other direction:

reverse = {[for all x, for all y], x + y}   # finds: x add y

Results display as matched_side → opposite_side.

Use .values(), .bindings(), and .sources() to inspect:

bt = ns['hits']
print(bt.values())    # ['x + y']
print(bt.sources())   # ['plain']
print(bt.items())     # [(bindings, value, axiom_name), ...]

Structural backtracking in Python

from newn.core import _ENGINE

results = _ENGINE.backtrack_structural(['x', 'y'], 'x add y')

Explicit structural mode

hits = {[for all x, for all y], x add y, structural}

Identical to the default — , structural is explicit confirmation of the mode.

---

Debug tools

All available inside .nn scripts and nn_exec code blocks:

Tool	Description
trace_on()	Print every axiom that fires as it fires
trace_off()	Stop tracing
show(value)	Pretty-print a value with its type information
which_axioms("op_name")	List all axioms registered for an op
explain("op", arg1, arg2)	Which axiom would fire for these exact arguments?
coverage("op_name")	Static coverage analysis — which input classes are handled?
why_not("op", arg1, arg2)	Explain why no axiom fired

Example:

trace_on()
r = 3 add absent(4)
trace_off()

explain("add", 3, absent(4))
coverage("add")
why_not("add", absent(3), absent(4))

---

Export

Prolog

from newn.export import export_prolog

nn_exec('...')
export_prolog('domain.pl')

Generates a loadable SWI-Prolog file:

?- consult('domain.pl').
?- add(3, 4, R).   % R = 7

Z3

from newn.export import export_z3
export_z3('domain_z3.py')

Generates a Z3 Python script with ForAll constraints for every axiom.

PDDL

from newn.export import export_pddl
export_pddl('domain.pddl')

Generates a PDDL domain file for use with planners like Fast Downward.

Python module

from newn.export import export_python
export_python('my_domain_api.py')

Generates a self-contained Python module that re-initialises the engine on import and exposes every op as a regular Python function.

---

Command-line interface

Run a .nn file:

python -m newn myfile.nn

Show the generated Python before running it:

python -m newn --transform myfile.nn

---

Full example — custom number system with categories using a .nn file

category unresolved: [for all x, for all y], absent(x) add y
axiom truth: [for all absent(x), for all y], absent(x) add y = absent(x) add y
axiom newtruth: [for all x in unresolved, for all y], x newad y = x.1 add (x.2 + y)
news = absent(5) add 7
fire = news newad 3
axiom forever: [for all x, for all y, for all z], absnet(z(x)) forevez z(y) = z(x(y))
axiom new: [for all x], x nop x = double(x)
axiom new2: [for all x, for all y], x op y = x(y)
axiom fifthen: [for all x, for all y], x(x) ching y = y ching x(x)
category unresolved: [for all x, for all y], x(x) ching y
axiom furyfire: [for all x in unresolved], x five x.2 = fuel(x.1) 
newfine = {[for all x, for all y, for all z], z(x(y))}
supback = {[for all x, for all y], y ching x(x)}
axiom newcan: [for all x, for all y, for all z], z(x) supadd y = z
axiom newcan: [for all x, for all y, for all z], z(x) supadd y = y
print(5(7) supadd 8)
print(supback)
print(newfine)
dict = {1: "happy", 2: "news", 3: "double"}
print(dict[1 op 3])
print(dict[1 nop 1])

---

Still in Construction

⚠ Warning — Probe-based backtracking is not yet fully operational.

The probe mode ({[for all x], pattern, probe}) executes axioms against test values to find matches. This feature is under active development and may produce incomplete or incorrect results in complex axiom systems. Use structural backtracking (the default) for reliable results.

⚠ Warning — Safety Net is not yet fully operational.

The SafetyNet class (from newn import SafetyNet) provides an API for validating external (e.g., neural network) outputs against your axiom rules, exporting rules as JSON or LLM prompts, and serving a local HTTP endpoint. The API surface is in place but the validation engine is under active development. Do not use SafetyNet in production workflows yet.

---

API Reference

Execution

Name	Description
nn_exec(code, *, base_dir=None)	Execute .nn code string; return namespace dict
nn_exec_file(path)	Execute a .nn file; return namespace dict
nn_transform(code)	Return the generated Python source without running it

Backward chaining

Name	Description
backchain(engine, op, target)	Symbolic inverse — find inputs that produce target
query(engine, op, target, domain)	Search over domain for inputs that produce target
prove(engine, op, *args)	Returns True if the call resolves to a concrete value

Types

Name	Description
PropValue(name, value)	A value wrapped with a named property
UnresolvedExpr(op, args)	A symbolic, unevaluated expression
BacktrackResult	Result of a {} backtrack query; iterable, has .values(), .bindings(), .sources(), .items()
MultiResult	List subclass returned when 2+ axioms match; supports indexing, len(), iteration
Category	Named category object; call .contains(value) to test membership
UnresolvedCategory	Category defined by op output membership
VisualDict	Mapping from inner values to display strings for prop printing
AxiomEngine	The runtime engine; access via ns['_nn_engine']

Errors

Name	Raised when
NewnError	Generic Error
NewnSyntaxError	.nn code has a syntax problem
AxiomNotFoundError	Specific axiom name not found
CategoryError	Category constraint violated
PatternError	Pattern matching failure

Export

Name	Description
export_prolog(path)	Write a SWI-Prolog .pl file
export_z3(path)	Write a Z3 Python script
export_pddl(path)	Write a PDDL domain file
export_python(path)	Write a self-contained Python API module

Multi-result

Expression	Returns
op(args)	Single value if one axiom matches; MultiResult if 2+ match
first(op(args))	Always a single value — the first matching axiom's result
op.all(args)	[(axiom_name, value), ...] for every matching axiom

---

.nn Language Quick Reference

# Comments
prop name: None                              # declare a prop
op name: None                                # declare an op

# Simple axiom
axiom label: for all x, for all y, x op y = x + y

# Bracket form (per-variable constraints)
axiom label: [for all x, for all absent(y)], x op absent(y) = absent(x + y)

# Range-constrained variable
axiom label: [for all x in range(0, 10)], process(x) = x * 10

# Category-constrained variable
axiom label: [for all x in small], process(x) = small(x)

# Ground axiom (no variables)
axiom exact: [None], 3 op 4 = 99

# Template op (prop family)
axiom gen: [for all n, for all pn(x)], lift(pn(x)) = pn(x + 1)

# Ground axiom (structural) backtracking
hits = {[for all x, for all y], x op y}

# Explicit structural
hits = {[for all x, for all y], x op y, structural}

# first() — first matching axiom's result
r = first(x op y)

# Include another file
include "other.nn"

# Python-backed op
from_python: math.sqrt as sqrt_op

# Bind (translation table)
bind label: prop(value) == [external_value]

---

License

MIT