Introduction

Welcome to the guide to transcendental syntax.

This guide presents the ideas of Jean-Yves Girard from the perspective of a computer scientist.

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!

(Initial translation provided by noncanonicAleae)

Transcendental Syntax

Logic usually lives in more or less intercompatible logical systems. We can speak of logical pluralism.

Logics usually function with a computational basis named syntax that follows rules dictated by a higher level syntax named semantic. In particular, are imposed: usable objects, their form, their possible interactions, and the formulas or specifications that can be expressed.

This action at a distance between two hermetic spaces, while being the fruit of our perception of a certain structuration of reality, is an obstacle to the manipulation and understanding of logical mechanisms. Logical reality as such is not directly accessible (why would it be?).

Our understanding of logic can only rest on apparently arbitrary, while effective, considerations. One needs to be able to justify their relevance and to recontextualize, if not naturalize them (and thus maybe obtain a science of logic?). Transcendental syntax, conceived by Jean-Yves Girard, proposes:

a reorganization of the concepts of computation and logic to highlight their distinctions and interactions;
a reverse engineering of logic from syntactic computation allowing us to reframe our knowledge in a new logical environment;
a computational justification of logical principles.

Example in automata theory

A finite automaton is a machine that can read a word (letter by letter and without memory) then accept it or not. An automaton can be characterized by its set of accepted words, making up its recognized language.

If faced with some given automaton, how to determine its recognized language? There are multiple possibilities:

analyze the automaton by evaluating and judging it (semantic option we want to avoid);
look at how it reacts against every word (rational but unrealistic option). What Girard calls the usage sense;
immerse the representation of automata and words in another larger interaction space in which we could test (in a more effective way) the automaton's reaction against a finite number of "exotic" objects allowing us to determine its recognized language. What Girard calls the usine sense.

Stellar resolution

Stellar resolution is the (theoretical) language of transcendental syntax. It is a language functioning through asynchronous interaction of independent agents. This interaction is based on a unification algorithm (that involved in the Prolog language) working as a minimal computation core.

It represents computation by a network of syntactical constraints that must be resolved to propagate information. The result of the computation corresponds to the information left by the networks that remained coherent until the end without encountering conflicts.

These ideas already exist in logical programming but are reformulated and used differently. In particular, we assign no logical sense to objects (even if they can be seen this way, they are not supposed to represent relations or objects of logical systems).

This calculus can be understood in several ways. It is:

a process calculus;
a constraint-based programming language;
a variant of disjunctive clauses with Robinson's resolution rule;
a non-planar generalization of Wang tiles or abstract tile assembly models (aTAM);
a generalization of Jonoska's flexible tiles used in DNA computing;
a generalization of LEGO bricks;
a low-level language expressing logical sense;
a toolbox for constructing types/formulas;
a generalization of Jean-Yves Girard's proof structures;
a form of Lafont's interaction nets using no other rules than term unification principles.

Stellogen language

The Stellogen language is a programming language used to define, manipulate, and put in interaction stellar resolution entities, and thus illustrate the principles of transcendental syntax.

It is one possible computer realization of stellar resolution and transcendental syntax, that makes design choices to adapt to programming practices.

It has an interpreter written in OCaml, as well as an execution engine for stellar resolution (which is an independent language) called "Large Star Collider" (LSC), also written in OCaml.

If stellar resolution is a language of elementary bricks (like LEGO), then:

transcendental syntax is the theory of bricks;
the Large Star Collider is the principle allowing brick connectivity;
Stellogen is a language allowing manipulation of these bricks to make advanced construction that would be too tedious to do by hand.

Stellogen is the language we are going to explore step by step in this small guide.

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 may end with a sequence of ' symbols. For example: x', X'', 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}.

Stars

With rays, we can form stars. These are unordered collections of rays:

+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)).

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.

Example

Consider the execution of the following constellation, where the only initial state star is prefixed by @:

+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z));
@-add(s(s(0)) s(s(0)) R) R.

For clarity, the selected rays will be highlighted with >> and <<. The steps are as follows:

+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z));
@-add(s(s(0)) s(s(0)) R) R.

The initial separation is:

+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z))
|-
-add(s(s(0)) s(s(0)) R) R

Select the first ray

+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z))
|-
>>-add(s(s(0))<< s(s(0)) R) R

+add(0 Y Y) cannot interact with -add(s(s(0)) s(s(0)) R) because the first argument 0 is incompatible with s(s(0)). However, it can interact with +add(s(X) Y s(Z)). Fusing:

-add(X Y Z) +add(s(X) Y s(Z))

with

-add(s(s(0)) s(s(0)) R) R

produces the substitution {X:=s(0), Y:=s(s(0)), R:=s(Z)} and the result:

-add(s(0) s(s(0)) Z) s(Z)

This leads to:

+add(0 Y Y);
-add(X Y Z) >>+add(s(X) Y s(Z))<<
|-
-add(s(0) s(s(0)) Z) s(Z)

Select the first ray again

+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z))
|-
>>-add(s(0) s(s(0)) Z)<< s(Z)

It can interact with +add(s(X) Y s(Z)), giving the substitution {X:=0, Y:=s(s(0)), Z:=s(Z')}:

+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z))
|-
-add(0 s(s(0)) Z') s(s(Z'))

Selecting the first ray once more

+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z))
|-
>>-add(0 s(s(0)) Z')<< s(s(Z'))

This ray interacts only with the first action star +add(0 Y Y), resulting in:

+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z))
|-
s(s(s(s(0))))

The result of the execution is:

s(s(s(s(0))))

Exercises

Determine the result of executing the constellations below. You can verify your results by writing the following code in a file:

print <constellation>

and then executing it.

For example:

print X +f(X); @-f(a).

@+f(X); -f(a).
@+f(X); -f(Y) a.
@+f(X) X; -f(a); -f(b).
@+1(X) -2(X); -2(X) +3(X).
@-1(X) +2(X); -2(X) +1(X).
@-1(X) +2(X); -2(X) +1(X).
@-f(X) X; +f(+g(a)); -g(X) X.

Defining constellations

Comments

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

Static definitions

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

Constellations are surrounded by braces { ... }.

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

Braces around constellations can be omitted when there is no ambiguity with identifiers:

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

We can also choose to associate an identifier to another:

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.

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 print command:

print +a; -a b.

Focus

We can focus all stars of a constellation by prefixing it with @:

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

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:

@+n0(0);
-n0(X) +n1(s(X)).

yielding

+n1(s(0)).

then

@+n1(s(0));
-n1(X) +n2(s(X)).

yielding

+n2(s(s(0))).

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

print 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:

print process
  +f(0).
  -f(X).
  clean.
end

Galaxies

The Stellogen language adds to stellar resolution an entity named galaxy.

A galaxy is either a constellation or a structure with named fields containing other galaxies.

More generally, Stellogen actually manipulates galaxies rather than constellations (that are special cases of galaxy).

In Stellogen, "everything is galaxy" in the same way that everything is object is programming languages like Smalltalk or Ruby.

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

Substitutions

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

Variables

Variables can be replaced by any other ray:

print (+f(X))[X=>Y].
print (+f(X))[X=>+a(X)].

Function symbols

Function symbols can be replaced by other function symbols:

print (+f(X))[+f=>f].

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

print (+f(X); f(X))[=>+a].
print (+f(X); f(X))[=>a].
print (+f(X); f(X))[+f=>].

Tokens and galactic replacement

Galaxy expressions can contain special variables such as #1, #2 or #variable.

These are holes named tokens that can be replaced by another galaxy:

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

This allows, notably, to write parametrized galaxies.

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

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 a #tested token and another #test token that 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:

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

Exercises

Paths

Give a value to the variables answer so that the following code can be executed without typing errors.

The idea is that these constellations represent paths to complete in order to obtain only the constellation ok as a result.

checker = galaxy
  interaction: #test #tested.
  expect: { ok }.
end
empty = {}.

answer = #replace_me.
exercise1 :: empty [checker].
exercise1 = ((-1 ok) {1})[1=>answer].

answer = #replace_me.
exercise2 :: empty [checker].
exercise2 = ((-1; +2) {1})[1=>answer].

answer = #replace_me.
exercise3 :: empty [checker].
exercise3 = ((-1 ok; -2 +3) {1})[1=>answer].

answer = #replace_me.
exercise4 :: empty [checker].
exercise4 = ((-f(+g(X)) ok) {1})[1=>answer].

answer = #replace_me.
exercise5 :: empty [checker].
exercise5 = ((+f(a) +f(b); +g(a); @+g(b) ok) {1})[1=>answer].

Solutions


checker = galaxy
interaction: #test #tested.
expect: { ok }.
end
empty = {}.
answer = +1.
exercise1 :: empty [checker]
exercise1 = ((-1 ok) {1})[1=>answer].
answer = +1 -2 ok.
exercise2 :: empty [checker]
exercise2 = ((-1; +2) {1})[1=>answer].
answer = +1 +2; -3.
exercise3 :: empty [checker]
exercise3 = ((-1 ok; -2 +3) {1})[1=>answer].
answer = +f(-g(X)).
exercise4 :: empty [checker]
exercise4 = ((-f(+g(X)) ok) {1})[1=>answer].
answer = -f(a); -f(b) -g(a) -g(b).
exercise5 :: empty [checker]
exercise5 = ((+f(a) +f(b); +g(a); @+g(b) ok) {1})[1 => answer].

Dynamical registers

Start from the following program:

init = +r0(0).

print process
  init.
  {replace_me}.
end

representing a memory with a register r0.

Stellogen can represent memory but in a particular way, by destroying to construct somewhere else. We cannot content ourselves of updating the register with a star -r0(X) +r0(1) as this star has a circular dependency that would allow it to be reused an unlimited number of times.

In fact, we can only move the register to modify it, for example with a star -r0(0) +r1(1) that destroys the register r0 and constructs a register r1 containing 1.

The goal is to define constellations. You can use the code above to do your tests.

Exercise 1. Define two constellations allowing to update the register r0to 1 by using an intermediary star to save the value of r0.

Solution

-r0(X) +tmp0(X).
-tmp0(X) +r0(1).

Exercise 2. Define a constellation allowing to duplicate and move the register r0 in two registers r1 and r2.

Solution

-r0(X) +r1(X);
-r0(X) +r2(X).

Exercise 3. Define two constellations allowing to set the value of r1 to 0 then define two constellations allowing to exchange the values of r1 and r2.

Solution

-r1(X) +tmp0(X).
-tmp0(X) +r1(0).
-r1(X) +s1(X); -r2(X) +s2(X).
-s1(X) +r2(X); -s2(X) +r1(X).

Exercise 4. How to duplicate r1 so as to be able to follow and update its copies all at once (as if dealing with a single register) to the value 5?

Solution

-r1(X) +r1(l X);
-r1(X) +r1(r X).
-r1(A X) +tmp0(A X).
-tmp0(A X) +r1(A 5).

Exercise 5. Using the previous method, duplicate all copies at once.

Solution

-r1(A X) +r1(l A X);
-r1(A X) +r1(r A X).

Boolean logic

We want to simulate boolean formulas with constellations. Each question uses the result of the previous question.

Exercise 1. Define a constellation computing negation such that it yields 1 as output when added to the star @-not(0 X) X and 0 when added to @-not(1 X) X.

Solution

not = +not(0 1); +not(1 0).

Exercise 2. How to display the truth table of negation with a single star, such that we obtain the output table_not(0 1); table_not(1 0).?

Solution

print @-not(X Y) table_not(X Y).

Exercise 3. Write in two different ways constellations computing conjunction and disjunction and display their truth table in the same way as for the previous question.

Solution


and = +and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1).
or  = +or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1).
and2 = +and2(0 X 0); +and2(1 X X).
or2  = +or2(0 X X); +or2(1 X 1).
print @-and(X Y R) table_and(X Y R).
print @-or(X Y R) table_or(X Y R).
print @-and2(X Y R) table_and2(X Y R).
print @-or2(X Y R) table_or2(X Y R).

Exercise 4. Use disjunction and negation to display the truth table of implication given that X => Y = not(X) \/ Y.

Solution


impl  = -not(X Y) -or(Y Z R) +impl(X Z R).
impl2 = -not(X Y) -or2(Y Z R) +impl2(X Z R).
print @-impl(X Y R) table_impl(X Y R).
print @-impl2(X Y R) table_impl2(X Y R).

Exercise 5. Use implication and conjunction to display the truth table of logical equivalence given that X <=> Y = (X => Y) /\ (X => Y).

Solution


eqq  = -impl(X Y R1) -impl(Y X R2) -and(R1 R2 R) +eqq(X Y R).
eqq2 = -impl2(X Y R1) -impl2(Y X R2) -and2(R1 R2 R) +eqq2(X Y R).
table_eqq  = @-eqq(X Y R) table_eqq(X Y R).
table_eqq2 = @-eqq2(X Y R) table_eqq2(X Y R).

Exercise 6. Define a constellation representing the formula of exclded middle X \/ ~X. Display the truth table corresponding to this formula.

Solution


ex = -not(X R1) -or(R1 X R2) +ex(X R2).
print -ex(X R) table_ex(X R).

Exercise 7. Determine for which values of X, Y and Z the formula X /\ ~(Y \/ Z) is true.

Solution

print -or(Y Z R1) -not(R1 R2) -and(X R2 1) x(X) y(Y) z(Z).

Introduction

Il existe plusieurs manières d'encoder des objets :

les encodages algébriques qui associent un sens aux symboles de fonction. Les objets sont donc encodés en tant que rayons;
les encodages interactifs, plus proche de la philosophie de la syntaxe transcendantale. Les objets sont encodés en tant que constellations. En particulier, la dynamique des objets est encodée dans les dépendances entre les rayons. Le sens des objets est donné par les types.

Encodage algébrique

Le langage Prolog utilise des encodages algébriques. Une paire pourra par exemple être représentée par un rayon +pair(X Y). Les composantes sont donc d'autres termes. Les fonctions sur les paires sont des étoiles contenant un rayon -pair(X Y) ou utilisant des symboles de fonction représentant des prédicats/propriétés comme +exchange(+pair(X Y) +pair(Y X)).

Encodage interactif

Dans un encodage interactif (plus proche de la théorie de la démonstration et notamment de la théorie des réseaux de preuve de la logique linéaire), chaque composante est donnée par une constellation.

Nous avons deux types de paires :

le tenseur où nous avons une union entre deux constellations disjointes. Nous n'avons pas forcément de fonction de projection dans ce cas;
le produit cartésien où quelque chose distingue chaque composantes et où nous aurions la possibilité d'extraire une composante en particulier (gauche ou droite).

La différence entre les deux types d'encodages est encore en cours de réflexion, je suis preneur si quelqu'un a un avis. Je pense que cela a des conséquences en expressivité et facilité de manipulation des types.

Symboles spéciaux

Stellogen définit un symbole binaire : infixe et associatif à droite nous permettant d'écrire a:X à la place de :(a X) ou encore cons(a X). Cela nous permet notamment de concaténer des symboles de façon lisible :

+f(a:b:c:e).

Séquences

Cas algébrique

Séquences fixes

+seq(a b c d).

On peut récupérer le premier élément avec :

head = +head(-seq(X1 X2 X3 X4) X1).
query = -head(+seq(1 2 3 4) R) R.
print (query head).

Pile de constantes

+list(a(b(c(e)))).

On peut ajouter ou retirer un élément en tête avec :

l = +list(a(b(c(e)))).
print process
  l.
  'push
    -list(X) +tmp(new(X)).
    -tmp(X) +list(X).
  'pop
    -list(new(X)) +list(X).
end

Remarque. On ne peut pas raisonner sur un symbole de fonction quelconque. On ne peut donc seulement empiler et dépiler des symboles spécifiques. Pour résoudre ce problème, il faut utiliser les symboles de fonction comme constructeurs et non valeurs.

Listes générales

On peut imaginer de nombreuses représentations équivalentes en utilisant les symboles de fonction pour concaténer les éléments ensemble.

+list(a:b:c:d:e).
+list(cons(a, cons(b, cons(c, cons(d, e))))).
+cons(a, +cons(b, +cons(c, +cons(d, e)))).

On peut ajouter et retirer des éléments de la manière suivante :

l = +list(a:b:c:d:e).
print process
  l.
  'push
    -list(X) +tmp(new:X).
    -tmp(X) +list(X).
  'pop
    -list(C:X) +list(X).
end

En suivant les principes de programmation logique on peut vérifier si une liste est vide :

empty? = +empty?(e).

print empty? @-empty?(e) ok.
print empty? @-empty?(1:e) ok.

Concaténer deux listes :

append =
  +append(e L L);
  -append(T L R) +append(H:T L H:R).

print append @-append(a:b:e c:d:e R) R.

Inverser une liste :

rev =
  +revacc(e ACC ACC);
  -revacc(T H:ACC R) +revacc(H:T ACC R);
  -revacc(L e R) +rev(L R).

print rev @-rev(a:b:c:d:e R) R.

Appliquer une fonction sur tous les éléments d'une liste :

map =
  +map(X e e);
  -funcall(F H FH) -map(F T R) +map(F H:T FH:R).

print
  map
  +funcall(f X f(X));
  @-map(f a:b:c:d:e R) R.

Cas interactif

Ensembles

c = +e1(a); +e2(b); e3(c).

Chaînes

c =
  @-e(1 X) +e(2 a);
  -e(2 X) +e(3 b);
  -e(3 X) +e(4 c);
  -e(4 X) +e(5 d).

Listes chaînées

c =
  @+e(1 e);
  -e(1 X) +e(2 a:X);
  -e(2 X) +e(3 b:X);
  -e(3 X) +e(4 c:X);
  -e(4 X) +e(5 d:X).

tsguide