Interview with Alberto Naibo on the "Géométrie des Algorithmes"

A logician among philosophers: showing claims to be true

Alberto Naibo: One could say my work defies description. First and foremost, I study logic from a philosophical perspective, or rather from the perspective of philosophical inquiry. It is a crucial detail, since some logicians work in mathematics or computer science departments. As a logician who works in a philosophy department, I investigate the concept of truth. This means I ask myself questions like: What is truth ? How do we assess it ? How can we show something to be true ?

This is how we get to the broader issue of demonstration. A demonstration is the action by which we show that something is true, or by which we make its truth evident. To demonstrate thus allows us to obtain the knowledge that something is true. More precisely, we can say that a demonstration is a kind of correct reasoning enabling us to conclude that a claim is true. Yet what does that amount to ? How can we make manifest this distinction between a correct reasoning and an incorrect one ? We do this by identifying rules which allow us to obtain truth, ie. rules which necessarily lead to a true conclusion when they are applied to true premisses. We then study these rules of inference and deduction. The specific part that logicians like myself play in such investigations is the study of inference or deduction rules from a formal perspective. What matters to logicians is the form of the claims on which these rules operate, rather than their content (that is because logicians want to study truth in general, rather than study it in relation to particular language objects).

To achieve this, we use symbolic languages, where the symbols will make the form or structure of some reasoning manifest. This leads to the issue of the manipulation of these symbols. Such manipulation is done through specific rules. But these rules of inference eventually become symbolic rules. The instruments which allow us to create these rules originate notably in mathematics, like those developed in symbolic algebra. This is why the connection between logic and mathematics has grown stronger ever since the end of the 19th century. This is also how the field known today as mathematical logic was born.

Nonetheless, it is difficult to treat logic as a unified field. Mathematical logic now counts many sub-fields, each of which works with distinct mathematical theories to craft its own tools. For instance, when we study the form of demonstrations and rules of inference, we study them as authentic mathematical objects by representing them with lists, trees or graphs. Theory of demonstration is not the sole subfield within logic, however. Other topics of study include set theory, computability theory, model theory, modal logic, etc. Each of these subfields uses different instruments and formal mathematical languages — and each must be taught in a different way, best suited to its specificities. An overview of these subfields and their associated coursework is available at the Logique et philosophie des sciences Master program within the Philosophie UFR at Paris 1 Panthéon-Sorbonne University.

Studying algorithms with the GoA project

Alberto Naibo: Studying logic has led me to investigate the nature of algorithms for two reasons. The first one has to do with mathematical practice. In general, but especially in the mathematical practice of Antiquity, most demonstrations start by establishing construction procedures which can be called “algorithmic”. For instance, if we want to demonstrate the Pythagorean theorem in the same way Euclid did, we must start by setting up a procedure such that, from a given line segment (in this particular case, one side of a triangle), step by step, a square can be obtained. Such a construction procedure amounts to a finite ordered series of operations through which the input of line segments will result, step by step, in an output of squares. In this sense, these procedures are “algorithmic”. Speaking in a broad way, algorithmic procedures used in mathematics can be identified based on some common traits — it is as if they are all members of the same family. But even though some demonstrations rely on algorithmic procedures, not all kinds of reasoning or demonstration amount to algorithms. This is the second reason which led to my interest in algorithms. How to identify precisely the reasonings or procedures which are algorithms ? And how to tell them apart from the reasonings and procedures which are not ?

This being said, algorithms are among the concepts we most frequently draw on in current public discussions. These discussions are generally led by reporters and journalists, and they take on a particular style in which the claims made aim to increase polarization in debates by bringing up positive or negative future scenarios concerning the impacts of algorithms on the economy, politics or society. But in these discussions, we never clearly learn what algorithms are. When an explicit definition is provided, it often relies on too simplistic an image (eg. an algorithm may be compared to a pastry recipe). The goal of the GoA project is to give a clear account of the kind of entities algorithms are, and thus specify the ways in which we can talk about them. Specifically, the project seeks to understand whether the concept of algorithm belong to a scientific, mathematizable concept, or not. If the latter option is the case, must we accept that when discussing algorithms, our object remains vague ? Must we turn to other fields, like sociology or law, in order to specify the status of algorithms ? The GoA project thus wants to move these public discussions into an academic environment. That will allow us to show how complex algorithms are, so that we may curtail mundane predictions about how they are affecting our lives and will continue to do so.

Besides, if we look more closely at the philosophical discussions on this topic, we will notice that algorithms are often connected to the mechanization of thinking. As I said previously, from a logical perspective, inference rules are taken simply as rule operating on symbols, ie. they are signs without meaning: what matters is the sign itself, and not the fact that it refers to something else. To use the rules properly, all we need to do is to consider the properties of the signs as objects of their own, properties like form and position. In other words, operations performed on such signs do not require an existing subject or subjectivity to interpret them and understand what they mean. This is because the manipulation or combination of these signs does not require any particular cleverness. It could be performed through a kind of calculus or “blind combinatorics” (as it was called by Kurt Gödel, one of the most important logicians of the 20th century) in which human agents would be replaced by machines. In logic, these reflections led to investigations into the nature of mechanically computable functions. Many tools were developed to capture the class these functions belong to in a mathematically specific way. Without a doubt, the best known among these tools is the one designed by Alan Turing, which builds theoritical calculating machines called “Turing machines”. But other theoretical frameworks have been developed as well: the lambda calculus, general recursive functions or Post canonical systems. And we can demonstrate that any function which can be calculated in one of these systems can also be calculated in the others. This could lead us to think that the concept of a mechanically computable function is what we call a “robust” theoretical concept. (Yet one could already object that some algorithms do not behave like functions in the strictest sense, since one input can result in several distinct outputs.)

There is, however, a more profound reason to doubt that studying mechanically computable functions could give us a satisfying account of what algorithms are. Such a study only considers functions from an extensional point view, ie. it takes a function to be a simple set of “input-output” pairs. For instance, showing that a function is mechanically computable only implies showing that there is some Turing machine or lambda term by which it can be calculated. But it may be the case that the Turing machine and lambda term obtain the same outputs relative to the same inputs while calculating them in a different way. In this case, the Turing machine and the lambda term would be two different programs calculating the same function. We could thus have two programs to calculate the value of a function generating the Fibonacci sequence, one of them being faster than the other. Could we say that both programs follow or, better yet, implement the same algorithm ? The answer to such a question can be “no” if we take algorithms to be intensional entities rather than extensional entities like functions. More specifically, the answer will be negative if we do not take algorithms to simply contain and perform a procedure by which output is mechanically obtained based on a certain input, but rather take them to take into account the way in which the calculation connecting the input and the output unfolds. As a matter of fact, the same issue arises where demonstrations are concerned. If we want to show that some claim is a theorem, we need only to show that there is a demonstration for this claim — but there can be different ways to demonstrate the same theorem. For instance, we could want to produce a demonstration which is simpler than another. How could we then know when two demonstrations are in fact the same demonstration ?

Within logic, the theory of demonstration studies demonstrations like objects in a mathematical theory. It develops special technical tools enabling researchers to perform operations on demonstrations and to study their properties. As such, it investigates demonstrations from a general and abstract perspective. The GoA project wants to look into the possibility of a similar theory for algorithms, and thus lay the foundations of a general theory of algorithms. To accomplish this, the project takes as its starting point a result obtained in mathematical logic known as the Curry-Howard isomorphism. It shows that there is a correspondence between formal demonstrations of some logical theories (which are usually written as natural deductions or sequent calculus) and computer programs (usually written with lambda calculus). Within that framework, asking whether two demonstrations are the same amounts to asking whether two programs are the same. We can then transfer methods and inquiries from one field to another — from logic and mathematics to theoretical computer science, and vice versa. Furthermore, if we think that writing a program is a way to implement an algorithm, then inquiring into the identity of different programs also becomes a way to inquire into the identity of different algorithms. This goes to show that the GoA project finds its natural place at the intersection of logic, philosophy of mathematics and philosophy of computer science.

Conducting interdisciplinary research

Alberto Naibo: The GoA project brings together several researchers from France and other countries. Most are affiliated with the Institut d’histoire et de philosophie des sciences et techniques (IHPST, UMR 8590), but some are from other French universities — like Jean-Baptiste Joinet, Professor at Lyon III University, and Liesbeth de Mol, CNRS researcher at Lille University — or from other universities — like Mattis Petrobo, Associate Professor at the Federal University of ABC Sao Paulo, and Walter Dean, Associate Professor at Warwick University (and was a Fellow with the Paris Institute of Advanced Studies in 2022-23). Most of us are “junior” researchers with different skills and trainings. For instance, Walter Dean has been trained in two fields, with one PhD in philosophy and another in theoretical computer science. But our ranks also count a mathematician like Thomas Seiller, who was trained in logic and philosophy at Paris 1 University: he and I met there as students, roughly 15 years ago now, and we have continued to collaborate on papers and projects since then. The mathematical skills and tools Thomas developed to work on problems of logic and computation complexity incidentally play a foundational role in the GoA project. Philosophers involved in the project also have interdisciplinary profiles, with training in mathematics, computer science and physics. Filippos Papayannopoulos, for instance, has been recruited as a postdoctoral researcher on the project, and has been trained in both physics and philosophy of science. But I can also mention Pierre Wagner, who wrote one of the very first doctoral dissertations on the significance of computer science and artificial intelligence in philosophy, and Marco Panza, who is currently working on how the way in which we handle large databases transforms our use of mathematics in the sciences. The work of Liesbeth de Mol, Jean-Baptiste Joinet, Mattis Petrolo and Walter Dean — whom I have mentioned before — also takes place at the juncture of philosophy, logic and theoretical computer science.

Let me point out that it is because of our interdisciplinary team that we were naturally led to interact with colleagues from Paris 1 University who, coming from different fields, were all interested in the issues surrounding AI. For instance, I had the opportunity to meet Stéphane Lamassé, from the History UFR, through the Sciences des données et IA initiative by UNA Europa. Stéphane and I then discussed the historical and philosophical aspects of algorithms.

One of the aims of the GoA project is to refrain from dogmatism surrounding our formal logic-centric approach. On the contrary, we want our analysis to draw on other approaches—since the concept we are investigating is in itself not limited to a single field. This is precisely why the GoA project includes workshops contrasting the use of algorithm as a notion in logic and in law.

Adopting a geometrical approach to study algorithms

Alberto Naibo: The hypothesis we use as a starting point is that we can only identify a truly scientific status for algorithms if we can account for them through a specific mathematical representation expressing measurable properties. The core idea leading our project is that such a representation can be designed based on geometry. Our geometrical approach should allow us to clearly set out the relations between algorithms and similar — yet distinct — concepts like calculation and program. This kind of analysis aims to lay the groundwork for a computer science ontology. Computer science could thus become a thoroughly mathematized theory, like physics. It is an essential feature of the project: the technical analysis of algorithms cannot be dissociated from conceptual analysis, because the concept of algorithm is found at the end of a conceptual ascent starting with the concepts of calculation and program. In order to convey this idea properly, and to explain what exactly is the geometrical approach I spoke of above, I have to discuss some matters into more detail.

First, my reference to physics as the scientific ideal of a fully mathematized theory was on purpose. There is research showing a connection between computation and physics — like the work of a student of Turing, Robin Gandy. More specifically, this work shows that a calculation process amounts to a physical process we can represent using dynamical systems as they are commonly described in mathematics, ie. using a space X and a fraction f associating an X with an X. Considered in this way, a calculus will be analyzed as a deterministic phenomenon, since it is described as a function in which each input yields one and only one output. In contemporary science computer practice, however, we are concerned with non-deterministic programs in which one input can result in different outputs. For instance, a probabilistic program will give two different results when it is run twice on the same input. Non-deterministic programs can thus both describe several possible calculi — even though each time the program runs, only one calculus is the actual output and triggers a deterministic process. This points to the fact that it is the passage from calculus to program which can account for the various modes or ways to calculate. This is where the concept of calculus model comes in. If we want to bridge the gap between calculus and program in our conceptual scale, we must use calculus models whose concept will be more general than dynamical systems (the latter being particular cases), but which we can also generalyze further to capture much richer concepts like programs. Our idea is to think of calculus models as actions performed in some space. We can think of this space as the one of all possible configurations for a machine (be it theoretical like a Turing machine, or concrete like a computer) and think about the primitive operations of this machine as giving definitions for actions in this space. And, since we can always generate new operations by performing primitive operations one after the other, what we are doing, mathematically speaking, is generating a monoid based on these primitive operations. In an abstract way, we can thus think of a calculus model as an action by a monoid M in a space X. This is where the geometrical approach of the GoA project becomes apparent. To see this clearly, we need to recall the fundamental idea behind the Erlangen program (designed at the end of the 19th century by the mathematician Felix Klein): that one could classify kinds of geometry based on the actions of a group of transformations in a space (and on the invariants created by these transformations). The GoA project is led by a similar idea: to classify programs based on the actions of an operation monoid in a space, and then to describe algorithms as more general structures implemented by programs. More specifically, we take programs to be graphs geometrically realised on a measurable space. The vertices in the graphs are subspaces (here configuration sets for a machine) and the edges are elements from monoid M (here machine operations). Let us use as an example an instruction given to a Turing machine: “if 0 is read, then the sensor moves to the right.” In our graph framework, this would mean that we have an edge whose source is the subspace of configurations where the sensor reads 0, this edge itself representing the monoid element “moving the sensor to the right”. I cannot go in more detail here. I will simply point out that since the edge in a graph can be the source of several vertices rather than only one, this mathematical framework naturally accounts for the non-deterministic programs we mentioned previously.

Using graphing, we can also account for a program’s execution dynamic. And if we give a weight to the graph’s edges and express it with a real number, we can even determine an execution path measurement in the graph space. Once programs are defined as graphs, algorithms can be defined as generalizations of those programs. To do this, we represent an algorithm as a graph A and we say that graph G implements graph A if there is some morphism from A to G. What is quite significant here is that a correspondence between an edge in A and an edge in G through morphism is not necessarily required. We can also establish a correspondence between an edge of A and an entire graph, like a subpart of G. To explicate this point, let us look into Euclid’s algorithm to calculate the highest common dividing number of two whole numbers. These can be a program P_¹ which implements this algorithm, and in which the modulo operation (which gives the rest of the division of two whole numbers) is a primitive operation. But there can also be a program P_², which calculates the highest common dividing number by calculating the rest of the division of two whole numbers with a subprogram P₃ defining the modulo operation as an iteration of the subtraction operation. This being laid out, Euclid’s algorithm can be represented with a graph A_E where all edges similarly labelled — for instance, edges e — correspond to the modulo operation which is the monoid element supporting graph G₁ representing P₁. We could then take this same graph A_E and connect edges e to graph G₃ representing P₃, G₃ being itself a subpart of graph G₂ representing P₂. This would allow us to say that P₁ and P₂ implement the same algorithm, since graphs G₁ and G₂ both implement the same graph A_^E. But we do not have to identify P₁ with P₂. For the way in which we describe algorithms is general enough to let us connect these two programs with the same algorithm — but it lets us connect them with two distinct algorithms as well, depending on the kind of morphism we use. This framework even allows us to account for cases where two algorithms are implemented by the same program.

This leads me to another crucial aspect of the GoA project. Our description of algorithms does not depend on a syntactic analysis where algorithms are texts resulting from a list of instructions or primitive operations, written in a semi-formal, code-like language. Our analysis rather uses actions or calculation steps, whose description can require several instructions or primitive operations. A calculation step is thus the unit we take to be relevant when it comes to describing some specific algorithmic process. What is at stake here is a crucial epistemological hypothesis: algorithms are not entities which exist independently from the users using them. Likewise, the way in which we describe algorithms is not absolute, but is more or less fine-grained depending on the interpretation resulting from user perspective. Identifying algorithms thus amounts to clarifying programs according to the types of behavior they share. Such types will, however, vary according to the aspects we single out when comparing programs.

I have talked quite a lot on this topic already. But I want to add one last thing to connect the kind of work I do within the GoA project and the one I do in logic and theory of demonstration. The idea that we can see graphs as programs was developed in Thomas Seiller’s work: he had used these graphs to study the structure of demonstrations in some linear logic systems within the framework of the Curry-Howard correspondence. And, as linear logic is one type of logic in which we can account for the resources used in a calculus, it seems natural to use graphs as a mathematical framework to tackle problems of computation complexity. Such problems point to yet more fundamental epistemological issues, which concern calculation feasability. Indeed, we can wonder whether computation capacities resulting from our use of algorithms can extend indefinitely beyond our own cognitive capacities, and thus lead to the creation of “superhuman intelligence”, or if there are theoretical limits to those capacities which humans or algorithms will never exceed.

⇒ Watch (in French): What is an algorithm? A geometrical approach (a contribution to the ANR CulturIA project seminar).

The role of AI in the GoA project

Alberto Naibo: When we ask what tasks we can perform using algorithms and what their limits would be, we naturally come to questions about artificial intelligence (AI).

In general, we can describe AI as the use of computer programs simulating behaviors (or otherwise obtaining results) which we consider characteristic of human intelligence. Yet the history of AI is quite complex, especially given the significant changes having occurred in the field in recent years. We could go as far as to say that AI has several souls, since there are several technologies — and paradigms, even — for AI. These include AI focused on data processing through the massive use of statistical tools, which is the one public discussions usually refer to under the generic name of AI; but there is also AI concerned with knowledge representation through the use of language and logical theories (like modal logic, epistemic logic or non-monotonic logic); and then there is AI which uses technology derived from combinatorics and automated reasoning. We must also note that the prime examples of AI activities changed over time: in the 1950’s, when AI was born, the most significant examples of what AI could do came from mathematics, while today’s prominent cases are object regognition and classification. For instance, one of the first results obtained in AI research was the development of a program by Allan Newell, Herbert Simon and Clifford Shaw. Called the Logic Theorist, this program could demonstrate — or, to put it better, it could re-demonstrate — most of the theorems of Alfred North Whitehead and Bertrand Russell’s Principia Mathematica. The Logic Theorist relied on heuristics, ie. practical methods for demonstration which are flexible, work in most cases and have low calculation costs, even though they are not guaranteed to reach a solution. But work in automated demonstration search have also benefited from results in decision and methods originating in logic (like resolution and unification). This work has led to some notable results, such as the demonstration in 1996 of the Robbins algebra, an abstract algebra problem, by a program developed by William McCune and his research group. This conjecture had been open for nearly 60 years, and this program running on an IBM RS/6000 generated a demonstration for it through purely automated processes after 8 days of work.

It is only in the last few years, however, that AI’s success in mathematics seems to become less irregular and anecdotal. SAT solvers — programs which use algorithms or heuristics to solve the satisfiability problem for formulas of propositional logic, ie. whether Boolean truth values (true and false) can be assigned to variables in a propositional logic formula so as to make that formula true or not. Thanks to techniques developed by SAT solvers, several open mathematical problems have been solved — originating in geometry (like Keller’s conjecture), or from a branch of combinatorics called Ramsey theory (like the Boolean Pythagorean triples problem, or BPTP). The idea driving the resolution of these problems is to translate or “code” the problem’s description into a propositional logic formula, and then to check whether it is satisfying or not. In the case of the BPTP, the formula obtained by Marijin Heule, Oliver Kullman and Victor Marek for the problem contained 7,825 propositional variables. This means that, since each variable can be assigned either true or false as a truth value, there are 2^{7 825} possible cases to consider. Such an amount of cases is much higher than what we are used to process. Indeed, 2^{7 825} is larger than 10^{2 300}, while we estimate the number of particles in the universe not to exceed 10¹⁰⁰. Even if we assigned a truth value to every particle in the universe, we would still have a long way to go to consider all possible assignations in the BPTP formula. Running SAT solving algorithms through this formula, however, allows us to automatically rearrange and decompose it. This drastically reduces the number of cases to take into consideration (for instance, by getting rid of non-relevant cases), and makes the problem solvable by the sole calculating power of computers. More specifically, Heule, Kullmann and Marek ran the algorithms on 800 parallel superprocessors during 2 days, and obtained an answer: the initial formula is not satisfiable. The problem was thus solved using the brute force of algorithms and computers (the idea that brute force can be used to solve a problem is not new; there is, incidentally, a name for it in Russian: “perebor”). This situation is quite different from other cases of computer-assisted demonstrations, like the well-known demonstration of the four color theorem by Kenneth Appel and Wolfgang Haken. In this case as well, the demonstration involves the analysis of a number of a cases, which is about one thousand (the number can vary in different versions). But this number is much lower than in the BPTP case, and what is more, the number of cases is determined by hand by mathematicians who conduct their own analysis of the problem. All the computer does is to verify the cases selected. Contrastingly, for the BPTB, the cases which the computer effectively verifies (and whose number is theoretically inferior to the 2^{7 825} possible cases) are selected through the use of SAT solving algorithms on the initial formula. The selection thus operates in a purely mechanical way, and requires no human intervention or cleverness. The problem has then been solved, so to speak, blindly. Does this mean that the resulting demonstration has no epistemological or explanatory value ? Or is there a kind of mechanical intelligence at play here ? Could it be that analyzing the algorithmic structure of this demonstration with the tools developed as part of the GoA project would enable us to extract information to compare this demonstration with other, more “traditional” demonstrations ?

All this shows that it is essential to study algorithms if we want to understand the current evolution of mathematical demonstrations under the impulse of AI-related technologies.