relation references as a term kind, written #Name

3 files changed, 79 insertions, 4 deletions

diff --git a/docs/language-specification.org b/docs/language-specification.org
index 639e8d6..602d3d4 100644
--- a/docs/language-specification.org
+++ b/docs/language-specification.org
@@ -60,6 +60,7 @@ The core lexical categories are:
 - literals (ground scalars)
 - records (tuple literals)
 - sequences (list literals)
+- references (relation-denoting values, =#Name=)
 - blocks (membership propositions)
 - logical combinator messages as labels
 
@@ -227,6 +228,31 @@ sequence of propositions (e.g. a schema's fact list) also uses
 =#( ... )=: it is honestly a sequence whose elements happen to be
 blocks.
 
+** References
+
+A reference is a first-class value denoting a relation by name,
+written with the Smalltalk symbol notation:
+
+#+BEGIN_SRC sol
+#Person
+#Increment
+#+END_SRC
+
+A reference is a term, not a proposition: it names a relation as
+data, resolved through the catalog of a state. It is deliberately
+distinct from a string (a string is inert; a reference resolves) and
+from a variable (an uppercase bare name in term position stays a
+variable). Wherever a relation must appear as an argument, the
+reference is the value: transition relations
+(=[Insert relation: #Person ...]=), higher-order relations
+(=[Map relation: #Increment ...]=), and the attributes of the
+catalog relations themselves.
+
+Because a reference variable ranges over the catalog, which is
+finite, an unbound reference is boundedly enumerable: the
+higher-order restriction becomes ordinary cardinality analysis
+rather than a prohibition.
+
 ** Blocks
 
 Blocks — square brackets — delimit exactly one thing: membership
diff --git a/docs/sakura-RNT-integration.org b/docs/sakura-RNT-integration.org
index 8207ee5..2df3892 100644
--- a/docs/sakura-RNT-integration.org
+++ b/docs/sakura-RNT-integration.org
@@ -778,6 +778,55 @@ elaboration (fresh variable plus flat conjunct). The privilege must
 be explicit and queryable, never assumed from position. Until a real
 program hurts without it, it is not built.
 
+* Decision 15: Relation References Are a Term Kind, Written #Name
+
+** The decision
+
+A relation reference is a first-class ground value denoting a
+relation by name, written with the Smalltalk symbol notation:
+
+#+BEGIN_SRC sol
+[Insert relation: #Person tuple: {name: "Ana" age: 12} before: S after: S2]
+#+END_SRC
+
+It is a new lexical kind, distinct from variables, strings, and
+propositions. A reference denotes the *catalog entry* resolved at a
+state, not an extension: two states where =Person= holds different
+tuples share the reference. Wherever a relation must appear as data,
+the reference is the value: transition arguments, higher-order
+arguments (=[Map relation: #Increment ...]=), and the attributes of
+the catalog relations themselves (decision 11).
+
+** The alternatives rejected
+
+- *Strings* (=relation: "Person"=): a conflation. The text and the
+  relation are different things with different semantics; a string
+  is inert, a reference resolves against a catalog at a state.
+  Identity is not representation (decision 12's own diagnosis).
+- *Context-resolved atoms* (=relation: Person= with the loader
+  special-casing certain argument positions): position-dependent
+  meaning of one spelling, the exact dishonesty the delimiter law
+  forbids, over an open set of special positions.
+
+** What it buys
+
+- P1 (honesty). Different semantics get a visibly different form.
+- P2 (decision 11). "You may only insert into a relation that
+  exists" stops being transition machinery and becomes an ordinary
+  foreign key into the catalog, checked at the =before:= state.
+- P3 (higher-order, grounded). A reference variable ranges over the
+  catalog, and the catalog is finite: an unbound relation variable
+  is *bounded generation*, admissible like =Between=. The
+  specification's higher-order restriction becomes ordinary
+  cardinality analysis instead of a prohibition.
+
+** Acknowledged costs
+
+- A new lexical category through the whole pipeline: token, term
+  and pattern kind, checker leaf, printing.
+- The resolution semantics (reference = name resolved through the
+  catalog of a state) must be respected by every world.
+
 * Consequences for the Pending Documents
 
 - =docs/core-design-and-pipeline.org= must treat transition relations
diff --git a/docs/states.org b/docs/states.org
index 7849918..aa5c507 100644
--- a/docs/states.org
+++ b/docs/states.org
@@ -38,16 +38,16 @@ tip, which is the elaboration rule of decision 7 for bare queries.
 =Insert= is a relation between states:
 
 #+BEGIN_SRC sol
-[Insert relation: "Person" tuple: {name: "Ana" age: 12} before: S1 after: S2]
+[Insert relation: #Person tuple: {name: "Ana" age: 12} before: S1 after: S2]
 #+END_SRC
 
 It holds when the successor of =S1= by admitting that tuple is =S2=.
 The tuple must match the relation's schema exactly and satisfy its
 domains, or there is no such transition: integrity is part of the
 relation, not a hook bolted on. Solving computes successor states
-and binds them; nothing moves. The relation name is a string for
-now, a provisional notation until relation references in term
-position get their own decision.
+and binds them; nothing moves. The relation is named by a reference,
+=#Person=, per decision 15: a dangling reference is simply no
+transition.
 
 Sequencing is the chain: =before: S1 after: S2= in one application,
 =before: S2= in the next. Conjunction stays commutative; the order