Metadata-Version: 2.4
Name: newn
Version: 1.0.0
Summary: Newn — define new mathematical systems through properties, categories, and axioms. Symbolic reasoning, bidirectional backtracking, and multi-format export.
Home-page: https://github.com/jordanbeitchman-spec/PhantomTrace
Author: Newn Project
License-Expression: MIT
Project-URL: Homepage, https://github.com/jordanbeitchman-spec/PhantomTrace
Project-URL: Documentation, https://github.com/jordanbeitchman-spec/PhantomTrace#readme
Project-URL: Issues, https://github.com/jordanbeitchman-spec/PhantomTrace/issues
Keywords: math,symbolic-reasoning,axioms,domain-specific-language,term-rewriting,formal-systems,logic,algebra,backtracking,ai
Classifier: Development Status :: 5 - Production/Stable
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Intended Audience :: Education
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.8
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Classifier: Topic :: Software Development :: Libraries :: Python Modules
Classifier: Topic :: Software Development :: Compilers
Requires-Python: >=3.8
Description-Content-Type: text/markdown
License-File: LICENSE
Dynamic: home-page
Dynamic: license-file
Dynamic: requires-python

# Newn

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

```bash
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

```bash
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:

```python
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:

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

### Structural backtracking in Python

```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

```python
from newn.export import export_prolog

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

Generates a loadable SWI-Prolog file:

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

### Z3

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

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

### PDDL

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

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

### Python module

```python
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:

```bash
python -m newn myfile.nn
```

Show the generated Python before running it:

```bash
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
