#+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: [Plus left: X right: 0 result: X]]
#+END_SRC

This says that the tuple ={left: X, right: 0, result: X}= belongs to
=Plus= for every integer =X=: the identity law stated as membership.
Note what it is not written as: =[Equal left: [Plus left: X right: 0]
right: X]=, with an application nested in term position. That form is
rejected. A block is a proposition, never a value; treating it as a
value would require privileging one attribute as "the" result, and a
relation has no distinguished output. The flat membership form is
both the honest one and the shorter one.

This should be proved symbolically, by the algebraic properties of
=Plus=, 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.