This is the link to the Pure See draft which will soon be updated.
What is Pure See
It is a common language over all versions of chemlambda, like chemlambda v2, dirIC or kali. All these versions of chemlambda are machines, or models of computation. They are graph rewrite systems with an algorithm of application of the rewrite rules.
It became clear that there is a common source from which all these graph rewrite automata come, and that many more are possible. They all share some part of a set of 6 trivalent nodes and we can prove that there is only one graph rewrite schema called SHUFFLE which generates all particular graph rewrites encountered in these models. (The way it generates it is via a “passage to the limit” so to say, or “emergent” schema, which deserves a separate explanation.)
Thus Pure See is a language version for graphs made of these 6 nodes, the SHUFFLE rewrite schema and the passage to the limit schema.
As 6 = 3!, we need 3 words to generate, by permutations, any of the 6 nodes. These 3 words are “from”, “see” and “as”.
Hence the name “Pure See”.
Pure See syntax as map making
When we make a map of something we see, in the most abstract way we need to mention 3 things:
- (1) where we are
- (2) what are we looking at
- (3) what is the representation, or name, or symbol of what are we looking at (2) as seen from where we are (1)
We say:
from a see b as c
and we mean
- from a (where we are)
- see b (we look at b)
- as c (we represent it as c)
But of course that “a”, “b”, “c” are just names. What matters is the structure given by “from”, “see” and “as”.
There are 6 permutations of this structure and each of them correspond to one (type of a) trivalent node.
Mind that trivalent nodes are just nodes with a node type and 3 ports together with an ordering of the ports. We write
Q a b c
to denote a node of type “Q” and with 1st port with name “a”, 2nd port with name “b” and 3rd port with name “c”.
Such nodes form graphs by connecting ports. Each edge has an unique name and two ports with the same name are connected by the edge with that name. The names of the edges don’t matter (we can rename them and we still have the same graph). We present the graph as a “mol” (short from “molecule”) which is just a list of node denotations. Of course, the order of the nodes in the list does not matter, we can permute the nodes and we still have the same graph.
At the language level this means that a proposition like “from a see b as c” represents a node (we’ll see how immediately), that graphs are represented as lists of such propositions, but the order of propositions does not matter, and that names like “a”, “b”, “c” can be modified by renaming into anything (except code words like “from”, “see”, “as”) with the condition that they are unique as names in the “mol”. Mind that each such name appears at most twice in a mol (i.e. twice if it representes an edge between two ports and only once if it represents a half-edge with the other end free). Therefore a renaming is a bijective trasformation of the list of names into another list of names, which is then used to replace in a mol each old name with the new name.
Now let’s see how to represent the type of the node in this language. It is simple: there are 6 permutations of 3 things and we have 6 nodes (types) to represent. These are
- from a see b as c, i.e. D a b c
- see a from b as c, i.e. L a b c
- as a from b see c, i.e. A a b c
- see a as b from c, i.e. FI a b c
- from a as b see c, i.e. FOE a b c
- as a see b from c, i.e. FOX a b c
The name of the node types is partly historical, like “FOE” which comes from “external FO” (and “FO” means “fanout” and “FI” means “fanin”), or like “D” which means “dilation” (from dilation structures or emergent algebras).
Forget about these names for now, but remember them later when you read the algebraic heuristics and anharmonic group sections.
Think that a priori these are 6 possible propositions which describe map making, or the descriptions of 6 different situations encountered when we make a map.
They are though related in subtle ways with well known subjects, like lambda calculus or interaction combinators. For the relation to interaction combinators go back to the link to dirIC.
Relation to lambda calculus
Lambda calculus is a term rewrite system. We can turn a lambda term into a graph (it’s syntax tree modified in a certain way) which uses 3 node types: L for lambda, A for application and a FO node for fanouts. We need fanouts because in a term rewrite system we are allowed to use many times the same variable name, or when we turn the term into a graph we need FO nodes to mark that several variable names are “the same”.
But “FO” type of node is not among out 6 nodes. Later, in another part, about this.
As lambda calculus is an inspiration for chemlambda, which in turn is in the scope of Pure See (excepting the FO node which has a special treatment), there is an association which we can make between lambda calculus and Pure See.
As concerns the lambda and application, they look like this, when we just suppose that we don’t care about repeated use of the same name variiable:
- in lambda calculus we write \x.A = B and in Pure See this is translated into “see A from x as B”
- in lambda calculus we write A B = C and in Pure See this is translated into “as A from B see C”.
Let’s see how we do this with some examples:
I = \x.x is “see x from x as I”
K = \x.\y.x is “see x from y as a; see a from x as K”
therefore there is this new “a” which is just “a = \y.x” here, so “K = \x.a”.
When we want to write for example
S = \x.\y.\z.((x z) (y z))
then is more difficult because we see that “z” appears 3 times. Just ignoring this, we might write in Pure See the following thing which is not a mol:
“see a from x as S;
see b from y as a;
see c from z as b;
as x from z see d;
as y from z see e;
as d from e see c”
It is not a mol because “z” appears 3 times. In the following we shall allow this, for the sake of the exposition. (But see Substitution is objective (II) for more.)
Algebraic heuristics
Well, the notation of the S combinator is not comfortable, so why not eliminate the intermediary a,b,c,…? For the lambda is simple:
instead of “see a from x as c” just write “c = see a from x”, rather close to “c = \x.a”.
We did something like this algebraic heuristics
see a from b as c = 0
see a from b = – as c
(see a from b) / (-as) = c
and we took as = -1 to obtain:
see a from b = c
Let’s try the same for the application:
as a from b see c = 0
as a from b = – see c
as a from b = see as c
(as a from b) / (see as) = c
(as / (see as)) a (from / (see as)) b = c
(1/see) a (from/ (see as)) b = c
We introduce new keywords
apply = 1/see
over = from/(see as)
and we get
apply a over b = c
which is very close to “a b = c” from lambda calculus.
Then, all in all we would have
S = see (see (see (apply (apply x over z) over (apply y over z)) from z) from y ) from x
which is a bit more verbose than lambda calculus, but it is recognoscible.
Anharmonic group
The algebraic heuristics is weird, but what we did?
The “from”, “see” and “as”, also “apply” and “over”, are like scalars.
The “a”, “b”, “c”, .. are like vectors.
Juxtaposition like apply a over b = c is vector addition.
But! The vector addition is not commutative, otherwise we collapse all permutations of the 3 “from”, “see”, “as”, into one.
Multiplication by scalars is distributive, OK.
as = -1
and any proposition is = 0.
Oh, 0 is a special vector, call it “origin”.
Recall now that the 6 permutations of 3 elements (here “from”, “see”, “as”) are a group, which is none the other than (isomorphic to) the anharmonic group.
The anharmonic group is made of 6 rational functions, of a parameter z (complex if you like). We can give roles in this game so that all the syntax explained, and the algenraic heuristics make sense, by a kind of magic.
For this let’s enumerate the 6 rational functions, with names from Pure See:
see[z] = z
from[z] = 1 – z
apply[z] = 1/z
over[z] = (z-1)/z
with[z} = 1/(1-z)
note[z] = z/(z-1)
This form a group with composition of functions. For example
see[from[z]] = from[z]
or
with[apply[z]] = note[z]
and mind that addition and multiplication of scalars is commutative.
To these 6 functions with made up names we add two more:
as[z] = -1
in[z] = 1
So then indeed
over[z] = from[z] / (see[z] as[z])
or
apply[z] = in[z]/see[z]
as we wrote in the algebraic heuristics.
As for the isomorphism of the anharmonic group with the 6 permutations which denote node types, this can be recovered from solving equations.
Indeed, we shall replace, formally the “from”, “see”, “as” with their functions, juxtaposition with vector addition with “+” and remember that “+” with vectors is not commutative!
from a see b as c becomes
from[z] a see[z] b as[z] c = 0
(1-z) a + z b + (-1) c = 0
(1-z) a + z b = c
We associate the node D, or the proposition “from a see b as c” with the function see[z] = z from the anharmonic group.
Now watch the treatment of L
see a from b as c
becomes
z a + (1-z) b + (-1) c = 0
z a + (1-z) b = c
(1 – (1-z)) a + (1-z) b = c
which after all it could be written as
from[from[z]] a + see[from[z]] b = c
that is
from[1-z] a + see[1-z] b = c
That is why we associate from[z] = 1-z with the node L, or with the proposition “see a from b as c”.
This works for the two propositions with end with “as”, but what we do with those which end with “see”?
We already explained this for A, or “as a from b see c”, let’s do it properly now
as[z] a + from[z] b + see[z] c = 0
(-1) a + (1-z) b + z c = 0
(-1) a + (1-z) b = (-z) c
(1/z) a + (z-1)/z b = c
which is indeed
apply[z] a + over[z] b = c
but also
from[over[z]] a + see[over[z]] b = c
which tells us that A, or the proposition “as a from b see c” is associated with the function over[z] = (z-1)/z from the anharmonic group.
All in all the 6 propositions from Pure See have the same equivalent form
from[g[z]] a + see[g[z]] b = c
for g[z] one of the 6 functions of the anharmonic group.
All this structure is not randomly here, it has to be explained intrinsically.
Note for example that if we believe that the association with the anharmonic group has any meaning, then we should have nontrivial relations between scalars, like
as from = see over
or
apply from = as over
For the moment we don’t have any more structure in Pure See, because there was nothing about the SHUFFLE schema.
But we can still play with the look of the beta rewrite in this language.
(\x.A) B
is written as (I’ll not put the “+” between “vectors”)
apply(see A from x) over B
We use the distributivity of the scalar multiplication (not yet justified)
((apply see) A (apply from) x) over B = C
(in A (as over) x) over B = C
… if the vector addition would be associative, then
in A ((as over) x over B) = C
then again distributivity
in A over (as x in B) = C
which is a kind of
A[x/B] = C
if we interpret the beta rewrite as meaning
as x in B = origin
otherwise said
x = B
and as a consequence
in A over origin = C
which, because origin is the neutral element of the vector addition, reads
A = C
But why? That is for later.
the condition (COLIN) impliex the condition (LIN)
and for any 
we have 
, otherwise arbitrary. (COLIN) is then equivalent with 
with 
and then we use (R2) and some groupings of terms then we obtain the following relation equivalent with (COLIN):
is a relative operation, namely 
to 
by using the topological axiom (em) and we obtain in the limit the following 
is the limit of 
, based at 
. We write it like this 
we deduce from (COLIN) the relation 
to 
equal to the scalar 
(up to an arbitrary exponential). 
and (LIN) for the infinitesimal level gives us the equivalent 
)
this time and we obtain that 
