« Return to Thoughts
Logical interaction and the social life of proofs
Prerequisite: Curry-Howard correspondence, linear logic, proof-nets, basic knowledge of Transcendental Syntax
I illustrate the synthetic part of the Transcendental Syntax: the distinction between meaning as factory or use. This article is purely illustrative and holds no true sociological meaning.
From the beginnings of the discovery of linear logic, there was the intuition that linear logic was about “interaction” for several good reasons.
- Formulas in linear logic can be seen as limited resources or concrete objects. We have a more primitive implication $A \multimap B$ which can be connected to a formula $A$. Both occurrences of $A$ will interact, be destructed and produce $B$.
- The monolateral version of the sequent calculus for linear logic make this more explicit. The axiom and the cut rule can be seen as two kind of interaction between $A$ and $A^\bot$. The later can be removed by a computational procedure representing a kind of “reaction” of the interaction taking place. Proof-nets makes this idea more natural.
- Girard’s geometry of interaction (in its original form) see logic as a dynamics happening during the interaction of logical entities studied from general mathematics. In this context, we are interested in interaction between dual objects of the same kinds (permutations, partitions, partial isometries, …).
I believe that Girard’s transcendental currently is the only place where we can give a true meaning to the idea of “logical interaction” even though it was a major intuition for a long time.
The stellar resolution
In the transcendental syntax, all objects live within the stellar resolution which is a model of computation using constellations as elementary objects. Constellations can be understood as sets of kind of molecules called stars which can interact with each other along compatible rays and form a hypergraph representing a kind of network. Each such networks of a constellation C (there can be infinitely many of them but finitely many “correct” ones) can be evaluated into a star by contracting/destructing the tiling step-by-step and propagating information to the edges. This procedure can fail in case of conflict. It is basically a resolution of conflicts in a network (hence the name “stellar resolution”). The set of all evaluations of networks constitutes a new constellation Ex(C).
I have a funny experiment to illustrate how this model computes. Imagine the media being a big constellation. A journalist or a TV channel can be a star. A journalist says “Today, something happened”. Another one says “Today, a car accident happened”. So the network now get the information that “something” is “a car accident”. Later, another one says “from my information, it was a bike accident”. Contradiction! The whole network collapses because it is incoherent. The execution of the constellation Ex(media) is the set of coherent information we can infer.
This is very similar to the idea of local interaction occuring in physics and biology. Actually, the stellar resolution can be seen as a generalisation of a model called flexible tiles which is used in DNA computing. Moreover, it seems that DNA-based computation is able to simulate Horn clauses and clausal resolution which is very similar to the stellar resolution.
More interestingly, we can make two constellations C, C’ interact by merging them into a big constellation C + C’ we can execute into Ex(C+C’). The stellar resolution is a uniform space of entities which can compute by local interaction.
A sociological interpretation
It is not the first time that one talks about a “sociology of proofs” to illustrate the interaction occuring in linear logic. Authors such as Samuel Tronçon or Arnaud Valence mention this illustration in their PhD thesis. Girard uses the terminology vehicle (can mean car but also the more abstract definition of vehicle – e.g language as the vehicle of thought) and format (“gabarit” in French) which is a kind of specification of the vehicle. In his geometry of interaction and some papers of Transcendental Syntax, he also used some terms related to sociology. I would like to try to illustrate the Transcendental Syntax through a friendly sociological interpretation.
We can see a set of constellations as a society. It is made of distinct individuals. The Transcendental Syntax then suggests two ways of putting them into groups. If we take the illustration very seriously, an individual is not necessarily a person. The illustration is still coherent if we accept animals, objects or even an abstract notion of environment as individual. The term entity would probably be more general. The model of computation we choose as basis has an effect on the construction of such entities. In our case, we can see both an individual and its environment as entities of the same kind. The asymmetric duality subject/object becomes symmetric in some sense.
Typing by stereotypes / labelling
We select a sample of finite representative individuals forming a group A (e.g male, female, potentially criminal, nice people). We would like to judge if an individual x can be put in the group A. In order to do so, we test x against all individuals in A with a definition of what we see as a sound interaction. If x passes all the tests of A then it is part of the group A. Such a group is called type.
We can see that because the choice of sample is arbitrary and its association with a concept subjective, A can be said to be a stereotype. Clearly, it misses some cases (some individuals considered men not passing the standard tests for men) but has the advantages of being tractable. We can easily check that an individual is part of a group. It provides a kind of certainty (subjective but still certainty).
If applied to objects, this corresponds to labelling certified objects or validating a vaccine. The tests are not perfect but at least we get a finished object which should do what we want. This world of labelling is rather convenient/comfortable because we can easily name things and what they are/do. But the factory said knives should be used to cook so you cannot use them for illegal purposes.
Typing by interaction / use
Another way to classify individuals is to look at how they interact with each other. We start by choosing a criterion (orthogonality relation) defining what we mean by a good interaction between two individuals. We can form an arbitrary group by selecting any individuals we want. The orthogonal ~A of a group A is the set of all individuals which interacts well with the individuals of A. Such a group is called behaviour.
This idea of typing is way more flexible but also very complex. Depending on the orthogonality relation, the orthogonal can be very huge. It’s very difficult to reason with such notion of typing. An individual can be part of infinitely many types and subtypes naturally exist. However, the advantage is that everyone can be put into a type which was not necessarily the case with typing by stereotypes.
When applied to objects, it is a bit more abstract (hence the choice of individuals in a society as illustration). A behaviour describes how the objects can be used. A knife will be in the behaviour of objects which can kill, used to cook, cut etc. Infinitely many uses so member of infinitely many behaviours. Notice that there is no strictly separated classes such as individual/objects, they are all seen as same-kind entities which can interact (successfully or not).
If there too few types, the society is less expressive which sounds quite boring but also problematic: some individuals are not accepted because their behaviour is not accepted by the defined types. If there are too many types, it becomes chaotic and you will have to remember the pronoun of every individuals. But more importantly, we would like the stereotypes to be at least confirmed sometimes, otherwise it would lead to discrimination. It takes the form of an adequacy theorem (similarly to classical realisability) stating that the tests for A should ensure that an individual x being tested is indeed in the behaviour corresponding to A. In other words, we would like the stereotypes to be not so wrong although they will usually miss some cases (relevant or not depending on the point of view).
Cause and consequence
It is not obvious in that interactive world of independent entities but it is possible to make a notion of cause emerge. The case of labelling is the usual notion of logical consequence. No one forbid us from defining the meaning of logical consequence and its rules as done in natural deduction or sequent calculus and then checking that it works as expected (so-called harmony in natural deduction or cut-elimination in sequent calculus).
In the case of typing by interaction/use, the notion of cause/consequence is deeply related to the potentially infinite interaction/use of entities. If it happens that when an object x interacts with any objects of behaviour A and the result of that interaction is of behaviour B then x is of behaviour A -> B. A perfect coffee machine will be of behaviour Coin -> Coffee but also Credit card -> Coffee. However, I can also interact by violently hitting the machine and it will probably be of behaviour Hit -> Broken machine. If a got a coffee from the machine, I cannot always track the cause as if there was a static wiring between cause and consequence (think of weird computer bugs). Notice that it is possible to have a potential interaction with entities of infinitely many types, thus adding complexity to this machinery of interaction.
Digression: dimensions of interaction
This is a very vague idea but notice that local interactions happens in an atomic scale (DNA, atoms, molecules, …) but can also be studied in a greater scale with proofs and programs but also (as illustration) between entities such as humans, environment etc. Imagine a human interacting with a computer making a program interacts with its environment, itself triggering an electrical interaction in the circuits of the computer. The human user is also probably subject to an interaction between brain cells.
I am currently wondering if it is possible to seriously talk about such a phenomena of different dimensions of interaction. For instance, is there a kind of hierarchy of structures of interaction? Can we see a constellation as a star and a pre-type as a constellation and so on?