Christine Paulin-Mohring

Christine Paulin

Kahn Networks In Coq Yves Bertot

Gérard Huet

Gilles Kahn

Y Bertot

J.-J Lvy

G Plotkin

A constructive denotational semantics for Kahn networks in Coq

.

. For that purpose, we developed a general library for cpos. Our cpos are defined with an explicit function computing the least upper bound (lub) of an increasing sequence of elements. This is different from what Kahn developed for the standard Coq library where only the existence of lubs (for arbitrary directed sets) is required, giving no way to explicitly compute a fixpoint. We define a cpo structure for the type of possibly infinite streams. It is then possible to define formally what is a Kahn network and what is its semantics, achieving the goal of having the concept closed under composition and recursion. The library is illustrated with an example taken from the original paper as well as the Sieve of Eratosthenes, an example of a dynamic network.

Introduction

Semantics of programming languages and interactive environments for the development of proofs and programs are two important aspects of Gilles Kahn's scientific contributions. In his paper "The semantics of a simple language for parallel programming" [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], he proposed an interpretation of (deterministic) parallel programs (now called Kahn networks) as stream transformers based on the theory of complete partial orders (cpos). A restriction of this language to synchronous programs is the basis of the data-flow Lustre language [START_REF] Pilaud | Lustre: a declarative language for programming synchronous systems[END_REF][START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF] which is used now for the development of critical embedded systems. Because of the elegance and generality of the model, Kahn networks are also a source of inspiration for extensions of the data-flow synchronous paradigm to higher-order constructions [START_REF] Caspi | Synchronous Kahn Networks[END_REF] or to more permissive models of synchrony [START_REF] Cohen | N -Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems[END_REF].

We present a formalization of this seminal paper in the Coq proof assistant [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF][START_REF] Coq | The Coq Proof Assistant Reference Manual -Version V8.1[END_REF]. For that purpose, we developed a general library for cpos. Our cpos are defined with an explicit function computing the least upper bound (lub) of a monotonic sequence of elements. This is different from what Kahn developed for the standard Coq libraries where only the existence of lubs is required, giving no way to explicitly compute a fixpoint. However, Kahn's library was intended as the background for a computer formalisation of the paper "Concrete Domains" by Kahn and Plotkin [START_REF] Kahn | Concrete domains[END_REF] and it covers general cpos with the existence of a lub for arbitrary directed sets while our work only considers ω-cpos with lubs on monotonic sequences which is a sufficent framework for modeling Kahn networks.

We define a cpo structure for the type of possibly infinite streams. This is done using a coinductive type in Coq with two constructors, one for adding an element in front of a stream, the second constructor add a silent step Eps. From the structural point of view, our streams are infinite objects; this is consistent with the fact that these streams are models for communication links which are continuously open even if there is no traffic on the line. However, we identify the empty stream with an infinite stream of Eps constructors, so our data type models both finite and infinite streams. We define the prefix order on this data type and the corresponding equality. We also develop useful basic functions: the functions for head, tail and append used by Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], but also a filtering and a map function.

It is then possible to define formally what is a Kahn network and what is its semantics, achieving the goal of having the concept closed under composition and recursion. A Kahn network will be defined by a concrete set of edges corresponding to links in the network, each one associated with the type of the objects which are transmitted on that link. With each noninput edge is associated a node which is a continuous function producing a stream of outputs from streams given as inputs. The type of Kahn networks has a natural cpo structure. The semantics of a Kahn network is obtained in the following way: we provide streams for the input edges of the system, then the system is interpreted as an equation on the streams corresponding to the traffic on all the edges, seen as a continuous function. The semantics of the network is the fixpoint of this continuous function. We prove that this solution is a continuous function both of the network and of the input streams. By selecting the appropriate outputs, a system can be interpreted as a new node to be used in another system. Also the continuity with respect to the system itself gives the possibility of recursively defining a system.

Our library is illustrated with an example taken from the original paper as well as the Sieve of Eratosthenes, an example of a dynamic network, recursively defined.

Outline The remaining part of the introduction gives the main notations used in this paper. Section 2 recalls Kahn's approach in [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] which introduces cpos as a natural structure for the semantics of a simple parallel language. Section 3 introduces our definition of Cpo structures in Coq. It is based on a structure of ordered types. We define the cpos of monotonic and continuous functions as well as several constructions for product of cpos. Section 4 introduces the type of possibly infinite streams and defines a cpo structure on it (in particular a lub function). We start with the simpler case of the flat cpo. We define a general function on the cpo of streams computing the value depending on the head and tail of the stream (and giving the empty stream in case the input is empty). We derive from this operator the constructions for head, tail and append as well as functionals for mapping a function on all elements of the stream or filtering the elements of a stream with respect to a boolean condition. We derive a cpo structure for natural numbers as a particular case of streams. Section 5 defines a type for Kahn networks and the associated semantics. Section 6 illustrates our library on two examples, one taken from the original paper [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], the other is the Sieve of Eratosthenes.

Notation In this paper, we use mathematical notations close to the Coq notations.

The expression A → B represents both the type of functions from type A to type B and the proposition: "A implies B". The arrow associates to the right:

A → B → C represents A → (B → C).
The expression ∀x, P represents the proposition "for all x, P " or the type of dependent functions which associate with each x an object of type P . We can annotate a variable with its type and put several binders like in ∀(x y : A)(z : B), P which represents the property: "for all x and y of type A and z of type B, P holds".

The function which maps a variable x of type A to a term t is written fun x ⇒ t or fun x : A ⇒ t. We can introduce several binders at the same time.

We write c x 1 . . . x n def = t to introduce c as an abbreviation for the term fun x 1 . . . x n ⇒ t. We write x = y for (polymorphic) definitional equality in Coq (i.e. terms that are structurally equal). We use the notation x == y for a specific equivalence relation associated with the type of x and y, defined as a setoid equality1 .

We shall also use the Coq notation {x : A|P } for the type of pairs (a, p) with a of type A and p a proof of P [a/x] and {x : A&{y : B|P }} for the type of triples (a, b, p) with a of type A, b of type B and p a proof of P [a/x, b/y].

From a simple parallel languages to cpos

In [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], Kahn proposes an algol like language to describe parallel system. Each process is defined as a procedure with input and output parameters which are interpreted as channels. In the body of the procedure, there is a possibility to wait for a value on an input parameter or to send a value on an output parameter. Global channels can be declared, the processus can be instatiated and executed in parallel. The idea is that each channel correponds to a fifo in which values can be stored or read. There is no bound on the size of the fifo and a processus can be blocked waiting a value on an empty channel.

More precisely a Kahn network is built from autonomous computing stations linked together. The stations exchange information through communication lines. The assumptions are that a computing station receives data from input lines, computes using its own memory and produces result on some of the output lines. The communication lines are the only medium of communication between stations and the transmission of data on these lines is done in a finite amount of time. With each communication line, we associate the type of data which transit on that line. Each node can use the history of the inputs to produce an output, so it can be seen as a function from the streams of inputs to the streams of outputs. This function is continuous, which means that an output can be delivered without waiting for an infinite amount of information on the inputs lines.

A Kahn network is represented as an oriented graph. The nodes are the computing stations and the edges are the communication lines. We distinguish the input lines which have no source node. The graphical representation of the example in Kahn's paper is given in figure 1.

h 0 f h 1 g Z Y T 1 T 2 X Figure 1: A simple example of Kahn network
In Kahn semantics, we look at the sequence of values that will be sent on each channel. This is a possibly infinite sequence (a stream). Locally each node is interpreted as a function taking as input a stream for each input edge and computing a stream for each output edge.

The system itself will behave as the solution of a set of equations defining the stream of values on the channels (one equation for each node). In our example, the system of equations will be:

X = f (Y, Z) Y = h 0 (T 1 ) Z = h 1 (T 2 ) T 1 = g 1 (X) T 2 = g 2 (X)
This is a recursive definition. In order to ensure the existence of a solution, we use a cpo structure on the set of streams (with the prefix order) and we prove that each node corresponds to a monotonic and continuous function.

Now if we have a system and we distinguish input and output edges, the solution is itself a continuous function from inputs to outputs so behaves like a node. This is an essential property for a modular design of systems. It gives also the possibility to recursively defined a system, like the Sieve of Eratosthenes which we describe in 6.2 and which corresponds to the network in figure 2. The precise definition of nodes in the previous examples will be given in section 6.

Formalizing cpos constructively

The basic structure used for the interpretation of Kahn networks is the ωcomplete partial order. We developed a Coq library of general results on ω-cpos.

Definition

An ω-cpo is a type D with a partial order ≤, a least element (usually written ⊥) and a least-upper bound (written lub h) for any monotonic sequence h of elements in

D (h : nat → D such that ∀nm, n ≤ m → h n → h m).
An ω-cpo is actually a weaker structure than ordinary cpos where lubs exist for any directed set of elements. However, ω-cpos are sufficient for the construction of fixpoints. In the following we refer to ω-cpos simply as cpos.

Ordered structure

We define the type ord of ordered structures. An object in the type ord is a dependent record with a type A, a binary relation ≤ on A, and a proof that this relation is reflexive and transitive.

An example of an ordered structure is the type nat of natural numbers with the usual order. In the following, we shall abusively write nat for the object of type ord corresponding to this structure.

Notations When O is an ordered structure, we write x : O to mean that x is an element of the carrier of O. The coercion mechanism in Coq allows us to support this abuse of notation: whenever a type is expected and an ordered structure O is provided, Coq automatically coerces the term O to its carrier.

When O is an ordered structure and x, y : O, the Coq notation mechanism allows to write x ≤ y to express that x and y are in the relation associated with the ordered structure O. We shall write x ≤ O y when we want to make the ordered structure explicit.

Equality We define an equality on an ordered structure by:

x == y def = x ≤ y ∧ y ≤ x;
this is obviously an equivalence relation.

Order on functions Given an ordered structure O and a type A, there is a natural order on the type A → O of functions from A to O, called the pointwise order, which is defined by f ≤ A→O g def = ∀x, f x ≤ O g x. We write A o → O for the corresponding ordered structure. → O 2 , it is formally a pair with a function and a proof of monotonicity. In Coq, we introduce a coercion from f to a function from O 1 to O 2 , such that we can write (f x) in a way consistent with mathematical practice. We consequently have the following property:

Monotonic functions

∀(f : O 1 m → O 2 )(x y : O 1 ), x ≤ y → f x ≤ f y.
We also proved that any monotonic function preserves equality.

The composition of two monotonic functions is monotonic:

when f : O 1 m → O 2 and g : O 2 m → O 3 , we define g@f of type O 1 m → O 3 the monotonic function such that (g@f ) x = g (f x) Notation fun x m ⇒ t. If t is an expression of type O 2 depending on x of type O 1 , we write fun x m ⇒ t for the object f in Coq of type O 1 m → O 2 ,
which is a monotonic function such that f x = t. In Coq, the object f is formally a pair built from the function fun x ⇒ t and a proof of monotonicity. The (informal) notation fun x m ⇒ t hides the proof of monotonicity and helps us to insist on the functional behavior of f . In our Coq development we try to systematically define objects in O 1 m → O 2 using combinators like the composition of monotonic functions in order to get proof of monotonicity for free relying on the type system. After the definition of such an object f , we systematically prove a (trivial) lemma f x = t which captures the functional behavior of the monotonic function. This lemma is useful for rewriting the expressions involving f .

Cpo structure

A cpo structure is defined as a record which contains:

• an ordered structure O;

• a least element ⊥ of type O;

• a least upper-bound function lub for monotonic sequences;

the constant lub has type: (nat

m → O) → O;
• proofs of the following properties:

-∀x : O, ⊥ ≤ x -∀(f : nat m → O)(n : nat), f n ≤ lub f -∀f : (nat m → O)(x : O), (∀n, f n ≤ x) → lub f ≤ x A cpo
lub (F @f ) ≤ F (lub f )
We say that F is continuous whenever the other direction is true, namely:

∀f : nat m → D 1 , F (lub f ) ≤ lub (F @f ). We write D 1 c → D 2 for the ordered structure of continuous functions. When g has type D 2 c → D 3 and f has type D 1 c → D 2 , we write g@ f the element of D 1 c → D 3 which corresponds to the composition of f and g, ie such that (g@ f ) x = g (f x).

Cpo constructions

The structure of cpos is preserved by the usual constructions of functions and products. In this part we show constructions for the cpos of functions, monotonic functions and continuous functions as well as the product of two cpos, of an arbitrary family of cpos and the k-times product D k of a cpo D.

Functional constructions

Given a cpo structure D and a type A, we can define a cpo structure on the set of functions from A to D using a pointwise construction for ⊥ and lub:

⊥ A→D def = fun x → ⊥ D lub A→D h def = fun x ⇒ lub D (fun n m ⇒ h n x)
We →D2 is a continuous function and lub preserves continuity, we also have a cpo structure on continuous functions from D 1 to D 2 . We write D 1 C → D 2 for this cpo structure.

Product constructions

We formalized other constructions on cpos corresponding to products.

Binary product The binary product

D 1 × D 2 of two cpo structures has a cpo structure written D 1 ⊗ D 2 . ⊥ D1⊗D2 def = (⊥ D1 , ⊥ D2 ) lub D1⊗D2 h def = (lub D1 (fun n m ⇒ fst (h n)), lub D2 (fun n m ⇒ snd (h n)))
The projection and pairing functions are continuous, we have defined

• FST : ∀D 1 D 2 , D 1 ⊗ D 2 C → D 1 SND : ∀D 1 D 2 , D 1 ⊗ D 2 C → D 2 ; • PAIR : ∀D 1 D 2 , D 1 C → D 2 C → D 1 ⊗ D 2 .
We also defined functions for currying and uncurrying

• CURRY : ∀D 1 D 2 D 3 , ((D 1 ⊗ D 2 ) C → D 3 ) C → D 1 C → D 2 C → D 3 , • UNCURRY : ∀D 1 D 2 D 3 , (D 1 C → D 2 C → D 3 ) C → (D 1 ⊗ D 2 ) C → D 3 .
Indexed product D For modeling Kahn networks, it is useful to have a generalized product over an arbitrary number of cpos.

We take a set I of indexes and a family D of cpos indexed by I, that is, D : I → cpo. The cpo structure for the product written D is just a dependent generalization of the function type I o → D in which the domain D may depend on the index. When D is a type expression depending on a free variable i, we write i D for (fun i ⇒ D)

• Carrier: ∀i : I, D i • Order: x ≤ ΠD y def = ∀i, x i ≤ D i y i • Least element: ⊥ ΠD def = fun i ⇒ ⊥ D i • Least upper bound: lub ΠD h def = fun i ⇒ lub D i (fun n m ⇒ h n i)
The interesting constructions on that structure are

• a projection function PROJ of type: ∀i : I, ( D) C → D i
• given two indexed families D and D ′ over the set I, the mapping MAPi of a continuous function on the elements of an indexed product has type (∀i, Di

C → D ′ i) → D C → D ′ and is defined such that MAPi f p i = f i (p i).
• An operation to lift the indexes. Assume that we have two sets of indexes I and J, a family D of cpos indexed by I, and a function f : J → I.

We define a continuous function LIFTi of type D C → j D (f j) such that LIFTi p j = p (f j). It allows to select, reorganize or duplicate the elements in the product.

Finite product D k It is also useful to have a finite product on the same cpo D. Given k : nat, one possibility is to take the function space {i|i < k} O → D, but in that case we will have to deal with the subset type in Coq which is not always convenient. Instead we take the type nat → D but instead of the pointwise order for functions, we introduce an order up-to k: f ≤ g def = ∀n, n < k → f n ≤ g n. We write k → D for the cpo structure with this order. The least element is defined pointwise. For the lub, there is a small difficulty. The natural definition would be:

lub k→D h n = lub D (fun p m ⇒ h p n)
But (fun p ⇒ h p n) is monotonic only when n < k. However, the value of lub k→D h n for k ≤ n is meaningless so we can choose an arbitrary one. Consequently we introduce h ′ such that h ′ p n = h p n when n < k and ⊥ otherwise. Then taking:

lub k→D h n = lub D (fun p m ⇒ h ′ p n)
gives us the expected properties.

Fixpoints

Given a cpo structure D and a monotonic function

F of type D m → D, we can define a monotonic function (iter F ) of type nat m → D such that iter F 0 = ⊥ and iter F (n + 1) = F (iter F n).
We define the fixpoint of F as the least-upper bound of this sequence:

fixp F def = lub (iter F ).
The constant fixp has type (D

m → D) → D.
It is itself a monotonic function. It is easy to show that fixp F ≤ F (fixp F ). The equality fixp F == F (fixp F ) is provable under the assumption that F is a continuous function.

We can also show that fixp is a continuous function from the cpo (D

FIXP F = fixp (fun x m ⇒ F x) FIXP F == F (FIXP F ).
Scott's induction principle We proved Scott's induction principle. A predicate is said to be admissible if it is true for the lub of a monotonic sequence when it is true for all the elements of the sequence:

admissibleP def = ∀f : nat m → D, (∀n, P (f n)) → P (lub f
). Scott's induction principle states that when a predicate is admissible, if it is true for ⊥ and preserved by a monotonic function F : D m → D, then it is true for the fixpoint of F :

∀P, admissible P → P ⊥ → (∀x, P x → P (F x)) → P (fixp F )
Minimality It is easy to prove that the fixpoint of a monotonic function is the minimal solution for the equation. Namely:

∀(F : D m → D)(x : D), F x ≤ x → fixp F ≤ x.

The cpo of streams

We now want to define a cpo structure for concrete data types. Before developing the construction for streams, we show the simpler case of a flat cpo, which illustrates the main ideas.

The flat cpo

The simplest nontrivial (i.e., not reduced to ⊥) cpo is the flat domain. Given a type A, we add an extra element ⊥ and we have x ≤ b if and only if x = ⊥ or x = b.

A natural solution could be to take as the carrier for this cpo the option type on A with values either None or Some a with a : A.

Inductive option (A:Type) : Type := None : option A | Some : A → option A

The constant None will be the least element. However we cannot define constructively a least upper bound. Indeed, given an increasing sequence of elements in our domain, we would have to decide whether all the elements are ⊥ in which case the lub is ⊥ or if there exists an element in the sequence which is of the form Some a in which case the lub is this element. Because we follow a constructive approach in Coq where functions correspond to algorithms, we cannot define a function which takes such a decision. The computation of lubs is possibly an infinite process, a solution to represent infinite computations in Coq is to use coinductive types. This is the approach taken by V. Capretta [START_REF] Capretta | General recursion via coinductive types[END_REF] for dealing with general recursive functions in Eps ∞ will be our least element and we need to identify all the representations of the value a ignoring the Eps constructors.

In order to achieve that, we define co-inductively the order on the flat domain with these three rules:

x ≤ y Eps x ≤ Eps y x ≤ Val a Eps x ≤ Val a y = Eps n (Val a) Val a ≤ y
From this definition we proved reflexivity, transitivity and properties like

Eps ∞ ≤ x or Val a ≤ x → x == Val a.
We can now look at the construction of lubs. We have a monotonic sequence h of elements in flat A and we want (constructively) to build the least upper bound which can be either ⊥ or a value.

If x is an element of flat A, we write [x] n for the same element but removing the n-th first Eps constructors (or less if we find a value before). We have x == [x] n . Now in order to build the least upper bound, we look at h 0. If we find a value then we have our bound; if not, we produce an Eps and we continue by looking at [h 0] 1 ; [h 1] 1 if we find a value then we are done, if the elements start with an Eps then we produce an Eps in the least upper bound and we continue. At the n-th step we look at the sequence [h 0] n ; [h 1] n ; . . . ; [h n] n , we try to find a direct value, otherwise we produce an Eps step and continue. This mechanism is illustrated in the figure 3; the Coq formalisation will be given in the more involved case of streams. If one of the elements (h k) in the sequence is a value, then there exists n such that [h k] n = Val a so we will eventually find this value before the p-th step with k ≤ p and n ≤ p.

Streams

We now look at the case of streams which is developed following the same kind of reasoning. As before Eps ∞ can be coinductively defined by Eps ∞ = Eps Eps ∞ . It represents the empty stream and is also our ⊥ element. We define a function [ ] n removing Eps in front of the stream by induction on n and case analysis on the stream.

[s] 0 = s

[Eps x] n+1 = [x] n [cons a x] n+1 = cons a x

Order

The order we consider on streams is the prefix order, we must also ignore the Eps steps which correspond to silent computations.

x ≤ y Eps x ≤ y

[y] n = cons a z x ≤ z cons a x ≤ y
The idea is that in order to show that x ≤ y, there are two cases: if x is Eps x ′ then we try to show x ′ ≤ y, if x is (cons a x ′ ) then after a finite number of Eps, y should be of the form (cons a y ′ ) and we need to show that x ′ is less than y ′ . We do not know how many Eps steps we should remove so we cannot decide whether x ≤ y or not, and similarly we cannot decide whether a stream is finite or not. This corresponds well to the vision of the streams as a model of asynchronous communication links: it is not possible to know if more information will arrive and when. If we want to transmit a finite number of elements, we have to decide on a special character to indicate the end of the data.

Decidability of the empty stream is not required for the development we want to perform and it is the price to pay for having an explicit computation of lubs and fixpoints.

We can prove the expected properties of the order besides reflexivity and transitivity :

• Eps ∞ ≤ x • ¬(cons a x ≤ Eps ∞ ) • cons a x ≤ cons b y ↔ a = b ∧ x ≤ y
Equality As in other ordered structures, equality on streams x == y is defined as x ≤ y ∧ y ≤ x. It is important to distinguish this equality from intensional equality in Coq: x = y means that x and y are structurally equal. For instance we have x == Eps x for all x while x = Eps x is only true for the Eps ∞ stream.

Simulation properties

Coinductive definitions in Coq correspond to greatest fixpoints. The primitive way to build a proof of x ≤ y is to use fixpoint definitions in Coq, which should be guarded. This guarded condition is very syntactic and not always convenient to use in tactics. An alternative way is to define a co-induction principle which in this case corresponds to a simulation principle.

We introduce a principle which does not rely on the intensional representation of streams. We have to find a relation R on streams that is compatible with equality on streams and such that when R x y holds and x is equal to a stream cons a x ′ then y is also equal to cons a y ′ and R x ′ y ′ also holds. If such an R exists then it is included in the relation ≤ on streams. This principle can be written as follows:

∀x y z t, x == z → y == t → R x y → R z t ∀a x y, R (cons a x) y → ∃z, y == cons a z ∧ R x z ∀x y, R x y → x ≤ y
From this we can derive a principle which says that in order to prove x ≤ y, it is enough to prove it in the particular case where x == cons a x ′ . This principle is in practice sufficient in order to avoid reasoning on whether x is the empty stream or not.

Least upper bounds

Destructuring streams We introduce a predicate is cons on streams. It is defined as an inductive predicate with two constructors is cons x → is cons (Eps x) and is cons (cons a x). We can prove that is cons x is equivalent to ∃a s, x == cons a s.

In Coq is cons is a noninformative proposition: we know the existence of a and s but we cannot use a and s to compute a value. However if we know that a stream contains a cons constructor, the algorithm that removes Eps constructors will eventually stop on a cons constructor. In Coq, we defined a function uncons of type: ∀x, is cons x → {a : A&{s : Str A|x == cons a s}}.

From the computational point of view, this function takes a (nonempty) stream as input and returns a pair (a, s) of its head and tail plus the proof that x == cons a s. Technically, the function uncons is defined in Coq by a fixpoint doing a structural induction on the proof of (is cons x) and a case analysis on the structure of x.

Building lubs The construction of lubs for monotonic sequences of streams is a generalization of the idea used in the case of flat domains.

Consider a monotonic sequence h of streams, and a natural number n. We can look at the first constructor of h 0 . . . h (n -1). Either we only have Eps steps or there exists m < n such that h m = cons a s. In this last case, the lub will start by cons a and we know that for all p ≥ m, the stream h p is equal to cons a s ′ (because h m ≤ h p) such that we can extract a subsequence of h corresponding to the tails of h p and recursively find the lub of this sequence. Following this idea, we built a function fCon which takes as argument a sequence of stream h and a natural number n and either answers that all h m starts with Eps for all m < n or find an element a and another sequence h ′ such that there exists m < n that all h (k + m) is equal to cons a (h ′ k). Formally the Coq type of fCon is:

∀(h : nat m → Str A)(n : nat), {a : A & {h ′ : nat m → Str A| ∃m, m < n ∧ ∀k, h (k + m) == cons a (h ′ k)}} + {∀m, m < n → h m = Eps( )}
This function is defiend by structural recursion on n.

We The lub of a stream sequence h is just defined as (lubn h 1). We proved that this is the lub of the sequence of streams.

Useful functions on streams

In his paper, Gilles Kahn introduced several functions to manipulate streams: taking the first element, the stream without the first element or the concatenation of the first element of a stream to another.

All these functions are proved to be continuous. In our development, we derive them from the more general scheme of a function from streams to streams defined by case analysis on the structure of the input stream. If the input is equal to cons a x then the result is computed from a and x by a given function

F , if it is Eps ∞ then the result is Eps ∞ . Let a parameter function F have type A → StrA m → StrB.
The function that we named case is coinductively defined by:

case F (Eps x) = Eps (case F x) case F (cons a x) = F a x
It is easy to check that case F ⊥ == ⊥ and that x == cons a y

→ case F x == F a y. When F is a continuous function of type A → StrA C → StrB, then case (fun a s c ⇒ F a s) is also a continuous function of type StrA C → StrB.
The case construction is also continuous with respect to the argument F , such that we can build

CASE of type (A O → StrA C → StrB) C → StrA C → StrB.
From this scheme, we derive the following functions:

• first has type Str A → Str A and is defined by: We remark that app x y only takes the first element of x, and adds it in front of y. It corresponds to the "followed by" operation in synchronous data-flow languages and not to the usual append function on lists which cannot be defined in that framework.

We also build their continuous versions: FIRST and REM of type

Str A C → Str A and APP of type Str A C → Str A C → Str A
We proved the properties which are given by Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF]:

first ⊥ == rem ⊥ = app ⊥ x == ⊥ first x == app x ⊥ x == app (first x) (rem x)
Instead of x = ⊥∨rem (app x y) == y in Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], we proved that is cons x → rem (app x y) == y.

We also proved that app (first x) y == app x y.

Bisimulation revisited Using the rem function, it is possible to express a bisimulation principle. In order to prove that two streams are equal, it is sufficient to find a relation R which is stable by equality, which implies equality on first elements and is preserved by remainders for nonempty streams. Such a relation R is included in equality:

∀D (R : Str A → Str A → P rop), (∀x 1 x 2 y 1 y 2 , R x 1 y 1 → x 1 == x 2 → y 1 == y 2 → R x 2 y 2 ) → (∀x y, (is cons x ∨ is cons y) → R x y → first x == first y) → (∀x y, (is cons x ∨ is cons y) → R x y → R (rem x) (rem y)) → ∀x y, R x y → x == y.

Mapping and filtering

Mapping A useful functional on streams is to apply a function F : A → B to any element of a stream of A in order to obtain a stream of B.

We easily build this function using our fixpoint construction and case analysis.

We first build a function Mapf of type (Str

A C → Str B) C → A O → Str A C → Str B such that Mapf f a s = cons (F a) (f s).
Then we introduce MAP Of course, we could have defined map directly in Coq using a guarded fixpoint (a fixpoint where recursive calls are directly under a constructor) on the coinductive type Str A which satisfies the following equations:

map (Eps x) = Eps (map x) map (cons a x) = cons (F a) (map x)
Proving monotonicity and continuity of this function requires specific co-recursive proofs. Our definition using FIXP and CASE gives us these results directly without extra work.

Our technique applies to recursive definitions of functions on streams which do not directly correspond to guarded fixpoints like the filter function.

Filtering. Filtering is an operation that selects elements of a stream that satisfy a given (decidable) property P . This operator has been widely studied because it is the typical example of a nonguarded definition on co-inductively defined infinite streams.

Using p of type A → bool to decide the property P , a definition in an Haskell-like language would be: filter p (cons a s) = if p a then cons a (filter p s) else filter p s

The problem is that if P only holds on a finite number of elements of the stream then the output is finite and there is no way to decide that. Y. Bertot [START_REF] Bertot | Filters on coinductive streams, an application to eratosthenes'sieve[END_REF] proposes a solution where there is an inductive proof that P holds infinitely many times in the input and this is used to produce an infinite stream as output. An alternative solution is to produce as output an infinite stream of values which are either a real value or a dummy constant.

With our representation of streams, we can simply define the stream in a similar way as for the map function using case analysis and fixpoint. We introduce Filterf p of type (Str

A C → Str A) C → A O → Str A C → Str A such that Filterf p f a s = if p a then cons a (f s) else f s.
Then we introduce FILTER p filter p (cons a s) == if p a then cons a (filter p s) else filter p s

Finiteness

We can define what it means for a stream to be finite or infinite. As usual, infinity is defined co-inductively and finiteness is an inductive predicate. We defined them the following way: We were able to prove

• s ≤ t → infinite s → infinite t • s ≤ t → finite t → finite s.
This property is not provable if we take a different version of finite with an extra hypothesis (is cons s) in the constructor fin cons. With such a definition of finite, a proof of finite t is isomorphic to the number of cons in t. Assuming s ≤ t, a proof of finite s should give us the exact number of elements in s, but there is no way to explicitely compute this number. With our definition of finite, a proof of finite s just gives us an upper bound of the number of cons in the stream and is consequentely compatible with the order on the streams.

• finite s → ¬infinite s

The particular case of natural numbers

We put an ordered structure on the type nat of natural numbers but this is not a cpo because there is no lub for the sequence h n = n. If we want a cpo structure, we need to add an infinite element. One way to define a cpo for natural numbers reusing our previous library is to take the type of streams on the trivial type unit with only one element tt : unit. The 0 element will be Eps ∞ as before, the successor function will be S x def = cons tt x. We can define the top element S ∞ with the cofixpoint S ∞ = S S ∞ and prove ∀x, x ≤ S ∞ .

We write Nat for this cpo. There is an obvious monotonic function from nat to Nat.

This domain is used in order to define the length function from Str A to Nat. It is just an application of the map construction with the functional funa ⇒ tt. We were able to show the following properties:

• ∀s : Str A, infinite (length s) ↔ infinite s • ∀n : Nat, S n ≤ n → infinite n
In the case of streams, we defined the append of streams x and y, just taking the first element of x (if it exists) and putting it in front of y. There is no way to define the usual append function on lists such that the concatenation of the empty stream and y is y, because we never know if x is empty by just looking at a finite prefix.

The situation is a bit different for the cpo of natural numbers where the concatenation corresponds to addition. When trying to add x with y we might look alternatively at the head part of x and y. Whenever we find a successor, we can produce a successor on the output. If one of x or y is 0 then we will always find Eps step on this input and the output will be equal to the other argument with just extra Eps steps inserted.

Following this idea, we have been able to define the addition as a continuous function on Nat and prove that it is commutative and that add n 0 == n.

Kahn networks

We shall now explain our representation of Kahn networks in Coq.

Representing nodes

.

We define a shallow embedding of nodes. A node with inputs of type A 1 , . . . , A n and outputs in types B 1 , . . . , B p is a continuous function of type

i Str A i C → j Str B j .
In general we allow arbitrary sets of indexes I for inputs and J for outputs. We associate with each index a type family A : I → Type and B : J → Type, a node of signature A B is an element of i Str (A i)

C → j Str (B j).
We distinguish the particular case of a simple node with only one output. Given a set of indexes I for inputs, a type family A : I → Type and a type B, we define a simple node of signature A B to be an element of i Str (A i)

C → Str B.
A node with several outputs can just be seen as a set of simple nodes, each one corresponding to the projection on the corresponding output.

Representing systems

We start from a concrete set of edges and we distinguish input edges (given by a type I) from the other ones (given by a type J). We consider all the noninput edges to be output edges, it is not relevant for the system which outputs we want to observe.

We associate with each edge a type, so we have a type family A : I + J → Type. The type I + J is the disjoint union of I and J. We write (l i) (resp. (r j)) for the element of I + J associated with i : I (resp. j : J).

We define SA def = fun i ⇒ Str (A i) the type family indexed by I + J of streams of elements of type A i and SA I def = fun i ⇒ SA (l i) the type family indexed by I associated with the inputs. Now each edge which is not an input edge has a source which is a node. Actually each edge is associated with one particular output of the source node. We already mentioned that a general node with n outputs is equivalent to n simple nodes.

In our model, each noninpu edge is associate to one simple node (its source). A simple node in general is a function

f of type k∈K Str A ′ k C → Str B.
We have to link the inputs of the node (indexed by K) with the edges of the system. This corresponds to producing a function σ : K → (I + J) which is compatible with the type system (i.e., A ′ k is convertible with A (σ k)). Given f and σ, we could use the DLIFTi operation introduced in paragraph 3.2.2 in order to build a function f ′ of type SA C → Str B, which can also be seen as a simple node but taking all the edges of the system as input. Instead of introducing for each node the extra level of indirection with the set K and the map σ : K → (I + J), we directly consider that an output edge is associated with a (simple) node of the system which is a continuous map taking all streams associated with an edge as input, i.e., an element of SA C → Str B. This gives us a very simple and uniform definition of the type of systems that we describe now.

A system with input edges I and output edges J of type A : I + J → Type is an object of type:

system A def = ∀j : J, ( SA) C → Str (A (r j))
The set of systems has a cpo structure corresponding to an indexed product

j ( SA C → Str (A (r j))).
Equation associated with a system A system defines an equation on the streams associated with the edges, provided we give values for the input edges.

Formally if we have a system s on a type family A : I + J → Type as before and an input inp which is a product of streams on I such that inp has type SA I , then we can define the set of equations as a continuous function (EQN of system s inp) of type SA

C → SA such that EQN of system s inp X (l i) = inp i EQN of system s inp X (r j) = s j X
Taking the fixpoint of this function gives us the output observed on all the edges. This function EQN of system is monotonic and continuous with respect to both the system and the input arguments. It has type:

system A C → SA I C → ( SA C → SA).
The solution of this equation for a system s and an input inp is obtained by taking the fixpoint of the functional (EQN of system s inp). It is still a continuous function both of the system of the inputs, so we obtain for each system s, a new node SOL of system s of type ( SA I ) C → ( SA) such that: SOL of system s inp == EQN of system s inp (SOL of system s inp). In the examples, we shall only be interested by one output o : J which is simply obtained by applying SOL of system s inp to (r o).

Remarks

There are a few differences between our formalization and Kahn's original definition [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF].

• Kahn defined a node as a continuous function, associated with edges for its inputs and outputs. In our formalism, we have the association between the edges and the output of a node but nothing on the link between the input of the node and the edges. The nodes are implicitly related to all edges. In practice, as we shall see in the examples, we shall start with a node defined as a continuous function with the appropriate number of arguments corresponding to the number of input edges in the node. Then, when defining the system, we simply project the relevant edges of the system on the corresponding inputs of the node.

• A noninput edge in our systems has one source node but may have several target nodes. This avoids the explicit use of duplication nodes which is discussed as a possible harmless extension in Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF].

6 Examples

A simple example

We illustrate our approach with the same running example as in Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF].

Definition

We first draw in figure 4 the graphical scheme corresponding to the network.

h 0 f h 1 g Z Y T 1 T 2 X Figure 4: A simple example of Kahn network
The edges are X, Y , Z, T 1 , and T 2 . There is no input edge so the set I is defined as the empty type. The set J is an enumerated set with elements X, Y , Z, T 1 , and T 2 . All the links contain values in type nat such that the type family A : I + J → Type is defined by A k = nat and we have SA k = Str nat.

The functions corresponding to the nodes are f , g and h. The node g has two outputs corresponding to the functions g 1 and g 2 . They satisfy the equations:

• f U V = app U (app V (f (rem U ) (rem V ))) • g 1 U = app U (g 1 (rem (rem U ))) • g 2 U = app (rem U ) (g 2 (rem (rem U ))) • h n U = cons n U
In Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], the equations involve an extra first application in the first argument of app, but because we proved: app (first x) y == app x y, we can eliminate it.

In order to define these nodes, we use the fixpoint construction and the composition of the (continuous) functions app, rem and cons on streams.

The system itself (called sys) is translated from the scheme in the figure 4 which can also be seen as the set of equations:

X = f Y Z Y = h 0 T 1 Z = h 1 T 2 T 1 = g 1 X T 2 = g 2 X
In Coq, sys is a function from J to the continuous functions from SA C → Str nat. Given p of type SA, we have:

• sys X p = f (p (r Y )) (p (r Z))
• sys Y p = h 0 (p (r T 1 ))

• sys Z p = h 1 (p (r T 2 )) • sys T 1 p = g 1 (p (r X)) • sys T 2 p = g 2 (p (r X))
Now the resulting stream (called result) of type (Str nat) is obtained the following way:

1. The solution sol of the system sys has type SA I C → SA.

2. Because I is empty, the type SA I containts a trivial element inp, we apply sol to inp and get an object of type SA.

3. The object sol inp X that is the projection of the previous system on the link X is the expected result.

Properties

Kahn's paper proves that the result is an infinite stream containing alternatively 0 and 1. For that he proves: result == cons 0 (cons 1 result). This is done in two steps, first he proves that result satisfies the following fixpoint equation:

result == cons 0 (cons 1 (f (g 1 result) (g 2 result)))
then proves that f (g 1 s) (g 2 s) == s.

The first equation is a consequence of two general properties of fixpoints:

1. A fixpoint on a continuous function is stable by composition: FIXP f == FIXP (f @ f ) == FIXP f n+1 . This is a consequence of a general lemma about fixpoint of composition of continuous functions:

∀(f g : D C → D), g@ f ≤ f @ g → f (FIXP g) ≤ FIXPg → FIXP(f @ g) == FIXP g 2.
Fixpoint on products can be simplified when the output on an index i depends only on the input on the same index i:

∀(I : Type)(D : I → cpo)(F : D C → D)(i : I)(F i : D i C → D i), (∀p : D, F p i == F i (p i)) → FIXP F i == FIXP F i .
We take the equation EQN sys of type SA C → SA associated with the system sys together with the empty input stream and we compose it three times. We obtain the equation:

EQN sys 3 p (r X) = f (h 0 (g 1 (p (r X)))) (h 1 (g 2 (p (r X)))).
Consequently the stream result which is the fixpoint of EQN sys on the output X is also the fixpoint of EQN sys 3 on the output X and is also the fixpoint of F X with F X s = f (h 0 (g 1 s)) (h 1 (g 2 s)). Using the definition of f and h, it is easy to see that: F X s == cons 0 (cons 1 (f (g 1 s) ( g 2 s)).

What remains to be proved is that ∀s, f (g 1 s) (g 2 s) == s. Kahn's paper uses a structural induction which is not appropriate because the stream s is possibly infinite. Instead we use a bisimulation technique.

We use a variation of the bisimulation principle given in section 4.2.4 which is:

∀D (R : Str A → Str A → Prop), (∀x 1 x 2 y 1 y 2 , R x 1 y 1 → x 1 == x 2 → y 1 == y 2 → R x 2 y 2 ) → (∀x y, (is cons x ∨ is cons y) → R x y → first x == first y) → (∀x y, (is cons (rem x) ∨ is cons (rem y)) → R x y → first (rem x) == first (rem y)) → (∀x y, (is cons (rem x) ∨ is cons (rem y)) → R x y → R (rem (rem x)) (rem (rem y))) → ∀x y, R x y → x == y.
We instantiate this principle by the relation R s t def = t == f (g 1 s) (g 2 s). The proof is based on algebraic properties of f , g 1 , g 2 , rem, and first.

We end up with the expected property result = cons 0 (cons 1 result) from which we deduce that result is an infinite stream because its length is infinite.

Sieve of Eratosthenes

The scheme corresponding to the sieve of Eratosthenes was given in figure 2 in section 2. What is interesting is that it is a recursive scheme. The scheme defines a node sift which is used as an internal node in the scheme itself. This is done using a fixpoint construction which is possible because the interpretation of a scheme is a continuous function of the nodes themselves.

The node fdiv is easily built using case and filter such that: fdiv (cons a s) = filter (div a) s

We introduce the input index type I which is just a type with one element i and the output index type J which contains 3 elements X, Y and o. All the links have type nat, so using the same notation as before we introduce

A : I + J → Type, SA : I + J → cpo, SA I : I → cpo such that A k = nat, SA k = Str nat and SA I i = Str nat.
We define the functional Fsift associated with the recursive system which has type (Str nat C → Str nat) C → system A and is defined by case on the output link with p of type SA:

Fsift f X p = fdiv (p (l i)) Fsift f Y p = f (p (r X)) Fsift f o p = app (p (l i)) (p (r Y ))
The construction SOL of system introduced in section 5.2 gives us a continuous function from systems to functions of type SA I C → SA from the streams corresponding to input edges to the streams corresponding to all edges.

The composition of SOL of system with Fsift gives us a continuous function from (Str nat We can prove, using the fixpoint equation for sift, the following equality:

sift == focus (SOL of system A (Fsift sift)).

Using the fixpoint equation for: SOL of system A (Fsift sift), it is easy to derive successively the following equalities for all stream s:

• SOL of system A (Fsift sift) (pair 1 s) (l i) == s. • SOL of system A (Fsift sift) (pair 1 s) (r X) == fdiv s.
• SOL of system A (Fsift sift) (pair 1 s) (r Y ) == sift (fdiv s).

• SOL of system A (Fsift sift) (pair 1 s) (r o) == app s (sift (fdiv s)).

From these equalities, the property of fdiv, and the fixpoint equality for sift we easily deduce the expected property of sift:

sift (cons a s) == cons a (sift (filter (div a) s)) sift ⊥ == ⊥ 7 Conclusion

Contributions

This paper describes three contributions.

The first one is a general Coq library for ω-cpos. This is a constructive version of cpos where there is an explicit function to build the least-upper bound of any monotonic sequence. It contains useful constructions such as generalized products, cpos of monotonic and continuous functions and combinators to manipulate them. It also introduces a fixpoint combinator. This library has also been used in a Coq library for modeling randomized programs as distributions [START_REF] Audebaud | Proofs of randomized algorithms in Coq[END_REF][START_REF] Audebaud | Proofs of randomized algorithms in Coq[END_REF].

The second contribution is the definition of the cpo of streams of elements in a type A. This type, defined co-inductively, covers both the case of finite and infinite streams but without any explicit way to decide if the stream is finite or not. The type itself is not very original, it corresponds to an infinite stream with values which can be present or absent. What is interesting is the order defined on that data structure and the derived equality. Modulo this equality, we are able to reason on this data structure by only considering the interesting cases where the streams are equal to (cons a s). The most difficult construction on the type of streams was the least-upper bound. The fixpoint given by the cpo structure makes it possible to define in a natural way a function like filter that selects the elements of a stream satisfying a predicate P . This function is problematic with most representations of streams in Coq because the output can be finite or infinite depending on the number of elements in the input which satisfies P .

The last contribution is the modeling of Kahn networks as they are described in the paper [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF]. We chose a shallow embedding where a system is represented using a set of links and for each noninput link a continuous function corresponding to the node. Each node can possibly take as input all the links of the system. This leads to a very simple and uniform definition of systems which itself can be seen as a cpo.

A system together with streams for inputs defines a continuous function on the streams associated with the links of the system (the history of the system). The fixpoint of this function defines the behavior of the system as a continuous function both from the inputs and the system.

Using this interpretation, we were able to formalize both the main example given by Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] and the sieve of Eratosthenes, an example of a recursive scheme which was presented by Kahn and MacQueen [START_REF] Kahn | Coroutines and networks of parallel processes[END_REF]. What is mainly missing is a syntactic facility in order to automatically build complex continuous functions by composition of simpler functions and functionals.

Remarks

Synchronous case. As we mentioned before, one important application of Kahn networks is their restriction to synchronous languages where no buffer is needed to store the values on the links. The nodes receive the inputs at a regular time given by a clock and instantaneously produce an output. A denotational semantics of this calculus in Coq was given by Boulmé and Hamon [START_REF] Boulmé | Certifying Synchrony for Free[END_REF]. Their approach is to make the type of the stream dependent on the clock (which is an infinite stream of boolean values), so there is a control on which data is available or not. They do that by considering ordinary infinite streams (only the cons constructor) with values which can either be an ordinary value in the type A of elements, or an absent value (when the clock is off) or a failure (no value when the clock is on).

We could adapt our development to this particular case by extending the definition of streams to make them dependent on the clock. Then in order to define the bottom element of a stream on a clock c, it is convenient to have a bottom element in the type A. So the natural framework is to consider a cpo structure on A. Then the order on the streams can be defined the following way (the clock argument of constructors Eps and cons can be derived from the type of the stream so it is left implicit in the Coq notation).

CoInductive

x ≤ y Eps x ≤ Eps y a ≤ b

x ≤ y cons a x ≤ cons b y It is simpler than in our case because we know exactly where the cons constructors are. The construction of lubs is also simplified, when the clock is true, there is a cons constructor in each element of the sequence of streams, we produce a cons constructor in the output with a value corresponding to the lub of the heads. However some extra properties have to be proved on the sequence if we want to ensure that there is no cons ⊥ left in the result.

Equations. Kahn's paper refers to the paper of Courcelle, Kahn and Vuillemin [START_REF] Courcelle | Algorithmes d'équivalence et de réduction à des expressions minimales dans une classe d'équations récursives simples[END_REF] which proves the decidability of equivalence in a language of fixpoints. We started to write a Coq version of this paper and in particular we defined the notion of terms and built the cpo corresponding to the canonical interpretation of equations built on sequences of terms. But the full formalization of this part still remains to be done.

Figure 2 :

 2 Figure 2: A Kahn network for the Sieve of Eratosthenes

1 m→ D 2

 12 structure is implicitly identified with the underlying ordered structure. In particular, if D 1 and D 2 are two cpo structures, we can write D for the ordered structure of monotonic functions from D 1 to D 2 . Continuity It is easy to show from the properties of lub that given D 1 and D 2 two cpo structures, F : D 1 m → D 2 a monotonic function from D 1 to D 2 and f a monotonic sequence on D 1 , we have

  write A O → D for the cpo of simple functions from A to D. Given an ordered type O, it is easy to show that ⊥ O→D is a monotonic function and that lub preserves monotonicity. So we have a cpo structure written O M → D on the type of monotonic functions. If D 1 and D 2 are two cpo structures, then because ⊥ D1 m

C

  → D) of continuous functions on D to D. Consequently, we are able to define FIXP of type (D C → D) C → D, such that for all F of type D C → D:

  Coq. The solution is to introduce: CoInductive flat (A:Type) : Type := Eps : flat A → flat A | Val : A → flat A A value in type flat is either finite of the form n Eps (. . . (Eps (Val a)) . . .) (written Eps n (Val a)) in which case it represents the value a (with extra Eps steps corresponding to silent computations) or an infinite object Eps ∞ coinductively defined by Eps ∞ = Eps Eps ∞ corresponding to a diverging computation.

Figure 3 :

 3 Figure 3: Computation of lubs in a flat domain

  write [h] def = fun n m ⇒ [h n] 1 for the sequence h where we have removed the first Eps step of each stream, our lub function is defined with a cofixpoint: CoFixpoint lubn (h:nat m → Str A) (n:nat) : Str A := match fCon h n with (a,h',_) ⇒ cons a (lubn h' 1) | ⇒ Eps (lubn [h] (n+1)) end This recursive function is accepted by Coq because it is a guarded fixpoint: any recursive call in the body appears under a constructor of the type of streams.

=

  case (fun a s m ⇒ cons a ⊥) • rem has type Str A → Str A and is defined by: rem def = case (fun a s m ⇒ s) • app has type Str A → Str A → Str A and is defined by: app x y def = case(fun a s m ⇒ cons a y) x.

def=→

  FIXP (CASE @ Mapf) of type Str A C Str B and map the underlying function of type Str A → Str B. From the properties of FIXP, CASE and Mapf, we obtain easily the expected equalities: map ⊥ == ⊥ map (cons a s) == cons (F a) (map s).

def=

  FIXP (CASE @ (Filterf p)) of type Str A C → Str A and (filter p) the corresponding function of type Str A → Str A. We easily check the expected property:

  Inductive finite (s:Str A) : Prop := fin bot : s ≤ ⊥ → finite s | fin cons: finite (rem s) → finite s. CoInductive infinite (s:Str A) : Prop := inf intro : is cons s → infinite (rem s) → infinite s.

  Now if we are only interested by a subset O of the output nodes, we use a mapping π : O → J and we use again the lift function in order to restrict our solution to a node indexed by I for inputs and O for outputs of type ( SA) C → ( o:O SA (r (π o))).

C→→→→

  Str nat) to SA I C → SA. Now the recursive graphical construction of the system says that sift is the functional corresponding to the input i and the output o.Using pair 1 (the continuous trivial function from D to i∈I D when I has only one element), it is easy to build a continuous function focus of type ( Str nat such that focus h s = h (pair 1 s) o.The composition of focus, SOL of system and Fsift is now a continuous function from (Str nat C Str nat) to (Str nat C Str nat). We introduce sift as the fixpoint of this operator.

Coq

  development The Coq development runs with Coq version 8.1 [15] currently under development. It makes an intensive use of the new setoid rewriting tactic. It is available from the author's web page. It contains approximately 1700 lines of definitions and statements and 3000 lines of proofs. The Coq notation mechanism as well as implicit arguments makes it possible to keep notations in Coq quite similar to the ones used in this paper.

  Str A :clock → Type := Eps : ∀ c, Str A c → Str A (false::c) | cons : ∀ c, A → Str A c → Str A (true::c)

we introduce the type of monotonic functions from O 1 to O 2 . Elements of this type are records with a function f of type O 1 → O 2 (formally from the carrier of O 1 to the carrier of O 2 ) and a proof that this function is monotonic. With the pointwise order on functions, this type is an ordered structure written O 1 m → O 2 . If an object f has type O 1 m

  Given two ordered structures O 1 and O 2 ,

In Type theory, there is a natural polymorphic equality called Leibniz equality which corresponds to convertibility and which allows rewriting in an arbitrary context. This equality is sometimes too strong. It is also possible to associate with a type a specific equivalence relation. The type together with the relation is called a setoid. The relation can be used pretty-much like an equality for rewriting, but only under a context built using operators which are proved to preserve the setoid relation. Coq offers facilities to manipulate the setoids.


Alizé Mouchard

Charles Le Bras

Olivia Ménard

Lucie Rault

Marie-Françoise Cochet

Impact of neonatal digestion on the physiology of breast milk bacteria and their immunomodulation capacities

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Centre

Bretagne -Normandie

Impact of neonatal digestion on the physiology of breast milk bacteria and their immunomudulation capacities

CONTEXT & AIM STRATEGY

RESULTS

Impact of digestion on the bacterial cultivability

 Exclusive breastfeeding in the first months of life has protective effects on infant health compared to formula-fed infants including, in the short term, a lower risk of gastrointestinal and respiratory infections and, in the long term, a lower risk of metabolic and immune disorders [1] .

 The highly diversified microbial counterpart of breast milk could contribute to its health benefits compared to infant formula (IF), due to its role in the development of the infant gut microbiota and possible impact on gut homeostasis [1] .

 The aim of this study was to evaluate the impact of newborn digestion on the physiology of breastmilk bacteria and on their immunomodulatory potential.  The strains were digested in an infant formula matrix, using a static in vitro model of digestion.

CONCLUSION & PERSPECTIVES

Following the gastric and intestinal phases of digestion, bacterial cultivability was assessed as well as the immunomodulation profile through the quantification of IL-10 (anti-inflammatory cytokine) and TNFα (pro-inflammatory cytokine) released by the macrophage THP-1 cell line (Figure 1)

Impact of digestion on the immunomodulatory potential of bacteria

Cutibacterium acnes Staphylococcus epidermidis

Lactobacillus gasseri Bifidobacterium breve

Streptococcus salivarius Enterococcus faecalis

 Variation in the impact of digestion on strain cultivability  Four out of six strains were only slightly affected  E. faecalis showed an increased cultivability after the double digestion, while two strains, L. gasseri and B. breve, were more strongly impacted by the intestinal phase of digestion.

Figure 1 :

 1 Figure 1 : Strategy to evaluate the impact of digestion on the selected strains

Figure 2 :Figure 3 :

 23 Figure 2 : Evolution of the concentration of cultivable bacteria during digestion. The concentration was corrected by the volume at each phase of digestion. B = Before digestion; G = After gastric phase; I = After intestinal phase. Results were obtained using an analysis of variance model (ANOVA and tuckey significant difference test). '****' p-value = 0.0001; '***' p-value = 0.001; '***' p-value = 0.001; '**' p-value = 0.01; '*' p-value = 0.05.


Matthieu Py
email: matthieu.py@uca.fr

Mohamed Sami Cherif
email: mohamed-sami.cherif@univ-amu.fr

Djamal Habet
email: djamal.habet@univ-amu.fr

Proofs and Certificates for Max-SAT (Extended Abstract) *

In this paper, we present a tool, called MS-Builder, which generates certificates for the Max-SAT problem in the particular form of a sequence of equivalence-preserving transformations. To generate a certificate, MS-Builder iteratively calls a SAT oracle to get a SAT resolution refutation which is handled and adapted into a sound refutation for Max-SAT. In particular, the size of the computed Max-SAT refutation is linear with respect to the size of the initial refutation if it is semi-read-once, tree-like regular, tree-like or semi-tree-like. Additionally, we propose an extendable tool, called MS-Checker, able to verify the validity of any Max-SAT certificate using Max-SAT inference rules.

Introduction

Given a Boolean formula in Conjunctive Normal Form (CNF), the Maximum Satisfiability (Max-SAT) problem consists in determining the maximum number of clauses that it is possible to satisfy by an assignment of the variables, while the Satisfiability (SAT) problem simply ascertains whether there exists an assignment which satisfies all the clauses. Max-SAT is an optimization extension of the satisfiability problem and is a natural formalism enabling to model many real-world and crafted problems [Muise et al., 2016;Zhang and Bacchus, 2012;[START_REF] Demirovic | Emir Demirovic and Nysret Musliu. MaxSAT-based large neighborhood search for high school timetabling[END_REF]Manyà et al., 2020;Achá and Nieuwenhuis, 2014;[START_REF] Bofill | [END_REF]Xu et al., 2003;Guerra and Lynce, 2012;[START_REF] Almeida | Model-based diagnosis with default information implemented through MAX-SAT technology[END_REF]. Different complete solving paradigms for Max-SAT have seen the day including Branch and Bound algorithms [Li et al., 2007;Küegel, 2012;[START_REF] Abramé | Ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver[END_REF][START_REF] Li | [END_REF] and SAT-based algorithms [Fu and Malik, 2006;[START_REF] Manquinho | [END_REF]Ansótegui et al., 2009;[START_REF] Davies | [END_REF]Ansótegui et al., 2013;Martins et al., 2014;Ignatiev et al., 2019].

Inference plays an important role in the context of Max-SAT solving [Li et al., 2007;Narodytska and Bacchus, 2014;[START_REF] Abramé | Ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver[END_REF] and this has led to an increasing interest in studying proof systems for Max-SAT in the literature [Larrosa and Heras, 2005;Bonet et al., 2006;Bonet et al., 2007;Larrosa and Rollon, 2020a;Larrosa and Rollon, 2020b;Bonet and Levy, 2020;Filmus et al., 2020;Cherif et al., 2022]. In particular, Max-SAT resolution [Larrosa and Heras, 2005;Bonet et al., 2006;Bonet et al., 2007] is one of the first known complete systems for Max-SAT and is a natural extension of the resolution rule [Robinson, 1965] used in the context of SAT. Max-SAT resolution proofs are more constrained than their SAT counterparts as the premise clauses are replaced by the conclusions when applying Max-SAT resolution. Consequently, switching from a resolution proof to a Max-SAT resolution proof is possible and well-known for the particular case of read-once resolution [Bonet et al., 2007;[START_REF] Heras | Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms[END_REF], where clauses can be used at most once in the proof. However, the adaptation of any resolution proof to a Max-SAT resolution proof is an established problem. Bonet et al. state that "it seems difficult to adapt a classical resolution proof to get a Max-SAT resolution proof, and it is an open question if this is possible without increasing substantially the size of the proof" [Bonet et al., 2006].

In this paper, we first contribute to the open problem of adapting resolution refutations for Max-SAT. To this end, we augment Max-SAT resolution with the split rule which allows to generate two clauses subsumed by the original clause. We prove that it is always possible to adapt a resolution refutation into a max-refutation, i.e., a refutation using Max-SAT inference rules, whose size is linear with respect to the initial refutation for the following cases: semi-read-once resolution, tree-like regular resolution, tree-like resolution and semi-treelike resolution. Furthermore, we propose a complete adaptation for any resolution refutation into a max-refutation, although with a worst-case exponential blow-up in the size of the proofs.

Secondly, we propose an independent tool, called MS-Builder, able to build certificates for the Max-SAT problem. To build such certificates, MS-Builder iteratively calls a SAT oracle to get a resolution refutation, adapts it for Max-SAT and applies it on the current formula. Moreover, we implemented an associated tool, called MS-Checker to check the validity of the certificates. Both tools are experimentally evaluated on the unweighted and weighted benchmarks of the 2020 Max-SAT Evaluation [START_REF] Bacchus | Fahiem Bacchus, Matti Järvisalo, and Ruben Martins[END_REF].

Preliminaries

Definitions and Notations

Let X be the set of propositional variables. A literal l is a variable x ∈ X or its negation x. A clause c = (l 1 ∨ l 2 ∨ ... ∨ l k ) is a disjunction of literals. A unit clause is composed of only one literal. A formula in Conjunctive Normal Form (CNF) ϕ = c 1 ∧ c 2 ∧ ... ∧ c m is a conjunction of clauses. An assignment I : X -→ {0, 1} maps each variable to a Boolean value. A literal l is satisfied (resp. falsified) by an assignment I if l ∈ I (resp. l ∈ I). A clause c is satisfied by an assignment I if at least one of its literals is satisfied by I, otherwise it is falsified. The empty clause □ contains zero literals and is always falsified. A CNF formula ϕ is satisfied by an assignment I, that we call model of ϕ, if each clause c ∈ ϕ is satisfied by I, otherwise it is falsified. Solving the Satisfiability problem (SAT) consists in determining whether there exists an assignment I that satisfies a given CNF formula ϕ. In the case where such an assignment exists, we say that ϕ is satisfiable, otherwise we say that ϕ is unsatisfiable or inconsistent. Solving the Maximum Satisfiability problem (Max-SAT) consists in determining the maximum number of clauses that can be satisfied by an assignment of a CNF formula ϕ, or equivalently the minimum number of clauses that each assignment must falsify. In the weighted partial Max-SAT problem, a finite or infinite weight is associated to each clause, representing the penalty of falsifying it.

SAT Resolution

To certify that a CNF formula is satisfiable, it is sufficient to exhibit a model of the formula. On the other hand, to prove that a CNF formula is unsatisfiable, we need to refute the existence of a model. A well-known SAT refutation system is based on an inference rule for SAT called resolution [Robinson, 1965]. The resolution rule deduces a clause called resolvent which can be added to the formula. Note that this rule is sound for SAT as it maintains SAT equivalence (models are the same before and after the transformation) and it is extensively used in the context of SAT solving and particularly the CDCL framework [Silva and Sakallah, 1996].

Definition 1 (Resolution [Robinson, 1965]).

c 1 = (x ∨ A) c 2 = (x ∨ B) c 3 = (A ∨ B)
It is possible to prove that a formula is unsatisfiable using a resolution refutation, which is a sequence of resolutions leading to an empty clause. Many restricted classes of resolution refutations have been studied in the literature namely linear [Loveland, 1970], unit [START_REF] Hertel | [END_REF], input [START_REF] Hertel | [END_REF], regular [Urquhart, 2011], read-once [Iwama and Miyano, 1995] and tree-like resolution refutations [START_REF] Ben-Sasson | Near Optimal Separation Of Tree-Like And General Resolution[END_REF] among others. In particular, a resolution refutation is tree-like if every intermediate clause is used at most once in the proof. Similarly, a resolution refutation is read-once if each clause is used at most once in the proof. Finally, a resolution refutation is regular if each branch, i.e., path from a leaf to the empty clause, contains at most one resolution per variable.

Example 1. We consider the CNF formula ϕ = (x 1 ∨ x 3 ) ∧ (x 1 ) ∧ (x 1 ∨ x 2 ) ∧ (x 2 ∨ x 3 ). The resolution refutation of ϕ, represented in Figure 1, is tree-like (and) regular, but not read-once because of clause (x 1 ).

x 1 ∨ x 3 x 1 x 1 ∨ x 2 x 2 ∨ x 3 x 3 x 2 x 3 □ Figure 1: A resolution refutation

Max-SAT Resolution

One of the first and most studied proof systems for Max-SAT is based on an inference rule called Max-SAT resolution, which is an extension of the resolution rule. The aim of complete Max-SAT systems is to compute the Max-SAT optimum of a given CNF formula, i.e., the maximum number of falsified clauses. The formula is thus refuted as many times as its optimum through equivalence-preserving transformations in the sense of Max-SAT (each assignment falsfies the same amount of clauses before and after the transformation).

Other than the resolvent clause, Max-SAT resolution introduces new clauses referred to as compensation clauses and which are essential to preserve Max-SAT equivalence.

Definition 2 (Max-SAT resolution [Larrosa and Heras, 2005;Bonet et al., 2006;Bonet et al., 2007]).

c 1 = x ∨ A c 2 = x ∨ B c r = A ∨ B cc 1 = x ∨ A ∨ b 1 cc 2 = x ∨ A ∨ b 1 ∨ b 2 . . . cc t = x ∨ A ∨ b 1 ∨ ... ∨ b t-1 ∨ b t cc t+1 = x ∨ B ∨ a 1 cc t+2 = x ∨ B ∨ a 1 ∨ a 2 . . . cc t+s = x ∨ B ∨ a 1 ∨ ... ∨ a s-1 ∨ a s
As a sound and complete rule for Max-SAT [Bonet et al., 2006], Max-SAT resolution plays an important role in the context of Max-SAT theory and solving. In particular, it is extensively used in the context of Branch and Bound algorithms [Li et al., 2007;Küegel, 2012;[START_REF] Abramé | Ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver[END_REF]Cherif et al., 2020] and more marginally in the context of SAT-based algorithms [START_REF] Heras | Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms[END_REF]Narodytska and Bacchus, 2014]. For a given CNF formula, it is always possible to generate a Max-SAT resolution proof of its optimum by applying the saturation algorithm [Bonet et al., 2006] to deduce empty clauses. A Max-SAT refutation, or simply max-refutation, is a sequence of Max-SAT inference steps deducing the empty clause. Its size is the number of its inference steps. Example 2. We consider the CNF formula from Example 1. A hand-made max-refutation of ϕ was proposed in [Bonet et al., 2006] and is represented in Figure 2.

x 1 ∨ x 3 x 1 x 1 ∨ x 2 x 2 ∨ x 3 x 3 x 1 ∨ x 3 x 2 ∨ x 3 x 1 ∨ x 2 ∨ x 3 x 1 ∨ x 2 ∨ x 3 x 3 □ Figure 2: A max-refutation
In recent work, Max-SAT resolution was augmented with other rules such as the split rule [Larrosa and Rollon, 2020b;Bonet and Levy, 2020;Py et al., 2021b;Py et al., 2021c] or the extension rule [Larrosa and Rollon, 2020a]. The addition of such rules to Max-SAT resolution can improve its efficiency in generating shorter proofs [Larrosa and Rollon, 2020b;Larrosa and Rollon, 2020a;Py et al., 2021c] or in simulating other proof systems [Filmus et al., 2020;Bonet and Levy, 2020]. To be exhaustive, we must also mention that other Max-SAT proof systems were introduced and studied in the literature [Li et al., 2016;[START_REF] Atserias | Albert Atserias and Massimo Lauria. Circular (yet sound) proofs[END_REF]Larrosa and Rollon, 2020a;Filmus et al., 2020]. Definition 3 (Split rule). Given a clause c 1 = (A) where A is a disjunction of literals and x a variable, the split rule replaces the premise c 1 by two new clauses as follows:

c 1 = (A) c 2 = (x ∨ A) c 3 = (x ∨ A)
If these proof systems have been extensively studied in theory, generating proofs remains an unexplored topic in practice. Hence, this work aims to contribute to this topic by proposing tools to build and check certificates for the Max-SAT problem. To this aim, we first propose adaptations from resolution refutations to max-refutations. These adaptations are used in a tool enabling to build certificates for the Max-SAT problem. For the sake of simplicity, we will exhibit examples with unweighted unpartial formulas to introduce MS-Builder. However, MS-Builder is also able to generate certificates for weighted (partial) Max-SAT formulas, using the fold and the unfold rules, and the weighted version of Max-SAT resolution and split [Bonet et al., 2007;Larrosa et al., 2008;Larrosa and Rollon, 2020b]. Definition 4 (Fold & Unfold). Given a weighted clause c and two positive weights w 1 and w 2 , the fold and unfold rules are respectively defined as follows:

(c, w 1 ) (c, w 2 ) (c,

w 1 + w 2 ) (c, w 1 + w 2 ) (c, w 1 ) (c, w 2 )
3 From Resolution Refutations to Max-Refutations

In the state of the art, the adaptation of any resolution refutation to get a max-refutation is known possible in the readonce case, and the size of the computed max-refutation is linear with respect to the size of the initial resolution refutation. In our work [START_REF] Py | [END_REF][START_REF] Py | [END_REF], we prove extend this result in the case of semi-read-once, treelike regular, tree-like or semi-tree-like resolution. We also prove that the adaptation is always possible in the unrestricted case, but with a worst-case exponential blow-up in the size of the proofs. The theoretical results are resumed in Table 1.

Resolution Refutation Size of the Max-Refutation

Read-Once Linear [Bonet et al., 2007 SAT algorithms are based on unit propagation, which means that when a unit clause is deduced, the value of its only literal is propagated in the whole formula, because satisfying this literal is necessary to satisfy the formula. Applying unit propagation can be seen as the use of a particular unit clause in several resolution steps. As such, transforming resolution refutations to fix non-read-once unit clauses can therefore be a useful preprocessing technique to our proof builder which relies on iterative calls to a SAT oracle, as will be shown in Section 4. To fix a non-read-once unit clause, we remove the resolution steps in which it is involved and we add a new resolution step at the end of the refutation. Such a strategy works when the refutation is based on unit propagation, i.e., every time a resolution step is applied on a unit clause, the variable contained in the unit clause no longer appears in the rest of the refutation. As SAT algorithms make a strong application of the unit propagation technique, we made the hypothesis, confirmed by experiments, that the computed resolution refutation will be often based on unit propagation. The proposed transformation can be seen as a preprocessing technique for any non-read-once resolution refutation. In particular, some non-read-once resolution refutations can be nonread-once only because of unit clauses and we say that such refutations are semi-read-once.

Definition 5 (Semi-read-once). A resolution refutation is semi-read-once if it is based on unit propagation and if each non-read-once clause is also a unit clause.

Theorem 1. Given an unsatisfiable formula ϕ and a semiread-once resolution refutation P of ϕ, there exists a maxrefutation of ϕ containing O(|P |) inference steps.

From Tree-Like Regular Resolution Refutations to Max-Refutations

To adapt a tree-like regular resolution refutation for Max-SAT, the idea is to use the split rule to fix non-read-once clauses. More precisely, if a clause c is used k times (k > 1) as a premise of a resolution step, we use the split rule on clause c with respect to a particular variable x which is carefully chosen to duplicate c into two distinct clauses c ∨ x and c ∨ x. We then use c ∨ x and c ∨ x to replace c as a premise of its resolution steps. If necessary, we repeat the same process on clauses c ∨ x and/or c ∨ x. Theorem 2. Given an unsatisfiable formula ϕ and a regular tree-like resolution refutation P of ϕ, there exists a maxrefutation of ϕ containing O(|P |) inference steps.

From (Semi-)Tree-Like Resolution Refutations to Max-Refutations

To extend the linear case to tree-like resolution refutations, we simply use a known transformation from any tree-like resolution refutation to a regular tree-like resolution refutation without increasing its size (proved in [Urquhart, 1995]). Theorem 3. Given an unsatisfiable formula ϕ and a tree-like resolution refutation P of ϕ, there exists a max-refutation of ϕ containing O(|P |) inference steps.

To extend our result to semi-tree-like resolution refutations, defined below, we propose an adaptation which relies on the fact that such refutations can be partitioned into two parts where the first part is a read-once sequence of resolutions and the second part is a tree-like resolution refutation. Definition 6 (semi-tree-like resolution refutation). A resolution refutation is semi-tree-like if, for any branch of the refutation, at most one clause is non-read-once. Theorem 4. Given an unsatisfiable formula ϕ and a semitree-like resolution refutation P of ϕ, there exists a maxrefutation of ϕ containing O(|P |) inference steps.

From Unrestricted Resolution Refutations to Max-Refutations

To adapt any resolution refutation to a max-refutation, we add a prior transformation to make the initial resolution refutation (semi-)tree-like. To achieve this prior transformation, we iteratively search the proof for the first non-read-once intermediate clause c, and we duplicate the the part of the proof leading to c. Repeating this treatment on intermediary nonread-once clauses forces the resolution refutation to become (semi-)tree-like, even if we accept an exponential blow-up of the size of the formula. Theorem 5. Given an unsatisfiable formula ϕ and an unrestricted resolution refutation P of ϕ, there exists a maxrefutation of ϕ with O(2 µ(P ) × |P |) inference steps.

MS-Builder & MS-Checker

MS-Builder [START_REF] Py | [END_REF]Py et al., 2021a] generates certificates for the Max-SAT Problem in the particular form of a Max-SAT-equivalence-preserving transformation from the initial formula into a formula composed of a set of empty (ϕ, opt) ← remove empty clauses(ϕ, opt) 7:

T ← concatenate(T, M RP ) 8: end while 9: I ← compute model(ϕ) 10: return (T, opt, I) clauses and a satisfiable sub-formula. Given an initial formula, MS-Builder iteratively calls a SAT oracle [START_REF] Biere | Armin Biere. Booleforce[END_REF] to get a resolution refutation, adapts it for Max-SAT and applies it to the current formula. When the SAT oracle returns that the current formula is now satisfiable (with a model), the algorithm terminates. The complete sequence of transformations generating k empty clauses is a proof that the Max-SAT optimum is at least k while the model is a proof that it is possible to falsify exactly k clauses and therefore that the Max-SAT optimum is k. MS-Builder also works on weighted (partial) formulas. MS-Builder receives a file containing a formula in the standard WCNF format and it returns a certificate. The builder is also coupled with a tool called MS-Checker which verifies the validity of the computed certificates.

On the complete track benchmarks of the 2020 Max-SAT Evaluation [START_REF] Bacchus | Fahiem Bacchus, Matti Järvisalo, and Ruben Martins[END_REF], MS-Builder has succeeded to construct full proofs for 163 instances over 576 unweighted (partial) instances and for 144 instances over 600 weighted (partial) instances. In the experiments, a slot of only 1 hour and at most 16 GB of memory was allocated to each instance. More interestingly, MS-Builder has also succeeded to build at least half of the proofs (with respect to the optimum value) of 302 instances over 463 unweighted instances and of 326 instances over 489 weighted instances for which the optimum cost is known. Finally, we report in Table 2 the encountered refutation types during proof building. We observed different behaviours for unweighted and weighted instances. Indeed, while the percentage of read-once and semi-read-once resolution refutations is 83.7 % in the unweighted benchmark, it is only 35.60 % in the weighted benchmark. Such a difference can explain why weighted instances are harder to proove than unweighted ones.

Table 1 :

 1 Adaptation of resolution refutations for Max-SAT

	]

3.1 From Semi-Read-Once Resolution Refutations

to Max-Refutations

Table 2 :

 2 Encountered types of resolution refutations

		Unweighted instances	Weighted instances
		Number Percentage Number Percentage
	read-once	169,239	83.7 %	135,594	35.60 %
	semi-read-once	24,556	12.1 %	87,748	23.04 %
	tree-like regular	2,879	1.4 %	23,612	6.20 %
	tree-like	1,795	0.9 %	87,529	22.99 %
	unrestricted	3,799	1.9 %	46,337	12.17 %