# referential math notation (rmn) specification
an ascii plaintext math notation

# identifiers, types, and function application
use lowercase ascii identifiers with underscores.
type annotations follow the form:
```
function_name(arg1: type1, arg2: type2): return_type
```
all operations use explicit prefix calls:
```
contains(set, element)
compose(f, g)
product(type_a, type_b)
```

# struct and module declarations
```
type group:
  id: string
  start_time: time
  duration: time
```
```
module potential_mounting:
  function referenced_groups(p: potential): list<group> = ...
  function root_group(p: potential): group = ...
```

# functions
```
function root_group(p: potential): group =
  find_shallowest(mounted_groups(p))
```
functions are total and context-free.
no overloading. no implicit dependencies.

# definitions and scoping
group related functions in bundled blocks:
```
potential_analysis:
  function root_group(p: potential): group = ...
  function evaluate_window(p: potential): (time, duration) =
    let g = root_group(p)
    in (g.start_time, g.duration)
```
allow lexical scoping with `let`, `match`, and block structure.

# quantification and iteration
replace symbolic quantifiers with iteration:
```
for g in all_groups:
  for p in referenced_potentials(g):
    evaluate_window(p, g)
```
use existential forms as needed:
```
for epsilon in positive_reals:
  exists delta in positive_reals:
    for x in reals:
      if abs(x - c) < delta:
        abs(f(x) - l) < epsilon
```

# indexing and summation
use explicit index binding:
```
sum(i: 1..n, a[i][j] * b[j][k])
```
define arrays as typed functions:
```
a: function(i: int, j: int): real
```

# function composition and pipelines
write composition and dataflow explicitly:
```
compose(g, f)(x) = g(f(x))
pipe(x, f, g) = g(f(x))
```
always declare domain and codomain:
```
f: function(x: a): b
g: function(y: b): c
```

# avoiding point-free style
avoid combinators and implicit flows. use named expressions:
```
delta(x) = (x, x)
pair(x) = (x, f(x))
```

# operator precedence
enforce full parenthesization:
```
sub(add(1, div(mul(2, pow(c, d)), e)), f)
```
optional infix dsls must define evaluation precedence explicitly.

# set comprehension
replace set-builder notation with functional constructs:
```
filter(x in reals, x*x < 2)
```
define derived sets explicitly:
```
def bounded_square_root_domain(): set<real> =
  filter(x in reals, x*x < 2)
```

# ranges and sequences
avoid `...`. use explicit ranges and generators:
```
sum(i: 1..n, i)
sequence(n: int): list<int> = map(i: 1..n, i)
```

# algebraic data types
support tagged sum types using variant syntax:
```
type expr =
  | number(value: real)
  | variable(name: string)
  | binary(op: operator, left: expr, right: expr)
```

# anonymous functions
allow inline function expressions:
```
map(list, function(x): x * x)
```

# preconditions and partial domains
define domains of partial functions explicitly:
```
function log(x: real): real
  precondition: x > 0
```
or use guarded total forms:
```
function log(x: real): real?
  if x > 0 then return natural_log(x)
```

# logic and proof annotations
represent predicates as first-class functions:
```
predicate is_prime(n: int): bool
```
annotate proofs as data when needed:
```
proof: exists p in primes: divides(p, n)
```

# error and result types
support result-returning functions for safe operations:
```
function safe_sqrt(x: real): result<real, error>
```

# symbol definitions and traits
define all functions explicitly:
```
phi: function(x: group_elem): group_elem = ...
```
use traits where needed:
```
trait group_homomorphism:
  function map(x: group_elem): group_elem
```

# notation expansion
allow symbolic shorthands through scoped definitions:
```
namespace innerproductspace:
  function inner(x: vector, y: vector): scalar
  notation: "⟨x, y⟩" maps to inner(x, y)
```
all notation must be expandable to referential form.

# additional constructs
partial functions with guards:
```
function safe_div(x: real, y: real): real?
  if y ≠ 0 then return x / y
```
first-class predicates:
```
is_even: function(n: int): bool = mod(n, 2) == 0
```
pattern matching on records:
```
match g as group:
  id = g.id
```
tagged functions with traits:
```
φ: map g -> h where φ is group_homomorphism
```

# examples
here are a few examples from traditional mathematics that are ideal for showcasing the clarity and compositional benefits of rmn. each is representative of a different domain and difficult to follow without prior symbolic fluency.

## epsilon-delta definition of limit (analysis)
traditional:
```math
∀ε > 0 ∃δ > 0 ∀x (0 < |x - c| < δ ⇒ |f(x) - l| < ε)
```
rmn:
```
for epsilon in positive_reals:
  exists delta in positive_reals:
    for x in reals:
      if 0 < abs(x - c) and abs(x - c) < delta:
        abs(f(x) - l) < epsilon
```

## functoriality and composition (category theory)
traditional:
```math
f(g ∘ f) = f(g) ∘ f(f)
```
rmn:
```
compose(f(g), f(f)) = f(compose(g, f))
```

## matrix multiplication (linear algebra)
traditional:
```math
c_{ik} = ∑_{j=1}^{n} a_{ij} b_{jk}
```
rmn:
```
c(i, k) = sum(j: 1..n, a(i, j) * b(j, k))
```

## set-builder and predicate logic (set theory / logic)
traditional:
```math
{x ∈ ℕ | ∃y ∈ ℕ, y² = x}
```
rmn:
```
filter(x in naturals, exists y in naturals: y * y = x)
```

## defining an inner product space (linear algebra / functional analysis)
traditional:
```math
⟨x, y⟩ = ∑_{i=1}^{n} xᵢ yᵢ
```
rmn:
```
inner(x: vector, y: vector): scalar =
  sum(i: 1..n, x(i) * y(i))
```

## pointwise function equality (set functions / logic)
traditional:
```math
f = g ⇔ ∀x ∈ a, f(x) = g(x)
```
rmn:
```
functions_equal(f, g, domain) =
  for x in domain:
    f(x) = g(x)
```

# canonical translation examples
```
∀x ∈ a: p(x)                         -> for x in a: p(x)
∃x ∈ a: p(x)                         -> exists x in a: p(x)
f ∘ g                                -> compose(f, g)
x ∈ a                                -> contains(a, x)
a × b                                -> product(a, b)
{ x ∈ ℝ | x² < 2 }                   -> filter(x in reals, x * x < 2)
1 + 2 + ... + n                      -> sum(i: 1..n, i)
∑_{i=1}^{n} f(i)                     -> sum(i: 1..n, f(i))
a[i][j]                              -> a(i, j)
let f: g -> h                         -> f: function(x: g): h
⟨x, y⟩                               -> inner(x, y)
id × f                               -> product(id, f)
δ(x)                                 -> (x, x)
(x, f(x))                            -> pair(x) = (x, f(x))
φ is a group homomorphism            -> φ: function(x: group_elem): group_elem satisfies group_homomorphism
f: a -> b, g: b -> c, h = g ∘ f        -> f: function(x: a): b, g: function(y: b): c, h(x) = compose(g, f)(x)
x ∈ dom(f)                           -> contains(domain(f), x)
∀ε > 0 ∃δ > 0 ∀x |x−c|<δ ⇒ ...       -> for epsilon in positive_reals: exists delta in positive_reals: for x in reals: if abs(x - c) < delta: ...
log(x), x > 0                        -> function log(x: real): real? if x > 0 then return natural_log(x)
{1, 2, ..., n}                       -> range(1, n)
λx. f(x)                             -> function(x): f(x)
~ x                                  -> not(x)
a ∩ b                                -> intersection(a, b)
a ∪ b                                -> union(a, b)
a ⊆ b                                -> subset(a, b)
a ∖ b                                -> difference(a, b)
true                                 -> true
false                                -> false
¬p ∨ q                               -> or(not(p), q)
p ∧ q                                -> and(p, q)
p ⇒ q                                -> implies(p, q)
p ⇔ q                                -> iff(p, q)
min(x₁, ..., xₙ)                     -> reduce(min, [x1, ..., xn])
max(x₁, ..., xₙ)                     -> reduce(max, [x1, ..., xn])
lim_{x->a} f(x)                       -> limit(f, x -> a)
d/dx f(x)                            -> derivative(f, x)
∫₀ⁿ f(x) dx                          -> integral(f, x, lower=0, upper=n)
a = b = c                            -> a = b and b = c
a ≠ b                                -> not(a = b)
if x ∈ a then y ∈ b                 -> if contains(a, x): contains(b, y)
```

# desugaring table
this table ensures that all high-level rmn constructs are syntactic sugar over a minimal, core language with function application, binding, types, and blocks.

## implicit ranges
```
sum(i: 1..n, expr)
```
->
```
sum(i in range(1, n), expr)
```

## pipeline
```
pipe(x, f, g)
```
->
```
g(f(x))
```

## function composition
```
compose(f, g)(x)
```
->
```
f(g(x))
```

## array notation
```
a[i][j]
```
->
```
a(i, j)
```

## anonymous function (lambda)
```
function(x): expr
```
->
```
lambda_expr(param = x, body = expr)
```

## set filtering
```
filter(x in domain, condition)
```
->
```
filter(domain, function(x): condition)
```

## optional types
```
real?
```
->
```
optional<real>
```

## precondition
```
function f(x: t): u
  precondition: p
```
->
```
function f(x: t): u?
  if p then return <body>
```

## record match
```
match r as t:
  f1 = ...
  f2 = ...
```
->
```
let f1 = r.f1
let f2 = r.f2
```

## shorthand trait tagging
```
φ: map g -> h where φ is group_homomorphism
```
->
```
φ: function(x: group_elem): group_elem
  satisfies group_homomorphism
```

# ebnf grammar sketch
```
program          ::= (definition | type_decl | module_decl)*
definition       ::= "function" identifier "(" param_list ")" ":" type ("=" expr | block)
                  | "predicate" identifier "(" param_list ")" ":" "bool"
                  | "proof" ":" expr
type_decl        ::= "type" identifier ":" field_list
                  | "type" identifier "=" variant_list
module_decl      ::= "module" identifier ":" block
variant_list     ::= variant ("|" variant)*
variant          ::= identifier "(" field_list ")"
field_list       ::= field ("," field)*
field            ::= identifier ":" type
param_list       ::= param ("," param)*
param            ::= identifier ":" type
block            ::= indent (definition | expr)* dedent
expr             ::= call_expr
                  | if_expr
                  | match_expr
                  | lambda_expr
                  | literal
                  | identifier
call_expr        ::= identifier "(" arg_list ")"
arg_list         ::= expr ("," expr)*
if_expr          ::= "if" expr "then" expr ("else" expr)?
match_expr       ::= "match" identifier "as" identifier ":" field_list
lambda_expr      ::= "function(" identifier ")" ":" expr
literal          ::= number | string | boolean
type             ::= identifier | type "?" | "list<" type ">" | "set<" type ">" | "result<" type "," type ">"
```
note: indentation-based syntax is assumed. sugar constructs (like `sum(i: 1..n, ...)`) must desugar into core forms.