diff options
| -rw-r--r-- | docs/language-specification.org | 1336 |
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. |