Gilles Dowek
email: gilles.dowek@inria.fr

Rules and derivations in an elementary logic course

When teaching an elementary logic course to students who have a general scientific background but have never been exposed to logic, we have to face the problem that the notions of deduction rule and of derivation are completely new to them, and are related to nothing they already know, unlike, for instance, the notion of model, that can be seen as a generalization of the notion of algebraic structure.

.

From inductive definitions to derivations 1.A method to define sets: inductive definitions

Inductive definitions are a way to define subsets of a set A. The definition of a subset P is given by functions f 1 , from A n 1 to A, f 2 , from A n 2 to A, ... These functions are called rules. For example, the function f 1 = → 0, from N 0 to N, and f 2 = a → a + 2, from N 1 to N are rules.

Instead of writing these rules f 1 = → 0 and f 2 = a → a + 2, we often write them f 1 0 a f 2 a + 2 but despite this new notation, rules are things the students know: functions.

To define the subset P , we first define a function F from P(A) to P(A) as follows

F (X) = i {f i (a 1 , ..., a n i ) | a 1 , ..., a n i ∈ X}
For example, the two rules above define the function

F (X) = {0} ∪ {a + 2 | a ∈ X}
and, for instance, F ({4, 5, 6}) = {0, 6, 7, 8}, F (∅) = {0}, F ({0}) = {0, 2}, ... The function F monotonic and continuous, thus it has a smallest fixed point P which is the inductively defined subset of A. This smallest fixed point can be defined in two ways

P = F (X)⊆X X = i F i (∅)
The first definition characterizes the set P as the smallest set closed by f 1 , f 2 , ... the second as the set containing all the elements that can be built with these functions in a finite number of steps. The monotonicity and continuity of F and the two fixed points theorems are easy lemmas [START_REF] Dowek | Proofs and Algorithms: An Introduction to Logic and Computability[END_REF] for mathematically oriented students. They can be admitted without proof otherwise. Continuing with our example, the set P of even numbers can be characterized as the smallest set containing 0 and closed by the function a → a + 2, or as the union of the sets F (∅) = {0}, F 2 (∅) = {0, 2}, F 3 (∅) = {0, 2, 4}, ...

Derivations

Defining a derivation as a tree whose nodes are labeled with elements of A and such that if a node is labeled with x and its children with y 1 , ..., y n , then there exists a rule f such that x = f (y 1 , ..., y n ), and a derivation of an element a as a derivation whose root is labeled with a, we can prove, by induction on i, that all the elements of F i (∅) have a derivation. The property is trivial for i = 0. If it holds for i and a ∈ F i+1 (∅), then by definition a = f (b 1 , ..., b n ) for some rule f and b 1 ∈ F i (∅), ..., b n ∈ F i (∅), thus, by induction hypothesis, b 1 , ..., b n have derivations. Hence, so does a.

Thus, from the second property P = ∪ i F i (∅), we get that all elements of P have derivations. Conversely, all elements that have a derivation are elements of P .

Continuing with our example the number 4 has the derivation 0 2 4

Rule names

There are several alternatives for defining the notion of derivation. For instance, when x = f (y 1 , ..., y n ), instead of labelling the node just with x, we can label it with the ordered pair formed with the element x and the name of the rule f . For instance, the derivation of 4 above would then be

0, f 1 2, f 2 4, f 2 more often written f 1 0 f 2 2 f 2 4
Such a derivation is easier to check, as checking the node 2 4 requires to find the rule f such that f (2) = 4, while checking the node 2 f 2 4 just requires to apply the rule f 2 to 2 and check that the result is 4.

But these rules names are redundant, as soon as the relation ∪ i f i is decidable. So, in general, they can be omitted.

Derivations and derivations

Instead of omitting the rule names, it is possible to omit the elements of A. The derivation of 4 is then

f 1 f 2 f 2 that can also be written f 1 . f 2 . f 2 .
Although it is not explicit in the derivation, the element 4 can be inferred from this derivation with a top-down conclusion inference algorithm, because the rules f i are functions. The conclusion of the rule f 1 can only be f 1 ( ) = 0, that of the first rule f 2 can only be f 2 ( 0 ) = 2, and that of the second can only be f 2 ( 2 ) = 4.

We can introduce this way two kinds of derivations labeled with objects and labeled with rules names.

Making the rules functional

Natural deduction proofs, for instance, are often labeled both with sequents and rule names axiom

P, Q, R ⊢ P axiom P, Q, R ⊢ Q ∧-intro P, Q, R ⊢ P ∧ Q
but they can be labeled with sequents only

P, Q, R ⊢ P P, Q, R ⊢ Q P, Q, R ⊢ P ∧ Q
and proof-checking is still decidable. They can also be labeled with rule names only, but we have to make sure that all the deduction rules are functional, which is often not the case in the usual presentations of Natural deduction. The rule

Γ ⊢ A Γ ⊢ B ∧-intro Γ ⊢ A ∧ B
is functional: there is only one possible conclusion for each sequence of premises, but the axiom rule axiom Γ, A ⊢ A is not. To make it functional, we must introduce a different rule axiom Γ,A for each pair Γ, A . Thus, the proof above must be written axiom {Q,R},P .

axiom {P,R},Q . ∧-intro . and its conclusion P, Q, R ⊢ P ∧ Q can be inferred top-down.

Derivations in elementary computability theory 2.1 A pedagogical problem

The set of computable functions is often defined inductively as the smallest set containing the projections, the null functions, and the successor function, and closed by composition, definition by induction, and minimization.

But to study the computability of properties of computable functions, we need a notion of program, that is we need a way to express each computable function by a expression, to which a Gödel number can be assigned. A usual solution is to introduce Turing machines at this point. This solution however is not pedagogically satisfying as, while the students are still struggling to understand the inductive definition, we introduce another, that is based on completely different ideas, letting them think that logic made of odds and ends. Moreover, the equivalence of the two definitions requires a tedious proof. Why do we not base our notion of program on the inductive definition itself?

Programs already exist

The function x → x + 2 is computable because it is the composition of the successor function with itself

x → x + 1 x → x + 1 x → x + 2
But such a derivation labeled with objects cannot be used as a program, because to label its nodes, we would need a a language to express all the functions, and there is no such language.

But if we use a derivation labeled with rule names instead

Succ . Succ . • 1 1 .
and write the trees in linear form: • 1 1 (Succ, Succ), we obtain a simple functional programming language to express the programs.

For instance, introduce a Gödel numbering . for these programs, and assume there is an always defined function h such that

• h(p, q) = 1 if p = f and f defined at q • h(p, q) = 0 otherwise then, the function k = • 1 1 (µ 1 (π 2 1 ), • 1 2 (h, π 1 1 , π 1 1 )
) is defined at k if and only if it is not.

We get this way a proof of the undecidability of the halting problem that requires nothing else than the inductive definition of the set of computable functions.

Derivations in elementary automata theory

When introducing the notion of automaton, we often introduce new notions, such as those of transition rules and recognizability. Having introduced the notion of derivation from the very beginning of the course permits to avoid introducing these as new notions.

Consider for instance the automaton which can be written in linear form a(a(a(ε))), or aaa.

Thus, a word w is recognized in a state s if and only if it is a derivation, labeled with rule names, of s.

This example introduces some points to be discussed: the rules even a odd odd a even are labeled with the same name. If the automaton is deterministic, we can replace these two rules with one: a function such that a(even) = odd and a(odd) = even. But for non deterministic automata, we either need to extend the notion of rule name, allowing different rules to have the same name, or to consider two rule names even a 1 odd odd a 2 even ε even and map the derivation a 1 (a 2 (a 1 (ε))) to the word a(a(a(ε))) with the function |.| defined by: |ε| = ε, |a 1 (t)| = a(|t|), and |a 2 (t)| = a(|t|).

Introducing the Brouwer-Heyting-Kolmogorov correspondence 4.1 A radical change in viewpoint?

The Brouwer-Heyting-Kolmogorov interpretation, and its counterpart, the Curry-de Buijn-Howard correspondence, are often presented as a radical change in viewpoint: proofs are not seen as trees anymore, but as algorithms. But, of course, these algorithms must be expressed in some language-often the lambda-calculus. Thus, proofs are not really algorithms, but terms expressing algorithms, and such terms are nothing else than trees. So, it is fairer to say that, in the Brouwer-Heyting-Kolmogorov interpretation, proofs are not derivation trees, but trees of a different kind. For instance, the tree

P ∧ Q ⊢ P ∧ Q P ∧ Q ⊢ Q P ∧ Q ⊢ P ∧ Q P ∧ Q ⊢ P P ∧ Q ⊢ Q ∧ P ⊢ (P ∧ Q) ⇒ (Q ∧ P )

What about derivation trees labeled with rule names?

Instead of following this idea of expressing proofs as algorithms, let us just try to label the derivation above with rule names. Five rules are used in this proof. Three of them are functional

Γ ⊢ A Γ ⊢ B ∧-intro Γ ⊢ A ∧ B Γ ⊢ A ∧ B ∧-elim1 Γ ⊢ A Γ ⊢ A ∧ B ∧-elim2 Γ ⊢ B
Let us just give them shorter names: , , f st, and snd. The rule

Γ, A ⊢ B ⇒-intro Γ ⊢ A ⇒ B
is functional, as soon as we know which proposition A in the left-hand side of the antecedent is used. So, we need to supply this proposition A in the rule name, let us call this rule λA. Finally, the rule axiom Γ, A ⊢ A is functional, as soon as we know Γ and A. We could supply Γ and A in the rule name. However, we shall just supply the proposition A and infer the context Γ. Let us call this rule [A]. So, the proof above can be written

[P ∧ Q] P ∧ Q ⊢ P ∧ Q snd P ∧ Q ⊢ Q [P ∧ Q] P ∧ Q ⊢ P ∧ Q f st P ∧ Q ⊢ P , P ∧ Q ⊢ Q ∧ P λP ∧ Q ⊢ (P ∧ Q) ⇒ (Q ∧ P )
and if we keep rule names only

[P ∧ Q] . snd . [P ∧ Q] . f st . , . λP ∧ Q . or in linear form λP ∧ Q snd([P ∧ Q]), f st([P ∧ Q])
. This is the scheme representation [START_REF] Dowek | On the expressive power of schemes[END_REF] of this proof.

Let us show that the conclusion can be inferred, although we have not supplied the context Γ in the axiom rule. The conclusion inference goes in two steps. First we infer the context bottom-up, using the fact that the conclusion has an empty context, and that all rules preserve the context, except λA that extends it with the proposition A

[P ∧ Q] P ∧ Q ⊢ . snd P ∧ Q ⊢ . [P ∧ Q] P ∧ Q ⊢ . f st P ∧ Q ⊢ . , P ∧ Q ⊢ . λP ∧ Q ⊢ .
Then, the right-hand part of the sequent can be inferred with a usual top-down inference algorithm, using the fact that the rules are functional

[P ∧ Q] P ∧ Q ⊢ P ∧ Q snd P ∧ Q ⊢ Q [P ∧ Q] P ∧ Q ⊢ P ∧ Q f st P ∧ Q ⊢ P , P ∧ Q ⊢ Q ∧ P λP ∧ Q ⊢ (P ∧ Q) ⇒ (Q ∧ P )

Brouwer-Heyting-Kolmogorov interpretation: an optional modification

In the rule Γ, A ⊢ B ⇒-intro Γ ⊢ A ⇒ B instead of supplying just the proposition A, we can supply the proposition A and a name x for it. Then, in the axiom rule axiom Γ, A ⊢ A

  where the state even is final. In this automaton, the word aaa is recognized in odd. of introducing a new notion of transition rule, we just define transition rules as deduction rules

  ∧ Q often written in linear form: λx : P ∧ Q snd(x), f st(x) .

Vol. \jvolume No. \jnumber \jyear IFCoLog Journal of Logic and its Applications

instead of supplying the proposition A, we can just supply the name that has been introduced lower in the tree for it. We obtain this way the tree x . snd .

x . f st . , . λx : P ∧ Q .

in linear form λx : P ∧ Q snd(x), f st(x) , which is exactly the representation of the proof according to the Brouwer-Heyting-Kolmogorov interpretation.

So, the Brouwer-Heyting-Kolmogorov interpretation boils down to use of derivations labeled with rule names plus two minor modifications: context inference and the use of variables. These two modifications can be explained by the fact that Natural deduction does not really deal with sequents and contexts: rather with propositions, but, following an idea initiated in [START_REF] Schroeder-Heister | A natural extension of natural deduction[END_REF], some rules such as the introduction rule of the implication dynamically add new rules, named with variables.


Francois Musy
email: francois.musy@ec-lyon.fr

Laurent Nicolas
email: laurent.nicolas@ec-lyon.fr

Ronan Perrussel
email: ronan.perrussel@ec-lyon.fr

Numerical Analysis

This note gives conditions that must be imposed to algebraic multilevel discretizations involving at the same time nodal and edge elements so that a gradient-prolongation commutativity condition will be satisfied; this condition is very important, since it characterizes the gradients of coarse nodal functions in the coarse edge function space. They will be expressed using graph theory and they provide techniques to compute approximation bases at each level.

un choix intéressant. Pour les systèmes provenant de discrétisations par éléments finis d'arête, Hiptmair a introduit des méthodes multiniveau pour une hiérarchie de maillages emboîtés [START_REF] Hiptmair | Multigrid method for Maxwell's equations[END_REF].

Cependant, dans des applications réalistes, on ne dispose généralement pas de maillages structurés. La stratégie multiniveau algébrique va donc s'imposer : il s'agit de définir des fonctions grossières nodales et d'arête grâce aux contributions de paquets de fonctions fines nodales et d'arête ; les combinaisons linéaires (1a) et (1b) définissent respectivement ces fonctions grossières nodales et d'arête.

Par construction les gradients des fonctions nodales fines appartiennent à l'espace des fonctions d'arête fines ce que traduit la relation [START_REF] Hiptmair | Multigrid method for Maxwell's equations[END_REF]. Dans cette relation, G h est la matrice d'incidence arcs-sommets du graphe orienté naturellement associé au maillage de travail. Les orientations des arcs sont arbitraires.

Pour adapter aux méthodes algébriques les lisseurs des méthodes géométriques, Reitzinger et Schöberl [START_REF] Reitzinger | An algebraic multigrid method for finite element discretizations with edge elements[END_REF] ont introduit une représentation explicite des gradients des fonctions grossières nodales dans la base des fonctions grossières d'arête, donnée par la relation [START_REF] Reitzinger | An algebraic multigrid method for finite element discretizations with edge elements[END_REF] où G H est une matrice d'incidence arcs-sommets.

En regroupant les relations (1) à (3), nous obtenons la relation matricielle [START_REF] Mandel | Energy optimization of algebraic multigrid bases[END_REF]. La matrice α est construite par exemple par les méthodes définies dans [START_REF] Mandel | Energy optimization of algebraic multigrid bases[END_REF] qui permettent d'obtenir les fonctions grossières nodales comme partition de l'unité et de contraindre leurs supports à être inclus dans des ensembles géométriques convenablement choisis.

Connaissant G h et α, nous souhaitons choisir G H comme matrice d'incidence arcs-sommets d'un graphe orienté S H . Nous donnons dans cette note une condition nécessaire et suffisante sur ce graphe, la proposition (2.3), qui assure l'existence d'une solution de [START_REF] Mandel | Energy optimization of algebraic multigrid bases[END_REF]. En effet, nous associerons, par un procédé décrit dans la partie en anglais, à chaque arête fine un sous-graphe du graphe grossier, qui doit être connexe.

La connaissance de ces sous-graphes donne les degrés de liberté disponibles pour déterminer des fonctions d'arête grossières compatibles avec les fonctions nodales grossières ; en résolvant un problème de flot sur ces sous-graphes, voir (14), nous pouvons alors construire la matrice β (Section 4).

Introduction

Numerical approximation of electric or magnetic field uses often edge finite elements whose relation with nodal finite elements contains important properties at discrete level [START_REF] Hiptmair | Finite elements in computational electromagnetism[END_REF]. In this note we restrict ourselves to lowest order approximation : P 1 for nodal elements and incomplete order 1 for edge elements. In order to solve large problems, multilevel methods are an attractive choice. While, for systems coming from edge element discretisation, Hiptmair [START_REF] Hiptmair | Multigrid method for Maxwell's equations[END_REF] proposed multilevel methods using nested meshes, engineering applications do not usually provide structured meshes. Therefore, algebraic multilevel methods are an interesting option: we have to build coarse nodal and edge functions by using aggregates of fine nodal and edge functions. If (φ h p ) p=1,...,N h and (λ h i ) i=1,...,E h respectively denote fine nodal and edge bases, the following linear combinations define coarse nodal and edge functions:

φ H n = N h p=1 α pn φ h p , ∀n ∈ {1, . . . N H }, (1a)
λ H e = E h i=1 β ie λ h i , ∀e ∈ {1, . . . , E H }. ( 1b
)
By construction, the gradients of fine nodal functions belong to the space of fine edge functions:

∀p ∈ {1, . . . , N h }, grad(φ h p ) = E h i=1 G h ip λ h i , (2)
where G h is the edge-node incidence matrix of the digraph naturally associated with the initial mesh.

The orientation of the edges can be arbitrarily chosen.

In [START_REF] Reitzinger | An algebraic multigrid method for finite element discretizations with edge elements[END_REF], Reitzinger and Schöberl deduced their smoother from the matrix G H involved in the relation:

∀n ∈ {1, . . . , N H }, grad(φ H n ) = E H e=1 G H en λ H e , (3)
which states that the gradients of the coarse nodal functions must also belong to the space of coarse edge functions. The matrix G H is an edge-node incidence matrix as in the structured case. Relation (3) does not guarantee the efficacy of the algebraic multilevel method but it leads to relevant strategies. Gathering Equations ( 1), ( 2) and ( 3), we obtain the matrix relation:

G h α = βG H . (4)
The matrix α is constructed following for instance the methods defined in [START_REF] Mandel | Energy optimization of algebraic multigrid bases[END_REF], which provides a family of coarse nodal functions, making up a partition of unity, whose supports satisfy appropriate conditions. Knowing the left-hand side of (4), we want to choose G H as an edge-node incidence matrix of a digraph S H , and we will give conditions on the coarse graph S H , which ensure the existence of a matrix β satisfying (4). Moreover, the proof of the proposition indicates how to choose the degrees of freedom which enables us to define the coarse edge functions. It also helps us to construct β.

Notation and statement of the problem

Let (L n ) n=1,...,N H be sets of indices in {1, . . . , N h } such that:

N H n=1 L n = {1, . . . , N h }. (5)
The matrix α describes the coarse nodal basis; we assume that it is has been previously computed and it has the following properties: -the coarse nodal functions make up a partition of unity, which can be algebraically stated as:

∀p ∈ {1, . . . , N h }, N H n=1 α pn = 1, (6)
-in order to restrict the support of each coarse basis function φ H n , the indices of the non-zero components of φ H n are included in the set L n , i.e.:

p ∈ {1, . . . , N h } \ L n =⇒ α pn = 0. (7)
The fine nodal function φ h p contributes to the coarse nodal function φ H n if p belongs to L n . We have a reciprocal set-valued function L: the set L p is the set of coarse nodal function indices to which the fine nodal function φ h p contributes. For the fine graph in Figure 1(a), we set L 1 = {1, 2, 3, 4, 5, 6, 7}, L 2 = {5, 6, 8, 9, 13, 14} and L 3 = {7, 8, 10, 11, 12}. One obtains, for instance, the set L 7 = {1, 3}.

We define two families of sets of fine edge function indices. We will denote a directed fine edge i by pq h where p and q are respectively the starting and ending nodes of the edge i. A similar notation is used for a directed coarse edge e = mn H .

The set C n is the set of indices of fine edges which have an extremity in L n :

C n = i ∈ {1, . . . , E h } : i = pq h , p ∈ L n or q ∈ L n . (8)
The fine edge function λ h i contributes to the gradient of the coarse nodal function φ H n if i belongs to C n . Indeed, for the directed fine edge i = pq h , G h ir is equal to -1 if r = p and +1 if r = q. Moreover, if p and q are not in L n , the components α pn and α qn vanish according to (7); therefore:

i ∈ {1, . . . , E h } \ C n =⇒ (G h α •n ) i = 0, (9)
where α •n denotes the n-th column of α. The reciprocal set-valued function C is such that C i is the set of coarse nodal function indices to whose gradient the fine edge function λ h i contributes. On Figure 1(b), the fine edges are numbered, set C 3 is highlighted and we can note, for instance, the set C 8 = {1, 3}.

Let e = mn H be an edge of the coarse graph S H ; we define:

I e = C n ∩ C m . ( 10
)
By analogy with the structured case and for restricting the support of λ H e , we enforce: i ∈ {1, . . . , E h } \ I e =⇒ β ie = 0.

(11)

The fine edge function λ h i contributes to the coarse edge function λ H e if i belongs to I e . The set-valued function I is such that I i is the set of coarse edge function indices to which the fine edge function λ h i contributes. The coarse graph in Figure 1(c) is related to the fine in Figure 1(a). Set I e3 is represented in Figure 1(d). The following statement can be easily deduced from (8) and the definition of

G h : Lemma 2.1 If i denotes the edge pq h , C i = L p ∪ L q .
In order to simplify notations, we introduce the set F = i ∈ {1, . . . , E h } : I i = ∅ , since some fine edge functions might not contribute to any coarse edge functions.

For any fine edge i, let S H,i be the induced subgraph defined by C i : the vertices of S H,i are the vertices of S H , which are indexed by the elements of C i and the edges of S H,i are those edges of S H whose extremities are vertices of S H,i .

The following lemma is a direct consequence of definition (10): Lemma 2.2 For any edge i ∈ F , the edges of S H,i are those edges of S H which are indexed by I i .

We may now state precisely our main result, which gives a necessary and sufficient condition on the coarse graph S H permitting the resolution of (4): Proposition 2.3 For all matrices α satisfying conditions (6) and (7), there exists a matrix β satisfying (11) and solving (4) iff for all i, the induced subgraph S H,i is connected.

The essential steps of the proof

First step. Many relations in (4) reduce to 0 = 0: this is the case for n / ∈ C i . Indeed, according to (9) the (i, n) coefficient of the right-hand side of (4) vanishes. Conversely, if e does not belong to I i , according to (11) and the definition of I i , β ie vanishes and:

E H e=1 β ie G H en = e∈ Ii β ie G H en . (12)
On the other hand if the directed coarse edge e denoted by lm H belongs to I i , Lemma 2.2 implies that l and m belongs to C i . However, for G H en not to vanish for all e, m or l must be equal to n, which means that n belong to C i , and this contradicts the assumption n / ∈ C i . Second step. We look at all the other equations, i.e. those for which n ∈ C i . We note that (12) remains and that the edges indexed by I i are precisely those of the graph S H,i according to Lemma 2.2.

We assume now i ∈ F and we define G H,i as the edge-node incidence matrix of S H,i and the (i, n) equation of ( 4) is rewritten:

e∈ Ii β ie G H,i en = Θ i,n where Θ i,n = r∈Ln G h ir α rn . (13)
This could be satisfied for all couples (i, n) such that n ∈ {1, . . . , N H } and i ∈ C n or equivalently i ∈ {1, . . . , E h } and n ∈ C i . For a fixed i, we may write that β i• , the i-th row of β satisfies the system:

e∈ Ii

β ie G H,i en = Θ i,n , ∀n ∈ C i . (14)
Thus, we solve line by line for β and we see that ( 14) is a flow problem whose solution is of the form:

β i• = β ′ i• + β ′′ i• . (15)
with (β ′′ i• ) t ∈ ker(G H,i ) t and β ′ i• a particular solution. More precisely, let T i be a spanning tree for S H,i ; call Γ i the edge-node incidence matrix associated with T i ; we know that Γ i has | C i |-1 rows and | C i | columns, and it is of rank | C i |-1. We choose a vertex m in Γ i and we solve the system:

e∈E(T i ) β ′ ie Γ i en = Θ i,n , ∀n ∈ C i \ {m}, (16)
where E(T i ) denotes the set of indices of the edges of T i . The system (16) is a regular system of | C i |-1 equations with | C i |-1 unknowns, and we put β ′ ie equal to 0 if e is in I i \ E(T i ). It remains to show that the forgotten equation of index m in ( 16) is automatically satisfied. Indeed, by denoting i by pq h , we sum the right-hand side of (14) with respect to n ∈ C i :

n∈ Ci Θ i,n = n∈ Lp∪ Lq α qn -α pn = 0, (17)
since in view of ( 6) and (7), On the other hand, if we sum the left-hand side of ( 14) with respect to n ∈ C i , we obtain:

n∈ Ci e∈ Ii β ie G H,i en = e∈ Ii β ie n∈ Ci G H,i en = 0, (18)
since each line of G H,i contains only two non-zero coefficients +1 and -1.

If i / ∈ F , | C i |= | L p |= | L q |= 1
Since C i is strictly included in L p ∪ L q , we will have C i ∩ L p = L p or C i ∩ L q = L q . Depending on the situation, we can construct a suitable matrix α such that: For these matrices α, the condition defined by (4) cannot be ensured.

Construction of the coarse edge functions

For a coarse graph satisfying the condition of Proposition 2.3 and by using the decomposition (15), any compatible matrice can be written β = β ′ + β ′′ , where the complete matrices are defined by gathering the lines of index i β i• , β ′ i• and β ′′ i• . The computation of each β ′ i• can be done by solving system (16). As concerns β ′′ i• , a basis of the kernel of (G H,i ) t is given by a set of k i independent cycles of S H,i . Then, i∈ F k i degrees of freedom should be determined by minimising an appropriate energy functional; such a problem is introduced in [START_REF] Musy | Compatible coarse nodal and edge elements through energy functionals[END_REF] and can be related to explanations in [START_REF] Mandel | Energy optimization of algebraic multigrid bases[END_REF].

We thank Michelle Schatzman for many fertile discussions.

  Fine graph with node indices. Sets (Ln) n=1,...,3 are surrounded.

  Fine graph with edge indices. Set C 3 is represented by bold edges. graph. (d) Set Ie 3 is represented by bold edges.

Figure 1 .

 1 Figure 1. Representation of the fine and coarse graphes, sets (Ln) n=1,...,3 , C 3 and Ie 3 .

  and the relation Now we assume that S H,i is not connected and we denote by C i the nodes of a connected component.

			E H
			β ie G H en = Θ i,n is satisfied from (12) and (17).
			e=1
					E H
	For the same reasons as in (18), if β satisfies (11) one gets		β ie G H en = 0.
				n∈ Ci	e=1
						N h
	However we can construct a matrix α satisfying (6) and (7) such that	G h ir α rn = 0. In fact, in
						n∈ Ci	r=1
	view of (7), for i = pq h we can write:
		N h
		G h ir α rn =	α qn -α pn =		α qn -	α pn .
	n∈ Ci	r=1	n∈ Ci	Ci∩ Lq	Ci∩ Lp


Julien Jaeger
email: julien.jaeger@cea.fr

Emmanuelle Saillard
email: emmanuelle.saillard.ocre@cea.fr

Patrick Carribault
email: patrick.carribault@cea.fr

Denis Barthou
email: denis.barthou@inria.fr

Correctness Analysis of MPI-3 Non-Blocking Communications in PARCOACH

Keywords: MPI, Non-blocking collectives, checker, static analysis

MPI-3 provide functions for non-blocking collectives. To help programmers introduce non-blocking collectives to existing MPI programs, we improve the PARCOACH tool for checking correctness of MPI call sequences. These enhancements focus on correct call sequences of all flavor of collective calls, and on the presence of completion calls for all nonblocking communications. The evaluation shows an overhead under 10% of original compilation time.

INTRODUCTION

Most parallel scientific applications rely on the distributedmemory specification called MPI (Message Passing Interface) to e ciently exploit a supercomputer and reach high parallel performance. This programming model proposes point-to-point and collective communications to transfer messages between the di↵erent processes. Furthermore, the first specification provides the notion of non-blocking point-topoint communications.

Non-Blocking Point-To-Point Communications and Completion Calls: Non-blocking point-to-point communication allows to overlap communication and computation and thus to leverage hardware parallelism. Several studies [START_REF] Hoefler | Optimizing a conjugate gradient solver with non-blocking collective operations[END_REF] have shown that the performance of parallel applications can be significantly enhanced with overlapping techniques. A call to a non-blocking point-to-point communication initiates an action without completing it. Another function, called completion call is necessary to finish the action. At the end of this completion call, the runtime ensures ACM ISBN 978-1-4503-2138-9. DOI: 10.1145/1235 that it is safe for the application to reuse the communication bu↵ers. One can distinguish two types of completion calls: completion calls that complete only one non-blocking operation ( functions MPI_{Wait,Waitany,Test,Testany}, referred to as unitary completion call or ucc) and completion calls checking in a list of operations all the ones that are done (functions MPI_{Waitall,Waitsome,Testall,Testsome}, referred to as multi completion call or mcc).

Collective Communications: Collective communications are an important part of parallel scientific computing [START_REF] Dureau | Hybrid parallel programming models for amr neutron monte-carlo transport[END_REF]. The non-blocking collectives provided in MPI-3 API combine the e cient algorithms of collectives operations with the overlapping benefits of non-blocking communications. The non-blocking collective model is similar to the one proposed by non-blocking point-to-point communications. The main di↵erence with point-to-point communications is that blocking collectives can not be matched to their non-blocking counterparts. The ordering of collectives between blocking and non-blocking collectives, and between non-blocking collectives, is very important. If one process calls a non-blocking collective, the remaining processes should also call the same function before initiating any other collective.

In this paper, we introduce an evolution of the PAR-COACH [START_REF] Saillard | Parcoach: Combining static and dynamic validation of MPI collective communications[END_REF] tool with a new static analysis allowing to debug MPI non-blocking call sequences.

ANALYSIS OF NON-BLOCKING COM-MUNICATIONS

To tackle the issues pointed out in Section 1, we propose two new analyses: (i) a new static pass to check if the number of completion calls may match non-blocking call (either collective or point-to-point) and (ii) a static analysis to check that the sequence of all flavor of collective is the same along all possible execution paths. These analyses have been implemented inside PARCOACH [START_REF] Saillard | Parcoach: Combining static and dynamic validation of MPI collective communications[END_REF], a tool proposing a twophase analysis to detect incorrect collective patterns in MPI programs. It combines a static analysis identifying the reduced set of problematic collectives with a selective instrumentation on the corresponding nodes in the Control Flow Graph (CFG) of the function to handle the deadlocks.

Matching Non-blocking Communication with Completion Calls: With this new pass, we determine if each non-blocking operation, either point-to-point or collective, can be matched to a completion call. For a path to be valid, each non-blocking operation should correspond to a unitary completion call or to a multi completion call. The exact matching would require to execute the code, checking all arguments passing and memory movements. Statically, we make the following assumption: a completion call always matches a previous pending non-blocking operation, if any. Within this assumption and for each basic block of the analyzed function, the number of pending non-blocking communications (called pnb) is computed, using an interval notation, following Algorithm 1. The lower bound (lb) corresponds to the number of pending communications when mcc statements complete all the previous non-blocking communications. The upper bound (ub) corresponds to the number of pending communications case when mcc statements only complete one of the previous non-blocking communication. Given this approach, a function is incorrect (completion calls missing) if the lower bound of the pnb for the function exit is greater than 0. The function may be incorrect if the upper bound of this pnb is greater than 0.

Algorithm 1 Evaluating the number of pending nonblocking communications 1: function PNB bound(G = (V, E))

. G: CFG

2:

Remove loop backedges in G 3:

for n 2 V ,

18:

Output pnb

19: end function

Extending PARCOACH with Non-Blocking Semantics:

In Section 1, non-blocking collectives have been shown to share the same constraint as blocking collectives when used together. Once this behavior is identified, supporting nonblocking collectives in the original analysis of PARCOACH is straightforward: the syntactic parser of collective names has to be enhanced with non-blocking ones. Since PARCOACH uses the output list of this step to instrument the problematic nodes, our enhancement will directly benefit from the instrumentation. PARCOACH will then be able to insert functions for runtime checking before all flavor of collectives, including non-blocking ones.

RESULTS

We tested our two static analyses on the Intel MPI Benchmarks version 4.0 (IMB) and a microbenchmarks suite of unitary tests we created (NBC-bench). These results were Figure 1 highlights the compilation-time overhead obtained with and without static instrumentation (validation functions insertions) on the two sets of benchmarks. For each test, the overhead of the original PARCOACH analysis, for blocking MPI collective calls, and our improved analysis, checking both blocking and non-blocking MPI collective calls, are provided. The black bars display the original overheads, and the grey bars show the additional overhead created by the addition of non-blocking collectives in the static analysis. Our addition to the checking of collective only bring an extra 1% to the overhead, which remains under 9% of the total compilation time.

CONCLUSION

In this paper, we extended the static analysis of PAR-COACH, originally designed for checking blocking collective calls, to include non-blocking collectives. A second static analysis was included to also check the completion of all non-blocking communications issued in an MPI program. The designed algorithms allow to find if non-blocking calls are not completed in a function, and return the list of problematic nodes for issuing warnings to the developer. This addition brought a small extra overhead compared to the original analysis, and the complete compilation time with the new analyses being less than 10% higher than initial compilation time.

Figure 1 :

 1 Figure 1: Overhead of average compilation time with and without verification code generation