an ascii plaintext math notation

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)

type group:
  id: string
  start_time: time
  duration: time

module potential_mounting:
  function referenced_groups(p: potential): list = ...
  function root_group(p: potential): group = ...

function root_group(p: potential): group =
  find_shallowest(mounted_groups(p))

functions are total and context-free. no overloading. no implicit dependencies.

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.

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

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

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

avoid combinators and implicit flows. use named expressions:

delta(x) = (x, x)
pair(x) = (x, f(x))

enforce full parenthesization:

sub(add(1, div(mul(2, pow(c, d)), e)), f)

optional infix dsls must define evaluation precedence explicitly.

replace set-builder notation with functional constructs:

filter(x in reals, x*x < 2)

define derived sets explicitly:

def bounded_square_root_domain(): set =
  filter(x in reals, x*x < 2)

avoid .... use explicit ranges and generators:

sum(i: 1..n, i)
sequence(n: int): list = map(i: 1..n, i)

support tagged sum types using variant syntax:

type expr =
  | number(value: real)
  | variable(name: string)
  | binary(op: operator, left: expr, right: expr)

allow inline function expressions:

map(list, function(x): x * x)

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)

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)

support result-returning functions for safe operations:

function safe_sqrt(x: real): result

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

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.

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

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.

∀ε > 0 ∃δ > 0 ∀x (0 < |x - c| < δ ⇒ |f(x) - l| < ε)

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

f(g ∘ f) = f(g) ∘ f(f)

compose(f(g), f(f)) = f(compose(g, f))

c_{ik} = ∑_{j=1}^{n} a_{ij} b_{jk}

c(i, k) = sum(j: 1..n, a(i, j) * b(j, k))

{x ∈ ℕ | ∃y ∈ ℕ, y² = x}

filter(x in naturals, exists y in naturals: y * y = x)

⟨x, y⟩ = ∑_{i=1}^{n} xᵢ yᵢ

inner(x: vector, y: vector): scalar =
  sum(i: 1..n, x(i) * y(i))

f = g ⇔ ∀x ∈ a, f(x) = g(x)

functions_equal(f, g, domain) =
  for x in domain:
    f(x) = g(x)

∀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)

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

sum(i: 1..n, expr)

sum(i in range(1, n), expr)

pipe(x, f, g)

g(f(x))

compose(f, g)(x)

f(g(x))

a[i][j]

a(i, j)

function(x): expr

lambda_expr(param = x, body = expr)

filter(x in domain, condition)

filter(domain, function(x): condition)

real?

optional

function f(x: t): u
  precondition: p

function f(x: t): u?
  if p then return 

match r as t:
  f1 = ...
  f2 = ...

let f1 = r.f1
let f2 = r.f2

φ: map g -> h where φ is group_homomorphism

φ: function(x: group_elem): group_elem
  satisfies group_homomorphism

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.