Axioma Programming Language Manual

Version 0.9   ·   Calculemus! — Leibniz A multi-paradigm language for mathematics, logic, knowledge, and reasoning.

Calculemus! is Latin for "Let us calculate!" — the motto of the philosopher and mathematician Gottfried Wilhelm Leibniz (1646–1716), co-inventor of the calculus. Leibniz dreamed of a characteristica universalis: a formal language in which any idea could be written down exactly, paired with a calculus ratiocinator, a mechanical procedure for reasoning over it. Then, he wrote, two people who disagreed would no longer need to quarrel — they could take up their pens and say "Calculemus" ("let us calculate") and settle the matter by reckoning. Axioma is a step toward that vision: a language where logic, mathematics, and knowledge are things you compute with.

1. Introduction

Axioma is the language in which formal philosophy and symbolic logic become executable: a natural-language-readable surface over a first-class epistemic kernel — concepts, epistemic grounding, defeasible rules, and checkable proof. Where most languages compute plain values, Axioma computes values that carry their epistemic status: a fact's derivation provenance (its grounding), whether it is contradicted, and whether an answer is decidable at all. Its flagship demonstration is a runnable formalization of praxeology (the Rothbard corpus), carried end-to-end by that kernel with no special-case machinery.

Around that kernel, Axioma blends styles freely — set theory, first-order logic, multi-valued logics, lambda calculus, frame-based concepts, relational logic programming, stack-based programming, and natural-language definitions live side by side and compose with each other. The surface is deliberately consolidating, not accreting: redundant spellings are retired over time toward one canonical form per idea (see §3), so expressive breadth does not buy a second way to say the same thing.

Key features

• Concept system with natural-language syntax (concept Stock, Stock has price: 150).
• Logic programming through deterministic, set-based pattern queries — Prolog-like relations without implicit depth-first backtracking.
• Six-grade epistemic grounding: every fact carries a grade on the ladder axiom > postulate > theorem > conjecture > hypothesis > datum, propagated through derivation as provenance.
• Five first-class logics: Boolean, Kleene K3, Łukasiewicz L3, Belnap B4, Gödel G3 (intuitionistic), automatically dispatched by operand type.
• Strict and defeasible rules in both backward and forward directions.
• Bilattice truth values with paraconsistent contamination (Belnap B4).
• SQLite-backed knowledge base shared with Cascade.
• Stack programming with both a user-accessible Stack type and a global interpreter stack.
• MCP server exposing tools for AI-assistant integration.
• Tools: axiomadoc (literate programming), VM mode, Wails GUI, web GUI, Jupyter kernel.

Influences

Axioma stands in a long line of languages and gratefully adapts the best of them, just as most languages do. For the record, the main lineages are:

• REBOL — the : value binding, the family of scalar value literals (URL, email, file, money, pair, issue, …), the get-word (:w), refinements (name/ref), and the value-returning (non-throwing) error model.
• Forth / Pop-11 — the stack model: the global interpreter stack, the postfix sequence notation, and the stack-shuffle verbs.
• SETL — set-theoretic data structures, comprehensions, bags, and the om / Ω undefined value.
• Lisp / Scheme — the ' quote (the 'w word literal), homoiconicity (code as data), and the S-expression view of the AST; Mathematica — fullform for viewing the AST as a symbolic expression.
• Prolog / Datalog — relational facts, rules, and queries.
• F-logic & Description Logic — the concept system: frame slots and the concept↔︎relation↔︎rule duality (F-logic), and subsumption / satisfiability reasoning over a tableau (Description Logic / ALC).
• Python, Haskell, Racket, Rust, Swift — assorted surface conveniences (comprehension spellings, string-escape and byte syntax, list accessors).

2. Getting Started

Installation

# Source checkout. If the repository is not publicly reachable yet, use the
# browser playground for zero-install evaluation until release archives are linked.
git clone https://github.com/vevenhar/axiomalang.git
cd axiomalang
go build -o axioma ./cmd/axioma/
./axioma --help
./axioma                         # Start REPL

Run a script

./axioma path/to/script.ax                # Run a script
./axioma --no-kb script.ax                # Skip Cascade KB preload (~10× faster startup)
./axioma --vm script.ax                   # Run in VM mode
./axioma --mcp                            # Start MCP server (stdio JSON-RPC)

Feature status at a glance

The browser column means the WebAssembly playground core: no host file system, no subprocesses, and no local SQLite KB. The native tree-walker is the reference runtime for the whole public language surface. The VM is useful for the compiled core, but some higher-level forms are intentionally still tree-walker-only.

First steps

axioma> a: {1, 2, 3}
{1, 2, 3}
axioma> b: {2, 3, 4}
{2, 3, 4}
axioma> a union b
{1, 2, 3, 4}
axioma> concept Person
axioma> Person has name: "Alice"
axioma> parent("John", "Mary")
axioma> {Y | Y <- parent("John", Y)}
{"Mary"}

3. Language Fundamentals

Bindings — one canonical form

Axioma has a single canonical value-binding operator: :. It's the shortest binding form of any mainstream language (two characters of overhead), puts the name first, and composes naturally with type annotations.

x: 5                            # bare binding
radius: 3.14 * 2                # expression on the RHS
a, b, c: 1, 2, 3                # multi-assignment (parallel)
(x, n): (3, 2)                  # pattern binding (nested / constants / `_`)
let (x, n) = (3, 2)             # same, fresh declaration (ML `val`)
d :: Day: Mon                   # with type annotation

All variants compile to the same LetStatement AST node. A multi-assignment evaluates every right-hand side first and then binds (so a, b: b, a swaps), updates each name wherever it already exists within the enclosing function frame (declaring it here otherwise — exactly the single-name rule), and evaluates to the tuple of all assigned values, so the REPL echoes (1, 2, 3). A multi-assignment may also open a bracket block — if val > best then [ best, at: val, idx ] — the leading name, name run is recognized as a statement, not array elements, so branch bodies can start with a parallel update (both the : and = spellings; plain [a, b] stays an array). The axioma/beginner subset uses only the bare form; multi-assign and type annotations show up later in the curriculum.

Pattern binding (ML-style tuple patterns)

When the left-hand side is a tuple pattern in parentheses, the right-hand side is matched as a whole and the identifiers in the pattern are bound — the same idea as match pair with | (x, n) => …, but as a declaration:

let (x, n) = (3, 2)                 # x ↦ 3, n ↦ 2  (Fresh)
(x, n): (3, 2)                      # find-or-update (`:`)
(x, n) = (3, 2)                     # find-or-update (`=`)
[head | tail] = [1, 2, 3]           # array/cons pattern (Elixir)
let [h | t] = xs                    # fresh
{a, b} = {a: 1, b: 2}               # hash-shape (implicit names)
{a: x, b: y} = dict                 # hash-shape (renamed)
(^tag, result) = ('ok, 13)          # pin: slot equals current `tag`, does not rebind it
# `2^3` is still POWER. Pin is only `^name` in a pattern.

# Nested patterns, wildcards, and constant sub-patterns:
let ((a, b), c) = ((1, 2), 3)
((_, flag), _, done): ((1, true), junk, false)
let (payload, 0) = (lookup(), 0)    # only matches when the second slot is 0
('ok, result) = ('ok, 13)           # Word tag — result ↦ 13
# `:ok` is a get-word (it fetches a binding), not a tag. Write `'ok`.

A failed match (wrong arity, non-tuple value, or a constant that does not equal the corresponding component) raises a catchable error — SML's Bind exception. No name is left partially bound. A paren pattern matches only a Tuple (not an Array). An array/cons pattern [h | t] matches an Array or a List (the rest of a List stays a List), not a Dictionary — bind keys with {a, b} = dict, or pairs with [h | t] = items(dict). A hash-shape pattern {a, b} / {a: x} matches a Dictionary (extra keys allowed; a missing key is Bind). A pin ^x in a pattern constrains the slot to the current binding of x and does not bind or rebind x (unbound ^x is an error). The same identifier may not appear twice in a binding pattern (let (x, x) = … / [x | x] = … is a SyntaxError). Under --vm, pattern bindings are refused at compile time (evaluator-only, like match). Array literals, cons expressions, and comprehensions that are not followed by = / : keep their ordinary readings.

With --typecheck, a known product RHS (tuple literal or Tuple of (…) annotation) assigns each pattern variable its slot type and reports static arity mismatches, a tuple pattern against a non-tuple, and literal sub-patterns that cannot match their slot type.

= is a find-or-update synonym of :. = declares a name if it is absent and updates it if present — for any name and case — so textbook mathematics reads verbatim: B = {2, 4, 6}, C = A union B, Pi = 3.14159. : stays the canonical binding (and the form to learn first); = is the math/textbook spelling. (= is no longer strict-update-only.)

Casing is context-local, not a global type tag. Both : and = admit a name of any case — B: {2, 4, 6} and B = {2, 4, 6} are set variables. The right-hand side decides concept-vs-value: a concept { ... } RHS names a Concept (uppercase required — Stock: concept { ... }; a lowercase LHS with a concept RHS errors), while any other value binds an ordinary variable. Uppercase still means a logic variable inside rules (the Prolog convention) and is the Concept-naming convention — it just no longer forces a top-level binding to be a Concept.

A and E are ordinary identifiers, not quantifier shorthands. Quantify with forall / exists, the glyphs ∀ / ∃, the backtick digraphs `forall / `exists, or ∃! (unique existential). E! (the free-logic existence predicate) is a separate token.

There is no :=, and let is not an assignment. Bind with : (canonical) or =; x := value is a syntax error with an inline hint pointing at x: value. let x = value is a different construct entirely — a fresh, immutable declaration that shadows rather than updates (below), exactly the let of mathematical prose: "let x = 5" fixes x for the rest of the argument. Its mutable twin is var x = value (let mut x = value / let mutable x = value are the Rust / F# spellings of the same declaration), and val x = value is a second spelling of let for readers who arrive from Scala, Kotlin, or Standard ML. Ordinary :/= names remain cells that find-or-update can write.

Binding model at a glance

One page for the whole story. The rest of this section is detail; if something surprises you, it is almost always one of the rows below.

Why this shape (and not :=). Axioma is a teaching and multiparadigm language: : is the short Rebol-style binder; = must read as textbook mathematics (B = A union C, area(r) = pi * r * r) without a second “assignment only” operator. Unifying introduction and update under find-or-update is what makes accumulators work (total: total + n inside a loop). Around that default sit the explicit keywords for the directions it doesn't take: rebind when a closure or nested function must update a name outside its own frame, global when the write is Julia's module cell (this file / this module body), and the fresh pair — let for a genuinely new binding that then stays fixed (the let of mathematical prose, and of most functional languages), var for the rare fresh binding that must keep varying. let fixes here; var varies here; rebind reaches the nearest cell; global reaches this unit; bare :/= does the sensible middle.

val is a second spelling of let. Readers arriving from Scala, Kotlin, or Standard ML write val for the immutable binding, and Axioma accepts it: val x = 5 builds exactly what let x = 5 builds — same fresh cell, same shadowing, same write-refusal. It is not a spelling of var; var is the mutable twin and stays a distinct word. let remains the canonical spelling, and it is the majority one — Swift, Rust, Nim, F#, OCaml, Haskell, Elm, and Gleam all read let as immutable, as does mathematical prose ("let x = 5" fixes x for the rest of the argument).

One asymmetry, and it is deliberate: the pattern form stays on let. let (x, n) = pair destructures; val (x, n) = pair does not, because val(...) is already a function call and a language may not quietly take a shape that already parses. Write let when you are destructuring.

let mut / let mutable are second spellings of var. Readers arriving from Rust write let mut x = 5; readers arriving from F# write let mutable x = 5. Both build exactly what var x = 5 builds — same fresh cell, same shadowing, same writable cell. They are not spellings of let. mut and mutable are reserved words (a bare mut: 99 is a SyntaxError); guard the name ($mut) to use it as data. val mut is refused (val means immutable); var mut is refused as redundant; let/mut is not a refinement. The pattern form works: let mut (x, n) = pair is var (x, n) = pair.

# Value bind (canonical) and textbook synonym
radius: 5
area = pi * radius ^ 2

# Equation — definition, because of the parenthesized head
double(x) = 2 * x
fun triple(x) = 3 * x

# Binder shadows; body assignment stays in-frame
sum_all: func(xs) [
  total: 0
  foreach n in xs [total: total + n]    # writes this frame's total
  total
]

# Outer write must be spelled
counter: 0
bump: func() [rebind counter: counter + 1]

# Fresh declaration — a NEW, immutable binding; the closure above keeps its
# own counter, and `counter: 1` from here on is refused
let counter = 0

# Fresh AND mutable — `var` is `let` minus the write-refusal
var scratch = 0
scratch: scratch + 1

# The same declaration, Rust / F# spellings
let mut scratch2 = 0
scratch2: scratch2 + 1
let mutable scratch3 = 0
scratch3: scratch3 + 1

# Immutable name — program-level, top-level only
const LIMIT = 100

Not part of this table (see below): lazy declare / definitional define, persistence refinements, multi-assign, type annotations on bindings. Cross-frame mistakes that used to be silent outer writes are reported by axioma --lint (see rebind).

Regression pins: tests/axioma/binding/test_scoping_shadowing.ax, tests/axioma/binding/test_let_fresh_binding.ax, tests/axioma/binding/test_let_immutable_var.ax, tests/axioma/binding/test_let_var_vm_parity.sh, tests/axioma/binding/test_let_mut_alias.ax.

Fresh declarations with let and var

let NAME = value declares a new, immutable binding in the current scope. It never updates an existing name — where bare x = value finds-or-updates and rebind updates-only, let declares-only, shadowing any outer binding of the same spelling — and the binding it makes then refuses every write: x: 6, x = 6, and rebind x = 6 all error with a hint. This is the let of mathematical prose — "let x = 5" fixes x for the rest of the argument — and of most functional languages.

var NAME = value is let minus the write-refusal: the same fresh, shadowing, block-scoped declaration, with a cell that stays writable. It is deliberately the marked spelling, because it is rarely needed — : is already the mutable workhorse (accumulators never involve let), so var exists for the narrow case that must shadow an outer name and mutate the shadow. let mut NAME = value and let mutable NAME = value are the same declaration (Rust and F# spellings):

let fixed = 5
fixed: 6           # ERROR: Cannot reassign 'fixed': `let` bindings are
                   # immutable — declare it with `var fixed = ...` if it
                   # needs to change

var counter = 0
counter: counter + 1   # fine — var cells vary

let mut n = 0
n: n + 1               # same cell as var

Everything below applies to both spellings. A closure made before the declaration keeps the binding it captured:

x: 1
peek: func() [x]
let x = 2
peek()      # 1 — the closure still sees the old binding
x           # 2 — everything after the let sees the new one

Because the right-hand side evaluates before the new binding exists, let xs = split(xs) reads the outer xs and then takes over the name — the classic rebind-by-shadowing idiom. Every let makes a fresh binding, even for a name already let in the same scope, so consecutive let x = … lines each leave the previous binding alive inside anything that captured it.

The details:

• = only, exactly as const: let x: 5 is a SyntaxError with a hint. Annotations and multi-targets use the same grammar as bare bindings — let d :: Date = today(), let a, b = 1, 2 (all values evaluate before any binding, so let a, b = b, a swaps).
• Named declarations may omit their initializer: let x and let x :: T reserve unreadable cells, exactly like their = _ spellings. If = is written, its RHS must be an expression or an allowed marker (_ or typed default). Invented bottoms are refused; name what you mean with none, om, _, default, or a real value (see Uninitialized slots and identity defaults below).
• Reserved word (since August 2026). let, var, and val are keywords, so a bare let: 42 is a SyntaxError that names the fix. To use one of them as an ordinary name, guard it: $let: 42, func($val), h.$val, $val() = 1 — the same $ guard every reserved word takes. POP-11 word lists are the exception that needs no guard: [let x var y] is still the array ["let", "x", "var", "y"], because there the words are data.
• Scoped to its block. In a loop body the binding is per-iteration; in a branch or value block it dies with the block; at the top level and in a function body it lasts to the end of that scope.
• Shadowing a const is refused — the program-level name stays one thing. Shadowing a let is allowed, in both directions: let's immutability is cell-level, so an inner let, var, parameter, or loop variable of the same spelling is a new cell, not a write.
• var is the same grammar throughout — patterns (var (x, n) = pair), annotations, multi-targets, markers, the soft-keyword gate (var: 42 binds the name var), and the same loud limits below.
• Current limits, each a loud error rather than a quiet difference: let at the top level of an imported file, let inside a trace block, and — under --vm only — let inside a nested branch/value block.

Uninitialized slots and identity defaults

Three different intents people often collapse into one:

= _ (uninitialized). Requires a fresh named binding spelling; a :: type is optional. The slot holds binding state, not a third bottom: it is not none, not om, not 0. Reading before the first successful assignment is a hard error. Later x = v / x: v fills the same cell and re-checks any snapshotted annotation. Without an annotation, the first value does not impose a permanent type on a mutable cell. A failed RHS or conversion leaves the cell uninitialized. Under let the hole takes exactly one write — the fill — and is immutable from then on (deferred initialization, as in a proof that names a quantity before computing it); a slot you intend to keep refilling is a var hole. Under --vm, let x :: T = _ is a loud compile refusal (the one-write allowance cannot be checked statically); var x :: T = _ compiles.

The marker does not construct a value of T, so it needs no default value or empty constructor. Function and arrow annotations, user concepts, records, variants, schemas, and aliases can describe holes as well as primitive types. val shares let's one-fill rule; local, let mut and let mutable share var's refill rule.

let age :: Integer = _
# println(age)        # error: uninitialized
age = 89              # the fill — allowed once
# age = 90            # ERROR: Cannot reassign 'age'

var lifespan :: Integer | "ongoing" | "uncertain" = _
lifespan = 89
lifespan = "ongoing"  # var holes refill freely

let callback :: Function = _
callback = func(n) [n + 1]
println(callback(2))           # 3
concept Person
let person :: Person = _
person = a Person {}
println(person is Person)     # true
var amount :: Float = _
amount: 3
println(amount is Float)      # true: the fill performs numeric conversion

The snapshotted type belongs to that cell: shadowing it creates a different cell and does not replace an earlier closure's contract. Fills through =, :, rebind, global, or a writable binding reference retain the destination's type checks and conversions. Persistent Array element and schema contracts govern later mutations. Existing source-sensitive rules still apply: a schema annotation on a fresh dictionary literal rejects extra keys, while ordinary assignment can accept them (access remains restricted to the schema).

--typecheck tracks fills along reachable paths. Sequential reads and both if/else arms are checked; an arm that returns need not fill a cell read only after the branch. Unreachable statements contribute no initialization facts, while their ordinary type/annotation checks remain active. Short-circuit and fallback operands supply a definite fill only when execution requires it; unknown conditions retain a possible skipped path. This preserves the runtime distinction between Boolean short-circuiting and multivalued logic.

Loop bodies and conditions are checked in execution order. Pre-test loops retain a zero-iteration path unless the checker knows the initial condition is true. That proves a first iteration, not nontermination: the body may change the condition. Literal while true and infinite loops exit normally through break. Post-test repeat [body] until condition checks the body first; continue reaches the condition, while break bypasses it. Labeled exits reach their target loop. A match can join common fills across an unguarded catch-all, both Boolean cases, or all closed constructors with irrefutable fields. Other matches retain their implicit no-write fallthrough.

A fresh branch declaration, match pattern, or loop variable names a separate cell; filling it does not fill an outer namesake. Get-word :x fetches a value and refuses an uninitialized cell, just like ordinary x. Taking &x obtains the cell without reading its value; *p still requires a filled cell.

The checker recognizes positive literal repetition counts, simple bindings holding those counts, and known nonempty literal collections, strings and ascending closed integer ranges. Every reachable break/continue path must still supply the fill. It follows direct reference aliases by cell identity: p = &x; *p = 1 fills x, even if a later fresh declaration hides that cell. Caught errors preserve writes completed before failure; try, attempt, otherwise, catch handlers and finally blocks join their actual exit paths. A potentially failing conversion retains its pre-fill error path.

Defining a function or lazy computation does not execute captured reads or writes. Body-local holes are checked independently. Simple known function calls also check captured reads and summarize writes through rebind or reference parameters, including normal returns and errors. Ordinary assignment inside a function still follows that function's local-write rule.

Known calls support fixed positional parameters, defaults, named arguments (including positional tags), and positional rest arguments. Defaults are analyzed at the call, in declaration order, only for omitted arguments; earlier converted parameters are available to later defaults. A default that fails before the body contributes no body writes. Exact Integer +, -, * and comparisons can supply evidence for a count or condition; folding is bounded and does not invoke user operators.

local answer
fill = func(n = 42) [rebind answer = n]
fill()
println(answer)                # 42; passes --typecheck

Initialization diagnostics distinguish a definite early read (the tracked cell is unfilled) from a possible early read (some paths may leave it unfilled). An analysis incomplete note marks an opaque call; a later read may also receive a possible-read diagnostic. Both read diagnostics stop --typecheck; the note alone is informational. Default execution warns and retains runtime read checks. This distinction changes the explanation, not the rule that a read requires a successful fill.

Repeated known calls can reuse a bounded context-specific effect summary when argument values, captured cells, readiness and alias facts agree. Normal and error exits are recorded separately. Changed facts trigger fresh analysis; opaque effects and escaping fresh cells prevent summary reuse.

This is bounded initialization analysis, not a complete safety proof. Unknown calls, recursion, multiple clauses, partial applications, named arguments combined with rest parameters, lazy/refinement/structural-pattern parameters, function-local global marks and arbitrary contracts remain conservative. Opaque effects discard uncertain alias/callable and collection facts; writes are never guessed. Loop-carried aliases and arbitrary nonemptiness require runtime enforcement. These rules are shared by all six fresh binding spellings and by typed or untyped bare declarations and explicit = _. An explicit annotation remains valid even when the checker cannot model it precisely (for example, a user concept or Function). This is gradual checking, not proof that every later value fits; runtime checks remain authoritative. Unknown annotation names are still errors. VM support remains narrower: immutable holes, concept/record declarations and persistent Array element contracts retain their explicit refusals.

= default (identity element). Requires let and a :: type. Fills the slot now with the same empty that nullary constructors return for types that have a genuine identity element:

Refused for scalars and unions — including Integer, Float, String, Boolean, Money, Date, literal types, and Integer | String. Those have no language-level silent default. Write the value you mean:

let xs :: Array = default      # Ok → []
let n :: Integer = 0           # Ok — you asked for zero
let n :: Integer = default     # error — use `= 0` or `= _`
let s :: String = ""           # Ok — you asked for empty string
let s :: String = default      # error

Why Integer is not default → 0. Zero is real data: it compares, adds, and branches like any other integer. Auto-zeroing would make “forgot to assign” look like a successful program that happens to use zero — the same §911 class that refuses nullary date() inventing an epoch. Axioma’s rule matches nullary constructors: containers may start empty; scalars do not get silent zeros. 0, "", and false remain fully legal as explicit initializers.

Bottoms vs holes vs empties.

let a = none                 # absence (value)
let b = om                   # undetermined (value); a == b is false
let c :: Integer = _         # hole (not a value); reading errors
let d :: Array = default     # empty array (value); len(d) is 0

For TypeScript readers. Axioma local/var creates a fresh mutable lexical binding; Axioma let/val is immutable after initialization. The spelling var does not import function-wide hoisting. Axioma const is a top-level name commitment that also prevents shadowing; it is not a general translation of a block-local TypeScript constant. A bare Axioma assignment may create a binding; an outer-frame write uses rebind. local x :: Number reserves a typed cell without an implicit undefined. Use = 0 only when zero is the intended value.

Eager bindings, deferred bindings, and definitions

let/val, var/local, and bare :/= bindings evaluate their RHS now. declare creates a fresh immutable lazy binding: reading its name runs the computation and caches a successful result. define records a definition in the knowledge system; it is not an alias of declare.

declare Answer :: Float = 6 * 7
println(type(Answer))             # Float: conversion occurs on first demand

A repeated declare creates a new cell, as let does. Earlier closures keep older cells. Assignment, rebind, and reference writes cannot replace the new cell; an Array obtained from it can still be mutated. A const name cannot be shadowed. Ordinary value names, including uppercase names, are accepted, with the same protection for seeded type names as other fresh bindings. global and a fresh declaration cannot select the same name in a function frame.

Recursive groups. Unlike an eager initializer, every deferred RHS sees the new names in its own declaration group. Annotations resolve in the preceding scope. Capture retains lexical cells: mutations to a captured cell before the first demand are visible; a later fresh shadow does not replace that cell.

declare left, right = right + 1, 41
println(left)                    # 42

declare ones = stream_cons(1, lazy ones)
println(first(ones, 4))           # [1, 1, 1, 1]

declare x = x + 1 therefore refers to its own new cell, not an earlier x. Demanding it reports a cyclic-demand error. Names introduced in a later fresh statement are not retroactively in scope; put mutually dependent names in one group. Each name requires its own RHS; lazy pattern destructuring is not part of this form. Duplicate names in a group are refused.

Value contracts. declare x :: T = e checks and converts the computed value before caching it. Array element and dictionary-schema constraints travel with the value. An unused computation is not evaluated just to check its result; --typecheck may still diagnose statically evident mismatches. declare x = [42] now means a one-element Array, exactly as it does in ordinary expressions. _ and default initialization markers belong to let/var, not declare.

Failures and effects. Only successful results are cached. A failed force can be retried, and effects from the failed attempt are not rolled back. Forcing never creates a binding in the reader's scope. declare, explicit lazy, and /lazy parameters share this demand behavior and remain evaluator-only.

declare/persist and declare/transient select persistence policy independently of evaluation. They do not make an unevaluated closure serializable; see the persistence limitations below. Saving must not run a computation implicitly.

define retains its distinct definition/speech-act forms: define concept, define axiom, define postulate, define theorem, define word, and define dialect. Computational value-form define currently evaluates in the reader's environment and caches an ordinary binding there; a cached binding can hide a subsequent definition version. Its lexical capture and version-aware cache are a separate design follow-up, not guarantees of declare.

Bare declarations — the same hole, with less syntax

Each fresh named binder allows omission of = _, with or without a type:

local result :: Integer
if true then [result = 10] else [result = 20]
println(result)                # 10
let callback :: Function
callback = func(n) [n + 1]
println(callback(2))           # 3

The declaration creates a fresh, optionally typed, uninitialized cell when execution reaches it. It creates no zero, none, om, or other default and does not hoist the name. Use assignment to fill that cell; another local result = 10 would create a fresh shadow. An earlier closure keeps its earlier cell.

A bare named batch permits independent annotations: var a, b :: String. b is constrained to String; a is unannotated. Bare patterns remain refused: a pattern decomposes an existing value, so it needs an initializer. A newline, semicolon, block terminator, or end of input ends the declaration, except that a following = continues an initializer even across a newline. const, declare, and rebind gain no valueless form; they serve different purposes. Detached x :: T retains its existing annotation role. The parser lowers the new forms to the existing hole node. Untyped holes remain explicitly unsupported under --vm; the earlier typed-hole VM limits are unchanged.

local — fresh mutable binding in this scope

local NAME = value shares var's fresh mutable binding semantics. It emphasizes where the binding lives; var emphasizes that it can change. Both use Axioma's lexical scopes. An initializer evaluates before the new binding exists, and earlier closures retain the cell they captured. Repeating local x = ... creates another fresh cell; it does not update the previous one.

function local_example()
  x = 10
  if true
    local x = 20
    x += 1
    println(x)                 # 21
  end
  x
end
println(local_example())       # 10

Replacing local x = 20 with bare x = 20 updates the function's existing x, so the final result becomes 21. Plain accumulators keep their usual rules. A loop-body local is fresh each iteration and ends with that body.

Forms include local x :: Float = 3, local a, b = 1, 2, local (a, b) = pair, and the array/hash patterns accepted by var. Existing type annotations convert and constrain later writes as usual. Initializers take = only. local x :: Integer and its explicit spelling local x :: Integer = _ create a refillable typed hole. local x and local x = _ create the same kind of cell without a type constraint. Declaration compound assignment local x += 1 remains refused. An explicitly typed = default is allowed when the type supplies an identity value: this initializes a real value, rather than leaving a hole.

An active local binding and global cannot select the same name in one function frame, in either order; this includes fresh let/var bindings and patterns. global marks the function frame, so a nested block cannot override that mark with local. A nested function has its own frame and may select its own local or global binding. At file/module level local binds in that unit, lasts to the end of that scope, and does not change export visibility.

This is an Axioma teaching spelling, not Julia's whole-scope declaration analysis or its interactive soft-scope rules. No declaration is hoisted and ordinary assignment still stops at a function boundary. local is reserved; use $local as an ordinary identifier. [local x] remains a POP-11 word list. Canonical AST printing uses var. The evaluator supports these forms; the VM shares var support and explicitly refuses unsupported nested-block bindings.

Scoping & shadowing

Axioma is block-structured: every block form pushes a nested lexical environment — function bodies, if/then/else branches, comprehensions, foreach loops. A fresh name bound inside a block dies with the block (stricter than Python, where if-branch and loop variables leak out):

if true then [z: 42]
z                              # ERROR: undefined — the branch scope is gone

doubled: [n * 2 | n <- [1, 2, 3]]
n                              # ERROR: undefined — comprehension-local

foreach w in [10, 20] [t: w]
w                              # ERROR: undefined — loop-local

A binder binds; a body assignment stops at its frame. That is the whole rule, and the two halves are worth stating separately.

Body assignment — name: value (and its = synonym) — is find-or-update, but the search stops at the enclosing function frame: it walks the blocks around it, and if the name exists anywhere within that frame it is updated in place; otherwise it declares here. So one function can never disturb another function's binding by accident:

v: 1
h: func() [v: 2]               # declares h's OWN v; the outer one is untouched
h()
v                              # → 1

x: "outer"
f: func(x) [x + "-inner"]      # a PARAMETER is always a fresh binding
f("param")                     # → "param-inner"
x                              # → "outer" — untouched

The boundary is the frame, not the block, and that distinction is doing all the work. Every block inside one function — an if branch, a loop body, a value block — is transparent to the search, which is what keeps accumulators and counters working:

sum_all: func(xs) [
  total: 0
  foreach n in xs [total: total + n]   # writes the frame's own total
  total
]
sum_all([1, 2, 3, 4])          # → 10

countdown: func(n) [
  i: 0
  while i < n [i: i + 1]       # a block-local i would never terminate
  i
]

Binder positions, by contrast, always introduce a fresh binding that shadows any outer name of the same spelling. A binder is any position where a form names the variable it is about to bind for you: a parameter, a loop variable, a comprehension generator, a quantifier variable, a relation logic variable, a match capture.

i: "outer"
foreach i in [1, 2, 3] [ ]     # the loop variable is the loop's own
i                              # → "outer" — untouched

sq: func(xs) [{i * i | i <- xs}]
sq([1, 2, 3])                  # → {1, 4, 9}
i                              # → "outer" — a comprehension is an expression,
                               #   and expressions have no side effects on you

rebind — writing a name in an enclosing frame

Because a body assignment stops at its own frame, reaching out of a function is spelled, not assumed. rebind walks the whole chain, updates the nearest binding it finds, and takes : or = like any other binding:

counter: 0
bump: func() [rebind counter: counter + 1]
bump()
bump()
counter                        # → 2

rebind never declares. A name that is bound nowhere is an error, which is the point: rebind states that the name already exists, so a typo in it is caught rather than quietly becoming a second variable.

bump2: func() [rebind countr: 1]
bump2()                        # ERROR: 'countr' is not bound in any enclosing scope

Two details worth knowing. rebind targets the nearest enclosing binding, not the outermost — so a function that has its own d and calls an inner function that rebinds d updates that middle one, not a top-level d. And none counts as bound, so x: none then rebind x: 5 works; declaring a slot empty and filling it later stays spellable.

global — Julia's module write

global is not an alias of rebind. It skips enclosing function locals and may declare the name on this file (or this nested module M … end body). rebind still updates the nearest existing cell and never declares. On a file-level accumulator they agree; they diverge when an enclosing function has the same name. The word is reserved: global: 5 is a SyntaxError; guard as $global. Word lists take it bare ([global x]).

If the module cell already exists, global total = total + x updates that cell (it does not shadow it the way let would). If it does not, a RHS that needs no prior read (global fresh = 7) declares it there. A loop does not redeclare: every iteration writes the same box. The module cell's :: applies — counted :: Integer = 0 then global counted = counted + 1 converts or refuses like any other write, and global ratio :: Float = 3 snapshots the annotation on that cell.

total = 0
function addall(t)
  for x in t
    global total = total + x   # same numbers as `rebind total = total + x`
  end
  total
end
addall([1, 2, 3, 4])           # → 10
total                          # → 10

x = "module"
function outer()
  x = "outer"
  function inner()
    global x = "inner"         # file x becomes "inner"; outer's x stays
  end
  inner()
  x                            # → "outer"
end

counted :: Integer = 0
function bump()
  global counted = counted + 1
end
bump()                         # counted is 1, still Integer
# global counted = "nope"      # type error

function seed()
  global ratio :: Float = 3    # converts; ratio is 3.0
end

axioma --lint finds the writes that no longer reach. A body that meant to update an outer name now declares a local instead, and nothing errors:

acc: 0
bump: func() [acc: acc + 1]    # reads the outer 0, writes a NEW local
bump()
bump()
acc                            # → 0

axioma --lint script.ax

Nothing is run: the file is parsed and each function body is read for one shape — a plain assignment whose target name is bound outside the function and is neither a parameter nor a binder variable. A path may be a file or a directory; # lint: ok on the offending line, or the line above it, says the local was deliberate. Exit status is non-zero when anything is reported, so it works as a gate.

The trade: closures mutate captured state, but say so. A closure still reaches the cell its factory declared — it just spells the reach:

make_counter: func() [
  acc: 0
  func() [
    rebind acc: acc + 1        # reaches the CAPTURED acc
    acc
  ]
]
c: make_counter()
c()                            # → 1
c()                            # → 2
c()                            # → 3

Each call to make_counter() still gets its own acc; two counters do not share a cell. (acc here is just a name; count also works — it stopped being a reserved word in July 2026 and is now a soft keyword, recognized only in the constrained-language shape count <<pattern>>.)

Builtins vs constants. The lowercase math names (pi, e, tau, im, …) are shadowable fallback builtins — pi: 3 wins locally and leaves the system untouched. The canonical UPPERCASE constants (PI, TAU, EULER, …) are seeded immutable: PI: 3 reports Cannot reassign constant 'PI' (non-fatal) and PI keeps its value. im is the imaginary unit (complex(0, 1)); there is no uppercase IM.

const — your own named constant. The same protection the seeded constants have, applied to a name you choose:

const LIMIT = 10
LIMIT                            # → 10
LIMIT: 20                        # → ERROR: Cannot reassign constant 'LIMIT'

const is a program-level commitment: one name, one value, everywhere. It refuses reassignment, refuses to be declared over any existing name, and refuses to be shadowed — let LIMIT = 99 is the same error. It is also top-level only (file, module top level, REPL): inside a function the immutable local is let, and a function-body const says so:

f: func() [ const MAX = 1 ]
f()   # → ERROR: `const` declares a program-level constant and is top-level
      #   only — inside a function write `let MAX = ...` for an immutable local

That division of labor is the whole design: let protects a cell, const protects a name. Use let for everyday working bindings, const for the SCREAMING_CASE handful whose point is that the name is globally unambiguous.

Two more things to know. First, const is the one place = and : are not interchangeable — the declaration takes = only, and const LIMIT: 10 is a SyntaxError. Second, the binding is constant, not the value: a const array is still a mutable place.

const xs = [1, 2]
push(xs, 3)
xs                               # → [1, 2, 3]   — the name is pinned, the array is not

Reassignment is fatal (exit 1), unlike the non-fatal report on the seeded PI. So const pins which value a name denotes; if you also need the value itself to hold still, reach for an immutable type — a List rather than an Array (§5).

given is retired. The natural-language alias of const duplicated it exactly and was removed (August 2026); the retired spelling errors with the migration:

given G = 5    # → SyntaxError: `given` was retired — write `let G = value`
               #   for an immutable binding, or `const G = value` for a
               #   top-level named constant

The word keeps its one living meaning: the premise line of a [solver| …] block — find d … given a = 3, b = 4 … condition … — which is Pólya's "the given" and is unchanged.

Regression pins: tests/axioma/binding/test_scoping_shadowing.ax, tests/axioma/constants/test_constants_comprehensive.ax, tests/axioma/binding/test_given_retired.sh.

Unicode identifiers

Names are not limited to ASCII. Any Unicode letter can start an identifier — Greek, Cyrillic, CJK, Arabic, Hebrew, Egyptian hieroglyphs — and emoji from the standard emoji blocks work too. Digits and combining marks may follow. Identifiers are NFC-normalised as they are read, so the precomposed and decomposed spellings of café are the same name:

α: 3.14159                       # Greek letters are ordinary names
Δx: 0.5                          # Δ is a letter (the symdiff glyphs are △ ∆ ⊖)
файл: "report.txt"               # Cyrillic
σύνολο: {1, 2, 3}                # a Greek word, diacritics included
😀: "happy"                      # emoji from the standard blocks
add1: func(β) [β + 1]            # parameters too
πλήθος: 3                        # words may START with π — see below

Five Greek letters double as built-ins — π, φ, τ (constants), Σ (sum), and Ω (om). Each keeps its built-in meaning when it stands alone, and is an ordinary first letter otherwise: π is 3.14159… while πλήθος is your variable. The one letter that always keeps its operator meaning is λ — λx.x is a lambda abstraction, so a name cannot start with λ. Operator glyphs (∪ ∩ ∈ ∀ → …) are never identifier characters, and two conventions stay ASCII on purpose: the TitleCase-means-Concept heuristic (Файл is an ordinary word, not a Concept) and the uppercase-initial logic-variable convention in relations and rules.

Guarded identifiers and atoms

To use a reserved word, a multi-word name, or punctuation as an identifier, guard it with $:

$forall: 5                      # `$name` — a reserved word used as a plain name
$"interest rate": 0.0525        # `$"..."` — spaces / punctuation in a name
$"GDP growth %": 2.1

$ disambiguates by what follows it: a digit keeps the money literal ($5, $5.00); a " opens a quoted guard; a letter opens a bare guard. The ${...} interpolation form inside strings is untouched — guards never use it.

Symbolic set elements (atoms) use the self-denoting word literal 'name, and cardinality is len(...):

A = {'p, 'q, 'r}                # a set of three atoms
'q in A                          # → true
len(A)                           # → 3   (the cardinality of A)

Persistence refinements

The : operator deliberately has no refinement slot — adding /persist to : would force three-token lookahead on every identifier parse, and : is one of the highest-frequency tokens in the language. For persistent value bindings, use the dedicated declare form:

declare/persist counter = 0     # Mark for saving; demand before saving
declare/transient temp = 42     # Discarded at session end
declare scratch = 0             # No refinement — uses the mode default

Default: REPL persists, scripts are transient.

Note the operator: declare uses = (the ASSIGN token), not :.

Persistence is a policy flag, not an implicit force. An unevaluated declaration is currently reported and skipped by session saving; demand it explicitly first. A successfully forced serializable value is saved and restored as an immutable binding, without rerunning its computation. Typed scalar results retain their converted value. Contracted compound results (such as Array of Integer) are reported and skipped because their value contracts cannot yet be serialized. Explicit lazy closures are also unsupported. A save warning means that named value was not included in the image; /persist alone is not a durability proof.

This keeps the canonical : form refinement-free and concentrates the persistence vocabulary in one place. The same /persist / /transient refinements apply to axiom, postulate, and define:

axiom/persist   gravity_constant = 9.81
postulate/transient working_hypothesis = "..."

Persistence-controlled bindings are written declare/persist counter = 0 (and declare/transient).

The public contract is the syntax above plus the persistence notes in §15.

Statement vs. expression syntax

Most language constructs come in dual forms:

Note that s: a Stock {} is not a concept-definition form — the indefinite article creates an instance (a ConcreteEntity) of an already-defined concept, a different operation entirely (see §13).

Use the natural-language statement form for concept lifecycle and properties, the functional/expression form for values and computation.

Typing the glyphs

Axioma's math notation (∈ ∪ ∩ ⊆ ⊇ ∀ ∃ λ ∧ ∨ → ≠ ≤ ≥ ⊻ …) is always optional — the operators have plain word twins (in, union, intersect, subset, superset, subsetneq/supsetneq for the proper forms ⊂ ⊃, forall, exists, lambda, and, or, implies, xor for ⊻, !=), so no setup is ever required. The exceptions are the description-logic pair ⊓ ⊔ and the NAND/NOR pair ⊼ ⊽, which stay glyph/digraph-only as infixes (the words nand/nor are their prefix builtins, deliberately unreserved). When you do want the glyphs, pick whichever input layer fits where you're typing — all of them resolve the same names from the same catalog (the one symbols() prints), so a spelling learned once works everywhere:

Names are LaTeX first (`cup, \subseteq), then Axioma's canonical names (`union), then word aliases — ~100 spellings. Discover them from inside the language: symbols() lists the whole catalog with LaTeX names and meanings; glyph("cup") looks one up.

The MVL truth-value literals (§9) live in the same catalog — symbols("mvl") lists all 13 (⊤⊥ᵇ, ?ᵏ, ½ł, ?ⁱ, …), each with digraphs from the same table: `belboth ≡ ⊤⊥ᵇ, `klunknown ≡ ?ᵏ, `lhalf ≡ ½ł, plus Priest's `glut / `gap. The REPL/LSP/playground/espanso layers above pick them up automatically (\belboth + Tab → ⊤⊥ᵇ).

Notes. The digraph leader is a backtick, not the Agda/Julia backslash, because \ is Axioma's set-difference operator; a backtick outside strings and comments was previously a syntax error, so the form is collision-free. A digraph is byte-identical to its glyph at the token level, so it works in every construct, in the VM, and in the playground. A digraph is unpaired — a matched pair of backticks is the unrelated infix-application form of §19.3 (3 `mysum` 4 ≡ mysum(3, 4)). The two are told apart by the closing backtick alone, never by looking the name up in this table, so the glyph catalog can grow without ever changing what an existing `name` means. --glyphify is token-aware (strings and comments are never touched) and verifies the rewrite lexes and parses identically before writing; conversions only happen where both spellings produce the same token, so not/¬ and value literals like true/false/om are deliberately left alone.

Formatting a file — --fmt

--glyphify canonicalizes how an operator is spelled; --fmt canonicalizes where it sits. The two compose, and together they are the canonical print form.

axioma --fmt script.ax         # rewrite in place
axioma --fmt-check script.ax   # report only; exit 1 if not canonical

What it normalizes — whitespace, and nothing else:

What it never touches: the bytes of any token, the contents of a string, and comments — including a trailing # … and the body of a /**md block. Intra-line spacing is left as you wrote it, so 2, 3, + and 1..9 and a's survive unchanged.

Two safety rules, both borrowed from --glyphify:

1. Unparseable input is refused. Like gofmt, a canonicalizer will not guess at a broken file.
2. The result is verified before it is written. The reformatted source must re-lex to an identical token sequence — same types and same literals — and must still parse. If it does not, nothing is written and the command reports why. A formatter that silently alters a program is worse than one that refuses.

--fmt-check writes nothing and exits 1 when any file would change, which is the form to use in CI or a pre-commit hook. --fmt-diff is the same gate with the detail — it prints the unified diff instead of just the filename:

axioma --fmt-check src/*.ax   # which files would change
axioma --fmt-diff  src/*.ax   # exactly which lines, as an applicable patch

Both write nothing. The diff is a genuine patch — patch -p0 and git apply accept it, and applying it reproduces what --fmt would have written, byte for byte, because both render from the same result. Since trailing whitespace is most of what the formatter strips and is invisible in a diff, a whitespace-only change is flagged with a note so the output does not read as a formatter bug.

In the editor. axioma-lsp serves the same engine as textDocument/formatting, so Format Document (and format-on-save) in VS Code, Cursor, Neovim or Helix produces bytes identical to axioma --fmt. It also serves textDocument/rangeFormatting, so Format Selection (and the extension's Format Axioma Selection) changes only the selected lines — at the indentation the whole file gives them, because the engine still runs on the whole buffer and only those lines are handed back. Rebuild the server to pick it up:

go install ./cmd/axioma-lsp     # or: cd vscode-axioma && ./reinstall.sh

Two things the editor path does deliberately: a buffer that does not parse yields no edits and no error (format-on-save fires on half-typed lines, and the parse error is already showing as a diagnostic), and the editor's tabSize / insertSpaces are ignored — a canonical formatter that varied by editor setting would defeat its own purpose.

4. Data Types

Primitives

Integers don't overflow

Integer is arbitrary-precision (the Python/Mathematica model, not C/Lua's fixed 64-bit wrap-around): when a result outgrows the machine word it promotes transparently, so 9223372036854775807 + 1 is 9223372036854775808, 2^100 is exact, and 3^39 has every digit right. This holds identically in the evaluator and under --vm (the VM delegates its integer core to the reference runtime, so the semantics agree by construction), and across the numeric builtins (succ/pred, sum, abs, divmod/quotient/remainder, floor/ceil/round/trunc/int, gcd/lcm, factorial, …).

Consequences of the design:

• There are no maxinteger/mininteger constants — a largest integer does not exist. (Python 3 removed sys.maxint for the same reason; Julia has no typemax(BigInt); Haskell's Integer has no Bounded instance.)
• Hex/binary/octal literals are magnitudes, not bit patterns: 0xFFFFFFFFFFFFFFFF is 2⁶⁴−1 (a positive number), not Lua's -1.
• Bit operators (band/bor/bxor/bshl/bshr) use Python's infinite-two's-complement reading: bshl is exact at any count (1 bshl 63 = 2⁶³, 1 bshl 100 = 2¹⁰⁰), and bshr is an arithmetic shift that drains to 0 (or -1 for negatives) past the width.
• Memory is the only bound. An operation whose single result would be astronomically large (a shift count or exponent past the ~67-million-bit budget) raises a catchable error rather than exhausting memory: try(1 bshl 10^12) is an Error value, not a crash.
• The representation is invisible: type(2^100) is "Integer" like any other integer. Mixing with a Float converts to float64 (precision may be lost past 2⁵³ — the universal int-meets-float rule).

Missing data cells: na and Na

na is the missing-cell value; Na is its programming type. NA remains a compatibility alias of the same value. Values and DataFrames display it as na; the internal tag and CSV's default external missing marker remain NA.

type(na) == Na          # true
@na == Na              # true
na is Na               # true
Na is DataType         # true
Na == na               # false — type versus value
NA == na               # true — compatibility alias
na == none             # false
na == om               # false
if na then true else false  # true
na ?? 5                # na (evaluator-only operator)
na ??? 5               # na (evaluator-only operator)

This is a data sentinel, not a third language bottom: it remains truthy and neither coalescing operator replaces it. Arithmetic such as na + 1 is a type error, not missing-value propagation. The foreign /eval bridges still map R NA, Julia missing, and JavaScript null/undefined to none.

Dual null types

Axioma has two distinct null-like values with different semantics — they are not interchangeable.

none == om             # false — never interchangeable
none is None           # true — type of none, parallel to om is Om
None == none           # false — type vs value, like Integer == 5
if none then ...       # never executes
if om   then ...       # never executes (om is falsy)
# `null` was retired — write `none`. The type is None (`none is None`).
# `nothing` was retired — write `none`. DL's empty concept remains `Nothing`.
# `Null` was retired — the type of `none` is `None`. Option's empty tag is `Absent`.

Operational rule: none means absence; om/Ω means an explicit undetermined value. They compare differently (none == om is false). Both are falsy for control flow, so if alone cannot tell them apart — use v is None / v is Om (or == none / == om). Because om folds onto the designation law (designated(om) is false), it agrees with typed Kleene unknown ?ᵏ (see §9). null and nothing are retired — they are SyntaxErrors, not aliases. JSON null stays the wire spelling. Option's empty constructor is Absent (truthy); Absent == none is false.

Strict assignment. Annotated T does not accept none — write T | None (and/or | Om) when absence is allowed. Prefer holes for “not yet set”: let x :: String = _ (read before assign is a hard error). Nullish defaults use ?? (none only) and ??? (none or om); not truthy-coalesce — see the section ?? / ??? — the absence railway. Safe property access is ?..

Full scorecard vs TypeScript-style strict null checking: resources/docs/claude/NULLABILITY_STRICT.md.

Multi-valued logic types

Written as literals (the same forms the interpreter prints) or built via constructors; both participate automatically in operator dispatch (priority Belnap > Intuit3 > Łukasiewicz > Kleene > Boolean). See §9.

glut: ⊤⊥ᵇ                        # Belnap glut literal  (≡ belnap("both"))
half: ½ł                         # Łukasiewicz half     (≡ lukasiewicz(0.5))
unknown_g3: ?ⁱ                   # Gödel G3 unknown     (≡ intuit3("unknown"))
score: lukasiewicz(0.73)         # constructor — any value in [0, 1]

(contradiction itself is a reserved word — hence glut, which is also Priest's term for the value.)

Strings — escape sequences, raw form, codepoint builtins

String literals are written between double quotes ("…"). A single-quoted 'x' is a Character. Strings are stored as UTF-8, so Unicode characters can appear directly in source:

greeting: "hello, world"
math:     "∀x ∃y. x + y = 0"
greek:    "λ φ Ω"

For cases where the character can't be typed directly, escape sequences decode at parse time:

"line1\nline2"            # 2 lines (LF in the middle)
"tab\there"               # 3 fields separated by TAB
"quote: \"hi\""           # quote: "hi"

"\u{2203}"                # → ∃   (BMP — 4 hex digits)
"\u{1D54A}"               # → 𝕊   (math S — 5 hex digits, supplementary plane)
"\u{1F600}"               # → 😀   (emoji — 5 hex digits)
"\u{10FFFF}"              # → 􏿿   (max valid Unicode codepoint)

The braced \u{H...H} form takes 1–6 hex digits. The 4-hex "\uXXXX" form is intentionally not supported — it only reaches the Basic Multilingual Plane and forces a second \U00000000 escape for everything above U+FFFF. The single braced form handles the entire codepoint range.

Surrogate codepoints rejected. \u{D800} through \u{DFFF} are rejected at parse time because they cannot appear in valid UTF-8. chr(N) enforces the same check at runtime.

Unknown escapes are preserved verbatim. "regex \d+" keeps \d as a literal \ followed by d — a back-compat hatch for strings that contain regex metacharacters. Define a proper escape only when needed; everything else passes through.

Literal prefix naming

Axioma uses one letter for each basic quoted literal prefix: r for raw text, f for formatted strings, b for bytes, and c for commands. A two-letter prefix combines two existing prefixes with compatible behaviors; it is never a longer abbreviation for a single feature. This naming rule applies to future quoted literal prefixes as well.

Each combination must be explicitly supported. Currently, rf and fr combine raw text with formatting; no other combinations are supported. Commands keep the single-letter c prefix.

Raw strings — r"..." and r'...'

The r prefix bypasses escape decoding entirely. Useful for paths, regex patterns, and any genuinely-literal content:

winpath:  r"C:\Users\alice\new"      # literal path — no \U, \n decoding
pattern:  r"\d+\.\d+"                 # literal regex
raw_unicode: r"\u{2203}"             # → 8 chars: \, u, {, 2, 2, 0, 3, }

The result is byte-identical to the source between the quotes. r"…" and "…" produce the same *ast.StringLiteral AST node — the raw form just skips the decode pass.

Triple-quoted and interpolated strings

Both also decode escapes:

multi: """
line one
line two \u{2203} ${some_var}
"""

x: 42
interp: "value = ${x}, glyph = \u{2200}"

Formatted strings — f"...", rf"...", and fr"..."

Formatted strings evaluate Axioma expressions, using {expression:spec}. Ordinary strings keep their existing ${expression} syntax. Both produce String values; neither invokes Python.

price: 12.345
name: "Ada"
f"Total: {price:.2f}"        # "Total: 12.35"
f"{42:05d}"                 # "00042"
f"{name:*^9}"               # "***Ada***"
f"{{{name}}}"               # "{Ada}"
rf"C:\reports\{name}"       # backslashes stay literal; name interpolates
f"{len("abc")}"             # nested quotes belong to the Axioma expression

rf and fr combine raw text with formatting. Single-quoted prefixed forms are also accepted. Fields evaluate once, left to right. Use {{ and }} for literal braces. Unclosed/empty fields and invalid expressions are syntax errors; incompatible values or unsupported format specifications are Errors.

The supported static format grammar is [[fill]align][sign][#][0][width][.precision][type]:

F, E, and G are uppercase variants. Omit the type for ordinary display; precision without a type selects String truncation or numeric g formatting. Width counts Unicode codepoints, not terminal cells. Width and precision are bounded at 1,000,000. Integer formats accept integral Float/Rational values, following Axioma's existing format rules; fractional values are rejected. Numeric formatting may round, as with format.

This is a focused formatting surface: Python conversions (!r, !s, !a), debug =, grouping separators, dynamic/nested format specifications, combined command-format prefixes, and triple-quoted prefixed forms are not supported. Parenthesize expressions whose top-level colon belongs to Axioma syntax, including Time values. Braced Unicode escapes in non-raw text keep their ordinary meaning.

Codepoint builtins — chr and ord

For programmatic codepoint construction (when the literal form can't help because the value comes from runtime):

chr(8707)              # → "∃"
chr(0x1F600)           # → "😀"
ord("A")               # → 65
ord("∃")               # → 8707
ord(chr(N)) == N       # round-trip for any valid codepoint

Both accept the full Unicode range U+0000..U+10FFFF; surrogates are rejected; ord("") errors with "empty string has no codepoint".

Case mapping — upper / lower / title (and Julia aliases)

upper("Hello")            # → "HELLO"
uppercase("Hello")        # → "HELLO"   Julia spelling, same function
lower("Hello")            # → "hello"
lowercase("Hello")        # → "hello"
title("hELLO wORLD")      # → "Hello World"
titlecase("hELLO wORLD")  # → "Hello World"
capitalize("hELLO WORLD") # → "Hello world"   not titlecase — one word's worth of shift

uppercase / lowercase / titlecase are aliases of upper / lower / title. A Character in is a Character out (uppercase('a') is 'A'). uppercasefirst is not capitalize (Julia leaves the rest of the string alone) and is not shipped.

Operators

"ab" + "c"            # → "abc"    concatenate
"ab" * 3              # → "ababab" repeat
"abc" - "ab"          # → "c"      bag difference (Miranda `--`)
"miranda" - "mira"    # → "nda"
"aa" - "a"            # → "a"      a bag, not a set — one `a` remains
"abc" - "ccar"        # → "b"      right-hand order does not matter

- walks the left string and drops a character whenever the right still has a remaining occurrence of it. It is not substring removal ("abab" - "ab" is "", not "ab").

Unicode normalization — normalize(s, [form])

The same visible text can arrive in different codepoint spellings: é is either the single codepoint U+00E9 or e followed by the combining acute U+0301. The two render identically but are invisible to == and count — one is 1 codepoint, the other 2. normalize rewrites a string to a canonical form so comparison and counting behave:

"e\u{301}" == "\u{E9}"                      # false — the problem is real
normalize("e\u{301}") == normalize("\u{E9}") # true  — NFC composes both
count("e\u{301}")                            # 2
count(normalize("e\u{301}"))                 # 1
normalize("\u{E9}", "NFD")                   # decomposes → "e\u{301}"
normalize("\u{FB01}", "NFKC")                # "fi" — compatibility fold (fi)
normalize("\u{2460}", "NFKC")                # "1"  — ① folds too
try(normalize("x", "NFX"))                   # catchable Error naming the forms

Forms: NFC (default — the W3C/web recommendation and JavaScript's String.normalize default), NFD (decomposed), NFKC/NFKD (additionally fold compatibility characters — ligatures, circled digits, full-width forms). The form name is case-insensitive. Normalize both sides before comparing text from mixed sources (file systems, user input, copy-paste — macOS file names, for instance, arrive decomposed). Grapheme clusters remain out of scope: count counts codepoints, so a combining sequence with no precomposed form still counts per codepoint.

Substring search — index_of and span_of

Two builtins locate a substring, both in 1-based character (rune) coordinates — the same coordinates substring, s[a..b] slicing, and nth use, so a found position feeds extraction directly:

index_of("hello Lua users", "Lua")        # 7   — 1-based START position
index_of("hello", "zz")                   # none — a miss is the falsy `none`
                                          #        (composes with if/??; never 0)
s, e: span_of("hello Lua users", "Lua")   # (7, 9) — the (start, end) PAIR,
substring("hello Lua users", s, e)        # "Lua"   1-based INCLUSIVE
span_of("abc", "z") ?? "absent"           # miss → none (falsy; composes)

index_of("aXbXc", "X", 3)                 # 4 — optional init: search FROM there
span_of("aXbXc", "X", -2)                 # (4, 4) — negative init counts from
                                          #          the end; result is ABSOLUTE

index_of(collection, target [, init]) answers where does it start — on strings, arrays, and tuples (a Set errors: no positions — use in). span_of(s, sub [, init]) answers where does it live: a Tuple of inclusive (start, end) positions, or none when absent. The optional init starts the search at that position (below 1 clamps to 1; an empty needle matches at the clamped init, up to one past the end), and because returned positions are absolute, the scan-all-occurrences loop is direct:

p: index_of(haystack, needle)
while p > 0 [
  # ... use p ...
  p: index_of(haystack, needle, p + 1)
]

Rune coordinates mean multibyte text is safe by construction: span_of("hällo wält", "wält") → (7, 10), and substring with those positions returns exactly "wält". For pattern-based (not literal) search, use the regex family below; for a membership test alone, contains(s, sub) / sub in s.

Regular expressions — native regex_* builtins

Five native builtins wrap Go's RE2 engine (linear-time, no catastrophic backtracking). Argument order is (subject, pattern) throughout. An invalid pattern returns a catchable Error value rather than crashing the host.

regex_replace supports $1/$2 backreferences; regex_captures returns group 0 (the whole match) followed by each capture group, or [] on no match. Use a raw pattern (r"\d+\.\d+") to avoid double-escaping. A typical tokenize-then-convert pipeline:

nums: regex_find_all("temp 38.5 hr 72 sat 0.97", "[0-9.]+")   # ["38.5", "72", "0.97"]
float(nums[1]) > 38.0                                          # → true

Binary data — Byte and Bytes

Distinct from Integer and String so the type system can dispatch byte-specific operations and so bs[0] == 0xff reads as a Byte/Byte comparison rather than implicit coercion. The cost is verbosity, the win is no silent UTF-8 corruption.

# Three construction forms
b1: byte(0xFF)                # single byte, 0..255 — errors otherwise
b2: bytes(0x48, 0x69)         # variadic — each arg 0..255 or Byte
b3: bytes([72, 105])          # from Integer array
b4: bytes("Hi")               # from String (UTF-8 byte view)
b5: b"Hi"                     # b"..." literal
b6: b"\xff\x00\x01"           # hex escapes (also \n \r \t \\ \" \0)

Operations

# Length, indexing (1-based), slicing, concat, equality
len(b"hello")                # 5
b"hello"[1]                  # Byte(104)  — that's 'h'
b"hello"[2:4]                # b"ell"
b"AB" + b"CD"                # b"ABCD"
b"AB" == bytes(0x41, 0x42)   # true

Conversions (explicit + fallible)

Bitwise ops — word-form infix (v3) + functional form

Symbolic bitwise operators (& | ^ << >>) all conflict with existing Axioma syntax (& is address-of, | is comprehension separator, ^ is POWER). Word-form operators sidestep the conflict and match Axioma's pattern of and / or / not / union / intersect.

# Word-form infix (precedence: SUM — same as +/-, binds tighter than ==)
0xF0 band 0x0F                    # 0
0xF0 bor  0x0F                    # 255
0xFF bxor 0x0F                    # 240
1    bshl 4                       # 16
0x80 bshr 4                       # 8
0xFF band 0x0F == 0x0F            # true — (0xFF band 0x0F) == 0x0F

# On two Bytes: stays Byte for &|^, also for shifts
byte(0xF0) band byte(0x0F)        # Byte(0x00)
byte(1) bshl byte(4)              # Byte(0x10)

# Mixed Byte/Integer: widens to Integer
byte(1) bshl 4                    # Integer(16)

# Functional form (still available — useful when you need a callable)
bit_and(byte(0xF0), byte(0x0F))   # Byte(0x00)
bit_or(byte(0xF0), byte(0x0F))    # Byte(0xFF)
bit_xor(byte(0xFF), byte(0x0F))   # Byte(0xF0)
bit_not(byte(0x0F))               # Byte(0xF0)
bit_shl(byte(1), 4)               # Byte(0x10)
bit_shr(byte(0x80), 4)            # Byte(0x08)
reduce(bit_or, byte(0), bytes_to_array(bs))  # fold OR over bytes → Byte

The functional forms are ordinary builtins, and builtins are valid higher-order callables — map / filter / reduce / df_filter accept them directly (map(bit_not, xs), reduce(bit_or, 0, xs)), the same way the Enumerable verbs (sort_by, detect, …) always have. The one exception is partial, which needs declared parameters to curry and so takes user functions only.

Shift counts must be 0..63. Shift by a larger amount errors rather than wrapping.

Arithmetic on Byte widens to Integer (no overflow surprise — explicit byte((a+b) % 256) to wrap):

byte(200) + byte(100)              # Integer(300) — wider than 255
byte((int(byte(200)) + 100) % 256) # Byte(0x2c) = 44 — wrap explicitly

Integer literal prefixes

Adding bytes also brought standard hex / binary / octal literals to the language:

0xFF                # 255
0xFF_AB             # 65451  — underscores for readability
0b1010_1100         # 172
0o755               # 493
1_000_000           # 1000000 — underscores work in decimal too

These produce Integer, not Byte — wrap with byte(0xFF) for the byte form.

AST inspection

fullform(b"AB")              # "Bytes(65, 66)"
headof(b"AB")                # "Bytes"
argsof(b"AB")                # ["65", "66"]
fullform(byte(0xFF))         # "byte(255)"  — AST of the call, not the value

Design notes

• Byte displays as decimal. byte(0xFF) prints as 255 — the Python / Go / Rust convention for byte values. For a hex rendering use bytes_to_hex(bytes(b)). (Bytes keeps the b"..." literal form with \xff escapes.)
• Encoding-aware separation. Bytes doesn't carry encoding metadata; conversion to String is explicit and fails on invalid input.
• Immutable. Operations return new Bytes rather than mutating in place — composes cleanly with comprehensions, rule derivation, and the VM's bytecode constant pool.
• 1-based indexing matches Array / String / Tuple.
• A String indexes by CHARACTER (rune), a Bytes by byte. "ääb"[2] → "ä" (the 2nd character; negative indices count characters from the end, "résumé"[-1] → "é"), consistent with nth / substring / the slice forms / the ordinal accessors — so s[i] == nth(s, i) always, under both runtimes. Byte-level access on a String is explicit: string_to_bytes(s)[i] → the i-th byte. (Before July 2026, s[i] selected the i-th byte and could return mojibake on multi-byte characters; the VM rejected string indexing entirely.)
• Colon-slice x[lo:hi] is 1-based and INCLUSIVE across Bytes / Array / String / Tuple — identical to x[lo..hi], so "hello"[2:4] → "ell" (3 elements). This is not Python's 0-based half-open slice ("hello"[1:3] → "el", 2 elements); pasting a Python slice yields a different, silently-valid result. Use .. (inclusive) or ..< (half-open) when you want to be unambiguous about the bound style.
• Slice edge policy (all spellings — lo:hi, lo..hi, lo..<hi): a negative bound counts from the end, exactly as a negative single index does (xs[-1] is the last element): xs[-3..-2] → the 3rd- and 2nd-from-last elements, xs[-3..] → the last three, "cynic"[2..-2] → "yni", xs[: -2] → all but the last (the end is inclusive, so xs[: -1] is the whole sequence; xs[1..<-1] stops before the last). In the colon spelling put a space before a negative end — xs[2: -2] — because :- lexes as the rule neck. Out-of-range bounds clamp ("hello"[5:10] → "o", xs[2..9999] → the tail, xs[-10..2] → xs[1..2]) and a reversed window yields the empty value ("hello"[4:2] → "", a[2..1] → [], xs[-2..-3] → [] — so the recursion idiom arr[2..len(arr)] is safe on a 1-element array with no guard). A slice never raises an out-of-bounds error. The two-bound ../..< forms lower to the same slice node as : at parse time, so all three run identically under --vm; an end-less xs[2..] slices to the end (≡ xs[2:] — arrays, strings, tuples). Descending selection spells its step explicitly — xs[5..1..-1] → reversed (the stepped x[lo..hi..step] form keeps the directional range path, evaluator-only); a step-less x[4..2] is an empty window, not a reversal.
• $ in [] is last-index of the collection being indexed (1-based, so $ equals len(xs)): xs[$] is the last element, xs[$-1] the second-to-last, "Julius Caesar"[8:$] → "Caesar", "Julius Caesar"[$-3:$] → "esar". Nested a[b[$]] binds $ to b. On a Matrix, $ is last-index of the axis it sits on (A[:, 2:$] is columns 2 through last; A[$, 1] is the last row). $5 is money and $name is the identifier guard — those are not last-index. end is the block closer (xs[end] is a SyntaxError). $ is not a length prefix on a named collection ($xs is the identifier xs); for i in 1..$ is a SyntaxError. Loop with an index as for e at i in xs.
• No infix bitwise ops in v1 — adding them would touch lexer + parser + VM. Functional form unblocks bit work now; infix sugar can come later.
• Bit pattern matching (Erlang's <<v:4, len:16, payload/binary>> — the most expressive byte primitive of any language) is provided in v2 as pack / unpack builtins using Python's struct-style format strings (see next subsection).

See tests/axioma/bytes/test_bytes.ax for a 48-assertion smoke test that runs identically under both the evaluator and --vm.

Binary serialization — pack / unpack

Python-struct-style format strings. pack serializes values into Bytes; unpack reads Bytes back into a Tuple of typed values. The format spec is small enough to memorize:

bs: pack(">BBH", 1, 2, 256)        # b"\x01\x02\x01\x00" (4 bytes)
header: unpack(">BBH", bs)
println(header[1], header[2], header[3]) # 1 2 256

# TCP-header-style parse: port (u16), length (u16), flags (u16), seq (u32)
packet: b"\x04\xd2\x00\x10\x00\x20\x00\x00\x00\x01"
parts: unpack(">HHHI", packet)
println(parts[1], parts[2], parts[3], parts[4])  # 1234 16 32 1

Format string grammar:

• Endian prefix (optional): < little, > big, ! network (= big), = "native" (= big). Default is big-endian.

• Type codes (each optionally preceded by a count):

  Code	Size	Pack from	Unpack to	Notes
  b / B	1	Integer / Byte	Integer / Byte	signed / unsigned 8-bit
  h / H	2	Integer	Integer	signed / unsigned 16-bit
  i / I	4	Integer	Integer	signed / unsigned 32-bit
  q / Q	8	Integer	Integer	signed / unsigned 64-bit
  f	4	Float	Float	IEEE 754 single
  d	8	Float	Float	IEEE 754 double
  s	N	String / Bytes	Bytes	counted byte field, pads/truncates
  c	1	Bytes(1)	Bytes(1)	single-byte field
  x	1	(none)	(none)	pad byte — consumes 0 values

• Count prefix: 4B = four unsigned bytes (consumes 4 args). For s, the count is the byte-length of the field: 4s packs/unpacks a 4-byte string field.

Out-of-range values error rather than silently wrap:

pack(">B", 300)            # ERROR: pack 'B': value 300 out of range 0..255
pack(">b", 200)            # ERROR: pack 'b': value 200 out of range -128..127

Round-trip identity:

unpack(">d", pack(">d", 3.141592653589793))[1]   # 3.141592653589793
unpack(">q", pack(">q", -9_000_000_000))[1]      # -9000000000

See tests/axioma/bytes/test_pack_unpack.ax for the full 48-assertion smoke test.

Slicing (v2)

Bytes slicing now works under --vm (the OpSlice opcode added in v2 also unlocked slicing for String, Array, and Tuple in the bytecode engine):

b"Hello World"[1:5]          # b"Hello"
b"hello"[3:]                 # b"llo"  — open end
b"hello"[:3]                 # b"hel"  — open start

Endian-aware read/write at offset (v3)

Offset-style protocol parsing sugar over pack/unpack. Each builtin reads or writes a single field of fixed width at a given 1-based offset (matching Axioma's indexing convention). Reads return values; writes return a new Bytes (originals are immutable).

# Parse a 10-byte packet (u16 port, u16 length, u16 flags, u32 seq)
packet: b"\x04\xd2\x00\x10\x00\x20\x00\x00\x00\x01"
port: read_u16_be(packet, 1)    # 1234
length: read_u16_be(packet, 3)    # 16
flags: read_u16_be(packet, 5)    # 32
seq: read_u32_be(packet, 7)    # 1

# Build a response — start with zeros, overwrite fields
resp: bytes(0, 0, 0, 0, 0, 0, 0, 0)
resp1: write_u16_be(resp, 1, port)
resp2: write_u16_be(resp1, 3, length)
# resp is still b"\x00\x00\x00\x00\x00\x00\x00\x00" — original untouched.

These compose with pack/unpack: round-trip identity holds. Use them when you want to read individual fields at known offsets without computing slice ranges, or when you want to mutate a buffer in protocol-style.

See tests/axioma/bytes/test_bitwise_endian.ax for a 39-assertion v3 smoke test that runs identically under both engines.

Scalar value types & literals

Axioma has a family of lexer-recognized scalar literals — you write a URL, an e-mail address, a file path, a date, money, or a 2-D pair directly, and the lexer gives it a first-class type. type() returns a TitleCase string that agrees with the @ sigil and the primitive-type concepts (@v, type(v), v is T and x :: T all match).

Two of these names do double duty. URL is also the knowledge-graph link entity you build with entity URL { url: … }, and Time is also Kant/Schopenhauer's pure form of intuition (the form argument to transcendental). Both senses answer: https://a.com is URL and myLink is URL are each true, and neither steals the other's answer — a scalar settles on its type, an entity on the concept it was built from.

type(https://example.com)   # → "URL"
type($123.45)               # → "Money"
type('X' => 10)             # → Pair
type(42%)                   # → "Percent"

is_url(https://example.com) # → true
is_pair('X' => 10)          # → true
is_url($5)                  # → false

12:34:56 is Time            # → true
"12:34:56" is Time          # → false
https://a.com is URL        # → true

Both duties of a double-duty name answer, and neither shadows the other:

myLink: entity URL { url: "https://example.com" }
myLink is URL               # → true    (the graph entity)
https://a.com is URL        # → true    (the scalar)
myLink is Integer           # → false   (no over-classification)

Sigil disambiguation — position and the next character decide. $ + digit is Money ($5), otherwise $name / $"…" is a guarded identifier. % + alphanumeric is a File (%data) — but only in prefix position: a % glued to the tail of a preceding value is the modulo operator (7%2 → 1), and a number takes a trailing % as a Percent literal only when no letter or digit follows (50% is a percent; 100%7 is 100 mod 7). # is the line comment wherever it appears outside a string, glued or spaced — #xs and # xs both comment to end of line, exactly like //. The 2026-09-03 flip retired both the #123 Issue literal and the #xs prefix length; write len(xs). HashWord labels were retired earlier — write 'hello.

Arithmetic on Money / Percent

$100 + $25        # → $125
$100 * 1.5        # → $150
10% * 200         # → 20        (percent of a number)
10% * $200        # → $20       (percent of money)
10% + 5%          # → 15%       (percent ± percent stays a Percent)
$200 + 10%        # → $220      (base + p% — increase by p percent of itself)
$200 - 10%        # → $180      ;  100 + 10% → 110 (plain numbers too)

Percent ± percent stays in percent space (10% + 5% == 15% → true; comparisons return Booleans). base ± p% adjusts the base by p percent of itself — the percent goes on the right ($200 + 10%, not 10% + $200), the money result is exact and displays to cents (so $19.99 + 7.25% shows $21.44 though its value is exactly $21.439275 — see "Money is exact" below), and left-assoc chaining compounds sequentially ($200 + 10% + 5% → $231). Compound assignment inherits: price += 10%. Multiplication is still the only other operator that crosses Percent with numbers or Money — 50% * 25%, 10% / 2, and mixed equality (10% == 0.1) remain errors.

Money is exact

Money carries an exact rational value — $1/3 is exactly one third of a dollar. Arithmetic never rounds; rounding happens at exactly two points — display and the explicit round(money, places) — and nowhere else.

($1 / 3) * 3          # → $1     EXACTLY — the third comes back
$1234567.07 + $0.01   # → $1234567.08  (no float drift)
($0.01 / 3) * 3       # → $0.01  a penny split three ways survives
$5 == $5.00           # → true   ;  len({$5, $5.00}) → 1  ;  $5 in {$5.00} → true
$100 * 0.1            # → $10     — a Float scalar is read by its DECIMAL spelling,
                      #            so no binary-0.1 drift (use a Rational for a
                      #            value a decimal cannot spell)

Display rounds to the cent (half-to-even), so a non-terminating amount looks like an ordinary price — but the stored value is exact, and comparison uses it:

"" + ($1 / 3)         # → "$0.33"   — DISPLAYS rounded…
($1 / 3) == $0.33     # → false     — …but a third of a dollar is not 33 cents
round($1 / 3, 2)      # → $0.33     — round() materializes cents as an exact value
round($1 / 3, 2) == $0.33   # → true
round($1 / 3, 2) * 3  # → $0.99     — rounded, then tripled, loses the third

So $1/3 and $0.33 print alike yet are different amounts (and key differently in a set) — the same "display is a rounded view" that Float already has. When you genuinely want cents, round(m, 2) is the one operation that rounds the value. (Cross-currency arithmetic still errors; display is two decimals for every currency.)

Quantity — units of measure

A Quantity is an exact rational tagged with a physical (or custom) dimension — the science twin of Money. Currency stays Money; wall-clock time stays Duration; the Schlick magnitude(value, "kg") entity stays a float-based KR value. They do not mix.

5 * kg                              # everyday form
qty(9.8, metre / sec^2)
qty(1, kg) == qty(1000, gram)       # true — same SI base
qty(1, kg) == 1                     # error
$5 + 5 * kg                         # error
unit share                          # custom dimension
unit m = metre                      # short alias
as_unit(5 * kg, gram)               # displays as 5000 gram; still == 5*kg
mag(as_unit(5 * kg, gram))          # 5000
dim(metre / sec^2)                  # "m/s^2"

unit is a soft keyword (unit: 5 still binds). There is no juxtaposition 5 kg (already a SyntaxError) and no F# 5.0<kg>. Convert with as_unit, not in (in is membership).

The prelude seeds kg, metre/meter, sec (the SI second), gram, newton, joule, watt, ampere, kelvin, mol, ohm, and a few prefixed names (km, cm, mm, ms). Short letters m/s/A/N/g are not seeded — they would silently change 2 * A. Write unit m = metre or use the long name. The identifier second is the ordinal accessor (second(xs), xs.second) — first..tenth — not the SI unit; write sec or qty(1, "second"). min / h / day stay unseeded (they collide with min the function and with Duration).

DateTime & Duration — the datetime package

The lexer's Date / Time literals above are date-only / time-of-day scalars. Full timestamps and elapsed-time values are the DateTime and Duration types, built by the datetime package — ambient since July 2026 (datetime.now() works with no import; see §27.2), with import … as remaining the renaming spelling:

import "builtin:datetime" as Dt

bday: Dt.date(1990, 5, 15)                   # midnight timestamp
type(bday)                                   # → "DateTime"
Dt.year(bday)                                # → 1990  (month / day / hour / minute / … too)
Dt.format(bday, "2006-01-02")                # → "1990-05-15"  (Go layout strings)

gap: Dt.time_between(Dt.date(1990, 6, 15), bday)
gap                                          # → 744h0m0s  (later argument FIRST — earlier-first is negative)
type(gap)                                    # → "Duration"
Dt.format(Dt.add(bday, gap), "2006-01-02")   # → "1990-06-15"  (add a Duration to a DateTime)

type(Dt.now())                               # → "DateTime"  (Dt.utc() for UTC)
is_datetime(bday)                            # → true  ;  duration?(gap) → true

The package also carries Dt.datetime(y, mo, d, h, mi, s), Dt.from_unix / Dt.unix, Dt.from_string / Dt.strftime, calendar accessors (weekday / yearday / week), and Dt.add_date(t, years, months, days).

Words — 'w, :w

A word is a value (a symbol), distinct from a variable you look up.

'hello            # → 'hello    (natural word — self-evaluating)
x: 42
:x                # → 42        (get-word — reads the bound value, no call)

:x is the get-word; @x / :: x are type-of. :: x (and @x) return "Integer" (the DataType tag of x), while :x returns 42 (the value). Use :x to read a value without evaluating it as a call. # is a comment. #xs (prefix length) and #123 (Issue) are retired as of 2026-09-03 — write len(xs). HashWord labels (#hello as a value) were retired earlier — write 'hello.

read and file I/O

read(source) is the file/URL read verb — one argument, returns a String:

f: "/tmp/notes.txt"
write(f, "Hello from Axioma!")   # → true
file_exists(f)                   # → true
read(f)                          # → "Hello from Axioma!"
append(f, " More.")              # → true
remove(f)                        # → true   (delete the file)
file_exists(f)                   # → false

write / append return a Boolean; non-string content is stringified. A failed read (missing file, network error) returns a catchable Error value, not a crash. For a richer path/line API, import "builtin:io" as IO exposes IO.read_file, IO.read_lines, IO.join_path, etc.

The built-in os namespace is the preferred home for directory operations. The io spellings remain supported as exact aliases:

These are exact aliases; the longer names remain supported. Failures return the same Error values and diagnostics as the longer names. pwd and ls return values without printing. os.ls() lists the current directory at the time of the call, as does os.ls("."); the io aliases share this default. An explicit path must be a String or File. An empty String remains an error. cd and mkdir each require a path. mkdir is recursive, like shell mkdir -p; these functions do not interpret shell flags or expand wildcards.

println(os.pwd())
println(os.ls())

Naming gotchas (reserved-word collisions).

• Existence is file_exists(path), not exists(...) — the bare word exists lexes as the existential quantifier (∃), so exists("/p") is a parse error. file_exists matches the io package's IO.file_exists.
• File deletion is remove(path), not delete(...) — prefix delete a[i] / delete h[k] retracts a collection place; remove(path) deletes a file.
• Tag (<tag>) is shadowed by the natural-language <…> literal, so type(<html>) is "NaturalLanguage", not "Tag" — treat <tag> as unavailable from source.
• Absolute %/abs/path does not lex (the character after % must be alphanumeric); use the String form read("/abs/path") for absolute paths.

Runnable tour: tests/axioma/rebol/rebol_data_types_showcase.ax. Assertion tests: tests/axioma/rebol/test_rebol_datatypes_and_read.ax and tests/axioma/io/test_io_functions.ax. Full reference: resources/docs/Data Types.md.

Ranges — ordered a..b, exclusive ..<, by step, open n..

a..b is a first-class ordered Range value — it knows its direction, its step, and (optionally) that it has no end. It displays compactly, tests membership in O(1), and iterates in source order everywhere:

r: 1..5                  # an ordered Range value (displays as 1..5)
type(r)                  # → "Range"
5..1                     # descending — walks 5, 4, 3, 2, 1
1..<5                    # exclusive upper bound — 1, 2, 3, 4
1..10 by 3               # stepped — 1, 4, 7, 10 (`by` takes a positive
10..1 by 3               #   MAGNITUDE; direction comes from the operands:
                         #   10, 7, 4, 1)
1..10..3                 # SIGNED-step spelling — 1, 4, 7, 10 here, but NOT a
10..1..-3                #   mere alias of `by`: the sign gives the direction
                         #   (→ 10, 7, 4, 1), and a sign that contradicts the
                         #   bounds yields an EMPTY range (10..1..3 → {}) where
                         #   `by` refuses outright (1..10 by -3 → error).
                         #   `range(a, b, step)` follows the SIGNED rule.
                         #   Both spellings read bare in a loop header:
                         #   `for i in 10..1..-3 […]`, `repeat i <- 1..10..3 […]`.
"a".."e"                 # character ranges too (single-character bounds)
2..                      # OPEN-ENDED — lazy and infinite: 2, 3, 4, …

50 in 1..100             # → true  — O(1), never materializes
3 in 1..10 by 2          # → true; 4 in 1..10 by 2 → false (the step grid counts)
(1..5).length            # → 5 — the sequence accessors work (§5)
array(5..1)            # → [5, 4, 3, 2, 1] — materialize in SOURCE order

Ordered in, ordered out. Every consumer walks a range in its own order: foreach/for loops, comprehensions ([x * x | x <- 5..1] → [25, 16, 9, 4, 1]), and the collection builtins — map/filter over a range return an ordered Array, reduce/foldr fold in source order, and nth/second…tenth/sample/sort/min/max/sum/product/zip/ enumerate all take ranges directly. (Before July 2026 a range materialized as an unordered Set, which is how zip(1..len(a), a) could silently scramble — the motivating bug for the Range type.)

Set operations decay to Set. A range used where a set is meant becomes the set of its points: (1..5) union {9}, (1..9) intersect (4..12), set(1..3), powerset(1..3), and the {1..5, 99} set-literal splice all produce ordinary Sets.

Open-ended ranges are lazy. 2.. never materializes; bounded consumers work and unbounded ones refuse loudly:

first(2.., 4)            # → [2, 3, 4, 5]     (pull as many as you ask for)
zip(1.., ["a", "b"])     # → [(1, "a"), (2, "b")] — truncates to the finite side
9 in 2..                 # → true              (arithmetic, still O(1))
first((x * x | x <- 1..), 5)   # → [1, 4, 9, 16, 25] — lazy comprehensions stream
foreach k in 1.. [ … if done then [break] ]    # loop until YOU stop it
sum(1..)                 # catchable Error — as are len, array, map, sort,
                         #   set-op decay, `.last`, and every other materializer:
                         #   an open range never hangs the interpreter

Open ranges are exact past machine precision — first(2^100.., 2) returns [2^100, 2^100 + 1] exactly. A finite range with bounds beyond int64 errors loudly instead of clamping (spell it open if you need the big start).

Two spelling notes. The end of a range must sit on the same line as the .. — a .. that ends the line reads as an open range, so a line-broken 1.. + 5 is two statements. And in index position a missing end means "to the end": a[2..] slices from position 2 (≡ a[2:]), following the slice clamping rules in the Bytes design notes above.

The literal replaces most uses of the older builders, which remain: range(5) → the Range 1..5 (1-based, inclusive) and setrange(1, 5) → a Set. range(a, b[, step]) is the call spelling of the same value the .. operator builds, so range(1, 5) == 1..5 — it returned an eager Array until July 2026, which made it the one constructor whose result type disagreed with its name. Write array(range(…)) where you want the materialized list. Runtimes agree — the VM compiles ranges to the same Range value (byte-identical output, pinned by tests/axioma/cli/test_ordered_range_vm.sh).

A Range reads like an Array wherever reading makes sense: len, sum, sort, min/max, map/filter/reduce, first/last/nth, in, zip, indexing r[2] (negative counts from the end), slicing r[2:4], reverse, contains, count, index_of, unique, rest, and [h | t] destructuring. Every one of them answers exactly what it answers for array(r). Writing is not in the surface — push on a Range is an error, by design. An open range answers where arithmetic can ((1..)[4], contains(1.., 400)) and otherwise raises a catchable "cannot materialize an open-ended range" rather than walking forever.

Tests: tests/axioma/types/test_ordered_range.ax, test_range_step_by.ax, test_range_open_ended.ax, tests/axioma/builtins/test_range_builtin_consumers.ax.

5. Collections & Stacks

Arrays

xs: [1, 2, 3]
xs[1]                # 1
len(xs)              # 3

An Array is a place: it has identity over time, aliases see writes and growth, and (since the July 2026 flip) the growth verbs mutate in place — push/append grow, insert_at/remove_at splice, pop / shift remove and return an end, all at amortized O(1) for the tail forms. Because a place is something you can command, an Array also answers the same message verbs a Stack does. A verb is a statement, and it dispatches wherever a statement lives — bodies, loop bodies, and (since July 2026) then/else branches and match arms, whose brackets read as bodies:

a: [1, 2, 3]
a push 4             # in place, alias-visible (append / add are synonyms)
a extend [5, 6]      # concat in place — append would NEST [5, 6] as one element
a pop                # drops the last element (capture it with pop(a))
a shift              # drops the first element (capture it with shift(a))
a unshift 0          # prepends; the front twin of push
if len(a) > 2 then [ a pop ]   # a branch takes commands too — and the
                               # branch's value is the popped element
a clear              # empties the place — a is [] and still an Array
sort!(a)             # in-place sort; sort(a) is the copy. Aliases see it.
reverse!(a)          # in-place reverse; reverse(a) is the copy
unique!(a)           # drop later duplicates in place; unique(a) is the copy
shuffle!(a)          # in-place shuffle; shuffle(a) is the copy

The front of the array is the same place. shift / unshift are verbs, so they mutate without bang — Julia writes shift! / unshift!; Axioma does not (push! stays Undefined word). splice! keeps the bang because unbanged splice is quasiquote splicing.

b: [1, 2, 3, 4]
shift(b)             # → 1       — b is now [2, 3, 4]
unshift(b, 0)        # → [0, 2, 3, 4]
splice!(b, 2)        # → 2       — b is now [0, 3, 4]
mid: [2, 3]
ast_eval(quasiquote([1, splice(mid), 4]))  # → [1, 2, 3, 4]

shift(a) is delete a[1]; unshift(a, v) is insert_at(a, 1, v); splice!(a, i) is delete a[i]. Capture the removed value from the call; remove_at(a, i) still yields the array.

Positional surgery keeps the function spellings (insert_at(a, i, x), or two-arg insert_at(a, x) which appends; remove_at(a, i)), plus prefix delete and slice assignment:

xs: [10, 20, 30, 40]
delete xs[2]                 # → 20  — xs is [10, 30, 40]
delete xs[2:3]               # → [30, 40] — xs is [10]
xs[1:1] = [1, 2]             # replace a window; length may change
extend(xs, [3, 4])           # concat in place; a extend other too

delete yields the removed value, so old: delete xs[1] binds it. remove_at(a, i) still mutates and returns the array (not the element). copy(a) is the escape hatch when you need a value snapshot. Contrast the List below, which answers no imperatives at all — that asymmetry is the doctrine: Array is a place; List is a value.

delete is a prefix expression over a place (a[i], a[i:j], h[k]). It is not a file delete (remove(path)), not variable unbind (REPL word x delete), and not postfix Foo delete (deprecated concept destroy — write Foo destroy). Bare delete x is refused. An open-map miss yields none; h["k"]: none is not deletion — the key stays in keys(h).

Index assignment (a[i]: v) writes a live slot. A write past the end is an error — growth is a verb, not a stray index. The error names the two ways forward: grow with append(a, v) or insert_at(a, v), or pre-size and then fill (fill(n, none) or [none,] * n, after which a[j]: v is an ordinary in-bounds store). The comprehension [none | i <- 1..n] is the same pre-size, written as a generator.

[](5)                      # [none, none, none, none, none]
[](5, 0)                   # [0, 0, 0, 0, 0]
fill(5, none)              # same as [](5)
fill(5, 0)                 # same as [](5, 0)
[0,] * 5                   # sequence repeat; 5 * [0,] too
[1, 2] * 3                 # [1, 2, 1, 2, 1, 2]

[1, 2] + [3]               # → [1, 2, 3]   concatenate
[1, 2, 3] .+ [4, 5, 6]     # → [5, 7, 9]   elementwise (not concat)
[1, 2, 3] .* 2             # → [2, 4, 6]   elementwise (not repeat)
[1, 2, 3] .^ 3             # → [1, 8, 27]
[1, 2, 3] ./ 2             # → [1/2, 1, 3/2]  exact — integer / stays Rational
[7, 8, 9] .% 2             # → [1, 0, 1]      elementwise mod
[7, 8, 9] .÷ 2             # → [3, 4, 4]      elementwise floor div (not ./)
# The dotted twins bind like their plain ones, above `..`: 1..5 .^ 2 is
# 1..(5 .^ 2) and refuses. Write array(1..5) .^ 2, or [x ^ 2 | x <- 1..5].
# Nested arrays are not a matrix: [[1,2],[3,4]] .^ 2 is an error.
# Spell matrix(xs) for linear algebra, or map(f, xs) for a function.
# Word operators have no dotted infix: map(x => x div 2, xs), not xs.div 2.
[1, 2, 3] - [2]            # → [1, 3]      bag difference
[1, 1, 2] - [1]            # → [1, 2]      a bag, not a set — one `1` remains
[1, 2, 3] - [3, 1]         # → [2]         right-hand order does not matter
xs -= [2]                  # compound assignment inherits: `xs = xs - [2]`

set(32)                    # empty set, capacity 32
{}(32)                     # same
dict(32)                   # empty dict, capacity 32

a: [10, 20, 30]
a fill 0                   # [0, 0, 0] — paint live slots
fill(a, 7)                 # same command, function form

# not the matrix constructors (those need two dimensions):
# zeros(5) / ones(5) / array(5) error and point at fill / [](n, v)

A trailing comma is allowed, and it is the way to write a one-element array unambiguously: [x,]. This matters because [...] is also a block body (in if cond then [body] else [body] the branch brackets are blocks, so a bare single-statement [x] evaluates to x). The comma forces the array reading in every position:

[5,]                              # → [5]        (a 1-element array)
["w1",]                           # → ["w1"]     (len 1 — NOT the string "w1")
[1, 2, 3,]                        # → [1, 2, 3]  (trailing comma in n-arrays too)
if c then ["a", "b"] else ["w1",] # else-branch is a 1-element array
if c then [42] else [0]           # bare [x] → the scalar 42 / 0 (block body)

Since the PiL ch5 parity round (July 2026) the trailing comma is valid in all three literal forms — {1, 2,} (set) and {a: 1, b: 2,} (dict) parse like [1, 2,] — so generated constructors never special-case the last element. It also holds inside a function body, where [x,] used to be a SyntaxError.

What a bracket means, by position

A body is a statement sequence; a branch and a value binding are expression positions. They agree except on a bare comma run, which reduces as Pop-11 postfix in a body (2, 3, + → 5, the third notation for the same identity) and builds an array in the other two:

The e reading belongs to the bracket that is the branch, body, or arm — then [e], else [e], => [e], | p => [e]. A bracket nested anywhere inside that expression is an ordinary array: if c then f(1, [2]) else 0 passes [2] to f, (p) => f(1, [p]) passes [p], and then len([2]) + 10 is 11 (before 2026-08-23 the nested bracket took the block reading and f received 2).

The difference is deliberate and load-bearing in both directions: making the branch a body slot costs the [x,] idiom and every array-returning branch, while making a body's commas build arrays removes Pop-11 postfix from function bodies. Write [e,] when you want the array in any position, and parenthesize a tuple ([(a, b)]) when you want one in a body.

A bracket that opens with something only a statement can be — if, match, case, cond, return, break, continue, rebind, let x = …, global, a where section, a multi-assignment, a destructuring binding, or a named function definition (f(x) = …, func f(x) = …, func f(x) [ … ]) — is a block wherever it is written, because none of those shapes has an array reading at all:

[ f(x) = x + 1  f(1) ]      # → 2   — a definition may open a block
r: [ double(n) = n * 2  double(4) ]   # → 8

[ f(x) ]                    # → an ARRAY holding one call result
[ func(x) [x] ]             # → an ARRAY holding an anonymous lambda

The = after the head is what decides it: a bare call is an ordinary array element, and func claims the block only when a name follows (func( is the anonymous lambda). Before 2026-08-23 a definition parsed only if it was not the block's first statement.

The [s pop] row is the July 2026 alignment: a branch bracket (and a match arm's) that opens with a lowercase word pair reads as a statement, so the message verbs dispatch there exactly as in a body — then [ s pop ] pops instead of silently building the word list ["s", "pop"]. The Pop-11 quoted word list keeps its meaning in value and argument position, in any bracket nested deeper inside the branch, and whenever the first word is capitalized ([Mary likes wine]).

Positional access on sets, list surgery, and range loops (PiL ch5 round)

Four additions from the Programming in Lua chapter-5 comparison (July 2026), each with full --vm parity:

s: {30, 10, 20}
s[1]                       # → 10 — the index operator now answers on sets,
s[-1]                      #   over the SAME canonical sorted order that
s[1..2]                    #   nth/first/`.second` always used (s[i] ≡
                           #   nth(s, i) by construction); slices come back
                           #   source-shaped ({10, 20}); s[1] = x stays a
                           #   loud error — sets have no positions to WRITE

insert_at([10, 20, 30], 1, 15)   # → [15, 10, 20, 30] — Lua's exact
remove_at([10, 20, 30], 1)       # → [20, 30]           table.insert/remove:
remove_at([10, 20, 30], -1)      # → [10, 20]           they MUTATE in place
                                 #   and return the same array (the July
                                 #   2026 dynamic-array flip; copy() first
                                 #   for a functional version; pop removes
                                 #   AND returns the last element)

foreach i in 1..len(xs) [ … ]    # bare ranges after `in` — the Lua/Python
foreach i in 2..n [ … ]          #   numeric-for idiom, no parens needed
foreach i in 1..xs.length [ … ]  # property access works in bare bounds
foreach v in d.xs [ … ]          #   … and as the iterable itself; chains
                                 #   (d.inner.ys, len(d.xs)) compose too

The range spelling also fixed a latent ordering bug: ranges (and set iteration generally) used to walk in randomized Go-map order — foreach i in (2..n) could visit 3, 4, 2 on one run and 2, 3, 4 on the next. Ranges now iterate numerically and sets iterate in their canonical sorted order, so every loop is deterministic run to run. (Since July 2026 that guarantee is structural: a..b is a first-class ordered Range value with direction, step, and open-ended forms — see Ranges in §4.)

Classic pitfall — seeding an accumulator with 0

The most common bug in a hand-rolled maximum loop is invisible on the data you first test with:

maximum: func(a) [
    best: 0                        # ← the bug: a hidden claim that
    at: 0                          #   every element is ≥ 0
    for i, e in enumerate(a) [
        if e > best then [
            best = e
            at = i
        ]
    ]
    return (best, at)
]
maximum([8, 10, 23, 12, 5])        # (23, 3)  — looks perfect
maximum([-4, -2, -9])              # (0, 0)   — silently WRONG: no element
                                   #   beats the seed, and 0 isn't even
                                   #   a valid position

The seed of an accumulator loop must be either the operation's identity element or a value from the data itself. 0 is the identity of + (and 1 of *) — the identity of max is negative infinity, which is why the 0 seed smuggles in an assumption. Three correct forms, most idiomatic first:

max(a)                             # the builtin — max([-4, -2, -9]) → -2;
(max(a), index_of(a, max(a)))      #   pair it with index_of for the position
best, at: a[1], 1                  # seed FROM THE DATA — works for any
                                   #   numbers; empty input now errors loudly
                                   #   (guard with a.empty) instead of
                                   #   returning a plausible wrong answer
best: -inf                         # or seed with max's true identity —
                                   #   every number beats -inf

The transferable habit: a constant seed encodes a claim about the data — test the claim, not just the happy path. Two inputs kill this whole bug class in review: a list of negatives and the empty list. (Note max([]) returns none — the builtins follow the query-never-crashes convention; a hand-rolled version must choose its own empty-input answer.) Axioma can also make the claim executable: declare ensures: result[1] in a on the function and every call — and check maximum over random inputs — polices it. See Contracts — requires / ensures / check f.

Sequence accessors — xs.length, xs's first, xs.indexed

Array, Tuple, String, Set, and Range carry a small closed set of read-only accessors, available in both the dot and the possessive spelling. Each mirrors its builtin twin (length/size ≡ len, first/last ≡ first()/last(), indexed ≡ enumerate(xs)):

nums: [10, 20, 30]
nums.length          # → 3        ;  nums's length → 3 (same accessor)
nums.first           # → 10       ;  nums.last → 30
nums.second          # → 20       ;  nums's third → 30 (ordinals second..tenth)
[].first             # → none     (empty: no crash — check xs.empty first)
[99].second          # → none     (out of range → none, where second([99]) errors)
"hello".last         # → "o"      (String edges — and ordinals — are whole runes)
{3, 1, 2}.first      # → 1        (sorted order, same as first(set))
{3, 1, 2}.second     # → 2        (set.second == second(set))
(1, 2, 3).size       # → 3        ;  {}.empty → true

nums.indexed         # → [(1, 10), (2, 20), (3, 30)] — the pairs feed the
                     #   indexed loop forms (§6) and comprehension destructure
"ab".indexed         # → [(1, "a"), (2, "b")]   (runes, like the edges)
{30, 10, 20}.indexed # → [(1, 10), (2, 20), (3, 30)] (canonical sorted order)
(3..1).indexed       # → [(1, 3), (2, 2), (3, 1)] — ranges keep DIRECTION
(1..).indexed        # catchable Error — an open range can't materialize;
                     #   loop it with `for e at i in 1..` + break instead

Parentheses apply a function, so nums.size() is not the length: nums.size is an Integer, and calling it is an error that names the property and the source line. Write the property with no parentheses (nums.size, nums.len, nums.length), or len(nums) / size(nums) in function position.

The accessors are read-only (nums.length: 5 is an error) and the accessor table is deliberately closed — but an unknown name on one of these receivers now falls back to the unary vocabulary (next section), so xs.sum answers sum(xs). Multi-argument transformation stays function-first (map(f, xs), not xs.map(f) — the fallback is strictly unary). Hashes are not included: a hash's dot namespace is its own keys (d.length reads the user key length), so hash metadata stays with len(d) / keys(d) / values(d). count is not an accessor name (it is the reserved comprehension keyword), and nth has no accessor form (it takes an argument — nth(xs, k) stays a builtin). The dot spelling has full --vm parity; the possessive is evaluator-only, like all possessive forms.

Lists and recursion — [h | t]

Arrays are the sequence. [h | t] conses onto one and destructures one, so the classic recursive list algorithms are written directly on arrays — there is no separate list type to convert to and from.

func total([])      [0]
func total([h | t]) [h + total(t)]
total([1, 2, 3, 4])               # → 10

The same spelling works in four positions:

# 1 — value position: cons
[1 | [2, 3]]                      # → [1, 2, 3]
[1 | []]                          # → [1]

# 2 — multi-clause function head (above)

# 3 — match arm
tot: func(xs) [
  match xs with
  | []      => 0
  | [h | t] => h + tot(t)
]

# 4 — relation head, where it UNIFIES in both directions
relation append(a, b, c)
append([], Ys, Ys) :- true
append([X | Xs], Ys, [X | Zs]) :- append(Xs, Ys, Zs)

{Z | Z <- append([1,2], [3], Z)}          # forward → {[1, 2, 3]}
{(A,B) | (A,B) <- append(A, B, [1,2,3])}  # reverse → all four splits:
                                          #   {([1,2,3],[]), ([1,2],[3]),
                                          #    ([1],[2,3]), ([],[1,2,3])}

Prolog's multi-head cons [X, Y | T] (several elements, then a tail) is the same ListPattern with more than one head. It constructs, destructures in a func head, and unifies in a relation head:

[1, 2 | [3, 4]]                           # → [1, 2, 3, 4]
func twohead([a, b | t]) [(a, b, t)]
twohead([1, 2, 3, 4])                     # → (1, 2, [3, 4])
lsplit([X, Y | T], [X | L], [Y | R]) :- lsplit(T, L, R)

A nested [a | [b | t]] in a function head is a SyntaxError (the rest binder is a name); write [a, b | t]. Nested cons in a relation head or in value position was already legal. A bare _ as a whole relation-head argument is the anonymous wildcard (lpart(_, [], [], []) matches any pivot); _ inside [H | T] always was.

Reverse-mode list unification — splitting a list given only the result — is the one thing here that pattern matching alone cannot do. It comes from the relation engine, not from the array.

Because the cons tail may be a call (July 2026), a recursive constructor reads the same way it destructures:

func lmap(_, [])      [[]]
func lmap(f, [h | t]) [[f(h) | lmap(f, t)]]
lmap(func(x) [x * x], [1, 2, 3])            # → [1, 4, 9]

func lapp([], ys)      [ys]
func lapp([h | t], ys) [[h | lapp(t, ys)]]
lapp([1, 2], [3, 4])                        # → [1, 2, 3, 4]

func ins(x, [])      [[x,]]
func ins(x, [h | t]) [ if x <= h then [x | [h | t]] else [h | ins(x, t)] ]
func isort([])      [[]]
func isort([h | t]) [ins(h, isort(t))]
isort([5, 2, 8, 1, 9, 3])                   # → [1, 2, 3, 5, 8, 9]

The tail may be an identifier, a list, a call, a property read, an index, or a whole comprehension. It may not be an infix expression — [h | a + b] still reads as a comprehension clause, which is where the genuine ambiguity with a filter lives. The tail must also evaluate to a list: [1 | 2] is rejected with "list-cons tail [.. | t] must be a list, got INTEGER", so there are no improper lists or dotted pairs.

Two traps worth naming:

• first / rest / last, not head / tail. head and tail are the homoiconicity AST accessors — head(xs) on an array errors with "argument must be an AST value". first(xs) / rest(xs) are the list accessors, and rest does not deep-copy, so a recursive first/rest descent is linear. The short spellings hd and tl are exact aliases of first and rest. Note that tl is rest, not last — the tail of a list is a list: tl([1,2,3]) is [2,3] where last([1,2,3]) is 3. And hd is partial where tl is total: hd([]) raises, tl([]) is [], so write the base case as empty?(xs) rather than leaning on the tail to fail.
• In a match arm, [h] is a block, not a one-element array — it evaluates to h. Everywhere else (binding right-hand side, call argument, operand, function-body last expression) [h] is the array [h]. Write [h,] when you mean a one-element array: it reads as an array in every position.

For a mutable chain — sharing, cycles, O(1) splice — use hash nodes rather than arrays; {val: v, lnk: nd} is a node and hashes are reference types. See test_doubly_linked_list.ax for a full doubly linked list with O(1) unlink from a bare node handle. Note that next is a reserved word, so either spell the field lnk/nxt or keep the conventional name with the guarded form $next, which stores the key bare:

xs: none
xs: {$next: xs, value: 1}
xs: {$next: xs, value: 2}
l: xs
while l [ println(l.value) ; l = l.$next ]   # `none` is falsy, so no != test

Unary dot fallback — xs.sum ≡ sum(xs) ≡ xs's sum

On a slot-less value — Array, Tuple, String, Set, Range, scalars, Bytes, Bag, AST — a dot or possessive read whose name is not an accessor applies the named unary operation to the receiver. One name, three positions, for the whole unary vocabulary:

xs: [3, 1, 4, 1, 5]
xs.sum                   # → 14        ≡ sum(xs) ≡ xs's sum
xs.sort                  # → [1, 1, 3, 4, 5]
xs.sort.reverse.first    # → 5         chaining falls out of naming
{1, 2, 3}.sum            # → 6         ;  (1..5).sum → 15
"hello".upper            # → "HELLO"   ;  "  hi  ".trim → "hi"
16.sqrt                  # → 4         scalars are slot-less, so eligible
double: func(x) [x * 2]
7.double                 # → 14        user functions participate identically
bytes("abc").len         # → 3         Bytes/Bag/AST get accessor parity free

The name resolves exactly as in function position — lexical environment first (user bindings shadow builtins), then the builtin table — and the accessor table above keeps precedence (xs.len answers the count even if len is rebound). Records and namespaces never fall back: a hash keeps miss → none (data wins — d.sum reads the key sum), entities and Concepts keep their property-not-found errors, and modules stay name qualification (math.sqrt is a member lookup, never sqrt(math)). Because a miss on every eligible receiver was already an error, the fallback only turns errors into answers.

The fallback for reads is strictly unary: xs.push surfaces the builtin's arity error. Registered collection calls, described next, add explicit receiver placement. On collection receivers, a lexical user-function call xs.f(a) passes xs first, as described next. To call a function returned by unary application, write f(xs)(a). Scalar receivers retain the earlier unary-result-call behavior. A non-callable name errors; an unresolved name produces the usual miss error ending with "…, or any unary operation in scope". Variadic operations remain unary-callable (xs.max → 5, the fold reading; "abc".max → "abc", max-of-one). The original unary-dot reads have --vm parity; new collection method calls are interpreter-side.

Collection method calls

The interpreter provides explicit method spellings for collection operations:

xs: [1, 2, 3]
xs.length                            # → 3, existing property
xs.length()                          # → 3, method call
xs.map(x -> 2 * x).reverse()          # → [6, 4, 2]
xs.filter(x -> x > 1)                 # → [2, 3]
xs.reduce(func(a, b) [a + b], 0)       # → 6
xs.contains(2)                       # → true

The method registry fixes the receiver position: xs.map(f) is map(f, xs), xs.filter(p) is filter(p, xs), and xs.reduce(f, init) is reduce(f, init, xs). Other registered methods put the receiver first: push, append, reverse, rev, sort, sorted, sum, prod, mean, min, max, length, len, size, count, first, last, rest, nth, contains, collect, elements, each, transpose, and shape. Builtin domain and mutation rules are unchanged: m.length() still refuses a Matrix; use m.shape(). Builtin receiver positions come from this registry.

On a collection property miss, a user function in scope receives the collection as its first argument, followed by the written arguments:

scale(values, factor) = values .* factor
xs: [1, 2, 3]
xs.scale(2)                          # → [2, 4, 6], scale(xs, 2)

This is one call, so overload selection sees the complete argument list. It supports the function's ordinary named/default/rest arguments and contracts. No candidate function is executed to guess the argument order. The rule covers existing collection receiver kinds; it does not add receiver insertion to scalar values or change record/module lookup.

Bare xs.scale keeps unary application. For the earlier two-stage call meaning, explicitly call the returned function:

maker(values) = (n -> length(values) + n)
maker([1, 2, 3])(10)                 # → 13

This replaces the earlier xs.maker(10) spelling. Extra parentheses around xs.maker alone do not select the old rule; use maker(xs)(10) or store the returned function in a binding before invoking it.

The receiver and written arguments are each evaluated once. Records, entities and modules keep their own fields. A callable field or accessor remains callable: [func() [99]].first() still returns 99. Lexical user functions on a property miss receive the collection first, including when they shadow a registered builtin name. Known accessors retain priority. Empty .first is a harmless absence query; .first() delegates to the builtin and errors on an empty Array. On lazy iterators use first(it) for extraction; .first() retains the old callable-result reading. For labels or refinements, use the builtin function form. Unsupported VM method forms refuse; existing callable-field calls continue to work.

Tuples

pair: (3, 4)
trip: ("Alice", 30, "engineer")

k => v is a Pair, the key–value cell — not a Tuple and not a Dictionary; k -> v is the same Pair (the thin arrow is the second spelling, since 2026-09-04, and a Pair always prints as =>). {k: v} stays the dict literal. dict(...) and arrays consume Pairs as values. Bare x => body / x -> body and (params) => body stay lambdas: a name on the left is a function of it, whichever arrow. Match / cond arm arrows are unchanged, and the Unicode → is implication, not a Pair. {'X' => 10} is a set of one Pair. The REBOL coordinate 100x200 is retired.

p: 'X' => 10
p.first                 # X
p.second                # 10
@p                      # Pair
p == ('X', 10)          # false
pair('X', 10) == p      # true
1 => 2 => 3             # 1 => 2 => 3 — right-associative, nested Pairs
'X' => 10 |> second     # 10
1 -> "one"              # 1 => "one" — the thin arrow builds the same Pair
dict('I' => 1, 'X' => 10) == {I: 1, X: 10}    # true
dict([1 => "one", (2, "two")])                # one Array / List / Set of Pairs or 2-tuples
dict(zip([1, 2], ["one", "two"]))             # zip() and items() produce that shape

Write (x, 10) when the left side is a name whose value you want — x => 10 is a function of x. pair() with no arguments is refused.

Lists (persistent cons lists)

Where an Array is a place (mutable, reference-semantic, growable in place), a List is a value: an immutable, singly-linked cons list whose cells can be shared safely. Write `[1, 2, 3] for a List literal and `[] for the empty List. The backtick touches the opening bracket; there is no closing backtick. [] remains an Array. The conversion constructor list retains the array()/set()/tuple() zero-or-one arity:

e: `[]                       # the empty List — a TRUTHY value, not a bottom
l: `[1, 2, 3]                # evaluate elements and construct a List
m: cons(0, l)                # O(1) persistent prepend — l is untouched
n: 0 cons l                  # the same call, written infix
first(l)                     # → 1            O(1) head
rest(l)                      # → `[2, 3]   O(1) SHARED tail — no copy
l == list([1, 2, 3])         # → true  (elementwise value equality)
l == [1, 2, 3]               # → false (type-strict against Array)
l[2]                         # → 2 — O(n) courtesy read; l[2] = 9 is an ERROR
map(lambda x => x * x, l)    # → `[1, 4, 9] — map/filter preserve the type
{x | x <- l, x > 1}          # lists feed comprehensions, foreach, quantifiers
array(l)                     # → [1, 2, 3] — cross the boundary explicitly

List literals evaluate each element once, from left to right. Each expression contributes one value: nested Lists, Arrays and Ranges stay nested. A trailing comma is allowed, and `[x] always makes a singleton List, including in a function or branch body. No intermediate Array or lookup of the name list is needed. The spine is immutable; a mutable value stored inside retains its identity. Printing uses the same literal notation: `[], `[1] and `[1, 2, 3]. This is the primary form in examples and display; list() and list(collection) remain fully supported with their existing behavior.

println(`[1 + 2, `[4], [5]])   # `[3, `[4], [5]]
println(len(`[1..3]))          # 1 — one Range value, not three elements
println(`[1, 2] :+ 3)          # `[1, 2, 3]
println(1 +: 2 +: `[])         # `[1, 2]

This prefix is construction, not quotation: quote(...) and '[...] retain their AST meanings. Named backtick glyphs and infix calls are unchanged. The new literal does not introduce comprehensions or new pattern forms; continue to use [h | t] and [] in sequence patterns. Evaluator and VM construct Lists; unsupported VM element expressions still refuse. HM --infer reports List literals outside its inferred fragment. --typecheck traverses the elements and checks explicit List of T annotations.

Spreading Arrays and Lists. A direct literal element prefixed with ... inserts the source sequence's elements in order. The outer literal determines whether the result is an Array or a List:

let source = [1, 2]
let linked = `[...source]
let copied = [...linked]
println(linked)                    # `[1, 2]
println(copied)                    # [1, 2]
println(`[0, ...source, 3])         # `[0, 1, 2, 3]
println(`[source])                 # `[[1, 2]] — the Array is one element
println([...source, ...linked])    # [1, 2, 1, 2]

Each operand evaluates once, left to right. A spread copies the source's outer elements immediately, before the next operand runs; nested values retain their identity. The result does not inherit an Array source's element contract: an explicit annotation on the result supplies its contract. Both evaluator and VM support this construction; --typecheck checks known operands and element types, while HM --infer explicitly skips spreading.

Only Arrays and Lists can be spread. For another collection, convert explicitly with list(value) or array(value) first. `[x] always wraps one value; `[...xs] inserts its elements. [...xs] is an Array even in a function or branch body. Spreading adds no call-argument or pattern syntax. Existing ...rest, set progressions, and the Array's syntactic range expansion remain unchanged; a Range directly inside a List remains one element.

The display change does not rename existing collection keys or canonical fact identities: those retain the legacy List spelling internally.

cons is the one new word (no car/cdr aliases). Infix h cons t is the same call, right-associative: 4 cons 2 cons 3 cons list() packs as cons(4, cons(2, cons(3, list()))). : is binding and :: is ascription; they are not cons. The empty List is `[] or list(); [] is an Array. cons requires a List second argument — proper lists only. Variadic list(1, 2, 3) is refused with a hint: the primary build spelling is `[1, 2, 3], the one-value wrap is `[x] (also cons(x, list())), so list(a) can never be ambiguous. is List, is_list(l) and list?(l) test the type (list? no longer aliases array?; an Array argument errors with a migration hint). The accumulate idiom is acc: cons(x, acc) in a loop, then reverse(acc) — every step O(1).

l1 + l2 concatenates, constructing: the left spine is copied and the right operand is shared as the result's tail (the persistent append); list() is the identity on either side, and List + Array errors — crossing the boundary is always explicit. sort(l) returns a sorted List, and lists take their place in the canonical order componentwise (numeric-aware, a proper prefix before its extension, never interleaved with Arrays), so sets of lists walk deterministically and sort_by/min_by/max_by order them the way a reader expects.

Why a List answers no message verbs. a push 4 is an imperative sentence: it commands a place — something with identity over time — to be different afterwards. A List has no such identity; like the number 5, it simply is its content. Every reading of l push 3 fails on its own terms: mutating the cell would silently edit every list sharing that spine (structure sharing is exactly what makes cons/rest O(1) — cells must never change); rebinding l under a verb would be assignment wearing a message costume; and constructing a new list only to discard it would be a silent no-op — precisely the bug class the retired discarded-grow lint existed to catch. So the refusal is loud and teaching:

l: `[1, 2]
l push 3    # ERROR: a List is a value and 'push' is an imperative —
            #        build a NEW list with cons(x, l) or l1 + l2, ...

A place takes imperatives (a push 4, s push 4); a value takes expressions (cons(0, l), l + m, first/rest). The grammar itself tells you which one you are holding.

[h | t] is shape-generic. The cons pattern — in relation heads, match arms, and multi-clause func heads — destructures a List as well as an Array, and on a List the tail binds as the shared spine: O(1) per step, so a recursive walk is linear where the same walk over an Array copies its tail every step. One definition serves both sequence types, and a body-position [f(h) | rest] rebuilds in the tail's own type:

func total([])      [0]
func total([h | t]) [h + total(t)]
total([1, 2, 3, 4])         # → 10  (Array walk — tails copied)
total(list([1, 2, 3, 4]))   # → 10  (List walk — tails shared, linear)

relation app(a, b, c)
app([], Ys, Ys) :- true
app([X | Xs], Ys, [X | Zs]) :- app(Xs, Ys, Zs)
{Z | Z <- app(list([1, 2]), list([3]), Z)}   # → {`[1, 2, 3]} — List in, List out

Sequence prepend and append

x +: xs prepends one element; xs :+ x appends one element. The sequence operand must be a List or Array, and the result has that same kind. Both operators construct a new sequence without modifying the original. An Array or List used as the element stays nested: these operators do not concatenate.

println(1 +: 2 +: `[])       # `[1, 2]
println([] :+ 1 :+ 2)           # [1, 2]
println([1, 2] :+ [3, 4])       # [1, 2, [3, 4]]
println((1 +: [2]) :+ 3)        # [1, 2, 3]
println((1 + 2) +: [4])         # [3, 4]

+: groups from the right; :+ groups from the left. They share the multiplicative precedence band with word cons, above addition and comparisons. Use parentheses around arithmetic elements and to mix +: with :+: 1 +: [2] :+ 3 is rejected until its grouping is explicit. This precedence is Axioma's existing cons convention, not ML's lower-than-addition precedence. Both operands are evaluated once, left to right. Binary function spellings (+:)(x, xs) and (:+)(xs, x) are also available.

List prepend is O(1) and shares the tail; List append is O(n) and copies the spine. Both Array operations are O(n): they copy outer storage, preserve nested object identity and retain explicit element constraints such as Array of Integer. They are shallow operations, not deep copies. Use repeated List prepend followed by reverse to accumulate linearly. cons(x, xs) stays List-only; Strings, Bytes, Tuples, Sets and Dictionaries are not sequence operands for this pair.

The adjacent characters +: and :+ are now reserved operator tokens. Write 2 + :x for addition of a get-word and n: +3 for a binding to a positive number; the former compact spellings 2+:x and n:+3 now mean sequence operations. Positive slice bounds such as xs[1:+2] keep their slice meaning. :: remains reserved for type annotations.

Sets

Sets are unordered collections of unique elements, written with braces. Duplicates collapse and order is irrelevant — {3, 1, 2, 2} is {1, 2, 3}, and {1, 2, 3} == {3, 2, 1}. The empty set is {} (equivalently set(), emptyset, or ∅); len(s) is the cardinality.

{3, 1, 2, 2, 1}          # → {1, 2, 3}    (deduped, unordered)
{1, 2, 3} == {3, 2, 1}   # → true         (order-independent)
{} == emptyset           # → true         ; set() == ∅ → true
len({1, 2, 3})           # → 3

Unordered as a value, deterministic as a walk. A set has no intrinsic order — that is what {1, 2, 3} == {3, 2, 1} means. But anything that walks a set has to pick some order, and Axioma guarantees it is always the same one: the set's canonical order, which is what first, nth, s[i], and display all show. Every consumer agrees with them — every loop form (foreach, repeat, loop), map, filter, array(s), the folds (reduce, foldl, foldr), and the Enumerable verbs (take_while, sort_by, min_by, group_by, flat_map, …).

s: {30, 4, 100, 2, 77}
first(s)                     # → 2       (canonical order is NUMERIC for numbers)
array(s)                     # → [2, 4, 30, 77, 100]
reduce(func(a, x) [a + str(x)], "", s)   # → "243077100" — the SAME on every run

This matters because a fold is order-sensitive: without the guarantee, reduce over a set would return a different answer each time you ran the program. Sets built by different insertion orders are indistinguishable to every consumer, which is the point.

The order itself is numeric for numbers. Elements compare at their exact mathematical value, so the whole exact tower — Integer, Float, Rational — sorts as one line by magnitude, at arbitrary precision:

array({2, 10})                  # → [2, 10]        (not [10, 2])
array({1/2, 0.25, 2, 3/2})      # → [0.25, 1/2, 3/2, 2]
array({2^100, 5, 2^64})         # → 5, then 2^64, then 2^100 — by magnitude,
                                #   at arbitrary precision (printed in full)
array({inf, 5, -inf})           # → [-Inf, 5, Inf]
array({"b", "a", "c"})          # → ["a", "b", "c"]   (strings by codepoint)

Non-numeric elements keep a stable order of their own, so a set mixing types still walks the same way every time. The law is checkable — axioma lib/laws/determinism.ax runs it as a property test.

Converting — array(s) materializes a set as an Array in canonical order, and set(xs) deduplicates any collection into a Set. They join the bare type-name coercions (str, int, float, bytes).

tuple(c) completes the family, materializing any of them as a fixed-arity Tuple. All three also answer the no-argument call with their empty value — the explicit spellings of the literals [], {} and ().

array({3, 1, 2})         # → [1, 2, 3]
set([1, 2, 2, 3])        # → {1, 2, 3}
tuple([1, 2, 3])         # → (1, 2, 3)
array(set([9, 1, 9]))    # → [1, 9]       (round trip)

array()                  # → []           (≡ the literal; a FRESH array each call)
set()                    # → {}           (≡ ∅)
tuple()                  # → ()

make_tuple is a different facility — it builds an AST node, not a value.

Algebra — each operation has a word form and a glyph, and yields a set:

a: {1, 2, 3, 4, 5}
b: {3, 4, 5, 6, 7}
a union b        # ∪   → {1, 2, 3, 4, 5, 6, 7}
a intersect b    # ∩   → {3, 4, 5}
a difference b   # \   → {1, 2}
a symdiff b      # △   → {1, 2, 6, 7}   (in exactly one of the two)

Relations & membership — each returns a Boolean:

2 in a               # → true    ;  9 notin a → true
{1, 2} subset a      # → true    ;  a superset {1, 2} → true
{1, 2} subsetneq a   # → true (proper) ;  a subsetneq a → false
2 ∈ a   and   {1, 2} ⊆ a    # → true    (glyphs work everywhere the words do)

in / notin are not set-only. Membership spans the whole container family, and the answer never depends on the element's type:

2 in [1, 2, 3]        # → true    Array
"b" in ["a", "b"]     # → true    Array of String
2 in (1, 2, 3)        # → true    Tuple
2 in 1..5             # → true    Range
2 in bag([1, 2, 2])   # → true    Bag
"a" in dict("a", 1)   # → true    Dictionary — tests the KEY
"ell" in "hello"      # → true    String — substring, not element
'e' in "hello"        # → true    Character in String

A right operand outside that family is refused, and the refusal names it: 2 in 3 → right operand of 'in' must be a set, infinite set, bag, array, tuple, string, range, or dict; got INTEGER.

Powerset & Cartesian product:

powerset({1, 2})                      # → all 4 subsets: {}, {1}, {2}, {1, 2}
{(x, y) | x <- {1, 2}, y <- {3, 4}}   # Cartesian product via a comprehension →
                                      #   {(1, 3), (1, 4), (2, 3), (2, 4)}

See also. Set comprehensions and quantifiers — {x | x <- s, p(x)}, forall / exists over a set — are covered in §7. The Ellipsis sets subsection just below covers textbook and infinite sets ({2, 4, 6, ...}) and the built-in number sets ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ. Draw set relationships as a diagram with venn(...) — see §23.

Ellipsis sets — textbook {2, 4, ..., 100} / {2, 4, 6, ...}

The ... ellipsis writes an arithmetic progression the way a textbook does. A bounded form materializes a set; an open form (no upper bound) is a lazy infinite set. The step is inferred from the leading terms — a third term, if given, must confirm it.

{2, 4, ..., 100}        # → {2, 4, …, 100} — a 50-element set
{1, ..., 10}            # step defaults to 1 → {1..10}
{10, 8, ..., 2}         # descending (step −2)

B: {2, 4, 6, ...}       # infinite (lazy)
first(B)                # → 2    ;  tenth(B) → 20  ;  nth(B, 50) → 100
first(B, 5)             # → {2, 4, 6, 8, 10}
100 in B                # → true ;   7 in B → false
first((x | x <- B, x > 10), 3)       # → [12, 14, 16]   (a filtered lazy stream)

Integer progressions only (non-integer or non-linear → a clear error pointing at an explicit generator like {x | x <- range(...)}); bounded sets cap at 1,000,000 elements. For an ordered infinite sequence use this form or infinite_set("naturals") — a bare naturals / ℕ generator enumerates unordered.

Pulling elements. first(s) is the first term; the ordinals second(s) … tenth(s) and the general nth(s, k) give the k-th — on a finite collection or an infinite set (tenth({2,4,6,...}) → 20). last(s) errors on an infinite set (no last element). Membership uses in: ellipsis and named sets test it exactly and instantly, while a custom function-defined set (infinite_set(func(n) [...])) does a bounded generate-and-check (up to 100k terms, with an early exit once an ascending sequence passes the target) — so 9 in infinite_set(func(n) [n * n]) is true without ever running away.

The standard number sets. The chain ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ is built in. The identifiers rationals / reals / complexes and the glyphs ℚ / ℝ / ℂ are membership sets:

3 in reals                # true   (an integer is real…)
2.5 in reals              # true   ; 2.5 in rationals → false  (a decimal reads as a real)
rational(1, 2) in rationals   # true
complex(0, 1) in complexes    # true ; complex(0, 1) in reals → false (nonzero imaginary part)
first(rationals, 5)       # {0, 1, -1, 1/2, -1/2}   (ℚ is countable → enumerable)
first(reals, 5)           # ERROR: ℝ is uncountable — use a membership test instead

Membership is type-faithful: an Integer belongs to all four; a RationalNumber to ℚ/ℝ/ℂ; a Float reads as a real, not a rational (decimals approximate reals — assert rationality with a rational(p, q) literal); a ComplexNumber belongs to ℂ, and to ℝ only when its imaginary part is 0. ℚ is countable, so first(rationals, n) enumerates it (Calkin–Wilf order, signs interleaved); ℝ and ℂ are uncountable and so are membership-only (enumeration is a clean error). infinite_set("rationals" | "reals" | "complexes") builds the same sets.

Bags (multisets)

A Bag is an unordered collection in which the same value may appear multiple times. Bags sit between Sets (no duplicates) and Arrays (ordered duplicates):

words: bag(["the", "quick", "the", "fox", "the"])
count(words, "the")          # 3 — multiplicity of an element
len(words)                   # 5 — total Σ multiplicities
"the" in words               # true
distinct(words)              # {the, quick, fox} — underlying support set

Operators. Standard multiset algebra is wired infix:

b1 ∪ b2        # union — max counts per element
b1 + b2        # additive sum — counts add (independent observations)
b1 ∩ b2        # intersection — min counts
b1 - b2        # difference — clamped at zero
b1 == b2       # multiset equality

∪ and + are genuinely different: bag([a,a]) ∪ bag([a]) == bag([a,a]) but bag([a,a]) + bag([a]) == bag([a,a,a]).

Comprehension iteration is over distinct elements (the underlying Set support), since {...} cannot carry multiplicities. Use to_array(b) to iterate every occurrence.

As slot values. Bags can be slot values on Concepts; the unify machinery uses additive sum as the merge policy — two partial observations of the same entity combine their evidence.

Typical use cases: word-frequency counts, inventory, voting tallies, evidence merging. Bags are first-class in SETL, Z, B, VDM-SL, Smalltalk, Python's Counter, C++ std::multiset, and Guava Multiset; they fill the same role in Axioma.

Tests: tests/axioma/collections/test_bag_basic.ax, test_bag_operators.ax, test_bag_use_cases.ax, test_bag_slot_value.ax.

Dictionaries ({key: value} literals)

person: {name: "Anna", age: 24}              # Unquoted keys
obj: {"first-name": "Bob", "age": 30}     # Quoted keys
nested: {user: {address: {city: "NYC"}}}

person.name          # "Anna" (dot access)
person["name"]       # "Anna" (bracket access)
person's name        # "Anna" (possessive — same as dot; miss → none)
dict()               # Empty dictionary  ({} is the empty SET ∅)
dictionary()         # same value — spelled-out twin of dict()
dict([1 => "one", (2, "two")])   # from one Array / List / Set of Pairs or 2-tuples
dict(zip(ks, vs))    # zip() and items() produce that shape; later entries win

delete person["age"] # retract a key; yields 24. Miss on an open map → none
person \ {"name"}    # NEW dict without those keys (pure). Right side is a
                     # Set or Array of keys — keys(other) composes.

type(person)         # "Dictionary"
person is Dictionary # true

A dictionary is a {key: value} map keyed by value: any value is a key, compared by ==, so 1 and 1.0 are one key and "1" another, and dict(1, "one"), dict(1 => "one") (or 1 -> "one") and {1: "one"} build the same entry. Build one with the {...} literal or, for the empty case, dict() — dictionary() is the spelled-out twin (constructor name = lowercase of the type), the same relationship as integer() / int(). type() and @ report "Dictionary", and x is Dictionary classifies it.

Naming note. This type was previously named ObjectMap (June 2026 standardized it to Dictionary and fully retired the old name — ObjectMap is now an undefined word, not an alias). Dict is accepted as a short alias in type annotations (x :: Dict) and is checks, matching the dict() constructor, but type()/@ always report the canonical Dictionary.

Schema field writes

A dictionary annotated with a row schema keeps its field contract after initialization. Property writes, index writes and writes through field references use the same checks in the evaluator and VM. The contract follows the dictionary object, so another name or a previously captured field reference cannot bypass it. A rejected write leaves the old value intact.

type WineRow = {alcohol :: Float | Na, quality :: Integer, note? :: String}
let wine :: WineRow = {alcohol: na, quality: 7}
let other = wine
other.alcohol = 12.5       # accepted; wine sees the same update
let p = &wine.quality
*p = 8                    # accepted; wine.quality is now 8
wine.note = "checked"     # an absent optional field may be added
delete wine["note"]       # an optional field may be removed

wine.alcohol = "twelve"   # Error: expected Float | Na
wine["quality"] = na      # Error: expected Integer
*p = "eight"              # Error: expected Integer
delete wine["quality"]    # Error: required field
wine.typo                 # Error in both runtimes, also for wine["typo"]

Optional means the key may be absent; it does not admit none or na as a present value unless the declared field type includes them. delete and del_key reject removal of required fields. Earlier field-type and requiredness constraints remain attached if another alias is annotated with a wider schema. Open dictionaries retain their ordinary insert/update/delete behavior.

copy(row), {row with field: value}, dictionary +, and dictionary \ retain schema contracts. Functional updates validate all replacement fields before attaching any new nested schemas. Dictionary + preserves both inputs' contracts. Removing a required field with \ is refused; removing an optional field produces an independent dictionary. copy preserves cycles and sharing among copied dictionary and array nodes.

Bindings, ascriptions, typed parameters and typed returns attach schemas in both runtimes, including schemas on nested dictionaries. --typecheck and the LSP diagnose incompatible writes when the receiver and field type are known; dynamic keys and other unknown types remain runtime checks.

This is a dictionary-field contract. Element mutation inside a field such as Array of Integer or Dictionary of String to Integer remains a separate collection-contract limitation; replacing that whole field is checked.

Unified type declarations

The unified header is type Name = kind-or-type-expression. Existing data, enum, concept, aliases, products, unions and opaque wrappers keep their meaning. In particular, concept Person remains the concise domain declaration.

type Distance = Float
type NumericCoordinate = Integer | Float
type Coordinates = (Float, Float)
type PersonId = opaque Integer
type Row = {x:: Integer, label?:: String}
type Point = struct {x:: Float, y:: Float}
type PointCursor = struct mutable {x:: Float, y:: Float}
type Shape = variant Circle(radius:: Float) | Origin
type Move = data Rock | Paper | Scissors
type Direction = enum North, East, South, West
type Person = concept

Records and mutation

Spellings: struct is the primary documented spelling; record is an alias in the type Name = kind slot. Both are immutable by default. Either mut or mutable after either word selects the same mutable struct: struct mutable, struct mut, record mutable and record mut are identical apart from spelling. Every form uses the existing struct AST, accepts braces or an end field body, and supports the same generic parameters. record means a nominal struct, not a structural Dictionary schema. It is contextual; ordinary record bindings and functions remain ordinary identifiers.

In the kind slot, record always starts a declaration, including an empty record … end body. If a variable named record holds a type value, write type Alias = (record) to reference it instead. The $record guard alone does not bypass a contextual kind marker; ($record) also works.

type Label = record {value:: Integer}
type Cell[T of Number] = record mut
    value:: T
end
type Counter = struct mut {value:: Integer}
type Gauge = record mutable {value:: Integer}
let cell = Cell(1)
let shared = cell
shared.value = 2
println(Label(1) == Label(1))
println({value: 1} is Label)
println(cell.value)
println(cell == shared)
println(cell == Cell(2))
println(Counter(3).value + Gauge(4).value)

This prints true, false, 2, true, false, 7, one per line: immutable values compare by value, a matching Dictionary is not a Label, shared mutable values observe the same checked field writes, and separate mutable constructions have distinct reference identity. All spellings retain the VM refusal below.

A struct is constructed with its own name, for example Point(1.0, 2.0). Fields must have explicit names; the :: annotation is optional. An annotated field is checked at construction and on every write, and an Integer given for a Float field converts to that Float the way an annotated parameter does, so P(1).x / 2 and P(1.0).x / 2 agree (a type-parameter slot keeps the argument's type). A bare lowercase name such as z declares an open field that accepts any value — the gradual reading every other unannotated position has, and the same rule as a bare data slot. A bare TitleCase word is refused, because a struct field needs a name.

type Pnt = record
    x :: Float,
    y :: Float,
    z            # open field: any value
end
Pnt(1, 2, "three").z   # "three"; x and y are 1.0 and 2.0

A matching Dictionary is not a Point. Structs do not register instances in a concept extent and do not support domain inheritance; has and had on a struct name refuse, as the article form does, because the field list is fixed by the declaration; P show properties lists the declared fields. An empty struct is constructed by Empty(); the bare name remains its type.

Immutable structs reuse single-constructor data values: structural equality, existing value identity and pattern matching, closed fields and shallow freezing. Nested Arrays, Dictionaries or mutable structs retain their own mutation rules.

Mutable structs use reference identity for both == and is/same. Two separate constructions are distinct, even with equal fields. Aliases share writes; copy(p) is the way to get an independent record, and the copy keeps the field validator. Set keys use stable reference identity, independent of field contents. Ordering refuses on every surface: the four operators, sort, sort!, sorted, min, max, and the keyed verbs when a key is or contains such a record. Order by a field key instead, sort_by(func(c) [c.x], cursors). Immutable structs keep their structural order in all of those, min and max included. An immutable let binding can hold a mutable struct: changing p.x does not rebind p.

A declared mutable field accepts p.x = value and writes through &p.x. Unknown fields and incompatible types refuse before modifying the value. Positional/index writes and index references are unsupported and refuse. {p with x: value} reconstructs a validated value for either struct kind; for a mutable struct it creates a distinct record. Untouched nested values stay shared. The validator belongs to the value, so updates also work after a local constructor leaves scope. Generic structs and variants reuse [T of Number] and the existing whole-field parameter rules: repeated T fields must agree in each construction or update; there is no implicit numeric promotion or specialized Point[Float].

Optional declaration bodies

Braces and end bodies parse field declarations into the same semantic nodes. Newlines separate fields; commas remain available. They do not execute arbitrary statements or introduce a class-body scope.

type Point = struct
    x :: Float
    y :: Float
end
type PointCursor = struct mutable
    x :: Float
    y :: Float
end
type Row = schema
    x :: Integer
    label? :: String
end
type Person = concept with
    name: ""
    age: 0
end
concept Student with
    university: ""
end
Student extends Person

schema explicitly opens a schema body. Concept bodies require with; bare concept Person and type Person = concept are complete declarations, including inside a surrounding function or loop. type Person = concept {name: ""} uses the existing concept slot/default rules, including their current enforcement limits. Struct field enforcement does not tighten ordinary concept slots. Aliases, opaque wrappers, tuple products, compact enums and variants do not require end. Variant alternatives may continue on lines beginning with |, and the first alternative may start on the next line as a TitleCase name; a header with no alternative refuses rather than reading the following statement as one. The kind words are contextual rather than new globally reserved identifiers. data in the kind slot is the same declaration as variant, so every standalone header's keyword is accepted after type Name =: type Move = data Rock | Paper, type Move = variant Rock | Paper and data Move = Rock | Paper are one declaration, with the same constructors, payloads, type parameters, tag, match and exhaustiveness checking. variant is the descriptive kind word in this section. Standalone variant, struct, record and schema headers are not forms. Bare TitleCase arms under type join existing types rather than declaring constructors; the refusal for type Move = Rock | Paper names type Move = variant Rock | Paper and type Move = enum Rock, Paper first, and the standalone spellings as the same declarations.

Execution surfaces

The parser and evaluator accept these forms, and --typecheck uses their existing semantic nodes, constructor annotations and parameter checks. A struct write is checked statically as a schema row's is — an undeclared field, a write to an immutable struct, or a value the field's annotation does not admit warns before the run — and a type declared inside a function body is visible to the checker from that point on. Runtime mutation checks remain authoritative; the static checker is not a proof of all writes. HM inference remains its existing supported fragment.

Top-level transparent schemas/products keep their existing VM support. Structs and variants lower to data declarations and explicitly refuse in the VM, as do enums and unsupported concept forms; opaque/local synonyms retain their existing refusal. No new VM record implementation is implied by a parser accepting a form.

Runnable tour: tests/axioma/showcase/type_declaration_family.ax.

Record update — { record with field: value, … }

{ r with … } returns a copy of r with the listed fields overridden. The original is never mutated, and later writes to the same field win.

Three kinds of value accept it, and they differ in how closed they are — that is, in what happens when you name a field the value does not have.

h: {name: "Ada", year: 1815}
{h with year: 1816}        # → {name: "Ada", year: 1816}
{h with nickname: "AL"}    # → adds the key — a hash is OPEN

A schema-annotated dictionary retains its contract and rejects undeclared or wrongly typed replacement fields. Dictionary record updates work in both the evaluator and VM; entity and constructor record updates remain evaluator-only.

A concept entity is closed: every field named must already be a property, so a typo is refused instead of quietly becoming a new slot. The copy is a fresh, independent individual, registered in its concept's extent.

concept Person { name: "", year: 0 }
ada: a Person { name: "Ada", year: 1815 }
older: {ada with year: 1816}
older.year                 # → 1816
ada.year                   # → 1815   — the source is untouched
{ada with nope: 1}         # → Error: field "nope" is not a property of concept Person

A data value is closed hardest: its slot list is fixed by the declaration and, unlike a concept, cannot later grow through has. This is also the only update path such a value has, because its slots refuse direct assignment — the tag and payload are the object, so p.x: 99 is an error by design.

data Point = P { x, y }
p: P { x: 1, y: 2 }
{p with y: 9}              # → P(1, 9)
{p with z: 9}              # → Error: field "z" is not a field of constructor P
p.x: 99                    # → Error — slots are frozen; rebuild instead

Because a rebuild carries the same tag and arguments, a no-op update is the original — identity falls out of the is/same rule rather than being special-cased:

{p with y: 2} is/same p    # → true    — same tag, identical arguments
{p with y: 9} is/same p    # → false

Positional constructors whose slots are declared by type — data Shape = Circle(Float) — have no field name to update by, and say so. Name the slots (Circle(radius)) to use the form.

Update rebuilds the spine, not the contents: an untouched field still holds the very same object, so a shared mutable payload stays shared.

JavaScript / TypeScript objects ↔︎ Axioma

# JS object literal → Dictionary
poet: {born: 1935, name: "Mary Oliver"}
poet's name          # "Mary Oliver"
@poet                # "Dictionary"

# Typed individual → entity (not a dict)
concept Poet
Poet has name: ""
mary: a Poet { name: "Mary Oliver" }
mary is Poet         # true
keys(mary)           # ["name"] — declared public slots
mary["name"]         # "Mary Oliver" — same hard miss as mary.name
poet["nosuch"]       # none (open hash)
mary["nosuch"]       # error (checked record)

A checked record is a concept instance. The hash literal is the open map. Choose the instance when you want undeclared fields to raise; keys / items / values / r[k] work on both, with that one difference on a miss.

REBOL’s influence in Axioma is mainly binding (:), refinements, and scalar value types — not a separate object! type. The hash is the JS/Monkey bag; entities own classification and kind.

Behavior interfaces — attach methods by type

Typeclass-style behavior without putting methods on dictionary values (no JS prototype / Ruby open classes on maps). Soft keywords; not reserved.

interface Showable {
  render: none                    # required op names (use non-reserved words)
}

implement Showable for Integer as {
  render: func(n) [ str(n) ]
}
implement Showable for Dictionary as {
  render: func(d) [ "dict:" + str(len(keys(d))) ]
}

dispatch(Showable, "render", 42)     # "42"
dispatch(Showable, "render", {a: 1}) # "dict:1"
42 is Showable                       # true after implement

# Concepts can implement interfaces; missing ops error at declaration
interface Drawable { draw: none }
concept Shape implements Drawable {
  draw: func(self) [ "shape" ]
}

Not the same as Carnap protocol_language / is_protocol (observational frameworks in the grounding layer). Not overridable: Eq / container keying stay structural (ObjectKey); use these interfaces for Showable-like ops, not for redefining ==.

Seeded at startup:

render(42)            # "42"
42 is Showable        # true
let x :: Showable = 42   # ok — same membership as `is`
5 is Numeric          # true
[1, 2] is Enumerable  # true
[1, 2] is Iterable    # true
[1, 2] is Sized       # true
[1, 2] is Indexable   # true
{a: 1} is Indexable   # false — Dictionary is keyed, not ordinal
elements([10, 20])    # [10, 20] — not iterate([10, 20])
[10, 20][2]           # 20
dispatch(Indexable, "at", [10, 20], 2)  # 20
dispatch(Indexable, "slice", [10, 20, 30], 2, 3)  # [20, 30]
check Showable        # ⊤ᵇ when all implements satisfy structural laws

combine("a", "b")     # "ab"
mempty("x")           # ""
mconcat(["a", "b"])   # "ab"
5 is Monoid           # false — + and * are both lawful; wrap one:
data Sum = MkSum(Integer)
implement Monoid for Sum as { combine: add_sums, empty: func(s) [ MkSum(0) ] }

check on a behavior interface verifies registered implements (e.g. render returns String) and any custom laws: predicates on the interface.

Under --vm, seeded names (Iterable, Sized, Indexable, Showable, …) and elements / dispatch on built-in types compile. implement … for and interface Name { … } refuse at compile time — run those without --vm.

Traits — shared method packs (trait / uses)

A trait is a named pack of methods (function slots only). It is not a kind: no extent, no a Trait {}, no extends Trait. Install packs onto concepts with soft-keyword uses (same house gate as interface / implement).

trait Printable {
  display: func() [ "display:" + it.title ]
  greet: func(who) [ "hi " + who + ", I am " + it.name ]
}

concept Document {
  title: ""
  name: ""
}
Document uses Printable

d: a Document { title: "Spec", name: "Doc1" }
d.display()                 # → display:Spec
d.greet("Ada")              # → hi Ada, I am Doc1
d is Printable              # false — traits are not kinds

Conflict rules. Local methods on the concept win (trait skipped for that name). Two traits in one uses list that both define the same method → error (no silent last-wins). Trait bodies may only hold functions.

With interfaces. concept Button implements Drawable uses BoxDraw — implements requires the ops; uses can supply the bodies.

Function-valued concept slots → methods (Actions)

A function value in a concept block or has is a method, not instance data:

concept Dog {
  name: ""
  bark: func(n) [ it.name + " barks " + str(n) ]   # → Actions, not Properties
}
rex: a Dog { name: "Rex" }
rex.bark(3)                    # → Rex barks 3
Dog has shout: func() [ upper(it.name) ]   # late-bound; existing instances see it

Methods live on the concept (shared, late-bound). They are not copied onto entities as rewritable fields. The explicit form Concept action name(params) [ … ] remains for the same table — required for operator overload (Concept action "+"(other) [ … ]) and still valid as dual spelling.

Manual: this section. Test: tests/axioma/concepts/test_traits.ax, test_function_slot_auto_promote.ax.

--typecheck residual for schema unions. When a name is a finite union of named dict schemas, "key" in x (and not ("key" in x)) narrows x to the alternatives that declare (or do not declare) that field:

type PoemPages = { name :: String, pages :: Integer }
type PoemRhymes = { name :: String, rhymes :: Boolean }
type Poem = PoemPages | PoemRhymes

f: func(p :: Poem) [
  if "pages" in p then needsPages(p) else needsRhymes(p)  # residual arms
]

A key present on all arms does not split. Non-schema unions are not refined. Tagged sum types still belong to data + match, not dict discriminants.

Stacks

First-class stack data type. See §18.

s: a Stack
s push 1
s push 2
s pop                # 2

Matrices, tensors & dataframes

Three numeric/data containers, constructed by builtins (no literal form). All three are first-class types — type(v), @v, and v is Matrix / is Tensor / is DataFrame agree.

Matrices — 2-D, with linear-algebra infix operators:

m: matrix([[1, 2], [3, 4]])                # 2×2 from nested arrays
type(m)                                    # → "Matrix"
m + matrix([[10, 20], [30, 40]])           # elementwise + / -
m * matrix([[5, 6], [7, 8]])               # MATRIX PRODUCT ;  m * 10 → scalar scale
m ^ 2                                      # matrix power (integer exponent)
transpose(m)                               # rows ↔ columns
det(m)                                     # → -2  ;  trace(m) → 5
reshape(matrix([[1, 2, 3], [4, 5, 6]]), 3, 2)   # 2×3 → 3×2
zeros(2, 2)                                # 2×2 of 0s ;  ones(2, 3) → 2×3 of 1s
solve(matrix([[2, 1], [1, 3]]), [5, 10])   # Ax = b → column vector (1, 3)

z: zeros(2, 3)
z[1, 2] = 1                                # row 1, column 2 (1-based)
z[2, 3] = 1
z[:, 2:$]                                  # columns 2 through last — a 2×2 Matrix
m[1, :]                                    # row as 1×n Matrix ;  m[:, 2] → column
m[1]                                       # first cell, row-major ;  m[0] errors
shape(z)                                   # [2, 3] ;  tuple(shape(z)) → (2, 3)

Index is 1-based on both axes. Last-index inside [] is $ (z[:, 2:$]), not end (end closes a block). size(z) is cardinality and errors on a Matrix — write shape(z). Nested arrays keep a[i][j]; a[1, 2] on an Array is refused. matrix cells must be numbers (matrix([["", ""]]) errors).

Iteration visits cells, row by row. for and foreach over a Matrix use the same order as its linear indices and m[:]. They do not yield row arrays. The iterator pulls one cell at a time, preserving its Integer, Rational, or Float type; starting another loop starts a fresh walk. No flattened copy is needed.

m: matrix([[-19, 23, 0], [-1, 22, -17]])
for v in m [println(abs(v))]              # 19, 23, 0, 1, 22, 17
collect(m)                               # [-19, 23, 0, -1, 22, -17]
[v * 2 | v <- m]                        # flat Array, same cell order
first(elements(m), 2)                    # [-19, 23], bounded lazy walk
for v in transpose(m) [println(v)]       # explicit column-major cell order

elements(m) and each(m) return a fresh single-use Generator; collect(m) and finite collection verbs such as map, filter, and reduce gather the same ordered cells. collect retains its allocation limit. Materializing is explicit and does not make len(m) / size(m) valid: dimensions still come from shape(m).

Loop binders are fresh on each iteration. Assigning to the binder does not change the matrix; an explicit write such as m[2] = 7 is visible when that cell is reached. Rebinding the name m does not redirect an already-started walk. To visit columns without constructing a transpose, use nested loops over shape(m)[2] then shape(m)[1] and read m[row, column]. Matrix iteration is supported in the interpreter; unsupported VM loop/iterator paths refuse.

Two naming gotchas. identity is the identity function (identity(42) → 42), not an identity-matrix constructor — write matrix([[1, 0], [0, 1]]). And there is no matrix-inverse builtin (inverse is the relation/set inverse) — for linear systems use solve(A, b) directly.

Tensors — n-dimensional generalization:

t: tensor([[[1, 2], [3, 4]], [[5, 6], [7, 8]]])   # rank-3 from nesting
shape(t)                                   # → [2, 2, 2]  ;  ndim(t) → 3
tensor([2, 3], 7)                          # shape + fill → 2×3 of 7s
tensor_reshape(tensor([1, 2, 3, 4, 5, 6]), [2, 3])  # → 2×3
squeeze(tensor([[1, 2, 3]]))               # drop size-1 axes → vector [3]
expand_dims(tensor([1, 2, 3]), 0)          # add an axis → 1×3

DataFrames — column-oriented tables (pandas-style):

df: dataframe({name: ["ada", "bob", "eve"], age: [36, 25, 30]})
type(df)                                   # → "DataFrame"
df_select(df, ["name"])                    # column projection
df_filter(df, func(row) [row["age"] > 26]) # row predicate — row is a Dictionary
df_sort(df, ["age"])                       # ascending (optional 3rd arg: ascending?)
df_head(df, 2)                             # first rows ;  df_tail(df, 1) → last rows
df_info(df)                                # schema: dtypes, non-null counts, memory
df_describe(df)                            # count / mean / std / min / quartiles / max

read_csv(path) loads a file into a DataFrame, and write_csv(df, path [, options]) writes one back (2026-08-27) — options {delimiter: ";", header: false, na: "NA"}; it returns the path, and integer cells keep their exact digits however large, so write∘read∘write is a fixed point. df_groupby(df, cols) buckets rows. (For plain in-memory grouping of arrays/hashes, group_by in §7 needs no DataFrame at all.)

Typed DataFrames. A row schema uses the existing dictionary type syntax; Float | Na permits a missing cell, while an optional field? permits an absent column. A present cell still has to satisfy its field's type.

type WineRow = {
    sample_id :: String,
    alcohol :: Float | Na,
    quality :: Integer
}
let wines = read_csv("wines.csv", {delimiter: ";", schema: WineRow})
let selected = df_filter(wines, lambda (row) => row.quality >= 7)
let revised = df_mutate(wines, "alcohol", [12.0, na])  # for a two-row table

dataframe(columns, {schema: WineRow}) checks in-memory columns against the same contract. The first version supports scalar String, Integer, Float, Boolean, None, Na, transparent aliases and unions of those types. Nested mutable cells are refused explicitly. Input column arrays are copied for typed tables so later writes through those arrays cannot violate the table.

With a CSV schema, String fields preserve text such as 00123; other fields parse as their declared type, with union alternatives tried in declaration order. Missing markers (by default NA, na, N/A, null, NULL, and the empty string, after trimming) become na and require a Na arm. Use na_strings: [] to preserve all those strings literally. Required columns, duplicate headers, invalid cells and unexpected columns are rejected with source/record/column context. extra_columns: "ignore" discards undeclared columns; the default with a schema is "reject". on_error currently accepts only "fail"; misspelled/unsupported options are errors. An empty file without headers cannot establish a schema; a header-only typed table is valid.

df_mutate(df, name, values) returns a new table with that column added or replaced, validates the complete candidate, and leaves df unchanged on failure or success. The row schema survives filtering, sorting, head/tail and column replacement; selection projects it onto the selected columns. df_filter requires a Boolean predicate result and reports predicate errors with a row number. The CSV writer validates typed tables before opening the output file.

These operations and top-level transparent type declarations work in both the evaluator and VM. Local type declarations and type ... = opaque ... remain evaluator-only. This adds no new schema grammar. Standalone row field writes also preserve their contracts; see Schema field writes above.

JSON is the value↔︎string pair to_json(v [, pretty]) / from_json(s) (2026-08-27) — pure functions, so they work in the browser build, and the file genre composes from shipped parts: from_json(read(%data.json)) and write(path, to_json(v, true)).

to_json({b: 2, a: 1})          # → {"a":1,"b":2} — keys SORTED, bytes stable
to_json({3, 1, 2})             # → [1,2,3] — sets in canonical order (one-way)
to_json(2 ^ 100)               # → exact digits, never a float
from_json("{\"k\": null}")     # → {k: none} — JSON's null IS none
to_json(om)                    # → Error: om has no JSON value (two bottoms,
                               #   one null — the round trip would lie)
to_json(1 / 3)                 # → Error: no finite JSON number — write
                               #   float(x) or a string if that loss is meant

6. Operators & Control Flow

Arithmetic

2 + 3       2 - 3       2 * 3       6 / 3       7 % 2       2 ^ 10
100 ÷ 7     10.0 ÷ 3.0                                     # floor division (glyph)
100 div 7   100 idiv 7                                     # same operator (keyword)
1 rdiv 8                                                   # word form of `/` → 1/8

Each binary operator has a symbolic/glyph form, a keyword form, and a prefix-builtin form. They produce identical AST and identical results — pick by readability:

True (exact/real) division is / and its word form rdiv — there is no Unicode glyph for it. ÷ is the floor form (Julia-style), not the elementary-school obelus for true division. Digraph: `div → ÷. fdiv is not an alias of /: it always returns a Float.

// is a line comment (full alias of #), pairing with block comments /* … */. It is not floor division.

100 ÷ 7       # → 14   (glyph)
100 div 7     # → 14   (keyword)
100 idiv 7         # → 14   (word alias of div)
100 quotient 7     # → 14   (keyword longhand)
div(100, 7)        # → 14   (prefix, keyword spelling)
idiv(100, 7)       # → 14   (prefix, idiv spelling)
quotient(100, 7)   # → 14   (prefix, long spelling)

1 rdiv 8           # → 1/8  (word form of /)
rdiv(1, 8)         # → 1/8  (prefix)
8 rdiv 2           # → 4    (whole quotient stays Integer)

100 % 7       # → 2    (symbolic)
100 mod 7     # → 2    (keyword)
100 modulo 7  # → 2    (keyword longhand)
100 remainder 7    # → 2    (keyword longhand)
mod(100, 7)        # → 2    (prefix, keyword spelling)
remainder(100, 7)  # → 2    (prefix, long spelling)
rem(100, 7)        # → 2    (prefix, short spelling — twin of div)
100 rem 7          # → 2    (keyword short)

divmod(100, 7)     # → (14, 2)   (combined — one division, both halves)

// this whole line is a comment
x: 10 // trailing comment (x is 10, not floor-div)

Each keyword has a prefix twin under its own name, so a reader holding mod never has to know that remainder is where it lives. mod / div / idiv / rdiv are not a second implementation: they hand their operands to the % / floor (div/÷) / slash (/) operators unchanged, which is why no example above can drift from its neighbour.

All four floor. The quotient rounds toward −∞ and the remainder takes the sign of the divisor, not the dividend — on integers exactly as on floats, so q * b + r == a holds for negative operands too:

-23 mod 7     # → 5     (NOT -2 — the sign follows the divisor)
23 mod -7     # → -5
-7 div 3      # → -3    (floor, NOT -2)
-7 ÷ 3        # → -3    (same)
divmod(-7, 3) # → (-3, 2)
mod(-23, 7)   # → 5     (prefix agrees, by construction)

/ / rdiv vs div/idiv/÷ for floats. / and rdiv are true/exact division (int/int may yield a Rational); floor division always returns an integer-valued result (floor toward −∞). The two differ for all float cases and for negative-result cases in particular:

100.0 / 7.0   # → 14.2857…   (real value)
100.0 ÷ 7.0   # → 14         (floor)
-7.0 / 3.0    # → -2.333…    (real value)
-7.0 div 3.0  # → -3         (floor toward -∞, NOT -2)

mod / modulo / div / idiv / rdiv / fdiv are soft keywords: lexed as plain identifiers and recognized as infix operators only when they sit between two expressions on the same line. Variables, hash keys, and function names with these spellings keep working (mod: 99, h.div, rdiv: 9).

Comparison

==   !=   ===   !==   <   >   <=   >=
3 ≤ 5         # glyph twin of <=  (≥ for >=; ≠ for !=; slanted ⩽ ⩾ also lex)
0 ≤ x < 10    # ordering comparisons CHAIN: ⇒ (0 ≤ x) and (x < 10)
1 == 1.0      # true   exact tower — mixed Integer/Float at the exact value
1 === 1.0     # false  type-strict (infix equal?); 1 !== 1.0 is true
'a' == "a"    # true   a Character is its one-character String as a VALUE
'a' === "a"   # false  …and a distinct TYPE — the Byte precedent (byte(65) === 65 is false)

== is the exact-tower equivalence: 1 and 1.0 are the same number, and collections key by ==. === / !== are Elixir-style strict equality — same as equal? / not equal? — so an Integer never strictly equals a Float, at any depth ([1] === [1.0] is false). The same line separates the equal as values, distinct as types pairs: byte(65) == 65 and 'a' == "a" hold, byte(65) === 65 and 'a' === "a" do not, at any depth (['a'] === ["a"] is false), while collections still key by == ({'a', "a"} has one element). Ordering comparisons (< <= > >= and their glyphs) chain like the mathematician's interval notation — a < b < c desugars to (a < b) and (b < c), reusing the middle operand. Equality (== != === !==) deliberately does not chain, preserving the (a == b) == c boolean idiom. Digraphs: `leq / `geq.

Compound assignment

i: 5
i += 1        # ≡ i = i + 1   (also -= *= /=)
s: "log"
s += ":entry" # + concatenates strings/arrays, so += inherits that
c.n += 1      # property, index, and dereference targets work too
xs[2] += 7    #   — the same target set the `=` form supports

target op= value is statement-level sugar: it desugars at parse time to the same AST as target = target op value (find-or-update), so the evaluator and --vm inherit semantics byte-for-byte. It is not an expression — y: (x += 1) is a parse error, so there is no value-of-assignment ambiguity. Only += -= *= /= exist; %= and **= error with a hint naming the rewrite. There is deliberately no ++/-- (the C-family increment): adjacent ++/-- are parse errors with a rewrite hint — before this, --i silently parsed as double negation -(-i) and returned i unchanged. Spaced forms keep their math meaning: -(-x) and - -x are still double negation. For a pure, value-returning step use succ(n) / pred(n) (§22).

Logical (auto-dispatched on operand type)

and    or    not    implies    iff    xor

&& and ∧ are exact aliases for and; || and ∨ are exact aliases for or. All spellings have the same precedence (and binds tighter than or) and evaluation rules: Boolean false on the left of and skips the right operand; Boolean true on the left of or skips it. A non-Boolean left operand retains the existing multivalued dispatch and evaluates the right operand. These aliases do not introduce operand-returning or truthiness-based logic; use andalso / orelse for the latter. A single & remains address-of, and | retains its structural roles.

println(1 < 2 && 2 < 3)             # true
println(true || false && false)     # true
println(false && (1 / 0 == 0))      # false; right operand is skipped
println(true || (1 / 0 == 0))       # true; right operand is skipped

When operands are multi-valued logic instances (Belnap, Intuit3, Łukasiewicz, Kleene), the operators dispatch automatically. See §9.

xor is exclusive or — true when exactly one side is true (iff is its negation, i.e. XNOR). The glyph ⊻ canonicalizes to xor (byte-identical, VM parity): true ⊻ true → false. Digraphs: `xor / `veebar.

andalso / orelse — the strictly two-valued pair

Both and and andalso short-circuit, so that is not what separates them. The difference is what happens when an operand is not a Boolean: and and or dispatch to the operand's logic, while andalso and orelse read its truthiness and hand back a plain Boolean.

om and true                    # → Ω        (dispatched: the SETL bottom propagates)
om andalso true                # → false    (om is falsy — collapsed to Boolean)

kleene("unknown") and true     # → ?ᵏ       (dispatched: Kleene's third value)
kleene("unknown") andalso true # → false

belnap("both") and true        # → ⊤⊥ᵇ      (dispatched: the glut survives)
belnap("both") andalso true    # → true     (a glut is truthy — collapsed)

Reach for andalso / orelse when a branch needs a yes-or-no answer whatever the operand's type — a guard, a filter predicate, an if test fed by data of unknown provenance. Reach for and / or when the third (or fourth) truth value is information you want to keep. Neither evaluates its right operand when the left already decides the result:

boom: func() [ raise("evaluated!") ]
false andalso boom()           # → false    (right operand untouched)
true orelse boom()             # → true

Logical negation — not / ¬ / ! (and what ~ is not)

Logical negation has three equivalent spellings:

not true               # → false     word form (Python / ML / SQL family)
¬ true                 # → false     math glyph
!true                  # → false     C / TypeScript / Go bang (prefix only)
!!flag                 # double negation
if !(x is String) then … else …
map(!, [true, false])  # → [false, true]   operator-as-value, same as `not`

Prefix ! is disambiguated from postfix factorial by position, the same way unary - is disambiguated from subtraction:

!true        # prefix  → logical not
5!           # postfix → factorial (120)
x: 6
x!           # → 720    (the name holds a number; factorial still)
!5!          # → false  ≡ !(5!)   (postfix binds tighter into the operand)
1 != 2       # digraph not-equal (not "prefix ! applied to =")
s !~ pat     # digraph regex non-match
sort!(xs)    # ident immediately followed by `!(` is ONE identifier —
             # the in-place twin of sort, not factorial of the sort builtin
splice!(xs, i)  # same glue; unbanged splice is quasiquote, so the array
                # mutator has to be a different identifier

The third reading of ! is a name, not an operator. sort!(xs) is the call form of sort! because the lexer glues ! onto an identifier only when the next character is (. Without the paren, x! stays factorial. sort! with no call is postfix on the sort function and yields the sort! builtin as a value. sort(xs) is a copy; sort!(xs) mutates the array in place and returns it. Tuples, lists, and sets stay on sort. The same pair exists for the other copy-named array functions: reverse/reverse!, unique/unique!, shuffle/shuffle!. Bang is a twin marker, not a decorator — push already mutates, so push!(t, x) is Undefined word, not an alias. Same for shift! / unshift!: the verbs are shift / unshift. splice! is the one mutator that keeps the bang, because unbanged splice is already quasiquote splicing (§5 Arrays).

Prefix ~x was retired (July 2026): it was an undocumented alias of not, and every C-lineage reader (C, Python, JS, Lua) reads ~5 as bitwise NOT (= -6), so the valid reading was a silent cross-language trap. ~5 is now a loud SyntaxError whose hint names the rewrites. Likewise a ~= b (Lua/MATLAB's not-equal) is a SyntaxError with a hint — write a != b (or a ≠ b). It will not become an alias: =~ is the regex-match operator, and mirror-image operators one transposition apart with unrelated meanings would turn typos into silent bugs.

Where ~ does appear: the defeasible markers (rule~, defines~, unify~, boundary~) and defeasible rule arrows (<~~, ~~>), and the Perl-borrowed regex pair (=~ match / !~ non-match). Bitwise NOT is bit_not(x) — bit_not(5) → -6, bit_not(0) → -1 — alongside band, bor, bxor, bshl, bshr.

nand / nor — the Sheffer stroke ⊼ and Peirce arrow ⊽

The two singly functionally-complete connectives (Post's theorem: each alone defines ¬, ∧, ∨ — the company here is Mathematica's n-ary Nand/Nor and APL's primitive ⍲/⍱). Two spellings each:

true ⊼ false               # → true    NAND glyph infix: ¬(p ∧ q)
false ⊽ false              # → true    NOR  glyph infix: ¬(p ∨ q)
nand(true, true)           # → false   prefix builtin
nand(a, b, c)              # n-ary: ¬(a ∧ b ∧ c), like Mathematica's Nand
nor([p1, p2, p3])          # collection fold — Wittgenstein's N-operator
                           #   (TLP 5.502): true iff EVERY proposition is false
(p ⊼ p) == (not p)         # → true    ¬ recovered from NAND alone

nand/nor are not keywords — a local nand: func(p, q) [...] binding shadows the builtin, so existing definitions keep working. The glyphs sit at xor/or precedence and are MVL-dispatched (each logic computes ¬∘∧ / ¬∘∨ with its own tables: om ⊼ true → Ω, belnap("both") ⊼ belnap("true") stays a glut). Digraphs: `nand / `barwedge, `nor / `barvee. Empty folds: nand([]) → false, nor([]) → true (the negated ∧/∨ identities). ⊼/⊽ chains are not associative with themselves — parenthesize, or use the n-ary builtin for ¬(a ∧ b ∧ …).

therefore / ∴ — the conclusion connective

p therefore q (glyph p ∴ q) draws a conclusion, marking it with [logical] grounding at full strength — distinct from the truth-functional implies. The glyph and the word are byte-identical:

p ∴ q                  # prints:  p →[logical] q  (strength: 1.00)
p therefore q          # identical to the glyph form

Type ∴ directly, with the backtick digraph `therefore / `qed / `thus, or via the REPL \therefore+Tab expansion.

Set operations

union    intersect    difference    symdiff    in       notin
subset   superset    subsetneq     supsetneq           # ⊆ ⊇ ⊂ ⊃ word twins
∪        ∩           \             △ ∆ ⊖       ∈  ∉    # glyph forms
⊆        ⊇           ⊂ ⊊           ⊃ ⊋                 # subset family (neq = proper/strict)

Conditional

if x > 0 then "positive" else "non-positive"

if x > 10 then [
    println("big")
] else if x > 0 then [
    println("small")
] else [
    println("non-positive")
]

Ternary cond ? a : b. The same expression as if cond then a else b — one AST, one evaluator path, --vm included. Right-associative; or / comparisons / arithmetic bind tighter. Only one branch runs.

sum(n) = n > 1 ? sum(n - 1) + n : n     # → 15 for sum(5)
fib(n) = n < 2 ? n : fib(n - 1) + fib(n - 2)
true ? 1 : 2                            # → 1
0 ? "T" : "F"                           # → "T"  (zero is truthy, as with `if`)

The ? of the ternary is an infix after a complete expression. It does not steal the predicate suffix: empty?([]) is still the identifier empty?. Prefix ?X is still a HiLog pattern variable. ?? / ??? / ?. still win the longer token.

Two compact spellings are not the ternary, and they are loud:

Write spaces around ? and :, as the examples above do. axioma/beginner refuses the ternary and points at if cond then a else b.

One-arm match. if pat = e then … else … (and the : spelling of =) desugars to match e with | pat => … | _ => …. The pattern must be a shape — a tuple, array, hash, constructor, pin, literal, or as/in pattern — not a bare lowercase name (if x = 5 then stays a SyntaxError; write if x == 5 then). Bindings live in the then-arm only.

if (1, x, 3) = pair then x else 0
if Circle(r) = s then r else 0
pair matches (1, _, 3)     # Boolean; bindings do not escape

matches is a soft keyword (matches: 5 still binds the name). --vm refuses match, if pat = e, and matches.

case is the noun form. case e | p => … is the same matcher as match e with, without a preposition: keyword, value, then | arms. switch is the ReasonML spelling of the same form (switch e | p => … ≡ case e | p => …; same CASE token). Reason's { } around the arms is not used — {} is the empty set ∅. case, switch, and cond are reserved words ($case / $switch / $cond to bind those spellings). case/strict / switch/strict is match/strict. case e of / with / do are SyntaxErrors. On match, the first | after with is optional: match e with p => … | _ => …. On case / switch, the first arm starts with | (the value is an expression). Postfix e match | p => … is the value-first spelling. Arm arrows are => or ->, the same pair as lambdas.

cond is chained if. cond | x > 0 => "pos" | else => "zero" desugars to if/else if and has --vm parity. Arms may wrap; the first | is optional. Catch-all arms: else, otherwise, _. No catch-all → none.

case pair | (1, x, 3) => x | _ => 0
case pair | (1, x, 3) -> x | _ -> 0
switch pair | (1, x, 3) => x | _ => 0
pair match | (1, x, 3) => x | _ => 0
cond | n > 0 => "pos" | n < 0 => "neg" | else => "zero"
cond
| n > 0 -> "pos"
| else  -> "zero"
area: function | Circle(r) => r * r | _ => 0

function | pat => … (also func | / fn | / fun |) is a one-argument match lambda. It requires the | so function f(x) stays a named func.

Open vs closed hashes. {name, age} matches if those keys are present; extra keys are allowed. {name, age} exactly requires those keys and forbids extras. {} exactly matches only dict(). {name, ..rest} binds leftover keys as a Dictionary.

match h with | {name, age} exactly => name | _ => none
match dict() with | {} exactly => "empty"
match h with | {name, ..rest} => rest

ADT leftover fields. P { x, ..rest } binds the unlisted constructor fields as a Dictionary. P { x, y } exactly requires every field of P to be listed. Unlisted fields are ignored when there is no .. / exactly.

data Point = P { x, y, z }
match pt with | P { x, ..rest } => rest.y
match pt with | P { x, y, z } exactly => x

exactly is a soft keyword (exactly: 5 still binds). {a, ..} exactly is a SyntaxError. | String(s) is not a type pattern.

Bracketed if-bodies are blocks, not arrays. Inside then [...] and else [...], a single-expression body returns the expression's value, not a single-element array — if cond then [42] else [99] returns 42, not [42]. Comma-separated [1, 2, 3] and empty [] still parse as array literals everywhere. The same contextual rule applies to match … | pat => [x] arms.

What counts as true

Only the bottoms are false. false and none are falsy; a typed multi-valued truth value is falsy when its logic does not designate it. Every other value is truthy — including 0, 0.0, "", [], {} and dict().

if 0 then "T" else "F"        # → "T"   — zero is a number, not a bottom
if "" then "T" else "F"       # → "T"
if [] then "T" else "F"       # → "T"
if {} then "T" else "F"       # → "T"   — ∅ is a set, not falsehood
if none then "T" else "F"     # → "F"
if ⊥ᵇ then "T" else "F"       # → "F"   — undesignated
if ⊤⊥ᵇ then "T" else "F"      # → "T"   — a glut IS designated
empty?([])                     # → true  — this is how you ask about emptiness

This is the SETL/Lisp policy rather than the C/Python/JavaScript one, and the reason is specific to Axioma. ∅ is a first-class mathematical object here, so a rule making the empty set false would leave set theory unable to state its own theorems: if (A intersect B) would silently mean "if they intersect" — a different proposition from the one written. Emptiness is a question you ask with empty?, which says what it means.

One consequence worth internalizing: truthiness is not a "did it work?" check. A caught Error is truthy — handle it with try/otherwise, not if. (none and om are both falsy, and a total read's absence is none, so you rarely need to if-test an error at all — but is_error(e) is the explicit test when you do.) The coalescing operators ?? / ??? are not a third option here: they fire on the bottoms, and an Error is a present value that passes straight through them — see §29.

Truthiness is a total function of the value, and if, while, filter, comprehension guards, the postfix if/unless modifiers and the logical operators all read the same one — in both runtimes. That is not a free-standing promise: before July 2026 the interpreter decided Booleans by comparing against its cached true/false objects, so a Boolean produced by, say, an FFI call was truthy whatever its value, and the same program could branch differently under --vm.

Loops

Three keywords. for is an alias of foreach, and loop of repeat, so there are three constructs and five spellings.

# ── while — condition-driven; the counter is YOURS and outlives the loop
n: 1
while n <= 5 [ println(n)  n = n + 1 ]
while (n < 10) [ n = n + 1 ]           # parens optional

# ── foreach ≡ for — source-driven, and the variable is SCOPED
foreach v in [10, 20, 30] [ println(v) ]
for     v in [10, 20, 30] [ println(v) ]      # same keyword

for _ in 1..3 [ println("hi") ]               # `_` DISCARDS: three trips,
                                              #   and the body cannot read it
for _i in 1..3 [ println(_i) ]                # `_i` binds — use it when the
                                              #   element is actually wanted

for v at i in xs [ println(i, v) ]            # 1-based index; three spellings
for v in xs with index i [ println(i, v) ]    #   of one idea
for i, v in xs.indexed   [ println(i, v) ]

foreach [x, y] in pairs [ println(x + y) ]    # destructuring; three spellings
foreach (x, y) in pairs [ println(x + y) ]
foreach  x, y  in pairs [ println(x + y) ]

for n in 1..3, m in 1..2 [ println(n * m) ]   # several generators: ONE loop over
for n in 1..3, m in 1..n                      #   the product, outer-major; the inner
  println(n, m)                               #   generator sees the outer variable;
end                                           #   break leaves the whole header

# ── repeat ≡ loop — source- OR condition-driven, one optional variable
repeat 5 [ println("hi") ]                    # count only, no variable
loop   5 [ println("hi") ]                    # same keyword
repeat i <- xs [ println(i) ]                 # bound variable over a source
repeat i <- 3  [ println(i) ]                 # a count IS a source — 1-based
repeat i 3     [ println(i) ]                 # older no-arrow spelling
repeat xs      [ println("tick") ]            # bare source, no variable

n: 0
repeat [n < 3] [ n = n + 1 ]                  # PRE-test block condition
n: 0
repeat [ n = n + 1 ] until n >= 3             # POST-test; body runs ≥ once
n: 0
repeat                                        # same post-test, end-form dual
  n: n + 1                                    #   (`loop … until … end` too)
until n >= 3
end

# `repeat` is an expression too, so it can sit on the right of a binding —
# same headers, and the bound value is a by-product only.
r: repeat i <- 1..10 by 3 [ println(i) ]

End-form blocks — if, while, for, loop, repeat, function, module … end

A second, keyword-terminated spelling of control-flow, function, and in-file module bodies (2026-08-27; module 2026-08-29; loop/repeat 2026-08-30). The rule: a header with no then and no [ whose next token sits on a later line opens a statement block that runs to a closing end. It lowers at parse time to exactly the AST the bracket form builds, so the two spellings cannot differ in meaning — pick per construct, and mix freely. module Name is the exception that needs a matching end to be nested: without one it is the file header, and a later function … end does not close it. Same-line empty while false end is the empty body.

grade: if score >= 90        # an if-EXPRESSION, so it can sit on
    "A"                      # the right of a binding
elseif score >= 80
    "B"
else
    "C"
end

n: 3
while n > 0                  # while … end — and an expression, so
    println(n)               # `y = while false end` binds none
    n: n - 1
end

loop 3                       # loop/repeat … end — dual of `[ … ]`
    n: n + 1
end

n: 0
repeat                       # post-test dual of `repeat [body] until cond`
    n: n + 1                 # later-line `until` closes the body; `end`
until n >= 3                 # closes the block. Same-line `p until q` in
end                          # the body stays the LTL operator.

for i in 1..9 by 2           # for … end — every header clause works:
    println(i * i)           # destructuring, `at i` / `with index i`, `by`
end

function countdown(n)        # function … end — all four spellings
    if n <= 0                # (func/fn/fun/function), the anonymous form,
        println("Blastoff!") # `:: ReturnType`, doc strings, `when`-guard
    else                     # clauses and pattern clauses all take it;
        println(n)           # `f(x) = expr` stays the equation short form
        countdown(n - 1)
    end
end

module Color                 # module … end — dual of `module Color [ … ]`
    name(c) = "c:" + c       # a file-header `module Name` with no matching
end                          # `end` stays a header (see §34)

The body is a plain statement sequence — newlines or ; separate statements, the last statement's value is the block's value, and an if … end with no true branch is none. elseif chains arms under ONE closing end; writing else if (two words) nests a fresh if instead, which carries its own terminator — exactly Julia's distinction, and why elseif exists. A parenthesized condition may span lines; an unparenthesized one ends with its line.

end and elseif are reserved words. A variable spelled end takes the guard ($end: 42), POP-11 word lists still read the bare word ([begin end] is ["begin", "end"]), and xs[end] is a SyntaxError whose hint points at xs[$] / xs[-1] / last(xs). Everything else is untouched: if c then …, then [ … ], while c [ … ], for x in xs [ … ], module M [ … ], a file-header module M with no matching end, and every bracket reading mean what they always meant, --fmt indents end-blocks without rewriting them, and source() prints the canonical bracket form.

Loop sources — the same set in for … in and repeat … <-:

for v in [1, 2, 3]           [ … ]   # array
for v in (1, 2, 3)           [ … ]   # tuple
for v in {3, 1, 2}           [ … ]   # set — ONE canonical order, numeric
for v in bag([3, 1, 2, 1])   [ … ]   # bag — a multiset, WITH multiplicity
for c in "abc"               [ … ]   # string, by character
for k in keys(d)             [ … ]   # dictionary keys, sorted
for k, v in items(d)         [ … ]   # dictionary pairs, destructured
for d in Day                 [ … ]   # enum, in declaration order
for x in SomeConcept         [ … ]   # a concept's instances

for i in 1..3                [ … ]   # range, inclusive
for i in 1..<3               [ … ]   # exclusive end
for i in 3..1                [ … ]   # descending, from the operands
for i in 1..10 by 3          [ … ]   # `by` = positive MAGNITUDE
for i in 10..1..-3           [ … ]   # `..n` = SIGNED step
for i in range(1, 10, 3)     [ … ]   # the call form — the same Range value
for i in 1.. [ if i > 3 then break ] # OPEN range — infinite, so break

for v in (n * n | n <- 1..)             [ … ]   # lazy comprehension
for i in iterate(func(v) [v * 2], 1)    [ … ]   # arbitrary-step stream
for i in take_while(func(x) [x < 20], iterate(func(v) [v * 2], 1)) [ … ]

break and continue work in every loop form, and return escapes the whole function from inside one. repeat-style loops without until are pre-test (the count or condition is checked before each pass); the until form is post-test — repeat [body] until cond or the end-form repeat … until cond end / loop … until cond end. A later-line until closes that body; same-line p until q remains the LTL operator.

Infinite loop / repeat, and break with a value. loop is a hard alias of repeat — every counted and source form already accepted both words. A one-block form with no count, no source, and no until is the infinite loop (Rust's loop { … }). break v is the value that loop yields; a bare break yields none. The value starts on the break's own line, the same rule return uses:

n: loop [
  break 123
]
# n is 123

k: 0
n: loop [
  k: k + 1
  if k == 3 then break k * 2
]
# n is 6 — `if c then break v` is the same sugar as `then [break v]`

while is an expression too: y = while false end binds none, and r: while true [ break 2 ] binds 2. A completing while (condition goes false, no break) yields none; break v is how it yields a value. The end-form dual of loop [ … ] is loop / repeat with a newline then body then end. --vm agrees on the no-break forms and refuses the infinite form by name until break compiles.

Loop labels. name: already binds the loop's result (n: loop [ break 123 ]). The loop's own name is a Word — 'outer — so Java/Go outer: for and Rust 'outer: loop have an Axioma twin that does not steal the binder or break v:

found: 'search: loop [
  for row in [[1, 2], [10, 30]] [
    for cell in row [
      if cell > 25 then break 'search cell
    ]
  ]
]
# found is 30

'rows: for n in 1..3 [
  for m in 1..3 [
    if m == 2 then continue 'rows
  ]
]

'name: before loop / repeat / while / for / foreach names that loop. break 'name / continue 'name target it; break 'name v still yields v. Unlabeled break leaves only the innermost loop. A combined header takes one name for the whole product ('prod: for n in 1..3, m in 1..3 [ break 'prod ]). Unknown and duplicate labels error. To yield a Word, parenthesize it: break ('ok). --vm refuses break (labeled or not).

A loop scopes what the loop binds. for/foreach and every source form of repeat bind the loop variable themselves, so it does not outlive the loop. The condition-driven forms — while, repeat [cond] […], repeat […] until cond, infinite loop [ … ] — bind nothing: the counter is yours, lives in your scope, and survives. A body still reads and updates enclosing names normally, so accumulator loops are unaffected — that is a body assignment, which is find-or-update. The loop variable itself is a binder, so one that matches a pre-existing outer name shadows it rather than writing it (see §Scoping & shadowing).

A lazy stream is what a lazy comprehension, an open range, and iterate(f, x) produce (@g → "Generator"). The loop pulls one element at a time, so an unbounded source is fine as long as the body breaks — or as long as take_while bounds it, which stops at the first failing element. iterate(f, x) without a count is how you get a counter whose step is an arbitrary function while keeping it scoped to the loop: for i in 1..n steps by a constant, and while takes any step but leaves its counter bound after the loop ends.

A stream is walked once. Stopping partway and looping again resumes where you left off; walking a stream that has already been drained (by force, by first, or by a loop that ran to the end) raises a catchable error rather than silently running zero iterations.

A complete, executable inventory of every form above — each one asserted, so it cannot rot — lives in tests/axioma/showcase/loops.ax.

Statement branches — if c then break, if c then a: 0. A branch may be a bare statement: break, continue, return, or a binding. Each is sugar for the block form the brackets already spelled (then [break]), built by the same parse, so the two spellings are the same AST and cannot drift. Both arms take all of them:

while true [
  if done then break              # ≡ if done then [break]
  if skip then continue
  if x < 0 then "note it" else break     # the else arm too
]

if a < 0 then a: 0                # bindings too — `=` spells it as well
if a < 0 then a = 0 else a: 100   # …in either arm
if hit then tally[k] += 1         # every assignment target the brackets
if hit then rec.total: 0          #   accept: multi-assign, index, property,
m, n: 1, 2                        #   compound
if swap? then m, n: n, m

Two things to know. A binding branch scopes a fresh name to the block, exactly as if c then [z: 1] always did — so if c then z: 1 on a new z binds something that vanishes at the branch's end, while an existing name is found-and-updated (the common case). And a postfix guard is return-only: return -1 if x < 0 works, break if x < 0 does not (write if x < 0 then break).

Indexed iteration — at i, with index i, .indexed

When a loop needs the element and its position, three equivalent surfaces attach a 1-based counter (element-first, so the common element-only loop stays the short one). for and foreach are one keyword — every form below works with either spelling:

fruits: ["fig", "plum", "lime"]

for f at i in fruits [ println("${i}. ${f}") ]       # at-clause
for f in fruits with index i [ println(i) ]          # with-index clause
for i, f in fruits.indexed [ println(f) ]            # destructure the pairs
for i, f in enumerate(fruits) [ println(i) ]         # builtin spelling

pairs: [(10, "x"), (20, "y")]
for v, tag at i in pairs [ … ]     # composes with destructure: v, tag
                                   #   from the element, i from the counter

for n at i in 2..100 by 2 [        # any iterable — ranges included; break
  if i == 3 then [break]           #   and continue see the same i
]

The counter is always 1-based and counts iterations (for a String it counts runes; for a Set it follows the canonical sorted order — the same order .indexed and enumerate report). at and index are soft keywords, recognized only in these clause positions — variables named at or index, and loops like for at in xs, keep working. Writing both clauses at once (for x at i in xs with index j) is a pointed error: pick one.

An open-ended range makes the classic search-until loop:

s: 0
foreach k in 1.. [                 # 1, 2, 3, … forever — until break
  s = s + k
  if s > 20 then [break]
]
s                                  # → 21

Like all loops, the indexed forms are evaluator-only under --vm (the pre-existing boundary). Tests: tests/axioma/control/test_indexed_iteration.ax, tests/axioma/properties/test_indexed_accessor.ax.

Operator precedence (high → low)

This table is for ordinary expression position. Parentheses explicitly group an expression. “Left” means (a op b) op c; “right” means a op (b op c). These are parsing rules, not mathematical associativity or a side-effect schedule. The Textbook's Appendix A operator reference expands the operator families, specialist forms and worked examples.

Grouping examples. 2 ^ 3 ^ 2 = 2 ^ (3 ^ 2) = 512; (2 ^ 3) ^ 2 = 64, so exponentiation is not mathematically associative. -2 ^ 2 = -(2 ^ 2) = -4, while (-2) ^ 2 = 4. not a == b is (not a) == b; use not (a == b) to negate the comparison. 1 cons 2 cons list() is cons(1, cons(2, list())). 1 => 2 => 3 is pair(1, pair(2, 3)); lambda heads and match/cond arms claim arrows before the infix pair parser. Unicode → is implication, not a pair.

Calls and composition. f(x)[i].field groups as ((f(x))[i]).field. 3 `f` 4 * 2 is f(3, 4) * 2. f ∘ g(x) is f ∘ (g(x)); write (f ∘ g)(x) to apply the composition. x |> f(a) inserts the value as the last argument, f(a, x); _ selects a position. <</>> compose functions; bit shifting uses bshl/bshr. See Forward pipe and Function composition below.

Special chains. a < b <= c rewrites to (a < b) and (b <= c); the shared middle expression can execute twice, so bind it once when necessary. ==/!= chains do not get this rewrite. 1..5..2 is start/end/signed-step, not a nested binary range. a ? b : c ? d : e is a ? b : (c ? d : e); the yes-branch accepts a whole expression up to its matching :, while the no-branch accepts another ternary/fallback but stops before a following pipe. Parenthesize mixes.

Two-word fallback exception. or else has the error trigger of otherwise, but currently enters at disjunction priority and reads its right side down to fallback priority. Thus a ?? b or else c is a ?? (b otherwise c), unlike a ?? b otherwise c, which is (a ?? b) otherwise c. Repeated or else nests right. Use (a ?? b) or else c when the whole coalescing expression is to be protected. It is not a precedence-identical replacement for otherwise.

Evaluation is a separate rule. Boolean false and rhs / true or rhs (and their glyph/ASCII aliases) skip rhs; multi-valued left operands may need both sides. andalso/orelse use truthiness and return a Boolean. otherwise selects its right operand for an Error, ?? for none, ??? for none or om. Conditionals run only the selected branch. Right-grouping power does not mean its rightmost operand runs first. The evaluator's ordinary pipe insertion can evaluate explicit call arguments before the appended input expression; bind side-effectful inputs first when order matters. Broadcasting has its own fusion/order rules. Precedence alone neither adds nor removes evaluations.

Specialist entry priorities, above postfix factorial, high to low: Manchester some/only; ontology/definition; analogy; argument; binary temporal; deontic; epistemic; causal/aspect. Same-band binary forms generally group left, but knows/believes/doubts and must/may/must_not/should take a whole expression on the right; causes/caused by take a right side tighter than equality, including another causation. R some C ⊓ D is (R some C) ⊓ D, not R some (C ⊓ D). Prefix modal/temporal forms use the ordinary prefix operand boundary instead. See Appendix A's complete specialist table and §10 for operand semantics.

Grammar boundaries. Rule arrows parse whole heads/bodies; show and graph operations use clause grammar even though entered at equality priority. Assignments, ::, type/pattern syntax, statement messages, comprehensions, commas and semicolons are not extra ordinary binary rows. A semicolon ends an ordinary expression. Newline and delimiter rules can stop an expression before precedence applies. ought/permitted/forbidden have no ordinary infix handler; satisfies, with_probability, infix probably/typically, denotes, normally, by_default have no active ordinary infix priority. Their presence in parser metadata does not make them supported expression operators.

Negative integer exponents stay exact. int ^ -n returns the exact Rational 1/int^n (an Integer when integral), the same way / keeps 1/2 exact — so 2 ^ -3 → 1/8, 2 ^ -1 → 1/2, 1 ^ -5 → 1. (0 ^ -3 is a division-by-zero error.) Use a Float base/exponent or pow(...) if you want a Float result instead.

A fractional exponent is a root, and exactness follows the operands. A rational exponent p/q takes the q-th root. When that root is exact you get an exact answer, at arbitrary precision — no detour through float64:

4 ^ (1/2)              # 2          — an Integer, not 2.0
(8/27) ^ (1/3)         # 2/3        — numerator and denominator each rooted
27 ^ (2/3)             # 9
4 ^ (-1/2)             # 1/2        — negative exponent inverts, as ever
(2^100) ^ (1/2)        # 1125899906842624   (= 2^50, exactly)

When no exact root exists, ^ still answers — as a Float, so it is never a dead end:

2 ^ (1/2)              # 1.4142135623731     — √2 is irrational

This is the same exactness rule + and * follow: two exact operands can give an exact result; one inexact operand makes the result inexact. So the exponent's spelling decides the type, and the two spellings still agree on the value:

4 ^ (1/2)              # 2       Integer  — exact exponent
4 ^ 0.5                # 2       Float    — inexact exponent
4 ^ (1/2) == 4 ^ 0.5   # true             — same number either way

A negative base has no real power at a non-integer exponent. It raises a catchable error rather than producing NaN:

(-1) ^ 0.5     # ERROR: negative base has no real power at a non-integer exponent: -1^0.5
(-2) ^ 3       # -8    — an INTEGER exponent is fine, whatever the sign
(-2.0) ^ 2.0   # 4

The rule keys on the exponent, not on the sign of the base alone. Erroring is deliberate: a NaN would flow silently through every later computation, and the neighbouring spelling sqrt(-1) has always errored — two spellings of one question should not disagree about whether it has an answer.

Floats keep IEEE semantics where the two systems differ: 0.0 ^ -1.0 is Inf, while the exact 0 ^ -1 is a division-by-zero error. The exact tower answers with mathematics; Float answers with IEEE.

The complex plane is the explicit opt-in. sqrt(-1) and (-1) ^ 0.5 stay real-domain errors, and both name the way through:

sqrt(complex(-1, 0))     # i
complex(-1, 0) ^ 0.5     # i   — the same value; the two spellings agree

Complex sits at the top of the numeric tower: every other numeric type embeds into it, so mixed arithmetic just works, and ^ is exact at integer exponents.

im                       # i            — the unit, shadowable like pi
1 + im                   # 1 + i
(1 + im)^2               # 2i
im^2                     # -1           — exactly, not -1 + 1.2e-16i
2 * im                   # 2i           — not 2im (juxtaposition is diagnosed)
complex(3, 4) + 1/2      # 3.5 + 4i     — Rational embeds
complex(3, 4) + byte(2)  # 5 + 4i       — so does Byte
conjugate(complex(3, 4)) # 3 - 4i
-complex(1, 2)           # -1 - 2i

sqrt, exp, log, sin and cos accept a Complex alongside the reals. The embedding runs through float64, so exactness stops at the complex boundary — exact?(complex(1, 0)) is false, and complex(0, 1) + 1/3 is inexact. Keeping exactness inside the plane would need exact Gaussian rationals, which Axioma does not have.

Function broadcasting

A dotted call applies an ordinary runtime function element by element:

f(x) = 2 * x
f.([1, 2, 3])                         # → [2, 4, 6]
broadcast(f, [1, 2, 3])               # → [2, 4, 6]
add(a, b) = a + b
add.([1, 2, 3], 10)                  # → [11, 12, 13]
add.([1, 2, 3], [10])                # → [11, 12, 13]
length.([[1, 2], [3]])                # → [2, 1]
add.(matrix([[1, 2]]), matrix([[10], [20]]))  # → 2×2 Matrix

Array, Tuple, List and finite Range inputs have one axis. Matrix and Tensor keep their explicit axes. Other ordinary values, including String and Dictionary, are scalar arguments. Nested Arrays remain elements: they do not create additional axes. With only scalars the function is called once; with an empty output it is not called. Unbounded/lazy iterators must be bounded and collected before broadcasting.

Axes align from the right. Equal sizes match; a singleton axis expands to the other size. A vector therefore matches the last Matrix/Tensor axis. Incompatible shapes error before callbacks. The output is Array for ordinary sequences, Matrix if a Matrix participates, and Tensor if a Tensor participates. Matrix cells retain exact numeric types; nonnumeric Matrix results refuse (use collect(m) as input for an unrestricted Array result). Tensor output keeps its Float storage and refuses silent loss of exact numeric precision.

The callable and arguments evaluate once, then calls run in row-major order with ordinary type, contract and effect checks. Named arguments are scalar options shared across calls. To use slash refinements, put the refined call inside a normal function and broadcast that function. Failures stop the walk without retry or rollback. Input shapes are captured; inputs are not repeated into temporary arrays. Eager output is limited to one million elements.

Nested dotted calls and supported dotted arithmetic use loop fusion:

square(x) = x * x
increment(x) = x + 1
increment.(square.([1, 2, 3]))        # → [2, 5, 10], one output walk
increment.([1, 2, 3] .^ 2)           # → [2, 5, 10]

Fusion builds a plan of the nested operations and creates only the final result collection. Leaf expressions and function expressions evaluate once; for each output cell, nested functions execute in expression order. Functions with side effects participate too: nested calls interleave per cell rather than completing every inner call before any outer call. A singleton or nullary inner operation can therefore execute repeatedly across the output shape. Empty outputs execute no scalar callbacks. Shape errors are checked before scalar callbacks; a callback error stops the walk without retry.

Ordinary function calls, including broadcast(...), break fusion. Bind an intermediate result when separate evaluation is intended. Ordinary pipe stages are also boundaries; nested dotted expressions within a stage can fuse without changing pipe argument insertion.

Only the final container is constructed: intermediate scalar values keep their types, without the promotions that a separately materialized Matrix or Tensor could introduce. Final Matrix/Tensor conversion remains strict. Existing dotted arithmetic retains its own numeric and shape rules; fusion does not grant Array operators singleton expansion or Matrix/Array mixing. Dotted calls and broadcast are interpreter features; the VM explicitly refuses them, including builtin aliases and higher-order use. Connected dotted arithmetic requiring fusion also refuses in the VM; standalone dotted arithmetic and explicit materialization boundaries retain their support.

Forward pipe |>

The forward pipe threads a value into a function call, so a chain of transformations reads left-to-right in the order it runs — instead of the inside-out nest that map/filter/reduce otherwise force:

xs |> map(g) |> filter(p) |> reduce(f, 0)     # ≡ reduce(f, 0, filter(p, map(g, xs)))
21 |> double                                    # bare name → double(21) → 42

The piped value is appended as the last argument — Axioma's higher-order functions are function-first / collection-last (map(fn, coll), filter(pred, coll), reduce(fn, init, coll)), so the everyday chain just works. For the collection-first builtins (str_join, first, push), an explicit _ hole says where the value lands:

["a", "b", "c"] |> str_join(_, "-")            # ≡ str_join(["a","b","c"], "-") → "a-b-c"
myset           |> first(_, 3)                  # ≡ first(myset, 3)

|> has the loosest precedence (so 20 + 1 |> double is (20+1) |> double), is left-associative, and composes in expression position — inside function bodies, if conditions, bindings, and across multiple lines (a leading |> continues the pipeline):

result: data
  |> filter(func(r)[r.valid])
  |> map(transform)

A natural fit for Axioma is post-processing a relational query or rendering with the *form family:

{Y | Y <- ancestor("tom", Y)} |> sort |> first(_, 3)
txns |> filter(func(t)[t.amount > 50]) |> tableform |> println

The same placement rule applies to broadcasting:

add(a, b) = a + b
[1, 2, 3] |> add.(10) |> sum           # → 36
[1, 2, 3] |> add.(10, _) |> sum        # → 36
[1, 2, 3].map(x -> 2 * x) |> sum      # → 12

The pipe passes the whole value; the dotted call then broadcasts it. Only the first bare _ among top-level positional arguments is replaced. There is no recursive hole search or implicit lambda: xs |> _.length() and xs |> map(_ * 2) are not receiver or lambda shorthand. Use xs |> length, xs.length(), or an explicit function argument. The pipe's VM support does not make unsupported broadcast/method operations VM-compatible.

Error-propagating pipe |?>

|?> is the safe sibling of |>: it short-circuits on a failed, absent, or undetermined value. If a stage yields an Error (e.g. from try(...) / error(...)), none, or om, the remaining stages are skipped and that value becomes the result — railway-oriented error flow without nested ifs:

input |?> parse |?> validate |?> compute   # stops at the first failing stage
5 |?> double |?> double                      # → 20   (nothing fails)
5 |?> boom   |?> double                      # → the boom Error  (double is skipped)
5 |?> nada   |?> double                      # → none            (double is skipped)
0 |?> double                                  # → 0   (0 is a valid value, not a failure)

It shares everything else with |> — last-argument insertion, the _ hole, left-associativity, dotted callables — and differs only in the short-circuit. A plain value (even a falsy one like 0 or "") is not a failure and flows through; only Error / none / om stop the pipeline. Use |> when every stage always succeeds, |?> when a stage may fail and you want the failure to propagate.

|?> propagates a failure; otherwise / ?? / ??? replace one, and ?. guards a single member read. They are one family seen from opposite ends — §29 has the table of which form fires on which bottom, and the two compose well: pipe the failure along, then coalesce it at the end. One practical difference: |?> is the only member with full --vm parity. The other four are evaluator-only and refuse at compile time, whereas |?> compiles and runs byte-identically in both runtimes.

7. Set Theory & Comprehensions

Comprehensions

{x * 2 | x <- {1, 2, 3, 4, 5}}                     # {2, 4, 6, 8, 10}
{x | x <- range(1, 10), x mod 2 == 0}              # {2, 4, 6, 8, 10}
{(x, y) | x <- {1, 2}, y <- {3, 4}}                # {(1,3), (1,4), (2,3), (2,4)}

[1 | _ <- [7, 8, 9]]                               # [1, 1, 1] — `_` DISCARDS:
                                                   #   walks, but binds nothing
[a | (a, _) <- [(1, 2), (3, 4)]]                   # [1, 3] — a bound, slot dropped

The generator clause is target <- source — or, in the set-builder slot described below, target in source / target ∈ source.

A _ target is a discard, exactly as in a for loop or a match arm: the generator still yields one row per element, but nothing can read _. Name the target (or use _i) when the element is wanted.

British/ISO colon separator

Math texts write set-builder two ways: {x | P(x)} (American) or {x : P(x)} (British/ISO). Set comprehensions accept both separators — the two forms are identical down to the AST:

{x : x <- range(1, 10), x mod 2 == 0}              # same set as the pipe form
{2 * k : k <- range(1, 5)}                         # {2, 4, 6, 8, 10}  — the {2k : k = 1..5} style
{(x, y) : x <- {1, 2}, y <- {3, 4}}                # multi-generator works too

Hash literals are unaffected: {k: v, ...} stays a hash — the colon is read as a comprehension separator only when a generator clause (target <- source, or a gated target ∈ source) provably follows it. The colon form applies to set comprehensions only; dict comprehensions keep | (their head already uses :), and list comprehensions keep | (inside [...] a colon means a block binding).

ISO membership generators — {x : x ∈ U, P(x)}

Real ISO/British texts put membership in the binder slot. in / ∈ is accepted as a generator alias for <- under one rule: the clause x in S is a generator iff x is not already bound in the comprehension and occurs in the head; otherwise it keeps its membership-filter meaning. This makes the textbook form executable verbatim while leaving every membership test untouched:

{x : x ∈ {1, 2, 3, 4}, x > 1}                      # {2, 3, 4}  — full ISO form
{x | x in range(1, 10), x mod 2 == 0}              # word form, pipe separator
[x * 2 | x in [1, 2, 3]]                           # lists too → [2, 4, 6]
{(x, y) : x ∈ {1, 2}, y ∈ {8, 9}}                  # multi-generator Cartesian
{a + b : (a, b) ∈ pairs}                           # tuple-destructure target

# Membership FILTERS keep their meaning (the gate):
{x | x <- s, x in t}                               # x bound → filter (s ∩ t idiom)
{c | c <- cs, g in c.allies}                       # g is outer/global → filter
{x | x <- s, x ∉ t}                                # ∉ never converts
[x for x in xs if x in t]                          # Python if-clause: always a filter

Works in all four comprehension flavors (set / list / dict / lazy), with both spellings (in, ∈) and both separators (|, :). One reinterpretation to know about: the hash {x: x in s} — the same name as key and membership subject — now reads as a comprehension; write {x: (x in s)} (parenthesized value) or quote the key to keep the hash.

Relational comprehensions (Prolog-style)

{X | X <- parent(X, _)}                            # All parents
{(X, Y) | parent(X, Y)}                            # All parent-child pairs
{X | X <- parent(X, _), age(X, A), A >= 18}        # With filter

Concept-extent comprehensions

When the iterable is a bare concept name, comprehension iterates the concept's auto-maintained Instances map:

usa: a Country {}
china: a Country {}
{X | X <- Country}                                 # All countries

Tag-filter comprehensions

Filter relational-source comprehensions by epistemic grounding tag — in the set, list, dict, multi-variable, and multi-generator forms:

{X @theorem    | X <- derived_relation(X, _)}          # Theorems only
{X @conjecture | X <- flies(X)}                        # Defeasibly derived
[X @axiom      | X <- parent(X, _)]                    # list form
{X: 1 @datum   | X <- parent(X, _)}                    # dict form
{(X, Y) @axiom | rel(X, Y)}                            # multi-variable form
{(X, Y, n) @axiom | (X, Y) <- rel(X, Y), n <- [1, 2]}  # multi-generator

Accepts @axiom, @postulate, @theorem, @conjecture, @hypothesis, @datum, @canceled, @all, @* (@standalone is a legacy alias of @datum). The tag filters facts drawn from relational sources by their stored grounding. On a non-relational source — a plain array/set, a concept extent (X is Country), or a chain query (rel1(...) and rel2(...)) — the tag is inert: those elements carry no per-fact grounding to filter on.

Dict comprehensions

Produce a hash by emitting a key/value pair per iteration. Pipe form and pipe-less form are both supported:

xs: [1, 2, 3, 4, 5]

{x: x * x | x <- xs}                               # {1:1, 2:4, 3:9, 4:16, 5:25}
{x: x * x | x <- xs, x > 2}                        # {3:9, 4:16, 5:25}
{x: x * x for x in xs if x > 2}                    # pipe-less form, same result

Walrus bindings (compute once, reuse)

Bind a name mid-clause to avoid recomputing. The canonical form is :, the same operator used for ordinary value binding:

{y | x <- xs, y: f(x), y > 0}                      # bind y once, filter on it

Bindings are iteration-local — they do not leak out of the comprehension (unlike Python's walrus, which escapes into the enclosing function scope).

A comprehension binding clause is written y: expr; there is no y := expr or let y = expr form.

Multi-filter folding

Multiple bare-expression filters in one comprehension are folded with and:

{x | x <- 1..10, x > 3, x < 8, x % 2 == 1}         # {5, 7}

Keyword aliases & the pipe-less form

Axioma also accepts for x in iter and if cond as aliases for <- and the bare filter inside the standard pipe form, plus a fully pipe-less form for all three comprehension flavors (so a comprehension copied from Python pastes in unchanged):

{x * 2 | for x in xs, if x > 2}                    # keywords inside pipe form
[x * 2 for x in xs if x > 2]                       # pipe-less list comp
{x * 2 for x in xs if x > 2}                       # pipe-less set comp
{x: x * x for x in xs if x > 2}                    # pipe-less dict comp

The first generator may use either for x in iter or x <- iter. Subsequent clauses are equally flexible.

Tests: tests/axioma/comprehensions/test_python_superset.ax

Deferred values — lazy, force, memoize

lazy <expr> defers a computation and hands you the thunk itself — a first-class value whose successful result is cached when you force it. A failed attempt may retry; recursive forcing reports cyclic demand.

t: lazy (6 * 7)        # nothing has run yet
force(t)               # → 42   computed now…
force(t)               # → 42   …and memoized: not recomputed

This is the expression twin of the declare binding:

The difference is what you can do with it. A declare binding has already forced itself by the time it reaches an argument; a lazy value can be passed, stored, and returned still unevaluated — so a computation that is never needed never runs at all:

pick: func(flag, thunk) [if flag then force(thunk) else "skipped"]
pick(false, lazy slow())    # → "skipped" — slow() never ran

Thunks are ordinary values, so they compose:

ts: [lazy (1 + 1), lazy (2 + 2)]
map(force, ts)              # → [2, 4]

force covers the whole family and is idempotent: a thunk computes (once), a generator drains, and anything else comes back unchanged — R7RS Scheme's rule, which is what makes force safe to map over mixed data.

memoize(f) is the per-call companion. Where lazy defers one expression, memoize caches every call, keyed by argument value:

fast: memoize(slow)
fast(9)     # computes
fast(9)     # cached — slow() is not called again

lazy is a soft keyword — it is still usable as an ordinary name (lazy: 5, f(lazy)). It binds at prefix precedence, so lazy 1 + 2 is (lazy 1) + 2; parenthesize to defer the whole expression. lazy and declare are both evaluator-only — rejected at compile time under --vm.

Lazy generator expressions

Comprehensions wrapped in parens produce a lazy Generator instead of materializing. The source is pulled one element at a time on demand.

g: (x * 2 | x <- [1, 2, 3, 4, 5])      # Axioma pipe form
g: (x * 2 for x in [1, 2, 3, 4, 5])    # pipe-less form
g: (x + 1 | x <- xs, x > 15)           # with filter
g: (x + 1 for x in xs if x > 15)       # Python with filter

Driver builtins:

Prefer first(gen, n) — it's the same "first n" verb you already use for arrays and infinite sets. The gen_* prefix exists only because take is a reserved keyword (natural-language selective import) and drop is the Stack op.

g: (x | x <- [1, 2, 3, 4, 5])
first(g, 3)           # [1, 2, 3]   (same as gen_take(3, g))
force(g)              # [4, 5]      — remainder after partial take

Phase 2b — full multi-clause surface. Lazy comprehensions now accept the same clause vocabulary as eager list/set/dict comprehensions:

# Multi-generator (Cartesian, streamed — inner is re-eval'd each outer step)
pairs: (x * y | x <- [1, 2, 3], y <- [10, 20])
py_pairs: (x + y for x in [1, 2] for y in [100, 200])

# Walrus binding (`:` — the canonical form)
g: (s | x <- xs, s: x * x)

# Tuple destructure in first OR subsequent generators
dest: (n + 1 | (n, _label) <- tagged)
lab: (s + ":" + name | (s, name) <- pairs)

# Concept-extent source — bare concept name OR is form
gdps: (c.gdp | c <- Country)
gdps2: (c.gdp | c is Country)

# Relational predicate source — a fact-store query as the iterable
kids: (c | c <- parent("John", c))           # single generator
gkids: ((p, g) | p <- parent("John", p), g <- parent(p, g))  # chained

Streaming semantics. Multi-generator lazy form materializes inner sources once per outer combination (so the inner can reference outer-bound names — same as the eager path). The outermost source can still stream from a true Generator or InfiniteSet. Inner positions cannot use InfiniteSet — they'd re-materialize infinitely on each outer advance. gen_take(N, ...) bounds total pulls, naturally cutting the outer loop short when N is reached.

Relational sources. When a generator's iterable is a relational predicate call (x <- parent(x, _)), the lazy paths fall back to the relational machinery — eager evaluation of such a call fails, so this is detected by probe. The relation extent is bounded, so it is resolved once per entry; downstream pulls stay lazy. Works in single-generator, chained, inner, and filtered positions. The same bridge serves list and dict comprehensions (July 2026), and a bare relation name is a valid source in every flavor ([x | x <- node], {x: y | (x, y) <- parent}). Because a relation extent is a set with no intrinsic order, materialization into an ordered collection is deterministic by construction: elements come out sorted (lexicographically by display form), so [Y | Y <- parent("John", Y)] and force((Y | Y <- parent("John", Y))) return the same array on every run — no sort(...) wrapper needed.

Limitations. OrderBy and Having clauses are accepted by the parser inside lazy form but silently discarded — both are intrinsically eager (sorting requires full materialization). For an ordered lazy stream, force(gen) then sort, or sort eagerly first.

Tests: tests/axioma/comprehensions/test_lazy_generators.ax (Phase 2a — single gen), tests/axioma/comprehensions/test_lazy_generators_phase2b.ax (Phase 2b — multi-clause), tests/axioma/comprehensions/test_lazy_relational_source.ax (relational sources)

ORDER BY clause

List comprehensions accept an orderby clause that sorts the result. Sets and dicts ignore orderby (they're unordered by nature). Direction defaults to asc; add desc to reverse:

[x | x <- xs, orderby x]                    # asc by default
[x | x <- xs, orderby x desc]               # descending
[p.name | p <- people, orderby p.age]       # sort by computed key
[x for x in xs orderby x desc]              # pipe-less form works too

The sort key is evaluated in the iteration environment (where the loop variable refers to the source element), so referring to fields of the source element works as expected.

Aggregation: group_by, items, keys, values

Four builtins fill the SQL-style aggregation gap. group_by(fn, coll) partitions a collection into a hash; items(hash) exposes it as (key, value) pairs; keys/values return the parts individually. All three enumerators walk the hash in sorted key order — the same canonical order println(h) shows — so repeated calls (and keys/values/items against each other) always agree.

orders: [
  {country: "US", amount: 100},
  {country: "UK", amount: 50},
  {country: "US", amount: 200},
]
by_country: group_by(func(o) [o.country], orders)
# {"US": [{...}, {...}], "UK": [{...}]}

# Iterate the hash with tuple destructure + ORDER BY:
pairs: items(by_country)
counts: [(p[1], len(p[2])) | p <- pairs]
sorted: [pair | pair <- counts, orderby pair[2] desc]
# [("US", 2), ("UK", 1)]

Tuple destructuring in <-

In any generator (first or subsequent), the iteration target can be a tuple pattern instead of a single variable — and since July 2026 the parentheses are optional, matching the loop form (for i, e in …):

pairs: [(1, "a"), (2, "b"), (3, "c")]

# First-generator tuple destructure (canonical form)
[n + len(s) | (n, s) <- pairs]            # list comp
{n: s     | (n, s) <- pairs}              # dict comp
{n * 2    | (n, s) <- pairs}              # set comp

# BARE destructure — same meaning, no parens (all flavors, any clause)
[n + len(s) | n, s <- pairs]
xs: ["p", "q", "r"]
{e | i, e <- xs.indexed, i > 1}           # → {"q", "r"} — the .indexed idiom
[e for i, e in enumerate(xs) if i > 1]    # pipe-less Python spelling too

# Idiomatic with items() over a hash
by_country: group_by(func(o) [o.country], orders)
{k: len(g) | (k, g) <- items(by_country)}

Source elements must be Tuples or Arrays of the matching arity. Mismatched arity is a hard error. The bare form commits only when a run of two-plus names closes with <-/in, so a bare-identifier filter ({x | x <- xs, flag, x > 1}) keeps its filter meaning.

A call as the source works like any other iterable — {(i, e) | (i, e) <- enumerate(xs)} binds by the pattern. (Before July 2026 this specific shape — tuple head + tuple pattern + a call source — was silently misread as a relation query over a relation named enumerate and returned {}; genuine relation sources like {(X, Y) | (X, Y) <- edge(X, Y)} still take the relational path.) Tests: tests/axioma/comprehensions/test_bare_destructure.ax.

Hash destructure in <-

First-generator targets can also be a hash pattern that binds named fields directly. Two surface forms — implicit binding (var name = key name) and explicit rename (key: var):

people: [
  {name: "Alice", age: 30, dept: "Eng"},
  {name: "Bob",   age: 25, dept: "Sales"},
  {name: "Carol", age: 35, dept: "Eng"}
]

# Implicit binding
[name | {name, age} <- people, age >= 30]
# → ["Alice", "Carol"]

# Explicit rename
[(n, a) | {name: n, age: a} <- people]
# → [("Alice", 30), ("Bob", 25), ("Carol", 35)]

# Mixed implicit + rename in same pattern
[name | {name, age: a, dept} <- people, a > 27 and dept == "Eng"]

# pipe-less form
[name for {name, age} in people if age > 27]
{n for {name: n} in people}
{name: age for {name, age} in people}

# Lazy form
g: (name | {name, age} <- people, age > 25)
force(g)   # → ["Alice", "Carol"]

# Combined with orderby + limit
[name | {name, age} <- people, orderby age desc, limit 2]
# → ["Carol", "Alice"]

Skip-on-missing-key. When a pattern key is absent from a source hash, that row is silently dropped — destructure acts as filter+extract in one step:

mixed: [{name: "Alice", age: 30}, {name: "Bob"}, {name: "Carol", age: 35}]
[n | {name: n, age: a} <- mixed]
# → ["Alice", "Carol"]   (Bob has no `age` key — dropped)

Wrong-type elements (anything not a Dictionary hash) surface a runtime error.

Scope. Hash destructure is currently supported only in the first generator position. Subsequent generators (after a , in pipe form) use the single-var or tuple-pattern forms — {...} in that position would be ambiguous with set/hash filter expressions.

Tests: tests/axioma/comprehensions/test_hash_destructure.ax

Multi-column ORDER BY

orderby accepts a comma-separated list of sort keys, each with its own direction. Sort is lexicographic across columns:

[p.name | p <- people, orderby p.dept, p.age desc]
# Sorts by dept ascending; within each dept, by age descending.

HAVING clause — terminal filter

having EXPR is a terminal filter that runs in the iteration environment (so it can reference the loop variable). Distinct from , EXPR filters only in position and intent — HAVING reads as "row filter after aggregate computation" by convention:

[o.amount | o <- orders, having o.amount > 70]

# Combined with orderby (having runs at iteration time, not after sort):
[o.amount | o <- orders, orderby o.amount desc, having o.amount > 70]

LIMIT / OFFSET clauses

SQL-style row caps. limit N keeps at most N output rows; offset N skips the first N post-filter rows. Both apply to all four comprehension flavors (list, set, dict, lazy) and to both surface forms (pipe and pipe-less). They are terminal-ish: once seen, only the other of the pair may follow.

# Basic
[x | x <- xs, limit 3]                       # first 3 rows
[x | x <- xs, offset 5]                      # skip first 5
[x | x <- xs, offset 5, limit 3]             # paging: skip 5, then take 3

# Order is free — these are equivalent
[x | x <- xs, limit 3, offset 5]

# Combined with orderby (SQL convention — limit/offset run AFTER sort)
[x | x <- unsorted, orderby x desc, limit 5]

# Combined with orderby + having
[t.amount | t <- txns, orderby t.amount desc, having t.amount > 50, limit 2]

# pipe-less form (no commas between clauses)
[x * 3 for x in xs if x > 2 limit 4]
[x for x in xs offset 6 limit 2]
[x for x in unsorted orderby x desc limit 2]

# Lazy generator — limit caps total Next() pulls, offset skips post-filter rows
g: (x * 2 | x <- big_source, x > 100, offset 10, limit 5)
gen_take(3, g)   # yields up to 3 elements (lazy stops emitting at limit anyway)

Soft keywords. limit and offset are NOT reserved at the lexer level — they remain ordinary identifiers usable as variable names, property names, and DSL slot names (bindings.limit, {limit:number}). The parser recognizes them as clause keywords only when they appear as the first token of a comprehension clause.

Caveat. Inside a comprehension clause list, you cannot use limit or offset as the LHS of a filter expression. [x | x <- xs, limit > 5] parses limit as the LIMIT clause keyword and chokes on > 5. Parenthesize to disambiguate: [x | x <- xs, (limit > 5)].

Validation. Both clauses evaluate to non-negative integers. Negative or non-integer values surface as runtime errors. limit 0 yields the empty result; offset N with N greater than the source length yields the empty result.

Sets/dicts. Limit/offset apply and slice the materialized result in its canonical order (July 2026 — previously Go-map order, which made the slice a different random sample per run): a set comprehension's prefix is its canonically-least members, and a dict comprehension slices its sorted key walk. Deterministic paging works in every flavor.

Tests: tests/axioma/comprehensions/test_limit_offset.ax

Tests: tests/axioma/comprehensions/test_tier15_first_gen_multi_having.ax

Tests: tests/axioma/comprehensions/test_tier1_orderby_groupby.ax

Range generators

Any range expression is a valid generator source, and iteration follows the range's own order (see Ranges in §4 — direction, ..<, by steps):

[x * x | x <- 1..10]            # inclusive 1..10  → [1, 4, 9, 16, …, 100]
[x | x <- 1..<10, x % 2 == 0]   # half-open       → [2, 4, 6, 8]
[x | x <- 10..1 by 3]           # descending, stepped → [10, 7, 4, 1]
{x | x <- 1..100, prime?(x)}    # set of primes ≤ 100
first((x * x | x <- 1..), 5)    # OPEN-ENDED range in a LAZY comprehension —
                                #   streams on demand → [1, 4, 9, 16, 25]
[x | x <- 1..]                  # eager comprehension over 1.. → catchable
                                #   Error (it would never finish)

An open range (1..) is the natural unbounded integer source: use it in a lazy (parenthesized) comprehension and pull with first(gen, k) / gen_take. For non-arithmetic infinite sources ("primes", "fibonacci", …) infinite_set(...) remains the tool.

Intensional-class generators (Russell iota)

Define an intensional class once with the <Concept> where <pred> and use it as a generator source. Membership is computed by combining the base concept's extent with the predicate restrictor:

adults: the Person where age >= 18
all_adult_names: [p.name | p <- adults]

This is the Russell-faithful form of "the things that satisfy P." Useful when the same restrictor predicate is consulted from several comprehensions — define it once, reuse by name.

The same question, many ways

Comprehensions, quantifiers, higher-order builtins, and the membership operator all answer overlapping questions. The cleanest illustration is the existential question — "is there an X in S satisfying P?" — which has 18 working surface forms in Axioma:

persons: {mike, alice}

# Quantifier family — three spellings, same AST
exists x in persons | x.name == "Mike"                             # keyword
`exists x in persons | x.name == "Mike"                            # backtick digraph (ASCII)
∃      x in persons | x.name == "Mike"                             # Unicode glyph

# Set-comprehension family — "the matching set is non-empty"
len({x | x <- persons, x.name == "Mike"}) > 0                      # Axioma pipe
{x | x <- persons, x.name == "Mike"} != {}                         # Axioma pipe
not ({x | x <- persons, x.name == "Mike"} == {})                   # De Morgan
len({p for p in persons if p.name == "Mike"}) > 0                  # Python
{p for p in persons if p.name == "Mike"} != {}                     # Python

# List-comprehension family — "indicator sum > 0"
sum([1 | p <- persons, p.name == "Mike"]) > 0                      # Axioma pipe
sum([1 for p in persons if p.name == "Mike"]) > 0                  # Python
len([1 for p in persons if p.name == "Mike"]) > 0                  # Python

# Higher-order — reductions over the collection
len(filter(func(p) [p.name == "Mike"], persons)) > 0
reduce(func(acc, p) [acc or p.name == "Mike"], false, persons)

# Walrus binding — compute name once, reuse it
{x | x <- persons, n: x.name, n == "Mike"} != {}

# Lazy + force — produce a generator, then materialize
g: (x | x <- persons, x.name == "Mike")
len(force(g)) > 0

# Lazy + gen_take(1) — SHORT-CIRCUITED existence (asymptotically cheaper)
len(gen_take(1, (x | x <- persons, x.name == "Mike"))) > 0

# Hash destructure — different source shape
hashes: [{name: "Mike"}, {name: "Alice"}]
len({n | {name: n} <- hashes, n == "Mike"}) > 0

# Negated universal — ∃x.P(x) ≡ ¬∀x.¬P(x)
not (forall x in persons | x.name != "Mike")

Plus the related-but-distinct membership test, which presupposes you already have the witness:

mike in persons                                                    # "is mike one of them?"

Why so many. Each form aligns with a different intellectual tradition: math ({x | …}), Python (for x in xs if …), SQL (orderby/having/limit/offset), Haskell (walrus), Prolog (<- over relational predicates), F-logic (concept extents, @tag filters), and indicator-sum probability. The right form is the one your reader will find most natural. Working showcase: tests/axioma/showcase/method.ax.

Short-circuit note. Quantifier forms (exists / ∃) and gen_take(1, lazy) stop at the first match. Eager comprehension forms scan the full collection. For large collections the difference matters — pick the short-circuiting form when the predicate is cheap and the collection is large.

8. First-Order Logic

Quantifiers

a: {1, 2, 3, 4, 5}
forall x in a: x > 0           # true
forall x in a: x > 3           # false
exists x in a: x > 3           # true
exists x in a: x > 10          # false

Bounded Range & Counting Quantifiers

Axioma supports advanced bounded range quantifiers (which operate over integer intervals without requiring an explicit set domain) and comparison-based counting quantifiers (which assert that a specific number of elements satisfy a predicate):

Bounded Range Quantifiers

• Double-sided range: evaluates the predicate over the range [lower..upper] (for <=) or [lower..<upper] (for <).

  forall 1 <= x <= 10: x > 0       # true
  exists 1 < x < 5: x == 3         # true

• Single-sided range: defaults to a lower bound of 0 and evaluates up to the upper bound.

  forall x < 5: x >= 0            # true (evaluates x = 0, 1, 2, 3, 4)
  exists x <= 0: x == 0           # true (evaluates x = 0)

Arbitrary Counting Quantifiers

Checks whether exactly, at least, or at most a specified number of elements in a set satisfy a predicate. Uses standard comparison operators (==, >=, <=, >, <) directly following the exists keyword:

domain: {1, 2, 3, 4, 5}
exists >= 3 x in domain: x > 2    # true (witnesses: 3, 4, 5)
exists <= 1 x in domain: x > 4    # true (witness: 5)
exists == 2 x in domain: x % 2 == 0 # true (witnesses: 2, 4)
exists > 1 x in domain: x < 3      # true (witnesses: 1, 2)

With predicates

nums: {1, 2, 3, 4, 5, 6}
forall x in nums: positive(x)
exists x in nums: even(x)
forall x in nums: x < 10 and x > 0

Combined

a: {2, 4, 6}
b: {1, 2, 3, 4, 5, 6}
forall x in a: even(x) and (x in b)
exists x in b: odd(x) and (x > 3)

Symbolic-mode quantifiers — textbook syntax

The bounded forms above (forall x in a: ...) iterate a domain and return a Boolean. Axioma also accepts bare textbook-style quantifiers with no in <domain> clause — these produce a Formula value, a symbolic carrier you can pass to the resolution/CNF/satisfiability machinery in fol/, sol/, and logic/.

# Bare textbook form — no marker between variable and body
f1: ∀x P(x)              # → ∀ x. P(x)        (type: formula)
f2: ∃x F(x)              # → ∃ x. F(x)

# Dot form
f3: ∀x. P(x)             # identical to f1
f4: ∃x. F(x)

# ASCII keyword equivalents
forall x P(x)
exists x F(x)
`forall x P(x)           # backtick digraph
`exists x F(x)

# Complex bodies — quantifier binds widely
∀x P(x) → Q(x)           # → ∀ x. (P(x) → Q(x))
∃x P(x) ∧ Q(x)           # → ∃ x. (P(x) ∧ Q(x))
∀x ¬P(x) ∨ Q(x)          # → ∀ x. ((¬P(x)) ∨ Q(x))

# Nested quantifiers
∀x ∃y P(x, y)
∃x ∀y P(x, y) → R(x, y)

Mode summary:

Tier 1 limitation: the connectives ¬ ∧ ∨ → ↔︎ on Formula operands still dispatch to Boolean semantics — building compound formulas like ¬∀x P(x) ↔︎ ∃x ¬P(x) at the symbolic level requires Tier 2 Formula-aware connectives. For now, keep connectives inside the quantifier body.

Other Tier 1 textbook additions

# Biconditional — both Unicode forms lex to IFF
true ↔ false                 # false  (U+2194, modern textbook)
true ⟺ false                 # false  (U+27FA, was lexed but never wired)

# Truth constants
⊥                            # false  (falsum, U+22A5)
⊤                            # true   (verum, U+22A4)

# Proper subset distinct from subset
{1,2} ⊊ {1,2,3}              # true  (proper subset)
{1,2,3} ⊊ {1,2,3}            # false (equal, not proper)
{1,2} ⊆ {1,2}                # true  (regular subset allows equality)

# Set difference — Enderton/Halmos notation
{1,2,3,4,5} \ {2,4}          # {1, 3, 5}

# Uniqueness quantifier
∃!x in {1,2,3} | x == 2      # true (exactly one)

Formula type + predicate

f: ∀x P(x)
@f                           # "formula"
formula?(f)                  # true
boolean?(f)                  # false

See tests/axioma/logic/test_textbook_parity_tier1.ax for full coverage.

9. Multi-Valued Logics

Axioma has five first-class logic kinds, each with its own truth-value type. Operators (and, or, not, implies, iff, xor) automatically dispatch based on operand types. The dispatch priority is Belnap > Intuit3 > Łukasiewicz > Kleene > Boolean.

Truth values are first-class. The forms the interpreter prints are themselves source — every non-Boolean truth value has a lexable glyph literal, an ASCII digraph, and a dotted member on its seeded Concept, all byte-identical to the constructor call:

Bare ⊤ / ⊥ stay Boolean true / false. Each seeded Concept also carries values — the logic's canonical domain (Belnap.values → [⊤ᵇ, ⊥ᵇ, ⊤⊥ᵇ, ?ᵇ]) — and the literals work as match patterns:

w: ⊤⊥ᵇ                            # ≡ belnap("both") — byte-identical value
m: match w with | ⊤⊥ᵇ => "glut" | ?ᵇ => "gap" | _ => "classical"   # → "glut"
forall p in Belnap.values | designated(p or not p)   # → false — the gap escapes LEM

Three semantic rules, uniform across the family:

1. Truthiness is designation. if/while on a typed truth value branch by the logic's designated set — B4 {⊤ᵇ, ⊤⊥ᵇ} (a glut is true-enough to act on), K3/G3 {true}, Ł3 {1.0}. So if ⊥ᵇ … and if ?ᵏ … take the else-branch, and if x always agrees with designated(x). (Untyped om keeps its SETL truthiness — see the dual-null note in §4.)
2. == / != are metalanguage equality — a plain Boolean, coercing the untyped spellings (belnap("true") == "true", ?ᵏ == om, lukasiewicz(1.0) == 1.0); values of different logics are never equal. The object-language biconditional is iff (?ⁱ iff ?ⁱ → ⊤ⁱ). Membership composes too: ⊤⊥ᵇ in Belnap.values → true.
3. Operands are validated — no silent coercion. Logic operators accept a typed value's own kind plus Boolean / om / Kleene (the canonical embeddings; Ł3 also takes raw numbers in [0, 1]) and error loudly on anything else: belnap("true") and "banana" is an error, not a quiet gap, and cross-logic mixes without a canonical embedding (⊤⊥ᵇ and ½ł, ⊤ⁱ and ⊤⊥ᵇ) are rejected with a wrap hint.

Boolean

Classical two-valued. Default for true/false.

true and false        # false
true implies false    # false
not true              # false

Kleene K3 (three-valued)

true / false / unknown. Two spellings of the same tables: the untyped SETL om / Ω (the historical K3 unknown), and the typed literals ⊤ᵏ ⊥ᵏ ?ᵏ (≡ kleene("true") / kleene("false") / kleene("unknown")).

om and true           # Ω    (unknown — untyped, stays om-flavored)
om or  true           # true
not om                # Ω
?ᵏ and ⊤ᵏ             # ?ᵏ   (typed — results stay Kleene)
?ᵏ == om              # true (canonical equality); `if ?ᵏ` AND `if om` are both
                      #      FALSY now (designation — om folds onto it in 2.5)

Łukasiewicz L3 (real-valued)

Continuous truth values in [0, 1]; the three canonical points have literals ⊤ł (1.0), ½ł (0.5), ⊥ł (0.0).

half: lukasiewicz(0.5)           # ≡ ½ł
qrtr: lukasiewicz(0.25)
half and qrtr         # min(0.5, 0.25) = 0.25
half implies qrtr     # min(1, 1 - 0.5 + 0.25) = 0.75
½ł and 0.8            # ½ł — raw numbers in [0,1] embed (the fuzzy idiom)
½ł == 0.5             # true; only ⊤ł (1.0) is designated/truthy

Belnap B4 (paraconsistent four-valued)

T, F, Both, Neither — supports contradictory information.

p: ⊤⊥ᵇ                           # the glut literal — ≡ belnap("both")
q: belnap("true")                # constructor form, ≡ ⊤ᵇ
p and q                          # ⊤⊥ᵇ — contamination propagates
Belnap.gap                       # ?ᵇ  (Priest's terms: .glut / .gap alias .both / .neither)
truth("parent", "John", "Mary")  # Query stored Belnap value (relation named by string)

The four values ⊤ᵇ, ⊥ᵇ, ⊤⊥ᵇ, ?ᵇ are lexable literals (not just display forms); designated(x) is true for ⊤ᵇ and the glut ⊤⊥ᵇ, and if/while branch accordingly.

The two orders of B4. B4 is a bilattice: the bare and/or/not above are the truth order (how true?), while evidence combination lives on the knowledge order (how much information? — neither < true,false < both), surfaced as b4_join (⊕ — accept everything every source says) and b4_meet (⊗ — keep only what all sources agree on):

w1: belnap("true")               # witness 1: guilty
w2: belnap("false")              # witness 2: innocent
b4_join(w1, w2)                  # → ⊤⊥ᵇ  conflict surfaces as a GLUT (⊕)
b4_meet(w1, w2)                  # → ?ᵇ   no consensus (⊗)
designated(b4_join(w1, w2))      # → true — a glut is true-enough to act on
w1 and (not w2)                  # → ⊤ᵇ   truth-order `and` can NEVER build a glut
b4_join(w1, w2, om)              # variadic; or fold a collection: b4_join([w1, w2])

w1 ⊕ w2                          # infix glyph forms (⊗ binds tighter than ⊕,
w1 `oplus w2                     #   mirroring ∩/∪); ASCII via `oplus / `otimes

Operands must be Belnap/Boolean/om/Kleene (strings error — wrap with belnap(...)). The same strictness covers the truth-order operators (and/or/not/implies/iff/xor) since July 2026 — see rule 3 above.

Evidence can also accumulate on a stored fact: set_truth_combine(rel, args..., value) ⊕-merges the incoming value onto the fact's stored B4 truth instead of overwriting it (contrast set_truth, which is last-write-wins):

relation rain(city)
axiom rain("seattle")                          # truth defaults to ⊤ᵇ
set_truth_combine("rain", "seattle", "false")  # ⊤ᵇ ⊕ ⊥ᵇ → stores + returns ⊤⊥ᵇ
truth("rain", "seattle")                       # → ⊤⊥ᵇ — the conflict is KEPT

The fact must already be stored, and the strict-bivalence mode (set_truth_logic("Boolean")) rejects a glut-producing report (non-fatal false, stored truth unchanged).

Gödel G3 (intuitionistic three-valued)

true / false / unknown (literals ⊤ⁱ ⊥ⁱ ?ⁱ) — but with intuitionistic semantics:

p: ?ⁱ                            # ≡ intuit3("unknown")
not p                            # ⊥ⁱ  (G3 collapses U to F; K3 keeps U)
p implies p                      # ⊤ⁱ  (reflexive — always)
g3_lem(?ⁱ)                       # ?ⁱ  — LEM is NOT a tautology
g3_dne(?ⁱ)                       # ?ⁱ  — double-negation elimination FAILS
designated(g3_lem(?ⁱ))           # false — so LEM fails as an inference too

p == ⊤ⁱ                          # false — plain Boolean METALANGUAGE equality
p iff p                          # ⊤ⁱ    — the object-language biconditional

The g3_* helpers (g3_and / g3_or / g3_not / g3_implies / g3_lem / g3_dne) return typed Intuit3 values, so their results flow straight back into and / not / designated. (== on G3 values used to return the biconditional itself — a truthy ?ⁱ for unknown == true; it is now Boolean equality, and the biconditional lives at iff.)

Constructors, types, and equality

The literals cover the canonical values; the constructors are the dynamic/coercion form — belnap() (B4), lukasiewicz() (Ł3, any value in [0,1]), intuit3() (G3), and kleene() (K3) — for converting a runtime String/Boolean/om into a truth value. type(x) and the :: x type-of sigil return the proper TitleCase name, and each value is is-checkable against its seeded primitive Concept:

ku: kleene("unknown")            # also kleene(om), kleene("u"), kleene("?") — or just ?ᵏ
type(ku)                         # → Kleene        (@ku is the same)
ku is Kleene                     # → true
ku == om                         # → true   (coerces to its canonical Boolean/Om form)

kt: kleene("true")
kt and ku                        # → ?ᵏ     (results stay Kleene)
not ku                           # → ?ᵏ
ku implies ku                    # → ?ᵏ     (K3 — contrast G3's reflexive → ⊤ⁱ)

type(⊤⊥ᵇ)                        # → "Belnap"
type(½ł)                         # → "Lukasiewicz"
type(?ⁱ)                         # → "Intuit3"

# Equality coerces each value's own untyped spellings — and ONLY those:
belnap("true") == "true"         # → true
⊤⊥ᵇ == "both"                    # → true
lukasiewicz(1.0) == 1.0          # → true  (== 2 is false — no clamping)
⊤ᵇ == ⊤ᵏ                         # → false (cross-LOGIC values are never ==)

Note: Kleene's unknown is still represented by om (Ω) at the operator level — the existing om and true tables are unchanged. kleene(...) / ?ᵏ is the typed form: it normalizes to om for evaluation, runs the same K3 tables, then re-wraps logic results back into a Kleene so they stay introspectable (mirroring how belnap/lukasiewicz/intuit3 operators return their own type). No asymmetry any more: ?ᵏ == om is true, and both if ?ᵏ and if om are falsy (designation — om folds onto the designation path in step 2.5, matching the typed unknown it equals).

Truth tables

Kleene       show truth_table for and
Lukasiewicz  show truth_table for implies
Belnap       show truth_table for or
Intuit3      show truth_table for implies

tableform(f, "belnap") prints the full grid of any function over an MVL domain ("kleene" / "lukasiewicz" / "intuit3" / "boolean" too) — and since the cells are lexable literals, a printed cell pastes back into the REPL as the value it shows.

10. Modal, Temporal, Epistemic & Deontic Logic

Modal operators

necessarily(p)        # □p — p holds in all accessible worlds
possibly(p)           # ◇p — p holds in some accessible world

Temporal logic

always(p)             # G p — p holds at all future times
eventually(p)         # F p — p holds at some future time
next(p)               # X p — p holds at the next time step
until(p, q)           # p U q — p until q

\newpage

Epistemic logic

alice: agent("alice")
b: believes(alice, "answer", 42)  # record a belief; do not assert its content
println(beliefs_of(alice))         # ["answer(42)"]
assert answer(42)
k: knows(alice, "answer", 42)     # requires an existing supporting fact

Stored believes(agent, relation, args...) and knows(agent, relation, args...) use an Agent entity. Their contents are canonical proposition strings: nested quotes, backslashes and quoted agent names retain their identity when listed or queried. Attributing another person's belief does not endorse its content. This explicit storage is distinct from natural-language attitude expressions and from evaluation in an activated possible-world model.

There is currently no public common_knowledge builtin. The internal finite-model checker tests the proposition at every world reachable through any finite sequence of the selected agents' accessibility links, including the actual world. Everyone knowing a proposition at the actual world is a weaker condition. Neither stored reports nor nested proposition strings supply a general calculus of common knowledge. See epistemic model boundaries.

Deontic logic

obligatory(action)
permitted(action)
forbidden(action)

The examples above are the public modal/temporal/epistemic/deontic surface in this manual; implementation notes live with the corresponding evaluator code.

11. Fuzzy Logic & Higher-Order Logic (SOL)

Fuzzy logic

Continuous truth in [0, 1] with fuzzy set membership:

tall: fuzzy_set("tall", lambda h => sigmoid(h - 180))
membership(tall, 175)          # 0.38
membership(tall, 190)          # 0.88

Second-Order Logic (SOL)

Quantification over predicates and functions:

forall_pred P: forall x: P(x) implies P(x)        # Trivially true
exists_pred P: forall x in domain: P(x)           # ∃P. ∀x. P(x)

Treat the SOL examples here as the public surface; the implementation is experimental and may change as the quantified logic engines mature.

12. Lambda Calculus & Higher-Order Functions

Function definitions

inc: lambda x => x + 1             # lambda arrow (multi-arg needs parens)
add: lambda (x, y) => x + y
dbl: (x) => x * 2                  # parenthesized arrow-lambda (no `lambda` keyword)
sum: (a, b) => a + b               # same AST as `lambda (a, b) => …`
multiply: func(a, b, c) [a * b * c]   # canonical REBOL bind
fn half(x) [x / 2]                 # `fn`, `fun`, and `function` alias `func`
fun thrice(x) [x * 3]
function scale(x) [x * 10]
func double(x) [x * 2]             # named declaration (optional keyword form)
double(x) = 2 * x                  # EQUATION form — same function, no keyword
fun circleArea(r) = pi * r * r     # optional designator on the equation form
function area(r) = pi * r * r      # long designator — same lowering

Relational generic functions — func[T]

A constructor such as data Pair[T] = MkPair(T, T) requires repeated direct fields to have the same runtime type. A generic function extends this rule to its arguments and result. Each call chooses its own type; a bound restricts the choice without promoting or converting values.

keep_first: func[T](left :: T, right :: T) :: T [left]
println(keep_first(10, 20))              # 10
println(keep_first("a", "b"))            # a
println(error?(try(keep_first(10, 20.0)))) # true

numeric_id: func[T of Number](value :: T) :: T [value]
println(numeric_id(3))                  # 3
println(error?(try(numeric_id("3"))))    # true

T is local to the declaration, even if an outer binding has the same name. Different names, such as [A, B], make independent choices. A bound uses the constructor convention T of Number; T of Float requires an actual Float. The return annotation uses the same choice as the arguments. A function promising :: T cannot accept an Integer and return a String or Float. Early returns and labeled calls enforce the same rule.

Declaration forms. The aliases func, fn, fun, and function all support the binder. Named declarations and equations put it after the name; anonymous functions put it after the function keyword. Bracket bodies and function … end bodies have the same contract.

func echo_value[T](value :: T) :: T [value]
echo_equation[T](value :: T) :: T = value

function echo_long[T](value :: T) :: T
  value
end

# Detached signatures cover every existing lambda spelling.
echo_arrow[T] :: T -> T
echo_arrow: value => value

echo_lambda[T] :: T -> T
echo_lambda: lambda value => value

println([echo_value(1), echo_equation(2), echo_long(3),
         echo_arrow(4), echo_lambda(5)]) # [1, 2, 3, 4, 5]

Write the parameter list once when using a detached signature. It transfers to the following definition, including parenthesized, bare-arrow, backslash, and Unicode lambda forms. An inline lambda[T] form is not introduced.

Partial application and defaults. A partial application retains the type choices made by its supplied arguments. Each subsequent call gets an independent copy of those choices, so an as-yet-unbound parameter remains polymorphic. Defaults are checked as arguments when evaluated; default expressions may refer to earlier parameters.

keep_second: func[T](left :: T, right :: T = left) :: T [right]
println(keep_second(8))                 # 8

same_second: func[T](left :: T, right :: T) :: T [right]
let after_integer = same_second(1)
println(after_integer(2))               # 2
println(error?(try(after_integer("x")))) # true

Clauses and guards. Put a detached generic signature above the first clause or pipe group. Its argument relationships are checked before pattern/guard selection. A type error does not try another clause. The chosen result must satisfy the return contract. For a generic group, an unmatched call's none is also checked: an Integer choice for T cannot silently return none. Existing non-generic clause fallback behavior is unchanged.

choose_value[T] :: Boolean -> T -> T -> T
choose_value(flag, left, right)
  | flag = left
  | otherwise = right
println(choose_value(false, 10, 20))     # 20

Explicit structural relationships. A direct T still compares outer runtime type identity: two Arrays can have different contents. Write Array of T or List of T to require one element type, or (A, B, C) for a tuple's individual component types. These structures can nest and appear in input and result annotations.

third_same[T] :: (T, T, T) -> T
third_same(t) = t[3]
third_any[A, B, C] :: (A, B, C) -> C
third_any(t) = t[3]
println(third_same((1, 2, 3)))                   # 3
println(error?(try(third_same((1, 2, "3")))))    # true
println(third_any((1, true, "3")))              # 3 (String)

numeric_first[T of Number] :: Array of T -> T
numeric_first(xs) = xs[1]
println(numeric_first([4, 5]))                   # 4
println(error?(try(numeric_first([4, 5.0]))))     # true

Different variables permit different types without requiring them. A bound applies to each occurrence, including nested elements, without converting a chosen T. Array of Array of T constrains innermost elements; Array of T with T chosen as Array checks only those elements' outer Array identity. Empty Arrays and Lists supply no element evidence. An empty collection result is valid, but a scalar result T is refused when no input established T's type. Partial calls retain their evidence; later calls recheck captured Arrays. Generic call contracts check inputs again after the body and do not attach call-local T variables as permanent constraints on an otherwise untyped Array. Existing concrete Array annotations keep their persistent write checks. A detected mutation error does not roll back other effects of the body.

Scope and execution boundaries. Every declared type parameter must occur in an input annotation, directly or inside a supported Array/List/product structure. T -> T as a callback annotation, unions involving T, other generic containers and specialized ADT annotations remain unsupported. Generic annotations on lazy parameters are refused. Fixed generic parameters may coexist with ordinary refinements, defaults, destructuring slots, and an untyped variadic rest parameter where the underlying function form supports them. Detached signatures retain their existing restrictions on variadics and destructuring. Generic clause groups currently require one fixed arity and one group signature.

The evaluator enforces the contract, including calls through aliases and higher-order builtins. --typecheck and the editor report known argument conflicts, unknown bounds, and definite return violations; dynamic cases remain runtime checks. The bounded HM lens additionally checks unbounded generic bodies under arbitrary rigid type parameters and exposes fresh instantiations per call; recursion remains monomorphic. It diagnoses bodies that cannot implement their signature, even before a call. Bounds, defaults and refinements remain runtime features outside that proof. --infer reports skips for unsupported bodies; #language axioma/hm rejects skips. The island's structural ML type rules are stricter than host outer identity for bare T applied to containers. This does not make the host checker a whole-language polymorphic inference engine. Explicit generics take precedence over the observational first-result cache of @infer. Generic activations use ordinary recursion so return checks are preserved; tail-call optimization for them is deferred. The VM explicitly refuses generic functions. External statement-stepping APIs also refuse generic calls until they can retain call-specific type constraints.

Parenthesized and bare arrow-lambdas — (params) => body, x => body

A parenthesized parameter list followed by a body arrow is a lambda, with no leading lambda / λ / \ keyword. It desugars to the same function value as lambda (params) => body — useful for dense callbacks and for readers coming from JavaScript / TypeScript.

Body arrows for these keyword-less forms are fat => and thin ->. The Unicode → (and the word implies, ⟹, -->) is material implication after a bare identifier or a parenthesized operand — p → q, (p) → q, not p implies q — so it does not open a lambda here; after a binder keyword it still does (lambda x → x + 1, \x → x + 1, λx → x + 1), because the keyword removes the ambiguity:

map((x) => x * 2, [1, 2, 3])             # → [2, 4, 6]
map((x) -> x * 2, [1, 2, 3])             # same
map(x => x * 2, [1, 2, 3])               # bare single-param (second wave)
map(x -> x * 2, [1, 2, 3])               # bare + thin arrow

typed: (x :: Integer) => x + 1
ret:   (x :: Integer) :: Float => x * x  # return type before the body arrow
hof:   (f :: Integer -> Integer) => f(3) # HOF param type may use thin arrows
idF:   (f) :: (Integer -> Integer) => f  # function *return* type: paren the type

greet: (name, greeting = "Hello") => greeting + ", " + name
pack:  (...xs) => xs
blk:   (x) => [ y: x * 2  y + 1 ]        # multi-statement body — use `[…]`, not `{…}`
dist:  (p) => [ (x, y): p  sqrt(x*x + y*y) ]  # destructuring bindings are statements here too
one:   (x) => [x]                        # `[e]` after `=>` is a block: yields e, not `[e]`
wrap:  (x) => [x,]                       # one-element array: trailing comma, or `[[x]]`

# `case` / `match` inside that block is the body, not an array of the result
data ShirtSize = Small | Medium | Large | XLarge
price: (size :: ShirtSize) :: Float => [
    case (size)
    | Small  => 11.00
    | Medium => 12.50
    | Large  => 14.00
    | XLarge => 16.00
]
price(Small)                             # → 11.00  (Float, not `[11.00]`)

A TitleCase parameter is refused — it is a signature, not a lambda. Type names are TitleCase, so Integer -> Integer in expression position would be a lambda whose parameter shadows the type Integer. That is never what an author means, and it used to be silent: sig : Integer -> Integer bound lambda(Integer) => Integer at exit 0, quietly discarding the signature, while the :: twin enforced it.

sig : Integer -> Integer     # SyntaxError: `Integer` is a type name, not a
                             # lambda parameter
sig :: Integer -> Integer    # the detached signature — enforced
sig: func(n) [ n ]

x -> x * 2                   # a lambda parameter is lowercase

The refusal is specific to the bare arrow form. A function-type synonym (type Mapper = Integer -> Integer), a match arm (| Absent -> -1), a typed parameter ((f :: Integer -> Integer) => …) and the frame form (usa[gdp -> 28000]) are separate arrows with their own gates, all unaffected.

Tail calls run in constant space in every spelling. A call in tail position — the last thing an if branch, a switch/match arm, or a block body does — is trampolined rather than recursed, for func, (params) => …, x => … and lambda alike (self- and mutual recursion, the inner-helper idiom included), so rep = (acc, n) => if n == 0 then acc else rep(acc + 1, n - 1) runs rep(0, 1000000) without ever nearing the recursion-depth guard (max Eval depth 50000). Destructuring parameters, ...rest and refinements keep the ordinary recursive path. A tail loop that re-enters the same call with the same argument objects — the Ω combinator twin = x => x(x), twin(twin), or a zero-argument poll() that never changes state — is refused after 1 000 000 such hops with a catchable recursion limit exceeded (tail loop re-entered the same call …) Error, the constant-space twin of the depth guard: caught, not hung.

Rules that differ from a blind JS port:

() alone is still the empty tuple; () => 42 and () -> 42 are nullary functions. Partial application and over-application follow the same rules as every other function. Defaults and rest parameters share the evaluator path with func (and are refused under --vm, §911).

Exhaustive exemplar: tests/typescript/src/functions.ax lists every shipped function and lambda spelling in one runnable file.

Destructuring parameters

An anonymous func or lambda may destructure a parameter in place, using the same pattern grammar as match. The commonest use is a higher-order call over pairs.

fst:  func((a, b)) [ a ]                     # tuple pattern — ONE param
both: func([a, b]) [ a * b ]                 # array pattern
head: func([h | t]) [ h ]                    # cons pattern
lfst: lambda ((a, b)) => a                   # lambda spells it the same way

map(func((a, b)) [ a + b ], [(1,2), (3,4)])  # → [3, 7]

Both pairs of parens are required. The outer pair is the parameter list, so func(a, b) and lambda (a, b) => … are the two-parameter forms — only the inner bracket makes a slot structural. Called with one tuple, lambda (a, b) => a + b returns a partial application rather than a sum.

Only ( and [ open a pattern: func(0) and func(_) are parameters literally named "0" and "_". Literal and wildcard patterns, guards, and multiple clauses all live on the named clausal form (func f(0) [...]) and on equations, both covered just below. Patterns compose with ordinary, typed and variadic parameters — func(k :: Integer, (a, b), ...rest) — and an argument that does not match the pattern raises a catchable error rather than binding silently.

Variadic parameters — ...rest

A parenthesized parameter list may end with a rest slot: ...name collects every argument beyond the fixed ones into an Array, empty when there are none. The form belongs to every parenthesized header alike — func/fn, the named declaration, the equation head, and lambda in all of its spellings:

tail: func(a, ...rest) [ [a, rest] ]
tail(1)                       # → [1, []]
tail(1, 2, 3)                 # → [1, [2, 3]]

pack: lambda (...xs) => xs    # rest-only lambda
pack()                        # → []
pack(1, 2, 3)                 # → [1, 2, 3]

count_tail: λ(a, ...t). len(t)   # the λ and \ spellings take it too
count_tail(1, 2, 3)           # → 2

The rest slot must be last — lambda (...xs, a) and func(...xs, a) are SyntaxErrors — and it lives only in a parenthesized header: the curried binder list (λx y. e) has no rest form, exactly as func has no unparenthesized header at all. Reflection reads both constructs identically: parameters lists the fixed slots, arity counts them, and signature renders the rest slot last.

arity(tail)                   # → 1     fixed slots only
arity(pack)                   # → 0
signature(tail)               # → "func(a, rest...)"
signature(pack)               # → "func(xs...)"

A typical use is a fold whose seed is the first argument:

variadic_max: lambda (first_v, ...more) =>
  reduce(lambda (a, b) => if a > b then a else b, first_v, more)
variadic_max(3, 1, 4, 1, 5)   # → 5

Defaults order before the rest slot — func(a, b = 2, ...rest) is the full ordering, covered under Labeled arguments just below. Under --vm a rest parameter is refused at compile time, on func and lambda alike (variadic parameter "...rest" is not supported under --vm); variadic code runs on the evaluator.

Labeled arguments — parameter defaults and calling by name

A parameter may carry its own default, and the call site may name the slot it is filling instead of counting positions. The two halves are one feature: the name written in the signature is the name the caller uses.

split_custom: func(line, on = ",") [ split(line, on) ]

split_custom("a,b,c")             # → ["a", "b", "c"]   default supplies `on`
split_custom("a-b-c", "-")        # → ["a", "b", "c"]   still positional
split_custom("a|b|c", on: "|")    # → ["a", "b", "c"]   filled by name

Two spellings declare a default, one spelling calls by name. In a signature on = "," and on: "," are the same declaration; at the call site only on: "|" is a labeled argument, and on = "|" is a syntax error. The colon is read by the house rule that type names are TitleCase — after :, a TitleCase identifier annotates a type and anything else is a default, so b: Integer is a typed required parameter while b: 99 defaults. Write = when the default is itself TitleCase. A typed slot takes both: n :: Integer = 5.

Pun: omit the value when a local of the same name exists. f(name:) is f(name: name) — the slot name is also the identifier that supplies the value. Lookup is the caller, not the parameter. Mix with explicit labels in one call; reorder still works. A newline after : is a missing value, not a pun. :name is a get-word (fetch), not a label. func(name:) in a definition stays a syntax error.

greet: func(name, greeting = "Hello") [ greeting + " " + name ]

name: "Ada"
greeting: "Yo"

greet(name:)                     # → "Hello Ada"     ≡ greet(name: name)
greet(name:, greeting:)          # → "Yo Ada"
greet(name:, greeting: "Hi")     # → "Hi Ada"        mixed
greet(greeting: "Hi", name:)     # → "Hi Ada"        reorder

Every positional argument must still precede the first labeled one: greet(name:, "Ada") is parameter 'name' assigned twice when name is the first parameter — the same error as greet(name: name, "Ada"). A pun is a labeled call, so it does not partially apply (add(x:) is missing value for parameter 'y', not a Function). Under --vm a labeled call, pun included, is refused at compile time.

Once a call names a slot it may name them all, in any order, and a defaulted slot may simply be left out:

box: func(w, h = 1, fill = "·") [ [w, h, fill] ]

box(3)                       # → [3, 1, "·"]
box(3, fill: "#")            # → [3, 1, "#"]     skips over `h`
box(h: 2, w: 3)              # → [3, 2, "·"]     order is the caller's

Positional arguments bind from the left as always, so every positional argument must precede the first labeled one — box(w: 3, 2) binds 2 to w a second time and raises parameter 'w' assigned twice (both positional and keyword). A label that matches no parameter raises unknown parameter; neither is a silent miss.

The default expression is evaluated on every call, in the frame being built, so it may read a parameter declared to its left and it cannot accumulate state between calls:

seed: func(xs = []) [ xs push 1 ]
seed()                       # → [1]
seed()                       # → [1]   a fresh [] each call, never [1, 1]

pad: func(x, upto = x + 1) [ upto - x ]
pad(10)                      # → 1     the default reads `x`

Defaults are declared after the required parameters (a required slot sitting to the right of a defaulted one can never be reached, and calling raises missing value for parameter), and ...rest stays last: func(a, b = 2, ...rest) is the full ordering.

Parenthesized lambda and parenthesized arrow-lambda accept untyped defaults (b = 2) and typed defaults (b :: Integer = 2) the same way func does. The equation form takes the same defaults — f(a, b: 5) = a + b then f(2) is 7 — because : inside the parens does not collide with the body's =. b = 5 inside the parens is the same declaration. A pun f(name:) = body is still a SyntaxError: that is a call-site form, not a missing default. A bare colon on a lambda parameter is still a type annotation, not a default: lambda (x, y: Integer) => … is two required parameters (the second typed); write y = 2 or y :: Integer = 2 for a default.

A builtin takes labels where it publishes parameter names. signature reports what a builtin's slots are called, and those are the labels it accepts — round(3.14159, digits: 2) is round(3.14159, 2). A builtin has no defaults, so a labeled call may reorder its slots but may not skip one, and a variadic tail (println(values...)) can only be filled positionally. Where a builtin publishes no names the label is refused, never ignored: labeling an argument that the callee cannot place is an error, not a silent fallback to the positional reading.

signature(round)                # → "round(x, [digits])"   — so `digits` is the label
round(3.14159, digits: 2)       # → 3.14
round(3.14159, 2)               # → 3.14   the same call
round(3.14159, zzz: 2)          # error: unknown parameter 'zzz' for round

Under --vm both halves are rejected at compile time — a defaulted parameter and a labeled call alike. They are evaluator-only (§911 — the VM rejects rather than answer differently).

Equations — name(args) = expr

The keyword-free equation is the textbook spelling of a function definition — f(x) = 2 * x reads exactly as mathematics writes it (and as Julia's short form). It is pure sugar: an all-plain-parameter equation is byte-identical to func name(args) [expr] (so it compiles under --vm and redefinition is last-write-wins), and an equation with patterns or a when guard is byte-identical to a clausal func (clauses accumulate by name in source order; unmatched calls fall through to none; --typecheck exhaustiveness applies). The two spellings may be mixed in one clause group.

An optional designator — func, fn, fun, or function (all one token) — may introduce the equation the same way relation / rule introduce theirs. It adds no semantics; it is for readers who want the word visible (ML's fun, JS/Java's function, explicit intent). Those words are full aliases of func on every function form, not only equations: anonymous function(x) […], named function f(x) […], and f: function(x) […].

double(x) = 2 * x                  # ≡ func double(x) [x * 2]
add5(a, b: 5) = a + b              # default; add5(2) → 7. `b = 5` is the same
fun circleArea(r) = pi * r * r     # optional designator — same lowering
function area(r) = pi * r * r      # long designator — same again
func fact(0) = 1                   # designator + clausal equation
fact(n) = n * fact(n - 1)          # … + catch-all: fact(5) → 120
sign(x) when x > 0 = 1             # guard sits between the head and `=`
sign(x) otherwise = 0              # ≡ `when true` — last-clause catch-all
sign(x) = 0                        # unguarded clause is also a catch-all
whichsign(n) = "Positive", if n > 0
             = "Zero",     if n == 0
             = "Negative", if n < 0  # Miranda order: body, then `, if` / `, otherwise`
                                     # (≡ `when`; equality in the guard is `==`)
head2([h | t]) = h                 # cons patterns work; so do constructor,
area(Circle(r)) = 3.14 * r * r     #   tuple, wildcard, or- and as-patterns

A bracket after the head is the BODY, exactly as in the func spelling — the two are one construct with one body parser, so they cannot mean different things. An array is the double bracket, its inner bracket sitting in value position as the body's final expression:

boxed(x) = [2 * x]                 # BODY ⇒ 2 * x     ≡ func boxed(x) [2 * x]
arrayed(x) = [[2 * x]]             # the 1-element ARRAY ⇒ [2 * x]
norm(x) = [                        # several statements ⇒ the last is the value
    m: x * 2
    m + 1
]
pairup(x) = [x, x + 1]             # commas in a body ⇒ the tuple (x, x + 1)
plain(x) = 2 * x                   # no brackets needed for a one-expression body
literal(x) = ([1, 2, 3])[x]        # a bracket wanted as a VALUE is parenthesized

A bare = binding is unaffected — v = [2 * x] is still the array, because it is a value binding, not a definition. The difference is the parenthesized head: f(x) = … defines a function and takes a body, v = … binds a value.

Boundaries: the head's parameters are patterns; typed parameters (x :: Integer) and defaults (b: 5 / b = 5) are accepted and lower to the same node func builds. In a function parameter slot, a capitalized name dispatches as a constructor when that constructor exists; otherwise it binds the parameter. Match-arm patterns retain their own constructor rules; answer = 42 (no parens) remains an ordinary value binding; and the bare Haskell spelling double x = 2 * x stays a SyntaxError whose hint names this form — Axioma calls are parenthesized, so definitions are too. This completes the keyword-optional lattice: relations may drop relation on the bare uppercase header (coord(X, Y)), rules may drop rule before :-/whenever, and functions may drop func before =.

Guard sequences and pipe clauses

A guard may contain comma-separated steps: an ordinary expression tested by Axioma truthiness, pattern <- expression matching one value, or let name = expression introducing a fresh immutable local. Steps run once, left to right. Each new name is visible to later steps and its branch's result. The same sequences work after when on function clauses and match-family arms.

scaled(value)
  when Some(x) <- value,
       x > 0,
       let doubled = 2 * x,
       doubled < 100
  = Some(doubled)
scaled(value) otherwise = Absent
println(scaled(Some(3)))  # Some(6)
println(scaled(Some(60))) # Absent
println(scaled(Absent))   # Absent

A function head can also precede a group of pipe clauses. Each pipe introduces a full guard sequence and its result; these are ordered function clauses.

sign_pipe(n)
  | n > 0 = 1
  | n < 0 = -1
  | otherwise = 0

scaled_pipe(value)
  | Some(x) <- value,
    x > 0,
    let doubled = 2 * x,
    doubled < 100 = Some(doubled)
  | otherwise = Absent
println([sign_pipe(-2), sign_pipe(0), sign_pipe(3)]) # [-1, 0, 1]
println(scaled_pipe(Some(3))) # Some(6)

A pipe separates guard branches, not clauses. The head is written once, above the group; | never repeats it. SML's fun f p = e | f q = e2 is therefore refused — and refused rather than added, because under a head | name(args) = result already reads as a guard branch that calls name(args), so one line would have two meanings with nothing to choose between them. Write ordered clauses on their own lines instead (length([]) = 0 / length([_ | xs]) = 1 + length(xs)), or keep the pipes and move the patterns into guard steps:

length(xs)
  | [] <- xs = 0
  | [_ | rest] <- xs = 1 + length(rest)
println(length([10, 20, 30]))  # 3

The first external | begins a new line deeper than the head; subsequent external pipes are aligned. Unbracketed nested match/case/switch/cond/function arms indent deeper than the external pipes. Parentheses and bracket bodies isolate nested boundaries. Keep the first RHS token on the = line; open [ there for a multiline body. Existing body-versus-array rules apply. Put where inside a branch bracket body. Same-line external pipes and bare group-wide where are not supported in this version. Guard steps and their result = may span lines; ordinary unguarded equations keep their existing line rules.

Falsey conditions and pattern mismatches try the next branch. Errors propagate; the first successful chain commits its body even when it returns none or an error. Effects are not rolled back. Branch bindings do not escape, and fresh let preserves closures made before a later shadow. Pins and pattern alternatives retain normal match semantics. No eligible clause at a supported arity still returns none. and/or and nested expression commas are unchanged; ; remains a statement separator, not guard OR. An old single-expression guard, including a scoped block expression, keeps its previous meaning.

In a bracket-body function, write indices tightly or group the guard: func first_positive(xs) when xs[1] > 0 [xs[1]] or func first_positive(xs) when (xs[1] > 0) [xs[1]]. A separated [ starts the body. An operator stranded after that body is diagnosed.

Detached signatures and refinements work on pipe groups. Inline typed/defaulted guarded heads are not added by this form. --typecheck visits the steps in branch scope; --infer types supported sequences and reports unsupported patterns. @infer and @strict check the observed return type as for ordinary functions. Clauses and match expressions remain evaluator-only; --vm refuses them. when/any and head-eliding repeated when are separate, unimplemented proposals.

Arity overloads — one name, several parameter counts

Clauses accumulate by name and arity, so a spelling may carry several independent functions. The idiom this exists for is the accumulator: a public one-argument entry point that seeds a private worker.

sum(l, acc) = match l with            # the worker — arity 2
  | []      => acc
  | [h | t] => sum(t, acc + h)
sum(l) = sum(l, 0)                    # the entry point — arity 1
sum([1, 2, 3])                        # → 6

The two are not clauses of one function that shadow each other; they are two functions, dispatched on argument count, and either may be called directly (sum([1, 2, 3], 10) → 16). Declaration order does not matter — the entry point may come first and call forward.

An exact arity match always wins over currying. With no overload, add(x, y) = x + y supplies too few arguments by returning a partial application (add(2)(3) → 5). When a clause of exactly that arity exists, it is dispatched instead — so adding e(x) alongside e(x, y) makes e(1) call the one-argument function rather than curry the two-argument one. Introduce a narrower overload only when you don't want the curried form for that count.

The ceiling is the widest arity declared for the name; more arguments than that is an error at every arity (no clause of 'e' accepts 3 argument(s)), and --typecheck reports it ahead of the run. A ...rest slot on any one of the overloads lifts the ceiling for the name entirely.

A same-arity redefinition replaces, and an annotated one says so. A parameter annotation (n :: Integer) is a contract on that parameter — it never chooses between bodies. So two heads of the same arity are one function defined twice, and the second wins, exactly as x: 1 then x: 2 leaves 2. When the two heads' annotations differ, both runtimes print a notice on stderr at the redefining line, naming both heads and the spelling that does dispatch:

func g(n :: Integer) ["int"]
func g(s :: String) ["str"]      # stderr: Warning: script.ax:2: `g/1` is redefined — a parameter
                                 #   annotation is a contract and does not select a clause, so
                                 #   `func g(s :: String)` replaces `func g(n :: Integer)`. To choose
                                 #   a body by type, guard it: `func g(s) when s is String [...]`.
g("x")                           # → "str"
g(5)                             # → type error: parameter s expects type String

The dispatching form is a guarded clause set — func g(n) when n is Integer ["int"] and func g(s) when s is String ["str"] accumulate, and g(5) → "int". Redefining a head with the same annotations, redefining an unannotated head, and adding an overload of a different arity all stay silent; the notice is for the one shape that reads as a method table and is not.

Return values — the last expression, and return

A function body returns its last evaluated expression — that is the native idiom, and most Axioma functions never write return at all. For early exits, return [value] is a statement (bare return yields none; in a :: Unit / -> Unit function it yields (), the same as omitting the return), and it unwinds through nested blocks and loops to the enclosing function:

func round_pil(x) [
    f: floor(x)
    if x == f then return f            # branch-position return (guard clause)
    else return floor(x + 0.5)
]

func classify_sign(x) [
    return "neg" if x < 0              # postfix guards — the Perl idiom
    return "zero" unless x != 0
    "pos"                              # fall-through: last expression
]

func find_first_even(xs) [
    foreach x in xs [
        if x == 0 then return x        # unwinds through the loop
    ]
    none
]

if c then return v is sugar for the block form if c then [return v] — byte-identical AST. Because return is a statement, it cannot appear in value position: x: return 5 is a SyntaxError (with a hint) — bind the value directly. A return at top level (outside any function) is a benign no-op; the return value must start on the same line as the keyword (a line break after return means a bare return). Under --vm, every function-level form compiles (the frame machinery already existed); top-level return stays evaluator-only.

Several results are one tuple. A function returns exactly one value, and Tuple is the product type — so write return (best, at) and destructure at the call site with a multi-assign: m, i = maximum(xs). The comma is a separator everywhere in Axioma (arguments, literals, comprehension clauses) — never an operator that builds values — so the bare spelling return best, at is a SyntaxError whose hint names the exact rewrite:

SyntaxError: 'return' takes one value
Hint: a comma list is not a value — to return several results, return one
tuple: `return (best, at)`. The call site destructures it: `a, b = f(...)`.

Contracts — requires / ensures / check f

A function's spec is data: the contract statement declares it next to the function, every later call enforces it, and check f verifies it over generated inputs. This is the function twin of the concept formation layer (concept X { purpose:, examples:, boundary: } + check X — § Concept formation), and the formal home of the accumulator-seed bug from the pitfall box: types cannot reject a well-typed wrong answer, but a postcondition can.

maximum: func(a) [
    best, at: a[1], 1
    for i, e in enumerate(a) [
        if e > best then [
            best = e
            at = i
        ]
    ]
    return (best, at)
]

contract maximum {
    purpose:  "Largest element of a non-empty array, with its 1-based position."
    requires: len(a) > 0
    ensures:  result[1] in a
    ensures:  forall e in a | result[1] >= e
    generate: func() [ map(func(k) [random(-99, 99)], range(1, random(1, 8))) ]
    trials:   200
}

maximum([8, 10, 23, 12, 5])   # (23, 3) — passing calls are unchanged
maximum([])                    # ERROR: contract violated: maximum requires
                               #   clause 1 (len(a) > 0)  +  an args: line
v: check maximum               # runs the trials → ⊤ᵇ (a Belnap verdict)

contract is a soft keyword — contract: value bindings, hash keys, and argument uses all keep working; the statement fires only in the exact shape contract name { … }. The braces are the declarative slot block (the concept surface), not an executable [ … ] body — a contract is declared metadata. Slots, all optional; requires:/ensures: repeat and conjoin:

Enforcement is always on for a contracted function — the cost is opt-in by declaring, and it survives rebinding, map/filter, and partial application (a partial defers checking to the eventual saturated call). Re-declaring a contract replaces it. Clauses evaluate in a child of the function's closure env, so they may call outer helpers. The contract attaches to the function object, so contract f must come after f is defined; multi-clause functions (func fib(0) [0] …) take one contract on the shared name, with pattern variables bound positionally (fib(0)/fib(n) ⇒ the contract's n sees the argument).

when guards vs requires. A guard selects among clauses — no clause matching is a legitimate outcome (none, the total-match rule). A requires clause rejects — calling outside the precondition is a loud, catchable Error. Both compose: guards route, requires polices.

check f — property verification. Runs the examples: first, then trials: draws from generate:; every input that passes requires: is applied and every ensures: clause evaluated. The verdict is a Belnap value, mirroring check Concept:

• ⊤ᵇ — every input passed (a ✅ --- CHECK PASS: summary prints);
• ⊥ᵇ — a counterexample or a call error was found; the first one stops the run and prints a report with the args:, result:, and how many inputs preceded it;
• ?ᵇ — nothing checkable: no contract, no input source, or every input was skipped by requires: (a generated input failing the precondition is discarded and counted, never a failure).

Generation runs under the ambient seeded RNG (fixed startup seed — § Randomness), so an unseeded check is reproducible run-to-run; call random_seed(…) first to vary the draws. Note the target parses like any check expression, so check f == x reads as check (f == x) — bind the verdict first (v: check f) to compare it.

check samples the effects: claim the same way it samples ensures. A function that declares effects: [] and then inserts fails the check (⊥ᵇ) and writes nothing — check writer and writer(1) now agree. A requires that queries the store is harness work, not a user write. When decreases: or effects: is present, the report adds a totality: line (postconditions / decreases / effects / exhaustive). The returned Belnap is still the postcondition axis: a missing Blue clause is ⊥ᵇ on that line and does not change check paint if every sampled ensures held. There is no total keyword.

Shrinking. A failing witness is minimized before it is reported: check greedily simplifies the counterexample — integers move toward 0, arrays and strings lose halves and single elements, one argument position at a time — accepting a simpler candidate whenever it still fails (any clause; the input must also still satisfy requires:, so shrinking never leaves the declared domain). The report's args: line shows the minimal witness and a shrunk from: (…) in N steps line shows the original draw:

❌ --- CHECK FAIL: bad_maximum ensures clause 1 (result[1] in a)
    args:   ([-1])
    shrunk from: ([-31, -74, -63, -10, -49]) in 6 steps
    result: (0, 0)

Shrinking is deterministic (no randomness) and capped at 500 candidate evaluations; when nothing improves, the line is omitted.

Input distribution — classify:. A passing suite can pass vacuously — the seed-bug lesson was that all-positive test data never exercises the interesting region. The classify: labeler makes the distribution visible: every input that runs is labeled, and CHECK PASS prints a census (percentages, largest first):

✅ --- CHECK PASS: maximum (0 examples + 200 trials)
    67% mixed · 19% all-negative · 15% non-negative

Auto-generation from :: annotations. When a contract declares no generate: and every parameter carries a supported scalar annotation — Integer, Float, String, or Boolean — check synthesizes the draws itself (integers and floats in ±100, strings of up to 8 lowercase letters, a fair coin), through the same seeded source as random. The summary says auto trials so the mode is visible:

inc: func(x :: Integer) [x + 1]
contract inc { ensures: result == x + 1 }
v: check inc        # ✅ --- CHECK PASS: inc (0 examples + 100 auto trials)

Containers are deliberately not auto-drawn (annotations carry no element type) — write a generate: for structured inputs. A partially annotated function keeps the ?ᵇ verdict, with the message pointing at both options.

Pre-state — old(). Inside an ensures: clause, old(e) denotes the value e had on entry to the call, so a postcondition can relate the result (or a mutated argument) to the pre-call state:

append_x: func(xs) [ push(xs, "x") ]
contract append_x { ensures: len(result) == old(len(xs)) + 1 }
append_x([1, 2])     # 3 elements — the clause compares against the ENTRY length

The capture is by value: every old(...) argument is evaluated before the body runs, and composite results (arrays, dictionaries, sets, tuples) are deep-copied, so an in-place mutation by the body cannot retro-edit the snapshot (Eiffel's old captures references and traps users exactly there; prefer scalar captures like old(len(xs)) when the whole collection isn't needed). old() takes exactly one expression and cannot nest; it is meaningful only in ensures: — in requires: the pre-state is the arguments. A binding named old in scope wins: the operator stands down and the call is ordinary code.

Termination — decreases:. The slot declares a termination measure over the parameters — an Integer that must be ≥ 0 and must strictly decrease on every recursive activation. The check is dynamic (the static discharge belongs to a future prove f), so it reports on the calls that actually happen — including self-tail-call iterations, which the tail-call optimizer runs in constant space where no recursion limit would ever trip:

fact: func(n) [ if n <= 1 then 1 else n * fact(n - 1) ]
contract fact { requires: n >= 0, decreases: n }
fact(5)              # 120 — measure 5 → 4 → 3 → 2 → 1

stuck: func(n) [ if n == 0 then 0 else stuck(n) ]
contract stuck { decreases: n }
try(stuck(3))        # catchable: … measure did not decrease (3 → 3)
                     #   (without the contract this tail loop spins forever)

The measure may be any Integer expression over the parameters (decreases: hi - lo for a shrinking span). A negative measure and a non-Integer measure are loud catchable errors. Under check f the measure stays live even while requires/ensures enforcement is suspended for the trials — so a generator that draws a non-terminating input turns the hang into a failed trial (⊥ᵇ with a shrunk witness). Mutual recursion is checked per function (each function's own measure across its own activations).

Declared effects — effects:. requires: and ensures: say what a function needs and what it promises. Neither says what it does, and a contracted function can write the fact store with its contract watching in silence. The effects: slot is where that gets declared:

save: func(n) [ insert("log", n) ]
contract save { requires: n > 0, effects: [kb] }

pure_calc: func(a, b) [ a + b ]
contract pure_calc { effects: [] }        # a real claim: neither effect

Three effect names, and the set is closed: kb covers fact assertion and retraction, grounding and truth metadata, and transactions; io covers file reads and writes; error covers producing an uncaught Error value (1 / 0, a missing slot, …). try(...) and error("…") (Caught) are data, not this effect. An unrecognized tag is refused rather than tolerated, because a tag that parsed but meant nothing would read like a declaration and promise nothing. The tags are bare words, not strings — effects: [kb], never effects: ["kb"] — and a single tag may drop the brackets (effects: kb). effects: [] is not the same as omitting the slot: it declares none of the three, where an absent slot declares nothing at all.

The kb half is enforced, and a violation refuses the write rather than reporting it:

relation r(x)
writer: func(n) [ insert("r", n) ]
contract writer { effects: [] }
writer(5)
# → ERROR: contract violated: writer declares effects: [] —
#          writing r(5) is a kb effect
#       permit: add kb to writer's effects, or move the fact write out of writer
{X | X <- r(X)}          # → {}   nothing was stored

Three properties make the declaration a guarantee rather than a comment. It is opt-in: a function with no contract, or a contract without the slot, is unconstrained, exactly as with decreases:. It covers the whole call context, not just the declaring body, so moving a write into an uncontracted helper does not escape it — while that same helper stays free when called from outside any declaration. And it catches every writing form, not only insert: assert, a bare relation call, forget, retract, the deontic and epistemic builtins, and the metadata writers — set_truth, cancel, challenge, and the transaction block — all reach it, including the form with no call expression at all —

q: func() [ forall x in [50, 51] | p(x) ]
contract q { effects: [] }     # refused; neither fact is written

which is why the check sits at the write rather than at the call.

Reading is not writing. A comprehension runs cleanly under effects: [], and so does a query over a recursive relation: forward chaining is lazy, so such a query materializes the closure into the store, but that write caches what the rules already entail rather than adding to them.

The io half covers the filesystem, in both spellings — the global write and the package io.write_file are one decision, and so are read, remove, read_csv/write_csv and the byte pair (to_json / from_json carry no tag: pure value↔︎string):

save: func(path, text) [ write(path, text) ]
contract save { effects: [] }
save("/tmp/x", "data")
# → ERROR: contract violated: save declares effects: [] —
#       calling write is an io effect

Reads count: a file read leaves the process, so effects: [] refuses read as surely as write. The two tags do not buy each other — effects: [kb] permits no file write, and effects: [io] permits no fact write. error is independent of both:

boom: func(n) [ 1 / n ]
contract boom { effects: [] }
boom(0)
# → ERROR: contract violated: boom declares effects: [] —
#          producing an Error is an error effect

Two exclusions are deliberate. Path helpers and metadata predicates — file_exists, is_file, file_size, join_path, base_name — open nothing and are not io, so a function may inspect a path under effects: []. And append splits on its first argument: append(array, elem) is the pure functional push and stays permitted, while append(path, text) is a file write and is refused.

The unary-dot fallback is covered as well: "/etc/hosts".read is refused under effects: [] exactly as read("/etc/hosts") is, while the fallback's effect-free use — 16.sqrt, "abc".len — is untouched.

The concept twin — invariant:. Concepts carry the instance-level counterpart: one invariant: <predicate> slot per concept block, open in slot names like boundary:, checked after instantiation and after every direct property write (dot assignment, compound assignment, and the x[attr -> val] frame form):

concept Account {
    balance: 0
    invariant: balance >= 0
}
acc: an Account { balance: 10 }   # checked at creation
acc.balance = 5                    # checked after the write — fine
poke: func() [ acc.balance = -1 ]
try(poke())          # catchable: concept invariant violated: Account (balance >= 0)
acc.balance          # 5 — the violating write REVERTED
try(an Account { balance: -3 })   # stillborn: no instance created, extent unchanged

A violating write is rolled back before the error returns, so the object never stays inconsistent (deliberately stronger than Eiffel's exception-leaves-object-dirty), and a violating creation is stillborn. Invariants are strict (invariant~: is rejected — spell conjunctions with and), inherit down extends chains (a child instance must satisfy its ancestors' invariants), and are error-loud: a predicate that fails to evaluate or returns a non-Boolean is itself a catchable error. Indirect writes — inverse-slot propagation, unify coreference merges, and Concept has default edits — are not invariant-checked in this round.

Proof instead of sampling — prove f. check f samples inputs; prove f decides contracts in a supported, explicitly typed runtime domain. Every parameter must be annotated Integer or Boolean. It hands the verification condition (requires ∧ result = body) implies ensures to the SMT solver, one ensures clause at a time. A discharged clause covers every scalar input of those types satisfying requires, subject to the limits below:

inc: func(x :: Integer) [ x + 1 ]
contract inc { requires: x > 0, ensures: result > x }
prove inc     # PROVE OK: covers the modeled Integer/Boolean scalar inputs

bad: func(x :: Integer) [ x + 1 ]
contract bad { ensures: result > 10 }
prove bad     # ❌ PROVE FAIL — counterexample: result = 10, x = 9

A refutation is a proof of failure, not an unlucky draw: the solver exhibits the input rather than stumbling on it. Inside ensures, old(e) is rewritten to e — in the verification condition the parameters already denote their entry values — so pre-state contracts prove without extra machinery. Branching bodies are in scope (if/else becomes a conditional term, with both arms required to have the same modeled runtime type). Parameter and result sorts are carried into the solver, including Boolean parameters used only in equality comparisons.

The verdict is Belnap, and the third value carries the weight: ⊤ᵇ discharged, ⊥ᵇ refuted, ?ᵇ not discharged. Not-discharged is never reported as refuted. Runtime Float arithmetic is not mathematical Real arithmetic: adding 1.0 to 1e20 rounds back to 1e20. Contracts over Float, broad Number, or unannotated parameters therefore return unknown. So do floating literals anywhere in the body or clauses, free closure values, and calls to helpers or builtins. An idealized solver interpretation cannot certify those runtime operations:

push_end: func(xs) [ push(xs, 1) ]
contract push_end { ensures: len(result) == old(len(xs)) + 1 }
prove push_end   # ?ᵇ - parameter domain and helper calls are not modeled
                #      (use `check push_end`, which runs the real ones)

inc_float: func(x :: Float) [ x + 1.0 ]
contract inc_float { ensures: result > x }
prove inc_float  # ?ᵇ - floating-point runtime arithmetic is not modeled

The admitted bodies are closed expressions over the parameters: exact integer addition, subtraction, multiplication by a constant, comparisons, Boolean operations, and conditionals. Preconditions and postconditions must be Boolean expressions in the same domain. In ensures, unshadowed old(e) is supported when its argument stays within the entry-value domain; nested snapshots and old(result) are refused. An explicit return annotation must match the modeled body type; return conversions are refused.

Multi-clause functions, lazy/variadic/patterned parameters, indexing, division, bounded forall e in a |, and nonlinear multiplication are also refused with a pointer at check. A parameter named result is refused because it conflicts with the postcondition result binding. Unknown is a limitation of this proof path, not a rejection of the function itself. Standalone [logic/smt | ...] and [logic/valid | ...] continue to reason over mathematical formulas, including exact SMT Real arithmetic; they do not certify floating-point program execution.

The verdict covers scalar values, not class descriptors or entity instances admitted by Axioma's broader concept-classification rules. For example, an Integer annotation can also admit the Integer concept itself at a runtime boundary; that reflective value is outside the SMT scalar model. The success message names this scope explicitly. These are postcondition proofs, not a guarantee that every possible call terminates or avoids runtime errors.

prove f is both a statement and an expression, so v: prove f binds the verdict exactly as v: check f does.

Functions as arguments — sub-contracts and blame. A function-valued parameter can carry its own contract in a nested block. Its clauses speak positionally — arg (or arg1…argN, and args) and result — because the contract's author does not choose the lambda the caller passes:

twice: func(f, x) [ f(f(x)) ]
contract twice {
    f: { requires: arg >= 0, ensures: result >= arg }
    ensures: result >= x
}
twice(func(n) [ n + 1 ], 5)      # 7

When one of these fails, the report names who is at fault, and the two directions are opposite. A sub-contract's requires failing means twice called the supplied function outside that function's domain — the callee is to blame. Its ensures failing means the function the caller supplied broke its own promise:

contract violated: twice's f ensures clause 1 (result >= arg)
    args:   (5)
    result: -95
    blame:  the caller of twice — the function it supplied for f
            broke that function's own promise

The incoming function is wrapped so the guard travels with the value: it still holds when the body passes it to map. Two consequences worth knowing: a wrapped function is a distinct object (identity comparison does not survive wrapping), and a recursive supplied function is guarded at its outermost call only, since its by-name self-calls reach the original.

Objects over time — stateful checking. A contract on a concept describes behavior across a lifetime rather than one call. check then runs random sequences of the listed operations against fresh instances, with the concept's invariant: as the oracle:

concept Account { balance: 0, invariant: balance >= 0 }
deposit:  func(acc, n :: Integer) [ acc.balance = acc.balance + abs(n) ]
withdraw: func(acc, n :: Integer) [ acc.balance = acc.balance - abs(n) ]

contract Account { operations: [deposit, withdraw], steps: 12, trials: 40 }
check Account
# ❌ --- CHECK FAIL: Account (stateful)
#     sequence (1 operation, shrunk from 2):
#       →  withdraw(1)
#     concept invariant violated: Account (balance >= 0)

The deliverable is the sequence, shrunk to the fewest operations that still break the object — an unshrunk twelve-step transcript is unreadable. Arguments after the receiver are drawn from the operations' :: annotations, so the same seeding and sizing rules apply. Each trial's instance is released afterwards, leaving the concept's extent exactly as it was. check Concept keeps its formation meaning (over examples: / counterexamples:) for every concept that declares no stateful contract — the stateful reading is chosen by declaring one, never inferred.

Sized generation. Generated inputs start small and grow across the run, so shallow bugs surface in the first trials instead of arriving as a large witness that then has to be shrunk. A generate: function opts in by taking one parameter:

contract sample { generate: func(size) [ random(0 - size, size) ], trials: 5 }
# sizes drawn: 1, 25, 50, 75, 100

A zero-argument generator is called exactly as before, so existing contracts draw identically. Auto-generation from :: annotations is sized too — magnitudes and string lengths follow the ramp, while Booleans do not (a coin has no magnitude). The size is a function of the trial index alone, never a draw from the random source, so seeded runs stay reproducible.

The seed-bug version of maximum (seeding best with 0) fails the membership clause on any all-negative input — maximum([-4, -2, -9]) errors at the call with result: (0, 0) in the report, and check maximum finds it in the first few trials. Evaluator-only: the contract statement and check f reject under --vm, and contracted functions called under --vm run without enforcement (the VM never consults the contract). Reference: doc contract, doc check, doc prove; tests: tests/axioma/contracts/ and tests/axioma/concepts/ for the concept invariant and stateful-checking files.

Anonymous functions

(lambda x => x * 2)(5)        # 10

Closures

makeAdder: lambda n => lambda x => x + n
addTen: makeAdder(10)
addTen(5)                     # 15

Closures also mutate captured state, with rebind — a plain assignment stops at the closure's own frame and would declare a local there instead. The counter idiom and the full scoping rules live in §3 Scoping & shadowing.

make_counter: func() [
  acc: 0
  func() [rebind acc: acc + 1
          acc]
]
c: make_counter()
c()  ;  c()                   # 2

Currying & partial application

multiply: lambda x => lambda y => x * y
double: multiply(2)
triple: multiply(3)

# User functions and operator prefix-calls both partial-apply:
add(x, y) = x + y
inc: add(1)                 # user function
map((+)(1), [1, 2, 3])      # operator prefix-call — same idea

Function composition

Composition wires two functions end to end: the output of one becomes the input of the next, and the pair behaves as a single new function. Because the result is itself a function, compositions nest without limit — that closure property is what makes point-free style possible.

Axioma ships both directions, deliberately distinct, because mathematics and pipelines read opposite ways and neither audience can be quietly overruled.

f: func(x) [x + 1]
g: func(y) [y * 10]

# ── left-to-right (pipeline order): f runs FIRST ──
compose(f, g)(3)     # → 40   the named form, n-ary
(f >> g)(3)          # → 40   the infix form

# ── right-to-left (mathematical order): f still runs first ──
(g ∘ f)(3)           # → 40   the glyph
(g << f)(3)          # → 40   its ASCII twin
(g `circ f)(3)       # → 40   the backtick digraph (`ring` also works)

The bridging identity, which holds in every spelling:

f >> g  ==  compose(f, g)  ==  g << f  ==  g ∘ f

Why two directions. On functions, f ∘ g universally means "apply g first" — a language that reversed the glyph would be wrong to every reader who learned it from a textbook. compose cannot follow the glyph, because it also composes relations, and a function is its graph: compose(R, S) is {(x,z) | (x,y) ∈ R ∧ (y,z) ∈ S}, left to right, which fixes compose(f, g) as x ↦ g(f(x)). Both readings are forced; neither is a preference. They are mirrors, not aliases.

Precedence. CALL binds tighter than every composition operator, so f >> g(3) reads f >> (g(3)). Write (f >> g)(3) to apply the composition — exactly as the parenthesisation works on paper.

Composed functions are values

normalize: trim >> lower                  # point-free: the argument is never named
map(normalize, ["  A ", "B  "])           # → ["a", "b"]

pipeline: compose(f, g)
map(pipeline, [1, 2, 3])                  # → [20, 30, 40]
{p: compose(f, g)}.p(1)                   # → 20    stored in a dict
twice: func(k) [compose(k, k)]            # returned from a function

The first stage receives every argument the composition was called with, so a pipeline may open from a multi-argument function; each later stage receives the single value its predecessor produced.

add: func(a, b) [a + b]
compose(add, g)(3, 4)                     # → 70   add sees both arguments

The degenerate arities

Composition has an identity element, so the empty and single cases are that element and that function — not errors. This is what lets a stage list be folded at any length, including zero.

compose()(7)                              # → 7    the identity element
compose(f)(3)                             # → 4    one stage is that stage
reduce(func(acc, s) [compose(acc, s)], compose(), [f, g])(3)   # → 40

Relations compose too

compose does double duty. On sets of pairs it is relational composition:

compose({("a",1), ("b",2)}, {(1,"x"), (2,"y")})   # → {("a","x"), ("b","y")}

The operators refuse sets on purpose. Relational R ∘ S has two incompatible conventions in the literature, so a glyph there would have to guess; compose is the spelling that commits to one in its name, and the error says so. Mixing a set with a function is a category error, not a coercion.

The surrounding combinators

flip(f) returns the swapped function (so it composes); flip(f, a, b) applies the swap immediately.

A flipped function partially applies, like any other function — an under-saturated call fixes what it was given and waits for the rest, so Haskell's (flip f) x idiom transfers directly. Once two or more arguments have arrived the callee receives them all in one call with the first two swapped (flip(f)(a, b, c) is f(b, a, c)), and a zero-argument call returns the function unchanged, matching f() on a user function. The closure also carries the callee's parameter list, swapped, whenever that shape is known — so reflection and partial have a real arity to work from:

sub: func(a, b) [ a - b ]
minus10: flip(sub)(10)          # fixes sub's SECOND argument to 10
minus10(3)                      # → -7    sub(3, 10)
flip(sub)(10, 3)                # → -7    the saturated spelling, same call
arity(flip(sub))                # → 2     the callee's arity, known
parameters(flip(sub))           # → ["b", "a"]   the callee's list, swapped

partial reaches builtin-backed callables too — a flipped function, a composed one, or a plain builtin — not only user functions. The residual carries the remaining parameter list when the callee's spec pins one (and makes no arity claim when it does not), and fixing more arguments than a known maximum is refused at partial() itself, where the mistake is:

partial(gcd, 12)(18)            # → 6
partial(flip(sub), 10)(3)       # → -7    the flip example, spelled via partial
partial(identity, 1, 2)         # ERROR — identity takes at most 1 argument

converge — branching and reconverging

Composition builds a chain. Real point-free code constantly needs a branch that reconverges — a mean is the sum and the length of the same input, divided. Without this the style collapses back to naming the argument just to mention it twice.

total:    func(xs) [reduce(func(a, b) [a + b], 0, xs)]
count_of: func(xs) [len(xs)]
div:      func(a, b) [a / b]

mean: converge(div, [total, count_of])
mean([2, 4, 6, 8])                        # → 5

Every branch receives the full argument list, so a fork can open from a multi-argument function. The branch list is an Array so the combiner stays in first position, matching map/filter/reduce.

on — the shape composition cannot express

cmp ∘ key would feed key's single result to a two-argument function. on applies the preprocessor to both arguments instead:

on(cmp, key)(a, b)  ==  cmp(key(a), key(b))

longer: on(func(a, b) [a > b], func(s) [len(s)])
longer("abcd", "ab")                      # → true

sort_by(key, coll) covers the common case for one verb; on generalises the key extraction to any binary function.

|> is not composition. It threads a value, so 3 |> f |> g is a one-shot computation with a 3 baked into it. f |> g computes g(f) — a type error, not a pipeline. Use compose(f, g) or f >> g when you want a function you can keep.

VM: the composition operators and the returning combinators (compose, pipe, curry, partial, flip, converge, on) are evaluator-only pending the VM parity effort. Each rejects under --vm rather than returning a wrong answer.

A full treatment — the history from group theory through the lambda calculus to modern functional languages, and how Axioma's surface compares — is in Function Composition in Axioma.

Map / Filter / Reduce

nums: {1, 2, 3, 4, 5}

map(lambda x => x * x, nums)                       # {1, 4, 9, 16, 25}
filter(lambda x => x > 2, nums)                    # {3, 4, 5}
reduce(lambda (acc, x) => acc + x, 0, nums)        # 15
sum(nums)                                          # 15  (works on arrays/sets/tuples)
Σ(nums)                                            # 15  (Unicode alias for sum)
mean((2, 4, 6, 8))                                 # 5   (array, tuple, or matrix; average is an alias)
median((3, 1, 2))                                  # 2   (even count averages the two middle values)

Enumerable verbs

The wider collection vocabulary, beyond map/filter/reduce/group_by. Every verb is collection-last, so it threads through the forward pipe |> with no _ hole (people |> max_by(...), xs |> each_slice(3)).

tally(["a", "b", "a"])                # → {a: 2, b: 1}   count occurrences (alias: frequencies)
words: ["hi", "hello", "hey", "yo"]
max_by(func(w) [len(w)], words)       # → "hello"        element with the largest key (argmax)
min_by(func(w) [len(w)], words)       # → "hi"           argmin; first-wins on ties; none if empty
sort_by(func(w) [len(w)], words)      # → ["hi", "yo", "hey", "hello"]   ordered by a derived key
sort_by(func(x) [x], [10, 2, 33, 4])  # → [2, 4, 10, 33] numeric-aware (not lexicographic), stable
flat_map(func(r) [r], [[1, 2], [3]])  # → [1, 2, 3]      map then flatten one level
flatten([[[1]], [[2]]])              # → [1, 2]          recursively descend Arrays
flat_map(identity, [[[1]], [[2]]])   # → [[1], [2]]       concatenate just one level
take_while(func(x) [x < 5], [1, 2, 9, 1])   # → [1, 2]   leading run while the predicate holds
drop_while(func(x) [x < 5], [1, 2, 9, 1])   # → [9, 1]   the complement
each_slice(3, [1, 2, 3, 4, 5, 6, 7])  # → [[1,2,3], [4,5,6], [7]]   consecutive fixed chunks
each_cons(2, [1, 2, 3, 4])            # → [[1,2], [2,3], [3,4]]      sliding windows
chunk([1, 1, 2, 3, 3])                # → [[1,1], [2], [3,3]]        group consecutive-equal runs
detect(func(x) [x > 3], [1, 2, 3, 4]) # → 4              first element matching (none if no match)
compact([1, none, 2, none, 3])        # → [1, 2, 3]      drop none (keeps om and everything else)
[3, 1, 2] |> sort |> tap(func(a) [println(a)])   # peek mid-pipeline, return the value unchanged

# the payoff — a readable left-to-right pipeline:
[5, 3, 8, 1] |> sort_by(func(x) [x]) |> take_while(func(x) [x < 6])   # → [1, 3, 5]

min_by/max_by return the element whose key is extremal (not the key value). sort_by shares sort's numeric-aware ordering, so integer keys sort by value. tally/frequencies return a dictionary (a string is counted character by character). Ruby's first-match is find/detect; find is a reserved solver keyword here, so the collection verb is detect. tap runs its function for a side effect and returns the value unchanged — handy for peeking inside a |> chain. All work under --vm.

List-library verbs (Haskell / OCaml)

The rest of the classic functional list library. Same function-first, collection-last shape as the Enumerable verbs, so they chain through |>.

zip_with(func(a, b) [a + b], [1, 2, 3], [10, 20])   # → [11, 22]      pairwise, truncates to shorter
scanl(func(a, x) [a + x], 0, [1, 2, 3])              # → [0, 1, 3, 6]  left fold, keeping every step
scanr(func(x, a) [x + a], 0, [1, 2, 3])              # → [6, 5, 3, 0]  right fold (f receives (x, acc))
iterate(func(v) [v * 2], 1, 5)                       # → [1, 2, 4, 8, 16]   first n of [x, f(x), f(f(x)), …]
iterate(func(v) [v * 2], 1)                          # → <generator>   the same sequence, unbounded and lazy
span(func(x) [x < 3], [1, 2, 3, 4, 1])               # → ([1, 2], [3, 4, 1])   (take_while, drop_while), one pass
separate(func(x) [x > 2], [1, 2, 3, 4])              # → ([3, 4], [1, 2])      partition by predicate
all?(func(x) [x > 0], [1, 2, 3])                     # → true          holds for every element (true on empty)
any?(func(x) [x > 2], [1, 2, 3])                     # → true          holds for some element (false on empty)
none?(func(x) [x > 5], [1, 2, 3])                    # → true          holds for no element (true on empty)

# unfold — the anamorphism, dual of reduce. The step returns Some((value,
# next_seed)) to continue or Absent to stop, using the built-in Option:
unfold(func(n) [if n > 5 then Absent else Some((n, n + 1))], 1)   # → [1, 2, 3, 4, 5]

scanl/scanr are the folds reduce/foldr with every intermediate kept (length n+1: scanl starts with the seed, scanr ends with it). span is exactly (take_while(p, xs), drop_while(p, xs)) computed in one pass; separate is partition under a different name (partition is reserved for concept partitions). all?/any?/none? short-circuit and read correctly in if.

The nine verbs above unfold work under --vm (byte-identical). unfold is evaluator-only: its step function builds Some/Absent, which are ADT constructors the VM does not compile, so an unfold under --vm is rejected at compile time rather than run.

Refinements — optional switches a function declares, in REBOL's model

A refinement is an optional switch on a function. It is declared in the parameter list, in every function form, as /word followed by the names it owns; it is invoked with a tight slash chain on the function's name; its owned names are passed by name inside the parentheses.

sum: func(a, b, /times amount) [ if times then (a + b) * amount else a + b ]
sum(1, 2)                          # 3  — inside, times is false and amount is none
sum/times(1, 2, amount: 10)        # 30 — times is true, amount is 10

copy2: func(xs, /part n, /deep, /reverse) [ [part, n, deep, reverse] ]
copy2/deep([1])                    # [false, none, true, false]
copy2/reverse/part/deep([1], n: 3) # [true, 3, true, true]   — any order
[9] |> copy2/part(n: 3)            # the pipe fills the positional slot; names ride along

The same declaration works on every form — func name(…), the equation head name(a, b, /times amount) = …, and an arrow lambda (a, /only) => … — and a list may open with a refinement: d: func(/deep) [ deep ].

The slash rule. Only a tight chain followed by ( is a refinement call: no whitespace on either side of any slash. Everything else is division, as it always was — x / y, n/d, x / q(2), x/(2 * y).

Refusals, never silent. An undeclared refinement (sum/nope(…)) is an error naming the declared ones; a used refinement whose owned name is missing (sum/times(1, 2)) is an error; an owned name without its refinement (sum(1, 2, amount: 10)) is an error. Multi-clause functions share one refinement set: the first clause to declare it fixes it, a later clause repeats it exactly or declares none and inherits it. signature(f) shows the declaration in order (func(a, b, /times amount)). Under --vm a refinement call refuses rather than answering from the positional arguments alone.

13. The Concept System

A concept is Axioma's central unit of knowledge representation — far more than an object-oriented class or record. Axioma's type names are concepts, but a concept is at once:

• a type name — the built-in primitives (Integer, Float, Set, Stack, …) and algebraic data types (data Shape = …) are first-class Concepts under the meta-concept DataType, so 5 is Integer, Integer is DataType, and x :: Day share one naming universe with any concept you declare;
• a frame — a named thing whose slots carry values and metadata (inverse, transitive, cumulative, cardinality), with an auto-maintained extent of its instances you can iterate like a set ({x | x <- Country}), and a concept↔︎relation↔︎rule duality;
• a description-logic concept — composable with ⊓ ⊔ ¬, ordered by subsumption ⊑ / ≡, with role restrictions (∃R.C, ∀R.C), Thing / Nothing (⊤ / ⊥), defined concepts, and partitions — all decided by a real ALC tableau reasoner (satisfiable, subsumption);
• a classifier — the is copula tests Russell's predication (∈, rex is Dog) and class inclusion (⊆, Dog is Animal); a defines predicate or a boundary turns membership into a rule, and every classification carries an epistemic grounding and may be defeasible;
• a designed, inspectable idea — the concept-formation layer (purpose, examples / counterexamples, formed_by, default_grounding) lets you state why a concept exists and check that it does its job — and an invariant: slot guards every instance's integrity at creation and on every property write (see The concept twin — invariant: under §Functions Contracts).