Matthieu Furet

Philippe Wenger

Derivation of a polynomial equation for the boundaries of 2-X manipulators

Keywords: Kinematics, crossed four-bar mechanism, anti-parallelogram, Workspace, Cuspidal

This paper derives the boundary equations of the workspace of a manipulator made of two crossed four-bar mechanisms in series. The boundaries are determined with the discriminant of the characteristic polynomial derived for the inverse kinematics.

Introduction

A crossed four-bar mechanism, referred to as X-mechanism, is a four-bar mechanism assembled in a X-shape configuration, see figure 1. Because of a variable instantaneous center of rotation (ICR), this mechanism has a large range of motion. Moreover, tendon driven actuation can be easily implemented and a lightweight manipulator with remote actuation can be designed by stacking several such mechanisms [START_REF] Moored | Analytical predictions, optimization, and design of a tensegritybased artificial pectoral fin[END_REF]. Eventually, lateral springs can be added on each side of the mechanism, thus defining a X-shape Snelson tensegrity mechanism [START_REF] Snelson | Continuous Tension, Discontinuous Compression Structures[END_REF], suitable for variable stiffness and natural interaction with the environment [START_REF] Bakker | Design of an environmentally interactive continuum manipulator[END_REF], [START_REF] Wenger | Kinetostatic Analysis and Solution Classification of a Planar Tensegrity Mechanism[END_REF]. This work is part of the AVINECK project involving biologists and roboticists with the main goal to model and design bird necks. Accordingly, a class of planar tensegrity manipulators made of a series assembly of several Snelson's X-shape mechanisms has been chosen as a suitable candidate for a preliminary planar model of a bird neck. A planar two-degree-of-freedom manipulator is obtained with a series assembly of two such mechanisms. First investigations on the kinematics of such manipulators have proven more challenging than expected, in particular for the solution of the inverse kinematics [START_REF] Furet | Kinematic analysis of planar 2-X tensegrity manipulators[END_REF]. This paper derives the boundary equations of the workspace of a manipulator made of two crossed fourbar mechanisms in series. The boundaries are determined with the discriminant of the characteristic polynomial derived for the inverse kinematics. It is found that internal boundary curves may exist with cusp points [START_REF] Furet | Workspace and cuspidality analysis of a 2-X planar manipulator[END_REF], showing that the manipulator at hand is cuspidal ( [START_REF] Omri | How to recognize simply a non-singular posture changing manipulator[END_REF], [START_REF] Wenger | Cuspidal and noncuspidal robot manipulators[END_REF]).

Manipulator modelling and Kinematic equations

The manipulators studied consist of a series assembly of two identical X-mechanisms as shown in figure 2. Both the base bar and the upper bar are of length Fig. 1: Snelson's X-shape mechanism made of a crossed four-bar mechanism with lateral springs b and the two crossed links are of length L with L>b. Thus, each X-mechanism defines a so-called anti-parallelgramm joint. A line segment of length l i is defined that links the middle points of the top and base bars of each mechanism i (shown in red dotted line in figure 2). The angle between this line and the direction orthogonal to the base bar, referred to as θ i , is used to define the configuration of mechanism i without ambiguity, assuming that it remains always in its crossedbar assembly mode [START_REF] Furet | Kinematic analysis of planar 2-X tensegrity manipulators[END_REF]. Accordingly, the manipulator configuration can be fully defined with (θ 1 , θ 2 ). To avoid any self collisions, the bars should be assembled in different layers or suitable joint limits should be defined. The base frame is centered at the middle point of the base bar of the first X-mechanism with the x-axis aligned along this bar. The reference point (x, y) is chosen as the middle point of the top-bar of the second X-mechanism (figure 2). Since the sides of

θ 1 θ 2 l 1 l 2 (x,y)
Fig. 2: Manipulator description each mechanism define an isosceles trapezoid, the length l i of the line segment that links the middle points of the top and base bars can be expressed as follows [START_REF] Furet | Kinematic analysis of planar 2-X tensegrity manipulators[END_REF]:

l i (θ i ) = L 2 -b 2 cos 2 (θ i ) (1)
The direct kinematic equations of the 2-X manipulator can be put in the following form :

x = -l 1 (θ 1 ) sin(θ 1 ) -l 2 (θ 2 ) sin(2θ 1 + θ 2 ) y = l 1 (θ 1 ) cos(θ 1 ) + l 2 (θ 2 ) cos(2θ 1 + θ 2 ) (2)
where l 1 and l 2 are defined in [START_REF] Moored | Analytical predictions, optimization, and design of a tensegritybased artificial pectoral fin[END_REF]. Note that these equations assume that each mechanism remains in its crossed-bar assembly-mode. The inverse kinematics is much more challenging to establish and cannot be obtained from (2) easily. A methodology was proposed in [START_REF] Furet | Kinematic analysis of planar 2-X tensegrity manipulators[END_REF], which makes it possible to derive a characteristic polynomial of degree four and it was shown that the manipulator may have up to four solutions.

Workspace boundary equations

The manipulator workspace is determined by means of its boundaries. These boundaries can be obtained from the discriminant of the 4th-order characteristic polynomial derived for the inverse kinematics. This characteristic polynomial in t=tan(φ 1 /2) was derived in [START_REF] Furet | Kinematic analysis of planar 2-X tensegrity manipulators[END_REF] and is recalled below, where L has been set to 1 without loss of generality:

a 4 t 4 + a 3 t 3 + a 2 t 2 + a 1 t + a 0 = 0 (3)
where :

a 4 = (b + 1) 2 (b 2 y 2 + x 4 + 2x 2 y 2 + y 4 + 4x 3 + 4xy 2 + 5x 2 + y 2 + 2x) (4)
a 3 = 4y(b + 1)(2b 2 x + b 2 -2x 2 -2y 2 -4x -1) (5)
a 2 = 2(b 4 y 2 + b 2 x 4 + 2b 2 x 2 y 2 + b 2 y 4 + b 2 x 2 -10b 2 y 2 + x 4 + 2x 2 y 2 + y 4 -3x 2 + 9y 2 ) (6) a 1 = 4y(b -1)(2b 2 x -b 2 + 2x 2 + 2y 2 -4x + 1) (7)
a 0 = (b -1) 2 (b 2 y 2 + x 4 + 2x 2 y 2 + y 4 -4x 3 -4xy 2 + 5x 2 + y 2 -2x) (8)
The discriminant of this polynomial is derived with the help of a symbolic computing software. Accordingly, a polynomial equation of degree 16 in x and y is obtained as shown below. Figure 3 shows the plot of these boundary curves for three cases. In the second and third cases, they divide the workspace into three regions. In the largest one, the manipulator admits two inverse kinematic solutions. In the two smaller regions (filled in grey), there are four solutions. Figure 4 shows the four inverse kinematic solutions for the manipulator defined by L = 1 and b = 9/10, at x = 0, y = 1.

Conclusion

The equation of the boundary curves of the workspace of a 2-X manipulator was derived using the discriminant of the characteristic polynomial derived for the inverse kinematics. The resulting polynomial is of degree 16 and, under some geometric conditions, reveals regions with four inverse kinematic solutions. Moreover, the boundary curves of the 4-solution regions feature two cusp points and one node.

4 b 14 y 6

 6 +12 b 12 x 4 y 4 +28 b 12 x 2 y 6 +17 b 12 y 8 +12 b 10 x 8 y 2 +60 b 10 x 6 y 4 +112 b 10 x 4 y 6 + 92 b 10 x 2 y 8 +28 b 10 y 10 +4 b 8 x 12 +36 b 8 x 10 y 2 +126 b 8 x 8 y 4 +224 b 8 x 6 y 6 +216 b 8 x 4 y 8 + 108 b 8 x 2 y 10 +22 b 8 y 12 +4 b 6 x 14 +32 b 6 x 12 y 2 +108 b 6 x 10 y 4 +200 b 6 x 8 y 6 +220 b 6 x 6 y 8 + 144 b 6 x 4 y 10 + 52 b 6 x 2 y 12 + 8 b 6 y 14 + b 4 x 16 + 8 b 4 x 14 y 2 + 28 b 4 x 12 y 4 + 56 b 4 x 10 y 6 + 70 b 4 x 8 y 8 + 56 b 4 x 6 y 10 + 28 b 4 x 4 y 12 + 8 b 4 x 2 y 14 + b 4 y 16 -24 b 12 x 2 y 4 -36 b 12 y 6 -48 b 10 x 6 y 2 -204 b 10 x 4 y 4 -276 b 10 x 2 y 6 -120 b 10 y 8 -24 b 8 x 10 -204 b 8 x 8 y 2 -612 b 8 x 6 y 4 -852 b 8 x 4 y 6 -564 b 8 x 2 y 8 -144 b 8 y 10 -36 b 6 x 12 -252 b 6 x 10 y 2 -720 b 6 x 8 y 4 -1080 b 6 x 6 y 6 -900 b 6 x 4 y 8 -396 b 6 x 2 y 10 -72 b 6 y 12 -12 b 4 x 14 -84 b 4 x 12 y 2 -252 b 4 x 10 y 4 -420 b 4 x 8 y 6 -420 b 4 x 6 y 8 -252 b 4 x 4 y 10 -84 b 4 x 2 y 12 -12 b 4 y 14 -8 b 12 y 4 +32 b 10 x 4 y 2 + 126 b 10 x 2 y 4 +102 b 10 y 6 +40 b 8 x 8 +332 b 8 x 6 y 2 +826 b 8 x 4 y 4 +816 b 8 x 2 y 6 +282 b 8 y 8 + 110 b 6 x 10 + 666 b 6 x 8 y 2 + 1564 b 6 x 6 y 4 + 1796 b 6 x 4 y 6 + 1014 b 6 x 2 y 8 + 226 b 6 y 10 + 54 b 4 x 12 + 324 b 4 x 10 y 2 + 810 b 4 x 8 y 4 + 1080 b 4 x 6 y 6 + 810 b 4 x 4 y 8 + 324 b 4 x 2 y 10 + 54 b 4 y 12 -4 b 10 x 2 y 2 + 56 b 10 y 4 -36 b 8 x 6 -164 b 8 x 4 y 2 -228 b 8 x 2 y 4 -92 b 8 y 6 -148 b 6 x 8 -716 b 6 x 6 y 2 -1244 b 6 x 4 y 4 -932 b 6 x 2 y 6 -256 b 6 y 8 -116 b 4 x 10 -572 b 4 x 8 y 2 -1128 b 4 x 6 y 4 -1112 b 4 x 4 y 6 -548 b 4 x 2 y 8 -108 b 4 y 10 +4 b 10 y 2 +17 b 8 x 4 +14 b 8 x 2 y 2 -143 b 8 y 4 + 126 b 6 x 6 + 294 b 6 x 4 y 2 + 136 b 6 x 2 y 4 -36 b 6 y 6 + 141 b 4 x 8 + 492 b 4 x 6 y 2 + 622 b 4 x 4 y 4 + 332 b 4 x 2 y 6 + 61 b 4 y 8 + 2 b 2 x 10 + 6 b 2 x 8 y 2 + 4 b 2 x 6 y 4 -4 b 2 x 4 y 6 -6 b 2 x 2 y 8 -2 b 2 y 10 -4 b 8 x 2 -20 b 8 y 2 -60 b 6 x 4 -20 b 6 x 2 y 2 + 172 b 6 y 4 -132 b 4 x 6 -200 b 4 x 4 y 2 + 28 b 4 x 2 y 4 + 96 b 4 y 6 -16 b 2 x 8 -32 b 2 x 6 y 2 + 32 b 2 x 2 y 6 + 16 b 2 y 8 + 16 b 6 x 2 +40 b 6 y 2 +70 b 4 x 4 +16 b 4 x 2 y 2 -98 b 4 y 4 +38 b 2 x 6 +38 b 2 x 4 y 2 -38 b 2 x 2 y 4 -38 b 2 y 6 -24 b 4 x 2 -40 b 4 y 2 -28 b 2 x 4 -8 b 2 x 2 y 2 + 20 b 2 y 4 + 16 b 2 x 2 + 20 b 2 y 2 + x 4 + 2 y 2 x 2 + y 4 -4 x 2 -4 y 2 = 0

Fig. 3 :Fig. 4 :

 34 Fig. 3: Workspace boundaries when L = 1 and b = 2/5 (left), b = 2/3 (center), b = 9/10 (right)

Acknowledgement This work has been conducted in part with the support of the French National Research Agency (AVINECK Project ANR-16-CE33-0025).


Miguel Couceiro
email: miguel.couceiro@loria.fr

Pierre Mercuriali
email: pierre.mercuriali@loria.fr

Romain P Échoux
email: romain.pechoux@loria.fr

Abdallah Saffidine
email: abdallah.saffidine@gmail.com

On the complexity of minimizing median normal forms of monotone Boolean functions and lattice polynomials

Keywords: Boolean function, Monotone Boolean functions, Lattice polynomials, Normal form, Median, Median algebra, Majority, Structural representation, Efficient representation, Complexity, Polynomial hierarchy

In this document, we consider a median-based calculus to represent monotone Boolean functions efficiently. We study an equational specification of median forms and extend it from the domain of monotone Boolean functions to the domain of polynomial functions over distributive lattices. This specification is sound and complete. We illustrate its usefulness when simplifying median formulas algebraically. Furthermore, we propose a definition of median normal forms (MNF), that are thought of as minimal median formulas with respect to a structural ordering of expressions. We investigate related complexity issues and show that the problem of deciding whether a formula is in MNF, that is the problem of minimizing the median form of a monotone Boolean function, is in Σ P 2 . Moreover, we show that it still holds for arbitrary Boolean functions, not necessarily monotone.

INTRODUCTION

Motivation Representing Boolean functions using different connectives may yield representations that are of drastically different sizes. In the case of Boolean functions, it has been shown that a median-based representation, that is, a representation based on the ternary median operator, yields asymptotically smaller formulas -in terms of number of connectives -than the classical DNF, CNF, and polynomial normal forms [START_REF] Couceiro | Composition of post classes and normal forms of boolean functions[END_REF]. Moreover, algorithmic procedures to obtain such median representations were given in [START_REF] Couceiro | An algorithm for producing median normal form representations for Boolean functions[END_REF]. However, these procedures may not produce median formulas of the lowest possible complexity (size). This fact asks for procedures to simplify median formulas, in analogy with well known resolution procedures for DNF and CNF expressions.

Since median expressions can be translated into the language of bounded distributive lattices and conversely, lattice polynomials can also be represented by median expressions. Thus, in addition to applications in logic and circuit design, these simplifications become useful when efficiently representing noteworthy lattice functions and other aggregation functions ( [START_REF] Grabisch | Aggregation functions[END_REF]).

Outline and contribution Motivated by these observations and following the work of [START_REF] Couceiro | Composition of post classes and normal forms of boolean functions[END_REF], in this paper we investigate the use of the ternary median connective to efficiently represent monotone Boolean functions.

In Section 2 we recall basic background on lattice functions and median algebras that will be used throughout this paper. In Section 3 we recall a finite equational specification (System 1) that allows the simplification of median formulas while preserving logical equivalence. As an immediate consequence of the soundness and completeness of this equational specification (Theorem 1), we may rewrite any formula into any other that is logically equivalent to it. Furthermore, median formulas can be simplified algebraically according to this equational specification. We then propose a structural and lexicographic ordering of formulas in Section 4, and introduce median normal forms (MNFs) as being median formulas that are minimal with respect to this ordering. In Section 5 we consider two decision problems related to the task of finding an MNF of a given formula, and we show that both are at most moderately intractable, by which we mean that they are likely to be intractable, but not beyond Σ P 2 . We also explore a different approach to the potential intractability issue by providing a term rewriting system based on the equational specification (System 1). Even though the resulting system is not complete, it runs in polynomial time, thus highlighting a trade-off in complexity: either we sacrifice completeness but preserve tractability, or we keep completeness at the cost of high complexity. In Section 6, we discuss the previous results with regard to arbitrary Boolean functions, not necessarily monotone. Naturally, allowing negations in median normal forms does not increase the complexity. However, we show that even in the case of monotone functions, allowing negated variables at the leaves may provide representations strictly smaller than the ones obtained with only variables and constants.

A preliminary version of the current paper appeared in the Proceedings of the 47th International Symposium on Multi-Valued Logic, [START_REF] Couceiro | Median Based Calculus for Lattice Polynomials and Monotone Boolean Functions[END_REF].

LATTICE POLYNOMIALS AND MEDIAN FORMULAS

Our first motivation for the systematic study of median formulas is the fact that they can represent lattice polynomials.

Notation and Preliminaries

In this subsection we recall definitions and notations on lattice and lattice functions, while adopting the terminology of [START_REF] Couceiro | Characterizations of discrete sugeno integrals as polynomial functions over distributive lattices[END_REF]. A lattice is an algebraic structure L, ∧, ∨ where L is a nonempty set, called universe, and where ∧ and ∨ are two binary operations that satisfy the laws of commutativity, associativity, absorption, and idempotence; a lattice is said to be distributive if the two laws distribute over one another. With no danger of ambiguity, we will denote a lattice L, ∧, ∨ by its universe L.

In what follows, L will always denote an arbitrary bounded distributive lattice with least and greatest elements ⊥ and , respectively. For a, b ∈ L, a ≤ b means that a ∧ b = a or, equivalently, a ∨ b = b. For any integer n ≥ 1, we set [n] = {1, . . . , n}. For an arbitrary nonempty set A and a lattice L, the set L A of all functions from A to L also constitutes a lattice under the operations

(f ∧ g)(x) = f (x) ∧ g(x) and (f ∨ g)(x) = f (x) ∨ g(x)
for every f, g ∈ L A . In particular, any lattice L induces a lattice structure on the Cartesian product L n , n ≥ 1, by defining ∧ and ∨ componentwise, i.e.,

(a 1 , . . . , a n ) ∧ (b 1 , . . . , b n ) = (a 1 ∧ b 1 , . . . , a n ∧ b n ), (a 1 , . . . , a n ) ∨ (b 1 , . . . , b n ) = (a 1 ∨ b 1 , . . . , a n ∨ b n ).
We denote the elements of L by lower case letters a, b, c, . . . and the elements of L n , n > 1, by bold face letters a, b, c, . . . . We now recall the notion of lattice polynomial function. The class of lattice polynomial functions (or simply, polynomial functions) from L n to L is defined inductively as the set of functions represented by expressions constructed in the language of lattices: the projections x → x i , the constant functions x → c, c ∈ L, and if f and g are polynomial functions, then so are f ∧ g and f ∨ g.

For instance, the ternary median m, i.e., the function given by:

m(x 1 , x 2 , x 3 ) = (x 1 ∧ x 2 ) ∨ (x 2 ∧ x 3 ) ∨ (x 3 ∧ x 1 ) = (x 1 ∨ x 2 ) ∧ (x 2 ∨ x 3 ) ∧ (x 3 ∨ x 1 )
is an example of such a polynomial function.

Equational specification and term rewriting system

We make use of the notations of [START_REF] Klop | Term rewriting systems[END_REF] and [START_REF] Baader | Term rewriting and all that[END_REF] to introduce equational specifications. An equational specification, (sometimes called equational system within this document) is a pair (Σ, E) of an alphabet or signature Σ and a set of equations E. The alphabet Σ consists of a countably infinite set of variables x 1 , x 2 , . . . and a nonempty set of function symbols or operator symbols.

In the current setting, this set contains m and constants. The set of terms (or expressions) over Σ is denoted by Ter(Σ) and it is defined inductively as follows:

(1) every variable and constant in Σ is in Ter(Σ), and

(2) if f is an n-ary function symbol and t 1 , . . . , t n are terms, then f (t 1 , . . . , t n ) is in Ter(Σ).

An equation is then an expression of the form s = t where s, t ∈ Ter(Σ). The set of all equations is denoted by E.

The set of median terms (also referred to as median expressions or median formulas in [START_REF] Couceiro | Composition of post classes and normal forms of boolean functions[END_REF]) M will denote the set of all formulas that are constructed using variables, constants and the median m. Even though [START_REF] Couceiro | Composition of post classes and normal forms of boolean functions[END_REF] focuses on median normal expressions for Boolean functions, this notion adapts to lattice polynomial functions, as the syntax of the language used to represent the monotone Boolean functions and lattice polynomial functions is the same.

Given a formula φ in M, its depth is denoted by d(φ) and defined recursively as follows:

(i) for every variable or constant a, d(a) = 0, (ii) for every formula φ = m(a, b, c) ∈ M,

d(φ) = max{d(a), d(b), d(c)} + 1.
The size |φ| of a median term φ is the number of medians in it. Two median terms φ and ψ are said to be equivalent, denoted by φ ≡ ψ, if they represent the same function.

Example 2. For instance, the median terms:

φ 1 = m(m(m(x, u, v), m(x, y, v), m(y, u, v)), x, v) φ 2 = m(m(u, y, v), x, v)
are equivalent. However, the median terms: φ 3 = m(m(x, y, z), u, v) and φ 4 = m(x, m(y, z, u), v) are not equivalent. The latter expresses the fact that m is not associative in the sense of [START_REF] Aczél | The associativity equation re-revisited[END_REF][START_REF] Couceiro | Aczélian n-ary semigroups[END_REF][START_REF] Post | Polyadic groups[END_REF].

A substitution is a map σ from Ter(Σ) to Ter(Σ) that satisfies

σ(F (t 1 , . . . , t n )) = F (σ(t 1 ), . . . , σ(t n ))
for every n-ary function symbol (here n ≥ 0).

Substitution together with the other rules recalled in Table 1, give rise to the so-called derivable equations, i.e., equations obtained by applying a finite combination of these rules. If an equation s = t is derivable from equations in E, than we write (Σ, E) s = t or s E t for short.

(Σ, E) t = t if t ∈ Ter(Σ) (Σ, E) s = t if s = t ∈ E (Σ, E) s = t (Σ, E) t = s (Σ, E) t 1 = t 2 , (Σ, E) t 2 = t 3 (Σ, E) t 1 = t 3 (Σ, E) s = t (Σ, E) σ(s) = σ(t)
for every substitution σ

(Σ, E) s 1 = t 1 , . . . , (Σ, E) s n = t n (Σ, E) F (s 1 , . . . , s n ) = F (t 1 , . . . , t n ) for every n-ary F ∈ Σ Table 1 Equational inference system.
We now recall definition and notation on term rewriting systems. A Term Rewriting System (TRS) is an equational specification with all its equations oriented. A pair (l, r) of terms in Ter(Σ), written as l -→ r, is a reduction rule if r is not a variable and all the variables in l are already contained in r.

Each term rewriting system yields a rewrite relation defined to be the closure by substitution and context of its reduction rules.

AXIOMATIZATION OF LATTICE POLYNOMIALS

In this section, we present an equational system for median calculus which is both sound and complete, and which we then use to manipulate median expressions.

First, recall that lattice polynomial functions f : L n → L are exactly the solutions of the median decomposition system [START_REF] Marichal | Weighted lattice polynomials[END_REF]:

f (x) = m(f (x ⊥ k ), x k , f (x k )) (1)
for all x = (x 1 , . . . , x n ), k ∈ [n] and c ∈ L, and where

x c k := (x 1 , . . . , x k-1 , c, x k+1 , . . . , x n ).
A direct consequence of this result is that every polynomial function can be represented by a median term. Indeed, recursive applications of (1) on each x 1 , . . . , x n of an n-ary polynomial function f produces a median formula representing f , see, e.g., [START_REF] Couceiro | An algorithm for producing median normal form representations for Boolean functions[END_REF]. However, this procedure may not produce optimal formulas (size wise), and this fact motivates the current study.

Example 3. Consider the 5-ary majority operator

m 5 : x → m 5 (x 1 , x 2 , x 3 , x 4 , x 5 )
over Boolean variables. Using the median decomposition algorithm mentioned above we can construct a median formula representation of this function using its values on every point of {⊥, } 5 . This produces a representation of size 1 + 2 + 4 + 8 + 16 = 31 that is not optimal. Indeed, there exists a much smaller representation of size 4, as shown in [START_REF] Bandelt | The algebra of majority consensus[END_REF][START_REF] Miller | Majority-logic synthesis by geometric methods[END_REF]:

m 5 (x 1 , x 2 , x 3 , x 4 , x 5 ) = m(m(m(x 2 , x 3 , x 4 ), x 4 , x 5 ), m(x 2 , x 3 , x 5 ), x 1 ).
Let us now recall an axiomatization of the algebraic structure L, m, ⊥, , that is the set L with the ternary median function m and the 0-ary functions (constants) ⊥ and , by the following equational system. It was given in, e.g., [START_REF] Birkhoff | Lattice theory[END_REF].

System 1.

(M 1) m(x, y, z) = m(x, z, y) = m(z, x, y),

(M 2) m(x, x, y) = x, (M 3) m(m(x, u, v), m(y, u, v), z) = m(m(x, y, z), u, v), (M 4) m(⊥, , x) = x, for all x, y, z, u, v in L.
Equations (M 1), (M 2), (M 3) are known as symmetry, majority, distributivity laws, respectively. Remark 1. An axiomatization of the Boolean algebra {0, 1}, ∧, ∨,., 0, 1 was used in [START_REF] Amarú | Majority-inverter graph: A novel datastructure and algorithms for efficient logic optimization[END_REF] to simplify Boolean circuits. System 1 is an adaptation of these results to the case of lattice polynomials.

In order to manipulate median formulas, we need to know whether the axiomatization given by System 1 is both sound and complete. Soundness means that every equation s = t that can be derived from System 1 is valid, i.e., that the formulas s and t are equivalent. Completeness means that every equation s = t that is valid can be derived from the axioms of the system. For our purposes, having a sound and complete system is interesting in order to rewrite median terms, and hopefully simplify them. Soundness indeed ensures that whatever simplification we do by applying an equation to a median term will preserve logical equivalence, while completeness ensures that we can infer a median term from an equivalent one by using System 1.

Theorem 1 ([7]

). The algebra L, m, ⊥, together with the axioms of System 1 is sound and complete. Sketch of Proof. Soundness is provable algebraically by deriving the axioms of the system using the properties of the lattice L. For instance, the symmetry (M 1) stems from the symmetry of the meet and join of L. Completeness is an immediate consequence of the Birkhoff's Completeness Theorem for equational logic, see, e.g., [START_REF] Burris | A Course in universal algebra[END_REF][START_REF] Klop | Term rewriting systems[END_REF].

MEDIAN NORMAL FORMS

In this section, we propose a structural description of median formulas and introduce the notion of median normal forms (MNF) that, as we shall see, correspond to median formulas that are "minimal" with respect to the lexicographical ordering of their structural description.

Orders A binary relation on a set S is a quasi-order, or preorder, if it is reflexive and transitive. A quasi-order is said to be a partial order if it is antisymmetric. If is a partial order, the structure S, is called a partially ordered set (or poset). A quasi-ordered set is well-founded if it satisfies the descending chain condition, i.e., there exists no infinite decreasing sequence • • • < t 2 < t 1 of elements of T . If for every pair (a, b), either a ≤ b or b ≤ a, then (T , ≤) is said to be totally ordered. A well-founded and totally ordered set is said to be a well-ordered set.

Let n be a positive integer, and T n the set of all ordered n-tuples over S. Let T = n≤1 T n . The lexicographical extension on T denoted by lex , is defined by: (

x 1 , . . . , x m ) lex (y 1 , . . . , y n ) if • m ≤ n and for all k ∈ [m], x k = y k , or I.e., (x 1 , . . . , xm) is a prefix of (y 1 , . . . , yn). • there is k ∈ [min(m, n)] such that for allj ∈ [k -1], we have x j = y j and x k ≺ y k (i.e., x k y k , x k = y k )
Example 4. The lexicographic order defined on a finite set of words is wellfounded. On the other hand, for S = {a, b} with a b, the lexicographical extension on the infinite product S * is not a well-order:

. . . aaab aab ab b.

Median normal forms

We now define a way to partially describe the structure of median terms that induces a well-order on the set of median formulas.

We then show that for every polynomial function, there exists a set of minimal representations with respect to this order, which we call median normal forms (MNF). As it is the case for DNF and CNF representations, this representation is unique modulo some properties like commutativity or associativity. However, the general structure of these minimal representations still eludes us.

Definition 1. Let φ be a median term of depth d. Let n 0 , . . . , n d be nonnegative integers, such that for all i ∈ {0} ∪ [d], n i is the number of medians at depth ≤ i. The structural representation of φ is the tuple

S φ = (n d , . . . , n 0 ).
Let ≤ S be the ordering of median formulas defined by:

φ 1 ≤ S φ 2 if S φ1 ≤ lex S φ2 .
Remark 2. Note that S φ is a decreasing sequence and that n d = |φ|. Also, the order ≤ S prioritizes the size of the formula over its depth. For instance, consider the following equivalent formulas

φ 1 = m(x 1 , x 2 , m(x 3 , x 4 , m(x 5 , x 6 , x 7 ))) φ 2 = m(m(x 1 , x 2 , x 3 ), m(x 1 , x 2 , x 4 ), m(x 5 , x 6 , x 7 )).
Clearly,

|φ 1 |= 3 < 4 = |φ 2 | while d(φ 1 ) = 3 > 2 = d(φ 1
). Looking at their structural representation, we have S φ1 = (3, 2, 1) whereas S φ1 = (4, 3),

and hence φ 1 ≤ S φ 2 .
We now give a definition of a median normal form as a minimal median representation.

Definition 2. We say that a median term φ is a median normal form (MNF) if for every median term φ ≡ φ, we have φ ≤ S φ .

Example 5. The formula φ = m(m(x, x, y), y, z) is not a median normal form since φ = m(x, y, z) is an equivalent formula, and

S φ = (1) ≤ lex (2, 1) = S φ .
Remark 3. As it has been defined, the structural order cannot account for permutations of variables. For instance, the formulas m(x, y, z) and m(x, z, y) have the same structural tuple (1), but they are also equivalent, and both are median normal forms. Thus, a formula does not have a single median normal form, but rather a set of median normal forms: the formula φ from Example 5 has for set of normal forms {m(x, y, z), m(x, z, y), m(y, z, x)}.

CONSIDERATIONS ON COMPLEXITY

In this section we address the question of finding median normal forms. To this end, we formalize two decision problems that express the tasks of finding median formulas of smaller structural representation. We show that both problems are at most moderately intractable, and we propose a term rewriting system as a tool for approximating solutions to them.

Structurally smaller formulas

Although, the definition of the median normal form is expressed simply, a procedure to convert an input formula into an equivalent formula in median normal form is likely intractable. Indeed, we will show that the mere task of checking if a given formula is in MNF seems to be expensive. We formalize this decision problem in Definition 3.

Definition 3. Consider the decision problem MONOTONE SMALLMED:

Input: a median term φ and a decreasing sequence S Output: succeeds if there exists a formula ψ equivalent to φ whose structural representation is strictly smaller than S. Fails if none exists.

Before proving that MONOTONE SMALLMED is intractable, we give a Σ P 2 upper-bound on its hardness. Recall that the Σ P 2 complexity class is on the second level of the polynomial hierarchy, between NP and PSPACE [START_REF] Savage | Models of computation: Exploring the power of computing[END_REF].

Theorem 2. MONOTONE SMALLMED is in the class Σ P 2 .

Proof. A convenient characterization of Σ P 2 is that it contains decision problems such that the accepting instances can be expressed as a set of words {x : ∃c 1 ∀c 2 F (x, c 1 , c 2 )}, where c 1 and c 2 are certificates whose lengths are polynomial in |x| and F is computable in polynomial time. Consider Algorithm 1 which solves MONOTONE SMALLMED. The size of the first certificate ψ, is indeed polynomial in the size of the input, |φ|, because its structural representation is bounded by that of φ. The size of the second certificate σ is also polynomial in the input. Therefore, Algorithm 1 ensures MONOTONE SMALLMED is in

Σ P 2 .
Algorithm 1 Finding a smaller equivalent median form.

Input: A formula φ, a decreasing sequence S.

1: Existentially guess a formula ψ such that S(ψ) < S

2:

Universally guess an assignment ς † 3:

Ensure that ς(φ) = ς(ψ)

4:
If so, return SUCCESS 5: If none exist, then FAIL Note that Theorem 2 simply provides an asymptotic upper bound on the complexity of MONOTONE SMALLMED, but a corresponding lower-bound still eludes us.

Definition 3 assumed that the desired formula size was given as part of the input. If instead we assume a constant target size, then it is possible to obtain a better complexity bound. Definition 4. For any fixed decreasing sequence S, we define the decision problem MONOTONE SMALLMED S as: Input: a median term φ Output: succeeds if there is a formula ψ equivalent to φ whose structural representation is smaller than S. Fails if none exists. Remark 4. Definition 4 is independent from any interpretation of the median formulas mentioned, in the sense that the objects manipulated are syntactic (i.e. median formulas and their structure). In fact, all results can be applied to, e.g., median representations of both lattice polynomials and monotone Boolean functions, since in both cases any function can be represented by a median formula (see, e.g., the definition of the set of median terms M above). In Remark 5 below (Section 6) we discuss equivalent decision problems related to, this time, the representation of Boolean functions. In that case, we consider a language where we allow negations. Theorem 3. For any decreasing sequence S, MONOTONE SMALLMED S is in the class co-NP.

Proof. Let s be the first element of the sequence S, n be the number of variables occurring in φ, and V φ be the set of variables occurring in φ. Any formula ψ of structural representation smaller than S, has no more than s medians. Hence, such a formula ψ cannot involve more than N = 2s + 1 variables. If φ is equivalent to a formula of structural representation smaller than S, then at most N variables among the ones that occur in φ are relevant.

For every subset of variables V ⊂ V φ of size at most N , there is a constant number of formulas smaller than S with variables drawn from V . For each such formula ψ, universally guess a variable assignment σ for the variables occurring in φ and check if φ and ψ agree on σ. If so, ψ is equivalent to φ and we can succeed. If no formula triggers a success, we can end the algorithm and fail.

The number of ways to specify the set V is bounded by n N . So the total number of universal guesses is bounded by O(n N ). Since N is constant, we conclude that we can determine if φ admits an equivalent formula of size smaller than S with a polynomial number of universal guesses. Therefore, MONOTONE SMALLMED S is in co-NP.

Algorithm 1 does not find an MNF for the input formula directly, but it can be used as a subroutine to an algorithm that does. Let φ be an input formula and let S φ be its structural representation, then a kind of binary search allows to identify the smallest structural representation such that Algorithm 1 succeeds. The output of the final call to Algorithm 1 is then an MNF of φ.

A binary search performs a number of comparison calls that is logarithmic in the size of the ordered domain. In our case, the domain is the set of sequences lexicographically smaller than S φ , and its cardinality is at most exponential in the size of φ. Therefore, the binary search performs a number of calls to Algorithm 1 that is polynomial in the input formula.

A term rewriting approach

A naive implementation of Algorithm 1 amounts to an exhaustive search for equivalent formulas among structurally smaller ones. A possible alternative would be to search for a structurally smaller formula among equivalent ones.

Recall from Theorem 1 that System 1 is sound and complete. In other words, for any two formulas φ and ψ, the formulas are equivalent if and only if there exists a rewriting of φ into ψ by means of a sequence of equations from System 1. This idea is implemented in Algorithm 2.

Algorithm 2 Bringing a formula closer to a median normal form. Input: A formula φ, a decreasing sequence S. Output: A formula ψ with structural representation S ψ < S, diverges if none exists.

1: Set ψ ← φ 2: While ψ ≥ S φ do 3:
Existentially guess a rewriting from System 1: ψ = ψ 4:

Update ψ ← ψ 5: return ψ This non-deterministic algorithm uses very little space, namely its space complexity is linear in the size of the input, and solves MONOTONE SMALLMED. In fact, MONOTONE SMALLMED is in the class NPSPACE, as this algorithm can be implemented in a Turing Machine using little space. However, it might not always stop and return a result.

From Savitch's theorem (see, e.g., [START_REF] Savage | Models of computation: Exploring the power of computing[END_REF]) we know that NPSPACE = PSPACE, but Σ P 2 is contained in PSPACE so Theorem 2 is stronger. We do not know whether Algorithm 2 is guaranteed to terminate in polynomial time, in the best case, when a structurally smaller formula exists. Indeed, equational reasoning to transform a formula into some smaller one may conceivably require an exponential number of rewriting steps. On the contrary, were Algorithm 2 to always terminate in polynomial time, it would constitute a proof of MONOTONE SMALLMED being in NP.

A solution to the problem of finding a derivation without unbounded searches is to orient the equations of the system using the order on the size of the formula: from bigger to smaller. As a result, applying any rule (except commutativity) to a formula will simplify it with regard to ≤ S : every derivation will be a simplification.

Let us then consider the following "term rewriting system" extracted from System 1 by orienting its equations according to the decreasing structural ordering.

System 2.

(R1) m(x, y, z) = m(x, z, y) = m(z, x, y),

(R2) m(x, x, y) -→ x, (R3) m(m(x, u, v), m(y, u, v), z) -→ m(m(x, y, z), u, v), (R4) m(⊥, , x) -→ x,
for all variables x, y, z, u, v in L.

The rewrite rule (R1), which is in fact (M 1), is kept the same, without orientation. Such systems are sometimes called rewriting systems modulo commutativity ( [START_REF] Baader | Term rewriting and all that[END_REF]). A similar situation takes place when dealing with systems that involve commutative binary operations like ∨ or ∧, and in such cases commutativity and associativity may be kept as equational rules. As explained in [START_REF] Veroff | First-order proof of a median algebra problem[END_REF], in the case of median terms, commutativity (M 1) can be oriented by defining a total order on terms. Some effects of this orientation are the sorting of the terms by the application of the now-oriented commutativity rules, as well as the occasional blockage of derivation proofs (in these cases we thus lose completeness of the system).

By orientating the rules, we can more easily test a derivation between formulas.

Lemma 1. Let φ and ψ be median formulas. If it exists, the derivation between φ and ψ is polynomial in the size of φ.

Proof. Every rewrite rule from System 2 save from the permutation (R1) removes a median m from any formula it is applied to. If such a derivation exists, necessarily φ has more medians than ψ. The derivation between φ and ψ thus contains n steps, with n being the difference between the number of medians in φ and the number of medians in ψ.

However, we may not be able to rewrite a formula into another equivalent one using System 2 (e.g., it is not possible to rewrite x into m(⊥, , x)), much less into a normal form. Example 6. Consider φ = m(m(m(x, y, z), u, v), y, z), which has for canonical form φ = m(m(x, u, v), y, z). No rule from System 2 can be applied to formula φ. Thus, it is not possible to simplify φ into φ . Let us now prove that φ = m(m(x, u, v), y, z) is the canonical form of φ (up to permutations). The proof of equivalence between the two formulas φ and φ is a particular case of a certain generalized rule we give hereafter. Recall that contexts are "terms" containing one occurrence of a special symbol , denoting an empty space. A context is generally denoted by C[ . ]. If t ∈ Ter(Σ) and t is substituted in , the result is

C[t] ∈ Ter(Σ); t is said to be a subterm of C[t]. The generalized rule is m z y C[m(x, y, z)] = m z y C[x]
with C a context. The proof of this rule lies in an induction on the depth of C.

The proof that φ ≡ φ can also be verified by comparing the truth tables of both formulas. Here we give an explicit derivation. Remark that some steps of this derivation require using some rules from System 2 in the reverse direction: the first and second steps, for instance, require using (R3) in reverse.

φ ≡ m(m(m(x, y, z), u, v), y, z) ≡ m(m(x, m(u, y, z), m(v, y, z)), y, z) ≡ m(m(m(u, y, z), y, z), m(m(v, y, z), y, z), x) ≡ m(m(u, y, z), m(v, y, z), x) ≡ m(m(x, u, v), x, y) ≡ φ .
Furthermore, φ cannot be rewritten into a smaller formula. Indeed, there are strictly more than 3 essential variables in φ : it is thus impossible to find a median formula of size 1 equivalent to it. Thus, φ is a median normal form for φ, yet is unreachable using System 2. Now, even though it is no longer complete, System 2 remains sound. Proposition 1. System 2 is sound but not complete.

Proof. Soundness follows from the fact that System 1 is sound (Theorem 1). Incompleteness follows from Example 6: the rule φ -→ φ , that is the rule m(m(m(x, y, z), u, v), y, z) -→ m(m(x, u, v), x, y), cannot be derived from the axioms of System 2.

EXTENSION TO THE NON-MONOTONIC CASE

In this section, we extend our results to the non-monotonic case, i.e., we now allow negations to appear in the median formulas. This allows us to represent all Boolean functions. Indeed, the set {m, .} is complete with regard to Boolean functions, that is, we can represent every Boolean function using medians and negations. Up to some adaptation of the equational specification to include the negation, most of the results and definitions given are similar to those of monotone Boolean functions. We thus recall most of the formalism of [START_REF] Couceiro | Median Based Calculus for Lattice Polynomials and Monotone Boolean Functions[END_REF].

Equational specification

We supplement System 1 with two rules in order to deal with negated variables and negated terms.

System 3. (B1) m(x, y, z) = m(x, z, y) = m(z, x, y), (B2) m(x, x, y) = x, (B3) m(m(x, u, v), m(y, u, v), z) = m(m(x, y, z), u, v), (B4) m(y, y, x) = x, (B¬) m(x, y, z) = m(x, y, z), for all x, y, z, u, v in {0, 1}.
Remark that rule (M 4) of System 1, namely that m(⊥, , x) = x, can be derived from rule (B4) of System 3. The propagation rule (B¬) in particular allows us to only consider literals, that is, variables and negated variables, in median formulas. For instance, the formula m(x 1 , x 2 , x 3 ) can be equivalently rewritten into the formula m(x 1 , x 2 , x 3 ).

Just as for monotone Boolean functions, in order to rewrite a median formula into any equivalent other, we need a sound and complete system with regard to Boolean functions. In fact, System 3 is both sound and complete. These properties stem the soundness and completeness of System 1 for monotone Boolean functions.

Theorem 4. The algebra < B, m, ., 0, 1 > together with the axioms of System 3 is sound and complete.

Extension of MNFs and corresponding complexity

In this section, we adapt the notions introduced in Section 4 in order to manipulate Boolean functions. As the notions are exactly the same for both monotone and arbitrary Boolean functions, we keep the same terminology. Definition 5. We denote the set of median terms (median expressions, median formulas) by M. It is the set of all formulas that are constructed using constants, variables, negated variables, and the median m. Given a median term φ of depth d, let n 0 , . . . , n d be nonnegative integers such that for all i ∈ {0} ∪ [d], n i is the number of medians in φ at depth i. The structural representation of φ is the tuple

S φ = (n d , . . . , n 0 ).
Similarly to the case of monotone functions, we can compare median terms given an ordering ≤ S : φ 1 ≤ S φ 2 if S φ1 ≤ lex S φ2 . As this is a well-order on a finite set of formulas, given a median term, we can consider its set of median normal forms. Definition 6. We say that a median term φ is in median normal form (MNF) if for every median term φ ≡ φ, we have φ ≤ S φ .

Given our previous results on monotone Boolean functions, a natural question arises. Let f be a monotone Boolean function and φ its median normal form. Does allowing ¬ in our language allow us to give a representation of f in median normal form smaller than φ?

It is straightforward that, given two minimal representations φ and φ ¬ of the same monotone function in which negations are not allowed and negations are allowed, respectively, then |φ ¬ |≤ |φ|, with equality when φ ¬ = φ.

Surprisingly, in certain cases the comparison can be strict. In other words, some monotone functions may have representations that are strictly smaller with negations than without. Proposition 2. There exists a monotone Boolean function f such that |φ ¬ |< |φ|, with φ ¬ and φ the minimal representations of f with and without negations, respectively.

Proof. Consider the two median formulas

φ = m(y, m(u, v, t), m(x, z, m(u, v, t))), φ ¬ = m(x, m(x, y, z), m(u, v, t)).
Remark that |φ|= 4 and |φ ¬ |= 3. First, we will prove that φ ≡ φ ¬ . One might verify by computing the truth tables of both formulas, or use the following derivation, that requires using the rule (B3) in reverse and the propagation rule (B¬):

φ ¬ = m(x, m(x, y, z), m(u, v, t)) ≡ m(y, m(m(u, v, t), x, x), m(x, z, m(u, v, t))) ≡ m m(y, m(u, v, t), m(x, z, m(u, v, t))) = φ.
Second, we will prove that φ is the smallest representation equivalent to φ ¬ , up to permutations and without negations. As the space of smaller formulas is finite, we have verified that no smaller formula equivalent to φ without negation exists by an automated exhaustive search. Here we give a formal proof of this fact. Suppose there exists a smaller formula φ that does not contain negations and is strictly smaller than φ. The idea behind the proof is to exhibit a tuple (sometimes called an assignment in this proof) X such that φ (X) = φ ¬ (X).

Remark that |φ |= 3 because all variables are essential in φ: its essential arity is 6, but median formulas of size 2 have at most an essential arity of 5. Without loss of generality φ may follow two different structures (cases (a) and (b) below). Furthermore, φ may either contain two repeated variables, or one constant. In the rest of the proof we will produce assignments φ ¬ and φ do not agree on. Consider the assignments:

• X: x, y, u = 1 and v, t, z = 0;

• Y : u, y, z = 1 and v, t, x = 0;

• Z: v, u, t = 1 and x, y, z = 0.

Each of these assignments are false points for φ ¬ .

1. First, suppose that there are no constants in φ .

(a) Suppose that φ = m(x 1 , m(x 2 , x 3 , x 4 ), m(x 5 , x 6 , x 7 )). There is a repeated variable; if x 2 = x 3 or x 2 = x 4 , then φ can be simplified further into m(x 1 , x 2 , m(x 5 , x 6 , x 7 )), of essential arity at most 5, with the majority rule (B2). A similar reasoning ensures that, without loss of generality ‡ , either

x 1 = x 2 or x 2 = x 5 . i. suppose that x 1 = x 2 .
A. if x is the variable that is repeated, then given the assignment X we have φ (X) = 1. ‡ Because the median is symmetric.

2. Second, suppose that there is a constant in φ . In particular no variable is repeated.

(a) Suppose that φ = m(x 1 , m(x 2 , x 3 , x 4 ), m(x 5 , x 6 , x 7 )), such that either x 1 , . . . , x 7 is a constant.

i. If this constant is 1, then all tuples of weight at least 3 are true points of φ , but there are false points of φ ¬ of weight 3.

ii. Suppose this constant is 0.

A. If x 1 = 0, then φ ≡ m(x 2 , x 3 , x 4 ) ∧ m(x 5 , x 6 , x 7 ).
Any tuple of weight 3 is a false point for this function, but there are true points of φ ¬ of weight 3.

B. Suppose that x 2 = 0 (equivalently for all remaining cases). If x 1 = x then the assignment x, y, u = 0, z, v, t = 1 is a true point for φ ¬ but not for φ ; the same assignment is adequate for the cases x 1 = y (equivalently z) and x 1 = u (equivalently v, t).

(b) Suppose that φ = m(m(m(x 1 , x 2 , x 3 ), x 4 , x 5 ), x 6 , x 7 ), such that either x 1 , . . . , x 7 is a constant.

i. Suppose this constant is 1. Remark that there is no tuple X of size 2 such that φ ¬ (X ) = 1; however, no matter where 1 occurs in φ (either x 7 = 1 or x 5 = 1 or x 3 = 1) one can produce assignments X of weight 2 such that φ (X ) = 1.

For instance, if x 7 = 1 then one can consider the assignment x 4 = 1, x 5 = 1, x i = 0 for i = 4, 5.

ii. Suppose this constant is 0. Remark that there is no tuple X of size 4 such that φ ¬ (X ) = 0; however, no matter where 0 occurs in φ (either x 7 = 0 or x 5 = 0 or x 3 = 0) one can produce assignments X of weight 4 such that φ (X ) = 0.

Thus, there is no median formula φ strictly smaller than φ and such that φ ≡ φ and such that φ does not contain negated variables.

This fact raises further questions to be investigated in the future. For instance, the problem of finding a general description, that is, that holds for representations of both monotone and non-monotone functions, of median normal forms remains open.

Another question of interest is whether the corresponding decision problems SMALLMED B and SMALLMED B S , that are the problems SMALLMED and Deciding whether two formulas are equivalent using System 3 thus remains a complex problem. As an illustration of this fact, remark that to prove the rule m(m(m(x, y, z), u, v), y, z) -→ m(m(x, u, v), x, y), by rewriting the left-hand side into the right-hand side using System 3, one needs to apply a rule that increases the size of the formula; c.f., Proposition 1. Remark 6. Just as for monotone Boolean functions in Section 5.2, in order to simplify the search for a derivation between formulas, we may consider a term rewriting system instead of a full equational specification, extracted from System 3 by orienting its equations according to the decreasing structural ordering. Even though System 4 is also no longer complete, like System 2, it remains sound.

CONCLUSION AND FUTURE WORK

In this paper, we discussed a median-based formalism to efficiently represent monotone Boolean functions as well as polynomial functions over distributive lattices. To this end, we propose median normal forms defined as being median expressions that are minimal with respect to a structural ordering of formulas.

We also formalized the problem of finding median formulas of smaller structural representation and investigated its computational complexity. This task turns out to be at most moderately intractable. In fact, we showed that the corresponding decision problem, that is, falls into Σ P 2 or co-NP according to whether the structural representation is given as part of the input. However, the question of determining corresponding complexity lower bounds remains open.

Furthermore, a natural generalization of the results to arbitrary Boolean functions, i.e. by allowing negated variables to appear in our formalism. A surprising result (Proposition 2) is that in certain cases allowing negated variables allows formulas that are strictly smaller than if negation hadn't been allowed. These and other complexity questions concerning decision problems that appear naturally in this median-based formalism are to be investigated in forthcoming collaborations.

Other connectives have been considered in [START_REF] Couceiro | Péchoux Comparing the efficiency of normal form systems to represent Boolean functions[END_REF] such as the Sheffer stroke x ↑ y ≡ ¬x ∧ ¬y, or the generator of monotone constant-preserving clique functions, u(x, y, z) ≡ (x ∨ y) ∧ z. These connectives share with the median the property of being quasi-Sheffer, that is, any Boolean function can be represented using a composition of one of these connectives, literals, and constants. We will investigate similar questions to those considered in this paper, such as the definition of normal forms with regard to these connectives, the definition of a sound and complete equational specification with the goal of simplifying formulas, or the complexity of related decision problems.

Example 1 .

 1 If φ = m(m(x, x, y), m(x, y, z), v) then d(φ) = 2 and |φ|= 3.

System 4 .

 4 (R1) m(x, y, z) = m(x, z, y) = m(z, x, y),(R2) m(x, x, y) -→ x, (R3) m(m(x, u, v), m(y, u, v), z) -→ m(m(x, y, z), u, v), (R4) m(⊥, , x) -→ x, (R5) m(y, y, x) -→ x, (R¬)m(x, y, z) -→ m(x, y, z),for all variables x, y, z, u, v in B.

  SMALLMED S , generalized to all Boolean functions (not just monotone), are in the same complexity classes as SMALLMED and SMALLMED S . Definition 7. Consider the decision problem SMALLMED B : Input: a median term φ (that represents a Boolean function) and a decreasing sequence S Output: succeeds if there exists a formula ψ equivalent to φ whose structural representation is strictly smaller than S. Fails if none exists. Theorem 5. SMALLMED B is in the class Σ P 2 . Proof. The proof is the same as for MONOTONE SMALLMED; remark that Algorithm 1 also solves SMALLMED B . Remark 5. As in Remark 4, the definition of SMALLMED B is independent from the objects that are represented, namely, Boolean functions.

† The assignment ς in Algorithm 1 refers to the standard interpretation of variables and symbols in the formula φ as Boolean variables and Boolean functions.

B. if y is the variable that is repeated (or equivalently, z), then given the assignment X we also have φ (X) = 1.

C. if u is the variable that is repeated (or equivalently, v or t) then given the assignment X we also have φ (X) = 1.

ii. Suppose that x 2 = x 5 .

A. if x is the variable that is repeated, then given the assignment X we have φ (X) = 1.

B. if y is the variable that is repeated (equivalently, z), then

C. if u is the variable that is repeated (equivalently, v or t)

). The reasoning is similar to the one above. The possibilities for repeated variables are, without loss of generality,

i. Suppose that x 1 = x 3 .

A. if x is repeated (x = x 1 ), X is a suitable assignment, that produces a clash: φ (X) = φ ¬ (X).

B. if y is repeated, then X is a suitable assignment.

C. if u is repeated, then X is a suitable assignment.

ii. Suppose that x 1 = x 5 .

A. if x is repeated, then X is a suitable assignment.

C. if u is repeated, then if x = x 3 or y = x 3 then X is a suitable assignment; else, if z = x 3 then Y is a suitable assignment.

iii. Suppose that x 3 = x 5 .

A. if x is repeated, then X is a suitable assignment.

B. if y is repeated, then if x = x 7 or u = x 7 then X is a suitable assignment; else, if z = x 7 then Y is a suitable assignment.

C. if u is repeated, then X is a suitable assignment.


David Delahaye
email: david.delahaye@inria.fr2.micaela.mayero@inria.fr

Micaela Mayero

Journées Francophones des Langages Applicatifs JFLA01 Field: une procédure de décision pour les nombres réels en Coq

Nous nous proposons d'automatiser les preuves d'égalités sur les nombres réels dans le système

Coq en utilisant la théorie des corps commutatifs. L'idée de l'algorithme consiste à se débarrasser des inverses an de pouvoir se brancher sur la procédure de décision déjà existante sur les anneaux abéliens (Ring). L'élimination des inverses se fait de manière complètement réexive et la réexion est réalisée au moyen d'un nouveau langage de tactiques intégré au système Coq (version V7).

Nous pensons étendre cette tactique à tous les corps commutatifs bien qu'actuellement, seuls les nombres réels soient concernés.

1.

Introduction

La théorie des nombres réels dans le système Coq est axiomatique [START_REF] Barras | The Coq Proof Assistant Reference Manual Version 6[END_REF] et les preuves se font à grand renfort de réécritures [START_REF] Boutin | Réexions sur les quotients[END_REF] , ce qui fait grossir la taille des scripts ainsi que les termes preuves. La tactique Ring qui permet de décider d'égalités sur les anneaux abéliens a permis de résoudre partiellement ce problème et se révèle très utile dans les preuves ne faisant pas intervenir l'inverse. On peut l'utiliser dans des théorèmes auxiliaires triviaux servant à compléter la théorie comme : ∀x, y ∈ R.x + y = 0 → y = (-x) où pas moins de cinq réécritures sont nécessaires pour résoudre sans la tactique Ring. Mais, on peut aussi l'utiliser dans des théorèmes non triviaux où l'inverse n'intervient pas, comme le théorème des 3 intervalles ( [11]).

Cependant, Ring ne règle pas le cas des égalités avec inverses qui, si elles ne sont pas diciles à montrer, n'en restent pas moins très fastidieuses à résoudre. Ces preuves sont d'autant plus pénibles à construire qu'elles ralentissent de manière conséquente le développement de la théorie des nombres réels. En eet, les théorèmes sur les limites et les dérivées font systématiquement intervenir des égalités avec des inverses dans les "preuves ε"3 lorsque l'on veut composer, additionner, ... Ces égalités sont relativement triviales et alourdissent considérablement les preuves fondamentales de limites et de dérivées. Un exemple typique est celui de la dérivée de l'addition où l'on doit montrer que la somme des dérivées est égale à la dérivée de la somme. Pour ce faire, on prend deux fonctions f et g ainsi que leurs dérivées en x0, c'est-à-dire f (x0) et g (x0). Par dénition, les deux dérivées peuvent s'exprimer comme suit :

f (x0) = lim x→x 0 f (x) -f (x0) x -x0 g (x0) = lim x→x 0 g(x) -g(x0)
x -x0 En utilisant le théorème d'addition des limites, on obtient directement :

f (x0) + g (x0) = lim x→x 0 f (x) -f (x0)
x -x0 + g(x) -g(x0)

x -x0

En utilisant la dénition de la limite, on a pour tout domaine D de R :

∀ε > 0, ∃α > 0, ∀x ∈ D\x0, si |x -x0| < α alors f (x) -f (x0) x -x0 + g(x) -g(x0) x -x0 -(f (x0) + g (x0)) < ε
Maintenant, il sut de montrer l'égalité suivante :

f (x) -f (x0) x -x0 + g(x) -g(x0) x -x0 = f (x) + g(x) -(f (x0) + g(x0))
x -x0 pour conclure que f (x0) + g (x0) et (f + g) (x0) coïncident. Cette dernière égalité est clairement triviale mais la preuve formelle l'est beaucoup moins [START_REF] Delahaye | A Tactic Language for the System Coq[END_REF] . Il faut d'abord réduire au même dénominateur (4 réécritures) puis montrer l'égalité sur les numérateurs (6 réécritures). L'utilisation de Ring sur les numérateurs économise des réécritures et au total, cette égalité nécessite 4 réécritures + 1 tactique (Ring). Nous pensons que ce genre d'égalité doit être résolue directement par une tactique, à la fois pour un gain de temps considérable dans les développements mais aussi de concision dans les scripts où l'on a plutôt envie de rendre implicites de telles preuves.

Dans ce papier, nous présenterons, tout d'abord, l'algorithme que nous avons utilisé pour décider les égalités sur les corps commutatifs (sur R en particulier) modulo certaines inégalités (conditions que les dénominateurs doivent être non nuls). Ensuite, nous donnerons une idée assez globale de l'implantation qui se fait de manière totalement réexive et qui utilise des spécicités propres à la version V7 de Coq, à savoir le langage de tactiques. Enn, nous nous appuierons sur plusieurs exemples, faciles pour certains et plus réalistes pour d'autres an de mettre en évidence la correction de la tactique ainsi que ses performances.

Algorithme

Principe

L'idée de l'algorithme est de minimiser les opérations de simplication de manière à se brancher le plus tôt possible sur la procédure de décision sur les anneaux abéliens (Ring). Cela signie qu'il faut éliminer tous les inverses intervenant dans l'égalité qu'il s'agit de résoudre.

Pour ce faire, nous proposons la suite d'étapes suivantes : Transformer les expressions x -y en x + (-y) et x/y en x * 1/y. Chercher tous les inverses apparaissant dans l'égalité pour en faire un produit. Distribuer totalement à gauche et à droite de l'égalité, excepté dans les inverses. Associer à droite chaque monôme, excepté dans les inverses [START_REF] Gabbay | The Undecidability of Intuitionnistic Theories of Algebraically Closed Fields and Real Closed Fields[END_REF] . Multiplier à gauche et à droite par le produit d'inverses, que l'on a construit précédemment, en générant la condition que tous les inverses doivent être non nuls.

Distribuer seulement le produit sur la somme de monômes à gauche et à droite sans réassocier à droite. Éliminer les inverses des monômes en utilisant la règle de corps x.1/x = 1, si x = 0 et en permutant les éléments du monôme si nécessaire, c'est-à-dire s'il reste des inverses et que la règle de corps ne peut pas s'appliquer [START_REF] Geuvers | Equational Reasoning via Partial Reection[END_REF] . Recommencer le processus s'il reste encore des inverses. La dernière étape qui consiste à réitérer le processus s'explique par le fait qu'il peut y avoir d'autres inverses dans les inverses et ce, dans des expressions pouvant être compliquées. Pour éviter la réitération, une idée serait de se lancer dans une simplication directe en utilisant la règle 1/1/x = x, si x = 0. Toutefois, l'expérience a montré que le codage de cette simplication était plutôt complexe et générait un lemme de correction dicile. Par ailleurs, les expressions devant être diérentes de 0 n'étaient pas exactement les mêmes que celles nécessaires pour l'élimination des inverses dans les monômes. On pouvait certes les déduire mais le lemme de correction correspondant à l'élimination des inverses devenait alors plus compliqué à montrer. On a donc tout avantage à se limiter à la règle x.1/x = 1, si x = 0 qui tend à simplier grandement l'algorithme et ce pour une perte d'ecacité négligeable en pratique [START_REF] Harrison | Metatheory and Reection in Theorem Proving : a Survey and Critique[END_REF] .

Après ces étapes, nous obtenons une expression débarrassée de tous ses inverses et il sut d'appeler Ring pour conclure.

Exemple

Considérons un petit exemple en détaillant les étapes de preuve an de voir comment la procédure fonctionne ; étant donné x et y, deux variables réelles, on se propose de montrer l'égalité suivante :

x * ( 1 x + x x + y ) = (- 1 y ) * y * (-( x * x x + y ) -1)
On commence par transformer les moins binaires et les divisions :

x * ( 1 x + x * 1 x + y ) = (- 1 y ) * y * (-(x * x) * 1 x + y + (-1))
On construit le produit d'inverses que l'on appellera p :

p = x * ((x + y) * (y * (x + y)))
On distribue totalement à gauche et à droite sauf dans les inverses :

x * 1 x + x * 1 x + y = (-1) * 1 y * y * ((-1) * (x * x) * 1 x + y ) + (-1) * 1 y * (-1)
On associe à droite chaque monôme sauf dans les inverses :

x * 1 x + x * 1 x + y = (-1) * ( 1 y * (y * ((-1) * (x * (x * 1 x + y ))))) + (-1) * ( 1 y * (-1))
On multiplie à gauche et à droite par p en générant la condition de correction :

(x * ((x + y) * (y * (x + y)))) * (x * 1 x + x * 1 x + y ) = (x * ((x + y) * (y * (x + y)))) * ((-1) * ( 1 y * (y * ((-1) * (x * (x * 1 x + y ))))) + (-1) * ( 1 y * (-1)))
Avec x * ((x + y) * (y * (x + y))) = 0.

On distribue ce produit sur les monômes sans réassocier à droite :

(x * ((x + y) * (y * (x + y)))) * (x * 1 x )+ (x * ((x + y) * (y * (x + y)))) * (x * 1 x + y ) = (x * ((x + y) * (y * (x + y)))) * (((-1) * ( 1 y * (y * ((-1) * (x * (x * 1 x + y ))))))+ (x * ((x + y) * (y * (x + y)))) * ((-1) * ( 1 y * (-1)))
On élimine les inverses en permutant si nécessaire :

((x + y) * (y * ((x + y)))) * x + (x * (y * (x + y))) * x = (x * (x + y)) * ((-1) * (y * ((-1) * (x * x)))) + (x * ((x + y) * (x + y))) * ((-1) * (-1))
On obtient alors une égalité sur les anneaux abéliens que Ring sait résoudre.

Remarques

Nous n'avons pas encore formalisé la preuve que cet algorithme décide bien des égalités sur les nombres réels et sur les corps commutatifs plus généralement modulo certaines preuves d'inégalités. Il semble clair, cependant, qu'il est correct dans la mesure où l'on n'utilise que des axiomes de corps. On peut également se convaincre de la terminaison de la procédure puisque le nombre d'inverses décroît à chaque étape.

Par ailleurs, il est important de souligner que notre démarche ne vise pas à résoudre le problème global de décision sur les corps commutatifs dont on ne sait pas, a priori, s'il est décidable ou non. En eet, nous ne cherchons pas à prouver les conditions sur les inverses qui sont laissées à l'utilisateur. Ainsi, nous nous plaçons dans une optique où l'inverse est une fonction totale. Dans un souci de généralité, notre méthode a pour vocation, à terme, de traiter tous les corps commutatifs. Si on avait voulu traiter seulement les nombres réels, notre approche aurait été bien diérente et on aurait certainement opté pour des algorithmes résolvant au premier ordre tels que, entre autres, la méthode de Tarski8 ( [12]), l'algorithme de Kreisel-Krivine9 ([9]) ou la décomposition cylindrique de Collins ([3]).

Toujours dans cette optique plus générale, on peut citer le travail du projet Fundamental Theorem of Algebra (Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack et Henk Barendregt), avec, dans le cadre d'une axiomatisation constructive des nombres réels en Coq, le codage de la tactique réexive Rational ( [6]), traitant des égalités similaires à celles que nous nous proposons de résoudre. Notre approche se démarque essentiellement du fait de choix diérents dans la formalisation des nombres réels. Tout d'abord, le fait que la fonction inverse soit totale permet de faire une réexion totale des expressions de R ce qui n'est pas le cas dans Rational où tout inverse contient aussi la preuve que le dénominateur est non nul. La réexion doit donc aussi être partielle ce qui rend le processus plus complexe. Enn, nous considérons l'égalité de Leibniz, ce qui permet à l'utilisateur d'appliquer des tactiques de réécriture à n'importe quel prédicat alors que dans Rational, l'égalité est plus large (setoïde) et il est nécessaire de prouver des lemmes de compatibilité an de passer au contexte.

Implantation

Comme nous l'avons dit précédemment, l'implantation de cette procédure de décision sur les nombres réels, que nous avons appelée Field, a été réalisée dans la version V7 de Coq an de pouvoir proter des nouvelles possibilités du langage de tactiques. Bien que la version V7 de Coq soit encore très expérimentale et, de ce fait, non disponible, le code de ce développement peut être récupéré en ligne à l'adresse suivante : ftp ://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/Field/Field.v

À propos de la réexion

Pour coder Field, il y a globalement deux choix possibles. Un codage explicite en utilisant la réécriture ou un codage par réexion en utilisant la réduction. Le codage explicite (approche à la LCF) est très coûteux du fait de l'utilisation de la réécriture qui prend du temps mais aussi et surtout de la place dans le terme preuve [START_REF] Leroy | The Objective Caml system release 3.00[END_REF] . Le codage par réexion est une alternative complètement satisfaisante pour laquelle nous avons opté. En eet, les réécritures sont remplacées par des phases de réduction plus ecaces et la taille du terme preuve est de l'ordre de celle du but à résoudre. Par ailleurs, on peut formaliser clairement la correction globale de la tactique ainsi que sa complétude (même si nous ne l'avons pas fait ici) alors que dans l'approche explicite, c'est bien plus dicile, voire impossible.

Avant de donner une idée de l'implantation de Field, rappelons rapidement le principe d'une tactique codée par réexion. Soit un langage C des termes concrets (typiquement un type quelconque) et un langage A des termes abstraits (typiquement un type inductif). Comme on ne peut pas manipuler les termes du langage C comme on voudrait (on ne peut pas ltrer), l'idée est de le rééchir dans le langage A qui lui est isomorphe. Une première phase, appelée métaication par Samuel Boutin ( [2]), consiste donc à traduire les termes de C vers les termes de A. Plus précisément, cela consiste, pour un terme c de C, à trouver le terme a de A tel que (f v a) = c, où f est la fonction d'interprétation de A vers C (codable dans Coq), v est une liste d'associations contenant les parties de C que l'on ne rééchit pas (atomes) et = est l'égalité de Leibniz. On peut se passer de la liste d'associations à condition que l'égalité sur les atomes soit décidable car on a généralement besoin de comparer les termes de A. La métaication s'assimile exactement à une phase d'analyse syntaxique comme on pourrait la trouver dans un langage de programmation.

Ensuite, on peut coder la fonction t de transformation des termes de A. Pour l'utiliser, il sut de prouver un lemme de correction [START_REF] Mayero | The Three Gap Theorem (Steinhauss Conjecture)[END_REF] de la forme :

∀a ∈ A.(f v (t a)) = (f v a)
Enn, après avoir appliqué ce lemme de correction, il sut de réduire totalement (Compute) pour transformer le terme abstrait (de A) et revenir à un terme concret (de C). Pour pousser l'analogie avec les langages de programmation, on pourrait voir ces deux étapes comme une phase d'évaluation suivie d'une phase de "pretty-print".

On peut résumer la situation au moyen du schéma suivant :

C - Métaication A ? Codage explicite C A f ? t

Réexion

Pour une description complète de la réexion, on pourra se reporter à [2] et [7].

Codage de la tactique

Nous allons maintenant entrer dans les détails de l'implantation de l'algorithme donné précédemment. Nous utiliserons une syntaxe spécique au langage Coq dont on pourra trouver une documentation complète dans [1]. Les seules spécicités de la version V7, que nous utiliserons, concernent le langage de tactiques. On pourra consulter [4] Les variables sont des expressions réelles quelconques pour lesquelles on ne peut clairement pas décider l'égalité. On les remplace donc par des indices entiers (nat) pour pouvoir décider l'égalité entre variables et on associe à un terme une liste d'associations entre les indices et les expressions de R.

Métaication

Pour traduire les expressions de R vers ExprR (métaication), il faut utiliser le métalangage de Coq. Jusqu'à la V7 exclue, le seul moyen était de coder cette traduction dans Objective Caml (le langage d'implantation et le métalangage de Coq, [10]) en utilisant un chier ML que l'on compilait avec le système et que l'on pouvait importer dans un toplevel bytecode de Coq. Ce protocole était un peu lourd à mettre en ÷uvre [START_REF] Tarski | A Decision Method for Elementary Algebra and Geometry[END_REF] où Assoc est une tactique qui donne l'indice correspondant à la variable réelle. À ce niveau là, on suppose que les constantes Rminus et Rdiv, à savoir respectivement les constantes du moins binaire et de division, ont déjà été dépliées.

Construction du multiplicateur

Ici, il s'agit de construire un produit de facteurs sans doublons inutiles (doublons qui apparaîtront entre monômes après distribution), constitué des inverses de l'égalité (on ne prend pas en compte les inverses dans les inverses qui seront traités dans d'autres passes de Field). Pour ce faire, on a le choix entre utiliser une fonction de Coq ou une tactique que l'on peut plus facilement écrire dans la V7. Pour des raisons d'aisance de programmation, nous avons opté pour une tactique puisque l'on est moins limité, entre autres, dans la récursivité. Le multiplicateur nous est donc donné par la tactique GiveMult utilisant la tactique RawGiveMult qui donne la liste des inverses : 13 En eet, le chargement dynamique de chiers bytecode dans un exécutable natif n'est pas encore très standard et le chargement dynamique de chiers natifs dans du natif n'est, quant à lui, clairement pas compris. La commande coqmktop permet de créer un toplevel "customisé" éventuellement en natif en indiquant une liste de chiers à inclure au moment de l'édition de liens. Toutefois, le processus est purement statique et on perd la possibilité d'appeler d'autres tactiques qui n'ont pas été "linkées" au moment du coqmktop. (e:ExprR)(lvar:(list (Sprod R nat))) (interp_ExprR lvar (assoc e))==(interp_ExprR lvar e).

Après avoir appliqué distrib et assoc, on obtient à gauche et à droite de l'égalité à prouver, deux termes qui sont des sommes de monômes associés à droite.

Multiplier les membres de l'égalité

Pour pouvoir eectuer la simplication des inverses, on multiplie ensuite par le multiplicateur qui a été construit précédemment (produit de tous les inverses excepté ceux qui sont dans d'autres inverses). Pour ce faire, il sut de montrer le lemme suivant sur les expressions de ExprR et qui a directement son équivalent dans R : Lemma mult_eq:

(e1,e2,a:ExprR)(lvar:(list (Sprod R nat))) ~((interp_ExprR lvar a)==R0)-> (interp_ExprR lvar (ERmult a e1))==(interp_ExprR lvar (ERmult a e2))-> (interp_ExprR lvar e1)==(interp_ExprR lvar e2).

Ce lemme permet de générer le but (que l'utilisateur devra prouver) que le multiplicateur doit être non nul. Ceci équivaut à dire que tous ses facteurs doivent être nuls ce qui est cohérent dans la mesure où l'on est sûr de devoir simplier ces expressions.

Une fois le produit eectué, on distribue ce produit sur les monômes sans réassocier à droite, ce qui est trivialement fait par une fonction Coq appelée multiply dont le lemme de correction est complètement similaire à ceux donnés précédemment pour la distributivité et l'associativité.

Élimination des inverses

L'élimination des inverses se fait monôme par monôme. À ce stade, un monôme est un produit du multiplicateur et d'une expression qui est un produit associé à droite (monôme obtenu après la phase de distributivité et d'associativité). Étant donné que la simplication doit se faire modulo permutation des membres du monôme (de manière à faire apparaître x.1/x), le plus simple consiste à manipuler des listes. On transforme donc le multiplicateur en une liste lp et le reste du monôme en une liste lm. Pour que les simplications soient correctes, il faut considérer une troisième liste ln qui est une liste d'expressions de ExprR non nulles (diérentes de ER0). Ainsi, l'algorithme de simplication consiste à parcourir lp et pour chaque élément de lp, s'il est dans ln et que son inverse est dans lm alors enlever l'inverse de lm sinon on rajoute cet élément à la n de lm. Finalement, on rend lm que l'on retransforme en monôme. Dans notre cas, on aura toujours lp = ln puisque les expressions du multiplicateur sont exactement les expressions que l'on va simplier. où list_of_monom et monom_of_list permettent respectivement de transformer un monôme en une liste de ses facteurs et une listes d'expressions en un monôme. remove_list réalise exactement l'algorithme que l'on vient de donner avec ln=l, lp=l1 et lm=l2. inverse est la fonction, qui étant donnée une expression, rend son inverse. Elle permet de tester si l'inverse d'un élément de l1 est bien dans l2.

Le lemme de correction d'élimination des inverses s'exprime comme suit :

Lemma inverse_correct: (e:ExprR)(l:(list ExprR))(lvar:(list (Sprod R nat)))(make_mult lvar l)-> (interp_ExprR lvar (inverse_simplif l e))==(interp_ExprR lvar e).

où make_mult génère la condition que l'interprétation du produit des expressions de l doit être non nulle (diérente de R0). Cette condition permet d'assurer la correction des simplications et ce pour tout l. Pour appliquer ce lemme et comme on l'a dit précédemment, on utilisera la liste des facteurs du multiplicateur pour l. La première ligne de Field (série d'Unfold) permet de déplier les moins binaires et les divisions. Ensuite, on crée la liste d'associations des variables (dans lvar) avec BuildVarList pour interpréter les deux membres de l'égalité, ce qui donne deux termes trm1 et trm2 de ExprR. Le multiplicateur mul est donné par GiveMult en prenant soin de sommer les deux termes pour tenir compte des inverses des deux membres de l'égalité. On transforme alors le multiplicateur en une liste de facteurs au moyen de list_of_mult, qui sera donnée au lemme de correction concernant l'élimination des inverses. Le Cut permet d'insérer les termes de ExprR dans le but à prouver. Par la suite, on peut leur appliquer les diérentes transformations dont nous avons parlé précédemment au moyen de tactiques. ApplyDistrib applique la distributivité, ApplyAssoc l'associativité, Multiply la multiplication par le multiplicateur à gauche et à droite de l'égalité, ApplyMultiply la distribution du multiplicateur et ApplyInverse l'élimination des inverses. ApplySimplif permet d'appliquer la tactique à gauche et à droite de l'égalité pour les tactiques qui travaillent sur un terme. On se débarrasse de l'hypothèse que l'interprétation du multiplicateur doit être non nulle au moyen de GrepMult, qui rend le nom de cette hypothèse pouvant être ainsi eacées (Clear). Enn, on teste s'il reste encore des inverses dans les termes de l'égalité grâce à la tactique InverseTest qui, soit ne fait rien s'il ne reste pas d'inverses permettant ainsi l'appel à Ring, soit échoue dans le cas contraire impliquant une nouvelle application de Field.

Exemples

Nous donnons ici quelques exemples, accompagnés du temps d'exécution. Ces exemples sont tirés de preuves faisant partie ou allant faire partie du développement14 des nombres réels où l'utilisation de cette tactique sera la bienvenue (autant par commodité que dans le but d'alléger les preuves).

Les tests sont eectués sur un Pentium III à 450Mhz sous Linux (RedHat 5.

Exemple 4

Nous nous intéressons ici aux preuves concernant les séries entières, utilisées pour dénir les fonctions transcendantes (en cours de développement) telles que exp , sin ou cos .

Considérons, par exemple, l'application du critère de d'Alembert à la fonction exponentielle. Rappelons, avant tout, les dénitions d'une série entière, de la fonction exponentielle ainsi que l'énoncé du critère de d'Alembert.

Une série entière réelle est une série de la forme : Après quelques tests rapides, nous avons éliminé des sources potentielles d'inecacité et isolé quelques causes probables. La perte de temps a lieu au sein des fonctions Coq et n'est donc pas due au métalangage. Les fonctions chargées de distribuer tous les termes (exponentielle en le nombre de noeuds de l'expression distribuée) an d'obtenir des monômes ainsi que la fonction de simplication des inverses semblent être les principales mises en cause. En particulier, l'algorithme de simplication des inverses, utilisant deux listes non triées, peut certainement être optimisé en eectuant un tri préalable. Néanmoins, des tests plus poussés doivent être eectués, car l'optimisation de ces deux fonctions ne réduirait, au maximum, le temps d'exécution que d'environ 30%.

Conclusion

Synthèse

La tactique Field contribue grandement au développement de la théorie des nombres réels en Coq. Elle permet une économie de temps précieux ainsi qu'un gain non négligeable de concision dans les scripts de preuves. Par ailleurs, étant intégralement réexive, elle permet la construction de termes preuves plus petits que dans l'approche directe en utilisant les réécritures. L'utilisateur peut maintenant se désintéresser de certaines parties de preuves comme il le ferait dans une preuve informelle. On peut voir ce travail comme s'inscrivant dans une optique plus globale qui est de créer, à terme, une tactique plus puissante capable de gérer aussi les inéquations comme le fait la tactique Omega pour les entiers naturels et relatifs. D'un point de vue plus technique, Field est un bon test pour le nouveau langage de tactiques de la V7, non pas en ce qui concerne l'implantation mais plutôt le type de situations où il peut être utile. En regardant le cas de Field, il semblerait que les tactiques réexives soient typiquement le genre de tactiques que l'on souhaite écrire à toplevel. En eet, seule la métaication nécessite l'utilisation, comme son nom l'indique, du métalangage. Étant particulièrement simple à concevoir et nécessitant du ltrage sur les termes Coq (d'un type non inductif), il est clair que la métaication

  , d'autant que le processus de métaication est extrêmement simple. Dans la V7, le langage de tactiques permet de se libérer de ce genre de contraintes au moyen d'un noyau fonctionnel et d'opérateurs de ltrage élaborés. Par ailleurs, un autre atout intéressant est, qu'étant intégré au toplevel de Coq, il est possible de faire tourner le code au moyen d'un toplevel compilé en natif sans perdre la modularité 13 du système. Dans Field, pour métaier, on utilise d'abord une tactique appelée BuildVarList qui construit la liste d'associations en évitant les doublons puis on appelle la fonction d'interprétation de R dans ExprR dénie de la manière suivante : Recursive Tactic Definition interp_R lvar trm := Match trm With | [R0] -> ER0 | [R1] -> ER1 | [(Rplus ?1 ?2)] -> Let e1 = (interp_R lvar ?1) And e2 = (interp_R lvar ?2) In '(ERplus e1 e2) | [(Rmult ?1 ?2)] -> Let e1 = (interp_R lvar ?1) And e2 = (interp_R lvar ?2) In '(ERmult e1 e2) | [(Ropp ?1)] -> Let e = (interp_R lvar ?1) In '(ERopp e) | [(Rinv ?1)] -> Let e = (interp_R lvar ?1) In '(ERinv e) | [?1] -> Let idx = (Assoc ?1 lvar) In '(ERvar idx).

  Concrètement, le travail est eectué par les fonctions Coq suivantes : Definition monom_simplif [l:(list ExprR);e:ExprR] : ExprR := Cases (list_of_monom e) of | (pairT l1 l2) => (monom_of_list (remove_list ExprR eqExprR inverse l l1 l2)) end. Fixpoint inverse_simplif [l:(list ExprR);e:ExprR] : ExprR := Cases e of | (ERplus e1 e2) => (ERplus (monom_simplif l e1) (inverse_simplif l e2)) | _ => (monom_simplif l e) end.

3. 2 . 7 .

 27 La tactique globale La tactique Field combine toutes les phases que nous venons de voir. Elle s'exprime directement dans le langage de tactiques de la V7 comme suit : Tactic Definition Field := Unfold Rminus;Unfold Rdiv; Match Context With | [|-?1== ?2] -> Let lvar = (BuildVarList '(Rplus ?1 ?2)) In Let trm1 = (interp_R lvar ?1) And trm2 = (interp_R lvar ?2) In Let mul = (GiveMult '(ERplus trm1 trm2)) In Let lmul = Eval Compute in (list_of_mult mul) In Cut (interp_ExprR lvar trm1)==(interp_ExprR lvar trm2); [Compute;Auto |(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc); (Multiply mul);[(ApplySimplif ApplyMultiply); (ApplySimplif (ApplyInverse lmul)); (Let id = (GrepMult ()) In Clear id);Compute; First [(InverseTest ());Ring|Field]|Idtac]].

2 )

 2 et la version (V7) de Coq utilisée a été compilée en natif. En eet, comme nous l'avons dit précédemment, l'utilisation du langage de tactiques de Coq pour coder Field s'adapte parfaitement à la compilation native. L'appel à Ring ne pose aucun problème puisque le code ML correspondant est linké par défaut dans la version native.

4. 1 . Exemple 1 L

 11 'exemple que nous donnons ici appartient à une famille d'égalités que nous pouvons qualier de simples. Néanmoins, ce type d'égalités revient assez souvent dans les preuves et l'accumulation de toutes ces petites preuves devient rapidement fastidieuse et ni par produire un terme preuve plus important qu'il ne devrait. Pour cette raison, il est intéressant de pouvoir utiliser Field fréquemment, tout comme Ring an de minimiser le nombres de réécritures. Nous considérons, par exemple, les parties de preuves présentes de manière récurrente telles que : b = b a × a. Welcome to Coq 7.00 (December 1999) Coq < Goal (a,b:R)``b == b*(1/a)*a``. Unnamed_thm < Intros. Time Field. 1 subgoal a : R b : R ============================ ``a <> 0`F inished transaction in 0 secs (0.35u,0s)Sans aucune réécriture, il ne nous reste plus qu'à prouver que a = 0, propriété que nous devions impérativement prouver même dans le cas où nous procédions par réécritures.4.2. Exemple 2 Nous voulons prouver queε 2+2 + ε 2+2 = ε 2 .Cette opération est utilisée dans la preuve concernant la multiplication des limites (limit_mul). La preuve du but énoncé ci-dessous fait actuellement environ 25 lignes de Coq, alors qu'après l'application de Field, il nous reste à prouver uniquement que 2 + 2 et 2 sont non nuls. Coq < Goal (eps:R)``eps*1/(2+2)+eps*1/(2+2) == eps*1/2``. Unnamed_thm < Intro. Time Field. 1 subgoal eps : R ============================ ``(2+2)*2 <> 0`F inished transaction in 0 secs (0.51u,0s) Comme dit précédemment, pour pouvoir simplier par 2 + 2 et par 2, nous utilisons le fait que 2 + 2 = 0 et 2 = 0. Ces deux conditions sont générées sous la forme d'un unique sous-but traduisant ces deux propriétés : (2 + 2) × 2 = 0. En eet, si un produit est non nul alors chacun de ses facteurs est également non nul.

4. 3 .

 3 Exemple 3 Revenons sur l'exemple cité en introduction, tiré de la preuve concernant l'addition des dérivées : Coq < Goal (f,g:(R->R); x0,x1:R) ``((f x1)-(f x0))/(x1-x0)+((g x1)-(g x0))/(x1-x0) == ((f x1)+(g x1)-((f x0)+(g x0)))/(x1-x0)-x0 <> 0`F inished transaction in 2 secs (2.17u,0s) Il ne reste plus qu'à prouver que x1 -x0 = 0, ce qui est une hypothèse de notre lemme d'addition des dérivées.

  La fonction exp (x) peut se dénir ainsi : Une forme du critère de d'Alembert est : si an+1 an -----→ n → +∞ 0 alors ∃l t.q. +∞ i=0 an.x n → l Une manière de dénir l'exponentielle est donc d'appliquer le critère de d'Alembert avec an = 1 Dans ce but, nous pouvons montrer l'égalité suivante et l'appliquer ultérieurement dans la preuve avec a = (S n) et b = n! : Coq < Goal (a,b:R)``a <> 0``->``b <> 0``->``1/(a*b)/(1/b) == 1/a`: ``a*b*(1/b*a) <> 0`F inished transaction in 0 secs (0.79u,0s) Nous remarquons la génération de deux nouveaux sous-buts. Conformément à l'algorithme utilisé, la première passe génère le sous-but 2 tandis que la seconde génère le sous-but 1. En eet, la première passe commence par multiplier par a.b × 1 b × a et, après simplications, il reste alors un 1 b . La seconde passe multiplie donc par b. Cela équivaut alors à montrer a.b = 0, 1 b = 0, a = 0 et b = 0, ce qui se déduit des hypothèses.

4. 5 .

 5 Exemple 5 Enn, nous pouvons donner l'exemple de la section 2.2, qui n'a pas de sens particulier mais qui est un bon test pour Field : Coq < Goal (x,y:R)``x*(1/x+x/(x+y)) == -1/y*y*(-(x*x)/(x+y)-1)``. Unnamed_thm < Intros. Time Field. 1 subgoal x : R y : R ============================ ``x*((x+y)*y) <> 0`F inished transaction in 1 secs (0.95u,0s) 4.6. Observation À la vue de ces quelques exemples, la principale observation concerne le temps d'exécution de la tactique. En eet, sur certains exemples, nous pouvons constater des performances assez moyennes.

  nil, cons et app sont les constructeurs et la concaténation des listes polymorphes. Union est une tactique qui concatène deux listes en éliminant les doublons (éléments communs aux deux listes). mult_of_list est une fonction Coq qui rend un produit associé à droite à partir d'une liste d'expressions de ExprR. Le Eval Compute in utilisé dans RawGiveMult permet de réduire les app pour obtenir une liste canonique pouvant être correctement ltrée (par mult_of_list).3.2.4. Distributivité et associativitéIl s'agit maintenant de distribuer totalement (sauf dans les inverses) et d'associer à droite (par rapport à l'addition et à la multiplication) dans les membres de l'égalité. Ces deux fonctions se font obligatoirement dans Coq car l'idée est de passer du terme initial au terme transformé via la réduction de Coq et un lemme de correction à prouver pour chaque fonction.

	Recursive Tactic Definition RawGiveMult trm :=
	Match trm With
	| [(ERinv ?1)] -> '(cons ExprR ?1 (nil ExprR))
	| [(ERopp ?1)] -> (RawGiveMult ?1)
	| [(ERplus ?1 ?2)] ->
	Let l1 = (RawGiveMult ?1)
	And l2 = (RawGiveMult ?2) In
	(Union l1 l2)
	| [(ERmult ?1 ?2)] ->
	Let l1 = (RawGiveMult ?1)
	And l2 = (RawGiveMult ?2) In
	Eval Compute in (app ExprR l1 l2)
	| _ -> '(nil ExprR).
	Tactic Definition GiveMult trm :=
	Let ltrm = (RawGiveMult trm) In
	'(mult_of_list ltrm).
	Lemma distrib_correct:
	(e:ExprR)(lvar:(list (Sprod R nat)))
	(interp_ExprR lvar (distrib e))==(interp_ExprR lvar e).
	où interp_ExprR est la fonction d'interprétation de ExprR vers R (écrite en Coq) et lvar la
	fonction d'associations des variables.
	L'associativité ne pose pas de problèmes dans son codage moyennant quelques précautions. De
	même que pour distrib, nous ne donnerons pas le code de la fonction d'associativité, nommée
	assoc, et il nous a fallu prouver le lemme de correction suivant :
	Lemma assoc_correct:

où La distributivité ne peut pas être codée directement et facilement dans Coq. En eet, les conditions de garde assurant la normalisation forte obligent à découper le problème de manière à faire des appels récursifs respectant la décroissance de la mesure (ordre sous-terme). Les fonctions peuvent donc sembler un peu compliquées mais il s'agit surtout de respecter ces conditions syntaxiques. Pour distribuer, l'idée est de distribuer d'abord tous les moins unaires ERopp. Ensuite, on distribue totalement dans les sous-termes et, pour le cas de la multiplication ERmult, on distribue d'abord à gauche puis à droite. Nous ne donnerons pas ici les fonctions en question qui ne présentent pas un intérêt particulier. Le lecteur intéressé pourra se reporter au code source. Pour utiliser la fonction de distributivité distrib, on a prouvé le lemme de correction suivant :

Ce choix provient d'un souci non seulement de simplicité mais aussi de rapidité dans le développement de la théorie.

Une construction des nombres réels ne changerait pas ce phénomène car R ne serait pas non plus un type inductif sur lequel on pourrait calculer. Voir, par exemple,[START_REF] Harrison | Theorem Proving with the Real Numbers[END_REF] pour s'en rendre compte.

On appelle preuves ε, les preuves utilisant la dénition explicite de la limite sous la forme : ∀ε > 0.∃α..... Dans la littérature anglaise, ces preuves sont plutôt connues sous la dénomination de preuves ε/δ.

Il ne s'agit pas ici d'entamer le leitmotiv bien connu que les preuves formelles sont bien plus diciles que les preuves que l'on peut trouver dans les meilleurs ouvrages de mathématiques mais de mettre en évidence une lacune d'automatisation qui, si elle venait à être comblée, pourrait nous permettre certaines "imprécisions" dans le sens où l'utilisateur n'aurait plus à montrer, à la main, certaines propriétés considérées comme triviales.

Cette étape est clairement non nécessaire mais elle permet un gain d'ecacité en évitant un double appel récursif pour toutes les fonctions manipulant ces expressions.

Il n'est pas nécessaire ici de vérier que x = 0 car la condition a déjà été générée lors de la multiplication par le produit de tous les inverses.

On estime, en eet, que les expressions contenant des empilements d'inverses d'inverses seront plutôt rares.

Cet algorithme ne fonctionne qu'en logique classique ([START_REF] Gabbay | The Undecidability of Intuitionnistic Theories of Algebraically Closed Fields and Real Closed Fields[END_REF]) mais ce n'est pas gênant dans la mesure où il en est de même pour les nombres réels en Coq à cause de l'axiome d'ordre total.

Kreisel et Krivine se sont aussi intéressés à un algorithme dans d'autres structures telles que les corps algébriquement clos, les anneaux de Boole séparables, ...

La taille du terme preuve est un point auquel il faut être très sensible car il n'est pas rare de rencontrer des scripts de preuves corrects pour lesquels on ne peut pas construire le terme preuve, faute de mémoire susante.

Il est intéressant de voir ici que dans le processus de réexion, la tactique et la preuve de sa correction sont indissociables.

En eet, il faut se procurer Objective Caml, Camlp4, compiler les sources de Coq, coder la métaication en comprenant la structure abstraite des termes Coq et enn compiler le chier en question.

Plus précisément, deux chiers sont principalement concernés : Rlimit.v et Rderiv.v.

D'un point de vue technique, cette abstraction s'eectue au moyen du mécanisme de sections de Coq. Tout le code peut être encapsulé dans une section où l'ensemble support, les constantes et les opérateurs s'y rapportant sont des paramètres. Le langage de tactiques s'adapte très bien à cette généralisation dans la mesure où il est également possible de ltrer sur des paramètres.