Terms and Definitions

The defining vocabulary on which the normative requirements of this specification rest. Each term is defined here and specified in full in the chapter cited.

For the purposes of this specification, the following terms and definitions apply. A term in bold at its point of definition carries the meaning given here throughout the document; where a later chapter is cited, that chapter is the full normative specification of the term and this entry is its capsule definition.

This clause is normative: a requirement stated elsewhere in terms of these words means exactly what is defined here. Where a term has a broader meaning in general usage, only the meaning given here applies within this specification.

Process and conformance

conforming implementation — an implementation that satisfies all requirements of this specification applicable to it. Defined in Conformance §3.

conforming program — a Clef program that violates no diagnosable rule of the language. Defined in Conformance §4.

normative — imposing a requirement. informative — explanatory, imposing no requirement. The distinction is defined in Conformance §2 and governs every clause and note.

implementation-defined behavior, unspecified behavior, undefined behavior — the three classes of behavior not fully fixed by this specification, defined and distinguished in Behavior Classification.

Compiler architecture

CCS (Clef Compiler Services) — the front end that elaborates Clef source, builds and saturates the program graph, and discharges design-time obligations. Introduced in Introduction.

Composer — the compiler that lowers the saturated graph through its middle end to target backends. Distinct from CCS (the front end) and from any one backend.

target pathway — a target-committing serialization pathway off the portable middle end; the point at which a target commitment is made and an artifact class is fixed. The LLVM pathway (CPU/MCU), the CIRCT pathway (FPGA), the MLIR-AIE pathway (NPU tile arrays), and the JSIR pathway (JavaScript) are target pathways. Defined in Backend Lowering Architecture.

Alex — the Composer middle-end component that witnesses the saturated graph and lowers it to MLIR; the “Library of Alexandria” that holds the platform-resolving lowerings. Introduced in Backend Lowering Architecture.

Baker — the saturation engine that settles the program graph into its saturated form, expanding constructs that have no single machine instruction.

nanopass — an elaboration or lowering pass of small, single-purpose scope; the front end and middle end are composed of nanopasses.

witness — a component that consumes an enriched graph node and emits the lowered form (e.g. an IntrinsicWitness); witnesses pattern-match on graph structure, not on names.

Program structure carriage

Program Semantic Graph (PSG) — the graph carrying a program’s structure and its design-time facts (dimensions, ranges, grades, coeffects, escape classes) as annotations, preserved through lowering. Defined in Program Semantic Graph.

Program Hypergraph (PHG) — the PSG extended with explicit relations over ordered participant occurrences, retaining joint premises, provenance, and conclusions alongside the computational spine. Hyperedges directly represent relationships such as a shared capacity budget or an ordered geometric operation; equivalent binary encodings require the corresponding relation structure. Defined in Program Hypergraph.

coeffect — context a computation requires, carried as codata on the graph beside the value (as distinct from an effect a computation produces). Representation selection, memory residency, and the quire allocation are carried as coeffects.

codata — data attached to a graph node and preserved through passes that do not touch it; the carriage mechanism for coeffects and inference results.

Types and dimensions

dimensional type — a type carrying a dimension drawn from a finitely generated free abelian group of base dimensions with integer exponents. Defined across Units of Measure and NTU Dimensional Architecture.

dimension versus range — a value’s dimension establishes its kind (e.g. meters); its range [a, b] establishes the concrete interval it occupies. Numeric selection takes the range, not the dimension, as its input. See Numeric Selection §1.

grade — the algebraic grade (scalar, vector, bivector, …) of a value in the geometric/Clifford algebra; a structural property the type system preserves.

Foreign boundaries

foreign boundary — an interface at which values enter or leave Clef’s type universe. Each boundary confines its own absence sentinels to its boundary conversions and admits values inward only through declared conversions. The C instance is defined in FFI Boundary Semantics; the JavaScript instance in JavaScript Boundary Semantics.

narrowing — the sole elimination of a foreign dynamic value: a generated, schema-directed check converting the value to a declared Clef type, total over its input, returning Result with the failed premise identified on failure. Defined in JavaScript Boundary Semantics §3.2.

boundary grade — the capability coeffect recording contact with the foreign pair (JsValue, JsRef<'T>), carried in signatures and composed in the lattice family; grade zero is proven freedom from foreign contact. Defined in JavaScript Boundary Semantics §4. Unrelated to the algebraic grade above.

Numeric representation

representation — the machine form chosen for a real value: a posit, an IEEE-754 float, or a fixed-point number. Selected from the value’s range, per target. Defined in Numeric Selection.

numeric selection — the compile-time function choosing a real value’s representation from its analyzed dimensional range. The real-valued counterpart of width inference.

width inference — the compile-time function sizing an integer from its value range. The integer counterpart of numeric selection. Defined in Width Inference.

regime — a classification of a value’s range into a representation family (e.g. near-unity-taper, wide-dynamic), the categorical output of selection prior to a concrete representation.

posit, b-posit — a tapered-precision real representation (Gustafson); b-posit is the bounded-regime variant. Precision is maximal near magnitude 1.0 and tapers toward the extremes. (Posits do not carry extra precision near zero; the value of the quire is exactness of accumulation, not near-zero precision.)

quire — a wide fixed-point accumulator that holds a sum of products without per-step rounding, rounding once at final conversion; provides exact accumulation. Defined in Numeric Selection §10.2.

coverage — the requirement that a representation’s dynamic range contain a value’s range. A non-covering representation SHALL NOT be selected, and an empty coverage set is a hard error. See Numeric Selection §2.1.

Memory and concurrency

escape class — the classification (e.g. stack-scoped, closure-capture, return-escape, by-ref-escape) of where an allocation’s lifetime reaches, determining its placement. Defined in Memory Regions and Access Kinds.

arena — a region whose entire contents are reclaimed as a unit when its owner (e.g. an actor) terminates.

actor — a unit of concurrency with private state, a single logical thread, and no shared mutable state; communication is by message only. The Clef actor execution is realized by Olivier (the actor runtime) under Prospero (the supervisor), with dispatch by Ariel (the scheduler).

wait-for edge — an edge from a caller to a callee that a synchronous reply suspends on; the relation whose acyclicity is deadlock-freedom. Defined in Synchronous RPC and Wait Classification.

scheduler — the component that selects which ready actor executes next and delivers each resume; realized by Ariel under the contract supervision takes as premises: fairness, turn discipline, control-plane immunity, admission, and determinism. Defined in Scheduler Contract.

turn — the execution of an actor from one scheduling event (a resume) to its next suspension, completion, or fault; the unit of dispatch, run to completion. Defined in Scheduler Contract.

Verification

tier — an organizational level of the verification architecture. Tier 1 covers admitted structural inference; Tier 2 covers local analysis and supported solver fragments, including QF_LIA, QF_LRA and QF_BV; Tier 3 covers parameterized domain and system theorem applications, including supported concurrent, distributed, termination and probabilistic results; Tier 4 covers relational judgments about executions, distributions or realizations. Each procedure has its own admitted domain and checking requirements. A tier does not by itself establish decidability, a latency bound or a trusted computing base. Evidence may compose between tiers under Conformance §6.1.

seal — an explicit developer commitment of a concrete representation at a site, turning the selection objective from a chooser into a coverage checker. Defined in Numeric Selection §5.