Introduction

Sol is a total (from 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)
references (relation-denoting values, #Name)
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:

Integer
Person
Adult
Plus
Length
Query
Relation

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:

value:
left:
right:
result:
name:
age:
person:
list:

Labels are not positional argument markers. They name the attributes of a relation.

For example:

[Plus left: X right: Y result: R]

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:

X
Y
R
PersonId
Age
Tail
Partial

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:

0
1
22
"Sun"
1/4
#()

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:

{name: "Marcos" age: 30}

{numerator: 1 denominator: 4}

{head: H tail: T}

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:

[R l1: t1 ... ln: tn]   ≡   {l1: t1, ..., ln: tn} ∈ R

Label order in records is irrelevant, as in applications.

Sequences

A sequence is list-literal sugar, written #( ... ) (after Smalltalk's array literal):

#()

#(1 2 3)

#(Head | Tail)

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

#(1 2 3)        ≡  {head: 1 tail: {head: 2 tail: {head: 3 tail: #()}}}
#(Head | Tail)  ≡  {head: Head tail: Tail}

#(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.

References

A reference is a first-class value denoting a relation by name, written with the Smalltalk symbol notation:

#Person
#Increment

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 propositions (relation applications). They are never list literals, never grouping, never sequences.

Examples:

[Integer value: X]

[Plus left: X right: Y result: R]

Grouping of a relational expression, where precedence demands it, uses parentheses:

([Integer value: X] :and [LessThanEqual left: X right: 120])

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:

[Relation label: Term label: Term ...]

Examples:

[Integer value: X]

[Person id: P name: "Damian" age: A]

[Plus left: X right: Y result: R]

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:

[Plus left: X right: Y result: R]

[Plus result: R right: Y left: X]

Conjunction

Conjunction is expressed explicitly with the message :and.

Example:

[Integer value: X] :and [Integer value: Y] :and [Plus left: X right: Y result: R]

This means:

Integer(X) ∧ Integer(Y) ∧ Plus(X,Y,R)

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:

[Integer value: X]
[Integer value: Y]

Instead, conjunction must be explicit:

[Integer value: X] :and
[Integer value: Y]

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:

Query expression:
  [Integer value: X] :and
  [Integer value: Y] :and
  [Plus left: X right: Y result: 10]

This means:

∃ X Y .
  Integer(X) ∧ Integer(Y) ∧ Plus(X,Y,10)

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:

Query expression:
  [Person id: P name: "Marcos"] :and
  [Adult person: P]

The shared variable P is the join point.

Semantically:

∃ P .
  Person(id=P, name="Marcos")
∧ Adult(person=P)

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:

[Integer value: X]

means:

X ∈ Integer

or:

Integer(X)

Infinite Domains

A crucial distinction in Sol is between membership and generation.

The expression:

[Integer value: X]

does not mean:

Generate every integer X.

It means:

Constrain X to be an integer.

This is essential for totality, as the same applies to other countably infinite domains:

[Rational value: Q]

[String value: S]

[List element: Integer value: XS]

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:

[Generate domain: Integer value: X]

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:

Relation named: Person schema: #(
  [name domain: String]
  [age domain: ([Natural value: X] :and [LessThanEqual left: X right: 120])]
)

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:

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]

This means:

Adult(P) ⇐ Person(P,A) ∧ GreaterEqual(A,18)

The body is explicitly a conjunction.

It is not written as:

Person id: P age: A
GreaterEqual left: A right: 18

because that would reintroduce implicit sequencing.

Operational Capabilities

Relations may declare operational capabilities.

For example:

Relation named: Plus capabilities: #(
  [Capability name: evaluate]
  [Capability name: solve]
  [Capability name: constrain]
)

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:

[Plus +left: X +right: Y -result R]

the preferred surface form is:

[Plus left: X right: Y result: R]

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:

[Equal left: X right: Y]

Equality may perform unification, literal comparison, or symbolic constraint propagation.

Examples:

Query expression:
  [Equal left: X right: 10] :and
  [Plus left: X right: 5 result: R]

This should bind or constrain X to 10, then relate R to 15.

Disjunction

Disjunction may be expressed with :or.

Example:

[Color value: "red"] :or
[Color value: "blue"]

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:

[World] :not [Adult person: P]

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:

[Integer value: X]

means that the tuple {value: X} must belong to the unary relation Integer, which is in itself a domain.

Likewise:

[Plus left: X right: Y result: R]

means that the labeled tuple {left: X, right: Y, result: R} must belong to the relation Plus.

This is the general form:

[Relation label: Term label: Term ...]

Semantically, this asks whether the labeled tuple belongs to Relation.

For example:

[Person id: P name: "Marcos" age: A]

means:

{id = P, name = "Marcos", age = A} ∈ Person

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:

[Equal left: X right: Y]

[LessThan left: A right: B]

[GreaterEqual left: Score right: 0]

[LessThanEqual left: Score right: 100]

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:

Constraint
  name: "score_range"
  relation: Result
  body:
    [GreaterEqual left: Score right: 0] :and
    [LessThanEqual left: Score right: 100]

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:

Constraint
  name: "score_range"
  relation: Result
  body:
    [Current label: score value: Score] :and
    [GreaterEqual left: Score right: 0] :and
    [LessThanEqual left: Score right: 100]

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:

Constraint
  name: "fk_employee_dept"
  relation: Employee
  body:
    [Current label: dept_id value: DeptId] :and
    [Department dept_id: DeptId]

This means:

For the current Employee tuple, its dept_id must appear as the dept_id
of some Department tuple.

No special foreign-key syntax is required. Foreign keys are relation membership criteria.

A schema entry may use a membership criterion as a refinement.

Example:

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])]
)

This means that score: is not merely an integer. It is an integer that belongs to the refinement relation:

Score ∈ Integer ∧ Score ≥ 0 ∧ Score ≤ 100

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:

[Integer value: X]

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:

[Take relation: Integer count: 10 value: X]

or:

[Between value: X lower: 0 upper: 10]

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:

Query expression:
  [Person id: P name: "Marcos"] :and
  [Adult person: P]

means:

∃ P .
  Person(id=P, name="Marcos") ∧ Adult(person=P)

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:

[Exists variable: P
        domain: PersonId
        body:
          [Person id: P name: "Marcos"] :and
          [Adult person: P]]

This means:

∃ P ∈ PersonId .
  Person(id=P, name="Marcos") ∧ Adult(person=P)

The domain: label is a membership criterion that restricts the search space of the variable.

For unary domains, this:

domain: PersonId

is shorthand for:

[PersonId value: P]

A more explicit form may be preferable where the quantified relation has named labels:

[Exists variable: P
        quantifier: [PersonId value: P]
        body:
          [Person id: P name: "Marcos"] :and
          [Adult person: P]]

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.

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]]]

The semantics are:

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.

This is equivalent to a relational join:

Suite.room_id = Room.room_id
Room.building_id = Building.building_id
Building.floors > 3

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:

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]

Here A is existentially quantified in the body.

The rule means:

Adult(P) ⇐ ∃ A .
  Person(id=P, age=A) ∧ A ≥ 18

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:

[Exists variable: P
        quantifier: [Person id: P name: "Marcos"]
        body: [Adult person: P]]

This is dangerous if it requires unbounded enumeration:

[Exists variable: X
        quantifier: [Integer value: X]
        body: [GreaterThan left: X right: 100]]

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:

[Exists variable: X
        quantifier: [Between value: X lower: 0 upper: 1000]
        body: [GreaterThan left: X right: 100]]

because the quantifier relation is bounded.

Universal Quantification

Universal quantification states that every value in a relation satisfies a body.

A possible syntax:

[ForAll variable: X
        quantifier: [Integer value: X]
        body: [GreaterEqual left: X right: 0]]

This means:

∀ X ∈ Integer .
  X ≥ 0

This particular example is false, because not all integers are greater than or equal to zero.

A true version would use Natural:

[ForAll variable: X
        quantifier: [Natural value: X]
        body: [GreaterEqual left: X right: 0]]

Universal Quantification Over Finite Relations

Universal quantification is straightforward over finite stored relations.

Example: every result score must be between 0 and 100.

[ForAll variable: R
        quantifier: [Result id: R score: Score]
        body:
           [GreaterEqual left: Score right: 0] :and
           [LessThanEqual left: Score right: 100]]

This means:

For every tuple in Result, its score is between 0 and 100.

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:

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]

corresponds to:

∀ tuple ∈ Result .
  tuple.score ≥ 0 ∧ tuple.score ≤ 100

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:

A tuple may be inserted into relation R only if it belongs to every
constraint-relation attached to R.

Universal Quantification and Negation

Universal quantification may be reduced to negated existence when the negation is decidable and the world is controlled:

∀ x ∈ R . P(x)
≡
¬ ∃ x ∈ R . ¬ P(x)

In Sol syntax, a possible form is:

[ForAll variable: X
        quantifier: [Result id: X score: Score]
        body:
           [GreaterEqual left: Score right: 0] :and
           [LessThanEqual left: Score right: 100]]

which may be planned internally as:

[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]]

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:

[ForAll variable: X
        quantifier: [Integer value: X]
        body: [Plus left: X right: 0 result: X]]

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:

[ForAll variable: X
        quantifier: [Integer value: X]
        body: [SomeArbitraryRelation value: X]]

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:

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]

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:

Rule
  name: "Loop forever"
  head: [Loop value: X]
  body: [Loop value: X]

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:

Query expression:
  [Map relation: Increment source: XS target: YS]

However, unrestricted higher-order unification is not allowed in the total core. The following may be rejected or restricted:

Query expression:
  [Map relation: P source: XS target: YS]

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:

[Integer value: X]

is a type-like assertion:

X : Integer

But this is not a separate static annotation detached from the program. It is a relation in the same logical language.

Similarly:

[Person id: P name: N age: A]

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.

Introduction

Core Design Intention

Lexical Categories

Atoms

Labels

Variables

Literals

Records

Sequences

References

Blocks

Relation Application Syntax

Conjunction

Query Syntax

Joins Through Unification

Domains as Unary Relations

Infinite Domains

Relation Schemas

Rules

Operational Capabilities

Modes

Equality

Disjunction

Negation

Membership Criteria

Membership as Integrity Control

Membership as Foreign Key

Membership as Refinement

Membership and Totality

Existential Quantification

Explicit Exists

Existential Through a Join

Existential Variables in Rule Bodies

Totality Requirements for Exists

Universal Quantification

Universal Quantification Over Finite Relations

Universal Quantification as Integrity Control

Universal Quantification and Negation

Universal Quantification Over Infinite Domains

Totality Requirements for ForAll

Recursion

Higher-Order Relations

Primary Type System

Secondary Runtime Categories

Important Non-Goals

Summary