language specification document

1 files changed, 1336 insertions, 0 deletions

diff --git a/docs/language-specification.org b/docs/language-specification.org
new file mode 100644
index 0000000..9158130
--- /dev/null
+++ b/docs/language-specification.org
@@ -0,0 +1,1336 @@
+#+TITLE: Sol Language Specification
+#+AUTHOR: Marcos Magueta
+
+* Introduction
+
+Sol is a total (from [[https://en.wikipedia.org/wiki/Total_functional_programming][totality]]) relational language inspired by Prolog,
+Coq, relational algebra, constraint logic programming, and
+message-oriented syntax of Smalltalk.
+
+The central idea of Sol is that relations are the primary semantic
+objects of the language. Types are not separate from logic. Rather,
+types are relations used as membership constraints. A program in Sol
+is therefore not primarily a sequence of instructions, but a
+structured logical expression made from relation unifications,
+conjunctions, constraints, and rules.
+
+Sol is intentionally not Turing complete, but still expressive. Its
+purpose is not to express arbitrary machine computation, but achieve
+something close through dependent relational typing. There's a large
+set of problems that can still be solved even if the language is not
+turing complete. For example: arithmetic, data structure algorithms,
+parsers, compilers, theorem provers, symbolic manipulators, certified
+interpreters, graph algorithms, sorting, balancing trees, type
+checkers, relational evaluators and normalization procedures; so long
+as their structures can be normalized and the whole can be proven
+total.
+
+In other words, Sol is a language that has no mu-recursion (unbounded
+minimization), instead implementing primitive recursion through
+fixpoint; while not having partial expressions.
+
+* Core Design Intention
+
+Sol is designed around the following principles:
+
+- Relations are the primary objects
+- Types are relations
+- Domains are unary relations (to represent atomicity) with special
+  operational capabilities
+- Explicit conjunction and disjunction
+- Joins happen through unification
+- Variables are logical unknowns
+- Infinite domains are membership constraints by default, not
+  enumerators, but can be enumerated as subsets
+- Totality is mandatory
+- Execution is proof search, constraint propagation, and
+  normalization
+- Syntax should remain Smalltalk-like: atoms, labels ending in colons,
+  literals, variables, and blocks.
+
+* Lexical Categories
+
+Sol keeps the surface syntax deliberately small.
+
+The core lexical categories are:
+
+- atoms
+- labels
+- variables
+- literals (ground scalars)
+- records (tuple literals)
+- sequences (list literals)
+- blocks (membership propositions)
+- logical combinator messages as labels
+
+Each delimiter has exactly one role, and the roles do not overlap:
+
+| Delimiter          | Role                                        |
+|--------------------+---------------------------------------------|
+| =[ ... ]=          | membership proposition (relation application) |
+| ={ ... }=          | record (labeled tuple) term                 |
+| =#( ... )=         | sequence (list) term                        |
+| =( ... )=          | grouping of a relational expression         |
+
+A =[= never opens a list, a ={= never opens a proposition, and
+grouping never uses square brackets.
+
+** Atoms
+
+Atoms name relations, domains, query forms, and other language-level receivers.
+
+Examples:
+
+#+BEGIN_SRC sol
+Integer
+Person
+Adult
+Plus
+Length
+Query
+Relation
+#+END_SRC
+
+Atoms begin with lowercase or uppercase letters, but by convention relation names are capitalized.
+
+** Labels
+
+Labels are attribute names ending or beginnign with a colon.
+
+Examples:
+
+#+BEGIN_SRC sol
+value:
+left:
+right:
+result:
+name:
+age:
+person:
+list:
+#+END_SRC
+
+Labels are not positional argument markers. They name the attributes
+of a relation.
+
+For example:
+
+#+BEGIN_SRC sol
+[Plus left: X right: Y result: R]
+#+END_SRC
+
+means that the relation =Plus= has labeled attributes =left=, =right=,
+and =result=.
+
+** Variables
+
+Variables begin with uppercase identifiers, just like atoms. We
+distinguish them by context.
+
+Examples:
+
+#+BEGIN_SRC sol
+  X
+  Y
+  R
+  PersonId
+  Age
+  Tail
+  Partial
+#+END_SRC
+
+Variables are logical variables. They may be unified with literals,
+other variables, or structured values.
+
+Variables are not assigned procedurally. They are constrained by
+relation "applications".
+
+** Literals
+
+A literal is not a separate ontological category. Every literal is
+canonical notation for a member of some domain — a tuple inhabiting a
+domain relation.
+
+Examples:
+
+#+BEGIN_SRC sol
+  0
+  1
+  22
+  "Sun"
+  1/4
+  #()
+#+END_SRC
+
+- =123= denotes a member of the =Integer= domain;
+- ="Sun"= denotes a member of =String=;
+- =1/4= is one token (no interior whitespace), denoting the tuple
+  ={numerator: 1 denominator: 4}= as a member of =Rational= — the
+  constraint that the denominator is a nonzero integer is a
+  membership criterion on that tuple, where it belongs;
+- =#()= denotes the empty sequence.
+
+Composite values are labeled tuples of members, uniformly. The
+recursion bottoms out at ground scalars (integers, strings, and
+kin), whose membership is decided by the host world's builtin
+membership criteria (see Membership Criteria).
+
+** Records
+
+A record is the written form of a labeled tuple — the central
+semantic object of the language:
+
+#+BEGIN_SRC sol
+{name: "Marcos" age: 30}
+
+{numerator: 1 denominator: 4}
+
+{head: H tail: T}
+#+END_SRC
+
+A record is a *term*: it asserts nothing. A membership proposition
+=[R l1: t1 l2: t2]= is precisely the assertion that the record
+={l1: t1 l2: t2}= belongs to the relation =R=. Relation application
+is therefore record-plus-membership, and this elaboration is
+normative:
+
+#+BEGIN_EXAMPLE
+[R l1: t1 ... ln: tn]   ≡   {l1: t1, ..., ln: tn} ∈ R
+#+END_EXAMPLE
+
+Label order in records is irrelevant, as in applications.
+
+** Sequences
+
+A sequence is list-literal sugar, written =#( ... )= (after
+Smalltalk's array literal):
+
+#+BEGIN_SRC sol
+#()
+
+#(1 2 3)
+
+#(Head | Tail)
+#+END_SRC
+
+Its elaboration into tuples is normative: a nonempty list is the
+tuple ={head: H tail: T}=, and the empty list is the distinguished
+member =#()=, so
+
+#+BEGIN_EXAMPLE
+#(1 2 3)        ≡  {head: 1 tail: {head: 2 tail: {head: 3 tail: #()}}}
+#(Head | Tail)  ≡  {head: Head tail: Tail}
+#+END_EXAMPLE
+
+=#(Head | Tail)= is thus a tuple pattern, not a special form. A
+sequence of propositions (e.g. a schema's fact list) also uses
+=#( ... )=: it is honestly a sequence whose elements happen to be
+blocks.
+
+** Blocks
+
+Blocks — square brackets — delimit exactly one thing: membership
+propositions (relation applications). They are never list literals,
+never grouping, never sequences.
+
+Examples:
+
+#+BEGIN_SRC sol
+[Integer value: X]
+
+[Plus left: X right: Y result: R]
+#+END_SRC
+
+Grouping of a relational expression, where precedence demands it,
+uses parentheses:
+
+#+BEGIN_SRC sol
+([Integer value: X] :and [LessThanEqual left: X right: 120])
+#+END_SRC
+
+A relation, just like other structures, should be understood as an
+object (we will talk about secondary types), and as such, it should be
+able to support messages such as composition with logical combinators,
+like =:and= or =:or=. Notice that such combinators are different
+labels, given their orientation of colon. They are used for messages
+to objects, in this case, =Relation=.
+
+* Relation Application Syntax
+
+A relation application has the form:
+
+#+BEGIN_SRC sol
+[Relation label: Term label: Term ...]
+#+END_SRC
+
+Examples:
+
+#+BEGIN_SRC sol
+[Integer value: X]
+
+[Person id: P name: "Damian" age: A]
+
+[Plus left: X right: Y result: R]
+#+END_SRC
+
+The order of labels should not matter semantically, provided the
+labels are unique and recognized by the relation schema. The internal
+representation should be closer to a labeled record/map than to a
+positional tuple.
+
+Thus these should normalize to the same relation application:
+
+#+BEGIN_SRC sol
+[Plus left: X right: Y result: R]
+
+[Plus result: R right: Y left: X]
+#+END_SRC
+
+* Conjunction
+
+Conjunction is expressed explicitly with the message =:and=.
+
+Example:
+
+#+BEGIN_SRC sol
+  [Integer value: X] :and [Integer value: Y] :and [Plus left: X right: Y result: R]
+#+END_SRC
+
+This means:
+
+#+BEGIN_EXAMPLE
+  Integer(X) ∧ Integer(Y) ∧ Plus(X,Y,R)
+#+END_EXAMPLE
+
+There is no implicit newline-based conjunction in the core syntax, and
+this is important, as the following should not be treated as a
+conjunction merely because two expressions are adjacent:
+
+#+BEGIN_SRC sol
+  [Integer value: X]
+  [Integer value: Y]
+#+END_SRC
+
+Instead, conjunction must be explicit:
+
+#+BEGIN_SRC sol
+  [Integer value: X] :and
+  [Integer value: Y]
+#+END_SRC
+
+* Query Syntax
+
+A query is a named wrapper around a relational expression. The result
+of a query itself is another relation object, that is in turn
+constructed atop of the other relations through conjunction.
+
+Example:
+
+#+BEGIN_SRC sol
+  Query expression:
+    [Integer value: X] :and
+    [Integer value: Y] :and
+    [Plus left: X right: Y result: 10]
+#+END_SRC
+
+This means:
+
+#+BEGIN_EXAMPLE
+∃ X Y .
+  Integer(X) ∧ Integer(Y) ∧ Plus(X,Y,10)
+#+END_EXAMPLE
+
+The query body is not a sequence of statements, it is one relational
+expression, built from relation applications and logical combinators.
+
+* Joins Through Unification
+
+Joins are expressed by sharing variables across relation
+applications. We can say that conjunctions with unifications are
+joins.
+
+Example:
+
+#+BEGIN_SRC sol
+Query expression:
+  [Person id: P name: "Marcos"] :and
+  [Adult person: P]
+#+END_SRC
+
+The shared variable =P= is the join point.
+
+Semantically:
+
+#+BEGIN_EXAMPLE
+∃ P .
+  Person(id=P, name="Marcos")
+∧ Adult(person=P)
+#+END_EXAMPLE
+
+No explicit join operator is necessary.
+
+* Domains as Unary Relations
+
+Domains are unary relations with special operational capabilities. A
+domain is not fundamentally separate from a relation, it is a relation
+with one principal attribute =value:=.
+
+Domains may support different modes:
+
+- membership checking
+- constraint attachment
+- literal validation
+- optional bounded generation
+
+However, domains do not enumerate by default, as they are potentially
+aleph zero in cardinality.
+
+Example:
+
+#+BEGIN_SRC sol
+  [Integer value: X]
+#+END_SRC
+
+means:
+
+#+BEGIN_EXAMPLE
+X ∈ Integer
+#+END_EXAMPLE
+
+or:
+
+#+BEGIN_EXAMPLE
+Integer(X)
+#+END_EXAMPLE
+
+* Infinite Domains
+
+A crucial distinction in Sol is between membership and generation.
+
+The expression:
+
+#+BEGIN_SRC sol
+  [Integer value: X]
+#+END_SRC
+
+does not mean:
+
+#+BEGIN_EXAMPLE
+Generate every integer X.
+#+END_EXAMPLE
+
+It means:
+
+#+BEGIN_EXAMPLE
+Constrain X to be an integer.
+#+END_EXAMPLE
+
+This is essential for totality, as the same applies to other countably
+infinite domains:
+
+#+BEGIN_SRC sol
+  [Rational value: Q]
+
+  [String value: S]
+
+  [List element: Integer value: XS]
+#+END_SRC
+
+These expressions constrain membership, and do not automatically
+enumerate all possible inhabitants. Generation must be explicit and
+controlled by the language. For example, a future generation form
+might look like:
+
+#+BEGIN_SRC sol
+  [Generate domain: Integer value: X]
+#+END_SRC
+
+However unbounded generation over infinite domains should either be
+rejected, delayed, bounded, or placed outside the total fragment (a
+subset).
+
+* Relation Schemas
+
+A relation has a schema: a set of accepted labels and their expected
+domains. A possible declaration form:
+
+#+BEGIN_SRC sol
+Relation named: Person schema: #(
+  [name domain: String]
+  [age domain: ([Natural value: X] :and [LessThanEqual left: X right: 120])]
+)
+#+END_SRC
+
+This declaration says that =Person= admits the labels:
+
+- =name:=
+- =age:=
+
+and that each attribute is constrained by its declared domain
+criterion: =name:= by membership in =String=, and =age:= by the
+refinement "a =Natural= at most 120".
+
+This declaration syntax is provisional, but it should obey the same
+principle as the rest of Sol: internal bodies should be explicit
+relational expressions, not implicit statement sequences. In this
+definition, we are dealing with a list of facts, not with a single
+expression, hence the sequence =#( ... )= — visibly a sequence whose
+elements are propositions, not itself a proposition.
+
+* Rules
+
+A rule defines one relation in terms of another relational
+expression. A possible rule form:
+
+#+BEGIN_SRC sol
+  Rule name: "Adult is a person with age greater than 18"
+       head: [Adult person: P]
+       body: [Person id: P age: A] :and
+             [GreaterEqual left: A right: 18]
+#+END_SRC
+
+This means:
+
+#+BEGIN_EXAMPLE
+Adult(P) ⇐ Person(P,A) ∧ GreaterEqual(A,18)
+#+END_EXAMPLE
+
+The body is explicitly a conjunction.
+
+It is not written as:
+
+#+BEGIN_SRC sol
+  Person id: P age: A
+  GreaterEqual left: A right: 18
+#+END_SRC
+
+because that would reintroduce implicit sequencing.
+
+* Operational Capabilities
+
+Relations may declare operational capabilities.
+
+For example:
+
+#+BEGIN_SRC sol
+Relation named: Plus capabilities: #(
+  [Capability name: evaluate]
+  [Capability name: solve]
+  [Capability name: constrain]
+)
+#+END_SRC
+
+The exact declaration syntax is provisional, but the semantic idea is
+important.
+
+A relation may support:
+
+- membership checking :: given a tuple (eg [left: 1 right: 2 result:
+  3] is of type Plus) see if it belongs to the relation
+- evaluation
+- backward solving
+- symbolic constraint propagation
+- finite enumeration
+- bounded generation :: for infinite generators, we must only operate
+  on subsets when enumerating, from for example a higher order
+  predicate Take[predicate: P many: N]
+- rewriting
+- normalization
+
+Operational capabilities are not the relation's meaning. They are the
+allowed ways the runtime may use the relation during proof search.
+
+* Modes
+
+Sol should not require ordinary query syntax to annotate every
+argument as input or output.
+
+Instead of writing =+= for inputs and =-= for outputs, as in:
+
+#+BEGIN_SRC sol
+  [Plus +left: X +right: Y -result R]
+#+END_SRC
+
+the preferred surface form is:
+
+#+BEGIN_SRC sol
+  [Plus left: X right: Y result: R]
+#+END_SRC
+
+The operational mode is inferred from:
+
+- bound variables
+- domain constraints
+- relation capabilities
+- solver availability
+- totality restrictions
+
+Though =+= and =-= are not necessary, we might want to still annotate
+them to help the planning.
+
+* Equality
+
+Equality may be represented as a relation.
+
+Example:
+
+#+BEGIN_SRC sol
+[Equal left: X right: Y]
+#+END_SRC
+
+Equality may perform unification, literal comparison, or symbolic
+constraint propagation.
+
+Examples:
+
+#+BEGIN_SRC sol
+Query expression:
+  [Equal left: X right: 10] :and
+  [Plus left: X right: 5 result: R]
+#+END_SRC
+
+This should bind or constrain =X= to =10=, then relate =R= to =15=.
+
+* Disjunction
+
+Disjunction may be expressed with =:or=.
+
+Example:
+
+#+BEGIN_SRC sol
+[Color value: "red"] :or
+[Color value: "blue"]
+#+END_SRC
+
+Disjunction introduces branching proof search.
+
+To preserve totality, disjunction must be finite or otherwise controlled.
+
+* Negation
+
+Negation must be restricted to the world that is being denied, as a
+negation has to come from something. World is a relation where every
+relation is part of it, and it cannot be enumerated.
+
+A possible syntax:
+
+#+BEGIN_SRC sol
+[World] :not [Adult person: P]
+#+END_SRC
+
+Semantically, Sol should support only stratified negation or decidable
+negation over finite/proven domains.
+
+Unrestricted negation-as-failure should not be admitted into the total
+core.
+
+* Membership Criteria
+
+A membership criterion is a relational expression used to determine
+whether a tuple belongs to a relation. In Sol, there is no fundamental
+distinction between a type check, an integrity constraint, and a
+relational membership check. All of them are expressed as relations.
+
+For example:
+
+#+BEGIN_SRC sol
+  [Integer value: X]
+#+END_SRC
+
+means that the tuple ={value: X}= must belong to the unary relation
+=Integer=, which is in itself a domain.
+
+Likewise:
+
+#+BEGIN_SRC sol
+  [Plus left: X right: Y result: R]
+#+END_SRC
+
+means that the labeled tuple ={left: X, right: Y, result: R}= must
+belong to the relation =Plus=.
+
+This is the general form:
+
+#+BEGIN_SRC sol
+  [Relation label: Term label: Term ...]
+#+END_SRC
+
+Semantically, this asks whether the labeled tuple belongs to
+=Relation=.
+
+For example:
+
+#+BEGIN_SRC sol
+[Person id: P name: "Marcos" age: A]
+#+END_SRC
+
+means:
+
+#+BEGIN_EXAMPLE
+{id = P, name = "Marcos", age = A} ∈ Person
+#+END_EXAMPLE
+
+A membership criterion should be defined for each relation or default
+to an attempt at unifying the members into it. On a domain Integer,
+for example, the host language may construct a builtin membership
+criteria that simply checks if the tuple {value: <literal_integer>}
+satisfies that, value is indeed an integer at the host language in
+which Sol is programmed in. Optionally we can define such as a rule
+for each, for example, rationals can bear a constraint that validates
+if the numerator and denominator are integers, but that the
+denominator is different from zero. Those are thus, quick ways to
+determine membership without having to resort to searching the space
+of the relation, specially since some relations are impossible to
+enumerate, but we still can tell its members apart. A last example,
+the World relation should yield true for every tuple assigned to it.
+
+A membership criterion may be used:
+
+- as a type-like assertion;
+- as a query goal;
+- as an integrity constraint;
+- as part of a rule body;
+- as a relation schema refinement;
+- as a symbolic constraint.
+
+Some examples of ordinary relations that are also constraints:
+
+#+BEGIN_SRC sol
+[Equal left: X right: Y]
+
+[LessThan left: A right: B]
+
+[GreaterEqual left: Score right: 0]
+
+[LessThanEqual left: Score right: 100]
+#+END_SRC
+
+There is no special built-in equality predicate required at the
+surface level. Equality may be treated as an ordinary relation with
+special operational capabilities, such as unification, literal
+comparison, and symbolic rewriting.
+
+** Membership as Integrity Control
+
+An integrity constraint is a membership criterion attached to a target
+relation.
+
+For example, a score must be between 0 and 100:
+
+#+BEGIN_SRC sol
+Constraint
+  name: "score_range"
+  relation: Result
+  body:
+    [GreaterEqual left: Score right: 0] :and
+    [LessThanEqual left: Score right: 100]
+#+END_SRC
+
+The variables in the constraint body are interpreted relative to the
+tuple being checked.
+
+If the target relation has a label =score:=, the constraint may bind
+that attribute explicitly:
+
+#+BEGIN_SRC sol
+Constraint
+  name: "score_range"
+  relation: Result
+  body:
+    [Current label: score value: Score] :and
+    [GreaterEqual left: Score right: 0] :and
+    [LessThanEqual left: Score right: 100]
+#+END_SRC
+
+Here =Current= denotes the tuple currently being checked.
+
+This preserves the same principle as Sakura's ICL: before accepting a
+tuple into a relation, the system verifies that the tuple satisfies
+all constraint-relations attached to the target relation.
+
+** Membership as Foreign Key
+
+A foreign key is just a membership check against another relation.
+
+Example:
+
+#+BEGIN_SRC sol
+Constraint
+  name: "fk_employee_dept"
+  relation: Employee
+  body:
+    [Current label: dept_id value: DeptId] :and
+    [Department dept_id: DeptId]
+#+END_SRC
+
+This means:
+
+#+BEGIN_EXAMPLE
+For the current Employee tuple, its dept_id must appear as the dept_id
+of some Department tuple.
+#+END_EXAMPLE
+
+No special foreign-key syntax is required. Foreign keys are relation
+membership criteria.
+
+** Membership as Refinement
+
+A schema entry may use a membership criterion as a refinement.
+
+Example:
+
+#+BEGIN_SRC sol
+Relation named: Result schema: #(
+  [student_id domain: Integer]
+  [score domain:
+    ([Integer value: Score] :and
+     [GreaterEqual left: Score right: 0] :and
+     [LessThanEqual left: Score right: 100])]
+)
+#+END_SRC
+
+This means that =score:= is not merely an integer. It is an integer
+that belongs to the refinement relation:
+
+#+BEGIN_EXAMPLE
+Score ∈ Integer ∧ Score ≥ 0 ∧ Score ≤ 100
+#+END_EXAMPLE
+
+The variable introduced in the refinement expression is local to that
+schema entry unless explicitly connected to another variable by the
+schema mechanism.
+
+** Membership and Totality
+
+Membership checking must be total.
+
+Given a fully grounded tuple, a membership criterion must either:
+
+- succeed;
+- fail;
+- or produce a finite, decidable set of residual constraints.
+
+It must not diverge, and for infinite domains, membership is allowed
+but unbounded enumeration is not.
+
+Thus:
+
+#+BEGIN_SRC sol
+[Integer value: X]
+#+END_SRC
+
+with =X= unbound constrains =X= to the domain =Integer=. It does not
+enumerate all integers.
+
+Enumeration must be expressed separately, and only through a bounded
+or otherwise total subset.
+
+Example:
+
+#+BEGIN_SRC sol
+[Take relation: Integer count: 10 value: X]
+#+END_SRC
+
+or:
+
+#+BEGIN_SRC sol
+[Between value: X lower: 0 upper: 10]
+#+END_SRC
+
+The exact enumeration syntax is provisional, but the principle is not:
+membership is not generation.
+* Existential Quantification
+
+Existential quantification states that there exists at least one value
+in a relation satisfying a body. In Sol, existential quantification is
+already implicit in ordinary queries and rule bodies.
+
+For example:
+
+#+BEGIN_SRC sol
+Query expression:
+  [Person id: P name: "Marcos"] :and
+  [Adult person: P]
+#+END_SRC
+
+means:
+
+#+BEGIN_EXAMPLE
+∃ P .
+  Person(id=P, name="Marcos") ∧ Adult(person=P)
+#+END_EXAMPLE
+
+A variable that appears in a query expression is existentially
+quantified unless it is explicitly bound by an outer context.
+
+** Explicit Exists
+
+Sol may also provide an explicit existential form.
+
+A possible syntax:
+
+#+BEGIN_SRC sol
+[Exists variable: P
+        domain: PersonId
+        body:
+          [Person id: P name: "Marcos"] :and
+          [Adult person: P]]
+#+END_SRC
+
+This means:
+
+#+BEGIN_EXAMPLE
+∃ P ∈ PersonId .
+  Person(id=P, name="Marcos") ∧ Adult(person=P)
+#+END_EXAMPLE
+
+The =domain:= label is a membership criterion that restricts the
+search space of the variable.
+
+For unary domains, this:
+
+#+BEGIN_SRC sol
+domain: PersonId
+#+END_SRC
+
+is shorthand for:
+
+#+BEGIN_SRC sol
+[PersonId value: P]
+#+END_SRC
+
+A more explicit form may be preferable where the quantified relation
+has named labels:
+
+#+BEGIN_SRC sol
+[Exists variable: P
+        quantifier: [PersonId value: P]
+        body:
+          [Person id: P name: "Marcos"] :and
+          [Adult person: P]]
+#+END_SRC
+
+This form generalizes better, because =quantifier:= may be any
+membership criterion.
+
+** Existential Through a Join
+
+A foreign key through a join can be expressed existentially.
+
+Example: a suite is valid if its room belongs to a building with more
+than three floors.
+
+#+BEGIN_SRC sol
+Constraint
+  name: "suite_in_tall_building"
+  relation: Suite
+  body:
+    [Current label: room_id value: RoomId] :and
+    [Exists variable: R
+            quantifier: [Room room_id: RoomId building_id: BuildingId]
+            body:
+              [Exists variable: B
+                      quantifier: [Building building_id: BuildingId floors: Floors]
+                      body:
+                        [GreaterThan left: Floors right: 3]]]
+#+END_SRC
+
+The semantics are:
+
+#+BEGIN_EXAMPLE
+For the current Suite tuple, there exists a Room with the same room_id,
+and there exists a Building with the Room's building_id, such that the
+Building has more than 3 floors.
+#+END_EXAMPLE
+
+This is equivalent to a relational join:
+
+#+BEGIN_EXAMPLE
+Suite.room_id = Room.room_id
+Room.building_id = Building.building_id
+Building.floors > 3
+#+END_EXAMPLE
+
+But no special join operator is needed. The join is expressed by
+shared variables.
+
+** Existential Variables in Rule Bodies
+
+Variables that appear in a rule body but not in the rule head are
+existential relative to the rule.
+
+Example:
+
+#+BEGIN_SRC sol
+Rule
+  name: "Adult is a person with age greater than or equal to 18"
+  head: [Adult person: P]
+  body:
+     [Person id: P age: A] :and
+     [GreaterEqual left: A right: 18]
+#+END_SRC
+
+Here =A= is existentially quantified in the body.
+
+The rule means:
+
+#+BEGIN_EXAMPLE
+Adult(P) ⇐ ∃ A .
+  Person(id=P, age=A) ∧ A ≥ 18
+#+END_EXAMPLE
+
+** Totality Requirements for Exists
+
+Existential quantification is only admitted into the total fragment
+when its search space is finite, bounded, structurally decreasing, or
+solvable symbolically.
+
+This is valid if =PersonId= is finite or indexed:
+
+#+BEGIN_SRC sol
+[Exists variable: P
+        quantifier: [Person id: P name: "Marcos"]
+        body: [Adult person: P]]
+#+END_SRC
+
+This is dangerous if it requires unbounded enumeration:
+
+#+BEGIN_SRC sol
+[Exists variable: X
+        quantifier: [Integer value: X]
+        body: [GreaterThan left: X right: 100]]
+#+END_SRC
+
+The latter must not enumerate integers until it finds one. It must be
+handled symbolically, bounded explicitly, or rejected from the total
+fragment.
+
+For example, this is admissible:
+
+#+BEGIN_SRC sol
+[Exists variable: X
+        quantifier: [Between value: X lower: 0 upper: 1000]
+        body: [GreaterThan left: X right: 100]]
+#+END_SRC
+
+because the quantifier relation is bounded.
+
+* Universal Quantification
+
+Universal quantification states that every value in a relation
+satisfies a body.
+
+A possible syntax:
+
+#+BEGIN_SRC sol
+[ForAll variable: X
+        quantifier: [Integer value: X]
+        body: [GreaterEqual left: X right: 0]]
+#+END_SRC
+
+This means:
+
+#+BEGIN_EXAMPLE
+∀ X ∈ Integer .
+  X ≥ 0
+#+END_EXAMPLE
+
+This particular example is false, because not all integers are greater
+than or equal to zero.
+
+A true version would use =Natural=:
+
+#+BEGIN_SRC sol
+[ForAll variable: X
+        quantifier: [Natural value: X]
+        body: [GreaterEqual left: X right: 0]]
+#+END_SRC
+
+** Universal Quantification Over Finite Relations
+
+Universal quantification is straightforward over finite stored
+relations.
+
+Example: every result score must be between 0 and 100.
+
+#+BEGIN_SRC sol
+[ForAll variable: R
+        quantifier: [Result id: R score: Score]
+        body:
+           [GreaterEqual left: Score right: 0] :and
+           [LessThanEqual left: Score right: 100]]
+#+END_SRC
+
+This means:
+
+#+BEGIN_EXAMPLE
+For every tuple in Result, its score is between 0 and 100.
+#+END_EXAMPLE
+
+Operationally, this can be checked by scanning the finite relation
+=Result= or by registering the condition as an integrity constraint
+checked on every insert/update.
+
+** Universal Quantification as Integrity Control
+
+A relation-level integrity constraint can often be understood as a
+universal statement.
+
+For example:
+
+#+BEGIN_SRC sol
+Constraint
+  name: "all_scores_are_in_range"
+  relation: Result
+  body:
+     [Current label: score value: Score] :and
+     [GreaterEqual left: Score right: 0] :and
+     [LessThanEqual left: Score right: 100]
+#+END_SRC
+
+corresponds to:
+
+#+BEGIN_EXAMPLE
+∀ tuple ∈ Result .
+  tuple.score ≥ 0 ∧ tuple.score ≤ 100
+#+END_EXAMPLE
+
+The constraint form is operationally preferable because it turns a
+global universal condition into a local membership check on each tuple
+mutation.
+
+This is the integrity-control interpretation:
+
+#+BEGIN_EXAMPLE
+A tuple may be inserted into relation R only if it belongs to every
+constraint-relation attached to R.
+#+END_EXAMPLE
+
+** Universal Quantification and Negation
+
+Universal quantification may be reduced to negated existence when the
+negation is decidable and the world is controlled:
+
+#+BEGIN_EXAMPLE
+∀ x ∈ R . P(x)
+≡
+¬ ∃ x ∈ R . ¬ P(x)
+#+END_EXAMPLE
+
+In Sol syntax, a possible form is:
+
+#+BEGIN_SRC sol
+[ForAll variable: X
+        quantifier: [Result id: X score: Score]
+        body:
+           [GreaterEqual left: Score right: 0] :and
+           [LessThanEqual left: Score right: 100]]
+#+END_SRC
+
+which may be planned internally as:
+
+#+BEGIN_SRC sol
+[World relation: Result] :not
+  [Exists variable: X
+          quantifier: [Result id: X score: Score]
+          body:
+             [LessThan left: Score right: 0] :or
+             [GreaterThan left: Score right: 100]]
+#+END_SRC
+
+This transformation is only valid when the negated world is decidable:
+for example, a finite stored relation, an indexed finite subset, or a
+symbolically decidable domain.
+
+** Universal Quantification Over Infinite Domains
+
+Universal quantification over infinite domains must not be implemented
+by enumeration.
+
+For example:
+
+#+BEGIN_SRC sol
+[ForAll variable: X
+        quantifier: [Integer value: X]
+        body:
+          [Equal left: [Plus left: X right: 0] right: X]]
+#+END_SRC
+
+This should be proved symbolically, by the algebraic properties of
+=Plus= and =Equal=, not by checking every integer.
+
+If Sol cannot prove such a universal symbolically, it must reject the
+program, keep it as an unproven obligation, or require an explicit
+trusted theorem/certificate.
+
+** Totality Requirements for ForAll
+
+Universal quantification is admitted when one of the following holds:
+
+- the quantified relation is finite;
+- the quantified relation is a bounded subset;
+- the body is decidable for every member of the quantified relation;
+- the universal can be discharged symbolically;
+- the universal is converted to a finite integrity-control check;
+- a totality/proof certificate is supplied.
+
+Universal quantification over an infinite domain with an undecidable
+body is not admitted into the total core.
+
+Thus this should be rejected or left as an obligation:
+
+#+BEGIN_SRC sol
+[ForAll variable: X
+        quantifier: [Integer value: X]
+        body: [SomeArbitraryRelation value: X]]
+#+END_SRC
+
+unless =SomeArbitraryRelation= has a declared decidable membership
+procedure or proof certificate.
+* Recursion
+
+Recursive rules are allowed only when the system can prove
+totality. Recursive calls must be structurally decreasing, guarded,
+finite, or otherwise accepted by a termination checker. The syntax
+must still use explicit conjunction.
+
+The body in the first rule is a relation that is simply true, called
+True.
+
+A corrected example:
+
+#+BEGIN_SRC sol
+  Rule
+    name: "An empty list is always true"
+    head: [Length list: #() result: 0]
+    body: [True]
+
+  Rule
+    name: "A list tail is summed"
+    head: [Length list: #(Head | Tail) result: R]
+    body: [Length list: Tail result: Partial] :and
+          [Plus left: 1 right: Partial result: R]
+#+END_SRC
+
+The recursive call is accepted only if the termination checker can
+see that =Tail= is structurally smaller than =#(Head | Tail)= — that
+is, than the tuple ={head: Head tail: Tail}= it elaborates to.
+
+An invalid rule:
+
+#+BEGIN_SRC sol
+  Rule
+    name: "Loop forever"
+    head: [Loop value: X]
+    body: [Loop value: X]
+#+END_SRC
+
+This must be rejected because no structural decrease exists. In Coq's
+Gallina this would have the type False, which breaks the logic system
+and falsifies it as a whole.
+
+* Higher-Order Relations
+
+Sol may support higher-order relations: relations that receive other
+relations as arguments.
+
+Example:
+
+#+BEGIN_SRC sol
+Query expression:
+  [Map relation: Increment source: XS target: YS]
+#+END_SRC
+
+However, unrestricted higher-order unification is not allowed in the
+total core. The following may be rejected or restricted:
+
+#+BEGIN_SRC sol
+Query expression:
+  [Map relation: P source: XS target: YS]
+#+END_SRC
+
+if =P= is an unconstrained relation variable and the system would need
+to synthesize arbitrary predicates.
+
+Higher-order relations must be governed by:
+
+- declared schemas;
+- capability restrictions;
+- totality certificates;
+- bounded search;
+- or parametricity constraints.
+
+* Primary Type System
+
+The primary type system of Sol is relational. Typing is enforced by
+proving relation membership.
+
+Example:
+
+#+BEGIN_SRC sol
+[Integer value: X]
+#+END_SRC
+
+is a type-like assertion:
+
+#+BEGIN_EXAMPLE
+X : Integer
+#+END_EXAMPLE
+
+But this is not a separate static annotation detached from the
+program. It is a relation in the same logical language.
+
+Similarly:
+
+#+BEGIN_SRC sol
+[Person id: P name: N age: A]
+#+END_SRC
+
+may constrain =P= to be a Person identifier (whatever domain it is),
+=N= to be Text, and =A= to be an Integer, according to the declared
+schema of =Person=.
+
+* Secondary Runtime Categories
+
+Sol may internally distinguish secondary runtime categories such as:
+
+- Query
+- Relation
+- DomainRelation
+- Rule
+- Variable
+- Literal
+- Constraint
+- Conjunction
+- Disjunction
+- SolverPlan
+
+These are implementation-level categories, rendering them not the
+primary semantic type system. The primary type system remains
+relational. This categorization serves to allow group operators, such
+as =:and= and =:or=.
+
+* Important Non-Goals
+
+Sol should not be:
+
+- a general-purpose imperative language,
+- an unrestricted Prolog,
+- a syntax skin over ordinary Turing-complete execution,
+- a language where every relation can accidentally enumerate its inhabitants,
+- a language where newline adjacency secretly means conjunction.
+
+* Summary
+
+Sol is a total relational language where:
+
+- relations are labeled propositions,
+- domains are unary relations,
+- typing is relation membership,
+- conjunction is explicit through =:and=,
+- joins happen by shared variables,
+- infinite domains constrain by default,
+- generation is explicit and controlled,
+- recursion is accepted only with a totality proof,
+- higher-order predicates are restricted,
+- and execution is proof search plus constraint solving.