Kevin Knight

A Small Collatz Rule without the Plus One

Keywords:

teaching and research institutions in France or abroad, or from public or private research centers.

Introduction

The famous Collatz rule has two frequently-used variations.

C(n) =

n/2, if n is even; 3n + 1, if n is odd.

T (n) = n/2, if n is even; (3n + 1)/2, if n is odd.

Iterating these rules yields interesting sequences, for example:

C(n) : 7 → 11 → 34 → 17 → 52 → 26 → 13 → 40 → 20 → 10 → 5 → 16 → 8 → 4 → 2 → 1 → 4 → 2 → 1 . . . T (n) : 7 → 11 → 17 → 26 → 13 → 20 → 10 → 5 → 8 → 4 → 2 → 1 → 2 → 1 . . .
The Collatz conjecture posits that every positive integer eventually reaches 1 under either rule. The conjecture has been verified for all 1 ≤ n ≤ 10 20 [START_REF] Barina | Convergence verification of the Collatz problem[END_REF] but has not yet been proven or refuted.

Main Result

The following rule K(n) simulates the Collatz C(n) rule. We present it in the spirit of other simple devices that compute Collatz trajectories, such as de Mol's tag system (de Mol, 2008), Korec's cellular automaton [START_REF] Korec | The 3x + 1 problem, generalized Pascal triangles, and cellular automata[END_REF], and Yolcu's rewrite system [START_REF] Yolcu | An automated approach to the Collatz conjecture[END_REF]. 4, 6, 12, 16, 18 or 24 (mod 30).

K(n) =                (375/2)n
Like rules by [START_REF] Conway | Unpredictable iterations[END_REF] and [START_REF] Monks | 3x + 1 minus the +[END_REF], K(n) simplifies Collatz trajectories by eliminating the "+1," which is a source of difficulties for analyzing Collatz dynamics. K(n) works on trajectory terms coded as powers of two. Here, it simulates the C(n) trajectory 3 → 10:

2 3 = 8 → 1500 → 93750 → 5859375 → 9765625 → 3906250 → 1562500 → 625000 → 250000 → 100000 → 40000 → 16000 → 6400 → 2560 → 2 10 = 1024
3 Background [START_REF] Conway | Unpredictable iterations[END_REF] situated the Collatz rule within a class of generalized Collatz rules that take the form

G(n) =          (a 0 n + b 0 )/d, if n ≡ 0 (mod d); (a 1 n + b 1 )/d, if n ≡ 1 (mod d); . . . (a d-1 n + b d-1 )/d, if n ≡ d -1 (mod d).
When d = 2, a 0 = 1, b 0 = 0, a 1 = 3, and b 1 = 1, G(n) implements the Collatz rule T (n). Conway also constructed a generalized Collatz rule that can mimic the computation of a universal Turing machine. The strong computational power of certain generalized rules may explain why the Collatz conjecture is so difficult to resolve.

Conway's universal rule did not require the "+b," being of the simpler form

G ′ (n) =          (a 0 n)/d, if n ≡ 0 (mod d); (a 1 n)/d, if n ≡ 1 (mod d); . . . (a d-1 n)/d, if n ≡ d -1 (mod d).
Monks ( 2002) constructed an ingenious generalized Collatz rule-also without "+b"-that simulates the Collatz rule itself. Monks proposed to study the Collatz dynamics in this simpler setting.

Both Conway and Monks presented their generalized Collatz rules in a more compact rule format called Fractran [START_REF] Conway | Fractran: A simple universal programming language for arithmetic[END_REF] To simulate the Collatz rule, each number in a Collatz T (n) trajectory (e.g., 7 → 11) is coded as a power of 2 (e.g., 2 7 → . . . → 2 11 ). Monks' Fractran rule is then applied to numbers of this form; other prime factors serve as registers for intermediate computations.

2 7 → 2 5 3 1 11 1 → 2 5 3 1 → 2 3 3 2 11 1 → 2 3 3 2 → 2 1 3 3 11 1 → 2 1 3 3 → 3 3 5 1 → 2 3 3 2 17 1 → 2 3 3 2 5 1 → 2 6 3 1 17 1 → 2 6 3 1 5 1 → 2 9 17 1 → 2 9 5 1 → 2 11 → 2 9 3 1 11 1 → 2 9 3 1 → . . . → 2 17 → . . . → 2 26 → . . . → 2 1 .
The Collatz conjecture is equivalent to the proposition that every integer 2 m (m ∈ N) eventually reaches 2 1 under Monks' rule.

The "if-then-otherwise" action of any Fractran rule can be expanded into a generalized Collatz rule. Monks sets d = lcm (11,15,17,5,21,13,7,4, 2) = 1021020 which implies conditions like

M (n) =          92820n/1021020,
if n ≡ 0 (mod 1021020); 7147140n/1021020, if n ≡ 1 (mod 1021020);

. . . 7147140n/1021020, if n ≡ 1021019 (mod 1021020).

Simplifying reveals the correspondence with Monks' Fractran rule:

M ′ (n) =         
(1/11)n, if n ≡ 0 (mod 1021020); (7/1)n, if n ≡ 1 (mod 1021020);

. . . (7/1)n, if n ≡ 1021019 (mod 1021020).

Simulating Collatz Trajectories

The new rule K(n) from Section 2 is much smaller, with only 30 conditions. This section explains its action.

Theorem 4.1. The rule K(n) simulates the Collatz rule C(n).

Proof: The logic of K(n) is straightforward. K(n) uses three registers (2, 3, 5) to keep track of the computational state. To simulate C(n) on start term 1, K(n) uses 6 steps.

2 1 375 2 -----→ 3 1 5 3 5 3 ---→ 5 4 2 5 ---→ 2 1 5 3 2 5 ---→ 2 2 5 2 2 5 ---→ 2 3 5 1 2 5 ---→ 2 4
To simulate C(n) on any odd term 2m + 1 (m ≥ 1), K(n) uses 8m + 6 steps. It starts by repeatedly decrementing the exponent of 2 by one while incrementing the exponent of 5 by three:

2 2m+1 → 2 2m+1-1 3 1 5 3 1 step of (375/2) → 2 2m+1-2 3 1 5 6 → . . . → 3 1 5 6m+3 2m steps of (125/2) → 5 6m+4 1 step of (5/3) → 2 1 5 6m+4-1 → 2 2 5 6m+4-2 → . . . → 2 6m+4 6m + 4 steps of (2/5)
Finally, K(n) uses 3m steps to simulate C(n) on any even term 2m (m ≥ 1). It begins by decrementing the exponent of 2 by two while incrementing the exponent of 3 by one.

2 2m → 2 2m-2 3 1 → 2 2m-4 3 2 → . . . → 3 m m steps of (3/4) → 3 m-1 5 1 → 3 m-2 5 2 → . . . → 5 m m steps of (5/3) → 5 m-1 2 1 → 5 m-2 2 2 → . . . → 2 m m steps of (2/5)
Here, K(n) uses 5 m as a stopover, instead of transiting directly from 3 m to 2 m -under the latter approach, upon encountering 2 a 3 b , K(n) would not know whether to decrement the exponent of 2 or increment it. Also, it is fortuitous that the (5/3) condition can be reused for different purposes. When processing odd terms, it puts the +1 in 3n + 1; for even terms, it transits from 3 m to 5 m . Now we must show that the K(n) classes modulo 30 encode the correct computational state. From the above trajectories, we see eight expressions that must be distinguished from one another: 2 2a+1 , 2 a 3 b 5 c , 3 b , 2 a 3 b , 2 a 5 c , 2 2a , 3 b 5 c , and 5 c . Using tables for 2 n , 3 n , and 5 n mod 30, we calculate possible classes (modulo 30) for these expressions.

2 2a+1 2, 8
2 a 3 b 5 c 0 3 b 3, 9, 21, 27 2 a 3 b 6, 12, 18, 24 2 a 5 c 10, 20 2 2a 4, 16 3 b 5 c 15 5 c 5, 25

Because the classes are distinct, K(n) can specify the correct action to take in each case.

Matthews-Watts Conjecture

The Matthews-Watts conjecture [START_REF] Matthews | Generalized 3x+1 mappings: Markov chains and ergodic theory[END_REF] provides another reason to study rules without "+b," beyond their simplicity. A generalized Collatz rule is defined as

contracting if a 0 a 1 • • • a d-1 < d d , and expanding if a 0 a 1 • • • a d-1 > d d .
The conjecture states that under a contracting rule, all start integers reach one of a finite number of cycles. Since the rule T (n) is contracting, the Matthews-Watts conjecture suggests that no start numbers diverge to infinity under the Collatz dynamics.

We follow Monks by investigating the possible combinations of fractions used in a cycle. Suppose (375/2) a (125/2) b (5/3) c (2/5) d (3/4) e = 1. Then 2 d-a-b-2e 3 a+e-c 5 3a+3b+c-d = 1, which means

d -a -b -2e = 0 a + e -c = 0 3a + 3b + c -d = 0.
This system of equations is solved by

b = e/2 -3a/2 (1) c = a + e d = 5e/2 -a/2.
By inspecting the action of K(n), we can assign interpretations to the variables. For example, K(n) processes an even number n by applying (3/4) some n/2 times. Therefore, e is half the sum of all even numbers in a Collatz cycle. This implies that the length of every K(n) cycle is a multiple of 5. Also, because e = a+b+c+d+e 5 , the (3/4) branch of K(n) is taken 20% of the time during any cycle, neither more nor less than its "fair share."

By further inspecting K(n), we note that a counts the number of odd terms in the cycle, while b is the sum of odd terms minus the count of odd terms. Letting m 1 • • • m k be the terms of any Collatz cycle, we rewrite Equation 1

(2m i + 1) = 1 2 even mi m i .
This is a well-known property of C(n) cycles. For the trivial 1-2-4-1 cycle, we have 2(1)+1 = 1 2 (2+4).

  Theorem 6.1. The rule K(n) takes 5 2 m steps to simulate a C(n) cycle, where m is the sum of even terms in the cycle. Proof: Because e is half the sum of the even numbers in the cycle, m = 2e. a + b + c + d + e = a + (e/2 -3a/2) + (a + e) + (5e/2a/2) + e

  , if n ≡ 2 or 8 (mod 30);

	(125/2)n, if n ≡ 0 (mod 30);
	(5/3)n,	if n ≡ 3, 9, 15, 21 or 27 (mod 30);
	(2/5)n,	if n ≡ 5, 10, 20 or 25 (mod 30);
	(3/4)n,	if n ≡

  . Monks' rule is The rule is interpreted as follows: if n is divisible by 11, replace n by (1/11)n; otherwise, if n is divisible by 15, replace n by (136/15)n, and so on.

	(	1 11 ,	136 15 ,	5 17	,	4 5	,	26 21 ,	7 13 ,	1 7 ,	33 4 ,	5 2 ,	7 1	).

The intuition behind the Matthews-Watts conjecture is that if each branch of a contracting rule is taken with equal frequency, then trajectories will trend downward. Surprisingly, the conjecture does not refer at all to a rule's "+b" parameters, which are presumed irrelevant to the ultimate fate of start numbers.

The 30-condition rule K(n) is not a true generalized Collatz rule, because (3/4)n in the fifth condition cannot be rewritten as (a 4 n + b 4 )/30. A 60-condition variation suffices: 60,if n ≡ 2,8,32,38 (mod 60) 4, 6, 12, 16, 18, 24, 34, 36, 42, 46, 48, 54 (mod 60).

Is K ′ (n) a contracting rule, according to the Matthews-Watts conjecture? This question turns out to be inapplicable, because the conjecture only applies when a 0 a 1 • • • a d-1 is co-prime with d, which is not the case with K ′ (n).

Ignoring the co-prime requirement allows us to engineer rules whose conditions are invoked with unequal frequencies. For example, the trajectories of K ′ (n) contain very few numbers of the form n ≡ 2 (mod 30) compared to numbers of the form n ≡ 15 (mod 30), and possibly no numbers of the form n ≡ 1 (mod 30), depending on how the unspecified conditions are handled. [START_REF] Conway | Fractran: A simple universal programming language for arithmetic[END_REF] exploits this unequal-frequency capability to create powerful rules with arbitrary looping and testing. Of course, not all such rules yield Turing-equivalent power. Even the simple C(n) generates more even terms than odd terms and is thus not subject to the Matthews-Watts conjecture; 3n + 1 = (6n + 2)/2 and gcd(6, 2) > 1. Of course, C(n) could still turn out to have Turing power, in which case the Collatz conjecture and the Matthews-Watts conjecture would both be false.

Cycles

The trivial Collatz cycle 1-2-4-1 has a trajectory of length 15 under the K(n) rule: 2 1 = 2 → 375 →


Gilles Dowek
email: gilles.dowek@polytechnique.edu

Specifying programs with propositions and with congruences

Introduction

Deduction modulo is an extension of first-order predicate logic where axioms are replaced by a congruence, modulo which deduction is performed. Like first-order predicate logic, Deduction modulo is a framework where many theories can be expressed, in particular predicative arithmetic [START_REF] Dowek | Arithmetic as a theory modulo[END_REF] and impredicative arithmetic, usually called first-order and second-order arithmetic (terminology that we try to avoid as both theories are expressed in a first-order setting).

Krivine and Parigot's Second-order functional arithmetic (FA 2 ) [START_REF] Leivant | Reasoning about functional programs and complexity classes associated with type disciplines[END_REF][START_REF] Krivine | Programming with proofs[END_REF][START_REF] Krivine | Lambda-calculus, types and models[END_REF] is a formulation of impredicative arithmetic tailored to be used to specify and prove programs. In this note, we give a presentation of FA 2 in Deduction modulo. Expressing FA 2 in Deduction modulo will shed light on an original aspect of the FA 2 approach: the fact that programs are specified, not with propositions, but with congruences.

Deduction modulo

Identifying propositions

In Deduction modulo, a theory is a congruence ≡ on terms and propositions, often defined with rewrite rules and equational axioms. If R is a set of rewrite rules and equational axioms, the congruence ≡ R defined by the rewrite system R is inductively defined as follows if l -→ r is a rewrite rule or ∀x 1 ...∀x n (l = r) (where all the free variables of l and r are among x 1 , ..., x n ) is an equational axiom of R and σ is a substitution, then σl ≡ R σr, the relation ≡ R is reflexive, symmetric and transitive, the relation ≡ is compatible with the structure of terms and propositions, i.e.

if f is a function symbol and t 1 ≡ R u 1 , ..., t n ≡ R u n , then f (t 1 , ..., t n ) ≡ R f (u 1 , ..., u n ), and similarly for predicate symbols, connectors and quantifiers. For instance, if the congruence ≡ is defined with the rules 0 + y -→ y S(x) + y -→ S(x + y) 0 × y -→ 0 S(x) × y -→ x × y + y x = x -→ ⊤ we have (2 + 2 = 4) ≡ ⊤ and we can prove, in natural deduction modulo ≡, that the number 4 is even

⊤-intro ⊢ 2 × 2 = 4 ⟨x, 2 × x = 4, 2⟩ ∃-intro ⊢ ∃x 2 × x = 4

Proof-terms

We sometime write natural deduction proofs modulo as proof-terms.

Definition 1 (Proof-term). Proof-terms are inductively defined as follows.

π = α | I | δ ⊥ (π) | ⟨π 1 , π 2 ⟩ | fst(π) | snd (π) | i(π) | j(π) | δ(π 1 , απ 2 , βπ 3 ) | λα π | (π 1 π 2 ) | λx π | (π t) | ⟨t, π⟩ | δ ∃ (π 1 , xαπ 2 )
Each proof-term construction corresponds to an intuitionistic natural deduction rule: terms of the form α express proofs built with the axiom rule, the term I expresses the proof built with the introduction rule of the symbol ⊤, terms of the form δ ⊥ (π) express proofs built with the elimination rule of the symbol ⊥, terms of the form ⟨π 1 , π 2 ⟩ and fst(π), snd (π) express proofs built with the introduction and elimination rules of the conjunction, terms of the form i(π), j(π) and δ(π 1 , απ 2 , βπ 3 ) express proofs built with the introduction and elimination rules of the disjunction, terms of the form λα π and (π 1 π 2 ) express proofs built with the introduction and elimination rules of the implication, terms of the form λx π and (π t) express proofs built with the introduction and elimination rules of the universal quantifier and terms of the form ⟨t, π⟩ and δ ∃ (π 1 , xαπ 2 ) express proofs built with the introduction and elimination rules of the existential quantifier.

Definition 2 (Reduction). Reduction on proofs is defined by the following rules that eliminate cuts step by step.

fst(⟨π 1 , π 2 ⟩) ▷ π 1 snd (⟨π 1 , π 2 ⟩) ▷ π 2 δ(i(π 1 ), απ 2 , βπ 3 ) ▷ (π 1 /α)π 2 δ(j(π 1 ), απ 2 , βπ 3 ) ▷ (π 1 /β)π 3 (λα π 1 π 2 ) ▷ (π 2 /α)π 1 (λx π t) ▷ (t/x)π δ ∃ (⟨t, π 1 ⟩, αxπ 2 ) ▷ (t/x, π 1 /α)π 2
We write ▷ * for the reflexive-transitive closure of the relation ▷.

A proof is said to be strongly normalizing if its reduction tree for the relation ▷ is finite. We write SN for the set of strongly normaling proofs.

FA 2 in Deduction modulo

Classes in first-order predicate logic and in Deduction modulo

The induction principle can be expressed as the fact that a class of natural numbers that contains 0 and that is closed by the successor function contains all the natural numbers. A class of numbers is just a collection of numbers definable in comprehension by a proposition of arithmetic.

To formalize the induction principle, one possibility is to leave the notion of class implicit and formalize this principle as an axiom scheme, with one axiom for each proposition defining a class in comprehension. Another possibility is to introduce a sort κ for classes and a binary predicate symbol ϵ for the membership of a natural number to a class.

This way, we obtain a two-sorted theory with a sort ι for natural numbers and a sort κ for classes and we can formulate the induction axiom as the proposition

∀X (0 ϵ X ⇒ ∀y (N (y) ⇒ y ϵ X ⇒ S(y) ϵ X) ⇒ ∀n (N (n) ⇒ n ϵ X))
To be able define classes in comprehension, for instance to define the class of the elements x such that ∃w (x = 2 × w), we need an axiom expressing the existence of this class. Thus, for each proposition A, we need an axiom expressing that there exists a class Z such that x ϵ Z if and only if A

∀y 1 . . . ∀y p ∃Z∀x (x ϵ Z ⇔ A)
where the free variables of A are among x, y 1 , . . . , y p .

In this comprehension scheme, we must be precise about the propositions A that define instances of the scheme. If we want to have equivalence with the "usual" formulation of predicative arithmetic, A must be a proposition in the language we had before adding the sort κ and the predicate symbol ϵ. In particular, A must not contain quantifiers over variables of sort κ.

Skolemizing each of these axioms, introduces an infinite number of Skolem symbols f x,y1,...,yp,A and the universal axiom ∀y 1 . . . ∀y p ∀x (x ϵ f x,y1,...,yp,A (y 1 , . . . , y p ) ⇔ A)

In Deduction modulo, these axioms can be transformed into rewrite rules x ϵ f x,y1,...,yp,A (y 1 , . . . , y p ) -→ A This construction generalizes to n-ary classes: for each n, we introduce a sort κ n for n-ary classes, a (n + 1)-ary predicate symbol ϵ n , a n-ary comprehension scheme ∀y 1 . . . ∀y p ∃Z∀x 1 . . . ∀x n (ϵ n (x 1 , . . . , x n , Z) ⇔ A)

We can skolemize this scheme and introduce Skolem symbols f x1,...,xn,y1,...,yp,A . Finally, we can transform the skolemized axioms into rewrite rules

ϵ n (x 1 , . . . , x n , f x1,...,xn,y1,...,yp,A (y 1 , . . . , y p )) -→ A
Following an idea of Von Neuman, Bernays and Gödel, but using the more recent tool of explicit substitutions [START_REF] Abadi | Explicit substitutions[END_REF], Kirchner has shown that this infinite number of Skolem symbols, could be replaced by a finite language [START_REF] Kirchner | A finite first-order theory of classes[END_REF], but, we shall not use this here.

Arithmetic in Deduction modulo

Together with Werner, we have given in [START_REF] Dowek | Arithmetic as a theory modulo[END_REF] a presentation of predicative arithmetic in Deduction modulo. Starting with the theory of unary classes, we have transformed Leibniz definition of equality into a rewrite rule

y = z -→ ∀X (y ϵ X ⇒ z ϵ X)
Using trivial equivalences in predicate logic, the induction axiom above can be reformulated as

∀n (N (n) ⇒ ∀X (0 ϵ X ⇒ ∀y (N (y) ⇒ y ϵ X ⇒ S(y) ϵ X) ⇒ n ϵ X))
Then using the class f x,N (x) and the Peano first and second axioms (N (0) and ∀x (N (x) ⇒ N (S(x))) this implication can be transformed into an equivalence

∀n (N (n) ⇔ ∀X (0 ϵ X ⇒ ∀y (N (y) ⇒ y ϵ X ⇒ S(y) ϵ X) ⇒ n ϵ X))
and then into a rewrite rule

N (n) -→ ∀X (0 ϵ X ⇒ ∀y (N (y) ⇒ y ϵ X ⇒ S(y) ϵ X) ⇒ n ϵ X)
The Peano third and fourth axiom (∀x∀y (S(x) = S(y) ⇒ x = y) and ∀x¬S(x) = 0) can be transformed into rewrite rules if we introduce a new function symbol Pred and a new predicate symbol Null Finally, the axioms of addition and multiplication can be trivially transformed into rewrite rules.

Pred (0) -→ 0 Pred (S(x)) -→ x Null (0) -→ ⊤ Null (S(x)) -→ ⊥ x ϵ fx,y 1 ,...,yn,A(y1, . . . , yn) -→ A y = z -→ ∀X (y ϵ X ⇒ z ϵ X) N (n) -→ ∀X (0 ϵ X ⇒ ∀y (N (y) ⇒ y ϵ X ⇒ S(y) ϵ X) ⇒ n ϵ X) Null (0) -→ ⊤ Null (S(x)) -→ ⊥ Pred (0) -→ 0 Pred (S(x)) -→ x 0 + y -→ y S(x) + y -→ S(x + y) 0 × y -→ 0 S(x) × y -→ x × y + y
We get this way the rewrite system HA of Fig. 2, that defines a congruence ≡ HA and we can prove that Deduction modulo ≡ HA is a conservative extension of intuitionistic predicative arithmetic [START_REF] Dowek | Arithmetic as a theory modulo[END_REF]. This system can be divided into two subsystems HA 1 contains the five rules that rewrite atomic propositions to propositions and HA 2 the six rules that rewrite terms to terms.

Impredicative arithmetic in Deduction modulo

Extending this theory to impredicative (i.e. second-order) arithmetic just requires to extend the comprehension scheme and introduce symbols f x,y1,...,yn,A and the associated rewrite rules for all propositions A, including those containing the symbol ϵ, variables of sort κ and quantifiers over these variables.

Datatypes

This theory can be extended to other datatypes such as lists or trees: starting from the theory of unary classes, we introduce function symbols for the constructors of the datatype, a unary predicate symbol for the membership to the datatype, function symbols for the right-inverses of the constructors and predicate symbols for the images of the constructors. Then, the associated rewrite rules permit to prove the closure of the datatype by the constructors (the equivalents of the Peano first and second axioms), the induction principle (the equivalent of the Peano fifth axiom), the injectivity of constructors (the equivalent of the Peano third axiom) and the non confusion of the constructors (the equivalent of the Peano fourth axiom).

Normalization

Poofs in Deduction modulo do not normalize for all theories. For instance, taking the rule P -→ (Q ⇒ P ), we obtain a theory where all proofs normalize, but taking the rule P -→ (P ⇒ Q), we obtain a theory where proofs do not always normalize.

Together with Werner, we have proved in [START_REF] Dowek | Proof normalization modulo[END_REF] that all proofs normalize modulo some congruence if this congruence has a C-model, i.e. a model where propositions are valued, not in the algebra {0, 1}, but in the algebra C of reducibility candidates. We now define this algebra.

Reducibility candidates Definition 3 (Reducibility candidates). [5]

A proof is said to be neutral if it is an axiom or an elimination (i.e. of the form α, δ ⊥ (π), fst(π), snd (π),

δ(π 1 , απ 2 , βπ 3 ), (π π ′ ), (π t), or δ ∃ (π, xαπ ′ )), but not an introduction. A set R of proofs is a reducibility candidate if -whenever π ∈ R, then π is strongly normaling, -whenever π ∈ R and π ▷ * π ′ , then π ′ ∈ R, -whenever π is neutral and if for every π ′ such that π ▷ π ′ , π ′ ∈ R then π ∈ R.
We write C for the set of reducibility candidates and we define the following operations on this set: we let ⊤ = ⊥ = SN , if A and B are reducibility candidates, we let

A ∧ B = {π ∈ SN | π ▷ * ⟨π 1 , π 2 ⟩ ⇒ (π 1 ∈ A ∧ π 2 ∈ B)} A ∨ B = {π ∈ SN | π ▷ * i(π 1 ) ⇒ π 1 ∈ A ∧ π ▷ * j(π 2 ) ⇒ π 2 ∈ B} A ⇒ B = {π ∈ SN | π ▷ * λα π ′ ⇒ ∀σ ∈ A (σ/α)π ′ ∈ B} if A is a set of reducibility candidates, we let ∀ A = {π ∈ SN | π ▷ * λx π ′ ⇒ ∀X ∈ A∀t ∈ T (t/x)π ′ ∈ A}
where T is the set of terms of the language and

∃ A = {π ∈ SN | π ▷ * ⟨t, π ′ ⟩ ⇒ ∃X ∈ A π ′ ∈ X}
It is routine to check that these sets are reducibility candidates [START_REF] Dowek | Proof normalization modulo[END_REF].

C-models

Definition 4 (C-model). A C-model M for a many-sorted language L is given by for every sort s a set M s , for every function symbol f of rank ⟨s 1 , . . . , s n , s n+1 ⟩ a mapping f from M s1 × . . . × M sn to M sn+1 , for every predicate symbol P of rank ⟨s 1 , . . . , s n ⟩ a mapping P from M s1 × . . . × M sn to C.

The denotation of a term or a proposition in a C-model is defined as follows.

-

x ϕ = ϕ(x), f (t 1 , . . . , t n ) ϕ = f ( t 1 ϕ , . . . , t n ϕ ), -P (t 1 , . . . , t n ) ϕ = P ( t 1 ϕ , . . . , t n ϕ ), -⊤ ϕ = ⊤, ⊥ ϕ = ⊥, -A∧B ϕ = A ϕ ∧ B ϕ , A∨B ϕ = A ϕ ∨ B ϕ , A ⇒ B ϕ = A ϕ ⇒ B ϕ , -∀x A ϕ = ∀{ A ϕ+a/x | a ∈ M s }, ∃x A ϕ = ∃{ A ϕ+a/x | a ∈ M s }.
A C-model is said to be a C-model of a congruence ≡ if when A ≡ B then for every assignment ϕ, A ϕ = B ϕ .

Proposition 1. If a congruence has a C-model, then all proofs modulo this congruence strongly normalize.

Proof. See [START_REF] Dowek | Proof normalization modulo[END_REF].

Normalization for arithmetic

We can build a C-model for both predicative and impredicative arithmetic by taking M ι = N and M κ = N → C (the set of functions from N to C). The symbols 0, S, +, ×, and Pred are interpreted in the standard way. The symbol ϵ is interpreted by the function mapping n and f to f (n). We define N ull as the function mapping 0 to ⊤ and the other numbers to ⊥. The equality predicate, the predicate N and the Skolem symbols are interpreted in such a way that the corresponding rewrite rules are valid [START_REF] Dowek | Arithmetic as a theory modulo[END_REF].

However, we shall use another C-model that will be more useful later, where M ι is a singleton. With usual models, where propositions are valued in {0, 1}, the set M ι cannot be a singleton because the rules Null (0) -→ ⊤ and Null (S(x)) -→ ⊥, that replace the Peano fourth axiom, require N ull ( 0) = 1 and N ull ( Ŝ( 0)) = 0 and thus 0 and Ŝ( 0) to be distinct. For models where propositions are valued in C, we have the conditions N ull ( 0) = ⊤ and N ull ( Ŝ( 0)) = ⊥, but ⊤ = ⊥ = SN , thus nothing prevents M ι from being a singleton. Proposition 2. All proofs normalize modulo ≡ HA .

Proof. We construct a C-model as follows.

We let M ι be a singleton {0} and M κ = C. The symbols 0, S, +, ×, and Pred are interpreted in the trivial way. The symbol ϵ is interpreted by the function mapping 0 and C to C. We define = as the function mapping 0 and 0 to ∀X (y ϵ X ⇒ z ϵ X) 0/y,0/z . To define N we first define the function Φ that maps any reducibility candidate C to the interpretation of the proposition ∀X (0 ϵ X ⇒ ∀y (N (y) ⇒ y ϵ X ⇒ S(y) ϵ X) ⇒ n ϵ X) in the model of domains M ι and M κ and where 0 is interpreted by 0, S by Ŝ, ϵ by ε, but N by C. The set of reducibility candidates ordered by inclusion is complete and the function Φ is monotonous, thus it has a fixed point D. We let N = D.

We define N ull as the function mapping 0 to ⊤ = ⊥. This way we can interpret all the propositions A that do not contain Skolem symbols. Finally, we interpret the symbols f x,y1,...,yn,A as the functions mapping 0, . . . , 0 to A 0/x,0/y1,...,0/yn .

Non confusion and uniformity

As usual, we want to prove that normal closed proofs are uniform, i.e. that they end with an introduction rule. This requires an extra property of the congruence: that it is non confusing.

A congruence ≡ is said to be non confusing when if two non atomic propositions A and B are congruent, then either

-A = B = ⊤, -A = B = ⊥, -A = A 1 ∧ A 2 , B = B 1 ∧ B 2 , A 1 ≡ B 1 and A 2 ≡ B 2 , -A = A 1 ∨ A 2 , B = B 1 ∨ B 2 , A 1 ≡ B 1 and A 2 ≡ B 2 , -A = A 1 ⇒ A 2 , B = B 1 ⇒ B 2 , A 1 ≡ B 1 and A 2 ≡ B 2 , -A = ∀x A 1 , B = ∀x B 1 and A 1 ≡ B 1 , -A = ∃x A 1 , B = ∃x B 1 and A 1 ≡ B 1 .
The following Proposition allows to prove, for instance, that ≡ HA is non confusing.

Proposition 3. If a congruence is defined by a confluent rewrite system that rewrite terms to terms and atomic propositions to propositions, then it is non confusing.

Proof. If A and B are non atomic propositions such that A ≡ B, then by confluence, there exits a proposition C such that A reduces to C and B reduces to C. Thus C is non atomic, the main connector or quantifier of A and B are the same as that of C and the components of A and B rewrite to those of C.

Specifying programs

Deduction modulo ≡ HA can be used in at least two different ways to specify programs.

Proofs as programs

If n is a natural number, we write n for the term S n (0) and we write ρ n for the Parigot numeral n [START_REF] Parigot | Programming with proofs: A second order type theory[END_REF], i.e. the proof of N (n) defined as follows

-ρ 0 = λXλαλβ α -ρ n+1 = λXλαλβ (β n ρ n (ρ n X α β)).
Proposition 5. Let t be a term and π be a normal closed proof of N (t) modulo ≡ HA , then there exists a natural number n such that π = ρ n and t ≡ HA n.

Proof. By induction on the structure of π.

If π is a closed proof of the proposition

∀x 1 (N (x 1 ) ⇒ ∀x 2 (N (x 2 ) ⇒ . . . ⇒ ∀x n (N (x n ) ⇒ ∃y N (y)) . . .))
then for each p 1 , . . . , p n the normal form of the proof (π p 1 ρ p1 p 2 ρ p2 . . . p n ρ pn ) is a pair ⟨t, σ⟩ where t is a term and σ a normal closed proof of N (t). Thus, there exists a natural number q such that σ = ρ q and t ≡ HA q.

The proof π is a program mapping p 1 , . . . , p n to q.

Specifying programs with propositions

The first method to specify programs is to use the fact that for every computable partial function f from N n to N, there exists a proposition A such that the proposition (p 1 /x 1 , . . . , p n /x n , q/y)A is provable in arithmetic if and only if q = f (p 1 , . . . , p n ).

Example 1. The characteristic function of the set of even numbers is represented by the proposition

((∃z x = 2 × z) ⇒ y = 1) ∧ ((∃z x = 2 × z + 1) ⇒ y = 0) If π is a proof of the proposition ∀x 1 (N (x 1 ) ⇒ ∀x 2 (N (x 2 ) ⇒ . . . ⇒ ∀x n (N (x n ) ⇒ ∃y (N (y) ∧ A)) . . .))
then the normal form of the proof (π p 1 ρ p1 p 2 ρ p2 . . . p n ρ pn ) is a pair ⟨t, ⟨σ, τ ⟩⟩ where t is a normal term and σ a proof of N (t) and τ a proof of (p 1 /x 1 , . . . , p n /x n , t/y)A.

Thus, there exists a natural number q such that t ≡ HA q and σ = ρ q . The proposition (p 1 /x 1 , . . . , p n /x n , q/y)A is provable hence q = f (p 1 , . . . , p n ).

The proof

π ′ = λx 1 λα 1 . . . λx n λα n ⟨f st(π x 1 α 1 . . . x n α n ), fst(snd (π x 1 α 1 . . . x n α n ))⟩ is a proof of ∀x 1 (N (x 1 ) ⇒ ∀x 2 (N (x 2 ) ⇒ . . . ⇒ ∀x n (N (x n ) ⇒ ∃y N (y)) . . .))
and it is a program mapping p 1 , . . . , p n to f (p 1 , . . . , p n ).

Specifying programs with congruences

An original aspect of the FA 2 approach is that the programs are not specified as above, using a proposition representing the function in arithmetic, but using a set of equations à la Herbrand-Gödel. Recall that for each computable function f , there exists a function symbol F 0 , auxiliary function symbols F 1 , . . . , F k and a set of equational axioms E such that the proposition q = F 0 (p 1 , . . . , p n ) is provable from the axioms of E and the axioms of equality if and only if q = f (p 1 , . . . , p n ).

Example 2. The characteristic function of the set of even numbers is represented by the equations F (0) = S(0), F (S(0)) = 0, ∀x (F (S(S(x))) = F (x)).

In the FA 2 approach the equalities of E do not have any computational content: if t = u is such an equation, and A an arbitrary proposition, any proof of (t/x)A is a proof of (u/x)A and vice versa. This can be formalized in Deduction modulo, as the fact that the equations of E are part of the definition of the congruence.

Let ≡ HA∪E be the congruence defined by the rules of HA and the equations of E. Proposition 6. Deduction modulo ≡ HA∪E has the cut elimination property.

Proof. The rules HA and the axioms of E are valid in the C-model build in the proof of Proposition 2.

Non confusion, in contrast, requires an extra hypothesis on the equations of E. Indeed, if we had in E the equation 0 = S(0), or even S(0) = S(S(F (0))) we we would have Null (0) ≡ HA∪E Null (S(0)), or Null (0) ≡ HA∪E Null (S(F (0))), and thus ⊤ ≡ HA∪E ⊥.

Thus, we restrict to the case where the rules and equations of HA 2 ∪E do not allow to prove a proposition of the form 0 = S(t), i.e. such that the congruence ≡ HA2∪E verifies the property 0 ̸ ≡ HA2∪E S(t). This includes all the cases where E can be interpreted in the standard model of arithmetic, but also others such those where E contains the equation F (0) = S(F (0)) that correspond to partial computable functions not defined in 0.

We consider the rewriting relation defined by the rules of HA 1 modulo ≡ HA2∪E , it is defined by A -→ HA1/HA2∪E B if there exists A ′ and B ′ such that A ≡ HA2∪E A ′ , A ′ -→ HA1 B ′ , and B ′ ≡ HA2∪E B, where A ′ -→ HA1 B ′ means that A ′ rewrites to B ′ with one of the rules of HA 1 .

The next proposition shows that the use of the congruence in -→ HA1/HA2∪E can be localized in the sense of [START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF][START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF].

We use the following notation, if A is a tree and o an occurrence in A, we write A |o for the subtree of A taken at occurrence o and A[B] o for the tree A where the tree B has been grafted at the occurrence o. Proposition 10. Let t be a term and π be a normal closed proof of N (t) modulo ≡ HA∪E , then there exists a natural number n such that π = ρ n and t ≡ HA∪E n.

Proof. By induction on the structure of π.

Finally, if π is a proof of the proposition

∀x 1 (N (x 1 ) ⇒ ∀x 2 (N (x 2 ) ⇒ . . . ⇒ ∀x n (N (x n ) ⇒ ∃y (N (y)∧y = F 0 (x 1 , . . . , x p ))) . . .))
then the normal form of the proof (π p 1 ρ p1 p 2 ρ p2 . . . p n ρ pn ) is a pair ⟨t, ⟨σ, τ ⟩⟩ where t is a normal term and σ a proof of N (t) and τ a proof of t = F (p 1 , . . . , p n ).

Thus there exists a natural number q, such that σ = ρ q and t ≡ HA∪E q the proposition q = F (p 1 , . . . , p n ) is provable modulo ≡ HA∪E .

Let r = f (p 1 , . . . , p n ). The proposition r = F (p 1 , . . . , p n ) is provable from the axioms of E and the axioms of equality, thus it is provable modulo ≡ HA∪E .

Thus, the proposition r = q is provable modulo ≡ HA∪E . As ≡ HA∪E is normalizing and non confusing it is consistent, thus q = r and q = f (p 1 , . . . , p n ).

The proof

π ′ = λx 1 λα 1 . . . λx n λα n ⟨f st(π x 1 α 1 . . . x n α n ), fst(snd (π x 1 α 1 . . . x n α n ))⟩ is a proof of ∀x 1 (N (x 1 ) ⇒ ∀x 2 (N (x 2 ) ⇒ . . . ⇒ ∀x n (N (x n ) ⇒ ∃y N (y)) . . .))
and it is a program mapping p 1 , . . . , p n to f (p 1 , . . . , p n ).

Specifications

We have seen that the characteristic function of even numbers could be specified either with the proposition

((∃z x = 2 × z) ⇒ y = 1) ∧ ((∃z x = 2 × z + 1) ⇒ y = 0)
or with the equational axioms

F (0) = S(0) F (S(0)) = 0 ∀x (F (S(S(x))) = F (x))
We may discuss if this equational specification should be called a specification or a program as, if we orient the equations, we get the rewrite rules F (0) -→ S(0) F (S(0)) -→ 0 F (S(S(x))) -→ F (x)

that define an algorithm computing the value of this function. However, the situation is not always as simple. For instance, if we add the equation F (0) = F (0), we obtain a rewrite system that is not locally deterministic, as the set term F (0) reduces both to S(0) and to itself and that is only weakly terminating. Thus although the specification remains executable, its execution mechanisms is better described as a proof search process in an equational theory rather than as a mere reduction. In this sense, the propositional specification also is executable, as for every p 1 , ..., p n we can use a proof search system to find a proof in arithmetic of ∃y (p 1 /x 1 , ..., p n /x n )A and extract a witness from this proof. The specification is just easier to execute in the second case because proof search is easier in an equational theory than in arithmetic. Thus, the difference between these two ways of specifying programs is not in the fact that one specification is executable and not the other.

The difference seems to be that the two approaches are based on a different notion of definition. In set theory, for instance, the notion of intersection of two sets can either be explicitly defined by stating that A ∩ B is an abbreviation for {x ∈ A | x ∈ B} or implicitly defined by introducing a new primitive symbol ∩ and the axiom x ∈ A∩B ⇔ (x ∈ A∧x ∈ B). In the same way, we can say that the characteristic function of the set of even numbers can either be explicitly defined by the proposition ((∃z x = 2 × z) ⇒ y = 1) ∧ ((∃z x = 2 × z + 1) ⇒ y = 0) or implicitly defined with the introduction of a new primitive symbol F and the axioms F (0) = S(0), F (S(0)) = 0, ∀x (F (S(S(x))) = F (x)).

Using an implicit definition requires to introduce axioms and thus jeopardizes the possibility to extract witnesses from constructive proofs. However, integrating these axioms in the congruence preserving normalization, non confusion and the form of the proofs of N (t), restores this possibility to extract witnesses from constructive proofs.

Fig. 1 .

 1 Fig. 1. Natural deduction modulo

Fig. 2 .

 2 Fig. 2. The rewrite system HA

Proposition 4 .

 4 If a congruence ≡ is non confusing, then normal closed proofs end with an introduction rule.Proof. By induction over proof structure.

Proposition 7 .Proposition 8 . 2 . 9 .

 7829 If A -→ HA1/HA2∪E B then there exists an occurrence o of an atomic proposition in A, a proposition rewrite rule l -→ r of HA 1 and a substitution σ such that A |o ≡ HA2∪E σl and B ≡ HA2∪E A[σr] o . Proof. By induction on the structure of A. The relation -→ HA1/HA2∪E is confluent.Proof. We prove more generally that this relation is strongly confluent, i.e. if A -→ HA1/HA2∪E B 1 and A -→ HA1/HA2∪E B 2 , then there exists a C such that(B 1 = C or B 1 -→ HA1/HA2∪E C) and (B 2 = C or B 2 -→ HA1/HA2∪E C).If A -→ HA1/HA2∪E B 1 and A -→ HA1/HA2∪E B 2 , then by Proposition 7, there exists an occurrence o 1 , a rule l 1 -→ r 1 of HA 1 , and a substitution σ 1 such that A |o1 ≡ HA2∪E σ 1 l 1 and B 1 ≡ HA2∪E A[σ 1 r 1 ] o1 and an occurrence o 2 , a rule l 2 -→ r 2 of HA 1 , and a substitution σ 2 such that A |o2 ≡ HA2∪E σ 2 l 2 , andB 2 ≡ HA2∪E A[σ 2 r 2 ] o2 .If the occurrences o 1 and o 2 are distinct, they are disjoint and we can close the diagram in one step.If they are equal, then, as 0 ̸ ≡ HA2∪E S(t), the rule is the same and B 1 ≡ HA2∪E B Proposition The congruence ≡ HA∪E is non confusing. Proof. The reflexive-symmetric-transitive closure of the relation -→ HA1/HA2∪E is the relation ≡ HA∪E . Thus, by Proposition 8, if A ≡ HA∪E B, there exists a proposition C such that A -→ * HA1/HA2∪E C and B -→ * HA1/HA2∪E C. Thus C is non atomic, the main connector or quantifier of A and B are the same as that of C and the components of A and B rewrite to those of C.

The deduction rules are expressed in such a way that deduction is performed modulo this congruence. The rules of intuitionistic natural deduction modulo are given Fig.1.axiom if A ∈ Γ and A ≡ B Γ ⊢ B ⊤-intro if A ≡ ⊤ Γ ⊢ A Γ ⊢ B ⊥-elim if B ≡ ⊥ Γ ⊢ A Γ ⊢ A Γ ⊢ B ∧-intro if C ≡ (A ∧ B) Γ ⊢ C Γ ⊢ C ∧-elim if C ≡ (A ∧ B) Γ ⊢ A Γ ⊢ C ∧-elim if C ≡ (A ∧ B) Γ ⊢ B Γ ⊢ A ∨-intro if C ≡ (A ∨ B) Γ ⊢ C Γ ⊢ B ∨-intro if C ≡ (A ∨ B) Γ ⊢ C Γ ⊢ D Γ, A ⊢ C Γ, B ⊢ C ∨-elim if D ≡ (A ∨ B) Γ ⊢ C Γ, A ⊢ B ⇒-intro if C ≡ (A ⇒ B) Γ ⊢ C Γ ⊢ C Γ ⊢ A ⇒-elim if C ≡ (A ⇒ B) Γ ⊢ B Γ ⊢ A ⟨x, A⟩ ∀-intro if B ≡ (∀x A) and x ̸ ∈ F V (Γ ) Γ ⊢ BΓ ⊢ B ⟨x, A, t⟩ ∀-elim if B ≡ (∀x A) and C ≡ (t/x)A

Acknowledgements

The author wants to thank Ying Jiang for her remarks on a previous draft of this note.