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

= 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 let or :=. Bind with : (canonical) or =. Writing let x = value or x := value is a syntax error with an inline hint pointing at x: value.

Three ways to introduce a name

: is the canonical value binding; two further keywords introduce a name lazily. They differ in when the right-hand side runs and what they can name:

x: 1 + 2                                  # eager — computed now
declare big = slow_query()               # lazy — runs on first read of `big`, then cached
define concept Point = { x: 0, y: 0 }    # a definition, not a value

: evaluates now; declare and define defer until the value is first needed and then reuse the cached result. Beyond that, declare adds the persistence refinements, while define is the gateway to the definition / speech-act family — define concept / define axiom / define postulate / define theorem / define word / define dialect (see §13).

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.

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, …) 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.

Regression pins: tests/axioma/binding/test_scoping_shadowing.ax.

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     # Saved to .axioma_session.bin
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 :. 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. --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.

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

Dual null types

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

none == om             # false — never interchangeable
if none then ...       # never executes
if om   then ...       # never executes (om is falsy)

Operational rule: none/null means absence; om/Ω means an explicit undetermined value. They compare differently and have different truthiness. Because om is falsy — it folds onto the designation law, so designated(om) is false and a bare if om then … runs the else branch — if/while/filter read om as absence. To branch on undeterminedness as a VALUE, test explicitly with == om (or is om). This makes om agree with the typed Kleene unknown ?ᵏ, which it equals and which is likewise falsy by designation (if ?ᵏ also takes the else-branch; see §9).

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 ("…") or single quotes ('…'). They 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.

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}"

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".

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): out-of-range bounds clamp ("hello"[5:10] → "o", xs[2..9999] → the tail) and a reversed window yields the empty value ("hello"[4:2] → "", a[2..1] → [] — 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.
• 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), and v is T all match).

type(https://example.com)   # → "URL"
type($123.45)               # → "Money"
type(100x200)               # → "Pair"
type(42%)                   # → "Percent"

is_url(https://example.com) # → true
is_pair(100x200)            # → true
is_url($5)                  # → false

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). # + digit is an Issue (#123), # + letter is a QuoteWord (#hello).

Arithmetic on Pair / Money / Percent

100x200 + 20x30   # → 120x230   (component-wise)
100x200 * 2       # → 200x400   (scalar scale)
$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.)

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, #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)
#tag              # → #tag      (quote-word — a literal symbol)

:x is the get-word; @x is not. @ is the type-of sigil, so @x returns "Integer" (the type of x), while :x returns 42 (the value). Use :x to read a value without evaluating it as a call.

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.

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.
• Deletion is remove(path), not delete(...) — delete is the reserved retract keyword.
• 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

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

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
remove_at([10, 20, 30], 1)       # → [20, 30]           table.insert/remove,
remove_at([10, 20, 30], -1)      # → [10, 20]           FUNCTIONAL (a new
                                 #   array; the input is untouched, the
                                 #   push contract; read the element first
                                 #   with xs[pos] — pop returns elements)

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 null — 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             # → null     (empty: no crash — check xs.empty first)
[99].second          # → null     (out of range → null, 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

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])}

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.
• 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 → null (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 is strictly unary. A multi-argument builtin surfaces its own arity error (xs.push → "push requires 2 arguments…"), and x.f(a) means (x.f)(a), never f(x, a) — for multi-argument calls use function position (contains(xs, 2)) or the pipe's hole (xs |> contains(_, 2)). A name bound to a non-callable errors; a name that resolves to nothing raises the familiar miss error, which now ends "…, or any unary operation in scope". Variadic operations are unary-callable, so they participate (xs.max → 5, the fold reading; "abc".max → "abc", max-of-one). The dot spelling has full --vm parity.

Tuples

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

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)

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)
dict()               # Empty dictionary  ({} is the empty SET ∅)

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

A dictionary is a string-keyed {key: value} map. Build one with the {...} literal or, for the empty case, dict(). 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.

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)

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; df_groupby(df, cols) buckets rows. (For plain in-memory grouping of arrays/hashes, group_by in §7 needs no DataFrame at all.)

6. Operators & Control Flow

Arithmetic

2 + 3       2 - 3       2 * 3       6 / 3       7 % 2       2 ^ 10
100 // 7    10.0 // 3.0                                     # INT_DIV (floor)

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

100 // 7      # → 14   (symbolic)
100 div 7     # → 14   (keyword)
quotient(100, 7)   # → 14   (prefix)

100 % 7       # → 2    (symbolic)
100 mod 7     # → 2    (keyword)
100 modulo 7  # → 2    (keyword longhand)
remainder(100, 7)  # → 2    (prefix)

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

/ vs // for floats. / preserves operand kind (int/int → int truncated; float/float → float real value); // always returns an integer-valued result via Go-native truncation (ints) or math.Floor (floats). The two differ for all float cases and for negative-result float 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 // 3.0   # → -3         (floor toward -∞, NOT -2)

mod / modulo / div 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).

Comparison

==   !=   <   >   <=   >=
3 ≤ 5         # glyph twin of <=  (≥ for >=; ≠ for !=; slanted ⩽ ⩾ also lex)
0 ≤ x < 10    # ordering comparisons CHAIN: ⇒ (0 ≤ x) and (x < 10)

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

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.

~ is not negation — the tilde family map

Negation is spelled not / ¬ only. 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")
]

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

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

# ── 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

# `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) ]

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.

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

1. Function application: f(x)
2. ^ (exponent), not, & (address), * (deref)
3. unary - (negation)
4. *, /, %, //, mod, modulo, div
5. +, -
6. Set: union, intersect, difference
7. Comparison: <, >, <=, >=, ==, !=, subset, in, is
8. and
9. or, xor / ⊻, ⊼ (nand), ⊽ (nor)
10. implies, iff
11. |> / |?> (forward pipe & error-propagating pipe — loosest; left-associative)

Associativity. ^ / ** / .^ (exponentiation) are right-associative, matching standard math convention: 2 ^ 3 ^ 2 is 2 ^ (3 ^ 2) = 512, not (2 ^ 3) ^ 2 = 64. Every other infix operator (+, -, *, /, %, …) is left-associative.

Unary minus binds looser than ^. Negation sits below exponentiation in the table above, so -2 ^ 2 parses as -(2 ^ 2) = -4, not (-2) ^ 2 = 4 — again the math-textbook reading. Parenthesize the base ((-2) ^ 2) to negate first. It still binds tighter than *//, so -2 * 3 is (-2) * 3.

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.

complex(3, 4) + 1/2      # 3.5 + 4i     — Rational embeds
complex(3, 4) + byte(2)  # 5 + 4i       — so does Byte
complex(0, 1) ^ 2        # -1           — exactly, not -1 + 1.2e-16i
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.

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

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.

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

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

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 that runs at most once, when you force it.

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 an ObjectMap 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 DO apply (cap output cardinality), but the slice is taken in Go-map iteration order — non-deterministic. Use list comprehensions for deterministic paging.

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

Epistemic logic

knows("alice", p)              # K_alice p — Alice knows p
believes("bob", p)             # B_bob p
common_knowledge(p, agents)    # CK p among agents

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
multiply: func(a, b, c) [a * b * c]   # canonical REBOL bind
func double(x) [x * 2]             # named declaration (optional keyword form)
double(x) = 2 * x                  # EQUATION form — same function, no keyword

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.

double(x) = 2 * x                  # ≡ func double(x) [x * 2]
fact(0) = 1                        # literal-pattern clause …
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) = 0                        #   (Haskell's own guard order, spelled `when`)
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/default/named parameters stay on the func spelling); a capitalized parameter is a nullary constructor pattern, not a binder — the same rule func f(X) […] and match follow; 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 (pair(X, Y)), rules may drop rule before :-/whenever, and functions may drop func before =.

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), 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 (om, 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.

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

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 all of them. It hands the verification condition (requires ∧ result = body) implies ensures — one ensures clause at a time — to the SMT solver, so a verdict covers every input at once:

inc: func(x) [ x + 1 ]
contract inc { requires: x > 0, ensures: result > x }
prove inc     # ✅ PROVE OK: inc (1 ensures clause discharged for ALL inputs)

bad: func(x) [ 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, its two arms sort-unified).

The verdict is Belnap, and the third value carries the weight: ⊤ᵇ discharged, ⊥ᵇ refuted, ?ᵇ not discharged. Not-discharged is never reported as refuted. Calls to helpers and builtins are uninterpreted in the solver — it may read len however it likes — so a counterexample involving one is an artifact of a missing definition, not evidence your contract is wrong:

push_end: func(xs) [ push(xs, 1) ]
contract push_end { ensures: len(result) == old(len(xs)) + 1 }
prove push_end   # ?ᵇ — `len`, `push` have no definition in the solver
                 #      (use `check push_end`, which runs the real ones)

Multi-clause functions, indexing, bounded forall e in a | and nonlinear * are refused by name with a pointer at check. 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)

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.

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)

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
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 None to stop, using the built-in Option:
unfold(func(n) [if n > 5 then None 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/None, which are ADT constructors the VM does not compile, so an unfold under --vm is rejected at compile time rather than run.

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 types are concepts, but a concept is at once:

• a type — the built-in primitives (Integer, Float, Set, Stack, …) are themselves concepts, so 5 is Integer and x :: Day run the same machinery as 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).

The surface is natural language throughout — concept Stock, Stock has price, rex: a Dog, rex is Dog, Dog extends Animal. The rest of this section works through each of these dimensions; together they make concepts the substrate of Axioma's knowledge representation and its cognitive paradigm.

Defining concepts

Axioma has two canonical concept-declaration surfaces:

There is a single canonical creation surface — the keyword-first concept X form. It absorbs four feature slots that were previously distributed across multiple competing forms:

• bare: concept X
• with postfix doc string: concept X "doc"
• with prefix refinement: concept/persist X, concept/transient X, concept/system X
• with refinement + doc: concept/persist X "doc"
• with slot-defaults block: concept X { slot: default, ... }
• with refinement + block: concept/persist X { ... }
• namespaced: concept FinKB.Stock, concept/persist FinKB.Bond "doc"

concept Stock                                   # bare concept creation
concept Stock "A financial instrument"          # with postfix doc
concept Stock {                                 # with initial slot defaults
  price: 0
  ticker: ""
}
concept/persist Stock                           # force KB persistence
concept/transient Scratch                       # never persist
concept/system InternalRegistry                 # mark as system-internal
concept/persist Stock "force-persist regardless of mode"

Stock extends Asset                             # specialize Stock as a subclass of Asset
apple is Stock                                # classify apple as a Stock (predication)

The keyword-first form pairs naturally with the rest of Axioma's speech-act family (define, axiom, postulate). is remains the canonical operator for instance classification (apple is Stock) and Boolean type queries (x is Stock in expression position).

Doc strings are also accepted inside the block form:

concept TreasurySec { doc: "A marketable US Treasury security" }
concept TreasurySec "A marketable US Treasury security"
TBill extends TreasurySec "Treasury bill, max 365 days"
TreasurySec has issuer: "US Treasury"
TBill has max_maturity_days: 365

Name-inference form — an anonymous concept { ... } literal on the RHS of a : binding picks up its name from the LHS identifier. The resulting Concept is fully named and behaves identically to concept X { ... }:

Widget: concept { price: 0, ticker: "" }      # name inferred from LHS
Gadget: concept { color: "red", count: 5 }
Foo: concept FooBar { rate: 0.05 }            # explicit RHS name wins; Foo aliases FooBar

Casing rule (enforced): the inferred name must start with an uppercase letter — the same isValidConceptName check every other concept-creation surface uses. tc: concept { ... } errors with concept name 'tc' should start with an uppercase letter. Use TC: concept { ... }. The bare-RHS form is also the only form that infers a name; anonymous concept { ... } literals nested inside a call argument or array element error cleanly at eval time.

Creating concepts — the canonical surface. A concept is created with the keyword-first concept form. There is no create-prefixed, postfix, or is Concept creation form:

concept Stock                       # bare
concept Stock "doc"                 # with a doc string
concept/persist Stock "doc"         # with a /persist | /transient | /system refinement
concept Stock { price: 0 }          # block form with slot defaults
concept FinKB.Stock "doc"           # namespaced
x: a Stock                          # instance creation, via the indefinite article
Stock extends Asset                 # class inclusion ⊆
Stock has price: 150                # property (auto-creates Stock on first verb use)

is is a predication operator, never a creation one — using it to create a concept would conflate two speech acts (constitutive declaration vs. descriptive predication, the distinction Russell draws on the copula). So aapl is Stock classifies an instance, X is Concept (in expression position) asks "is this a registered concept?", and a statement-level Stock is Concept is a parser error pointing at concept Stock.

Define-family form (define concept) — fills the typed-define slot left open in the existing family of define axiom / define postulate / define theorem / define word / define dialect:

define concept Stock = {                       # `=` assignment
  price: 0,
  ticker: ""
}

define concept Bond: { yield: 0.05 }           # `:` assignment
define concept Scratch = {}                    # empty body — bare creation
define/persist concept Pinned = { x: 1 }       # refinement: force-persist
define/transient concept Tmp = { x: 1 }        # refinement: skip persistence

Syntactically parallel to define dialect: uppercase name, { ... } body parsed as a hash literal. The implementation synthesizes an internal ConceptCreation AST and delegates to the canonical creation pipeline, so every formation-layer feature (boundary capture, examples auto-classification, formed_by cross-map, default-grounding cross-map, KB persistence) carries through transparently. Behaves identically to the equivalent concept Stock { ... } on every dimension except syntax.

Mapping to the rest of the family:

v1 limitations:

• Inheritance: no extends / is slot inline. Follow up with Stock is Asset on the next line, or use concept Stock extends Asset { ... } if you need it co-located.
• Defeasible boundary: the ~ suffix on hash-literal keys is not parsed (define concept Sage = { boundary~: ... } will fail). Use the canonical concept Sage { boundary~: ... } block form, or follow up with the statement-level Sage defines~ { ... } rule.
• Namespaced names: define concept FinancialKB.Stock = ... is not supported (the define parser produces a flat []*Identifier symbol list). Use the prefix concept FinancialKB.Stock { ... } for namespaced concepts.

Tests: tests/axioma/concepts/test_define_concept.ax (happy paths) and the three matching _reject files (lowercase, /unpersist, non-hash body).

Concept introspection at every level — what is checks depends on syntactic position:

• <Name> is Concept at statement level (TitleCase LHS) → parser error (use concept X [doc] [refinement] to create a concept)
• <Name> is <Parent> → declares a specialization (class-inclusion ⊆)
• <instance> is <Concept> → classifies the instance (membership ∈) — canonical
• <expr> is <C> in expression position → Boolean predication query — canonical (including X is Concept as a "is this a registered concept?" query)

Inheritance

concept Animal
Dog extends Animal
Dog has bark: lambda => println("Woof!")

Concept formation layer (Phase 1)

Three slot names on a concept carry first-class concept-design semantics. They turn concept Foo { ... } from a plain class declaration into a contract that pairs prose intent with executable regression tests over the extent.

concept CFP_Choice                              # base concept for entities
positive_a: a CFP_Choice {}
positive_b: a CFP_Choice {}
negative_a: a CFP_Choice {}

concept DecisionFatigue
df1: a DecisionFatigue {}
df2: a DecisionFatigue {}

DecisionFatigue has purpose: "Explain degraded choices after repeated decisions"
DecisionFatigue has examples: [df1, df2]
DecisionFatigue has counterexamples: [negative_a]

check DecisionFatigue   # → ⊤ᵇ  (contract holds)

The four reserved slot names:

The formed_by: enum accepts five string values. As of Phase 2b-1 the cross-map is automatically derived into a default_grounding slot at concept-creation time, and as of Phase 2b-2 the derived grounding is actively applied to stored is-facts at instance-creation and classification time:

concept Monoid {
  purpose: "Algebraic structure with associative binary op and identity"
  formed_by: "stipulation"
}

concept Smartphone {
  purpose: "Phone + computer + camera + internet, unified"
  formed_by: "combination"
}

Invalid values are rejected at creation time:

ERROR: concept 'X': formed_by = "stipulashun" is not a recognized creation mode.
Use one of: abstraction, combination, distinction, stipulation, metaphor

The contract is verified by check Concept (the existing automated-reasoning check keyword, specialized for Concept targets). It returns a Belnap B4 value:

check on a non-Concept target falls through to the legacy AutomatedReasoningObject wrapper (check 42 still returns the generic consistency-check string).

Phase 2b-2 adds the boundary: slot and the active application of default_grounding. A boundary: value is a predicate, not an open expression — it captures the AST before the property eval loop runs and registers it as a defines classifier scoped to the concept:

concept P_Person
P_Person has age: 0
P_Person has name: ""

concept P_Adult {
  formed_by: "stipulation"      # → default_grounding: "axiom"
  boundary: age >= 18 and is P_Person
}

alice: a P_Person {name: "Alice", age: 30}
println(alice is P_Adult)                          # → true (auto-classified)
println(grounding("isa", alice, P_Adult))            # → "axiom"

The stored is-fact inherits axiom grounding (not the strict-defines default of theorem) because Stipulation-formed concepts cross-map to axiom. The same active-grounding flow fires at object-instantiation time:

concept P_Stock { formed_by: "stipulation" }         # default_grounding: "axiom"
aapl: a P_Stock {}
println(grounding("isa", aapl, P_Stock))             # → "axiom"

The instance-creation is-fact is gated: a concept without formed_by: (or explicit default_grounding:) keeps the pre-2b-2 behavior — the instance is registered in concept.Instances for comprehension iteration, but no synthetic is-fact is stored. This preserves the legacy corpus verbatim.

Phase 3 closes the loop on the Phase 1 contract by making examples: load-bearing. When the concept has opted into the formation layer (default_grounding set, either via formed_by: cross-map or explicitly), the examples: slot is treated two different ways depending on whether a boundary: predicate is present:

• No boundary — examples become the extent declaration. Each entity in the list is force-classified as a member of the concept, at the inherited default_grounding. Useful for small enumerated concepts that are easier to list than to describe with a rule:

  concept VIP {
    formed_by: "stipulation"        # → default_grounding: "axiom"
    examples: [alice, carol]        # auto-classified as VIPs
  }
  println(alice is VIP)                          # → true
  println(grounding("isa", alice, VIP))            # → "axiom"
  println(check(VIP))                             # → ⊤ᵇ (trivially)

• With boundary — the boundary owns membership; examples become test cases for the boundary. check Concept verifies the boundary classifies every listed example and rejects every counterexample:

  concept Adult {
    formed_by: "stipulation"
    boundary: age >= 18 and is Person
    examples: [alice, carol]        # both ≥ 18 → boundary agrees
    counterexamples: [bobby]        # < 18 → boundary correctly rejects
  }
  println(check(Adult))             # → ⊤ᵇ (boundary agrees with examples)
  
  concept AdultBad {
    formed_by: "stipulation"
    boundary: age >= 18 and is Person
    examples: [dave]                # dave is 8 — boundary disagrees!
  }
  println(check(AdultBad))          # → ⊥ᵇ (example missing from extent)

Counterexamples are never auto-classified — there's no opponent rule to push against. They still participate in check's negative verification (no counterexample may be in the extent).

Phase 4 adds the defeasible boundary form: boundary~:. The tilde parallels the statement-level defines~ and marks the membership rule as defeasible — classifications derived from it cap at conjecture-grade, even on a stipulation-formed (axiom) concept. This expresses a coherent two-level epistemic stance: the concept itself is definitional, but specific memberships derived from an uncertain rule remain tentative.

concept Sage {
  formed_by: "stipulation"          # concept is axiom-grade
  boundary~: age >= 65 and wisdom >= 70 and is Person
}

alice: a Person {age: 70, wisdom: 80}
println(alice is Sage)             # → true
println(grounding("isa", alice, Sage))   # → "conjecture" (cap fires)

The cap rule: defeasibility lowers grounding to conjecture when the concept's default_grounding is stronger (axiom, postulate, theorem). When already weaker (hypothesis, datum), the value passes through unchanged. Declaring both boundary: and boundary~: on the same concept is rejected at creation time.

See tests/axioma/concepts/test_concept_formation_phase1.ax for the contract test matrix, tests/axioma/concepts/test_concept_formation_phase2b2.ax for the boundary + active-grounding tests, tests/axioma/concepts/test_concept_formation_phase3_examples.ax for the examples-auto-classification tests, and tests/axioma/concepts/test_concept_formation_phase4_defeasible_boundary.ax for the defeasible-boundary tests.

Phase 5 surfaces the formation layer as queryable data via the concepts_formed_by(mode_string) builtin. Returns an array of every concept whose formed_by: slot equals the given mode, validating the mode against the same enum used at creation time:

concept Monoid  { formed_by: "stipulation" }
concept Group   { formed_by: "stipulation" }
concept Penguin { formed_by: "distinction" }

len(concepts_formed_by("stipulation"))   # → 2
stips: concepts_formed_by("stipulation")
println(stips[1].formed_by)              # → "stipulation"

concepts_formed_by("stipulashun")        # → ERROR (typo rejected,
                                         #   same enum as Phase 2a)

The return value is a plain Array<Concept>, so it composes with comprehensions, len, and the rest of the array vocabulary. Useful for KB audits and for tooling that wants to render formation-layer choices.

Instances

usa: a Country {}
china: a Country {}
alice: a Person {name: "Alice", age: 30}

Property access

alice.name                    # Dot
alice's name                  # Possessive
alice[name -> "Bob"]          # ErgoAI frame-form (returns "Bob")

is predicate

alice is Person              # true
{X | X is Country}           # All instances of Country
{X | X is Country, X.gdp > 20000}   # With filter

Cardinality constraints

cardinality(Country, "capital", 1, 1)    # Exactly one capital per country

Concept introspection

Stock show properties
Concept display hierarchy

KM-style surface syntax

Four ergonomic forms adopted from Peter Clark & Bruce Porter's KM 2.0 (The Knowledge Machine). Each composes with the existing concept system above and adds no new semantic machinery — they are surface forms over the canonical ObjectInstantiation AST node, concept-level has, and the existing it keyword.

Instances are created with the natural-language a / an / entity forms (a Stock {}, an Item {}, entity Gadget {}) — all three produce the same AST and runtime value. There is no object keyword.

Indefinite-article instance literals — a Concept {props} and an Concept {props} are the canonical instance-creation expressions. The property block is optional. The article is a soft keyword: it only triggers when followed by a capitalized identifier (Axioma's concept convention), so variables named a or an continue to work.

mycar: a Car {make: "Toyota", price: 26000}
cat: an Animal {species: "Felis catus"}
cheap: a Car {}                    # empty-property form
dyn: (a Car {price: 99999}).price  # usable mid-expression
fleet: [a Car {price: 10000}, a Car {price: 20000}]

it anaphora — every fresh instance binds it in the surrounding scope, so subsequent statements can refer back to it without naming. Method-self semantics (when it is bound inside an object action) take precedence; the global binding only fires between consecutive top-level statements.

a Car {make: "Toyota", price: 26000}
println(it.make)            # Toyota
mycar: it              # capture by name
a Car {make: "Honda"}       # rebinds it
println(it.make)            # Honda
println(mycar.make)         # Toyota (unchanged)

every Concept has prop: val — universal-slot quantifier; sugar for the existing concept-level has. Useful when emphasizing intent in literate-style scripts.

every Car has wheels: 4
every Car has make: ""
c: a Car {make: "Toyota"}
println(c.wheels)           # 4 (inherited default)

what is X? / what is X's Y? — interrogative queries. Evaluates the operand, pretty-prints <source> is <value>, and returns the value (so it can be assigned). The trailing ? is required. Slot access via either possessive ('s) or dot notation is accepted.

mycar: a Car {make: "Toyota", price: 26000}
what is mycar?              # → mycar is a Car {make: "Toyota", price: 26000}
what is mycar's price?      # → mycar's price is 26000
what is mycar.make?         # → mycar.make is "Toyota"

KM influence note: Axioma already implements most of KM's deep semantic machinery (frames, inheritance, situations via hypothetical contexts, defaults via defeasible rules, reification, persistence) and goes beyond it on truth representation (B4 bilattice, six-level epistemic grounding, five logic kinds with automatic dispatch). The natural-language surface forms above bring KM's ergonomics in alongside that deeper machinery. See tests/axioma/km/ for the complete test set.

Coreference merging — unify x with y

Collapses two named entities into one canonical entity with the union of their slot values. Solves entity resolution — when "Acme Inc." and "Acme Industries" turn out to be the same company, unify merges them in place. Composes with B4 paraconsistent truth, six-level grounding, and atomic transactions.

concept CelestialBody
morning_star: a CelestialBody {visible_at: "dawn"}
evening_star: a CelestialBody {visible_at: "dusk"}

unify morning_star with evening_star          # Russell's classical case

println(morning_star == evening_star)         # → true

Defeasible: unify~ x with y records the merge with grounding conjecture (cancellable later).

B4 paraconsistent slot merging: conflicting single-valued slots keep the canonical's value and record a Both truth marker. Multi-valued slots get set-unioned.

Transaction-safe: unify inside transaction_begin() / transaction_rollback() is reversible — both entities' pre-merge slots and identity are restored.

Intensional class descriptions — the Concept where <pred>

A Russell-style definite description with restrictor (KM §18.2). the Stock where price > 1000 denotes the anonymous class of Stocks whose price exceeds 1000. Composes with is, comprehensions, and named classes.

concept Stock
Stock has price: 0
luxury: a Stock {price: 80000}

big: the Stock where price > 1000
println(luxury is big)                        # → true

# Inline membership test
println(luxury is (the Stock where price > 50000))   # → true

# Comprehension over the implicit extent
bigs: {X | X is (the Stock where price > 1000)}

Bare slot names in the predicate resolve to it.<slot> (same convention as defines predicate bodies). The intensional class is transient — it's not registered in the KB, so it adds no permanent vocabulary; use it for one-off queries or as a slot value when you want to denote a class without naming it.

Partitions and subsumption

Concept partition Member1, Member2, … declares the listed subclasses as mutually exclusive. An instance can be a member of at most one. The disjointness is enforced by auto-classification — when a defines predicate would classify an instance into a partition member that conflicts with an existing membership, the new classification gets the Belnap both truth value (paraconsistent — no crash).

concept Animal
Bird extends Animal
Mammal extends Animal
Fish extends Animal

Animal partition Bird, Mammal, Fish

robin: a Bird {}
println(robin is Mammal)        # → false (disjoint)

A subsumes B is the class-class subsumption infix (Russell class- inclusion, KM §18.3) — true when A is a superclass of B.

Animal subsumes Bird             # → true
Concept subsumes Bird            # → true
Bird subsumes Mammal             # → false

partitions_of(Concept) returns the declared partition tuples on a concept.

Querying a partition's live extent

Four builtins make the partition laws — disjointness and exhaustiveness — queryable over a concept's actual instances, returning witness instances (not just a verdict) when a law fails:

concept Thing
UpToUs extends Thing
NotUpToUs extends Thing
Thing partition UpToUs, NotUpToUs
opinion: an UpToUs {}
weather: a NotUpToUs {}

is_partitioned(Thing)            # → true   (disjoint AND exhaustive over the extent)
partition_overlap(Thing)         # → {}     (instances in >1 part — empty ⇔ disjoint)
partition_gap(Thing)             # → {}     (extent instances in 0 parts — empty ⇔ total)
partition_member(opinion, Thing) # → UpToUs (the part it falls into, or `none`)

mystery: a Thing {}              # a bare Thing — in neither part
is_partitioned(Thing)            # → false  (exhaustiveness now fails)
mystery in partition_gap(Thing)  # → true   (the gap WITNESS)

This models Epictetus' dichotomy of control as a real partition rather than two hand-rolled relations. Each verdict is open-world — a statement about the facts seen so far; an empty extent is vacuously partitioned.

Description Logic — concept algebra ⊓ ⊔ ¬ ⊑ ≡ + satisfiable

Concepts compose into compound concept expressions with the DL operators, and a built-in tableau reasoner answers subsumption, equivalence, and satisfiability questions about them. ⊓ (and) and ⊔ (or) and ¬ (not) build a first-class ConceptExpr value; ⊑, ≡, and satisfiable(...) decide.

concept Person
concept Student
concept Employee
Student extends Person
Employee extends Person

ws: Student ⊓ Employee           # a compound concept (intersection)
@ws                              # → "ConceptExpr"

Student ⊑ Person                 # → true   (subsumption: left is the SUBconcept)
Person ⊑ Student                 # → false
(Student ⊓ Employee) ⊑ Person    # → true   (tableau derives it from `extends`)
Student ⊑ (Student ⊔ Employee)   # → true

Student ≡ Employee               # → false  (equivalence = mutual subsumption)
(Student ⊓ Employee) ≡ (Employee ⊓ Student)   # → true

satisfiable(Student ⊓ Employee)  # → true
satisfiable(Student ⊓ ¬Student)  # → false  (the complement clashes)

⊑ vs subsumes — converse readings. The glyph ⊑ reads in the standard DL direction (C ⊑ D means C is the more specific subconcept — Student ⊑ Person is true). The English word subsumes reads the other way (A subsumes B means A is the more general superclass — Person subsumes Student is true). They are converses of the same relation; pick whichever reads naturally.

¬ / not is type-dispatched: applied to a concept it builds the complement; applied to a boolean it is ordinary logical negation, unchanged. satisfiable reasons over the TBox assembled from extends declarations; it is for concepts — boolean/propositional formulas use the separate is_satisfiable.

The reasoner is the ALC tableau in reasoner/.

Role restrictions, partitions, and extensional membership

A role restriction quantifies a concept over a binary relation (a role). Use the COLON form ∃role: Concept (some filler is a Concept) and ∀role: Concept (every filler is a Concept); the role is a native relation.

concept Doctor
concept Cardiologist
Cardiologist extends Doctor
relation hasChild(x, y)

g: ∃hasChild: Doctor                                      # a ConceptExpr (prints ∃hasChild.Doctor)
satisfiable((∃hasChild: Doctor) ⊓ (∀hasChild: ¬Doctor))  # → false  (a filler can't be C and ¬C)
(∃hasChild: Cardiologist) ⊑ (∃hasChild: Doctor)           # → true   (reasons through the role)
(¬(∃hasChild: Doctor)) ≡ (∀hasChild: ¬Doctor)             # → true   (quantifier duality)

A declared partition now becomes real logic: C partition A, B, … makes the members pairwise disjoint and jointly exhaustive of C.

concept Animal
concept Cat
concept Dog
Cat extends Animal
Dog extends Animal
Animal partition Cat, Dog

satisfiable(Cat ⊓ Dog)      # → false   (disjoint)
(Cat ⊔ Dog) ≡ Animal        # → true    (covering)

⊑, ≡, and satisfiable answer open-world (over declared axioms). Extensional membership x is <ConceptExpr> answers closed-world, over the instances and relation facts actually present:

felix: a Cat {}
felix is (Cat ⊓ ¬Dog)                    # → true
{p | p <- Animal, p is ¬Dog}             # compound/role concepts in a comprehension FILTER

dora: a Doctor {}
mary: a Cat {}                           # placeholder unrelated entity
hasChild(felix, dora)                     # role fillers should be ENTITIES
felix is (∃hasChild: Doctor)             # → true   (some child is a Doctor)
felix is (∀hasChild: Doctor)             # → true   (every child is a Doctor)

(Role fillers must be entities to carry concept membership — a bare string filler is not an instance of any concept.)

Defined concepts, ⊤/⊥, and more spellings

A defined concept gives a concept a necessary-and-sufficient body with concept X ≡ <expr> (the word equivalent works too). The definition is a genuine axiom in both directions, so subsumptions that follow from it decide, and membership is read off the body:

concept Person
concept Doctor
Doctor extends Person            # so a Doctor is a Person
relation hasChild(x, y)
concept Parent ≡ Person ⊓ (∃hasChild: Person)

Parent ⊑ Person                  # → true   (from the definition)
alice: a Person {}
dora:  a Doctor {}
hasChild(alice, dora)
alice is Parent                  # → true   (a Person with a Person child)

Thing (⊤) and Nothing (⊥) are built in — the universal and bottom concepts, available without declaration (you may still concept Thing "..."; it is an idempotent alias). Every concept satisfies C ⊑ Thing and Nothing ⊑ C; satisfiable(Thing) is true and satisfiable(Nothing) is false; extensionally every individual is a Thing and none is a Nothing. A partition of Thing therefore says the universe is exactly covered:

concept UpToUs
concept NotUpToUs
UpToUs extends Thing
NotUpToUs extends Thing
Thing partition UpToUs, NotUpToUs
(UpToUs ⊔ NotUpToUs) ≡ Thing      # → true  (the dichotomy is total)

Role restrictions have three interchangeable spellings — the COLON form above, the textbook DOT form, and the OWL Manchester words (role on the left):

(∃hasChild.Doctor) ≡ (∃hasChild: Doctor)        # DOT
(hasChild some Doctor) ≡ (∃hasChild: Doctor)    # Manchester ∃
(hasChild only Doctor) ≡ (∀hasChild: Doctor)    # Manchester ∀

(The DOT form never disturbs the symbolic quantifier ∀x. flies(x), and some/only stay ordinary words outside this position — some S is P categorical syntax and an only: binding are untouched.)

A compound concept can also drive a comprehension source for the ⊓/⊔ cases:

{x | x <- (Person ⊓ ¬Doctor)}    # the persons who aren't doctors

A bare ¬C / ∃R.C / ∀R.C / Thing source has no finite extent without a domain universe, so it is a clean error pointing you at FILTER position ({x | x <- C, x is <expr>}); those universe-bearing sources are deferred.

The older dl_kb(...) family of builtins remains for explicit string-keyed knowledge bases. DL operators evaluate in the tree-walking interpreter (not under --vm, which does not compile concept declarations).

Enumerated types — Concept enumerates A, B, C (Pascal/Ada/Inform-7)

X enumerates A, B, C, … declares X as an enum concept whose extent is sealed and ordered. Each member becomes a ConcreteEntity instance of X with ord (0-based declaration index) and name properties. Members are bound bare (Mon resolves directly) and also as concept-qualified (Day.Mon).

Day enumerates Mon, Tue, Wed, Thu, Fri, Sat, Sun

println(Mon)              # Mon (inspect renders the bare name)
println(Mon.ord)          # 0
println(Day.Mon == Mon)   # true (shared identity)
println(succ(Wed))        # Thu   (succ/pred also step Integers: succ(5) → 6)
println(pred(Fri))        # Thu
println(Day.first)        # Mon
println(Day.last)         # Sun
println(len(Day))         # 7

# Ordered comparison uses ord:
println(Mon < Fri)        # true

# Iteration walks members in declaration order:
foreach d in Day [
  println(d.name)
]

# Strict cross-enum (Pascal/Ada-style):
Color enumerates Red, Green, Blue
# Mon < Red             # ERROR: cannot compare Day and Color

Built-ins: succ, pred, len, Day.first, Day.last. Cross-enum comparison errors with a clean message (Pascal/Ada strict). Re-declaring a member name across two enums collides at declaration time — qualify with Day.Mon to disambiguate. Tests under tests/axioma/types/.

Integer subrange types — Concept ranges A..B (Pascal/Ada)

X ranges Low..High declares X as an integer subrange type. Used in :: annotations, the bound is runtime-checked; with the --typecheck static pre-pass (§26), literal violations are caught before any code runs.

Digit ranges 0..9
Percent ranges 0..<100              # half-open

d :: Digit : 5                  # OK
d :: Digit : 12                 # type error
p :: 0..<100 : 50               # inline range annotation
p :: 0..<100 : 100              # type error

# Reassignment honors the binding-time snapshot:
r :: Digit : 3
r = 7                                # OK
r = 99                               # type error

The by step is rejected in ranges declarations (membership becomes ambiguous). Inverted bounds (5..0) and empty half-open (5..<5) also error at declaration time.

Enum subrange — Sub extends Enum in From..To (Pascal/Ada)

Workday is Day in Mon..Fri declares a subtype of an existing enum restricted to a contiguous slice. Every Workday IS a Day (widening is automatic); a Day with ord outside the slice cannot be a Workday (tightening is runtime-checked). Member identity is shared — Mon is still Day.Mon.

Day enumerates Mon, Tue, Wed, Thu, Fri, Sat, Sun
Workday extends Day in Mon..Fri
Weekend extends Day in Sat..Sun

d :: Workday : Wed              # OK
d :: Workday : Sat              # type error: Sat outside Workday
any :: Day : Wed                # widening — every Workday is a Day

# Iteration visits only the slice:
foreach d in Workday [
  println(d.name)                   # Mon Tue Wed Thu Fri
]
println(len(Workday))               # 5

Endpoints must belong to the named parent enum (cross-enum endpoints error). Inverted bounds, integer endpoints with an enum parent, and non-enum parents all error at declaration time.

Slot-metadata helpers — inverse, transitive, find-or-create

Three small builtins covering common KR patterns. All ship as configuration calls; no new keywords.

# Inverse slots — auto-maintain bidirectional relations
concept Car
concept Engine
Car has parts: none
Engine has part_of: none
inverse_slot("parts", "part_of")

car: a Car {}
engine: a Engine {}
car.parts: engine             # auto: engine.part_of = car

# Transitive slots — walk a chain in one builtin call
concept Person
Person has parent: none
transitive_slot("parent")

alice: a Person {}; bob: a Person {}; carol: a Person {}
alice.parent: bob
bob.parent: carol
ancestors: transitive_closure(alice, "parent")   # [bob, carol]

# find_or_create — definite description with reification
concept Country
Country has name: ""
usa1: find_or_create(Country, {name: "USA"})
usa2: find_or_create(Country, {name: "USA"})    # same instance as usa1

find_or_create is the canonical KB ingestion primitive — it makes "if this entity already exists, give me it; else make it" a one-liner. Inverse-slot propagation is one-step (the propagation guard prevents recursive inverse-of-inverse loops). Cycle-safe entity rendering is automatic — ConcreteEntity.Inspect detects already-visiting entities and emits a short reference.

Auto-classification via defines

A fourth concept-verb that attaches a membership predicate to a class. Any instance whose slots satisfy the predicate is automatically classified; slot mutations re-evaluate and promote/demote in real time. Faithful to KM §17, with Axioma additions (B4 truth, six-level grounding, defeasibility).

concept Person
Person has age: 0

Adult defines { age >= 18 and is Person }
Senior defines { age >= 65 and is Adult }
Sage defines~ { age >= 80 }      # defeasible — grounding=conjecture

alice: a Person {age: 30}
alice is Adult                  # true (auto-classified)
alice is Senior                 # false

alice.age: 70
alice is Senior                 # true (re-classified on slot mutation)

alice.age: 5
alice is Adult                  # false (auto-demoted)

Distinction from has: Concept has prop: val is unidirectional (is(x, C) → prop(x, val) — every member has this property). Concept defines { body } is bidirectional (is(x, C) ↔︎ body(x) — membership iff predicate). See KM §17 for the canonical Mexican/Square contrast.

The three logical roles, separately surfaced:

Predicate body conventions:

• Bare slot names (age, price) implicitly refer to it.<slot>.
• is Concept in prefix position desugars to it is Concept.
• and / or / not and comparison operators work normally; Belnap values propagate through.

Grounding & truth integration:

• Strict defines → grounding=theorem; defines~ → conjecture.
• grounding("isa", instance, Concept) reports the grounding.
• proof("isa", instance, Concept) reports the derivation chain.
• Demoted classifications get truth("false") (Belnap), preserving provenance for audit. Re-promotion re-fires the predicate cleanly.
• Belnap Both results from predicate body propagate to the is fact's truth without crashing (paraconsistent semantics).

Auto-create: if the named concept doesn't exist when defines is evaluated, it's created automatically (extending root Concept). No need for a separate concept Adult line.

Value constraints — constrain()

Write-time validation on slot writes. Where defines classifies instances based on their slot state, constrain gatekeeps the slots themselves: register a predicate that every subsequent write must satisfy, and bad writes are silently rejected (the slot retains its prior value) with a warning to stderr.

concept Customer
Customer has age: 0
Customer has email: ""

constrain(Customer, "age",   lambda v => v >= 0 and v <= 150)
constrain(Customer, "email", lambda v => contains(v, "@"))

alice: a Customer {age: 30, email: "[email protected]"}   # accepted
bad: a Customer {age: -5}                                # WARN; age stays at default 0

alice.age: 200             # WARN; alice.age stays at 30
alice.age: 45              # accepted

# Multiple constraints AND
constrain(Customer, "age", lambda v => v != 13)
teen: a Customer {age: 13}                                 # rejected (second constraint)

# Subclass inheritance — every constraint declared on Customer applies to VIP
VIP extends Customer
v: a VIP {age: -1}                                         # rejected

Predicate contract:

• Takes exactly one argument — the value being written.
• Returns a Boolean-ish value (truthy = accept, falsy = reject).
• May reference other slots only via captured closure variables; cross- slot constraints (predicates referencing self.other_slot) are better expressed as defines, which already sees the full entity.

Enforcement sites: every slot-write path is hooked —

• a Concept {slot: val, ...} — the per-property initialization loop.
• entity.slot: val — direct assignment.
• entity[slot -> val] — ErgoAI frame-attribute set.

Distinction from neighbouring features:

Introspection:

constraints_of(Customer, "age")   # → 2 (count of predicates on this slot, walking ancestors)
constraints_of(Customer)          # → {age: 2, email: 1} (all constrained slots)

KM mapping: closes the gap with KM 2.0 §12 (Value Constraints) — the must-be-a / must-be facets — without committing to a specific type-system facet. The predicate body has the full expression language available, so must-be Integer where v >= 0 and v <= 150 is just lambda v => v >= 0 and v <= 150 when the type check is sugar for an instanceof call.

Test: tests/axioma/concepts/test_value_constraints.ax.

English paraphrases for why — paraphrase()

KM §19.3. Register an English template against a concept; when why X is Concept fires, render the template instead of the default structured proof. Closes the gap between Axioma's structured explanation engine and the regulator-/user-friendly English output that compliance domains require.

concept Person
Person has age: 0
Person has name: ""

Adult defines { age >= 18 and is Person }
paraphrase(Adult, "{it.name} qualifies as an Adult because their age ({it.age}) is at least 18.")

alice: a Person {name: "Alice", age: 30}
why alice is Adult
# → "Alice qualifies as an Adult because their age (30) is at least 18."

Placeholder grammar:

Inheritance: a subclass without its own paraphrase inherits its parent's. Most-specific wins; the parent-chain walk mirrors how constrain constraints are inherited.

Fallback: if no paraphrase is registered for the concept (or any ancestor), why runs the existing structured-proof rendering. The feature is purely additive — adopt it for the classes where English output matters.

Composition:

• defines + paraphrase → auto-classification rendered in English
• unify + paraphrase → the canonical entity's slot values are resolved before placeholder substitution
• Subclass + paraphrase on parent → subclass inherits the parent's template until it registers its own

Test: tests/axioma/concepts/test_paraphrase.ax.

Defined instances — Concept identified by ...

KM §17.3 — automatic coreference by identity key. Where defines auto-classifies instances by their slot state, defined instances auto-merge instances by a declared identity key. Declare which slot(s) uniquely identify an individual, and any two instances of the concept with matching key values are automatically unified — reactively, on every slot write, with no explicit unify call.

The recommended canonical surface is the has/identity slot refinement — identity-ness is slot metadata, so it belongs on the slot declaration rather than in a separate statement that re-names the slot. It parallels Axioma's existing keyword refinements (declare/persist, axiom/transient, is/same).

concept Customer
Customer has/identity ssn: ""        # ssn is the identity key
Customer has name: ""

c1: a Customer {ssn: "123-45-6789", name: "Alice Smith"}
c2: a Customer {ssn: "123-45-6789", name: "A. Smith"}
println(c1 == c2)        # → true (auto-unified)
println(c1.name)         # → A. Smith (newest write wins)

# Composite key — mark each participating slot; all /identity slots
# on a concept jointly form ONE key (declaration order preserved)
concept Order
Order has/identity customer_id: ""
Order has/identity order_number: ""
Order has total: 0

Alternative surfaces (all valid, all lower to the same registry, nothing deprecated):

Customer identified by ssn                       # statement form
Order identified by customer_id, order_number    # composite, explicit grouping
define_equivalence(Customer, "ssn")              # functional builtin

It is the automatic dual of the two manual coreference primitives:

Semantics:

• Each has/identity slot is appended to the concept's key in declaration order; multiple such statements accumulate into one composite key (re-declaration is deduped/idempotent).
• An incomplete key (key slot missing, or holding "") never matches — a partially-populated instance is not a dedup candidate yet. A later write that completes the key triggers the merge.
• The triggering entity wins (newest write wins on slot conflict); the pre-existing match redirects via Canonical.
• Reuses the full unify machinery — B4 paraconsistent slot-merge, transaction rollback, strength/proof/why.
• The merged-away loser is removed from the concept extent, so {X | X <- Concept} counts distinct identities, not raw records.
• Subclasses inherit the parent's key.

Introspection: equivalence_key_of(Concept) returns the key slots as an array of strings (parent chain walked), [] if none.

KM mapping: closes KM 2.0 §17.3 (Defined Instances — Testing for Equivalence), the equivalence half of KM's automatic-classification duality. The membership half (§17.2 Defined Classes) is Axioma's defines.

Test: tests/axioma/concepts/test_defined_instances.ax.

inspect / see — identity-passing evaluate-and-display

A prefix directive that evaluates an expression, prints <source> = <value> to stdout, and returns the value unchanged. Modelled on Elixir's IO.inspect / Julia's @show — the prevailing non-imperative idiom for inline inspection.

c: a Car {price: 150}
inspect c.price                # prints "c.price = 150"
inspect c is Car              # prints "(c is Car) = true"

# Identity-pass: composes inside expressions
n: inspect expensive()    # binds n; the value also printed

Lowest-precedence prefix, so inspect fred is Person consumes the whole is expression without parens.

see is a true alias — same token, same semantics. see c.price is identical to inspect c.price; use whichever reads better in context. The lexer maps both inspect and see to the INSPECT token, so there's one implementation.

The conformance harness (tests/km-conformance/) uses inspect instead of println boilerplate, making the Axioma side structurally parallel to KM's ;;CHECK + form, and the harness compares the two ordered value lists positionally.

Test: tests/axioma/concepts/test_inspect.ax.

Cumulative slots — Concept has slot/cumulative: val

KM-conformant additive slot inheritance. By default Axioma overrides an inherited slot when a subclass redeclares it. The has/cumulative slot refinement opts a declaration into KM's semantics: the newly declared value is unioned with the inherited value into a set. Override (default) and accumulate (opt-in) coexist.

concept Animal
Animal has legs: 4
Dog extends Animal
Dog has legs/cumulative: 3        # union with inherited 4
println((a Dog).legs)            # → {3, 4}

Cat extends Animal
Cat has legs: 3                  # plain decl → override
println((a Cat).legs)            # → 3

The refinement attaches to the slot name (slot/cumulative), parallel to has/identity but on the slot. Semantics:

• The union is computed at concept-declaration time, so is must precede the cumulative has (the canonical order).
• A cumulative slot is always set-valued; set operands are flattened so repeated cumulative declarations down a taxonomy accumulate into one flat set; duplicates drop.
• Slots not declared cumulative keep the default override behaviour.

KM mapping: closes the slot-inheritance gap found by the KM-conformance harness (tests/km-conformance/ case 06) — KM unions slot values across a taxonomy, and has/cumulative lets Axioma reproduce that while keeping override as its default.

Test: tests/axioma/concepts/test_cumulative_slots.ax.

14. Logic Programming (Prolog-Like)

Axioma provides Prolog-like relational programming through set-based deterministic queries — no backtracking, complete result sets, mathematical foundations.

Facts

Declare a relation with relation, then assert facts with assert (or the graded axiom / postulate — see §15):

relation parent(x, y)
relation age(x, n)
relation works(x, role)

assert parent("John", "Mary")
assert parent("Mary", "Alice")
assert parent("John", "Bob")
assert age("Alice", 25)
assert works("John", "Engineer")

Note: an undeclared bare call like parent("John", "Mary") at statement position is read as a function call and errors with Undefined word: parent. Declare the relation first (after which a bare parent(...) call adds a fact), or prefix with assert. As a shorthand, a bare header whose arguments are all uppercase-initial and unbound — pair(X, Y) — is itself read as a relation declaration (the optional-relation form). A bound TitleCase argument is a real thing (a type Concept, a declared relation, Thing/Nothing), so calls like doc(Integer), tableform(Edge), or satisfiable(Doctor) keep their call semantics.

Pattern queries

{X | X <- parent(X, _)}                           # All parents
{Y | Y <- parent("John", Y)}                      # John's children
{(X, Y) | parent(X, Y)}                           # All parent-child pairs

Filtered queries

{X | X <- parent(X, _), age(X, A), A >= 18}       # Adult parents

Cross-relation unification (set ops)

parents: {X | X <- parent(X, _)}
workers: {X | X <- works(X, _)}
working_pars: parents ∩ workers

Variable chain unification

# Equivalent to Prolog: grandparent(X,Z) :- parent(X,Y), parent(Y,Z)
johns_kids: {Y | Y <- parent("John", Y)}
johns_grands: {Z | Y <- johns_kids, Z <- parent(Y, Z)}

Complex term matching

relation person(x, attr1, attr2)
relation location(x, attr1, attr2)
assert person("John", ("age", 30), ("job", "engineer"))
assert location("John", ("city", "NYC"), ("country", "USA"))

{X | X <- person(X, _, ("job", "engineer"))}      # All engineers
{X | X <- location(X, ("city", "NYC"), _)}        # NYC residents

Relations as first-class values

A relation name resolves to a first-class Relation value (not its fact-adder builtin), so it is type-introspectable and iterable over its extent — symmetric with how a concept name iterates its instances:

relation parent(x, y)
assert parent("John", "Mary")
assert parent("John", "Bob")

type(parent)                       # → "Relation"   (@parent is the same)
for (x, y) in parent [ ... ]       # iterate facts directly — no comprehension
{(X, Y) | (X, Y) <- parent}        # bare relation as a comprehension source
{x | x <- node}                    # unary relation → bare elements

parent("Alice", "Carol")           # STILL callable — adds a fact

A predicate's rules are introspectable too. rules_of(pred) returns an Array of RuleClause values, completing the F-logic concept → relation → rule arc (concepts iterate instances, relations iterate facts, rules are inspectable as data):

relation edge(x, y)
path(X, Y) :- edge(X, Y)
path(X, Y) :- edge(X, Z) and path(Z, Y)

rs: rules_of("path")               # Array of 2 RuleClause
type(rs[1])                        # → "RuleClause"   (rs[1] is RuleClause → true)
rs[1].head                         # → "path(X, Y)"        (.head_name / .name → "path")
rs[1].body                         # → "edge(X, Y)"
rs[1].defeasible                   # → false               (.strict → true)
rs[1].direction                    # → "backward"          ("forward" for ==> / ~~>)
{c.head_name | c <- rules_of("path")}

Note: because a relation name is now a value, the KB builtins that take a relation (insert, forget, truth, set_truth, grounding, cancel, challenge, …) expect the relation's name as a string — grounding("parent", "John", "Mary"), not grounding(parent, …). See §16 and §17.

HiLog meta-queries

Reflective queries over predicate names and arities:

predicates_of("alice")             # All facts mentioning alice
predicate_names()                  # All predicate names with ≥1 fact

?P("tweety")                       # Prolog-style meta-call: which predicates mention tweety?
?P("alice", ?Y)                    # Pattern with wildcard in 2nd position
?P(?X, "carol")                    # Strict arity, per-position unification

15. Knowledge Base, Axioms & Postulates

Declaring knowledge — the six grounding grades

Every stored fact carries an epistemic grounding — how strongly it is held — on this ordered ladder:

axiom > postulate > theorem > conjecture > hypothesis > datum

You declare a fact at a grade with the matching keyword; derivation and runtime insert produce the rest. Read a fact's grade back with grounding(rel, args…).

axiom      parent("Adam", "Cain")     # foundational
postulate  married("Cain", "Awan")    # tentative — may be refuted
hypothesis visited("Cain", "Nod")     # a working assumption
assert     lives_in("Cain", "Nod")    # plain fact → grounding "datum"

grounding("parent", "Adam", "Cain")   # → axiom

# theorem / conjecture come from derivation (§16); or set any grade at runtime:
insert("parent", "Seth", "Enos", "theorem")

Grounding tracks derivation provenance — a strict rule yields a theorem, a defeasible rule yields a conjecture. The derived grade is fixed by the rule type (strict vs. defeasible), not by the premises' grades: the tier records how a fact was derived, not a confidence floor over its inputs (a theorem strictly derived from a datum-grade premise is still a theorem). See §16 for the mechanics, and challenge (below) / cancel · force_cancel (§17) for revising graded facts.

Persistence control

axiom/persist     gravity = 9.81           # Saved to cascade.db
axiom/transient   demo_axiom = 42          # Session-only
postulate/persist working = "..."
postulate/transient debug = "..."

Default: REPL persists, scripts are transient.

The public persistence forms are the /persist and /transient refinements shown above, plus the declare persistence forms in §3.

The shared SQLite KB

Axioma and Cascade share a single SQLite database (cascade.db) using the same schema. Both processes can read/write concurrently.

./axioma --no-kb script.ax        # Skip Cascade KB preload (~10× faster)

16. Rules, Derivation & Epistemic Grounding

Rule forms

Strict rules

The primary spelling is the natural one — the rule connective is the word whenever, so a clause reads as English and wears its logic honestly: "whenever" is English's universal conditional, exactly the ∀-bound Horn head ("there is a path from X to Y whenever there is an edge from X to Y" — true of every pair). The other spellings remain first-class: head if body (Visual Prolog's word, gated — see below), <== (and legacy <=) and Prolog's :- in arrow/Prolog dress, and the forward direction is operator-only (==> / ~~>):

grandparent(X, Z) whenever parent(X, Y) and parent(Y, Z)   # primary
grandparent(X, Z) if parent(X, Y) and parent(Y, Z)         # if-form (gated)
grandparent(X, Z) <== parent(X, Y) and parent(Y, Z)        # operator twin (also <= / :-)
parent(P, Q) and parent(Q, R) ==> grandforward(P, R)       # forward — operator only

All spellings store the same clause and share the fixpoint engine, multi-clause accumulation, theorem grounding, and safety diagnostics:

path(X, Y) whenever edge(X, Y)                     # primary natural spelling
path(X, Y) whenever edge(X, Z) and path(Z, Y)      # recursive clause
path(X, Y) :- edge(X, Y)                           # same rule, Prolog dress
mortal("socrates") whenever human("socrates")      # ground head — works bare

whenever is a soft keyword (whenever: 5 still binds a variable) with no conditional reading, so the shape head(args) whenever body is a rule by fiat — no gate, any argument casing, ground heads included. The if spelling is different: because EXPR if COND is also the postfix conditional modifier (cancel(d) if challenged(d)), bare if reads as a rule only when the head call's arguments include an uppercase logic variable and the head does not resolve to a callable — push(s, V) if V > 3 keeps its conditional meaning (push is a builtin), while path(X, Y) if edge(X, Y) stores a rule clause. With the explicit rule prefix there is no gate for either word: rule H(args) whenever body and rule H(args) if body are always rules. Both bare natural forms map to the strict reading only; for the defeasible natural spelling see typically in the next subsection.

Defeasible rules

A defeasible rule states a default — an inference that holds unless overridden. Where a strict rule's conclusion is a theorem that always follows, a defeasible rule's conclusion is a conjecture: a plausible default that can be defeated by a stricter rule, by conflicting evidence, or by an explicit cancel. This is how Axioma expresses "typically / normally / by default" reasoning (non-monotonic logic) — birds typically fly, even though penguins don't. And that literature gloss is the primary spelling: the statement prefix typically (synonym twin: normally) marks the clause defeasible, in Reiter's own words:

typically flies(X) whenever bird(X)   # PRIMARY — "birds typically fly"
normally  sings(X) if bird(X)         # synonym twin; composes with if too

The operator twins write the same default in arrow dress:

flies(X)  <~~ bird(X)     # backward: flies(X) holds by default when bird(X) does
bird(X)   ~~> flies(X)    # forward:  the same default, written premise-first

(The infix use of the same word — birds typically fly — is the separate default-logic engine with Reiter extensions, unchanged; the rule marker is the statement-start position only.)

The rule prefix offers two further equivalent markers, both lowering to the same clause as <~~:

rule~ flies(X) whenever bird(X)        # tilde marks defeasible (like defines~ / unify~)
rule/defeasible flies(X) if bird(X)    # refinement spelling (like concept/persist)
rule/strict walks(X) if bird(X)        # explicit spelling of the strict default

Every marker composes idempotently with a matching operator (typically chirps(X) <~~ bird(X) and rule~ sings(X) <~~ bird(X) are fine), while a contradiction such as typically p(X) :- q(X) or rule~ p(X) :- q(X) is a loud parse error ("conflicting rule strength") — an explicit defeasibility marker never silently stores a strict clause.

Both operator forms express the same rule and produce conjecture-grade conclusions; they differ only in reading direction — <~~ writes the conclusion first, ~~> the premise first (see the rule-forms table above). Their strict twins <= (backward) and ==> (forward) instead produce theorems:

A defeasible conclusion is overridden when a strict rule proves the contrary, or by a cancel / force_cancel directive (§17) — and grounding-aware cancel refuses to defeat a theorem. So flies("tweety") is a conjecture you can retract, while a theorem stands until you revise its premises.

Frame-logic rule bodies

Bodies can mix is, function calls, attribute paths, and conjunctions:

TradeLink extends Concept
TradeLink has source
TradeLink has target

{tl | tl is TradeLink, tl.target.gdp_billion > tl.source.gdp_billion * 2}

Epistemic grounding (six ordered grades)

axiom > postulate > theorem > conjecture > hypothesis > datum

• axiom — declared with axiom. Foundational.
• postulate — declared with postulate. Tentative.
• theorem — derived by a strict rule from axioms/postulates.
• conjecture — derived by a defeasible rule.
• hypothesis — user-marked working assumption.
• datum — a plain asserted fact, or a runtime insert(...) without explicit grounding — the floor of the ladder.

Strict rules produce theorems, defeasible rules produce conjectures — the derived grade is fixed by the rule type, recording derivation provenance rather than a min(body_groundings) confidence floor. A theorem strictly derived from a datum-grade premise is still a theorem, not a datum.

The introspection builtin is grounding, and the floor grade is datum.

Grounding & Kind as first-class values

grounding(...) and truth_kind(...) return typed values, not bare strings. A Grounding is ordered (the ladder above); a Kind is a flat five-member set (logical / empirical / transcendental / motive / metalogical). Both coerce against a plain String, so existing == "axiom" comparisons keep working.

relation edge(x, y)
axiom edge("a", "b")
path(X, Y) :- edge(X, Y)

g: grounding("edge", "a", "b")              # → axiom   (a Grounding value)
type(g)                                      # → "Grounding"   (g is Grounding → true)
grounding("edge", "a", "b") >= "conjecture"  # axiom >= conjecture → true  (ordered)
grounding("edge", "a", "b") >= grounding("path", "a", "b")   # axiom >= theorem → true

relation color(x, y)
axiom/empirical color("apple", "red")
k: truth_kind("color", "apple", "red")       # → empirical   (a Kind value)
type(k)                                       # → "Kind"
k == "empirical"                              # → true  (String coercion — no ordering on Kind)

The possessive accessors agree with the builtins: fact's grounding and fact's kind return the same Grounding / Kind value types.

Bilattice truth propagation

Every stored fact carries a Belnap B4 value (T, F, Both, Neither) that propagates through Horn-clause bodies via lattice meet. Paraconsistent contamination (Both) survives derivation.

set_truth("parent", "John", "Mary", "true")
truth("parent", "John", "Mary")          # Returns Belnap value

Provenance & introspection

The relation is named by string (a relation name is now a first-class value — §14):

grounding("parent", "John", "Mary")       # a Grounding value: axiom / theorem / conjecture / datum / ...
proof("grandparent", "John", "Alice")    # Walks derivation chain back to axioms
why grandparent("John", "Alice")         # Prose explanation (keyword form — takes the conclusion call)
rules_of("path")                          # The predicate's rules as first-class RuleClause values

Challenging axioms

Axioms must be challengeable (Q1 requirement):

challenge("parent", "John", "Mary")       # Marks suspect
challenged("parent", "John", "Mary")      # Returns true/false

The axiological (value) axis

Orthogonal to epistemic grounding, a fact can carry an explicit value judgment relative to an authority. The axis has three judged stances plus a distinct fourth "never judged" state:

epictetus: agent("epictetus", "Stoic — virtue is the only good")
value_good("courage", "any_agent", epictetus)
value_bad("cowardice", "any_agent", epictetus)
value_indifferent("wealth", "any_agent", epictetus)   # the Stoic adiaphoron

value_kind_of("courage", "any_agent")     # → "good"
value_kind_of("wealth", "any_agent")      # → "indifferent"   (a JUDGMENT)
value_kind_of("has_blue_eyes", "any_agent")  # → "neutral"    (SILENCE — never valued)
facts_by_value_kind("indifferent")        # enumerate the judged-indifferent facts

value_indifferent makes "positively judged neither-good-nor-bad" a first-class stance, distinct from a fact that was simply never valued (neutral) — the difference between the Stoic adiaphora and mere silence.

Aspectual facts — qua

qua (Latin "in the capacity of") makes the same fact viewable under a handle, and rules can key on the handle — so one fact can carry two value-laden framings with divergent consequences (intensionality made executable):

relation departed(x)
departed("the_estate") qua "lost"
departed("the_estate") qua "given_back"

framings_of("departed", "the_estate")            # → {"lost", "given_back"}
framed_qua("departed", "the_estate", "lost")     # → true

disturbs(it)  <~~ it qua "lost"                  # `it` binds to every fact tagged "lost"
at_peace(it)  <~~ it qua "given_back"
# the SAME fact is now both disturbing AND at peace — Enchiridion 11

it qua "h" binds it to every fact tagged h; the relation-anchored form rel(X) qua "h" instead binds X to the argument. qua stays an ordinary identifier outside this position (a same-line soft keyword).

17. Mutation, Transactions & Conflict Resolution

Runtime mutation

The relation is named by string (relation names are first-class values now — §14):

insert("parent", "Eve", "Seth")          # Defaults to grounding "datum"
insert("parent", "Eve", "Seth", "axiom") # Explicit grounding
forget("parent", "Eve", "Seth")          # Retract from all groundings

Note: delete and retract are reserved keywords. Use forget for the function-call form. The statement form retract [...] is a separate existing feature.

Atomic transactions

transaction_begin()
insert("parent", "X", "Y")
set_truth("parent", "X", "Y", "true")
transaction_commit()                     # OR transaction_rollback() — undoes ops AND metadata

Defeasible-conflict resolution

relation bird(x)
flies(X) <~~ bird(X)
assert bird("tweety")                    # Tweety conjecturally flies
cancel("flies", "tweety")                # Tweety is a penguin
canceled("flies", "tweety")              # true
uncancel("flies", "tweety")              # Restore

Canceled facts retain their provenance but are filtered out of comprehensions.

Grounding-aware cancellation

cancel is grounding-aware: it refuses to defeat a derived theorem (a strict consequence), returning a non-fatal "refused: …" string that points you at revising a premise (challenge) or overriding with force_cancel. Defeasible conclusions (conjectures) and base posits (axioms / postulates / data) stay directly cancelable.

tranquil(P) <== free(P)                  # strict rule → derives a theorem
assert free("sage")
cancel("tranquil", "sage")               # → "refused: … is a theorem …"  (NOT canceled)
force_cancel("tranquil", "sage")         # → "canceled: tranquil(\"sage\")"  (explicit override)

forget_cascade — justification-based retraction (a TMS)

Plain forget retracts a premise but orphans the conclusions already derived from it. forget_cascade walks the derivation chains forward, withdraws the premise and every materialized fact that transitively depends on it, then lets lazy re-derivation rebuild whatever still has independent support:

disturbed(P) <~~ judges_bad(P)
assert judges_bad("novice")
{p | p <- disturbed(p)}                   # → {"novice"}
forget_cascade("judges_bad", "novice")
{p | p <- disturbed(p)}                   # → {}   (the conclusion lifts with its premise)

A conclusion that also follows from a surviving rule re-derives automatically on the next query.

18. Stack-Based Programming

Axioma implements a first-class stack model:

• a first-class Stack value — construct it with s: a Stack or with stack(); both build a real Stack (@s → "Stack"). stack(c) additionally converts an array, set, tuple or finite range, with position 1 as the top: stack([1, 2, 3]) is Stack[1 | 2 | 3], and array(s) / set(s) / tuple(s) convert back. (stack_new() was the older nullary-only spelling; retired July 2026 — it now errors with a pointer at stack().)
• a global interpreter stack, inspectable from the REPL with :stack

A Stack value has two equivalent surfaces — use whichever reads best:

Natural-language — a message verb mutates (statement position) and a possessive reads (expression position):

s: a Stack
s push 5
s push 10
s's top            # → 10        (peek;  s's depth → 2,  s's empty → false)
s's items          # → [10, 5]   (top-to-bottom)
s pop              # remove the top — value discarded in statement position
v: pop(s)          # …so capture a popped value with the pop() function

Mutating verbs: push pop peek drop clear dup swap over rot nip tuck. Possessive reads: top/peek, bottom/base, depth/size/ height/length, empty, items/elements/contents. top on an empty stack returns none (check s's empty first).

Function form (Forth / Pop-11) — every operation is a function taking the stack as its first argument: push(s, x), pop(s), peek(s), dup(s), … These are the same operations as the verbs above (kept as aliases) and are the form used in the tables below. (The natural-language surface is evaluator-only; under --vm, use the function form.)

Core operations

Stack-shuffle operations

All take the stack as the first argument and mutate it in place.

Bulk & depth operations

Array conversion

Example

s: stack()
push(s, 1)
push(s, 5)
dup(s)                 # 1 5 5
swap(s)                # 1 5 5  (top two swapped)
println(pop(s))        # 5
println(depth(s))      # 2
println(stack_to_array(s))   # [5, 1]   (top first)

REPL inspection

The global interpreter stack is inspected with REPL commands:

:stack          # Show stack contents
:s              # Alias for :stack
:stack trace    # Show stack with type information
:stack depth    # Show stack depth
:stack clear    # Clear the stack

See tests/axioma/stack/ for comprehensive examples.

19. Three Notations, One Tree

Most languages pick one notation and bury the others under syntactic surcharge: Lisp commits to prefix, ML to infix, Forth to postfix. Axioma treats all three as surface forms of the same AST node. The unifying claim is concrete: for any expression you can write in two notations, fullform returns the same string.

fullform(2 + 3)        # "+(2, 3)"   — infix
fullform(+(2, 3))      # "+(2, 3)"   — Julia-style prefix
fullform(seq_of(2, 3, +))  # "Sequence(2, 3, +)" — postfix sequence (a different node)

The first two are identical because both parse to the same InfixExpression. The third is a SequenceExpression whose stack-reduction semantics happen to produce the same value.

19.1 Prefix: operators are functions

Every binary operator can be called like an ordinary function. The parser recognizes op(args) where op is one of:

+   -   *   /   %   #   ^   **   .*   ./   .+   .-   .^
==  !=  <   >   <=  >=

+(2, 3)             # 5
*(4, 5)             # 20
<(3, 5)             # true
+(1, 2, 3, 4)       # 10 — left-folded across all args

The variadic form (+(1, 2, 3, 4)) is a left-fold via the same evalInfixExpression dispatch the infix form uses, so multi-valued logic dispatch, set operations, and lattice operators all behave identically. See §9.

19.2 Operators as values

A bare operator name evaluates to a synthetic two-argument function. You can bind it, pass it, and compose it like any other callable:

plus: +
times: *
lt: <

plus(2, 3)                          # 5
reduce(+, 0, [1, 2, 3, 4])          # 10
reduce(*, 1, [1, 2, 3, 4])          # 24
reduce(-, 20, [1, 2, 3])            # 14

The synthetic function has parameters _op_a, _op_b and body _op_a OP _op_b — the same dispatch path the infix form uses. Limitation: the synthetic is binary. (-)(5) returns a partial-application lambda, not the unary negation; for unary minus on a value use -(x) directly.

19.3 Postfix: comma sequences

A comma-separated chain whose elements include at least one operator or stack word is parsed as a SequenceExpression and evaluated by stack reduction:

2, 3, +                        # → 5
2, 3, +, 4, *                  # → 20  (push 2, push 3, +, push 4, *)
10, 4, +, 6, 2, -, *           # → 56

Sequence semantics: walk the elements left-to-right; numeric/string/array literals push onto a parse-time stack; an operator pops the top two and pushes the result; a stack-shuffle word rewrites the stack (see below). The whole sequence reduces to the single remaining stack value.

A sequence is the right-hand side of an ordinary expression — so it composes:

r1: 2, 3, +                    # r1 = 5
r2: 2, 3, +, 4, *              # r2 = 20
r3: 10, 4, +, 6, 2, -, *       # r3 = 56

2, 3, +, .                     # prints 5 — Forth `.` pops and prints
println(r1)                    # prints 5 (inside a CALL, commas separate
                               #   arguments: println(2, 3, +) passes THREE
                               #   args — bind the sequence first)

Postfix sequences live inside the expression grammar rather than seizing the whole program, so they coexist peacefully with infix and prefix in the same line.

Multi-bind still works

The parser only collapses a chain to a sequence when at least one element is an operator or stack word. The classic multi-bind pattern is unchanged:

a, b: 5, 6                     # a = 5, b = 6 — not a sequence

19.4 Stack-shuffle words inside sequences

Inside a SequenceExpression, the stack-shuffle vocabulary is in scope and operates on the local parse-time stack rather than the global interpreter stack from §18:

20, 4, swap, /                     # 4 / 20? no — swap before /: 4, 20, /  → 0
20, 4, /, 2, +                     # 20 / 4 + 2 → 7
1, 2, 3, rot, -, +                 # rot: 2,3,1 → 3-1=2 → 2+2 = 4

These names shadow the same-spelled global-stack operations only inside a sequence; outside sequences the global-stack semantics from §18 apply.

19.5 The . (dot) inspect sigil

A trailing . prints the value of the preceding expression — a compact "print-and-go" — and works in two positions:

Statement-trailing (after any top-level expression):

2 + 3 .                            # prints 5
x: 42 .                       # prints 42
fullform(2 + 3) .                  # prints "+(2, 3)"

The dot may also sit tight against the expression — a sentence-style full stop. It works after every literal family and closer: 2 + 3., 2.5., 10% + 5%., $100 + $25., 100x200 + 20x30., type(x)., [1, 2]. all print. A . not followed by a digit never reads as a decimal point, so $100.50 and 2.5 stay intact while the trailing dot lexes as the sigil. The one exception: literals whose own syntax contains dots — URLs, emails, file paths, dates — absorb a tight trailing dot into the literal (https://example.com. is a valid trailing-dot FQDN), so use the spaced form . after those.

Sequence-internal (pops the current top of the parse-time stack and prints it — the . is consuming, not duplicating):

2, 3, +, .                         # prints 5 (stack empty after)
20, 4, /, 2, +, .                  # prints 7 (stack empty after)
2, 3, +, ., 10, 5, -, .            # prints 5, then prints 5 (two checkpoints)

The dot is parsed as the existing PERIOD token wrapped in a ScopedStatement for the trailing form, and as a stack-print step for the sequence-internal form. It is interchangeable with inspect / see in spirit but more compact.

19.6 Tracing sequence reduction

The existing trace keyword accepts a sequence (or seq) category that prints a step-by-step view of stack reduction:

trace sequence
20, 4, /, 2, +, .

# push 20         →  [20]
# push 4          →  [20, 4]
# /               →  [5]
# push 2          →  [5, 2]
# +               →  [7]
# .  (inspect)    →  [7]

Bare trace is equivalent to trace all — every category enables, including sequence. The same untrace / untrace sequence disable mirror.

The domains

Tracing selects by domain — a whole class of operation — not by named function. Every domain answers to several spellings; an alias always selects the whole domain, never a narrower slice of it.

An unrecognized domain is a catchable error naming the recognized set — a typo, a domain that prints nothing, and "the traced operation never ran" would otherwise be indistinguishable.

The epistem domain reports the grounding tier each fact is written at, which is the thing worth watching: assert writes datum, the bottom of the ladder, while assert/axiom routes to the axiom path and writes at the top.

trace/verbose epistem [ assert likes("alice", "bob") ]
# → Asserting Fact
#   arity: 2
#   grounding: datum
#   relation: likes
# ← Fact Asserted (relation): Epistem{type=datum, value="likes(...)", ...} (EPISTEM)

Detail lines are sorted by key, so a /verbose transcript is byte-reproducible and can be asserted on through trace_log().

Scoped trace blocks — trace <domain> [ ... ]

trace has two forms, and the domain list is optional in both:

Naming several domains in one statement widens the trace in one go; untrace func control mirrors it. Every name is validated before any is applied, so a typo rejects the whole statement rather than half-enabling it:

trace binding contrl           # ERROR: unknown trace domain "contrl" — and
                               #   `binding` is NOT switched on either

The block form traces only its body and restores the previous state on exit, so a forgotten untrace cannot flood the rest of the run:

trace binding [ total = 42 ]
outside = 7                    # NOT traced — the block restored on exit
println(total)                 # → 42

Three properties make it composable:

• Additive. A block widens the trace for its extent; it does not replace what is already on. So trace control [ ... ] nested inside an active trace binding shows both, and leaves binding running afterwards — restore puts back the prior state, not "off".
• Scope-transparent. Bindings made inside the block survive it. A debugging lens must never change the program it observes; if the block opened a scope, switching tracing on would silently alter the result.
• The transcript survives. As with untrace, you read the log after the traced region — trace_log() still returns it once the block has exited. Clear it with clear_trace_log().

Refinements compose, and are restored along with the domain:

trace/verbose binding [ v = 7 ]    #   v = 7 (INTEGER)
trace binding
w = 8                              #   w = 8        ← /verbose did not survive
untrace

The block is same-line gated, so a [ opening the next line is still its own statement — bare trace followed by an array literal keeps its old meaning.

19.7 AST inspection — fullform, treeform, headof, argsof, hold, seq_of

The fullform / treeform / headof / hold family, spelled in Axioma's call-with-commas idiom. Every builtin in this group has hold semantics: the argument's AST reaches the builtin unevaluated, so fullform(2 + 3) prints the tree, not 5.

fullform(2 + 3)                    # "+(2, 3)"
fullform(2 + 3 * 4)                # "+(2, *(3, 4))"
fullform(f(x, y + 1))              # "f(x, +(y, 1))"

treeform(2 + 3 * 4)
# +
# ├── 2
# └── *
#     ├── 3
#     └── 4

headof(2 + 3)                      # "+"
argsof(2 + 3 * 4)                  # ["2", "*(3, 4)"]

h: hold(a + b * c)
fullform(h)                        # "+(a, *(b, c))" — auto-unwraps the held AST

s: seq_of(2, 3, +, 4, *)
fullform(s)                        # "Sequence(2, 3, +, 4, *)"

Auto-unwrap of held AST values. When the argument to fullform / treeform / headof / argsof is an identifier whose value is a *AST (produced by hold or seq_of), the builtin walks through the binding and inspects the held node. This is what makes h: hold(2+3); fullform(h) render +(2, 3) rather than the identifier "h".

19.8 Why "one tree" is the load-bearing claim

The point of the three notations is not stylistic preference. It is that the evaluator never branches on notation — 2 + 3, +(2, 3), and reduce(+, 0, [2, 3]) all converge on the same evalInfixExpression dispatch. Adding a new operator (or fixing a multi-valued logic semantics bug) touches one path, and every notation that surfaces that operator inherits the fix.

Concretely, the identity is testable:

verify("identity prefix/infix",
       fullform(2 + 3), fullform(+(2, 3)))   # both "+(2, 3)"

See tests/axioma/notation/ for the full assertion battery (operator-prefix, postfix sequence, dot inspect, stack words, sequence trace, fullform, operator-as-value, three notations) and tests/axioma/showcase/11_three_notations.ax for a single-file walkthrough.

19.9 Homoiconicity — building code as data

The inspection family above (fullform / headof / argsof) lets you read code as data. The construction family closes the loop: you can build AST values from scratch in Axioma source, manipulate them, and ast_eval them back into computation. That's metaprogramming — programs that produce programs.

Constructors. Each make_* returns an AST value. Args may be other AST values OR raw Axioma values (auto-lifted via the same machinery quasiquote uses):

Round-trip identity. Constructed and quoted ASTs compare equal structurally:

make_infix("+", 2, 3) == hold(2 + 3)       # true — same canonical form
ast_eval(make_infix("+", 2, 3))            # 5
make_identifier("x") == hold(x)            # true
quote(x * y) == make_infix("*", make_identifier("x"), make_identifier("y"))   # true

Recursive traversal via parts(ast). Unlike argsof (which returns strings), parts returns Array of AST values — so you can walk a tree without re-parsing at each level:

h: hold((a + b) * c)
outer: parts(h)         # [AST(a + b), AST(c)]
inner: parts(outer[1])  # [AST(a), AST(b)]
ast_string(inner[1])         # "a" — use ast_string for inline display
                              # (fullform has hold semantics; bind first or use ast_string)

is_ast(x) predicates the type — useful in pattern-matching code:

is_ast(hold(2 + 3))     # true
is_ast(42)              # false

The dispatch loop. Recursive AST walks dispatch on ast_kind:

walk: func(expr) [
    k: ast_kind(expr)
    if k == "integer_literal" then ...
    else if k == "identifier" then ...
    else if k == "infix_expression" then ...
    else expr
]

The killer demo: symbolic differentiation in 25 lines

Below is a complete textbook differentiator written entirely in Axioma. No interpreter extension required:

diff_infix: func(expr, var_name, dx) [
    op: headof(expr)
    lhs: parts(expr)[1]
    rhs: parts(expr)[2]
    if op == "+" then make_infix("+", dx(lhs, var_name), dx(rhs, var_name))
    else if op == "-" then make_infix("-", dx(lhs, var_name), dx(rhs, var_name))
    else if op == "*" then make_infix("+",
        make_infix("*", dx(lhs, var_name), rhs),
        make_infix("*", lhs, dx(rhs, var_name)))
    else expr
]

dx: func(expr, var_name) [
    k: ast_kind(expr)
    if k == "integer_literal" then make_integer(0)
    else if k == "identifier" then (
        if headof(expr) == var_name then make_integer(1) else make_integer(0)
    )
    else if k == "infix_expression" then diff_infix(expr, var_name, dx)
    else expr
]

d: dx(quote(x * x + 3 * x + 5), "x")
println(fullform(d))   # +(+(+(*(1,x), *(x,1)), +(*(0,x), *(3,1))), 0)
                       # — unsimplified; equivalent to 2x + 3

A simplify(expr) pass (fold 0*x → 0, 1*x → x, x+0 → x) is another function in the same style; together they make a small CAS. substitute(expr, var, value) for evaluating at a point is five lines around make_integer. Everything you'd want from a computer algebra system is achievable in user-space code.

Definition-time macros

Beyond runtime AST construction, Axioma has Julia/Elixir-style macros — macro name(params) body definitions that expand at the call site. Macro arguments arrive as unevaluated AST, the body must return an AST (typically built via quasiquote(...) + unquote(...)), and the expansion is then evaluated in the calling context.

macro double(x) quasiquote(unquote(x) * 2)
double(21)                                  # → 42

# Inspect the expansion without running it:
ast_string(macroexpand(double(21)))         # → "(21 * 2)"

# Multi-arg, conditional, nested all work:
macro unless(cond, body) quasiquote(if not unquote(cond) then unquote(body) else none)
macro addAndDouble(a, b) quasiquote((unquote(a) + unquote(b)) * 2)
addAndDouble(3, 4)                          # → 14

double(double(3))                           # → 12 (nested expansion)

Hygiene via gensym:

gensym()                # → G__1   (fresh unique symbol)
gensym("tmp")           # → tmp__2

Use inside macros that introduce temporaries (__r: gensym("r")-style) to avoid capturing user identifiers. Like Julia (and unlike Elixir or Clojure-syntax-rules), Axioma macros are non-hygienic by default — you opt into hygiene with gensym.

Implementation: parser at parser/parser.go:9866, expansion engine at evaluator/macro_expansion.go:187, macroexpand builtin at evaluator/evaluator.go:25913. Test corpus: tests/axioma/metaprogramming/ (10+ files).

The head / operands / make_expr normal-form algebra

Mathematica unifies every expression under one shape — head[args]. Axioma renders its three surface notations (infix, prefix, postfix) and call syntax to that same normal form, and a small algebra reads and rebuilds any quoted expression uniformly, regardless of which syntax produced it.

head('(2 + 3))                                  # → "+"
operands('(2 + 3))                              # → [<AST: 2>, <AST: 3>]
make_expr(head('(2 + 3)), operands('(2 + 3)))   # → <AST: (2 + 3)>   (round-trips)
head('(add(7, 9)))                              # → "add"   (a call's functor)
head('(if x then 1 else 2))                     # → "if"

make_expr(head(e), operands(e)) == e holds for infix / prefix / postfix / call / binding / rule / if. Fixity is recovered from a curated operator table; an unknown head builds a CallExpression.

Pattern rewriting — match_pattern / subst / replace_all / rules

The algebra above is the substrate for term rewriting — Mathematica's expr /. rule and the heart of a computer-algebra system. Patterns reuse Axioma's existing ?x variable syntax; no new lexer.

match_pattern('(?a + ?b), '(2 + 3))                  # → {a: <AST: 2>, b: <AST: 3>}
subst('(?a * ?a), {a: '(7)})                         # → <AST: (7 * 7)>
replace_all('(x + 0), rules('(?a + 0), '(?a)))       # → <AST: x>   (additive identity)

A nonlinear pattern (?x + ?x) enforces same-subtree consistency. Each rule may carry a guard — a third element, a quoted predicate over the ?vars (Mathematica's /;); the rule fires only when the guard holds, and guards see the builtins and the caller's definitions. Pattern variables in head position (?f(?x)) bind the functor, and sequence patterns match variable-arity argument runs — ?xs__ (one or more) and ?xs___ (zero or more), in call-argument position. Together these are enough to write algebraic simplification and symbolic differentiation as a rule list rather than a hand-written dispatch.

A form is a collection — the "Julia-Plus" tier

A quoted expression also behaves as the sequence of its operands for the universal collection operations, so generic code traverses code the same way it traverses data:

len('(2 + 3))                  # → 2          (was an error before)
'(add(7, 9))[1]                # → <AST: 7>   (1-indexed into the operands)
[op | op <- '(a + b + c)]      # comprehension over a form's operands
foreach op in '(2 + 3) [ println(op) ]
map(func(x) [x], '(2 + 3))     # map / filter accept a form

The code ↔︎ data bridge — to_data / from_data

Two converters cross the line between a quoted AST and an ordinary value:

to_data('(2 + 3))                  # → 5            (evaluate a form to its value)
from_data(5)                       # → <AST: 5>     (lift a value into an AST literal)
to_data(from_data(v)) == v         # round-trips for scalars, arrays, sets, tuples

from_data understands the set-theory core (Set and Tuple values lift, not only scalars and arrays). The bridge is the frictionless path between the two worlds: where the '(…) quote-forms carry bracket-overloading gotchas ('[…] is a block quote, '([…]) is an array-literal quote), from_data(theValue) is unambiguous.

Where Axioma sits in the homoiconicity taxonomy

Per Wikipedia's taxonomy of homoiconic languages, Axioma is in the "weaker tier" alongside Julia, Elixir, and Nim — full toolkit (quote, quasiquote, AST construction, AST evaluation, macros, macroexpand, hygiene primitive) but source code is parsed rather than being a literal data structure.

The article explicitly notes "no consensus exists on a precise definition" of homoiconicity — under a lenient definition Axioma qualifies fully; under the strict "source IS data" definition it doesn't. Reaching the strict tier would require abandoning the multi-syntax three-notations design, which is intentional (see §19.1–§19.4).

The head / operands / make_expr algebra and the match_pattern / replace_all rewriter above add a facility usually associated with Mathematica — a uniform head[args] normal form plus structural pattern matching and term rewriting — onto the reified-AST base. That strengthens the practical tier (think "Julia-Plus") without changing where Axioma sits in the strict sense: a quoted form is still a dedicated AST value, not source-as-list, so '[1, 2, 3] == [1, 2, 3] remains false. The algebra unifies the operations over code-as-data; it does not unify the representation. Reaching the strict "source is data" tier would require a different language kernel and is deliberately out of scope for the current design.

See docs/code-as-data.md for comparison tables and cookbook patterns.

Limits

See tests/axioma/notation/test_homoiconic.ax for the 46-assertion smoke test, and demo_differentiate.ax for the full symbolic-differentiation example.

Grammar classification — is Axioma context-free?

Not as a single fixed context-free grammar. Axioma has a context-free skeleton, but the language the parser actually accepts steps outside CFG-land in one decisive way and two softer ways:

1. alias makes the grammar adaptive (the decisive one). The parser's parseAliasStatement installs the mapping into the live lexer (Lexer.AddAlias), and identifier lexing consults that table on every subsequent token — so after alias myif = if, the word myif tokenizes as the if keyword for the rest of the same source stream (verified: alias myif = if + alias mythen = then + alias myelse = else makes myif 1 > 0 mythen "a" myelse "b" parse as a full conditional). How a program's suffix parses depends on the content of its prefix. A language whose sentences extend their own grammar mid-stream is not context-free (the same argument that puts Lisp reader macros and Forth word definitions outside CFGs — declared-name ↔︎ used-as-keyword dependencies are the classic cross-serial pattern). Note this is keyword remapping, not a general reader-macro facility: alias re-lexes identifiers onto existing tokens; it cannot introduce new syntactic forms (see the limitations table above).

2. Recognition is PEG-style, not CFG-style. The hand-written recursive descent + Pratt parser carries a dozen-plus SaveState/RestoreState speculative-parse sites — colonHeadsSetComprehension trial-parses to split the British set comprehension {x : x <- s} from a hash literal {k: v}; pipeStartsConsTail splits the cons pattern [H | T] from a comprehension [h | h <- xs]; dotBodyIsConcept splits the DL restriction ∃hasChild.Doctor from the quantified formula ∀x. flies(x). Backtracking with ordered choice is parsing-expression-grammar semantics; PEGs and CFGs are incomparable classes, and "valid Axioma" is defined operationally by what this parser commits to — no equivalent CFG is maintained.

3. Layout and token-shape sensitivity — inelegant but CF-encodable. Dozens of same-line gates make the soft keywords (mod, div, unless, whenever, qua, only, limit, offset, …) operators only between same-line expressions not followed by :; the lexer decides token identity from local context ($5 Money vs $name guard, %data File vs 7 % 2 modulo, #123 Issue vs #hello QuoteWord). These could be encoded in a (much larger) CFG by promoting NEWLINE to a terminal and splitting identifier classes, so they don't change the classification by themselves.

What genuinely is context-free: the Pratt expression core (operator- precedence grammars are a subset of deterministic CF), all bracket-balanced structure including [python | …] foreign-language blocks (bracket matching is the textbook CFL), nested string interpolation — and, worth stressing, macros do not break the surface grammar: unlike Lisp reader macros, Axioma macros expand post-parse on the AST, so macro double(x) quasiquote(…) never changes how source tokenizes.

The standard footnote applies as it does to every real language: the set of programs that run (no undefined words, arity checks, the uppercase-concept rule, --typecheck's :: Ordinal discipline) is context-sensitive anyway — true of C and Python too — which is why the question is conventionally asked of surface syntax only. Honest one-line classification: a deterministic context-free core, recognized with PEG semantics, made formally non-context-free by one deliberate feature (alias) in the Lisp/Forth adaptive-grammar tradition. (Runtime-registered dialect grammars don't affect the surface class — their blocks are just balanced brackets to the parser; the dialect matching happens at evaluation time.)

20. Russell's Three Meanings of "is"

Axioma distinguishes the three classical meanings of the copula "is":

hesperus is same as phosphorus               # Identity
sky is blue                                  # Predication
there is x in {1, 2, 3}: x > 2               # Existence

Refinement operators: is/same, is/identical, is/property.

Identity is Leibniz identity, not address comparison

is/same asks whether two expressions denote one object. It is a refinement of ==, not a synonym: == asks whether two values denote the same thing, is/same asks whether they are the same thing.

5 is/same 5          # → true   — there is only one 5
1 == 1.0             # → true   — same number
1 is/same 1.0        # → false  — `type` and `exact?` tell them apart
[1, 2] is/same [1, 2]  # → false — two arrays
[1, 2] == [1, 2]       # → true  — with equal contents

The answer follows Leibniz's two principles, with "property" read as any predicate Axioma can express:

• Identity of Indiscernibles — indiscernible therefore identical — holds for immutable scalars: numbers, strings, booleans, dates, URLs and the rest of the REBOL scalars. These are abstract objects with no haecceity; nothing distinguishes one 5 from another, so 5 is/same 5 is true.

• It fails for concrete particulars and containers. Two dogs with the same name are two dogs; two arrays with equal contents are two arrays, because you can push onto one and observe that the other did not change. Identity there is reference identity — which is what makes the Hesperus/Phosphorus case come out right, since two names for one object are identical and the difference of sense belongs to the name:

  concept Planet { name: "" }
  hesperus: a Planet { name: "Venus" }
  phosphorus: hesperus
  hesperus is same as phosphorus       # → true  — one planet, two names
  twin: a Planet { name: "Venus" }
  hesperus is same as twin             # → false — two planets

• Indiscernibility of Identicals — identicals agree on every predicate — runs the other way and is what keeps is/same finer than ==. 1 is/same 1.0 is false because exact? and type are predicates that disagree on them: it is settled by observation, not by fiat.

Two IEEE corners fall out of the same reasoning. nan is/same nan is true even though nan == nan is false — no predicate tells one NaN from another, and identity must be reflexive. -0.0 is/same 0.0 is false even though -0.0 == 0.0 is true — str renders them "-0" and "0", so they are discernible. (Scheme's eqv? gives both the same answers.)

The executable statement of these laws is lib/laws/equality.ax; run it with axioma lib/laws/equality.ax.

21. Pointers & References

C-style pointers

x: 42
p: &x                      # Take address
*p                               # 42 — dereference
*p = 100                         # Write through pointer
x                                # 100

arr: [10, 20, 30]
p2: &arr[2]                # Pointer to array element
*p2                              # 20

alice: a Person {age: 30}
p3: &alice.age           # Pointer to property
*p3 = 31
alice.age                        # 31

Pointers work in both interpreted and VM modes.

Deep copy

copy(value) returns an independent deep copy:

a: [10, 20, 30]
b: copy(a)                       # deep copy — mutating b leaves a untouched

Note — @ is type-of, not a reference get-word. @x returns the type of x (@42 → "Integer"), identical to type(x). Plain x already yields the value, and the address/dereference operators &x / *p (above) are Axioma's actual reference mechanism.

22. Mathematical Constants & Built-ins

Mathematical constants

Set constants

Mathematical functions

Randomness — random / random_seed / shuffle / sample

Lua's math.random surface, natively:

random()          # Float in [0, 1)
random(6)         # Integer 1..6 — a die roll
random(10, 20)    # Integer 10..20 inclusive
random_seed(42)   # select a deterministic stream (returns 42)
random_seed()     # entropy opt-in — reseed from the OS, RETURNS the chosen seed
shuffle(xs)       # new shuffled array (the input is untouched)
sample(xs)        # one random element (arrays, tuples, sets)
sample(xs, 2)     # 2 distinct elements, without replacement
values(sample(normal(0, 1), 3))   # distribution draws — values() unwraps a Sample

The seeding model (deliberate). The generator starts with the fixed seed 1, so every run of an unseeded program replays the same sequence — reproducibility is the default, matching the rest of the language (doctests, expect() pins, the deterministic test sweep). This is the classic Programming in Lua (≤5.3) model; modern Lua 5.4+ auto-seeds at startup instead — a deliberate divergence. When you want fresh randomness (a game, a real simulation), call random_seed() once at the top: it seeds from OS entropy and returns the seed it chose, so even a "fresh" run can be logged and replayed exactly. One seedable source backs the scalar family and the probability-distribution samplers, so random_seed(42) also makes sample(uniform(0, 1), n) reproducible.

The long tail. Python's random module breadth (expovariate, gammavariate, weighted choices, getrandbits, …) stays one spelling away through the FFI block:

[python/eval | __import__("random").expovariate(1.5) ]

with one caveat: Python-routed draws live in the subprocess's own generator and do not obey random_seed — only the native family and the prob distributions join the seed contract. When a distribution earns a native home, it lands in prob's seedable source (the normal/uniform/ binomial/beta path) precisely so it does.

Formatted output — printf / stringf / format

C-style format verbs; printf writes to stdout, stringf returns the String (use it inside expressions). format is an exact alias of stringf — the spelling Lua, Ruby, Java/C#, and Rust hands reach for, and in every one of those languages it returns the string rather than printing (Lua's string.format, Ruby's format ≡ sprintf; printing stays printf, or compose println(format(...))). All three interpret escape sequences in the format and share one verb-aware argument adapter (also behind the log_*f family):

printf("%05d|%6.2f|%-6s|\n", 42, 3.14159, "ab")   # 00042|  3.14|ab    |
stringf("%d %d", floor(x), floor(x + 0.5))         # ints under %d
format("%x", 255)        # "ff"        — exact alias of stringf (returns, never prints)
stringf("%d", 35.0)      # "35"        — an INTEGRAL Float converts
stringf("%.2f", 1/3)     # "0.33"      — Rationals format under the float verbs
stringf("%f", 5)         # "5.000000"  — Integers too
stringf("%s", [1, 2])    # "[1, 2]"    — %s/%q take anything (display form)
stringf("%d", 2^100)     # big-int aware
stringf("100%% sure")    # "100% sure" — %% is the literal percent
stringf("%d", 35.7)      # ERROR: %d needs an integer value, got 35.7 —
                         #   use floor(x) or round(x), or format with %g

Verbs: %d %b %o %x %X %c %U (integer class — %x/%X also hex-dump a String), %f %e %g + upper (float class), %s %q %v, %t (Boolean only), %%; flags/width/precision (%-6s, %05d, %6.2f, *) follow Go's fmt. The adaptation rule is the numeric tower's own stance (35.0 == 35 is already true): an integral value converts across the verb classes; a fractional value under an integer verb is a loud, catchable error with a rewrite hint — never silent junk. Every mismatch errors this way (wrong type, missing or extra arguments, unknown verbs, a bare trailing %), and a Go-style %!… badge can never appear in output.

Predicates

even(4)            # true
odd(3)             # true
positive(5)        # true
negative(-3)       # true

Scheme/Lisp-style predicates (? suffix)

Lisp/Scheme spell the test marker ? rather than Common Lisp's p. A trailing ? is part of the identifier (zero? is one word), so these read naturally. The sign predicates treat a non-number as false (matching even/positive).

# sign / parity (over Integer, Float, Rational)
zero?(0)           # true       plus?(5)      # true   (strictly positive)
positive?(5)       # true       minus?(-1/3)  # true   (strictly negative)
negative?(-5)      # true       even?(4)      # true        odd?(3)  # true

# type predicates (join number?/integer?/string?/boolean?/null?/pair?/array?…)
list?([1, 2, 3])   # true       procedure?(func(x) [x])  # true
empty?([])         # true   — also "" / set() / {} / dict() ; an infinite set is never empty
symbol?('hello)    # true   — a lit-word is a symbol ; symbol_name('hello) → "hello"

# float domain  (`inf` / `nan` are builtins producing ±∞ / NaN floats)
nan?(nan)          # true        infinite?(inf)      # true        finite?(3.14)  # true
integral?(5.0)     # true   — the VALUE is whole (5.01/NaN/±Inf → false; the TYPE test is integer?)

# equality:  eq? / eql? / eqv?  are shallow identity (collections by reference);
#            equal?  is deep, type-strict (the `==` engine)
eq?(1, 1)          # true        eq?([1,2], [1,2])     # false  (distinct objects)
equal?([1,2], [1,2])  # true     equal?(1, 1.0)        # false  (type-strict)

Higher-order functions

map(fn, set)           # Transform
filter(pred, set)      # Select
reduce(fn, init, set)  # Aggregate (left fold)
sum(coll)              # Numeric sum over array/set/tuple (Σ is Unicode alias)

# Scheme/Lisp folds & combinators
foldl(fn, init, coll)  # left fold, fn(acc, elem) — like reduce (also fold_left)
foldr(fn, init, coll)  # right fold, fn(elem, acc) (also fold_right)
append_map(fn, coll)   # map then concatenate the per-element collections (flatmap / mapcat)
for_each(fn, coll)     # apply fn for side effects; returns null
constantly(x)          # → a function that ignores its args and returns x
negate(pred)           # → a predicate that logically negates pred (≠ set `complement`)

List & string helpers

butlast([1, 2, 3, 4])              # → [1, 2, 3]   (all but the last)
dedupe([1, 2, 2, 3, 1])           # → [1, 2, 3]   order-preserving (remove_duplicates / unique)
chars("abc")                       # → ["a", "b", "c"]   (string → char array)
char_alphabetic?("a")              # → true   (also char_numeric? / char_whitespace?)

Knowledge-base builtins

rel is the relation name as a string ("parent", not the bare value parent); args are the fact's arguments.

MVL constructors

intuit3("true"/"false"/"unknown")
belnap("true"/"false"/"both"/"neither")
lukasiewicz(0.0..1.0)

23. Venn Diagrams & Visualization

a: {1, 2, 3, 4}
b: {3, 4, 5, 6}
venn(a, b)                       # 2-set diagram

c: {3, 4, 5}
venn(a, b, c)                    # 3-set diagram with all intersections

Diagrams auto-pop in the default image viewer and are saved to diagrams/venn_diagram_TIMESTAMP.png.

Run ./scripts/clean_diagrams.sh to clean accumulated PNGs.

The *form family — rendering expressions & relations

A family of introspection builtins renders a value to text. fullform / treeform show an expression's AST; tableform / graphform render a relation's extent (rule-derived facts included, since they walk the same fact store as comprehensions); tableform also renders a function's truth table. Relations pass as a held bare identifier or a string.

relation edge(x, y)
assert edge("a", "b")
assert edge("b", "c")

println(tableform(edge))
# relation: edge  (2 facts)
# ┌─────┬─────┐
# │  x  │  y  │
# ├─────┼─────┤
# │ "a" │ "b" │
# │ "b" │ "c" │
# └─────┴─────┘

println(graphform(edge))             # default ASCII adjacency
# graph: edge  (2 edges)
#   "a" → "b"
#   "b" → "c"

graphform(edge, "dot")               # Graphviz DOT — paste into `dot -Tsvg`
graphform(edge, "cg")                # Sowa conceptual-graph linear notation [a]→(edge)→[b]
graphform(edge, "png")               # force-directed PNG → visualizations/graph_<ts>.png
graphform(edge, "svg")               # scalable SVG (preferred for web / VS Code)

Headers come from the declared slot names; output tuples are sorted deterministically. Higher-arity relations fall back to positional notation (binary is the natural graph case).

Truth tables — tableform(func, [domain])

Give tableform a function instead of a relation and it prints the function's truth table: one row per assignment of domain values to the parameters, leftmost parameter varying slowest (the textbook layout). Input columns are headed by the parameter names and the result column by the function's actual body expression (p and q — a multi-statement body falls back to result); a bound function's name appears in the title. The companion truth_table(f) returns the same rows as a Set of tuples — truth_table is the data, tableform the display.

println(tableform(func(p, q) [p and q]))
# truth table: (p, q)  (4 rows)
# ┌───────┬───────┬─────────┐
# │   p   │   q   │ p and q │
# ├───────┼───────┼─────────┤
# │ true  │ true  │ true    │
# │ true  │ false │ false   │
# │ false │ true  │ false   │
# │ false │ false │ false   │
# └───────┴───────┴─────────┘

The optional second argument selects the value domain — this is how the multi-valued logic tables print. Name a logic ("boolean", "kleene", "belnap", "lp", "lukasiewicz", "g3") to enumerate its canonical value set, or pass an explicit Array/Set for a general function table:

println(tableform(func(p, q) [p ⊼ q], "kleene"))   # strong-Kleene NAND, 3×3
println(tableform(func(p, q) [p and q], "belnap")) # the full B4 4×4 ∧ table
println(tableform(func(p) [not p], "g3"))          # G3's ¬U = F, visible
println(tableform(func(x) [x * x], [1, 2, 3]))     # function table over a domain

Rows are capped at 4096 (domain^parameters); bodies dispatch per operand type as usual, so the same ⊼ body prints classical, K3, or B4 tables depending only on the domain.

24. Comments & Literate Programming

Basic comments

# Single-line comment
x: 5  # Inline comment

Markdown documentation blocks

/**md ... */ blocks are extracted by axiomadoc for HTML/Markdown/PDF rendering:

/**md
# Function: calculateDistance

## Purpose
Euclidean distance between two points.

## Math
$d = \sqrt{(x_2-x_1)^2 + (y_2-y_1)^2}$

## Cross-references
- {@link otherFunction}
- {@concept Point}
*/
calculateDistance: func(x1, y1, x2, y2) [
    sqrt((x2 - x1) ^ 2 + (y2 - y1) ^ 2)
]

Generating documentation

./axiomadoc generate -input . -output docs -format html  -template default
./axiomadoc generate -input . -output docs -format html  -template academic
./axiomadoc generate -input . -output docs -format markdown
./axiomadoc serve    -port 8080 -watch -input .         # Live-reload server
./axiomadoc validate -input . -check-links -run-examples

Doctests — examples that test themselves

A documentation example can also be a test, so the examples in your docs can't silently rot. A fenced axioma doctest block — written inside a /**md … */ literate block in a .ax file, or directly in a .md file — is executed line by line:

Lines in one fence share an environment; each fence is isolated. The expected value is compared by canonical value form (so (14, 2), {1, 2, 3}, "hi", true compare as values, not as strings).

The fence opens with the info string axioma doctest (shown here inside a literate block):

/**md
## divmod — quotient and remainder together

```axioma doctest
divmod(100, 7)        # → (14, 2)
divmod(10, 0)         # raises: by zero
n: divmod(9, 2)       # setup line — run for effect
n[1]                  # → 4
n[2]                  # -> 1
```
*/
divmod: func(a, b) [(a // b, a % b)]

Run them from the CLI, or with the Playground's ✓ Doctest button:

axioma --doctest path.ax        # one file
axioma --doctest docs/          # walk a directory for .ax / .md fences

--doctest prints ok: / not ok: per assertion and a N passed, M failed summary, exiting non-zero if any assertion fails or if no fence is found (so a mistyped axioma doctest tag can't pass silently). The engine is shared between the CLI and the WebAssembly build, so the in-browser Playground ✓ Doctest button gives identical results. For assertions inside ordinary scripts (rather than docs), see the expect builtin (§26).

25. Interactive Features (REPL)

Line editing

• ↑/↓ — command history (persistent across sessions)
• ←/→ / Home/End — cursor movement
• Tab — keyword completion

Special commands

help               # Language help
doc <topic>        # Topic documentation
:stack             # Inspect interpreter stack
:s                 # Alias for :stack
:stack trace       # Step-by-step stack trace
exit               # Quit

doc — statement and call form

doc is a language statement, not just a REPL command — it works in scripts too, and it has a call twin that prints the identical text through the same renderer:

doc Integer        # statement form
doc(Integer)       # call form — byte-identical output
doc("if")          # keywords/operators can't be call arguments — use a String
doc                # the full topic catalog (sorted); also doc()

The call form holds its bare-identifier argument un-evaluated (doc(random) documents the name random, not the function value), prints like println, and returns null. It is evaluator-only — under --vm it rejects with a clear message.

Runtime reflection — the self-describing surface

Axioma answers its own reference questions at the prompt. doc <Type> on a built-in primitive type prints a type card — bounds, literal forms, operations, conversions, and related functions — and the headline limits are also live members on the seeded type concepts:

doc Float            # the full card: IEEE 754 binary64, literal forms, ==
                     #   pitfalls, conversion family, related functions
Float.max            # → 1.79769313486232e+308 (Ruby Float::MAX, native;
                     #   exactly: Float.max == 1.7976931348623157e308)
Float.min_positive   # → 4.94065645841247e-324 (smallest subnormal)
Float.epsilon        # → 2.22044604925031e-16 (the gap above 1.0)
Float.digits         # → 15 (guaranteed significant decimal digits)
Integer.bounded      # → false — and asking anyway teaches:
Integer.max          # ERROR: Integer has no max — integers are
                     #   arbitrary-precision … see `doc Integer`
Byte.bounded         # → true; Byte.min → 0, Byte.max → 255

Cards exist for Integer, Float, String, Boolean, Rational, Complex, Byte, Bytes, Array, Tuple, Set, and Dictionary. Every card line is verified by running the interpreter, and doc X ≡ doc(X) stays byte-identical.

Four enumeration/search builtins complete the surface:

keywords()           # every reserved word (sorted); keywords("if") → true
builtins()           # every builtin function name (sorted; 1000+);
                     #   builtins("map") → true — works under --vm too
concepts()           # every Concept visible here — seeded + user-declared
bindings()           # what YOU have bound this session (fresh session → [])
apropos("substr")    # search names AND documentation text; prints
                     #   name — category — summary lines, sorted

builtins() is precise by design: it lists the standard (VM-shared) table; env-aware builtins (tableform, grounding, …) are documented individually and surface through apropos. concepts(), bindings(), and apropos() walk the live environment, so they are evaluator-only (clean rejection under --vm) and shadowable — a user binding of the name wins.

Function signatures are data (the REBOL model — help renders from the spec). Spec-registered builtins carry a runtime-true parameter list, and three introspection functions read it — for user functions too:

signature(round)     # → "round(x, [digits])"  ([x] = optional, xs... = variadic)
signature(max)       # → "max(values...)"
arity(map)           # → 2   (fixed arity from the spec; -1 when not one number)
parameters(round)    # → ["x", "[digits]"]
adder: func(a, b) [a + b]
signature(adder)     # → "func(a, b)"   ·   arity(adder) → 2
doc round            # the doc card now opens with Signature: and the summary

A builtin without a spec yet renders honestly as name(...) — the spec table backfills incrementally, and a drift-guard test pins every registered spec to the live implementation (its arity claims are exercised against the real argument checking, so the metadata cannot rot).

Per-type function catalogs — functions(Type) (Julia's methodswith view). Each card-bearing type carries a curated, verified list of the builtins that operate on it (or construct it) — the runtime answer to "what can I do with this type?":

functions(Integer)     # → ["abs", "add1", "bin", …, "zero?"]  (sorted)
functions("String")    # same catalog by name (this spelling works under --vm)
"divmod" in set(functions(Integer))   # → true
functions()            # → the cataloged type names (the doc-card set)

Functions only — operators (+, band, union, …) stay documented on the type card, which remains the home of the full operations story. Every (type, function) pair in the catalog was verified by running before being listed, and a drift test pins each entry to a live builtin — so the catalog deliberately excludes the lookalikes (choose is the binomial coefficient, not a set picker; drop is the Forth stack verb; abs rejects Rationals).

Value inspection — describe(x) (the Elixir i/1 / Common Lisp describe model). Where doc documents names, describe inspects values: it prints a card with the display form, the type, and the type-specific facts you would otherwise probe by hand, then points at doc <Type> and functions("<Type>"):

describe(42)           # Parity/Sign/Digits + the card pointers
describe("héllo")      # Bytes: 6 (len) vs Runes: 5 (count)
describe(round)        # the R3 Signature: + Summary: lines
describe(none)         # the none-vs-om teaching card (falsy absence vs truthy Ω)
describe(my_relation)  # arity + live fact count + tableform pointer

Collections report size and element types; MVL values report their logic and designation; relations report their extent (which is why describe is evaluator-only — it reads the live environment; --vm rejects it with a clear message). It returns null — the output is the effect — and it is shadowable: a user binding named describe wins.