Introduction

Welcome to the guide to the Stellogen language.

Please note that this guide is highly experimental and subject to frequent changes. The language it describes is equally unstable.

I welcome any opinions, recommendations, suggestions, or simple questions. Feel free to contact me at boris.eng@proton.me.

Happy reading!

Translated from the French guide by:

noncanonicAleae
ChatGPT 4o

How it all began

Stellogen was created from Boris Eng's research to understand Jean-Yves Girard's transcendent syntax program.

Transcendent syntax proposes a new foundation for logic and computation, extending the Curry-Howard correspondence. In this new framework, logical entities such as proofs, formulas, and concepts like truth are redefined/built from an elementary computational model called "stellar resolution," which is a highly flexible form of logical programming language.

To experiment with these ideas, Eng developed an interpreter called the "Large Star Collider (LSC)" to execute stellar resolution expressions. It was initially developed in Haskell and later reimplemented in OCaml.

Later, it became apparent that a metaprogramming language was necessary to properly work with these objects, especially for writing proofs in linear logic (which was the original project). This led to the creation of the Stellogen language.

Over time, Stellogen gradually diverged from transcendent syntax to develop its own concepts.

Philosophy

Mechanics of meaning

Types, specifications, algorithms, and logical formulas are questions that we pose. They carry a subjective intention. Programs are answers to these questions. They follow an objective dynamic: they can be implicit and evolve into an irreducible explicit form (this is execution leading to a computational result).

The big question is: how can we determine whether we are facing an answer to a question? We need a connective framework for the interaction between questions and answers.

Iconoclasm and decentralization

Traditionally, logic and type systems define systems with:

classes of entities (first-order individuals and relations);
semantic rules (the compiler/interpreter is responsible for the meaning of expressions, and the user manipulates these expressions according to this meaning);
forbidden interactions;
allowed interactions.

This establishes a preconceived logical framework. In particular, compilers and interpreters hold semantic authority: they define which questions can be asked and how to judge whether an answer is valid.

Stellogen seeks to return semantic power to the user, making them responsible for creating meaning through elementary building blocks that compose both programs and types/formulas/specifications. Interpreters and compilers then take on the role of maintaining a basic core that ensures proper connectivity between these blocks, as well as managing metaprogramming. This shifts their role from semantic authority to protocol and administrative evaluation.

Meaning through experience

To determine whether a program has a certain type (if an answer satisfies a question), we proceed as follows:

we construct a type by defining a set of tests that must be passed—these tests are themselves programs;
we build a "judge" that determines what it means to "pass a test";
we connect a program to each test of the type and check whether the judge validates all interactions.

This provides non-systemic, local guarantees, similar to "assert" statements in programming. We could choose to organize types and constraints within structured systems if needed.

Order in chaos

The computational model we work with, based on elementary building blocks, could be described as chaotic. It is possible to write unintuitive constructs with unpredictable outcomes. In some cases, confluence does not even hold different execution orders lead to different results).

There are two ways to bring order to chaos:

natural, local emergence by creating local guarantees on program fragments;
imposing a closed system that defines restrictions/constraints in which only certain types can be used.

Stellogen aims to leave both possibilities open. The first choice allows for great flexibility, while the second provides efficiency and usability advantages, along with stronger guarantees.

Partial verification

From a programming perspective, particularly in formal methods, Stellogen is driven by a notion of "partial" verification, in contrast to total verification, where a program and its properties are fully modeled to obtain formal proofs.

Stellogen focuses on expressive local constraints that could later be integrated into a broader system.

Getting started

To install the Stellogen interpreter, go to this Git repository:

https://github.com/engboris/stellogen

You can either compile from sources or download a pre-compiled executable:

For Linux x86-x64: https://github.com/engboris/stellogen/releases

You can then simply write your programs in any text file and follow the instructions in the README.md file of the git repository to execute your programs.

For a quick preview, don't hesitate to look up:

If you are ready, let's go!

Term Unification

Syntax

In unification theory, we write terms. These are either:

variables (starting with an uppercase letter, such as X, Y, or Var);
functions in the form f(t1, ..., tn) where f is a function symbol (starting with a lowercase letter or a digit) and the expressions t1, ..., tn are other terms.

All identifiers (whether for variables or function symbols) can include the symbols _ and ? (but not at the beginning). For example : is_empty? and X_1.

Examples of terms. X, f(X), h(a, X), parent(X), add(X, Y, Z).

It is also possible to omit the comma separating a function's arguments when its absence causes no ambiguity. For instance, h(a X) can be written instead of h(a, X).

Principle

In unification theory, two terms are said to be unifiable when there exists a substitution of variables that makes them identical. For example, f(X) and f(h(Y)) are unifiable with the substitution {X:=h(Y)} replacing X with h(Y).

The substitutions of interest are the most general ones. We could consider the substitution {X:=h(c(a)); Y:=c(a)}, which is equally valid but unnecessarily specific.

Another way to look at this is to think of it as connecting terms to check if they are compatible or "fit" together:

A variable X connects to anything that does not contain X as a subterm; otherwise, there would be a circular dependency, such as between X and f(X);
A function f(t1, ..., tn) is compatible with f(u1, ..., un) where ti is compatible with ui for every i.
f(X) and f(h(a)) are compatible with {X:=h(a)};
f(X) and X are incompatible;
f(X) and g(X) are incompatible;
f(h(X)) and f(h(a)) are compatible with {X:=a}.

Stars and Constellations

Rays

The language of stellar resolution extends the notion of terms with the concept of rays. A ray is a term where function symbols are polarized with:

+ (positive polarity);
- (negative polarity);
nothing (neutral polarity or absence of polarity).

The compatibility of rays follows the same rules as term unification, except:

instead of requiring equality f = g of function symbols when f(t1, ..., tn) is confronted with g(u1, ..., un), we require f and g to have opposite polarities (+ versus -); symbols without polarity cannot interact.

For example:

+f(X) and -f(h(a)) are compatible with {X:=h(a)};
f(X) and f(h(a)) are incompatible;
+f(X) and +f(h(a)) are incompatible;
+f(+h(X)) and -f(-h(a)) are compatible with {X:=a};
+f(+h(X)) and -f(-h(+a)) are compatible with {X:=+a}.

String literals

Stellogen also allows to define special constants representing string literals:

"this is a string literal"

Sequences

It is possible to use a special infix symbol : as in:

+w(0:1:0:1:e).

It is possible to put parentheses around it to make the priorit explicit (right-associative by default):

+w((0:(1:(0:(1:e))))).
+w((((0:1):0):1):e).

Stars

With rays, we can form stars. These are unordered collections of rays which can be surrounded by brackets:

+f(X) -f(h(a)) +f(+h(X))

[+f(X) -f(h(a)) +f(+h(X))]

The empty star is denoted as [].

Constellations

Constellations are unordered sequences of stars separated by the ; symbol and ending with a .:

+f(X) X; +f(+h(X) a f(b)).

They can be surrounded by braces:

{ +f(X) X; +f(+h(X) a f(b)) }.

Variables are local to their stars. This can be made explicit by writing:

+f(X1) X1; +f(+h(X2) a f(b)).

The empty constellation is denoted as {}.

Constellations are, in fact, the smallest objects we can manipulate. They are the ones that can be executed in the same way programs are executed.

Execution of Constellations

Fusion of Stars

Stars interact with each other using an operation called fusion (which can be likened to an interaction protocol) based on the principle of Robinson's resolution rule.

The fusion of two stars:

r r1 ... rk

and

r' r1' ... rk'

along their rays r and r' is defined by a new star:

theta(r1) ... theta(rk) theta(r1') ... theta(rk')

where theta is the most general substitution induced by r and r'.

Note that:

r and r' are annihilated during the fusion;
the two stars merge;
the substitution obtained from resolving the conflict between r and r' propagates to the adjacent rays.

Example: The fusion of X +f(X) and -f(a) makes +f(X) and -f(a) interact, propagating the substitution {X:=a} to the remaining ray X. The result is X{X:=a}, i.e., a.

This fusion operation corresponds to the cut rule in first-order logic (also linked to the resolution rule). However, the context here is "alogical" (our objects carry no logical meaning).

Execution

Execution is somewhat akin to solving a puzzle or playing darts. You start with a constellation made up of several stars. Choose some initial stars, then create copies of other stars to interact with them through fusion. The process continues until no further interactions are possible (saturation). The final constellation is the result of the execution.

Formally, the constellation is split into two parts for execution:

the state space, corresponding to stars which will be targets for interaction;
the action space, corresponding to stars which will interact with stars of the state space.

This separation can be represented as follows, with the action space on the left and state space on the right, separated by the symbol |-:

a1 ... an |- s1 ... sm

Execution proceeds as follows:

Select a ray r from a state star s;
Find all possible connections with rays r' from action stars s;
Duplicate s on the right for each such ray r' found;
Replace each copy of s with the fusion of a and s;
Repeat until no further interactions are possible in the state space. stars.

Focus

State stars are prefixed by @:

@+a b; [-c d].

+a b; [@-c d].

Example

Consider the execution of the following constellation:

@+a(0(1(e)) q0);
-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2).

For the example, we surround the selected way between >> and <<. We have the following step:

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2);
@+a(0(1(e)) q0).

And the following separation:

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
+a(0(1(e)) q0)

Select the first ray of the first star:

>>-a(e q2)<< accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
+a(0(1(e)) q0)

It cannot be connected to +a(0(1(e)) q0) because its first argument e is incompatible with 0(1(e)). However, it can interact with the two next stars (but not the last one because of an incompatibility between q0 and q1) We do a duplication and a fusion between:

-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);

and

+a(0(1(e)) q0)

and obtain the substitution {W:=1(e)} then the result:

+a(1(e) q0);
+a(1(e) q1)

We obtain the following step:

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
+a(1(e) q0);
+a(1(e) q1)

The second state star +a(1(e) q1) cannot interact with an action star. However, we can focus on +a(1(e) q0).

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
>>+a(1(e) q0)<<;
+a(1(e) q1)

It can connect to -a(1(W) q0) with substitution {W:=e}:

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
+a(e q0);
+a(1(e) q1)

No further interaction is possible. The result of execution is then:

+a(e q0);
+a(1(e) q1)

Defining constellations

Static definitions

We can name constellations that are directly written. Identifiers follow the same rules as for ray function symbols.

w = { a }.
x = +a; -a b.
z = -f(X).

When we refer to a constellation identifier, we use the prefix #:

y = #x.

As for application in functional programming, union of constellations is written with a space:

union1 = #x #y #z.

We can also add parentheses around expressions for more readability or to avoid syntactic ambiguity:

union1 = (#x #y) #z.

However, note that unlike in functional programming there is no defined ordering.

Static definitions correspond to the notion of "proof-object" in Curry-Howard correspondence.

Focus

We can focus all stars of a constellation by prefixing it with @ and put it around parentheses:

x = +a; -a b.
z = -f(X).
union1 = @#x #z.

Inequality constraints

It is possible to add a sequence of inequality contraints between terms:

ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.

This makes invalid any interaction where X and Y are fully defined (no variable) and instanciated to the same value.

Those inequalities can be separated by spaces or commas:

X!=Y X!=Z

X!=Y, X!=Z

Pre-execution

The execution of a constellation within a block exec ... end also defines a constellation:

exec +f(X); -f(a) end

Commands

Comments

Comments begin with ' and are written between ''' for multi-line comments. They are ignored during execution.

'this is a comment

'''
this is a
multiline comment
'''

Display

To display constellations, you can use the command show followed by a constellation:

show +a; -a b.

The show command does not execute constellation. If you want to actually execute the constellation and display its result, use the show-exec command:

show-exec +a; -a b.

Execution trace

It is possible to follow step by step the execution of a constellation:

ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.
'trace ineq.

Reactive effects

Stellogen uses "reactive effects" which are activated during the interaction between two rays using special head symbols.

Print

For printing, an interaction between two rays %print is needed. The interaction generates a substitution defining the ray to be displayed:

+%print(X); -%print("hello world\n").

This command displays hello world then an end of line symbol.

Running a constellation

When constellations produce an effect, a run command is available to execute them:

run +%print(X); -%print("hello world\n").

Substitutions

Substitutions are expressions of the form [... => ...] replacing an entity by another.

Variables

Variables can be replaced by any other ray:

show-exec (+f(X))[X=>Y].
show-exec (+f(X))[X=>+a(X)].

Function symbols

Function symbols can be replaced by other function symbols:

show-exec (+f(X))[+f=>+g].
show-exec (+f(X))[+f=>f].

We can also omit the left or right part of => to add or remove a head symbol:

show-exec (+f(X); f(X))[=>+a].
show-exec (+f(X); f(X))[=>a].
show-exec (+f(X); f(X))[+f=>].

Constellation identifiers

show-exec (#1 #2)[#1=>+f(X) X][#2=>-f(a)].

Logic programming

Constellations are sort of logic programs as in Prolog. They are all-purpose materials.

In logic programming, rays are seen as predicates, properties or relations.

'a is the child of b
childOf(a b).

Positive rays are outputs/conclusions and negative rays are inputs/hypotheses. With rays, it is possible to create facts (truth of a knowledge base):

'knowledge base
+childOf(a b).
+childOf(a c).
+childOf(c d).

but also inference rules:

-childOf(X Y) -childOf(Y Z) +grandParentOf(Z X).

Facts and inference rules form action stars which will interact with query stars which allows to aks questions like how one queries a database:

-childOf(X b) res(X).

It returns a result telling who are the children of b.

Unlike dedicated languages like Prolog, in Stellogen you have to organize en trigger interactions:

knowledge =
  +childOf(a b);
  +childOf(a c);
  +childOf(c d);
  -childOf(X Y) -childOf(Y Z) +grandParentOf(Z X).

query = -childOf(X b) res(X).

show-exec #knowledge @#query.

Galaxies

Constellations can be represented by labelling sub-constellations. This is what we call galaxies.

Galaxies are defined with blocks galaxy ... end containing a series of labels label = followed by the associated galaxy:

g = galaxy
  test1 = +f(a) ok.
  test2 = +f(b) ok.
end

Fields of a galaxy are then accessed with ->:

show #g->test1.
show #g->test2.

This resembles the concept of a record in programming, except that when galaxies are used, they are represented by their underlying constellation (by forgetting the labels).

Interfaces

It is possible to check whether a galaxy is constructed in a certain way with fields of some specific name and type:

interface nat_pair
  n :: nat.
  m :: nat.
end

g_pair :: nat_pair.
g_pair = galaxy
  n = +nat(0).
  m = +nat(0).
end

Typing

Typing in Stellogen illustrates key principles of transcendental syntax, where types are defined as sets of tests, themselves constructed using constellations. Type checking involves passing all the tests associated with a type.

Types are represented by a galaxy, where each field corresponds to a test that must be passed:

t = galaxy
  test1 = @-f(X) ok; -g(X).
  test2 = @-g(X) ok; -f(X).
end

It is also possible to prefix the definition with a spec keyword to make explicit that it is a specification:

spec t = galaxy
  test1 = @-f(X) ok; -g(X).
  test2 = @-g(X) ok; -f(X).
end

A galaxy/constellation under test must therefore satisfy all the tests defined by the galaxy above to be of type t.

A type with a single test can be defined as a simple constellation.

However, we still need to define what it means to:

be confronted with a test;
successfully pass a test.

In line with the Curry-Howard correspondence, types can be viewed as formulas or specifications. This can also be extended to Thomas Seiller's proposal of viewing algorithms as more sophisticated specifications.

Checkers

We need to define checkers, which are "judge" galaxies that specify:

an interaction field, necessarily containing the identifiers #tested and #test. It explains how the tested and the test interact;
an expect field indicating the expected result of the interaction.

For example:

checker = galaxy
  interaction = #tested #test.
  expect = ok.
end

Test-based typing

We can then precede definitions with a type declaration:

c :: t [checker].
c = +f(0) +g(0).

The constellation c successfully passes the test1 and test2 tests of t. Thus, there is no issue. We say that c is of type t or that c is a proof of the formula t.

However, if we had a constellation that failed the tests, such as:

c :: t [checker].
c = +f(0).

We would receive an error message indicating that a test was not passed.

Here is an example of a type with a single test for a naive representation of natural numbers:

spec nat =
  -nat(0) ok;
  -nat(s(N)) +nat(N).

0 :: nat [checker].
0 = +nat(0).

1 :: nat [checker].
1 = +nat(s(0)).

We can also omit specifying the checker. In this case, the default checker is:

checker = galaxy
  interaction = #tested #test.
  expect = ok.
end

This allows us to write:

0 :: nat.
0 = +nat(0).

1 :: nat.
1 = +nat(s(0)).

Plurality of types

It is possible to associate seveeral types to a same constellation:

either by defining several type declarations;
or by writing sequences of types (separated by commas) when a same checker is used.

For example:

nat2 = -nat(X) ok.
2 :: nat [checker].
2 :: nat2.
2 = +nat(s(s(0))).

3 :: nat, nat2.
3 = +nat(s(s(s(0)))).
```

## Interface

It is possible to define interfaces describing a series of identifiers with
a corresponding type to satisfy.

```
nat_pair = interface
  n :: nat [checker].
  m :: nat [checker].
end
```

It is then possible to ask for a galaxy to satisfy that interface.

```
g_pair :: nat_pair.
g_pair = galaxy
  n = +nat(0).
  m = +nat(0).
end
```

Expectations

It is possible to verify whether a constellation is equal to another one with an expectation test:

x :=: +f(X).

In particular, passing the test of some specification such as:

spec t = galaxy
  test1 = +f(X).
  test2 = +g(X).
end

g :: t.

can be reformulated in an equivalent way like this:

t1 :=: ok.
t1 = #g #t->test1.
t2 :=: ok.
t2 = #g #t->test2.

Construction process

We can chain constellations with the expression process ... end:

c = process
  +n0(0).
  -n0(X) +n1(s(X)).
  -n1(X) +n2(s(X)).
end

This chain starts with the first constellation +n0(0) as a state space. The next constellation then interacts as an action space with the previous one seen as a state space). Thus we have an interaction chain with a complete focus on the previous result.

It's as if we did the following computation:

c = +n0(0).
c = @#c {-n0(X) +n1(s(X))}.
c = @#c {-n1(X) +n2(s(X))}.

This is what corresponds to tactics in proof assistants such as Coq and could be assimilated to imperative programs which alter state representations (memory, for example).

Dynamical constructions correspond to the notion of "proof-process" in Boris Eng or "proof-trace" in Pablo Donato. Proof-processes construct proof-objects (constellations).

Process termination

In the result of an execution, if we represent results as rays with zero polarity, then stars containing polarized rays can be interpreted as incomplete computations that could be discarded.

To achieve this in construction processes, we can use the special #kill expression:

c = process
  +n0(0).
  -n0(X) +n1(s(X)).
  -n1(X) +n2(s(X)).
  -n2(X) result(X); -n2(X) +n3(X).
  #kill.
end

show-exec c.

We used a ray +n3(X) to continue computations if desired. The result is stored in result(X). However, if we want to keep only the result and eliminate any further computation possibilities, we can use #kill.

Process Cleanup

Sometimes we encounter empty stars [] in processes. These can be removed using the #clean command:

show-exec process
  +f(0).
  -f(X).
  #clean.
end

tsguide