Absolute Generality and Genericity in Models of Computability

This text was originally written in French and has been translated by AI. Original text by Luc Pommeret, submitted to Brice Halimi (Université Paris-Cité) in May 2024, as part of a philosophy of mathematics course.

Abstract

Here we wish to demonstrate that genericity and absolute generality are naturally distinct in models of computability, and particularly in the λ-calculus. We bring into dialogue two antagonistic desires: that of an integral formalism, enabling us to speak of all things, and that of an associated model of computation which always “terminates”. We observe that logic does not cover the entire domain of the computable (because of fixed points), and that logic (necessity) enables the guarantee of proper termination of calculations.

1. The Computable as General

1.1 Calculemus: the Leibnizian Reduction of Problems

“To resolve a question or terminate a controversy, adversaries need only take up their pens, adjoining a friend as arbiter if necessary, and say: ‘Let us calculate!’” — Couturat explaining Leibniz

In our analysis of models of computation, we wish to begin with the Leibnizian dream of the calculus ratiocinator to explore the different modes that can be attributed to calculation. To this end, we rely on the concepts of genericity and absolute generality. Absolute generality is the act of speaking of all things in general by aiming at all objects (the science of things in general is called metaphysics), whilst genericity is the act of targeting any object in general.

We can here mobilise the Set-Theoretic Principle of Genericity:

Given a set, reference to any member of that set is guaranteed.

This we can advantageously transpose into the world of types, in which variables live, and this is what we shall do in studying the typed λ-calculus. In this world, we can refer to any member of an inhabited type.

We shall first briefly explore the problems that presented themselves to logicians and mathematicians who wished to establish a calculus ratiocinator on a universal language, then we shall explore the question of degenerate objects of absolute generality, and finally we shall see that logic, that is to say necessity, is the guarantor of proper calculation, a calculation that terminates.

1.2 Hilbert, Ackermann and the Entscheidungsproblem

The mathematicians of the early 20th century attempted to find methods of calculation and to prove that the Entscheidungsproblem¹ was decidable, that is to say that any well-formed proposition in the language of a sufficiently powerful axiomatic theory (that of Peano, or even that of the Principia Mathematica), was decidable.

To this end, mathematicians gradually equipped themselves with a definition of computability, beginning with recursive functions, which can be traced back to Dedekind, but whose formalism is above all associated with Skolem, Ackermann, and then Gödel.

Primitive recursive functions are total functions, in the sense that their calculation terminates for any value. The counter-example of the Ackermann function shows, however, that there exists a function that is not primitive recursive, but which is nonetheless totally recursive, thus showing that the computable extended further than that.

The epigraph quotation shows that already in his time, Leibniz formulated the wish for a syntax that could express all things (whether the problem be mathematical, scientific or metaphysical), and a calculation procedure enabling the reduction of these problems. This desire necessitated two things: — A Characteristica universalis, a syntax capable of expressing all things (also seen as an international language), which must therefore be associated with absolute generality; — A Calculus ratiocinator, or calculation procedure enabling the reduction of all problems formulated in the Characteristica universalis.

The Leibnizian dream was shared by numerous philosophers at the beginning of the 20th century, including Bertrand Russell and Louis Couturat, who were both great readers of Leibniz, having published on him.

Already in his time, Leibniz considered reasoning as diagrammatic, even if his syntax sketches must be seen as a historical curiosity. We shall see in the coming sections that logicians of the early 20th century threw themselves body and soul into this Leibnizian quest for a universal language and a confluent and strongly normalising calculation, but that the diagrammatic model of calculation is an idea that would make its mark on numerous logicians and computer scientists. Kluge (1980) maintains that Frege’s Begriffschrift was inspired by this Leibnizian problem.

1.3 End Game: Gödel’s Theorems

Gödel’s first theorem marks, as we know, the end of the hope for a calculation on an absolutely general syntax, a characteristica universalis that always terminates. Certain problems are, as we know, undecidable, such that it is doomed to failure to construct a calculation founded on a universal language that has an answer to all things in general, at least in the domain of mathematics².

Gödel’s second theorem shows that in particular, the statement that proves the coherence of a system formalising arithmetic at minimum is also undecidable.

2. Exploration: Absolute Generality as the Locus of Antinomies

2.1 Russell’s Paradox: Punishment of Absolute Generality?

A well-known episode of the crisis in the foundations of mathematics, Russell’s paradox brings down the overly general, overly logicist structure of naive set theory, which was developed (amongst others) by Gottlob Frege in Grundgesetze der Arithmetik at the end of the 19th century. The paradox is devastating: it consists in using all the generality of Frege’s syntax (a mad but impossible dream of making mathematics fit within a syntax, whose entities are what can be written in it) to write a degenerate set (called Russell’s set): ${x \mid \neg x \in x}$.

The solution adopted by logicians and mathematicians is always to introduce a hierarchy between the entities considered (which Russell does with ramified type theory in the Principia Mathematica), a hierarchy between sets and classes in ZF, by adding an axiom of foundation that forbids a set from belonging to itself, and by considering de facto only sets, and not classes, as the sole mathematical entity (although this is debatable, several important objects being classes, such as the class of ordinals, for example).

Another course taken was (for logician-philosophers) to invent a much less expressive formalism, which is not subject to Russell’s paradox, but which does not permit the expression of much: mereology. This latter formalism creates no hierarchy between types of objects, nor between individuals and predicates, but is not adequate for founding mathematics (except in a hyper-finitist perspective, in which one considers that mathematics stops at a certain integer, say three billion). It is for this reason that mereology is regularly adopted as an ontology by analytical philosophers (Lewis notably), because of its reputation for neutrality and simplicity³ with regard to the postulated entities, which conforms to Occam’s razor.

In short, Russell’s paradox is a fixed point⁴ that arises in general systems, that is to say systems that wish to say much without restraining themselves with a hierarchy of entities. The analogy between naive set theory and pure λ-calculus is moreover striking:

Let $M$ be an involutive term (such that $MMx = x$).

One must take “$\in$” for the application of two λ-terms and “$\neg$” for the involutive term $M$. One recognises here the λ-term $\Omega$ which never normalises. This is a striking example that degenerates because of its excessive generality, and its lack of necessity, which lends credence to the thesis that the necessary does not saturate the universal (contrary to the correlation thesis).

2.2 λ-calculus

The λ-calculus is a formalism invented by Alonzo Church following Russell and Whitehead’s Principia Mathematica, in which the abstraction of $x$ was noted “$\hat{x}$”, which Church noted “$\hat{\cdot}x$” and then naturally “$\lambda x$”, in all generality.

As we have seen, the λ-calculus, which abstracts all things, is the locus of generality, which is concretely translated by the existence of paradoxical λ-terms, which never reduce to normal form.

Just like partial recursive functions, the λ-calculus possesses mutatis mutandis its generic equivalent, which guarantees its termination. What is interesting here is that concerning the λ-calculus, it is directly logic (the necessary) that is used to avoid loops!

This generic λ-calculus is typed, that is to say prevented from looping infinitely by a sort of logical super-ego. Here, we are interested in the simply typed λ-calculus for reasons of concision.

The type system rests on a unique typing judgement, noted $\Gamma \vdash M : \tau$ (in the context $\Gamma$, the term $M$ has type $\tau$). This judgement is derived from the following three rules:

These rules are in fact rules for the construction of λ-terms. They guarantee proper construction and proper termination of calculations, thanks to the strong normalisation property of typed λ-calculus. It is this formalism that will serve as a theoretical basis for (typed) programming languages, which cannot afford to crash as in the general case, which contains completely degenerate objects⁵.

To take an interest in the rules of construction of λ-terms is in fact to take an interest in the conditions of possibility of genericity, that is to say in how to restrict an overly general system by adding logical rules (necessity) to it. Here, necessity is directly logic itself, because when one removes the λ-terms (qualified as “decorations” in proof theory), one obtains the following logical system:

One will have recognised minimal logic, which can be extended to other logical systems via the addition of rules.

2.3 The Super-Ego of Calculation: Logic

In calculation, what prevents genericity from degenerating into absolute generality is therefore necessity, which is none other than logic itself. As we have seen, this is striking in the λ-calculus: typed λ-calculus has equipped itself with a logical super-ego that prevents λ-incest⁶.

It is at this point that we can observe that in models of computation also, universality is not saturated by necessity, for there exist places (general universality) in which logical necessity is not present. However, when we speak of typed λ-calculus, we are indeed speaking of genericity and necessity, since types are precisely derived from logic.

In this context, logic acquires a new role: that of the mechanical guarantee of calculation termination, showing that calculation without logic is a risky business, subject to paradoxes and computer crashes.

3. Logic as Guarantor of the Generality of Calculation

3.1 The Curry-Howard Isomorphism: Isomorphism of the General

We have seen that concerning calculation, logic was the introduction of the necessary into an overly general system, which had the consequence of rendering the system generic, and therefore of guaranteeing the termination of calculations.

The Curry-Howard isomorphism designates the fact (which we discussed in section 2.2) that λ-terms are the “decorations” of logical formulae, and that reciprocally, logical formulae are the “types” of λ-terms. But we can extend this correspondence further and find some twin concepts on either side of logic and calculation:

This table⁷ enables us to observe the conceptual extent of the Curry-Howard isomorphism. This isomorphism is of the domain of the generic; it only permits speaking of the generic universal, that is to say the universal guided by logical necessity.

3.2 Linear Logic or the Geometrisation of the Generic

Linear logic, emanating directly from the Curry-Howard isomorphism, was conceived from its origins in 1986 as a typing system for λ-terms. It is distinguished by an original approach to computational resources: once a resource is used, it can no longer be reused. This characteristic manifests itself fully in the truly linear fragment MLL, and allows us to envisage proofs, and therefore well-constructed λ-terms, as graphs, whose correction graphs (induced by the &s) are connected and acyclic, in other words, having a tree structure.

Cut elimination in this framework can be seen as a transformation of graphs, simplified by two fundamental rules in proof nets:

First reduction:

     ax      πm
      \     /
       cut         ⇝      πm

(Axiom-cut: the cut with an axiom is simplified)

Second reduction:

    πm   πn            πo   πp
      \ /              \ /
       ⊗                &
        \              /
         ---- cut ----

               ⇝

      πm              πn
      |               |
     cut             cut
      |               |
      πo              πp

(Tensor-Par: the cut between a tensor and a par decomposes into two cuts on the sub-proofs)

Where $\pi_m, \pi_n, \pi_o$ and $\pi_p$ are proofs.

Bearing in mind the Curry-Howard isomorphism, we can establish a parallel between λ-terms and logical formulae, and between β-reduction (calculation) and cut elimination. This perspective also authorises us to consider “interaction nets” (studied by Yves Lafont) as graphical representations of β-reduction.

We thus obtain a geometric model of calculation, observable in an elegant manner in dynamic demonstrations such as those of Interaction nets (Yves Lafont, 1995). This geometric visualisation of calculation creates the link with the oldest branch of mathematics: geometry.

3.3 The Blind Spot of Logic: Statistical Convergence, or How to Reach Our Goal with Very High Probability

But one should not therefore bury the Leibnizian project for ever. Even if in the world of certainty, the desire to reconcile a generic system, capable of speaking of all things, with a model of computation that always terminates is proved vain (halting problem, undecidability of the Entscheidungsproblem, term $\Omega$), there subsists a world in which all seems possible: that of statistics.

Universality is not saturated by necessity as we have seen, but nothing prevents a machine from deciding with high probability the halting of any other machine⁸. Property testing is a post-logical discipline in which rather than studying whether a property is true or false with certainty, one studies whether it is so with high probability (an arbitrarily high probability that one can reach with certainty).

Today, the characteristica universalis and the calculus ratiocinator raise a good laugh amongst logicians, but it may be that the problem is today formulated in other terms: does there exist a machine that can say with an arbitrarily high probability whether any statement is true or false? It may be that the characteristica universalis is vectors of high dimension, and the calculus ratiocinator a particularly vast neural network.

Conclusion

We have seen that in the models of computation that we have considered, total recursive functions and typed λ-calculus could be associated with the concept of genericity, and partial recursive functions and pure λ-calculus with the concept of absolute generality. We have been able to exploit this distinction with profit by showing that one obtains genericity by introducing logic, that is to say necessity. We have finally explored the new interactionist or geometric paradigm of generic models of computation, introduced by linear logic and interaction nets.