Gilles Dowek
email: gilles.dowek@inria.fr

Around the physical Church-Turing thesis: cellular automata, formal languages, and the principles of quantum theory

The physical Church-Turing thesis explains the Galileo thesis, but also suggests an evolution of the language used to describe nature. It can be proved from more basic principle of physics, but it also questions these principles, putting the emphasis on the principle of a bounded density of information. This principle itself questions our formulation of quantum theory, in particular the choice of a field for the scalars and the origin of the infinite dimension of the vector spaces used as state spaces 1 .

1 The Church-Turing thesis and its various forms

Why a thesis?

It is a quite common situation in mathematics, that a notion, first understood intuitively, receives a formal definition at some point. For instance, the notion of a real number has been understood intuitively in geometry, for instance as the length of a segment, before it has been formally defined in the 19th century, by Cauchy and Dedekind. Another example is the notion of an algorithm, that has been understood intuitively for long, before a formal definition of the notion of a computable function has been given in the 30s, by Gödel and Herbrand, Church, Turing, and others.

There is however a difference between these two notions. When the notion of a real number was defined, there seems to have been no real discussion of the fact that the formal definition of Cauchy or Dedekind was indeed a formalization of our intuitive notion of a real number. In the same way, there is no discussion of the fact that the formal definitions of the notions of a triangle, a square, or a circle are indeed formalizations of our intuitive notions of a triangle, a square, or a circle. Even for the formal definitions of the notions of a distance and of orthogonality, based on the notion of an inner product, we finally agree that they correspond to our intuitive notion of a distance and of orthogonality.

The situation is different with the notion of a computable function, as the formal definition of this notion came with a thesis that this formal definition indeed captures our intuitive notion of computability.

This peculiarity of the notion of a computable function can be explained by its history. Before the modern definition, another had been given: the notion of a primitive recursive function, and it was then noticed that there existed functions, such as the Ackermann function, that were intuitively computable, but not primitive recursive. This has raised a reasonable doubt that history may repeat itself and that another counterexample may be given to this new definition.

The physical Church-Turing thesis

Stated as such, the epistemological status of the Church-Turing thesis is unclear. It cannot be proved, as it uses a notion that is not formally defined: that of a function computable in the intuitive sense. It cannot be experimentally tested as it is not a statement about nature. But it could be falsified, if anyone came with a counterexample, i.e. a function that is not computable in the formal sense, but such that everyone agrees that it is computable in the intuitive sense, as it happened with the Ackermann function. Yet, this requirement of a consensus on the computability, in the intuitive sense, of this function puts it at the border of falsifiability. Thus, stated as such, the Church-Turing thesis is hardly a thesis, and several attempts have been made to replace this notion of computability in the intuitive sense by a more precise notion. These attempts go at least in three directions.

-The first is to axiomatize a computability predicate and to prove the equivalence of this implicitly defined notion with that defined by Gödel and Herbrand, Church, Turing, etc. This is the way taken by Dershowitz and Gurevich [START_REF] Dershowitz | A natural axiomatization of the computability and proof of Church's thesis[END_REF], and others. -The second is to define a notion of computability based on the analysis of the operations executed by a human being performing a computation and to prove the equivalence of this notion with that defined by Gödel and Herbrand, Church, Turing, etc. This is the way taken by Turing himself, and others. -The third is to define a notion of computability based on the analysis of the operations executed by a machine performing a computation and to prove the equivalence of this notion with that defined by Gödel and Herbrand, Church, Turing, etc. This is the way taken by Gandy [START_REF] Gandy | Church's thesis and principles for mechanisms[END_REF], and others.

The thesis expressing that any function computable by a machine is computable in the sense of Gödel and Herbrand, Church, Turing, etc. is called the physical Church-Turing thesis.

Giving a meaning to this thesis requires to give a definition of the notion of a machine. A machine is any physical system, equipped with a interaction protocol defining a way to communicate some information to the system by choosing some parameters a = ⟨a 1 , ..., a n ⟩, when preparing the system, and to extract some information from the system, by measuring some values b = ⟨b 1 , ..., b p ⟩.

Such a machine defines a relation: the relation R such that a R b if b is a possible result for the measurements, when the chosen parameters are a. We say that this relation R is realized by this machine. For instance, if one applies an electrical tension U to a conductor of resistance R and measures the current I passing through this conductor, then a = ⟨U, R⟩ and b = I and the realized relation is that relating ⟨U, R⟩ and I when U = RI. In the same way, if one lets a body freely falling in vacuum for some time t and measures the position x of this body, the realized relation is that relating t and x when x = 1 2 gt 2 . The physical Church-Turing thesis expresses that relations realized by a machine are computable.

The physical Church-Turing thesis is obviously a thesis about nature. Thus its correctness depends on the world we are in. It is easy to imagine worlds where this thesis is valid and worlds where it is not. In particular this thesis is not valid in worlds where accelerating machines or infinitely parallel machines can be built. The theory of hypercomputability studies such worlds.

Yet, not everyone agrees on the epistemological status of this thesis. According to some, such as Deutsch [START_REF] Deutsch | Quantum theory, the Church-Turing principle and the universal quantum computer[END_REF], this thesis -or its negation -is a principle of physics, like the homogeneity of space or the homogeneity of time. According to others, such as Gandy, this thesis -or its negation -must be established as a consequence of other principles of physics. There is no real contradiction between these two points of view, as we know that the choice of axioms in a theory is somewhat arbitrary. For instance, in set theory, we may chose a particular form of the axiom of choice and prove the others. Yet, some propositions are simple enough to be taken as axioms or principles, and others are not.

Beyond natural numbers

Computability is primarily defined for the functions from the set of natural numbers to itself, but many functions we use when discussing the physical Church-Turing thesis are defined on other domains. Thus, the notion of computability must be defined beyond the set of natural numbers.

Indexings

The first way to define a notion of computability on a set S different from the natural numbers is to transport the notion of computability from the set of real numbers to the set S with the use of an indexing, i.e. a bijection ⌜.⌝ between S and a subset of N.

Then, a function f from S to S is said to be computable, if there exists a computable function f from N to N such that for all x in S, ⌜f (x)⌝ = f (⌜x⌝).

An objection to this method, due to Montague [START_REF] Montague | Towards a general theory of computability[END_REF], is that the defined notion of computability depends on the choice of the indexing. To see why, let us consider an undecidable set U , that does not contain 0 and the function D mapping -2n to 2n + 1 and 2n + 1 to 2n if n ∈ U , -2n to 2n and 2n + 1 to 2n + 1 otherwise. Then, consider a set S, an indexing ⌜.⌝ of this set, elements u and v in S such that ⌜u⌝ = 0 and ⌜v⌝ = 1, and the function f from S to S defined by f (x) = u if ⌜x⌝ is is even and f (x) = v otherwise. As the function f from N to N defined by f (n) = 0 if n is even and f (n) = 1 otherwise is computable, the function f is computable with respect to the indexing ⌜.⌝.

But, the function

D • ⌜.⌝ is also an indexing of S S f S f N N D D N f N and the function f = D • f • D is not computable. Indeed f (2n) = 1 if and only if D( f (D(2n))) = 1 if and only if D(2n) is odd if and only if n ∈ U .
Thus, the function f is not computable with respect to the indexing D • ⌜.⌝. The computability of f therefore depends on the chosen indexing. Thus, unless we have a canonical way to represent the parameters a and the measured values b by natural numbers, the formulation of the physical Church-Turing thesis is relative to the choice of an indexing.

Three answers have been given to this objection. This permits to define indexings for all articulated sets of trees, where a set of tree is articulated if it is n-articulated for some n, 0-articulated if all its elements are labeled in a finite set and (n + 1)-articulated if all its elements are labeled in a n-articulated set of trees. For instance, proofs are trees labeled by sequents, that are trees labeled by formulae that are trees labeled by function symbols, predicate symbols, and variables, that are trees labeled in a finite set. Thus the set of proofs is articulated. In a similar way, all the sets of syntactic objects, formulae, proofs, programs, etc., are articulated.

Articulation A list
Let S be an articulated set of trees, ultimately labeled in the finite set E. Using the canonical indexing of trees above, we can transform any indexing ⌜.⌝ 0 of the set E into an indexing ⌜.⌝ n of S by ⌜f (t 1 , ..., t k )⌝ r+1 = (⌜f ⌝ r ; ⌜t 1 ⌝ r+1 ; ...; ⌜t k ⌝ r+1 ; 0) As all finite functions are computable, the choice of the indexing ⌜.⌝ 0 is immaterial and all the indexings based on this canonical tree indexing define the same set of computable functions.

Finite generation This argument has been generalized by Rabin [START_REF] Rabin | Computable algebra, general theory and theory of computable fields[END_REF] to all finitely generated algebraic structures.

In mathematics, we are not interested in sets per se, but in structures, i.e. sets equipped with operations: ⟨N, S⟩, ⟨N, +, ×⟩, ⟨L, ::⟩, ⟨L, @⟩, etc. As their name suggests, these operations must be computable. Thus, when indexing a structure, we must restrict to the admissible indexings: those that make these operations computable.

A structure is said to be finitely generated when all its elements can be built from a finite number of elements with the operations of the structure, for instance the set of natural numbers equipped with addition, the set of lists of elements of a finite set equipped with concatenation, the set of rational numbers equipped with addition, multiplication and division, etc. are finitely generated structures.

When a structure is finitely generated, if i and j are two admissible indexings, then there exists a computable function f such that j = f •i. Thus, all admissible indexings define the same notion of computability: computability is stable.

In particular computability is stable on all the finite extensions of the field of rational numbers, all the finite-dimensional vector spaces over such fields, etc. [START_REF] Arrighi | On the completeness of quantum computation models[END_REF].

Computability of sets of functions Programs in a given programming language are lists of letters in a finite alphabet. We have seen that, as the set of lists of elements of a finite set equipped with concatenation @ is finitely generated, all its admissible indexings define the same set of computable functions, and the characteristic function χ of the set of terminating programs is non computable, relatively to any admissible indexing. In other words, for any indexing, if the function @ is computable, then the function χ is not.

Boker and Dershowitz [START_REF] Boker | The Church-Turing thesis over arbitrary domains[END_REF] have suggested that this result could be stated without focusing on the concatenation operation @, as the fact that the functions @ and χ cannot be both computable, with respect to the same indexing. Calling a set of functions computable, if there exists an indexing with respect to which all the elements of the set are computable, the set {@, χ} is non computable, in an absolute sense.

The set {χ} is computable as it is possible to cheat on the indexing and associate an even number to terminating programs and an odd number to non terminating ones, but the price to pay is to make concatenation non computable.

Another way to formulate this result is that the set C of functions computable with respect to an admissible indexing is a maximal computable set of functions. Indeed, let ϕ be a function that is not in C and i an indexing such that ϕ is computable relatively to i. Then, i is not admissible and the concatenation operation is not computable with respect to i. Thus, there exists a function of C that is not computable with respect to i and the set of functions computable with respect to i is not a proper superset of C.

In other words, changing the indexing can change the set of computable function, but it cannot extend it.

As a consequence, if we formulate the physical Church-Turing thesis as the fact that the set of functions realized by a machine is the set of computable functions, we obtain a thesis that depends on the way we interpret the physical parameters and the measured values. And this thesis can be invalidated by building a machine that computes the parity of a natural number and interpreting it as a machine deciding the halting problem, by cheating on the indexing.

But if we formulate this thesis as the fact that the set of functions realized by a machine is a strict superset of the set of computable functions for no indexing, then we have a thesis that is independent on the choice of an indexing.

Real numbers

The use of an indexing permits to transport the notion of computability to countable sets only. Computability over non countable sets is an unexplored world, except for one set: that of real numbers. As real numbers might be useful in physics, we have to say a few words about the computability of real functions.

To know a real number x is not to be able to answer the query "give me all the digits of x", but to be able to answer the query "give me the n th first digits of x" for all n, or equivalently to the query "give me a rational approximation of x with an error less than ε" for all ε [START_REF] Pour-El | Computability in Analysis and Physics[END_REF][START_REF] Weihrauch | Computable analysis: an introduction[END_REF].

To know a real function f is to be able to answer all the queries of the form "give me a rational approximation of f (x) with an error less than ε" provided we are answered all queries of the form "give me a rational approximation of x with an error less than η".

Thus a function f from R to R is computable if there exists a computable function F from Q × (Q + \ {0}) to Q × (Q + \ {0} ∪ {+∞}) such that for all x in R, q and r in Q, η and ε in Q + \ {0} (F (q, η) = (r, ε) and |x -q| ≤ η) ⇒ |f (x) -r| ≤ ε and if (q n ) n , (η n ) n ,
are sequences such that for all n, |x -q n | ≤ η n and the sequence η goes to 0 at infinity, then, calling (r n , ε n ) = F (q n , η n ), the sequence ε also goes to 0 at infinity.

Non-determinism

Computability theory is a theory of computable functions. However, when describing a machine we spoke, not about functions, but about relations. This is because several sequences of measured values b may correspond to the same sequence of parameters a. This non-determinism may have different sources, it may either come from the absolute non-determinism of nature, or because some variables are kept hidden: for instance, in the experiment above, if we choose the resistance R and measure the intensity I, then I does not depend functionally on R.

We know that a non deterministic algorithm from a set A to a set B may always be considered as a deterministic algorithm from the set A to the powerset P(B): a relation R may always be considered as a function mapping a to the set R a = {b ∈ B | a R b}. If we represent the set R a by an algorithm computing its partial characteristic function, then a relation R may be called computable when there exists an algorithm mapping a to an algorithm mapping b to 1 if and only if a R b. Using the fact that a function taking values in a functional space is equivalent to a function of several arguments, the relation R is represented by its own partial characteristic function. Thus, a relation is computable if and only if it is semi-decidable.

We could also represent the set R a by an enumeration function and this would lead to define computable relations as effectively enumerable relations. On natural numbers, and on any set on which equality is decidable, these two notions coincide. This is not the case on real numbers and only the second notion makes sense in this case [START_REF] Dowek | Non determinisitic computation over the real numbers[END_REF].

Gandy's proof

As previously noticed, some statements are too complex to be taken as axioms or principles and must rather be derived from more basic ones. This is probably the case with the physical Church-Turing thesis. And indeed Gandy [START_REF] Gandy | Church's thesis and principles for mechanisms[END_REF] has shown how to derive this thesis from three more basic hypotheses about nature.

Gandy's hypotheses

Gandy's hypotheses are the homogeneity of space and time, the boundedness of the velocity of propagation of information, the boundedness of the density of information.

The boundedness of the velocity of propagation of information can be expressed as the fact that the state of a system in one place can only affect the state of a system in another only after a delay, proportional to their distance. This principle has been part of the principles of physics, at least since special relativity.

The boundedness of the density of information can be expressed as the fact that a physical system of finite diameter has a finite state space. This principle is a more original idea. We may see it as an abstract formulation of the quantization idea: the fact that a variable cannot take any real number as a value, but only one of a discrete set. A similar principle has been stated more explicitly by Bekenstein [START_REF] Bekenstein | Universal upper bound to entropy-to-energy ratio for bounded systems[END_REF].

Gandy's proof

Then, to prove the physical Church-Turing thesis from these hypotheses, we just need to partition the space into an infinite number of identical cells of finite diameter. Because information has a bounded density, the state space of each cell is finite. Because space is homogeneous, this state space is the same for all cells. At the origin of time all the cells except a finite number are in a particular quiescent state. Like space, time can be discretized. Because the velocity of propagation of information is bounded and space and time are homogeneous, the state of a cell at a given time step is function of the state of a finite number of neighbors cells at the previous time step.

This function of a finite number of variables varying in a finite set is computable. Hence the state of each cell at each time step can be computed from the initial state.

In other words, using Gandy's hypotheses, a tiling of space and time allows to describe the evolution of any system as a cellular automata [START_REF] Wolfram | A new Kind of Science[END_REF]. Of course, the choice of the tiling should not affect the evolution of the system, as the tiling is not a property of the system itself, but of our description of the system.

Criticizing Gandy's hypotheses

Gandy's hypotheses can be, and have been [START_REF] Copeland | Physical Computation: How General are Gandys Principles for Mechanisms?[END_REF], criticized. For instance, it is well-known that, in Newtonian mechanics, gravity is instantaneous and thus information can be propagated with an infinite velocity. Also, the position of a body between two points A and B, the distance AB taken as a unit, can be any real number between 0 and 1 and thus can contain an infinite quantity of information: any infinite sequence in a finite alphabet can be encoded as the digits of such a number, in an appropriate base. Yet, these properties of Newtonian mechanics seem to be rather weaknesses of this theory than properties that would allow to communicate instantaneously or to store an infinite amount of information in a finite space: Gandy's hypotheses have not be refuted experimentally, for instance by the construction of an instantaneous computer network or by the construction of a hard drive with an unbounded capacity.

More importantly, even if Gandy's hypotheses must be refined, Gandy's proof shows that the physical Church-Turing thesis is a consequence of some hypotheses about nature, that do not refer to notions such that those of language or computability. [START_REF] Arrighi | Unitarity plus causality implies localizability. QIP 2010[END_REF] The physical Church-Turing thesis and the Galileo thesis

The Galileo thesis

The effectiveness of mathematics in natural sciences The thesis that mathematics are effective in the natural sciences has been formulated by Galileo in 1623: "Philosophy is written in this vast book, which continuously lies open before our eyes (I mean the Universe). But it cannot be understood unless you have first learned the language and recognize the characters in which it is written. It is written in the language of mathematics" [25]. Galileo formulated this thesis, but did not give any explanation why it held. And long after Galileo, the lack of such an explanation was noticed by Einstein according to whom "The eternal mystery of the world is its comprehensibility" [START_REF] Einstein | Physics and Reality[END_REF] or Wigner according to whom "The enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and that there is no rational explanation for it" [START_REF] Wigner | The unreasonable effectiveness of mathematics in the natural sciences[END_REF].

Insufficient explanations Several explanations of this unreasonable effectiveness of mathematics in the natural sciences have been attempted:

1. God is a mathematician and He wrote the vast book in the language of mathematics. 2. The mathematical concepts are built by abstracting from empirical objects. 3. Scientists select only those phenomena that can be mathematically described. 4. Scientists approximate the phenomena they study, until they can be mathematically described.

5. Our brain is part of nature, hence our concepts are natural objects, thus they are of the same kind as the objects they describe.

Each of these explanation is insufficient. The first reduces the problem to that of why God is a mathematician, which seems even harder to explain. The second is partial: if some mathematical concepts are built by abstracting from natural objects, the concept of ellipse, for instance, has not been built by abstracting from the trajectory of the planets, as it has been introduced some two thousands years before. The third leaves intact the problem of why so many -if not all -phenomena can be described in the language of mathematics. The fourth leaves intact the problem of why phenomena can be approximately -if not accurately -described in the language of mathematics. The fifth presupposes that we understand better a phenomenon from the inside than from the outside, which is not the case in general.

Perhaps several kinds of effectiveness

The effectiveness of mathematics in the natural sciences may be of different kinds. And instead of looking for a global explanation of all kinds of effectiveness, we should perhaps look for more local explanations.

For instance, the atomic masses of the chemical elements have a regular structure, as they are the integer multiples of some unit. When this regularity was discovered, there were three exceptions to this rule, because no elements of atomic mass 45, 68, and 70 were known. Yet, as some chemists trusted the structure of the natural numbers better that their observations, they predicted the existence of these three elements, that were later discovered. This is a striking example of the effectiveness of the structure of natural numbers in chemistry.

But, this striking regularity is easily explained by the fact that the mass of the atoms is mostly due to the mass of protons and neutrons that constitute their nucleus and that each nucleus contains a whole number of such particles.

Yet, this explanation sheds light on the effectiveness of the structure of natural numbers to describe the atomic masses of the chemical elements, but it does not shed light on the effectiveness of mathematics in the natural sciences in general, for instance, it does not shed light on the effectiveness of the quadratic functions to describe the free fall in vacuum.

Thus, we shall focus on a particular instance of the general thesis that mathematics are effective in the natural sciences: the fact that physically realized relations can be expressed by a proposition of the language of mathematics.

Physically realized relations Let us imagine an experiment where one prepares a physical system by choosing some parameters a = ⟨a 1 , ..., a n ⟩ and measures some values b = ⟨b 1 , ..., b p ⟩. Such an experiment defines a relation: the relation R such that a R b if b is a possible result for the measurements when the chosen parameters are a. We say that this relation R is realized by this experiment. A relation that is realized by an experiment is said to be physically realized.

For instance, if one applies an electrical tension U to a conductor of resistance R and measures the current I passing through this conductor, then a = ⟨U, R⟩ and b = I and the realized relation is that relating ⟨U, R⟩ and I when U = RI. In the same way, if one lets a body freely falling in vacuum for some time t and measures the distance crossed by this body, the realized relation is that relating t and x when x = 1 2 gt 2 . The relation between ⟨U, R⟩ and I can be expressed by a proposition in the language of mathematics U = RI. In the same way, the relation between the time and the position of a body freely falling in vacuum can be described by a proposition in the language of mathematics x = 1 2 gt 2 . Among the uncountable number of relations between numbers, only a countable number can be defined by a proposition in the language of mathematics, such as U = RI or x = 1 2 gt 2 and all the physically realized relations seem to be in this small set.

As Galileo stressed the rôle of the language of mathematics, we can call the Galileo thesis the thesis that all physically realized relation can be expressed by a proposition in the language of mathematics.

Instead of attempting to explain the general thesis that mathematics are effective in the natural sciences, we shall restrict our investigation to attempt to explain this unreasonable effectiveness of the propositions of the language of mathematics to express physically realized relations.

The physical Church-Turing thesis implies the Galileo thesis

Our definition of the notions of a machine and of an experiment are identical, both a machine and an experiment is a physical system prepared by choosing some parameters a = ⟨a 1 , ..., a n ⟩ and on which some values b = ⟨b 1 , ..., b p ⟩ are measured. Thus the notion of a relation realized by a machine and of a physically realized relation are identical.

The physical Church-Turing thesis states that physically realized relations are computable and the Galileo thesis states that they can be expressed by a proposition in the language of mathematics.

Once we have identified that the Galileo thesis and the physical Church-Turing thesis are theses about the same set of relations, we may remark that the physical Church-Turing thesis implies the Galileo thesis [START_REF] Dowek | The physical Church thesis as an explanation of the Galileo thesis[END_REF]. Indeed, as any program expressing a computable relation is a mathematical expression, all computable relations can be defined by a proposition in the language of mathematics. In fact, computable relations can even be expressed by a proposition in a very small fragment of mathematics: the language of Peano arithmetic. Thus, if the physical Church-Turing thesis holds, then all physically realized relations are computable, hence they can be expressed by a proposition of the language of mathematics, i.e. the Galileo thesis holds.

We have seen that -Gandy's hypotheses imply the physical Church-Turing thesis, and the physical Church-Turing thesis implies the Galileo thesis. Thus, we can deduce that Gandy's hypotheses imply the Galileo thesis and attempt to prove this directly.

Yet, from a historical point of view, it is important to notice the rôle of computability theory and of the physical Church-Turing thesis in connecting Gandy's hypotheses to the Galileo thesis.

An algorithmic description of the laws of nature

A side effect of this explanation of the Galileo thesis is that the laws of nature can be described not only in the language of mathematics, but also in an algorithmic language.

Instead of expressing the law of free fall in vacuum by the proposition x = 1 2 gt 2 , we could express it by the algorithm fun t -> g * t * t / 2, leading to a second Galilean revolution in the language of natural sciences. In particular, as long as differential equations have computable solutions [START_REF] Pour-El | Computability in Analysis and Physics[END_REF][START_REF] Bournez | A survey on continuous time computations[END_REF][START_REF] Collins | Effective computability of solutions of ordinary differential equations -The thousand monkeys approach[END_REF][START_REF] Collins | Effective computability of solutions of differential inclusions -The ten thousand monkeys approach[END_REF] the language of differential equations can be seen as an algorithmic language. Yet, this algorithmic description of the laws of nature may have a broader scope than the description of the laws of nature with differential equations. For instance, the transformation of a messenger RNA string to a protein is easily expressed by an algorithm, while it cannot be expressed by a differential equation.

A property of nature or of the theory?

An objection to Galileo's formulation of the Galileo thesis "The Universe [...] is [...] a book [...] written in the language of mathematics" is that it confuses nature with our description of nature: nature itself is neither a book written in the language of mathematics, nor a book written in another language: it is not a book at all. Only our description of nature is a book. Thus, we could imagine that our description of nature is written in the language of mathematics because we have chosen to write it this way, nature having nothing to do with our decision [START_REF] Ziegler | Physically-relativized Church-Turing hypotheses: Physical foundations of computing and complexity theory of computational physics[END_REF].

Yet, nature and our description of nature are not independent: our description must have an experimental adequation of some sort with nature. And as we shall see, when constructing a theory, the scientists have very little freedom when "choosing" the set of physically realized relations.

Let us consider first a particular case where all the realized relations are functional. Then, we show that if two theories differ on the set of realized relations, one of the theories can be, at least in principle, experimentally refuted. Indeed, if the set of the realized relations differ, then there exists a relation R that is realized according to one theory T but not according to the other theory T ′ . Let E be the experiment realizing R according to the theory T and R ′ be the relation realized by this experiment according to the theory T ′ . As R is not realized according to T ′ , the relations R and R ′ are different. Thus, there exists a, b, and b ′ , such that b ̸ = b ′ , a R b, and a R ′ b ′ . Then, if we perform the experiment E with the parameters a, the measures will either give the result b and refute T ′ , or b ′ and refute T, or an other value and refute both theories.

When the realized relations need not be functional, we have a weaker result: either a theory can be refuted, or it predicts, among others, a result that never occurs, whatever the number of times the experiment is repeated. Again, if the set of the realized relations differ, then there exists an experiment that realizes a relation R according to one theory and a relation R ′ , R ′ ̸ = R, according to the other. Thus, there exists an a, such that the set R a of the b such that a R b and the set R ′ a of the b such of b such that a R ′ b differ. As these sets are different, they are not both equal to R a ∩ R ′ a . Then, if we repeat the experiment with the parameters a, either the measures give one result that is not in R a ∩ R ′ a and at least one of the theories is refuted, or the measures always give results in R a ∩R ′ a and at least one theory predicts a result that never occurs. [START_REF] Arrighi | Unitarity plus causality implies localizability[END_REF] The physical Church-Turing thesis and the quantum theory

The bounded density of information in the quantum case

The hypothesis of a bounded density of information seems to be inspired by the idea of quantization of the state space, but is in contradiction with quantum theory. Indeed in quantum theory even a system with two distinct states u and v has an infinite number of states αu + βv, for |α| 2 + |β| 2 = 1. Thus, in quantum theory, this hypothesis cannot be formulated as the fact that the state space of a cell is finite. Yet, this does not mean that the amount of possible outcomes of a measurement of some value associated to this system, is itself infinite and the bounded density of information principle can be formulated as the fact that each such measurement may only yield a finite number of possible outcomes.

This requirement amounts to the fact that the state space of a region of space of finite diameter is a finite-dimensional vector space. This constitutes a good alternative to the fact that the amount of possible outcomes, when measuring the system, is finite, as this formulation does not involve the notion of a measurement.

In the classical case, the finiteness of the state space S is used to deduce that any function from S to S is computable. When S is a finite-dimensional vector space, it is not the case that all functions from S to S are computable, but it is the case that all linear maps are computable, as the application of a linear map to a vector boils down to matrix multiplication, i.e. to addition and multiplication of scalars. Fortunately, quantum evolutions are always linear maps, hence they are computable. In short, linearity tames infinities, when infinite sets are restricted to finite-dimensional vector spaces.

To define the state space of an non necessarily bounded region of space, we first decompose this region into a finite or infinite number of cells of finite diameter. The state space of each cell is a finite-dimensional vector space. Let e 1 , . . . , e n be a base of this set. The state space of the whole system is the tensor product of all these finite-dimensional spaces. Its vectors are linear combinations of tensor products of elements of e 1 , . . . , e n . As all the cells but a finite number of them are in a quiescent state, we can even restrict to finite tensor products.

We get this way a Fock-like space. This space is infinite-dimensional, hence it is not finitely generated with the operations + and ., but as it has a base formed with vectors that are tensor products of elements of e 1 , . . . , e n : it is finitely generated with the operations +, . and ⊗. In particular computability is stable on such a space [START_REF] Arrighi | On the completeness of quantum computation models[END_REF].

Thus, in the quantum case, the hypothesis of a finite density of information does not rule out infinite-dimensional vector spaces, but it explains where this infinity comes from: from the fact, that in an unbounded physical space, we can assemble an unbounded number of cells.

A difficult question is that of the impact of this hypothesis of a boundedness of information on the choice of the field of scalars we use. If we use the field C, then a scalar contains an infinite quantity of information, for instance any infinite sequence of 0 and 1 may be encoded as the digits of a scalar. Thus, the linear combination αu + βv, also contains an infinite quantity of information. Of course, this information cannot be retrieved in a single measurement, but it can, in principle, be probabilistically retrieved, by repeated measurements on similarly prepared systems.

On the opposite, we might consider that when superposing two base states αu + βv, only a finite number of linear combinations are possible.

A intermediate solution is to assume that the state space of each cell is a finite-dimensional vector space over a finite-degree extension of the field of rationals. Since we are in discrete-time discrete-space quantum theory, such a restriction as little consequences: we have all the scalars that can be generated by a universal set of quantum gates for instance [START_REF] Boykin | On universal and fault-tolerant quantum computing: A novel basis and a new constructive proof of universality for Shor's basis[END_REF], see also [START_REF] Arrighi | Operational semantics for formal tensorial calculus[END_REF] for a more in-depth discussion. Nevertheless, in the continuous picture, this kind of assumptions are not without consequences, and these are currently being investigated [START_REF] Connes | The Witt construction in characteristic one and quantization[END_REF][START_REF] Benioff | New gauge fields from extension of space time parallel transport of vector spaces to the underlying number systems[END_REF].

The bounded velocity of information in the quantum case

Like the hypothesis of a finite density of information, that of a finite velocity of propagation of information has to be defined with caution in the quantum case. For instance, according to some interpretations of the Einstein-Podolsky-Rosen paradox, it could be said to contradict quantum theory.

In the Einstein-Podolsky-Rosen paradox, however, no accessible information can be communicated faster than the speed of light [START_REF] Bell | On the Einstein Podolsky Rosen paradox[END_REF]. Similarly, it can be proved that not more than one bit of accessible information can be stored within a single qubit [START_REF] Holevo | Information-theoretical aspects of quantum measurement[END_REF]. Drawing this distinction between the description of the infinite, nonlocal quantum states and the information that can actually be accessed about them, hints towards the quantum version of these hypotheses.

In the classical case we could assume that the state of a compound system was simply given by the state of each component. In the quantum setting this no longer holds, some correlation information needs to be added. In other words, the state space of two regions is not the Cartesian product of the state space of each region, but its tensor product. Actually, if we stick to state vectors, knowing the state vector, e.g. (u ⊗ u) + (v ⊗ v), of the compound system, we cannot even assign a state vector to the first system. In order to do so, we need to switch to the density matrix formalism. Each state vector u is then replaced by the pure density matrix |u⟩u and if ρ is the density matrix of a compound system, then we can assign a density matrix to each subsystem, defined as a partial trace of ρ. The partial trace is defined by mapping A × B to A and extending linearly to A ⊗ B → A. Still, knowing the density matrix of each subsystem is again not sufficient to reconstruct the state of the compound system.

In this setting, the most natural way to formalize the bounded velocity of propagation of information hypothesis is that given in [START_REF] Arrighi | Quantum cellular automata over finite, unbounded configurations[END_REF] where it was referred to as Causality. Causality says that there exists a constant T such that for any region A, any point in time t, the density matrix associated to the region A at time t + T , ρ(A, t + T ) depends only on ρ(A ′ , t), with A ′ the region of radius 1 around A. Actually, this definition is a rephrase of the C * -algebra formulation found in [START_REF] Schumacher | Reversible quantum cellular automata[END_REF], which itself stems from quantum field theoretical approaches to enforcing causality [START_REF] Buchholz | Current trends in axiomatic quantum field theory[END_REF]. The difficulty of this axiomatic formalization of the bounded velocity of propagation of information in the quantum case, is that it is quite non-constructive: it is no longer the case that because we know that ρ(A, t + T ) is a local function f A of ρ(A ′ , t), and ρ(B, t + T ) is a local function f B of ρ(B ′ , t), that ρ(A ∪ B, t + T ) can be reconstructed from ρ(A ′ ∪ B ′ , t) by means of these two functions.

A more constructive approach to formalizing the bounded velocity of propagation of information in the quantum case would be to, instead, state that the global evolution is localizable [START_REF] Beckman | Causal and localizable quantum operations[END_REF][START_REF] Eggeling | Semicausal operations are semilocalizable[END_REF][START_REF] Schumacher | Locality and information transfer in quantum operations[END_REF][START_REF] Arrighi | Unitarity plus causality implies localizability. QIP 2010[END_REF], meaning that the global evolution is implementable by local mechanisms, each of them physically acceptable. Here this would say that the global evolution G is in fact quantum circuit of local gates with infinite width but finite depth. But the disadvantage of this approach is that this is a strong supposition to make. Fortunately, in [START_REF] Arrighi | Unitarity plus causality implies localizability. QIP 2010[END_REF][START_REF] Arrighi | Unitarity plus causality implies localizability[END_REF], the two approaches where shown to be equivalent. Hence we only need to assume causality and we can deduce locality.

With these two hypotheses formalized as explained, it is possible to extend Gandy's theorem to quantum theory [START_REF] Arrighi | The physical Church-Turing thesis and the principles of quantum theory[END_REF].

Conclusion

The physical Church-Turing thesis explains the Galileo thesis, but also suggests an evolution of the language used to describe nature.

It can be proved from more basic principle of physics, but it also questions these principles, putting the emphasis on the principle of a bounded density of information. This principle itself questions our formulation of quantum theory, in particular the choice of a field for the scalars and the origin of the infinite dimension of the vector spaces used as state spaces.

4

  This function is a non computable bijection from N to N. Moreover it is involutive, i.e. D -1 = D, D(0) = 0, and D(1) = 1.

  a 1 , a 2 , ..., a k of natural numbers has a canonical index

	where ; is the bijection between N 2 and N\{0} defined by (n; p) = (n+p)(n+p+
	1)/2 + p + 1. And a tree indexed by natural numbers p(t 1 , ..., t k ) has a canonical
	index
	⌜p(t 1 , ..., t k )⌝ = (p; ⌜t 1 ⌝; ...; ⌜t k ⌝; 0)
	⌜a 1 , a 2 , ..., a k ⌝ = (a 1 ; (a 2 ; (...; (a k ; 0))))

These tutorial notes owe a lot to Pablo Arrighi with whom most of this research has been done and to Maël Pégny with whom I gave a course on the Church-Turing thesis in the PUC Rio in

2011, on the invitation of Luiz Carlos Pereira. I also want to thank Olivier Bournez, José Félix Costa, Nachum Dershowitz, Jean-Baptiste Joinet, Giuseppe Longo, and Thierry Paul for many discussion on this thesis.


Gilles Dowek
email: gilles.dowek@inria.fr

Ying Jiang

On the Expressive Power of Schemes

We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike λ-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names are introduced for the hypotheses. We show that despite its non-determinism, some typed scheme-calculi have the same expressivity as the corresponding typed λ-calculi.

Introduction

We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs without introducing names for the hypotheses.

A scheme calculus

In the algorithmic interpretation of proofs, introduced by Brouwer, Heyting, and Kolmogorov, proofs are expressed by terms of a typed λ-calculus. In such a calculus, two kinds of variables are often used: those of the logic and those introduced to name the hypotheses. In System F , for instance, type variables and proof variables are often distinguished.

When variables are introduced to name the hypotheses, the two occurrences of the proposition A in the context of the sequent A, A ⊢ A must be distinguished, and thus the contexts must be multisets of propositions. In contrast, in automated theorem proving, in order to reduce the search space (e.g. to a finite space), the contexts of the sequents are often considered as sets of propositions [START_REF] Kleene | Introduction to Metamathematics[END_REF]. Thus, slightly different notions of sequents are used in proof-theory and in automated theorem proving. Moreover, these hypothesis names make the proofs of a given proposition a non-context-free language, even in the minimal propositional logic [START_REF] Zaionc | Probabilistic approach to the lambda definability for fourth order types[END_REF][START_REF] Joly | On lambda-definability I: the fixed model problem and generalizations of the matching problem[END_REF][START_REF] Dowek | Enumerating proofs of positive formulae[END_REF].

In this paper, we introduce a calculus, called the scheme-calculus, that permits to express proofs without introducing names for the hypotheses and where the contexts are just sets of hypotheses. In other words, we keep the variables of predicate logic, but do not introduce another category of variables for the hypotheses.

In the scheme-calculus, the proofs of a given proposition in minimal propositional logic and even in the positive fragment of minimal predicate logic form a context-free language. In fact, this scheme-calculus stems from previous works on the grammatical properties of sets of λ-terms [START_REF] Ben-Yelles | Type-assignment in the lambda-calculus; syntax and semantics[END_REF][START_REF] Zaionc | Mechanical procedure for proof construction via closed terms in typed lambda-calculus[END_REF][START_REF] Takahashi | Normal schemes and their grammar[END_REF][START_REF] Comon | Higher-order matching and tree automata[END_REF][START_REF] Broda | A context-free grammar representation for normal inhabitants of types in TA-lambda[END_REF][START_REF] Broda | On long normal inhabitants of a type[END_REF][START_REF] Dowek | Eigenvariables, bracketing and the decidability of positive minimal predicate logic[END_REF][START_REF] Dowek | Enumerating proofs of positive formulae[END_REF][START_REF] Salvati | Recognizability in the simply typed lambda-calculus[END_REF].

From the grammar generating the schemes of a given type, we can build an algorithm generating all the λ-terms of this type, as each scheme corresponds to a finite number of terms that can be computed from it [START_REF] Dowek | Enumerating proofs of positive formulae[END_REF]. A scheme containing n abstractions and p variables aggregate up to p n λ-terms. In this sense, more proofs are identified in the scheme-calculus than in the λ-calculus, but, unlike in the formalisms based on proof irrelevance, not all the proofs are identified, for instance the terms λx P λy P x and λx P λy P y are identified, but the terms λx P λf P ⇒P x and λx P λf P ⇒P (f x) are not.

Despite its simplicity, we show that this scheme-calculus is as expressive as the dependently-typed λ-calculus: for some type systems, all the functions that are provably total in impredicative (i.e. second-order) arithmetic can be expressed in the scheme-calculus. In this expressivity result, the determinism does not come from a local property, such as confluence, as for the λ-calculus, but from the subject-reduction property and the fact that dependent types are powerful enough to specify the value of terms.

The notion of variable

To understand the basic idea of the scheme-calculus, it is useful to go back to the origin of the notion of variable. A term expressing a function is usually built using a function-former, often written as λ, and a place-holder for the yet unknown argument of the function, sometimes written as P. For instance, the function mapping a number to its double can be expressed by the term λ(2 × P) Applying this term to 4 yields a term that reduces to 2 × 4.

But, when applying the term

λλ (2 × P × P × P)
that contains several occurrences of the symbol λ, to the arguments 4 and 5, for instance, we may get eight different syntactic results by replacing each occurrence of the symbol P either by 4 or by 5. Hence arises the need of a pointer associating a function-former occurrence λ to each place-holder occurrence P.

In the λ-calculus, this pointer is expressed by giving a name to each occurrence of a λ and to each occurrence of a P. The λ associated to a place-holder P x is then the first λ x above it in the term seen as a tree. This way, the function mapping two numbers to the double of the product of the square of the first and of the second is written as

λ x λ y (2 × P x × P x × P y )
or, in a simpler way, as

λxλy (2 × x × x × y)
Other solutions have been investigated. A solution related to Bourbaki's is to express the pointer with a directed edge from each P to the corresponding λ λλ 2 × × × While, in the solution proposed by de Bruijn, each P is assigned the height of its associated λ above it. So we get

λλ (2 × P 2 × P 2 × P 1 )
Applying these three terms to the terms 4 and 5 yields terms that reduce, in each formalism, to 2 × 4 × 4 × 5 only.

In many cases, both λs and Ps are typed and the pointers must relate objects of the same type. This identity of types guarantees the subject-reduction property: the reduction of a well-typed term yields a term of the same type. Knowing the type of each λ and P often reduces the possibilities of linking occurrences of the symbols P and λ in a raw term. For instance, in the raw term λ scal λ vect (2.P scal .P scal .P vect )

there is only one way to associate a λ to each P, but in the raw term

λ nat λ nat (2 × P nat × P nat × P nat )
there are still eight ways to associate a λ to each P.

In the scheme-calculus, instead of distinguishing eight terms λxλy (2×x×x× x), λxλy (2 × x × x × y), ..., we consider a single scheme λ nat λ nat (2 × ⟨nat⟩ × ⟨nat⟩ × ⟨nat⟩), where ⟨nat⟩ is the canonical (i.e. only) variable of type nat. In this scheme, each place-holder is possibly associated to any function-former above it, provided they have the same type. The scheme (λ nat λ nat (2 × ⟨nat⟩ × ⟨nat⟩ × ⟨nat⟩) 4 5) aggregates eight terms and reduces, in a non-deterministic way, to (2 × 4 × 4 × 4), (2 × 4 × 4 × 5), ... The reduction of schemes is therefore non-deterministic, but it does enjoy the subject-reduction property.

In general, the scheme ((λ A ...λ A ⟨A⟩) t 1 t 2 ... t n ) reduces, in a non-deterministic way, to each of the t i s. This is typical of non-deterministic extensions of λcalculus, such as G. Boudol's λ-calculus with multiplicities [START_REF] Boudol | The lambda-calculus with multiplicities[END_REF], where the term (λx x) (t 1 | ... | t n ) reduces also in a non-deterministic way to each of t i 's.

In the λ-calculus, when we apply the substitution (f y)/x to the term λy : B (g x y), we must rename the bound variable y in order to avoid the variable capture. As there is only one variable of type B in the scheme calculus, we are no longer able to rename the variables this way and the variable captures cannot be avoided.

The algorithmic interpretation of proofs

In the algorithmic interpretation of proofs, the subject-reduction property is more important than the uniqueness of results. For instance, consider the natural deduction proof ax

A, A ⊢ A ⇒i A ⊢ A ⇒ A ⇒i ⊢ A ⇒ A ⇒ A t ⊢ A ⇒e ⊢ A ⇒ A u ⊢ A ⇒e ⊢ A
where t and u are two cut free proofs of the sequent ⊢ A. This proof can be reduced, in a non-deterministic way, to t or to u, but in both cases, we get a cut free proof of ⊢ A.

When we associate a term of λ-calculus to this proof, we must associate a variable name to each hypothesis of the sequent A, A ⊢ A, and we must choose the variable used in the axiom rule. Different choices lead to different proofterms: ((λαλβ α) t u) and ((λαλβ β) t u), and each of these terms reduces to a unique normal form.

This example shows that, in some presentations of natural deduction with unnamed hypotheses, proof reduction is non-deterministic, and λ-calculus introduces determinism in a somewhat artificial way.

As shown by Statman and Leivant (see [START_REF] Troelstra | Basic Proof theory[END_REF][START_REF] Leivant | Assumption classes in natural deduction[END_REF]) the proof reduction process defined directly on natural deduction proofs with unnamed hypotheses is not strongly normalizing, while that of λ-calculus is. This non-termination can be seen as a consequence of the fact that variable captures are allowed. As, in general, termination is lost in the scheme-calculus, a strategy must be chosen.

Names and specifications

In the cross-fertilization of the theories of proof languages and of programming languages, the expression of natural deduction proofs in λ-calculus can be seen as the importation in proof theory of the concept of variable name, that is familiar in the theory of programming languages. On the opposite, the schemecalculus can be seen as an importation in the theory of programming languages of the concept of anonymous hypothesis, that is familiar in proof theory.

Yet, this idea of anonymous resource is not completely new in computer science. For instance, when we connect a computer to a local network, we just need to use any unnamed Ethernet cable. Its type "Ethernet cable" is sufficient to guarantee the connection to the network. In the same way, when a type system is strong enough to specify the value returned by a program, there is no need to give names to different programs of the same type: when such a program is needed, any program, that has the right type, goes. Identifying programs by their specification and not by their name may be a way to avoid the proliferation of variable names in programs and other formal objects.

The main calculus we shall introduce in this paper is a scheme-calculus with dependent types (Section 3), that permits to express proofs of various theories in minimal predicate logic. We shall prove three properties of this dependentlytyped scheme-calculus, that are subject-reduction (Section 4), normalization (Section 5), and an expressivity result (Section 6). As an introductory example, we start with a simply-typed scheme-calculus.

2 A simply-typed scheme-calculus

t = ⟨A⟩ | λ A t | (t t ′ )
The scheme ⟨A⟩ is the canonical variable of type A, λ A t is the scheme obtained by abstracting the canonical variable ⟨A⟩ of type A in t, and (t t ′ ) is the application of the scheme t to the scheme t ′ .

The typing rules are given in Figure 1. Notice that as contexts are sets, if A is an element of Γ, then Γ ∪ {A} is just Γ. For instance, using these rules, the scheme λ A λ A λ A ⟨A⟩ can be given the type A ⇒ A ⇒ A ⇒ A with the following derivation.

A ⊢ ⟨A⟩

: A A ⊢ λ A ⟨A⟩ : A ⇒ A A ⊢ λ A λ A ⟨A⟩ : A ⇒ A ⇒ A ⊢ λ A λ A λ A ⟨A⟩ : A ⇒ A ⇒ A ⇒ A Definition 2.4 (Scheme in context) A scheme in context is a pair t Γ where t is a scheme and Γ is a context such that t is well-typed in Γ.
We sometimes omit the context Γ when there is no ambiguity.

Reduction

When reducing the underlined redex in the scheme

λ A . . . λ A (λ A (λ A . . . λ A ⟨A⟩) u) A ∈ Γ Γ ⊢ ⟨A⟩ : A Γ ∪ {A} ⊢ t : B Γ ⊢ λ A t : A ⇒ B Γ ⊢ t : A ⇒ B Γ ⊢ u : A Γ ⊢ (t u) : B Figure 1: Simply-typed schemes
the variable ⟨A⟩ may be bound by the λ A of the redex, but it may also be bound by another λ A , either higher or lower in the scheme. So, in general, the scheme u may be substituted for the variable ⟨A⟩ or not, hence the non-determinism of the substitution. However, if the variable ⟨A⟩ is bound neither higher nor lower in the term, the only possible binder for ⟨A⟩ is that of the redex. In such a case, the variable ⟨A⟩ must be substituted. Thus, the fact that the scheme u may or must be substituted for the variable ⟨A⟩ depends not only on the reduced redex but also on the position of this redex in the scheme. Therefore, the reduction relation cannot be defined on schemes. Instead, it has to be defined on schemes in contexts.

To define the reduction relation, we must first set up a notion of substitution. A substitution is a function of finite domain, written as [t 1 /A 1 , ..., t n /A n ], associating schemes t 1 , ..., t n of types A 1 , ..., A n , respectively, to the variables ⟨A 1 ⟩, ..., ⟨A n ⟩. Applying a substitution to a scheme may produce several results, thus this application produces a set of results. Moreover, this application is always performed with respect to some context Γ that specifies the variables for which the substitution may or must be performed. More precisely, when A is in Γ, we may choose whether we substitute the canonical variable of type A or not and when A is not in Γ, this substitution is forced. If σ is a substitution, t is a scheme and Γ a context, we write σ Γ t for the result of the application of σ to t, with respect to the context Γ.

To simplify the notations, if S and S ′ are sets of schemes, we write λ A S for the set of schemes of the form λ A t for t in S and (S S ′ ) for the set of schemes of the form (t t ′ ) for t in S and t ′ in S ′ . Definition 2.5 (Substitution)

• σ Γ ⟨A⟩ = {⟨A⟩, σ(A)} if A ∈ dom(σ) and A ∈ Γ, • σ Γ ⟨A⟩ = {σ(A)} if A ∈ dom(σ) and A ̸ ∈ Γ, • σ Γ ⟨A⟩ = {⟨A⟩} if A ̸ ∈ dom(σ), • σ Γ (λ A t) = λ A σ (Γ∪{A}) t, • σ Γ (t u) = (σ Γ t σ Γ u).

Definition 2.6 (Reduction)

The one step top level β-reduction, written as -→, is defined by the rule

((λ A t) u) Γ -→ v Γ
where A, t, u, and Γ are arbitrary and v is any element of [u/A] Γ t.

The one step β-reduction relation £ is the contextual closure of the relation -→. It is inductively defined by

• if t Γ -→ t ′ Γ , then t Γ £ t ′ Γ , • if t Γ £ t ′ Γ , then (t u) Γ £ (t ′ u) Γ , • if u Γ £ u ′ Γ , then (t u) Γ £ (t u ′ ) Γ , • if t Γ∪{A} £ t ′ Γ∪{A} , then (λ A t) Γ £ (λ A t ′ ) Γ .
This β-reduction relation £ * is the reflexive-transitive closure of £.

The reduction relation is not confluent. Indeed, if A ̸ ∈ Γ, the scheme ((λ A λ A ⟨A⟩) t u) Γ reduces to both t Γ and u Γ , in a non-deterministic way. This formalizes the intuition that, in the scheme (λ A λ A ⟨A⟩) Γ , the variable ⟨A⟩ may be bound by either of the occurrences of the symbol λ A .

More surprisingly this reduction relation is not strongly normalizing.

Counter-examples to strong normalization

Proposition 2.1 (Statman [START_REF] Troelstra | Basic Proof theory[END_REF], Leivant [START_REF] Leivant | Assumption classes in natural deduction[END_REF]) The simply-typed scheme-calculus is not strongly normalizing.

Proof. Let t = ((λ A ⟨A⟩) ⟨A⟩) A . The scheme ((λ A t) t) A reduces to each of the elements of [t/A] A t, e.g. to ((λ A t) t) A .

This counter-example shows that, when we express natural deduction with sequents without naming the hypotheses, proof reduction is not strongly normalizing. For instance, the proof

ax A ⊢ A ⇒i A ⊢ A ⇒ A ax A ⊢ A ⇒e A ⊢ A ⇒i A ⊢ A ⇒ A ax A ⊢ A ⇒i A ⊢ A ⇒ A ax A ⊢ A ⇒e A ⊢ A ⇒e A ⊢ A contains a cut. If we eliminate this cut, we have to replace in the proof t ax A ⊢ A ⇒i A ⊢ A ⇒ A ax A ⊢ A ⇒e A ⊢ A
the axiom rules on the proposition A with the proof t itself. As A was already in the context, before being introduced by the ⇒i rule of the cut, we may choose to replace each axiom rule or not. If we replace both, we get back the proof we started with. This counter-example is based on the fact that the scheme-calculus permits the substitution of bound variables. Yet, even if we forbid this substitution of bound variables, the variable captures of the scheme-calculus are sufficient to jeopardize strong normalization. We give here another counter-example.

Example. Consider the context Γ = {A ⇒ B, B ⇒ A, A ⇒ B ⇒ A, A, B}, and the schemes in Γ, f = ⟨A ⇒ B⟩, g = ⟨B ⇒ A⟩, h = ⟨A ⇒ B ⇒ A⟩ a = ((λ B ⟨A⟩)(f ⟨A⟩)) b = ((λ A ⟨B⟩)(g ⟨B⟩)) u 0 = (h a b) u n+1 = (g (f u n )) v n = ((λ B u n ) (f u n ))
Remark that, for each i, the schemes a and b are subschemes of the scheme u i and that they do not occur in the scope of any binder.

The scheme

v n reduces to [(f u n )/B] Γ u n that contains a subscheme [(f u n )/B] Γ b, i.e. ((λ A (f u n ))(g (f u n ))) that, in turn, reduces to [(g (f u n ))/A] Γ (f u n ), that contains a subscheme [(g (f u n ))/A] Γ a, i.e. ((λ B (g (f u n )))(f (g (f u n )))
) that is v n+1 . Therefore v n reduces to a scheme that contains v n+1 as a subscheme.

Strategies

As with any non-deterministic system, we can restrict the reduction of the scheme-calculus by defining strategies. In the scheme-calculus, non-determinism arises from two different origins. First, as in the λ-calculus, when a scheme contains several redex occurrences, we may choose to reduce one or another first. Then, once the redex occurrence is chosen, we still have several ways to reduce it, because substitution itself is non-deterministic.

The simplest strategies are obtained by restricting the non-determinism of the substitution.

The definition of the substitution of the minimal strategy is the same as that of the general notion of substitution (Definition 2.5), except for the first clause: here we take the scheme ⟨A⟩ only, i.e.

• σ Γ ⟨A⟩ = {⟨A⟩}, if A ∈ dom(σ) and A ∈ Γ.
Notice that, in this case, σ Γ t is always a singleton. Its only element also is denoted by σ Γ t.

For instance, if A ̸ ∈ Γ, the scheme ((λ A λ A ⟨A⟩) t) Γ reduces to (λ A ⟨A⟩) Γ , and so does the scheme (λ A ((λ A ⟨A⟩) t)) Γ . But the scheme ((λ A ⟨A⟩) t) Γ reduces to t Γ .

The dual strategy is the maximal strategy. The definition of the substitution of this strategy is the same as that of the general notion of substitution except for the first clause: here we take the scheme σ(A) only, i.e.

• σ Γ ⟨A⟩ = {σ(A)}, if A ∈ dom(σ) and A ∈ Γ.
The scheme ((λ A λ A ⟨A⟩) t) Γ now reduces to (λ A t) Γ and so does the scheme

(λ A ((λ A ⟨A⟩) t)) Γ .
Intuitively, in the minimal strategy, we substitute a variable if we have to, while in the maximal strategy, we substitute a variable if we are able to.

A more complex strategy is the strategy with reference to the closest binder, also known as the total discharge strategy [START_REF] Takahashi | Normal schemes and their grammar[END_REF][START_REF] Troelstra | Basic Proof theory[END_REF]. In this strategy, the variable ⟨A⟩ always refers to the closest binder above it. The substitution is the same as that of the minimal strategy, but now the definition of the reduction is modified in such a way that ((

λ A t) u) Γ reduces to [u/A] ∅ t instead of [u/A] Γ t.
This way, the scheme ((λ A λ A ⟨A⟩) t) Γ reduces to (λ A ⟨A⟩) Γ , but the scheme

(λ A ((λ A ⟨A⟩) t)) Γ reduces to (λ A t) Γ .
The dual strategy is the strategy with reference to the furthest binder. The substitution is the same as that of the maximal strategy, but the definition of the reduction is modified in such a way that ((λ A t) u) Γ reduces to ([u/A] Γ t) Γ when A ̸ ∈ Γ and to t Γ when A ∈ Γ. This way, the scheme ((λ

A λ A ⟨A⟩) t) Γ reduces to (λ A t) Γ , but the scheme (λ A ((λ A ⟨A⟩) t)) Γ reduces to (λ A ⟨A⟩) Γ .
The counter-examples of Section 2.3 show that the maximal strategy and the strategy with reference to the closest binder do not normalize, even if we restrict to weak reduction, i.e. if we forbid reduction under abstractions. We leave open the problem of the normalization of the minimal strategy and the strategy with reference to the furthest binder. However, we shall prove in Section 5 the normalization of weak reduction for the minimal strategy.

Finally, λ-calculus is also a strategy of the scheme-calculus. There, in order to reduce the scheme ((λ A λ A ⟨A⟩) t) Γ , we need to know the history of the reduction, so that we are able to decide which binder the variable ⟨A⟩ refers to. In both schemes of type A ⇒ A ⇒ A in the context B:

((λ A⇒A λ A ⟨A ⇒ A⟩) (λ A ⟨A⟩)) and λ A ((λ B⇒A λ A (⟨B ⇒ A⟩⟨B⟩)) (λ B ⟨A⟩))
there is no ambiguity in the reference of the variable ⟨A⟩ that appears in the scope of a single binder of type A.

When we reduce these schemes, we get the normal scheme λ A λ A ⟨A⟩ in both cases. But to determine the reference of the variable ⟨A⟩ in this normal form, we have to know where this scheme is coming from. This is the role of variable names. Calling x the variable ⟨A⟩, y the variable ⟨B⟩, f the variable ⟨A ⇒ A⟩ and g the variable ⟨B ⇒ A⟩, the first term ((λf λx f ) (λx x)) reduces to λxλx x and the second λx ((λgλx (g y)) (λy x)) to λxλx ′ x, where a new name x ′ has been introduced by substitution to avoid the variable capture and keep the pointer from the occurrence of the variable x to its binder.

In this sense, the scheme-calculus generalizes both the lambda-calculus and the total discharge calculus.

A dependently-typed scheme-calculus

The simply-typed scheme-calculus is much less expressive than the simply-typed λ-calculus: with the general β-reduction the uniqueness of normal forms is lost and if we restrict the calculus to any deterministic strategy, as there is only one normal scheme of type A ⇒ A ⇒ A, it is impossible to express both projections.

In this section, we introduce a scheme-calculus with dependent types and prove that it is as expressive as the corresponding typed λ-calculus. In particular, we construct a dependent type system that permits to express all the functions that are provably total in impredicative arithmetic. This choice of impredicative arithmetic is just an example and we could construct similar type systems for various theories.

Terms and types

We first define terms and types (or propositions) as usual in many-sorted predicate logic.

We consider a language i.e. a set of sorts, a set of function symbols each of them being equipped with an arity of the form ⟨s 1 , . . . , s n , s⟩, where s 1 , . . . , s n , s are sorts, and a set of predicate symbols each of them being equipped with an arity ⟨s 1 , . . . , s n ⟩, where s 1 , . . . , s n are sorts. We consider also, for each sort, an infinite set of variables. The terms of sort s are inductively defined by

a = x | f (a 1 , . . . , a n )
where x is a variable of sort s, f a function symbol of arity ⟨s 1 , . . . , s n , s⟩ and a 1 , . . . , a n are terms of sorts s 1 , . . . , s n , respectively. The types are inductively defined by

A = P (a 1 , . . . , a n ) | A ⇒ A ′ | ∀x A
where P is a predicate symbol of arity ⟨s 1 , . . . , s n ⟩ and a 1 , . . . , a n are terms of sorts s 1 , . . . , s n , respectively. We could include other connectives and quantifiers and everything would generalize smoothly. However, we prefer to define them in the theory HA 2 presented in Section 3.2.

Free and bound variables, alphabetic equivalence, as well as substitution are defined as usual on terms and types.

A context is a finite set of types.

To define a theory, such as arithmetic, we do not consider axioms. Instead, we extend the natural deduction rules with a conversion rule allowing us to replace a proposition by an equivalent one for a given congruence, at any time in a proof, like in Deduction modulo [START_REF] Dowek | Theorem proving modulo[END_REF]. The congruence has to be non-confusing, that is, if A ≡ B then either at least one of the propositions A, B is atomic, or both are implications or both are universal quantifications, if

Γ ⊢ A A ≡ B conv Γ ⊢ B x 1 , . . . , x p ϵ p f ⟨x1,...,xp⟩,⟨y1,...,yn⟩,A (y 1 , . . . , y n ) -→ A x = y -→ ∀c (x ϵ 1 c ⇒ y ϵ 1 c) N (x) -→ ∀c (0 ϵ 1 c ⇒ ∀y (N (y) ⇒ y ϵ 1 c ⇒ S(y) ϵ 1 c) ⇒ x ϵ 1 c) Null (0) -→ ∀c (ϵ 0 (c) ⇒ ϵ 0 (c)) Null (S(x)) -→ ∀c ϵ 0 (c) Pred (0) -→ 0 Pred (S(x)) -→ x
(A ⇒ A ′ ) ≡ (B ⇒ B ′ ) then A ≡ B and A ′ ≡ B ′ , and if (∀x A) ≡ (∀x B) then A ≡ B.

Impredicative arithmetic

Following [START_REF] Dowek | Arithmetic as a theory modulo[END_REF], we can express predicative (i.e. first-order) and impredicative (i.e. second-order) arithmetic in Deduction modulo, hence the proofs of these theories can be expressed in the scheme-calculus.

We introduce a sort ι for natural numbers and a sort κ n (n = 0, 1, 2, ...) for n-ary classes of natural numbers. The function symbols are 0 (of sort ι), S and Pred (of arity ⟨ι, ι⟩). The predicate symbols are = of arity ⟨ι, ι⟩, N and Null of arity ⟨ι⟩ and ϵ n of arity ⟨ι, ..., ι, κ n ⟩. We write p ϵ 1 c to express that the number p is an element of the (unary) class c, and p 1 , ..., p n ϵ n c to express that the sequence p 1 , ..., p n is an element of the n-ary class c. Thus, ϵ 0 (c) is the proposition corresponding to the nullary class c. Moreover, for each proposition A, and sequences of variables ⟨x 1 , . . . , x p ⟩, ⟨y 1 , . . . , y n ⟩, such that the free variables of A are among x 1 , . . . , x p , y 1 , . . . , y n , we introduce a function symbol f ⟨x1,...,xp⟩,⟨y1,...,yn⟩,A which is, informally speaking, obtained by Skolemizing the instance of the comprehension scheme corresponding to A with x 1 , ..., x p as arguments of the class of arity p and y 1 , ..., y n as parameters. Such symbols exist for all propositions not containing Skolem symbols themselves, in particular for propositions containing quantifiers on classes (hence the impredicativity).

The meaning of these symbols is not expressed by axioms but by the rewrite rules in Figure 2. These rules define a congruence on terms and propositions.

As is well known, the connectives and quantifiers ⊤, ⊥, ¬, ∧, ∨, ⇔, and ∃ can be defined in HA 2 .

⊤ = ∀c (ϵ 0 (c) ⇒ ϵ 0 (c)) ⊥ = ∀c ϵ 0 (c) ¬A = A ⇒ ⊥ A ∧ B = ∀c ((A ⇒ B ⇒ ϵ 0 (c)) ⇒ ϵ 0 (c)) A ∨ B = ∀c ((A ⇒ ϵ 0 (c)) ⇒ (B ⇒ ϵ 0 (c)) ⇒ ϵ 0 (c)) A ⇔ B = (A ⇒ B) ∧ (B ⇒ A) ∃x A = ∀c ((∀x (A ⇒ ϵ 0 (c))) ⇒ ϵ 0 (c))
Using the congruence defined by the rules in Figure 2 and the conversion rule, the usual axioms of impredicative arithmetic, can easily be proven.

∀x (x = x) ∀x∀y∀c (x = y ⇒ x ϵ 1 c ⇒ y ϵ 1 c) N (0) ∀x (N (x) ⇒ N (S(x))) ∀x∀y (S(x) = S(y) ⇒ x = y) ∀x ¬(0 = S(x)) ∀c (0 ϵ 1 c ⇒ ∀y (N (y) ⇒ y ϵ 1 c ⇒ S(y) ϵ 1 c) ⇒ ∀x (N (x) ⇒ x ϵ 1 c) ∀y 1 ...∀y n ∃c∀x 1 ...∀x p ((x 1 ...x p ϵ p c) ⇔ A)
where A is any proposition not containing Skolem symbols, and whose free variables are among y 1 , ..., y n , x 1 , ..., x p .

Schemes

Definition 3.1 (Schemes) Schemes are inductively defined as follows.

t = ⟨A⟩ | λ A t | (t t ′ ) | Λx t | (t a)
Each construct corresponds to a natural deduction rule. Typing rules are given in Figure 3. They are the rules of natural deduction.

Definition 3.2 (Scheme in context)

A scheme in context is a pair t Γ where t is a scheme and Γ is a context such that t is well-typed in Γ.

We sometimes omit the context Γ when there is no ambiguity.

We now define the reduction relation on schemes. Before that, we define the application of a substitution of term variables and that of scheme variables to a scheme. Definition 3.3 Let θ be a substitution of term variables and t be a scheme. The scheme θt is inductively defined by

A ∈ Γ ax Γ ⊢ ⟨A⟩ : A Γ ∪ {A} ⊢ t : B ⇒i Γ ⊢ λ A t : A ⇒ B Γ ⊢ t : A ⇒ B Γ ⊢ u : A ⇒e Γ ⊢ (t u) : B Γ ⊢ t : A x ̸ ∈ F V (Γ) ∀i Γ ⊢ Λx t : ∀x A Γ ⊢ t : ∀x A ∀e Γ ⊢ (t a) : [a/x]A Γ ⊢ t : A A ≡ B conv Γ ⊢ t : B Figure 3: Dependently-typed schemes • θ⟨A⟩ = ⟨θA⟩, • θ(λ A t) = λ θA θt, • θ(u v) = (θu θv), • θ(Λx t) = Λx ′ (θ[x ′ /x]t)
, where x ′ is a variable which occurs neither in Λx t nor in θ,

• θ(t a) = (θt θa).

Remark that this substitution, as usual, avoids variable capture by renaming bound term variables.

A substitution of scheme variables is a function of finite domain associating schemes to types. The application of a substitution to a scheme with respect to a context is defined as follows.

Definition 3.4 (Substitution)

• σ Γ ⟨A⟩ = {⟨A⟩, σ(A)}, if A ∈ dom(σ) and A ∈ Γ, • σ Γ ⟨A⟩ = {σ(A)}, if A ∈ dom(σ) and A ̸ ∈ Γ, • σ Γ ⟨A⟩ = {⟨A⟩}, if A ̸ ∈ dom(σ), • σ Γ λ A t = λ A σ (Γ∪{A}) t, • σ Γ (u v) = (σ Γ u σ Γ v), • σ Γ Λx t = Λx ′ σ Γ [x ′ /x]t
, where x ′ is a variable that occurs neither in Λx t nor in σ,

• σ Γ (t a) = (σ Γ t a).

Definition 3.5 (Reduction)

The one step top level β-reduction is defined by the rules

• ((λ A t) u) Γ -→ v Γ , for all v ∈ [u/A] Γ t, • ((Λx t) a) Γ -→ ([a/x]t) Γ .
The one step β-reduction relation £ is the contextual closure of this relation and the β-reduction relation £ * is the reflexive-transitive closure of the relation £.

4 Subject-reduction Proposition 4.1 (Substitution)

• If Γ ⊢ t : B, then [a/x]Γ ⊢ [a/x]t : [a/x]B. • If Γ ∪ {A} ⊢ t : B and Γ ⊢ u : A, then Γ ⊢ v : B, for all v in [u/A] Γ t.
Proof. By induction over the structure of t.

Remark that this substitution lemma holds although bound variables may be substituted and variable capture is allowed. That is because the captured variables have the same type as the binder that captures them. 4. If t = Λx u, then there exists a variable x and a type B such that Γ ⊢ u : B and A ≡ (∀x B) and x ̸ ∈ F V (Γ).

If t = (u a)

, where u is a scheme and a a term, then there exists a type

B such that Γ ⊢ u : ∀x B and A ≡ [a/x]B.
Proof. By induction on the typing derivation. If the last rule is conversion, we apply the induction hypothesis and the transitivity of ≡. Otherwise the premises of the rule yield the result.

We are now ready to prove the subject-reduction property. Before that, we need to prove the proposition below. Proof. We show, by induction on the derivation of t Γ £ u Γ , that if Γ ⊢ t : A and t Γ £ u Γ then Γ ⊢ u : A and we conclude by induction on the length of reduction sequences.

Proposition 4.3 If Γ ⊢ t : A and t Γ -→ u Γ , then Γ ⊢ u : A. Proof. If t = ((λ B t 1 ) t 2 ) and u ∈ [t 2 /B] Γ t 1 ,

Weak normalization of weak reduction

We now prove that each scheme can be reduced to a normal form. Because of the counter-examples given in Section 2, we cannot expect to prove strong normalization for the reduction of the scheme-calculus. Of course, it is possible to prove weak normalization by mimicking the reductions of λ-calculus. But the scheme reduction strategy provided by the proof of the normalization theorem is as important as the theorem itself and the strategy provided by this trivial proof would require to introduce variable names, which is precisely what we want to avoid. Thus, we shall give another normalization proof which provides a strategy that can be defined without introducing variable names.

The first step towards a normalization result is to restrict substitution to minimal substitution, i.e. to modify the first clause of Definition 3.4: instead of taking the clause

• σ Γ ⟨A⟩ = {⟨A⟩, σ(A)}, if A ∈ dom(σ) and A ∈ Γ
we take the following one

• σ Γ ⟨A⟩ = {⟨A⟩}, if A ∈ dom(σ) and A ∈ Γ.
Restricting substitution to minimal substitution rules out the counter-examples of Section 2. Moreover, minimal substitution enjoys several properties of substitution of λ-calculus. In particular, bound variables are never substituted.

of type A in the context Γ, then ([v/A] Γ t) Γ reduces to ([v/A] Γ u) Γ . For in- stance, if Γ = {A ⇒ A, B ⇒ A, B}, t = ((λ A ⟨A⟩) (⟨A ⇒ A⟩ ⟨A⟩)), u = ⟨A⟩ and v = (⟨B ⇒ A⟩ ⟨B⟩), then t Γ∪{A} reduces to u Γ∪{A} . But ([v/A] Γ t) Γ = ((λ A ⟨A⟩) (⟨A ⇒ A⟩ (⟨B ⇒ A⟩ ⟨B⟩))) Γ reduces to (⟨A ⇒ A⟩ (⟨B ⇒ A⟩ ⟨B⟩))
and not to ([v/A] Γ u) Γ = (⟨B ⇒ A⟩ ⟨B⟩). This property is unfortunately needed in normalization proofs for strong reduction based on reducibility candidates. But, it is not needed, if we restrict to weak reduction.

On the other hand, the normalization of weak reduction is sufficient to prove the existence of weak head normal forms, which is itself sufficient to extract witnesses from existential proofs.

The proof presented in this section is based on ideas similar to those of [START_REF] Dowek | Proof normalization modulo[END_REF]. The main difference is that we take into account that reduction does not commute with substitution.

Reduction

The one step minimal top level reduction -→ min is defined as in Definition 3.5 except that substitution is minimal substitution. Instead of considering the contextual closure of this relation, we define the one step weak minimal reduction as follows.

Definition 5.1 (Weak minimal reduction) The one step weak minimal reduction ↠ is defined by considering any abstraction and any application whose left-hand side is normal, as a normal form, otherwise by reducing the leftmost reduct. It is inductively defined as follows.

Let t and u be schemes and a be a term,

• if t Γ -→ min u Γ then t Γ ↠ u Γ , • if t Γ ↠ t ′ Γ , then (t u) Γ ↠ (t ′ u) Γ , • if t Γ ↠ t ′ Γ , then (t a) Γ ↠ (t ′ a) Γ .
The weak minimal reduction relation ↠ * is the reflexive-transitive closure of the relation ↠.

Notice that the relation ↠ is functional (i.e. deterministic) in the sense that, for each scheme t, there is at most one scheme t ′ such that t ↠ t ′ .

The reduction sequence issued from t Γ is the (finite or infinite) sequence t 0,Γ , t 1,Γ , t 2,Γ , . . . such that t 0,Γ = t Γ , and for all i, if there exists a t ′ such that t i,Γ ↠ t ′ Γ , then the sequence is defined at i + 1 and t i+1,Γ = t ′ Γ , otherwise t i,Γ is the last element of the sequence. A scheme in context t Γ is said to be normalizing if its reduction sequence is finite. Hereafter, we write N for the set of normalizing schemes in contexts.

Proposition 5.1 (Properties of minimal substitution)

1. If t is well-typed in Γ, then [w/A] Γ t = t. 2. If A ∈ Γ, then [w/A] Γ t = t. 3. If B ̸ = A, then [w/A] Γ∪{B} t = [w/A] Γ t.
Proof.

1. By induction on the structure of t. The only non-trivial case is when t = ⟨B⟩. In this case, B ∈ Γ and both schemes are equal to ⟨B⟩. The denotation of propositions is defined by

• P (a 1 , . . . , a n ) ϕ = P ( a 1 ϕ , . . . , a n ϕ ), • A ⇒ B ϕ = A ϕ ⇒ B ϕ , • ∀x A ϕ = ∀ { A ϕ+x=e | e ∈ M s },
where s is the sort of the variable x and ϕ + x = e is the valuation coinciding with ϕ everywhere except in x where it takes the value e.

Definition 5.4 A congruence ≡ is said to be valid in a C-model M if for all types A and B, and every valuation ϕ, A ≡ B implies A ϕ = B ϕ .

Weak normalization of weak reduction

As variable captures are allowed in the scheme calculus, the substitutions cannot be composed as usual. For instance if Γ = {B ⇒ A, C ⇒ B, C}, f is the variable ⟨B ⇒ A⟩ and u is the term (⟨C ⇒ B⟩ ⟨C⟩), we have

[u/B] Γ [(f ⟨B⟩)/A] Γ∪{B} (λ B ⟨A⟩) = (λ B (f ⟨B⟩)) and [u/B] Γ [(f ⟨B⟩)/A] Γ∪{B} ⟨A⟩ = (f u)
but there is no substitution σ and context ∆ such that

σ ∆ (λ B ⟨A⟩) = (λ B (f ⟨B⟩)) and σ ∆ ⟨A⟩ = (f u)
because we cannot have at the same time σ ∆∪{B} ⟨A⟩ = (f ⟨B⟩) and σ ∆ ⟨A⟩ = (f u). Thus arises the need for the notion of free sequence of substitutions.

• ax. The scheme t is equal to ⟨A⟩. If A is not in the domain of any substitution of ρ or A ∈ Γ, then (ρt) Γ = ⟨ρA⟩ Γ . Thus, as the candidate A ϕ contains all normal neutral schemes, (ρt) Γ ∈ A ϕ . Otherwise, let [w/A] Γ be the rightmost substitution of ρ binding A. We have ρ

= ρ 2 , [w/A] Γ , ρ 1 and (([w/A] Γ , ρ 1 )⟨A⟩) Γ = ([w/ρ 1 A] Γ , ⟨ρ 1 A⟩) Γ = w Γ .
The sequence ρ is a free sequence of substitutions, the scheme w is well-typed in Γ, and it does not contain any term variable bound in ρ 2 , thus, using Proposition 5.1(1), (ρt) Γ = w Γ ∈ A ϕ .

• ⇒i. The scheme t has the form λ B u, A = (B ⇒ B ′ ) and (ρt) Γ = (ρ(λ B u)) Γ . Traversing the abstraction, the substitutions of ρ have their context extended to Γ ∪ {C} for some type C. Using Proposition 5.1(2), we drop those substitutions in ρ that bind the type C and using Proposition 5.1(3), we erase C from the context of the remaining ones. We get this way another free sequence of substitutions ρ ′ in Γ, ϕ and (ρt) Γ = (λ ρB (ρ ′ u)) Γ = (λ ρ ′ B (ρ ′ u)) Γ . This scheme is normal, hence it is normalizing and it only reduces to itself. To prove that it is in A ϕ = B ⇒ B ′ ϕ , we need to prove that for all schemes v in Γ such that v Γ ∈ B ϕ , the scheme ([v/ρ ′ B] Γ (ρ ′ u)) Γ = (([v/B] Γ , ρ ′ )u) Γ is in B ′ ϕ . This follows from induction hypothesis and the fact that ([v/B] Γ , ρ ′ ) is a free sequence of substitutions.

n, and a ′ is a term, then (u ′ a ′ ) Γ ∈ [a/x]B ϕ = B ϕ+x= a ϕ . As this scheme is neutral, all we need to prove is that its potential one-step reduct is in B ϕ+x= a ϕ . If the reduction takes place in u ′ , we just apply the induction hypothesis. Otherwise, the reduction takes place at top level. We have u ′ Γ = (Λx u ′′ ) Γ and the reduct is ([a ′ /x]u ′′ ) Γ which, by definition of ∀x B ϕ , is in B ϕ+x= a ϕ .

• conv. If the last rule is a conversion rule, by induction hypothesis, we have (ρt) Γ ∈ B ϕ for some B ≡ A, and we have B ϕ = A ϕ . Thus (ρt) Γ ∈ A ϕ .

Theorem 5.1 (Normalization) Let ≡ be a congruence that has a C-model M. Let Γ be a context and t a scheme of type A modulo ≡ in Γ. Then t Γ is normalizing.

Proof. By Proposition 5.3, for all ϕ, t Γ ∈ A ϕ , thus it is normalizing. To define N , we first define the function Φ that maps any function α of N → C to the function that maps n to the interpretation of the proposition ∀c (0 ϵ 1 c ⇒ ∀y (N (y) ⇒ y ϵ 1 c ⇒ S(y) ϵ 1 c) ⇒ x ϵ 1 c), for the valuation n/x, in the model of domains M ι and M κn , and where 0 and S are interpreted in the standard way, ϵ n is interpreted by εn , but N is interpreted by α. The set N → C ordered by pointwise inclusion is complete and the function Φ is monotonous, thus it has a fixed point β. We let N = β.

This way we can interpret every proposition A that does not contain Skolem symbols. Finally, we interpret the symbols f x1,...,xp,y1,...,yn,A as the functions mapping a 1 , . . . , a p to the function mapping b 1 , . . . , b n to A a1/x1,...,ap/xp,b1/y1,...,bn/yn .

Expressivity

We shall now see that, despite the non-determinism of the reduction, given in Definition 3.5, the uniqueness of results may be guaranteed for some schemes, and that every function that is provably total in HA 2 can be expressed by such a scheme.

If n is a natural number, we write n for the term S n (0). Proposition 6.1 (Parigot's numerals [START_REF] Parigot | Programming with proofs: A second order type theory[END_REF]) Let n be a natural number, then there exists a scheme ρ n of type N (n).

Figure 2 :

 2 Figure 2: The rewrite system HA 2

Proposition 4 . 2 (

 42 Inversion) Let Γ ⊢ t : A. 1. If t is some variable ⟨B⟩, then Γ contains the proposition B and A ≡ B, 2. If t = λ B u, then there exists a type C such that Γ ∪ {B} ⊢ u : C and A ≡ (B ⇒ C). 3. If t = (u v), where u and v are schemes, then there exist types B and C such that Γ ⊢ u : B ⇒ C and Γ ⊢ v : B, and A ≡ C .

  then by Proposition 4.2(3), there exist types B ′ and C ′ such that Γ ⊢ λ B t 1 : B ′ ⇒ C ′ , Γ ⊢ t 2 : B ′ and A ≡ C ′ and by Proposition 4.2(2), there exists a type C such that Γ ∪ {B} ⊢ t 1 : C and B ′ ⇒ C ′ ≡ B ⇒ C. As the congruence is non-confusing, we have B ≡ B ′ and C ≡ C ′ . Using the conversion rule, we have Γ ⊢ t 2 : B. By Proposition 4.1, we get Γ ⊢ u : C and using the conversion rule, Γ ⊢ u : A. If t = ((Λx t 1 ) a) and u = [a/x]t 1 , we choose x not occurring in Γ. Using Proposition 4.2, non-confusion and conversion, we get a type B ′ such that Γ ⊢ t 1 : B ′ and A ≡ [a/x]B ′ . We conclude with Proposition 4.1 and conversion.

Theorem 4 . 1 (

 41 Subject-reduction) If Γ ⊢ t : A and t Γ £ * u Γ , then Γ ⊢ u : A.

5. 5 2 Proposition 5 . 4

 5254 Normalization in HA All schemes well-typed in HA 2 are normalizing. Proof. We construct a C-model as follows. Let M ι = N and M κn = N n → C. The symbols 0, S, and Pred are interpreted in the standard way. The function εn maps k 1 , . . . , k n and f to f (k 1 , . . . , k n ), = maps n and m to ∀c (x ϵ 1 c ⇒ y ϵ 1 c) n/x,m/y and N ull maps 0 to ∀c (ϵ 0 (c) ⇒ ϵ 0 (c)) and the other numbers to ∀c ϵ 0 (c) .

  2. By induction on the structure of t. The only non-trivial case is when t = ⟨A⟩. In this case A ∈ Γ and thus both schemes are equal to ⟨A⟩. Proof. By definition, all the schemes in the sets E ⇒ F and ∀ S are normalizing. For closure by reduction, just remark that if t Γ ↠ * t ′ Γ and t Γ is normalizing, then so is t ′ Γ and that if t Γ ↠ * t ′ Γ and t ′ Γ ↠ * u Γ , then t ↠ * u Γ . For the third property, remark that if t Γ is a scheme in context and for all t ′ Γ such that t Γ ↠ t ′ Γ , t ′ Γ is normalizing then t Γ is normalizing and that if t Γ is a neutral scheme in context and t Γ ↠ * u Γ where u is an introduction, then the reduction sequence is not empty, thus there exists a scheme t ′ Γ such that t Γ ↠ t ′ Γ ↠ * u Γ . model valued in the algebra of reducibility candidates, or C-model, is defined as a classical model except that propositions are interpreted in the algebra C of reducibility candidates. Thus it consists of a set M s , for each sort s, a function f from M s1 ו • •×M sn to M s , for each function symbol f of arity ⟨s 1 , . . . , s n , s⟩, and a function P from M s1 × • • • × M sn to C, for each predicate symbol P of arity ⟨s 1 , . . . , s n ⟩. The denotation of terms in a valuation is defined as usual.

	5.3 C-models

A

† State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O. Box 8718, 100190 Beijing, China, jy@ios.ac.cn

Thus, we conjecture this minimal reduction to be strongly normalizing. However, we shall leave this problem open and prove a slightly weaker result: the normalization of weak reduction, i.e. of the reduction where reduction is not performed under abstractions. Indeed, the minimal reduction lacks one property of the reduction of λ-calculus: the commutation of reduction and substitution, i.e. that whenever t Γ∪{A} reduces to u Γ∪{A} and v is a scheme

By induction on the structure of t. The only non-trivial case is when t = ⟨A⟩. In this case, either A ∈ Γ in which case both schemes are equal to ⟨A⟩ or A ̸ ∈ Γ, in which case A ̸ ∈ (Γ ∪ {B}) and both schemes are equal to w.5.2 Girard's reducibility candidatesDefinition 5.2 (Operations on sets of schemes) If E and F are sets of schemes in contexts, we define the setE ⇒ F = {t Γ ∈ N | ∀t ′ ∀u ((t Γ ↠ * (λ A t ′ ) Γ and u Γ ∈ E) ⇒ ([u/A] Γ t ′ ) Γ ∈ F )} If S isa set of sets of schemes in contexts, we define the set∀ S = {t Γ ∈ N | ∀t ′ ∀a∀E ((t Γ ↠ * (Λx t ′ ) Γ and E ∈ S) ⇒ ([a/x]t ′ ) Γ ∈ E)} Definition 5.3 (Reducibility candidate[START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types[END_REF]) A scheme is said to be neutral if it corresponds to an axiom rule or an elimination rule, but not to an introduction rule. A set R of schemes in contexts is said to be a reducibility candidate, if the following conditions are satisfied:• if t Γ ∈ R, then t Γ is normalizing, • if t Γ ∈ R and t Γ ↠ * t ′ Γ , then t ′ Γ ∈ R, • if t Γ is neutral, and for every t ′ Γ such that t Γ ↠ t ′ Γ , we have t ′ Γ ∈ R, then t Γ ∈ R.We write C for the set of reducibility candidates.Remark that, as the reduction relation is deterministic, the third condition can be rephrased as:[START_REF] Kleene | Introduction to Metamathematics[END_REF] if t Γ is neutral and normal, then t Γ ∈ R, and (2) if t Γ is neutral, has a one-step reduct t ′ Γ and this reduct is in R, then t Γ is in R. Proposition 5.2 If E and F are sets of schemes in contexts, then E ⇒ F is a reducibility candidate. If S is a set of sets of schemes in contexts, then ∀ S is a reducibility candidate.

• ∀i. The scheme t has the form Λx u, we can assume, without loss of generality, that x does not occur in ρ. We have A = (∀x B) and ρt = Λx ρu. This scheme is normal, hence it is normalizing and it only reduces to itself. To prove that it is in A ϕ = ∀x B ϕ , we need to prove that for all terms a, and e in M s , where s is the sort of the variable x, the scheme ([a/x](ρu)) Γ = (([a/x], ρ)u) Γ is in B ϕ+x=e . As x does not occur in ρ, the sequence ([a/x], ρ) is a free sequence of substitutions for Γ, (ϕ+x = e). Thus, this scheme is in B ϕ+x=e by induction hypothesis.• ⇒e. The scheme t has the form (u v). Thus, ρt = (u ′ ρv), where u ′ = ρu. By induction hypothesis, u ′ Γ ∈ B ⇒ A ϕ and (ρv) Γ ∈ B ϕ . Thus, the scheme u ′ Γ is normalizing. Let n be the length of the reduction sequence starting from u ′ Γ . We prove, by induction on n that if u ′ Γ ∈ B ⇒ A ϕ and the length of the reduction sequence starting from u is n, andv ′ Γ ∈ B ϕ then (u ′ v ′ ) Γ ∈ A ϕ . As (u ′ v ′ ) Γ isneutral, all we need to prove is that its potential one-step reduct is in A ϕ . If the reduction takes place in u ′ , we just apply the induction hypothesis. Otherwise, the reduction takes place at top level. We haveu ′ Γ = (λ ρB u ′′ ) Γ and the reduct is ([v ′ /ρB] Γ u ′′ ) Γ which is in A ϕ by definition of B ⇒ A ϕ .• ∀e. The scheme t has the form (u a), where u has type ∀x B, A = [a/x]B, ρt = (u ′ ρa), where u ′ = ρu. By induction hypothesis, u ′ Γ ∈ ∀x B ϕ . Thus, the scheme u ′ Γ is normalizing. Let n be the length of the reduction sequence starting from this scheme. We prove, by induction on n that if u ′ Γ ∈ ∀x B ϕ , the length of the reduction sequence starting from u is

The authors want to thank the anonymous referees who helped them to improve the paper in many respects. This work is partially supported by NSFC 60673045, NSFC 60833001 and NSFC 60721061.

Definition 5.5 (Free sequence of substitutions) Let Γ be a context, and ϕ be a valuation, the free sequences of substitutions in Γ, ϕ are inductively defined as follows.

• The empty sequence is a free sequence of substitutions.

• If ρ is a free sequence of substitutions, C is a type, w is a scheme in the context Γ, such that w Γ ∈ C ϕ , then ([w/C] Γ , ρ) is a free sequence of substitutions.

• If ρ is a free sequence of substitutions, x is a term variable that does not occur in ρ, and a is a term, then ([a/x], ρ) is a free sequence of substitutions.

Definition 5.6 Let ρ be a free sequence of substitutions in Γ, ϕ and a be a term. The term ρa is defined as follows.

• If ρ is the empty sequence, then ρa = a,

Let A be a type, the type ρA is defined as follows.

• If ρ is the empty sequence, then ρA = A,

Let t be a scheme, the scheme ρt is defined as follows.

• If ρ is the empty sequence, then ρt = t,

In the proposition below, we prove, as usual, that if a scheme has type A then it is an element of the interpretation of A (hence we shall be able to deduce that it is normalizing). Proposition 5.3 Let ≡ be a congruence, M be a C-model of ≡, Γ and ∆ be contexts, ϕ be a valuation, t be a scheme of type A modulo ≡ in ∆, and ρ be a free sequence of substitutions in Γ, ϕ such that ρt is a scheme well-typed in Γ.

Proof. By induction on the typing derivation of t. From the witness property we get the expressibility of all functions that are provable in HA 2 . We need first to use the following result of elementary logic. Proposition 6.3 For every computable function f from N n to N, there exists a proposition A such that [p 1 /x 1 , . . . , p n /x n , q/y]A is provable in HA 2 if and only if q = f (p 1 , . . . , p n ). Definition 6.1 (Provably total function) The function f is said to be provably total in HA 2 if

is provable in HA 2 . Theorem 6.1 For every computable function f provably total in HA 2 , there exists a scheme t such that for all p 1 , ..., p n , the normal form of the witness extracted from the scheme (t p 1 ρ p1 p 2 ρ p2 . . . p n ρ pn ) is f (p 1 , ..., p n ).

Proof. Take any scheme of type ∀x 1 (N (x 1 ) ⇒ . . . ⇒ ∀x n (N (x n ) ⇒ ∃y (N (y) ∧ A)) . . .).

Whether the set of functions provably total in HA 2 is equal or a strict subset of the set of functions that can be expressed in the scheme calculus, is left as an open problem.

Future Work

Besides HA 2 , Theorem 5.1 applies to many theories e.g. simple type theory and some variants of set theory. When they cannot be defined in the theory, all connectives and quantifiers must be taken as primitive, like in [START_REF] Dowek | Proof normalization modulo[END_REF]. Although tedious, the normalization proof generalizes smoothly.

A more challenging problem is to prove normalization for other reduction strategies than weak minimal reduction. This probably requires to generalize proofs by reducibility to cases where reduction and substitution do not commute.

22