2025-10-06

ascii plaintext math notation

definition

identifiers

identifier ::= ascii_lower | ascii_lower_with_underscores

functions

function ::= "function" name "(" arg ":" type ... ")" ":" type ["=" expr]
application ::= name "(" expr ... ")"
lambda ::= "function(x):expr" -> "lambda_expr(param=x,body=expr)"

types

struct ::= "type" name ":" field ":" type ...
trait ::= "trait" name ":" function
adt ::= "type" name "=" variant ...
variant ::= "|" constructor "(" field ":" type ... ")"
module ::= "module" name ":" definition ...
optional ::= type "?" -> "optional"

blocks

block ::= "let" binding "in" expr
        | "match" expr "as" id ":" block ...

quantification and iteration

iteration ::= "for" var "in" domain ":" expr
exists ::= "exists" var "in" domain ":" expr

arrays, indexing, summation

array ::= "function" "(" indices ")" ":" type
indexing ::= a "[" i "]" ... -> a(i, ...)
sum ::= "sum(" var ":" range "," expr ")"
desugar ::= "sum(i:1..n, expr)" -> "sum(i in range(1,n), expr)"

notation and desugaring

compose(f, g)(x) -> f(g(x))
pipe(x, f, g) -> g(f(x))
filter(x in domain, condition) -> filter(domain, function(x):condition)
notation ::= symbolic -> referential
trait_tag ::= phi: map g -> h where phi is T
           -> phi: function(x:tau):tau satisfies T

summary

identifier ::= ascii_lower | ascii_lower_with_underscores
function ::= "function" name "(" arg ":" type ... ")" ":" type ["=" expr]
application ::= name "(" expr ... ")"
lambda ::= "function(x):expr" -> "lambda_expr(param=x,body=expr)"
struct ::= "type" name ":" field ":" type ...
trait ::= "trait" name ":" function
adt ::= "type" name "=" variant ...
module ::= "module" name ":" definition ...
optional ::= type "?" -> "optional"
block ::= "let" ... | "match" ...
iteration ::= "for" var "in" domain ":" expr
exists ::= "exists" var "in" domain ":" expr
array ::= "function" "(" indices ")" ":" type
indexing ::= a "[" i "]" ... -> a(i,...)
sum ::= "sum(" var ":" range "," expr ")"
notation ::= syntactic sugar -> core form

examples (ascii only, desugared)

epsilon-delta:

for epsilon in positive_reals:
  for delta in positive_reals:
    for x in reals:
      if (0 < abs(x - c)) and (abs(x - c) < delta):
        condition = abs(f(x) - l) < epsilon

matrix multiplication:

c(i, k) =
  sum(j in range(1, n),
    a(i, j) * b(j, k))

set-builder:

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

inner product:

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

pointwise equality:

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

shorthand trait tagging:

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

minimal core

  • functions
  • type definitions
  • blocks
  • iteration and quantification
  • arrays and sums
  • lambdas
  • primitive data and operators all other forms desugar to these.