README · Reference · Playground

Ajisai Language Semantics

Status: Canonical
Specification version: 1.0.0-beta.1
Release stage: Beta. A breaking change to the vocabulary, to program meaning, or to the host protocol raises the specification version and is named in the release that ships it; a compatibility guarantee begins at 1.0.0.

This document defines the correspondence between Ajisai source programs and observable values, states, effects, and diagnoses. It is a compact semantic kernel: differences between individual Words belong to the machine-readable vocabulary registry, not to parallel prose definitions.

Ajisai is built from ten concepts. Everything below is one of them, or a consequence of one of them.

1. Exact rational arithmetic, closed under square roots, with no rounding.
2. Three outcomes: a value, a reasoned absence, or an error.
3. A stack of values and vectors of values.
4. Code blocks, evaluated only when a Word asks for it.
5. One consumption rule: a Word consumes what it reads, and BIND names a value for reuse.
6. A two-tier dictionary — sealed Core, user-defined User — with content-addressed identity.
7. A machine-readable contract for every Word.
8. A pre-execution check of user declarations against those contracts.
9. One host protocol, which is the only way anything outside the language observes it.
10. An executable conformance corpus that decides whether an implementation is Ajisai.

1. Authority and Compatibility

LANG.AUTHORITY.SOURCES — Normative sources

Eight sources are authoritative, each for a different part of the language:

SPECIFICATION.html renders the two prose sources — this document and spec/gui-semantics.md — and is not edited directly. The six data sources are read directly by the implementation and its gates rather than through it: a source is authoritative because this table says so, not by appearing in that document.

Neither implementation layout nor explanatory text can override an observable contract. A document that is not in the table above defines nothing; docs/dev/ holds design notes and history on those terms.

LANG.AUTHORITY.PRESENT — Present-tense description

Ajisai has three reading surfaces: the README, the Reference, and this Specification. Each describes the language as it currently is. A definition, an example, or an explanation may rest only on concepts the language has, and every Word it names must exist in the vocabulary registry.

Superseded designs, migration history, and the reasoning behind a change are recorded outside these three surfaces, in notes that define nothing. A negative statement belongs on a reading surface only when it constrains an implementation — "an implementation must not convert malformed use to NIL" is such a constraint — and not when its only content is a contrast with a design the language does not have.

LANG.AUTHORITY.IDENTITY — Language identity

Ajisai identity is the correspondence from normalized source to the ordered observation of stack, output, dictionary state, and structured diagnosis. Two implementations are semantically equivalent when that correspondence agrees for every conforming program.

Kernel and Standard are both ordinary Core Words in one flat dictionary, reached by their plain names, with contracts, laws, and conformance held to the same standard. Growth is not the goal: a proposed Word that is expressible as a user definition over the existing vocabulary does not belong in Core — unless expressing it that way costs asymptotically more than the same work done in the kernel, in which case what the definition demonstrates is a gap in the vocabulary rather than the absence of one.

LANG.AUTHORITY.FREEDOM — Implementation freedom

In particular an implementation may execute a Word by any route it likes, provided the route is unobservable.

2. Source and Desugaring

LANG.SOURCE.TEXT — Source domain

A program is Unicode text tokenized by the sealed Ajisai lexical grammar (spec/grammar.json). There are five kinds of token: a number, a string, a name, and the two delimiters [ and ]. Everything else — which Word a name is, whether a Vector is code, what a definition is — is decided after tokenizing, not by it.

A decimal literal carries at least one digit on both sides of the point: 0.5 and 5.0 are numbers, .5 and 5. are not. The point is therefore never the first or last character of a number, so a lone . is unambiguously a name rather than a truncated literal.

This numeric grammar is the single definition of what text denotes a number. A conversion from Text to a Scalar accepts exactly the lexemes a source literal accepts and projects everything else to NIL, so the language has one numeric grammar rather than one per entry point. A rational whose denominator is zero, 1/0, has the shape of a number and denotes none: in source it is a source error, and as text it projects to NIL like any other text that is not a number. How large a number a lexeme may denote is bounded by the numeric-literal ceiling (LANG.MACHINE.LIMITS), counted in the digits it denotes rather than the characters it takes — 1e5000 denotes a 5001-digit integer — at every entry point that reads this grammar.

Whitespace is the sole token delimiter and is otherwise insignificant; a line break is whitespace like any other, so a program written across lines and the same program written flat are one program, with one Word identity (LANG.DICTIONARY.MUTATION). A line break ends a comment, which is the only thing it ends: # at the start of a word runs to the end of its line. No other character splits a token, the delimiters included: each of [ and ] must stand alone like every other word, so [ 1 2 3 ] is well-formed and [1 2 3] is a source error asking for the missing space, and # glued to a preceding lexeme is just part of that one name, not a comment. A quoted string is the one delimiter of its own: it may hold whitespace internally ('hello world'), but its closing ' must itself be followed by whitespace or end of input to close.

An unclosed string, a delimiter glued to anything, a zero denominator and an unbalanced delimiter are the source errors, and there are no others: every lexeme the other rules decline is a name, so no name is invalid as text. A source error refuses the whole program before any of it runs. It does not denote NIL.

LANG.SOURCE.NORMALIZE — Name normalization

Word lookup is case-insensitive through the canonical normalization, and case is all it folds: a Word has exactly one name, and no second spelling resolves to it.

Normalization does not merge distinct value tags, invent dictionary entries, or change string and code-block contents.

LANG.SOURCE.DESUGAR — Surface forms

Desugaring is deterministic and semantics-preserving. The registered delimiter forms lower to canonical concepts before evaluation.

If \(D\) is desugaring and \(O\) observation, then \(O(p)=O(D(p))\) for every well-formed program \(p\). Sugar cannot introduce a new value domain or failure category.

LANG.SOURCE.CODE — Code values

Code is a Vector holding source for later evaluation — not a distinct domain from data, but the same Vector domain (LANG.VALUES.DISJOINT) read as executable by a Word whose contract requests it. [ ] is the sole bracket, for both: [ 1 2 ADD ] is equally a data literal and, wherever a Word's contract requests it, executable code. A value's construction history is not part of it (LANG.VALUES.DENOTATION), so nothing about how a Vector came to exist marks it as "code" or "data" ahead of use. Evaluated as code, a Vector's elements run in order: a Symbol names a Word, and every other element pushes itself exactly as it is held — a NIL with its reason, a Record, an exact irrational — whether or not any source text denotes it.

Producing, storing, displaying, and evaluating a Vector as code are distinct operations. Quoted code is not eagerly executed: evaluation occurs only through a Word whose contract requests it — EXEC and the higher-order family — never merely by building or holding the value; CONTRACT reads a block without evaluating it. Branching is not among them: SELECT chooses between two values the program has already built, so a branch evaluates nothing and skips nothing. A bare name written where a Vector element is being collected denotes a Symbol (LANG.VALUES.VECTOR) — data until something executes it — so a name is not resolved merely by appearing inside a literal.

LANG.SOURCE.FRAME — What a block sees

A block has no stack discipline of its own: the Word that evaluates it decides what the block reaches and what it may leave, and the block's text does not say which rule applies. The difference is whether an ADD written inside it finds two operands or none. Two rules cover every case.

A block written inside another block is data where it is written, evaluated only when the Word receiving it runs it, under that Word's rule and not the enclosing block's. This holds regardless of what name the block writes: a name naming the word being defined, reached only through such a nested block, is still a reference to that word for LANG.DICTIONARY.ACYCLIC to see, even though nothing here evaluates it.

A frame also holds local bindings. BIND consumes a value and a name and makes the name that value for the rest of the frame, however many times it is written; several names destructure a Vector of the same length. The isolation above is of the stack, not of names, so the blocks a Word evaluates read the frame they were written in — and a Word call does not: a body reads its own bindings and its operands and nothing of its caller's, so what a Word means never depends on where it is called. A binding ends with its frame, and a name is a Word or a binding and never both.

3. Value Domains

LANG.VALUES.DISJOINT — Tagged domains

Values form a disjoint tagged sum of exactly seven domains: Scalar, Boolean, String, Vector, Record, NIL, and Symbol. A Record is a keyed correspondence (LANG.RECORDS.STRUCTURE); it is not a Vector, a Vector of pairs is not a Record, and nothing converts between them implicitly. A Symbol is a bare name, data until something executes it (LANG.SOURCE.CODE); it is its own domain, reachable standalone ([ ADD ] 0 GET leaves the Symbol ADD on the stack) as well as nested inside a Vector. Two values are never equal merely because their encodings resemble one another: a Symbol is not the String of the same spelling.

In particular FALSE is not scalar zero, TRUE is not scalar one, and an absent value is not an ERROR.

LANG.VALUES.DENOTATION — Identity is denotation

A value is what it denotes, never how it was made. Two values are one value exactly when they denote the same thing, whatever operations produced each of them: \(\sqrt{8}\) and \(\sqrt{2}+\sqrt{2}\) are one value, and two NILs carrying one reason are one value. Construction history is not part of a value and cannot be read back out of one.

An internal representation is therefore unobservable, and a display is derived from the value rather than from the source that produced it. A procedure that decides identity answers about denotation, and where it cannot decide it answers that it cannot, never "different": comparison over the exact field decides (LANG.VALUES.EXACT), and the content identity of LANG.DICTIONARY.MUTATION decides only one direction. spec/identity.json states the law and what each level delivers.

LANG.VALUES.EXACT — Exact scalars

A scalar is an exact real. The domain is fixed by a condition rather than by a list: it is a field — closed under addition, subtraction, multiplication and division — whose equality and order an implementation decides in finite time through a normal form it exhibits. Comparison over this field is accordingly total: every comparison of two of its scalars yields TRUE or FALSE in finite time, not as a separate guarantee but as the half of the condition that fixes it.

The field \(\mathbb{Q}(\sqrt{d_1},\dots,\sqrt{d_k})\) generated over the rationals by square roots of non-negative rationals, in multiquadratic normal form \(\sum_d c_d\sqrt{d}\) with rational \(c_d\) and square-free integer \(d\), is the witness that meets the condition. Because every \(d\) is square-free the form is one per number, so a display and the protocol's exactTerms are read off the value and never off the operations that built it (LANG.VALUES.DENOTATION): 8 SQRT and 2 SQRT 2 MUL are one value written one way. Reaching the square-free part factors the radicand, which no cheap algorithm does for every integer, so that factoring is charged to the run's numeric work and a radicand the remaining work cannot factor is resourceLimitExceeded (LANG.MACHINE.LIMITS). Integer, fraction, decimal, and scientific-notation literals are source forms for exact rationals, and SQRT generates the rest from a rational radicand: it is what builds the field rather than an operation the field is closed under. POW answers inside the field — an integer exponent is repeated multiplication or division, and an exponent p/2 over a non-negative rational base is a power of its square root; every other exponent leaves the field and projects domainMiss — and GCD and RATIO read the integers and the reduced numerator and denominator that every rational carries. Arithmetic performs no intermediate rounding, and coefficients are arbitrary-precision, so a coefficient grows to whatever size the value requires. Rounding happens only where a program names it and only into text: FORMAT renders a scalar as decimal text with a stated number of digits, a tie rounding away from zero as ROUND rounds, and the field's decidable order settles every digit, an irrational's last one included. A real with no exhibited normal form is not an Ajisai value: widening the domain means exhibiting a new normal form that meets the condition, not amending the condition.

LANG.VALUES.TRUTH — Three-valued truth

The Boolean domain has exactly three truth values: TRUE, FALSE, and UNKNOWN. TRUE and FALSE are the two Boolean data values; UNKNOWN is not a fourth variant but NIL (LANG.VALUES.NIL) read in truth position — a Word with nothing to decide from produces NIL, and NIL standing where a truth value is expected reads as UNKNOWN. AND and NOT compose all three values by the strong Kleene tables below, and so does every connective written from them — a disjunction is a NOT b NOT AND NOT; composition is not passthrough, so an absent operand yields UNKNOWN only where the other operand does not already settle the result by itself.

FALSE dominates AND even against an UNKNOWN operand, decided by the definite operand alone; where neither operand settles it, the output is UNKNOWN and carries whichever operand's absence reason applies — the left operand's, when both are absent (LANG.FAILURE.PASSTHROUGH's left-to-right rule). UNKNOWN enters the truth domain one way: through an absent operand read in truth position. Every comparison over the exact domain decides in finite time and yields TRUE or FALSE: totality is a domain property of the field (LANG.VALUES.EXACT), not a limit this clause imposes. Misuse still lives outside this domain: an operation that is malformed raises ERROR, which is never a truth value. The host protocol observes TRUE and FALSE as boolean nodes carrying semantics.truthValue "true" or "false", and UNKNOWN as the NIL it is — a nil node carrying its absence reason (LANG.OBSERVATION.PROTOCOL); a consumer reads these rather than display text (LANG.OBSERVATION.FIREWALL). Being read in truth position adds an observation; it takes none away. UNKNOWN is still the NIL it is: NIL? answers TRUE for it, NIL-REASON reports the reason it arrived with, a fallback can be chosen in its place, and a passthrough Word passes it on — so 1 0 DIV TRUE AND is an UNKNOWN whose reason is still divisionByZero. An implementation that reports UNKNOWN as present, or that drops its reason, contradicts LANG.VALUES.NIL.

LANG.VALUES.NIL — Diagnostic absence

NIL is a value representing absence from a well-formed partial operation. It carries a reason: a stable, machine-readable identifier for why production failed. The reason is observable through NIL-REASON and through the protocol. The reason space has two layers: the closed set of identifiers spec/outcomes.json registers, and one of them, userDeclared, which a program reaches by ABSENT and which carries the Text the program gave as its parameter — that Text is what NIL-REASON answers for it.

The reason is the entire observable content of a NIL, the declared Text of a userDeclared NIL included; so two ABSENT NILs are the same value exactly when their Texts are equal. An implementation may emit richer diagnostics on the host channel, and no program behavior may depend on them.

LANG.VALUES.VECTOR — Vectors

A Vector is an ordered finite collection of values. Indexing is 0-origin and negative indices count from the end. Vectors nest, and nesting expresses ragged and grouped data.

Vector length is semantic even when storage is flattened, shared, or lazily materialized. Order and length are a Vector's whole observable structure, and a nested Vector is an element like any other.

Inside a Vector literal a name denotes a Symbol (LANG.VALUES.DISJOINT): data until something executes it, and building the literal is not itself execution, so no dictionary lookup occurs there. [ FOO ] is the one-element Vector holding the Symbol FOO whether or not FOO is a defined Word, so a Vector literal denotes the same value under every dictionary state. Only TRUE, FALSE and NIL denote values rather than a Symbol carrying their name. A consequence worth stating: a misspelled name inside a Vector literal is a Symbol element, not an error.

LANG.RECORDS.STRUCTURE — Records

A Record is a keyed correspondence: a sequence of distinct keys, each any value, paired position by position with a sequence of values. Those two sequences are its whole observable structure — KEYS and VALUES read them back, aligned — so two Records are one value exactly when their key sequences and their value sequences are (LANG.VALUES.DENOTATION), and key order is observable: PUT replaces a present key in place and appends an absent one, and MERGE keeps the left operand's order, takes the right operand's value where both hold a key, and appends the right's remaining keys. RECORD builds one from a Vector of keys and a Vector of values, and raises two ERRORs rather than making a choice for the program — a key left without a value under it is the length mismatch between the two sequences, and a repeated key is duplicateKey. A Record is read and written by key with the same two Words that read and write a Vector by index, GET and PUT. Reading or removing an absent key (GET, WITHOUT) projects notFound; HAS? asks presence alone, so a stored NIL is told apart from an absent key. A Record in a leaf or truth operand lifts the Word over its values, keys kept (LANG.COLLECTIONS.LIFT); in a data operand of a Word that reads a Vector it raises the operand ERROR the contract declares, and a Record Word given anything else raises nonRecord. TALLY and GROUP answer Records, keyed by the distinct elements and the keys they bundle by. JSON-DECODE reads JSON text into these domains — an object is a Record, an array a Vector, a number the exact rational it spells, null a NIL — projecting invalidEncoding for text that is not one JSON value and spaceExhausted for nesting past the machine's bound; JSON-ENCODE writes the inverse, spelling a rational with no finite decimal as its lexeme inside a string rather than rounding it, and projects domainMiss for a value with no JSON image.

4. Machine State and Evaluation

LANG.MACHINE.STATE — State

A machine state contains the data stack, the dictionary, the output stream, and the execution controls needed by observable contracts.

Host-only caches, allocation arenas, compiled plans, and counters are not semantic state.

LANG.MACHINE.TRANSFORMERS — Programs

Each executable token denotes a partial state transformer. A program denotes left-to-right composition of those transformers after desugaring and name resolution.

Execution is deterministic relative to the initial state. Optimization may reassociate internal work only when the observable sequence is unchanged.

LANG.MACHINE.WORD — Word contracts

A canonical Word contract selects a semantic family and supplies its differences: stack arity, NIL policy, projection condition and reason, error conditions, purity, determinism, effects, clause links, documentation, and executor key. Determinism classifies what the result is relative to: deterministic from operands alone, state-relative when the wider stack, frame bindings, or dictionary also decide it (LANG.MACHINE.STATE) — a pure Word can still be state-relative, since purity (LANG.EFFECTS.OUTPUT) asks only whether the same stack and dictionary always yield the same result — or host-relative when the host's own rendering, capture, or discard of the effect also decides it (LANG.EFFECTS.OUTPUT).

The executor must refine its contract. Documentation is a projection of the same canonical entry, not an independent semantic authority.

LANG.MACHINE.ORDER — Evaluation order

Token evaluation, output emission, and dictionary mutation preserve their observable order.

LANG.MACHINE.LIMITS — Work limits

A host bounds a run along several axes, and what distinguishes them is not which resource they meter but which of the three outcomes (LANG.FAILURE.TRICHOTOMY) exhausting one produces:

The materialization row differs in kind: a collection too large to build is a well-formed request the host declines, so it projects (LANG.FAILURE.PROJECT), while the other rows are the host refusing to continue at all. Nesting depth and the digits of a number sit in both, by the same rule: a Word asked to build from data a result past the ceiling declines it — a shape of too many axes or JSON text nested too deep (LANG.COLLECTIONS.BUDGET), text spelling too large a number to NUM or JSON-DECODE — while the same size reached any other way — a literal written that deep or that long, or Words wrapping values that already exist — is refused, because no request was made that the host could decline. That split and each row's category are normative; how many ceilings a host divides the last row into, and every numeric value, is implementation freedom. These are safety controls, not semantic constraints — termination already follows from LANG.DICTIONARY.ACYCLIC, so they bound cost rather than decide it.

5. Stack and Consumption

LANG.STACK.ORDER — Stack observation

The stack is an ordered sequence with a distinguished top. A Word takes its operands from the top and returns its results to the top.

A display transformation cannot reorder, coerce, drop, or invent stack values.

LANG.STACK.CONSUMPTION — Consumption

A Word consumes the operands it reads: they leave the stack, and its results take their place. Nothing modifies this, and a Word whose result is empty is no exception — BIND, DEF and DEL consume their operands too. A value used more than once is named with BIND and read by that name as often as it is needed: 5 'N' BIND N N 1 ADD leaves 5 6. Because every call consumes exactly what it reads, writing a User Word's body in place of the Word never changes which operands are consumed, which is what lets a program be expanded into Core Words alone.

A Word selects operands from the top of the stack, validates its registered contract, computes or projects the result, and then consumes its operands. ERROR does not masquerade as a successful NIL projection.

6. Partiality and Failure

LANG.FAILURE.TRICHOTOMY — Value, absence, misuse

Every attempted operation ends in exactly one of three categories:

An implementation must not convert malformed use to NIL and must not raise ERROR merely because a registered partial projection has no value. Recovery operates on absence alone: a program can choose a fallback in place of a NIL, while an ERROR propagates and halts evaluation. A program declares either outcome itself: ABSENT makes a NIL whose reason is the Text it is given, and FAIL raises an ERROR (category declaredFailure) whose message is the Text it is given. A declared ERROR is an ERROR in full — no Word catches it — so the trichotomy is closed against the program as well as against the implementation.

LANG.FAILURE.PROJECT — Projection

A projection condition is a semantic predicate over well-formed inputs. When it holds, the Word produces NIL with the reason its contract registers.

Division by zero, domain exclusion, out-of-range indexing, a value not found where one is sought, failed parsing, and space exhaustion are among the reasons a projection condition keeps distinct — spec/outcomes.json (LANG.AUTHORITY.SOURCES) is the exhaustive list, this clause only fixes how the shared ones behave. A Word's own contract names the reasons that Word projects for, which is a subset: a reason exists in the outcome space whether or not any contract currently reaches it.

LANG.FAILURE.ERROR — Errors

Arity failure, nonconforming type, malformed source, invalid dictionary operation, and an exhausted execution-step limit raise their registered ERROR category.

ERROR halts evaluation and propagates. It is never a truth value and never a stack value.

LANG.FAILURE.PASSTHROUGH — NIL passthrough

What a Word does with a NIL operand follows from what it does with that operand, and from nothing else. Each operand position has one role, declared per Word as stack.operands in spec/words.json. A data or leaf operand is read (a leaf as one Scalar, String or Boolean, lifted over a container, LANG.COLLECTIONS.LIFT): an absent one is the result, flowing to the output position without changing its reason; the primitive does not run, no projection condition is re-run or relabels it, and when several data operands are absent the leftmost is the result. An element is carried without being read (a value stored, bound, printed, encoded or inspected, an accumulator, a needle compared by equality): a NIL there is an ordinary value (LANG.VALUES.NIL). A control operand directs the Word rather than being data it transforms — a block it evaluates, a name it binds, defines, deletes or looks up, or a message it raises: it cannot be absent, so a NIL there is malformed use, raising the condition the Word declares for any other operand that does not belong there, and this is decided before any data operand passes through. A truth operand reads a NIL as UNKNOWN (LANG.VALUES.TRUTH).

A Word's nilPolicy summarises its roles and is never a choice of its own, so two Words that treat an operand alike treat a NIL there alike. A Word of data-dependent arity declares no roles and states its NIL handling in its contract.

LANG.FAILURE.RECOVERY — Recovery

Recovery is a phrase, not a form of its own. NIL? consumes a value and answers whether it is absent, which is what SELECT reads as its truth operand, so a subject named once and read twice chooses between itself and a fallback: subject 'S' BIND fallback S S NIL? SELECT leaves the subject when it is present and the fallback when it is not, the fallback an ordinary operand computed before the choice like every other operand. The question is asked of the whole value: a Vector holding an absent lane is present, so a lane recovered inside a Vector is recovered there rather than around it.

Recovery does not erase absence from already emitted output.

7. Collections and Higher-order Evaluation

LANG.COLLECTIONS.LIFT — Element lifting

A Word applies element-wise wherever it reads an operand as one value: a leaf operand, read as one Scalar, String or Boolean, and a truth operand (LANG.FAILURE.PASSTHROUGH). Given a Vector there, it answers a Vector of its answers for the elements; given a Record, a Record of its answers under the unchanged keys (LANG.RECORDS.STRUCTURE). Every Word lifts by this one rule, arithmetic, comparison, logic and text alike, and a one-element Vector is a Vector there, never its element. A scalar combines with every element of a vector, however that vector is nested, including a ragged one. A Record lifts first: any other operand combines with each of its values, two Records combine value by value when their key sequences are equal, and two whose key sequences differ are a shapeMismatch ERROR.

Two vectors combine by pairing their axes. A vector whose nesting is rectangular has a shape: the lengths of its axes, outermost first. The two shapes are aligned at their innermost axis, and an axis the shorter shape does not reach counts as length 1. Paired axes combine when their lengths are equal, and when one of them is 1 that operand's single lane is reused across the other's length; the result carries the longer length on that axis. This makes a one-element vector combine with a vector of any length, and [ 1 2 3 ] [ 10 ] MUL is [ 10/1 20/1 30/1 ]. Any other pairing is ERROR, and so is any pairing of two vectors where either one is ragged. A program reads this shape with SHAPE, which answers a rectangular vector's axis lengths and, for a ragged one, the reasoned absence domainMiss — a ragged vector has no shape; RESHAPE regroups a vector's leaves, in order, under a shape whose product is their count; FLATTEN collapses every axis into one; DEPTH answers how deeply a value nests, a leaf being 0. The last two cannot be written as user definitions: nesting depth is not known in advance, and a language with no recursion and no unbounded loop cannot walk a structure of unknown depth (LANG.DICTIONARY.ACYCLIC).

Each lane preserves the exactness, truth, NIL, and ERROR distinctions of the scalar law. Vectorization cannot turn an ERROR lane into NIL.

LANG.COLLECTIONS.HIGHER — Higher-order evaluation

MAP, FILTER, FOLD, and SCAN evaluate their code operand (LANG.SOURCE.CODE) once per visited element, in index order, with the block's stack effect isolated to its own operands. A block reaches an inner axis by nesting: [ [ f ] MAP ] MAP applies f one level down.

FOLD and SCAN are one walk over the elements, carrying an accumulator the block rewrites at each one; they differ in which accumulators the walk answers with. FOLD answers the last, so a walk with nothing to visit answers the seed it was given. SCAN answers every one of them, one per visited element and the seed not among them, so a walk with nothing to visit answers no elements and an absent collection answers that same absence. This is the one shape a computation carrying state from one element to the next can take, because a Word cannot call itself (LANG.DICTIONARY.ACYCLIC) and there is no unbounded loop.

Element visitation order is observable where a supplied block can emit output or mutate dictionary state. The block's result is what it leaves on top when it finishes, taken as it stands, whatever domain it is in: a Vector of one element is a Vector of one element (LANG.VALUES.DISJOINT), so [ 1 2 ] [ 1 COLLECT ] MAP answers [ [ 1 ] [ 2 ] ] and no Word unwraps a result on the grounds of its length. A block that finishes having left nothing raises the blockContractViolation its caller's contract registers; leaving more than the result is ordinary and the rest is discarded, because a block may push a bound name or a value it computed along the way, and only its top is the result.

LANG.COLLECTIONS.BUDGET — Materialization

RANGE, FILL, RESHAPE and JSON-DECODE honor the materialization ceiling, and the last three the nesting ceiling as well, since the number of axes a shape names and the depth a JSON text nests are sizes of what they were asked to build. A well-formed request that cannot materialize within them yields NIL with reason spaceExhausted; malformed dimensions remain ERROR.

8. Dictionary and Effects

LANG.DICTIONARY.RESOLUTION — Deterministic lookup

The dictionary has two tiers, and those two are the whole of it. Core holds the 78 canonical Words and is sealed: a Core name cannot be redefined or deleted. User holds definitions made by DEF. Resolution is a deterministic function of the normalized name and the current dictionary, and User never shadows Core. The host's lookup, hover, the Reference, and execution must identify the same canonical entry.

LANG.DICTIONARY.MUTATION — User Words

DEF binds a name to a code block; DEL removes a User Word and fails with ERROR if any other definition still depends on it, and DEF of a name that other definitions still depend on fails the same way (definitionConflict): a caller resolves the name when it runs, so the definition it calls cannot be changed under it, only deleted after the caller is. A definition depends on every User Word its body names, whichever of the two was defined first. A dictionary mutation commits atomically or raises ERROR with no partial visible mutation. A definition is kept as its source: DEF takes any Vector as a body, and a value that body carries whole rather than as written — a Record, an exact irrational, a Vector holding either — is written back as the source that builds it ([ keys ] [ values ] RECORD, the normal form over SQRT, … n COLLECT), so the body the dictionary holds, shows, saves and identifies is one text in every session; a NIL carrying a reason has no source, and a body holding one is refused (invalidDefinitionBody).

Every Word has a content identity: a digest over its normalized definition and the identities of the Words it calls, so a change to a dependency changes the identity of everything that depends on it, and what a Word or its dependencies are named does not reach it. Equal identities mean one Word, which is what lets a host deduplicate by content; unequal identities mean nothing, since two definitions can denote one function and normalize differently (LANG.VALUES.DENOTATION). DIGEST answers that identity for a Symbol naming a Word, and for any other value the digest of its denotation, under the same asymmetry.

LANG.DICTIONARY.ACYCLIC — No definition may name itself

The User dictionary's reference graph is acyclic: DEF raises ERROR rather than commit a definition that names the word being defined, directly or through a chain of other User words, however that name is reached (LANG.SOURCE.FRAME), and BIND refuses a value that names its own binding, directly or through other bindings the frame can see, since a binding is looked up when its Vector runs and would otherwise call itself with no Word in between. Both checks read every Symbol the body or value holds, including one inside a Record or other value a body built from a Vector carries whole, and they are complete because a Word runs only when a Symbol names it: no Word turns text into a Symbol, and a String is not code (LANG.SOURCE.CODE), so a call can never be computed. No Word can call itself, so repetition is only the bounded higher-order Words (MAP, FILTER, FOLD, SCAN) over an already-finite Vector, and every evaluation is structurally finite: termination follows from the dictionary's shape alone, and the execution-step ceiling (LANG.MACHINE.LIMITS) is left to bound cost, not decide it. Ajisai is therefore total and not Turing-complete — a deliberate trade, whose price is that a computation which must run until it converges has to be re-expressed over a finite Vector the program builds first, and whose return is that the language denotes without domain theory: no divergence, so no bottom, no continuity obligation and no fixed-point construction. spec/termination.json carries the argument in full.

LANG.EFFECTS.OUTPUT — Output

Output is the only effect that leaves the machine. PRINT consumes its operand and appends it to the ordered output stream. No other Word emits output, so the output stream is the whole of what a host observes a program doing.

A host may render, capture, or discard the output stream, but may not reorder it or change language-side validation.

A Word may have exactly one other effect, and it stays inside the machine: DEF and DEL change the dictionary, under LANG.DICTIONARY.MUTATION. Output emission and dictionary mutation are therefore the two effects, and LANG.MACHINE.ORDER orders both of them against token evaluation.

Every other Word changes nothing: given the same stack and dictionary it produces the same result. A Word that evaluates a supplied code block has the effects of that block and no others, so it is pure exactly when the block is.

9. Contracts and Static Checking

LANG.CONTRACT.REGISTRY — Machine-readable contracts

Every Core Word's contract is a machine-readable record in spec/words.json, conforming to spec/words.schema.json. The record is the single place a Word's arity, NIL policy, projection reason, error conditions, purity, and documentation are stated.

Prose that restates a contract is a projection of that record and carries no independent authority. CONTRACT answers the record from inside the language, as a Record keyed by those fields, for a Symbol naming a Core Word; for a User Word, or for a block of code, it answers the inferred contract of LANG.CONTRACT.CHECK in one shape, and for a Symbol naming nothing it projects notFound.

LANG.CONTRACT.CHECK — Pre-execution check

A user definition may carry a declaration of its own contract, written as the keys of a contract Record with the values those keys take — inputs, outputs, purity, partiality, determinism and cost. The inferred contract answers every key a registered contract also carries in the registry's own vocabulary, so a declaration, an inference and a Core Word's record state one fact one way. ajisai check --contract verifies that declaration against the Core contracts of the Words it calls, without running the program. CONTRACT reaches the same inference from inside the language, over a Vector of code (LANG.SOURCE.CODE) or the name of a User Word: it never evaluates its operand, so calling it carries none of the operand's own effects. Its answer is a Record whose confidence and gaps carry the three outcomes below as data.

The check is deliberately conservative and partial. It reports exactly three outcomes per declaration, each the trichotomy of LANG.FAILURE.TRICHOTOMY applied at check time rather than at run time:

Anything outside the syntactic fragment the inference analyzes — a higher-order body whose block is not statically known, or dynamic control — is reported as cannot verify and is never silently passed. A tool that reports verified for an unanalyzable body is nonconforming.

The correspondence classifies outcomes, not mechanisms, and does not make the check evaluate the program: division by zero, a failed parse and an out-of-range index already share one outcome category while sharing no mechanism, and an inference that could not decide joins that list on the same terms.

10. Observation and Host Protocol

LANG.OBSERVATION.PROJECTIONS — Observable surfaces

Ajisai exposes four projections: Input, Output, Stack, and Dictionary. Presentation may tile or select them according to the Presentation Profile, but their language-side contents are determined here.

LANG.OBSERVATION.PROTOCOL — The host protocol

One recursive node shape observes every stack value, rendered by a single serializer shared across hosts (spec/host-protocol.schema.json): a type naming the value's domain (LANG.VALUES.DISJOINT's seven domains as seven wire types — nil, boolean, number, string, vector, symbol, and record, the last carrying its aligned key and value sequences as two arrays of nodes), a value shaped by that type, and an optional semantics bag carrying a Boolean's truth, a NIL's absence reason, and an irrational's exact terms. Every field is derived from the value itself, never from the Word that produced it (LANG.VALUES.DENOTATION). The CLI/MCP agent surface wraps an array of these nodes in its own JSON envelope (docs/dev/agent-cli-output-contract.md, non-canonical); the WASM/GUI boundary exposes the same nodes directly from its own methods, with no enclosing envelope of its own. It is the only structured channel through which anything outside the language observes the stack; a text rendering such as the CLI's stackDisplay is a view of these nodes, not a second protocol. The schema is enforced: the MCP self-test validates every stack the live server returns against it.

No version field exists on this node shape today: the CLI envelope around it carries its own plain integer schemaVersion, and the WASM boundary carries no version signal at all, so a breaking change to the shape this clause fixes would be silent until one is added. Existing field deletion, rename, semantic change, and tuple reorder or reshape remain forbidden regardless: an implementation offers exactly one protocol.

LANG.OBSERVATION.FIREWALL — Semantic firewall

External consumers branch only on published protocol axes. They do not branch on Rust types, debug strings, display text, internal numeric form, or incidental GUI state.

The GUI never infers exact equality, stack effect, resolution, or absence reasons on its own.

LANG.OBSERVATION.DIAGNOSIS — Diagnosis

An ERROR carries a stable category identifier and a human-readable message; a NIL carries its reason. Those identifiers are the machine-readable surface, and human wording may evolve only where they are preserved.

11. Conformance

LANG.CONFORMANCE.CORPUS — Executable correspondence

The conformance corpus links each case to one or more clause IDs and compares stack, output, dictionary state, and diagnosis identifiers. An implementation is Ajisai when it preserves the source-to-observation correspondence for every case.

The corpus is the decision procedure for the question "is this Ajisai?". No prose answers it.

LANG.CONFORMANCE.FAMILIES — Family laws

Every semantic family has law tests for arity, consumption, NIL policy, projection, ERROR boundaries, lifting, purity, and effects as applicable. Every Word contract has at least one conformance path to its family and clause IDs.

LANG.CONFORMANCE.CHANGE — Change discipline

A semantic change begins in one authoritative source, regenerates all derived surfaces, updates clause-linked conformance cases, and demonstrates unchanged observations unless the change is explicitly versioned.

Presentation Profile

Current GUI contract

Presentation ranks below the language semantics: a conforming Ajisai need not present any surface visually, and a host with no display still defines the four observation projections. What follows is the contract the current Web and Tauri GUI realizes, stated concretely rather than as a formal system.

The GUI has four named surfaces: Input, Output, Stack, and Dictionary. Desktop presentation uses two columns (Input or Output on the left; Stack or Dictionary on the right), while mobile presentation exposes one selected surface at a time.

The operations Run, Step, Abort, and Reset retain their current behavior. The desktop shortcuts are respectively Shift+Enter, Ctrl+Enter, Escape, and Ctrl+Alt+Enter; Format is Shift+Alt+F, Stack clear is Ctrl+Alt+S, Editor clear is Ctrl+Alt+E, and Lookup is Ctrl+Alt+L. The mobile presentation has Run as a triple-tap on the Input surface, and Format, Stack clear, and Editor clear as controls in their own surfaces; Step, Abort, Lookup, and Reset are reachable there only from an attached keyboard, and the Input surface's own text says so. Stack clear discards the stack's values and leaves the dictionary — that is what distinguishes it from Reset. Editor clear discards only the Input surface's typed text, leaving the stack, the dictionary, and everything else untouched. Output copy and focus behavior, Core/User dictionary sheets, search, deletion, canonical stack display, opt-in LaTeX display, nested-vector bracket coloring, stack snapshots, and persistence of user words are compatibility requirements.

Editing affordances. These too retain their current behavior. A Run that ends OK empties the Input surface, and the submitted programs of the session are recalled into it with Ctrl+↑ (older) and Ctrl+↓ (newer); a Run that fails leaves its text in place. A click on a Dictionary word writes that word into the Input surface, with a space between it and any name it would otherwise run into; a click on the space between the word buttons writes a space, and a double-click there takes the last word back. Each of these is an ordinary edit of the Input surface, taken back with the platform's undo. A User Word is deleted from its button's context menu. User Words are exported to and imported from a file with the Dictionary surface's Export and Import controls. On desktop, Run is Shift+Enter alone: a triple-click on the Input surface selects the line, as it does in any text field, and does not run the program. A double-click on the Output surface returns the left column to Input. A #code= fragment in the page address preloads the Input surface with that text. On mobile, a swipe changes surface, a double-tap on Stack shows Output, and a double-tap on Output shows Input.

The Stack surface reads in ordinary reading order: top to bottom, left to right, with the top of the stack last. The top of the stack is marked, so the value the next Word reads is identifiable without counting, at any number of values and whatever the wrapping.

Operations without a typed spelling. Reset, Stack clear, Editor clear, and Lookup are reached by a shortcut or a control and have no typed spelling; none of them can be typed into the Input surface and run. This is deliberate in both directions: the vocabulary holds nothing that throws away the values a program was handed, the text it was typed as, or the dictionary it was defined in, and the Input surface holds nothing but the program being written. A name typed there — including RESET, STACK-CLEAR, or EDITOR-CLEAR — resolves as an ordinary program, exactly like any other name, and is a User Word or an unknown word like any other.

Lookup resolves the word at the current cursor position in the Input surface against the current dictionary and answers without running anything, always in the Output surface: a Core Word's reference text and a User Word's reconstructed DEF source are shown the same way, as prose to read rather than text loaded back for editing. The cursor can be anywhere in a program still being written, so nothing about a lookup may overwrite the Input surface. A name the dictionary does not hold is reported as an unknown word. This too is deliberately not a Word: reference prose is not a value, no program can do anything with the answer, and a Word whose entire result reached the output rather than the stack would be claiming otherwise. The lookup observes and changes nothing — the stack, the dictionary, and the Input surface are the same afterwards — and it must identify the same canonical entry that hover, the Reference, and execution do.

Four rules are normative, because each ties what is shown, or what can be reached, to what the user is doing rather than to geometry:

1. Every surface stays reachable. A hidden surface is concealed, never destroyed, and some finite sequence of operations exposes it again from any state.
2. Editing and execution are observable. Any state in which source text can be entered shows Input, and a Run shows each surface it changed, so what it produced is surfaced: on desktop a changed Output takes the left column and a changed Stack or Dictionary the right (Dictionary before Stack); on mobile, which shows one surface, the first changed of Dictionary, Output, Stack. A Run that changed nothing leaves the presentation as it was.
3. At least one surface is always visible. The user is never shown nothing.
4. Nothing a surface is reached by goes unsaid. A gesture is invisible — no control on screen shows that it exists — so wherever a surface can only be reached, or an operation only run, by a gesture or a shortcut, that surface says so in its own text, and what it says stays readable at the moment it is needed. This is a rule about telling, deliberately not a rule about supplying a control for everything: a control is not free, it is taken out of the surface it sits on, and an editor shrunk to a third of itself to seat a row of buttons has paid more than the buttons were worth. Where the cost is not worth paying, the operation may stay on a shortcut the surface names and a keyboard reaches.

Everything else — column geometry, the breakpoint at which the layout switches, which control sits where, gesture thresholds, tap counts — is tuning, not semantics, and has the same standing as the execution step limit: a host control rather than a language constraint.

The GUI consumes the current host protocol and does not independently decide exact-real equality, Word stack effects, dictionary resolution, absence metadata, or numeric representation. Web and Tauri platform adapters may supply capabilities, but may not change language observations. Existing accessibility names, focus paths, keyboard operation, and panel transitions are part of this GUI contract.