Davide Ancona
email: davide.ancona@unige.it

Giovanni Lagorio
email: giovanni.lagorio@unige.it

Static single information form for abstract compilation

In previous work we have shown that more precise type analysis can be achieved by exploiting union types and static single assignment (SSA) intermediate representation (IR) of code. In this paper we exploit static single information (SSI), an extension of SSA proposed in literature and adopted by some compilers, to allow assignments of more precise types to variables in conditional branches. In particular, SSI can be exploited rather easily and effectively to infer more precise types in dynamic object-oriented languages, where explicit runtime typechecking is frequently used. We show how the use of SSI form can be smoothly integrated with abstract compilation, our approach to static type analysis. In particular, we define abstract compilation based on union and nominal types for a simple dynamic object-oriented language in SSI form with a runtime typechecking operator, to show how precise type inference can be. This work has been partially supported by MIUR DISCO -Distribution, Interaction, Specification, Composition for Object Systems. 1 Coinduction allows proper treatment of recursive types and methods [5].

.

, and proved to be more effective than SSA for performing data flow analysis, program slicing, and interprocedural analysis. Similar IRs are adopted as well in formal software development tools.

We show how SSI can be exploited rather easily and effectively by abstract compilation to improve type inference of dynamic object-oriented languages, where explicit runtime typechecks are frequently used.

To this aim, we formally define the operational semantics of a simple dynamic object-oriented language in SSI form equipped with a runtime typechecking operator, and then provide an abstract compilation scheme based on union and nominal types supporting more precise type inference of branches guarded by explicit runtime typechecks.

The paper is structured as follows: Section 2 introduces SSA and SSI IRs and motivates their usefulness for type analysis; Section 3 formally defines the SSI IR of a dynamic object-oriented language equipped with an operator instanceof for runtime typechecking. Section 4 presents a compilation scheme for the defined IR, based on nominal and union types, and Section 5 concludes with some considerations on future work. Abstract compilation of the code examples in Section 2 together with the results of the resolution of some goals can be found in an extended version of this paper. 2 2 Type analysis with SSA and SSI In this section SSA and SSI IRs are introduced and their usefulness for type analysis is motivated.

Introduction

In previous work [START_REF] Ancona | Idealized coinductive type systems for imperative object-oriented programs[END_REF] we have shown that more precise type analysis can be achieved by exploiting union types and static single assignment (SSA) [START_REF] Cytron | Efficiently computing static single assignment form and the control dependence graph[END_REF] intermediate representation (IR) of code. Most modern compilers (among others, GNU's GCC [START_REF] Novillo | Tree SSA -a new optimization infrastructure for GCC[END_REF], the SUIF compiler system [START_REF] Holloway | The machine-SUIF static single assignment library[END_REF], Java HotSpot [START_REF] Griesemer | A compiler for the java hotspottm virtual machine[END_REF], and Java Jikes RVM [START_REF] Alpern | The jalapeño virtual machine[END_REF]) and formal software development tools implement efficient algorithms for translating code in advanced forms of IR particularly suitable for static analysis, thus offering the concrete opportunity of exploiting such IRs to obtain more precise type analysis and inference, and to fruitfully reuse those software components devoted to IR generation.

Abstract compilation [START_REF] Ancona | Coinductive type systems for object-oriented languages[END_REF][START_REF] Ancona | Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification? In FoVeOOS[END_REF][START_REF] Ancona | Idealized coinductive type systems for imperative object-oriented programs[END_REF] is a modular approach to static type analysis aiming to reconcile types and symbolic execution: an expression e is well-typed if the goal generated by compiling e succeeds w.r.t. the coinductive 1 model of the constraint logic program obtained by compiling the source program in which the expression is executed. In such a model terms are types representing possibly infinite sets of values, and goal resolution corresponds to symbolic execution.

Type analysis with static single assignment form

Method read() declared below, in a dynamic object-oriented language, creates and returns a shape which is read through method nextLine() that reads the next available string from some input source. The partially omitted methods readCircle() and readSquare() read the needed data from the input, create, and return a new corresponding instance of Circle or Square. this . print ( " A circle with radius " ); this . print ( sh . getRadius ()); } else i f ( st . equals ( " square " )) { sh = this . readSquare (); this . print ( " A square with side " ); this . print ( sh . getSide ()); } else throw new IOException (); this . print ( " Area = " ); this . print ( sh . area ()); return st ; } } Although method read() is type safe, no type can be inferred for sh to correctly typecheck the method; indeed, when method area() is invoked, variable sh may hold an instance of Circle or Square, therefore the most precise type that can be correctly assigned to sh is Circle ∨ Square. However, if sh has type Circle ∨ Square, then both sh.getRadius() and sh.getSide() do not typecheck.

There are two different kinds of approaches to solve the problem shown above. One can either define a rather sophisticated flow-sensitive type system, where each occurrence of a single variable can be associated with a different type, or typecheck the SSA IR, in which the method can be compiled.

In an SSA IR the value of each variable is determined by exactly one assignment statement [START_REF] Cytron | Efficiently computing static single assignment form and the control dependence graph[END_REF]. To obtain this property, a flow graph is built, and a suitable renaming of variables is performed to keep track of the possibly different versions of the same variable; following Singer's terminology [START_REF] Singer | Static Program Analysis based on Virtual Register Renaming[END_REF] we call these versions virtual registers. Conventionally, this is achieved by using a different subscript for each virtual register corresponding to the same variable. For instance, in the SSA IR of method read() there are three virtual registers (sh0, sh1 and sh2) for the variable sh. To transform a program into SSA form, a pseudo-function, conventionally called ϕ-function, needs to be introduced to correctly deal with merge points. For instance, in block b5 the value of sh can be that of either sh0 or sh1, therefore a new virtual register sh2 has to be introduced to preserve the SSA property. The expression ϕ(sh0,sh1) simply keeps track of the fact that the value of sh2 is determined either by sh0 or sh1.

τ 0 φ(τ 0 ,τ 1 ) = τ 0 \/τ 1 τ 2 τ 1 τ 0 τ 1 τ 2 if (sh 0 instanceof τ)
σ(τ 0 ) = (τ 0 /\τ, τ 0 \τ)

Fig. 1. Type theoretic interpretation of ϕ-function and σ-function

At the level of types, the ϕ-function naturally corresponds to the union type constructor (Figure 1): arrows correspond to data flow and, as usual, to ensure soundness the type at the origin of an arrow must be a subtype of the type the arrow points to. That is, for the types shown in the figure ,τ

0 , τ 1 ≤ τ 0 ∨ τ 1 ≤ τ 2 .
Thanks to pretty standard and efficient algorithms for transforming source programs into SSA IR [START_REF] Cytron | Efficiently computing static single assignment form and the control dependence graph[END_REF][START_REF] Das | A practical and fast iterative algorithm for phifunction computation using DJ graphs[END_REF], the flow analysis phase, where source code is transformed into IR, can be kept separate from the subsequent type analysis phase, favoring simplicity and reuse. Indeed, flow analysis and consequent transformation into IR is implemented by most compilers and formal software development tools. Abstract compilation makes such an approach even more modular, by dividing the overall process into three separate stages. First, the source code is transformed into a suitable IR. Then, the IR is compiled into a set of Horn clauses and a goal. Finally, the goal is resolved with an appropriate inference engine (typically, implementing coinductive constraint logic programming [START_REF] Ancona | Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification? In FoVeOOS[END_REF]).

This paper mainly focuses on the second stage of the overall process (that is, compilation from IR into Horn clauses), in the particular case when the adopted IR allows precise flow analysis, as happens with SSI, of dynamic object-oriented languages.

Type analysis with static single information form

Let us consider method largerThan(sh) of class Square, where instanceof is exploited to make the method more efficient in case the parameter sh contains an instance of (a subclass) of Square. Since variable sh is not updated, both blocks b2 and b3 refer to the same virtual register sh0. As a consequence, the only possible type that can be correctly associated with sh0 is Square, thus making the method of little use. However, this problem can be addressed if one considers the SSI IR of the method [START_REF] Ananian | The static single information form[END_REF][START_REF] Singer | Static Program Analysis based on Virtual Register Renaming[END_REF].

largerThan ( sh0 ) { b1 :{ i f ( sh0 instanceof Square ) with ( sh1 , sh2 ) = σ( sh0 ) ( this1 , this2 ) = σ( this0 ) jump b2 ; else jump b3 ;} b2 :{ r0 = this1 . side > sh1 . side ;
jump out ;} b3 :{ r1 = this2 . area () > sh2 . area (); jump out ;} out :{ r2 =ϕ( r0 ,r1 ); return r2 ;} } SSI is an extension of SSA enforcing the additional constraint that all variables must have different virtual registers in the branches of conditional expressions. Such a property is obtained by a suitable renaming and by the insertion of a pseudo function, called σ-function. As a consequence, suitable virtual registers and a σ-function have to be introduced also for the read-only pseudo-variable this.

The notion of σ-function is the dual of ϕ-function (Figure 1); the type theoretic interpretation of σ depends on the specific kind of guard. If it is a runtime typecheck (of the form (sh0 instanceof Square) as in the example), then σ splits the type τ 0 of sh0 in the type τ0∧Square, assigned to sh1, and in the type τ0\Square, assigned to sh2, where the intersection and the complement operators have to be properly defined (see Section 4). For instance, if sh0 has type Square∨Circle, then sh1 has type (Square∨Circle)∧Square=Square, and sh2 has type (Square∨Circle)\Square=Circle, therefore Square∨Circle turns out to be a valid type for the parameter sh0 of the method largerThan.

For what concerns this, in this particular example no real split would be necessary: this0 has type Square, so Square is split into (Square,Square), that is, both this1 and this2 have the same type Square.

Language definition

In this section we formally define an SSI IR for a simple dynamic object-oriented language equipped with an instanceof operator for performing runtime typechecking. Even though we have chosen a familiar Java-like syntax both for the IR and the source code used in the examples, the language is fully dynamic: code does not contain any type annotation, hence, under this point of view the language is quite different from Java.

prog ::= cd n {b n } cd ::= class c1 extends c2 { f n md k } (c1 = Object) md ::= m(r n ) {b n } b ::= l :e r ::= xi e ::= r | new c(e n ) | e.f | e0.m(e n ) | e1; e2 | r = e | e1.f = e2 | jump l | r = ϕ(r n ) | return r | if (r instanceof c) with (r , r ) = σ(r ) n jump l1 else jump l2
Syntactic assumptions: inheritance is not cyclic, method bodies are in correct SSI form and are terminated with a unique return statement, method and class names are disjoint, no name conflicts in class, field, method and parameter declarations, main expression and declared parameters cannot be this.

Fig. 2. SSI intermediate language

A program is a collection of class declarations followed by an anonymous main method with no parameters and contained in an anonymous class (conventionally its fully qualified name is . ), whose body is a sequence of blocks (see the comments on method bodies below).

The notation cd

n is a shortcut for cd 1 , . . . , cd n . A class declares its direct superclass (only single inheritance is supported), its fields, and its methods.

Object is the usual predefined root class of the inheritance tree; every class comes equipped with the implicit constructor with parameters corresponding to all fields, in the same order as they are inherited and declared. For simplicity, no user constructors can be declared. Method bodies are sequences of uniquely labeled blocks that contain sequences of expressions. We assume that all blocks contain exactly one jump, necessarily placed at the end of the block. Three different kinds of jumps are considered: local unconditional and conditional jumps, and returns from methods. Method bodies are implicitly assumed to be in correct SSI IR: each virtual register is determined by exactly one assignment statement, and all variables must have different virtual registers in the branches of conditional expressions. Finally, all method bodies contain exactly one return expression, which is always placed at the end of the body. 3Virtual registers have the form x i , where x is the corresponding variable. If r is a virtual register, then var (r ) returns the variable the register refers to, therefore if r = x i , then var (r ) = x . The receiver object can be referred inside method bodies with the special implicit parameter this, hence the IR contains virtual registers of the form this i .

Besides usual statements and expressions, we consider ϕ and σ pseudofunction assignments. Conditional jumps contain σ-functions which split each virtual register r occurring in either branches into two new distinct versions used in the blocks labeled by l1, and l2, respectively. The guard can only be of the form (r instanceof c); however, more elaborated guards can be easily expressed in terms of this primitive one by suitable transformations during the compilation from the source code to the IR. Depending on the types and abstract compilation scheme, there could be other kinds of guards for which SSI would improve type analysis; for instance, if one includes the type corresponding to the null references, then a guard of the form (r == null) would take advantage of SSI to enhance null reference analysis. For those guards for which no type refinement is possible the σ-function performs no split, that is, σ(τ )=(τ ,τ ).

Semantics: To define the small step semantics of the language we first need to specify values v (see Figure 3), which are just identities o of dynamically created objects. Furthermore, we add frame expressions ec{e}, where ec is an execution context; frame expressions are runtime expressions needed for defining the small step semantics of method calls. An execution context ec is a pair consisting of a stack frame fr and a fully qualified name µ. A frame expression fr , µ {e} corresponds to the execution of a call to a method m declared in class c, where e is the residual expression (yet to be evaluated) of the currently executed block, fr is the stack frame of the method call, and µ = c.m is the fully qualified name of the method. Stack frames fr map virtual registers to their corresponding values. Each association is labeled with a distinct time-stamp t, which specifies how recently the register has been updated (higher time-stamp values correspond to more recent updates). Such labels are used to define the semantics of ϕ-function assignments.

H ::= o → c, f → v j k (heaps) C[•] ::= [•] | ec{C[•]} | new c(v n , C[•], e j ) | C[•].f | C[•].m(e k ) | v0.m(v j , C[•], e k ) | C[•]; e | x = C[•] | C[•].f = e | v.f = C[•] | if (C[•]) with (x , x ) = σ(x ) n jump l1 else jump l2
Heaps H map object identifiers o to objects, that is, pairs consisting of a class name c and the set of field names f with their corresponding value v.

Figure 4 shows the execution rules. Rule (main) defines the main judgment; a value v is returned if the runtime expression fr , . {e}, where e is the first block (retrieved by the auxiliary function firstBlock ) of the main method, transitively rewrites to v (and a heap H which is discarded). The evaluation context fr , . of the frame expression specifies that initially the frame ( fr ) is empty (neither this, nor parameters are accessible), and that execution starts in the main method, whose fully qualified name is . (recall that, conventionally, the main method is anonymous and is contained in an anonymous class).

The auxiliary judgment H e → H , e is defined by the three rules (methcall) (a new execution context is created), (ctx) (evaluation continues in the currently active execution context), and (return) (the current execution context is closed).

(main) firstBlock ( . ) = e H fr , . {e} → * H, v cd n {b n } ⇒ v (meth-call) H(o) = c, firstBlock (c.m) = e params(c.m) = r n fr = r → v n , this0 → o H C[o.m(v n )] → H, C[ fr , c.m {e}] (ctx) currentEC (C[•]) = ec H, ec e → H , ec , e C [•] = updateEC (C[•], ec ) H C[e] → H , C [e ] (return) H C[ fr , µ {return r }] → H, C[fr (r )] (fld-acc) H(o) = c, f → v n f = fj H, ec o.f → H, ec, vj (reg) H, fr , µ r → H, fr , µ , fr (r ) (new) o fresh in H fieldNames(c) = f n H, ec new c(v n ) → H[ c, f → v n /o], ec, o (seq) H, ec v; e → H, ec, e (reg-asn) H, fr , µ r = v → H, fr [v/r ], µ , v
(fld-asn) In rule (meth-call), the object referenced by o is retrieved from the heap to find its class, c. Then, the auxiliary functions firstBlock and params return the first block of the method and its parameters, respectively. The result of the evaluation is a frame expression, where the new stack frame maps parameters to their corresponding arguments, and this 0 to o, the fully qualified name c.m corresponds to the invoked method, and the expression is the first block of the method. Rule (ctx) deals with context closure. Contexts (the standard definition is in Figure 3) correspond to a deterministic call-by-value and left-to-right evaluation strategy. A single computation step in the current execution context (corresponding to the most nested frame expression) is performed. The active execution context is extracted by currentEC ; then, if the redex e rewrites to e yielding H and ec (see the other rules defining the auxiliary evaluation judgment), then the C[e] rewrites to C [e ], yielding the new heap H ; context C [ ] is obtained from C[ ] by updating the frame expression corresponding to the active execution context with the new execution context ec . In rule (return) the current execution context is closed, the heap is unaffected, and the result is the value associated with the returned virtual register r in the frame of the closing context.

H(o) = c, f → v n f = fj if i = j then v i = v else v i = vi H, ec o.f = v → H[ c, f → v n /o], ec, v (jump) block (µ, l ) = e H, fr , µ jump l → H, fr , µ , e (phi) H, fr , µ r0 = ϕ(r n ) → H, fr [mru(fr , r n )/r0], µ , v (if)
H(fr (r )) = c , if c ≤ c then l = l1, fr = fr [fr (r )/r n ] else l = l2, fr = fr [fr (r )/r n ] block (µ, l ) = e H, fr , µ if (r instanceof c) with (r , r ) = σ(r ) n jump l1 else jump l2 → H, fr , µ , e
The remaining rules define the auxiliary judgment H, ec e → H , ec , e , one for any distinct kind of redex. In rule (reg) a virtual register is accessed by extracting the corresponding value from the stack frame fr .Variable and field assignments evaluate to their right values; rule (reg-asn) has the side effect of updating, in the current stack frame fr , the value of the virtual register r and its associated time-stamp (this is implicit in the definition of fr [v/r ]) since, after the assignment, r becomes the most recently updated register. Rule (fld-asn) deals with field assignments: the object referenced by o is retrieved from the heap, and its value updated. In rule (seq) the left-hand-side value in a sequence expression is discarded to allow evaluation to proceed with the next expression. In rule (phi), register r 0 is updated with the value (denoted by mru(fr , r n )) of the most recently updated register in the stack frame, between r n . In rule (new) a new object, identified by a fresh reference o, is added to the heap H. The fields f n of the newly created object are initialized by the values passed to the constructor. In rule (fld-acc) field accesses are evaluated: the object is retrieved from the heap, and the resulting expression is the value of the selected field. Rules (jump) and (if) deal with unconditional and conditional jumps, respectively. The evaluation of a jump returns the expression e contained in the block labeled by l in the method µ of the current execution context. The conditional jump (rule (if)) selects which branch to execute and which virtual registers have to be updated, depending on whether the value fr (r ) of the register r is a reference to an object of a subclass of c. If it is the case, then the returned expression is that labeled by l 1 and the virtual registers r n are updated; otherwise, the returned expression is that labeled by l 2 and the virtual registers r n are updated.

As

Abstract compilation

In this section we define an abstract compilation scheme for programs in the SSI IR presented in Section 3. Programs are translated into a Horn formula Hf (that is, a logic program) and a goal B ; type analysis and inference amounts to coinductive resolution of B , that is the greatest Herbrand model of Hf [START_REF] Ancona | Coinductive type systems for object-oriented languages[END_REF] is considered. The proof of soundness of such a translation is sketched in the Appendix.

In previous work [START_REF] Ancona | Coinductive type systems for object-oriented languages[END_REF][START_REF] Ancona | Idealized coinductive type systems for imperative object-oriented programs[END_REF] we have used expressive structural types; however, since SSI favors more precise type analysis, we have preferred to follow a simpler approach based on nominal types. Structural types could be used as well to allow data polymorphism, with the downside that subtyping relation becomes much more involved and termination issues must be addressed.

Subtyping is treated as an ordinary predicate, thus allowing only global analysis; compositional analysis can be obtained by considering subtyping as a constraint, and by using coinductive constraint logic programming [START_REF] Ancona | Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification? In FoVeOOS[END_REF].

The compilation of programs, class, and method declarations is defined in Figure 5. We follow the usual syntactic conventions for logic programs: logical variable names begin with upper case, whereas predicate and functor names begin with lower case letters. Underscore denotes anonymous logical variables that occur only once in a clause; [ ] and [e|l] respectively represent the empty list, and the list where e is the first element, and l is the rest of the list.

Each rule defines a different compilation judgment.

(prog) ∀ i = 1..n cd i Hf i e (t | B ) cd n e (Hf d ∪ Hf n |B ) (class) ∀ i = 1..k md i in c1 Hf i inhFields(c1) = f h class c1 extends c2 { f n md k } Hf k ∪ 8 > > < > > : class(c1 ) ← true. extends(c1 , c2 ) ← true. dec field (c1 , f ) n ← true. new (CE , c1 , [T h , T n ]) ← new (CE , c2 , [T h ]), field upd (CE , c1 , f , T ) n . 9 > > = > > ; (meth) b n (t | B ) m(r n ){b n } in c  dec meth(c, m) ← true. has meth(CE , c, m, [This0 , r n ], t) ← subclass(This0 , c), B . ff (body) ∀ i = 1..n bi Bi b n l :return r (r | B n )
Fig. 5. Compilation of programs, class, and method declarations and bodies.

md i (see below), clauses asserting that class c 1 declares field f i , for all i = 1..n, and three specific clauses for predicates class, extends, and new . The clause for new deserves some explanations: the atom new (ce, c, [t n ]) succeeds iff the invocation of the implicit constructor of c with n arguments of type t n is type safe in the global class type environment ce. The class environment ce is required for compiling field access and update expressions (Figure 6): it is a finite map (simply represented by a list) associating class names with field records (finite maps again simply represented by lists) assigning types to all fields of a class. Class environments are required because of nominal types: abstract compilation with structural types allows data polymorphism on a per-object basis, whereas here we obtain only a very limited form of data polymorphism on a per-class basis. Type safety of object creation is checked by ensuring that object creation for the direct superclass c 2 is correct, where only the first part h of the arguments corresponding to the inherited fields (returned by the auxiliary function inhFields whose straightforward definition has been omitted) are passed; then, predicate field upd defined in Figure 7 checks that all remaining n arguments, corresponding to the new fields declared in c 1 , have types that are compatible with those specified in the class environment. The clause dealing with the base case for the root class Object is also defined in Figure 7.

The judgment m(r n ){b n } in c Hf states that the method declaration m(r n ){b n } contained in class c compiles to Horn clauses Hf . Two clauses are generated per method declaration: the first simply states that method m is declared in class c (and is needed to deal with inherited methods Figure 7), whereas the second is obtained by compiling the body of the method. The atom has meth(ce, c, m, [t 0 , t n ], t) succeeds iff, in class environment ce method m of class c can be safely invoked on target object of type t 0 , with n arguments of type t n and returned value of type t. The predicate subclass (defined in Figure 7)

ensures that the method can be invoked only on objects that are instances of c or one of its subclasses. For simplicity we assume that all names (including this) are translated to themselves, even though, in practice, appropriate injective renaming should be applied [START_REF] Ancona | Coinductive type systems for object-oriented languages[END_REF]. The compilation of a method body b n l :return r consists of the type of the returned virtual register r , and the conjunction of all the atoms generated by the compilation of blocks b n .

Figure 6 defines abstract compilation for blocks, and expressions. Compiling a block l :e returns the conjunction of atoms obtained by compiling e; the type t of e is discarded. The compilation of e 1 ; e 2 returns the type of e 2 and the conjunction of atoms generated from the compilation of e 1 and e 2 . The compilation of an unconditional jump generates the type void and the empty conjunction of atoms true. A conditional jump has type void as well, but a nonempty sequence of predicates is generated to deal with the splitting performed by the σ-functions; predicates inter and diff (defined in Figure 7) compute the intersection T and the difference F between the type of r and c, respectively, and predicate var upd (defined in Figure 7) ensures that the type of virtual registers r i and r i are compatible with the pairs of types returned by the σfunctions. In case r i refers to the same variable of r the types of such a pair are the computed intersection T and difference F , respectively, otherwise the pair (r i , r i ) is returned (hence, no split is actually performed). Compilation of assignments to virtual registers and fields yields the conjunction of the atoms generated from the corresponding sub-expressions, together with the atoms that ensure that the assignment is type compatible (with predicates var upd and field upd defined in Figure 7). The returned type is the type of the right-hand side expression. Compilation of ϕ-function assignments to virtual registers is just an instantiation of rule (var-upd) where the type of the expression is the union of the types of the virtual registers passed as arguments to ϕ. Compilation rules for object creation, field selection, and method invocation follow the same pattern: the type of the expression is a fresh logical variable (except for object creation) corresponding to the type returned by the specific predicate (new , field , and invoke defined in Figure 7). The generated atoms are those obtained from the compilation of the sub-expressions, together with the atom specific of the expression. Rules (var) is straightforward.

(block) e (t | B ) l :e B (seq) e1 (t1 | B1) e2 (t2 | B2) e1; e2 (t2 | B1, B2) (c-jmp) if var (r i ) = var (r ) then t i = T, t i = F else t i = r i , t i = r i T, F fresh if (r instanceof c) with (r , r ) = σ(r ) n jump l1 else jump l2 in (void | inter (r , c, T ), diff (r , c, F ), var upd (r , t ), var upd (r , t ) n ) (var-upd) e (t | B ) r = e (t | B , var upd (r , t)) (jmp) jump l (void | true) (field-upd) e1 (t1 | B1) e2 (t2 | B2) e1.f = e2 (t2 | B1, B2, field upd (CE , t1, f , t2)) (phi) r = ϕ(r n ) (∨r n | var upd (r , ∨r n )) (new) ∀ i = 1..n ei (ti | Bi) new c(e n ) (c | B n , new (CE , c, [t n ])) (field-acc) e (t | B ) R fresh e.f (R | B , field (CE , t, f , R)) (invk) ∀ i = 0..n ei (ti | Bi) R fresh e0.m(e n ) (R | B0, B n , invoke(CE , t0, m, [t n ], R)) (var) r (r | true)
The clauses (see Hf d in (prog)) that do not depend on the specific program are defined in Figure 7 in the Appendix.

Predicate subtype defining the subtyping relation deserves some comments: as expected, classes c 1 and c 2 are both subtypes of c 1 ∨ c 2 , but c 1 is not a subtype of c 2 when C 1 is a proper subclass of c 2 : since no rule is imposed on method overriding, subclassing is not subtyping. Consider for instance the following source code snippet: Predicate field looks up the type of a field in the global class environment, and is defined in terms of the auxiliary predicates has field , class fields, field type, and no def . In particular, predicate has field checks that a class has actually a certain field, either declared or inherited. The definitions of class fields, field type, and no def are straightforward (no def ensures that a map does not contain multiple entries for a key), whereas the clause for has field dealing with inherited fields is similar to the corresponding one for invoke (see below).

If the target object has a class type c, then the correctness of method invocation is checked with predicate has meth applied to class c and to the same list of arguments where, however, the type c of this is added at the beginning. If the target object has a union type, predicate invoke checks that method invocation is correct for both types of the union, and then merges the types of the results into a single union type.

Finally, the clause for has meth deals with the inherited methods: if class c does not declare method m, then has meth must hold on the direct superclass of c.

Predicates inter and diff define type splitting for σ-functions; both predicates never fail, but the type empty is returned when a branch is not reachable. Their definition is straightforward: the former keeps all classes that satisfies the runtime typechecking, the latter all classes that do not satisfy it.

Conclusion

We have shown how SSI IR can be exploited by abstract compilation for static global type analysis of programs written in a dynamic object-oriented language equipped with an instanceof operator for runtime typechecks. The approach allows a rather precise analysis with just nominal and union types.

We have stated soundness of type inference and sketched the proof; to do that, a small step operational semantics of the SSI IR language has been formally defined; this is also an original contribution, since, to our knowledge, no prior formal definition of the semantics of an SSI IR language can be found in literature.

There already exists interesting work on type inference of dynamic objectoriented languages, and several papers have defined and studied flow sensitive type systems [START_REF] Anderson | Towards type inference for javascript[END_REF][START_REF] An | Dynamic inference of static types for Ruby[END_REF][START_REF] Foster | Flow-sensitive type qualifiers[END_REF][START_REF] Heidegger | Recency types for analyzing scripting languages[END_REF] (to mention just a few). The main distinguishing feature of abstract compilation, when compared with all other approaches, is its modularity. Abstract compilation allows one to implement different kinds of analysis, for different languages with a suitable compilation scheme, by using the same inference engine. Furthermore, abstract compilation is particularly suited for directly compiling IR languages, as SSI, to greatly improve the precision of the analysis.

Guarded type promotion [START_REF] Winther | Guarded type promotion (eliminating redundant casts in Java)[END_REF] for Java allows more precise type analysis of branches guarded by dynamic type checks in a very similar way as in our approach. However, here we consider the more challenging problem of inferring types for a dynamic language where no type annotations are provided by the programmers.

  v ::= o (values) e ::= v | ec{e} | . . . (runtime expressions) ec ::= fr , µ (execution context) fr ::= r →t v k (stack frames) µ ::= c.m (full method names)

Fig. 3 .

 3 Fig. 3. Syntactic definitions instrumental to the operational semantics

Fig. 4 .

 4 Fig. 4. Small-step semantics

Fig. 6 .

 6 Fig. 6. Compilation of blocks and expressions

  class(object) ← true. subclass(X , X ) ← class(X ). subclass(X , Y ) ← extends(X , Z ), subclass(Z , Y ). subtype(empty, ) ← true. subtype(T , T ) ← true. subtype(T1 ∨ T2 , T ) ← subtype(T1 , T ), subtype(T2 , T ).subtype(T , T1 ∨ ) ← subtype(T , T1 ). subtype(T , ∨ T2 ) ← subtype(T , T2 ). field (CE , empty, , ) ← true. field (CE , C , F , T ) ← has field (C , F ), class fields(CE , C , R), field type(R, F , T ). field (CE , T1 ∨ T2 , F , FT1 ∨ FT2 ) ← field (CE , T 1, F, F T 1), field (CE , T 2, F, F T 2). class fields([C : R|CE ], C , R) ← no def (C , CE ). class fields([C1 : |CE ], C2 , R) ← class fields(CE , C2 , R), C1 = C2 . field type([F :T |R], F , T ) ← no def (F , R). field type([F1 : |R], F2 , T ) ← field type(R, F2 , T ), F1 = F2 . no def ( , [ ]) ← true. no def (K1 , [K2 : |Tl ]) ← no def (K1 , Tl ), K1 = K2 . invoke( ,empty, , , ) ← true. invoke(CE , C , M , A, RT ) ← has meth(CE , C , M , [C |A], RT ). invoke(CE , T1 ∨ T2 , M , A, RT1 ∨ RT2 ) ← invoke(CE , T1 , M , A, RT1 ), invoke(CE , T2 , M , A, RT2 ). new ( , object, [ ]) ← true. has field (C , F ) ← dec field (C , F ). has field (C , F ) ← extends(C , P ), has field (P , F ), ¬dec field (C , F ). has meth(CE , C , M , A, R) ← extends(C, P ), has meth(CE , P, M, A, R), ¬dec meth(C, M ). var upd (T1 , T2 ) ← subtype(T2 , T1 ). field upd (CE , C , F , T2 ) ← field (CE , C , F , T1 ), subtype(T2 , T1 ). inter (C1 , C2 , C1 ) ← subclass(C1 , C2 ). inter (C1 , C2 , empty) ← ¬subclass(C1 , C2 ). inter (T1 ∨ T2 , C , IT1 ∨ IT2 ) ← inter (T1 , C , IT1 ), inter (T2 , C , IT2 ). diff (C1 , C2 , C1 ) ← class(C1 ), ¬subclass(C1 , C2 ). diff (C1 , C2 , empty) ← class(C1 ), subclass(C1 , C2 ). diff (T1 ∨ T2 , C , IT1 ∨ IT2 ) ← diff (T1 , C , IT1 ), diff (T2 , C , IT2 ).

Fig. 7 .

 7 Fig. 7. Clauses defining the predicates used by the abstract compilation

  an example, let us consider the expression x0=new C();return x0 in a program where C is defined and has no fields. Then H fr , . {x 0 =new C();return x 0 } → H, fr , . {x 0 =o;return x 0 } by rules (ctx) (with context x 0 =[•]; return x 0 ) and (new), where H = o → C, ; H fr , . {x 0 =o;return x 0 } → H, fr , . {o;return x 0 } by rules (ctx) (with context [•]; return x 0 ) and (var-asn), where fr = x → o, x 0 → o; H fr , . {o;return x 0 } → H, fr , . {return x 0 } by rules (ctx) (with context fr , . {[•]}) and (seq); finally, H fr , . {return x 0 } → H, o by rule (return) (with context [•]).

  Type inference of the main expression is obtained by coinductive resolution of the goal B in Hf d ∪Hf n . The Horn formula Hf d contains all clauses that are independent of the program (Figure 7), whereas each Hf i is obtained by compiling the class declaration cd i (see below); the goal B is generated from the compilation of the main expression e (see below); the term t corresponds to the returned type of e; it is ignored here, but it is necessary for compiling expressions. The compilation of a class declaration class c 1 extends c 2 { f n md k } is a set of clauses, including each clause Hf i obtained by compiling the method

The judgment cd n e (Hf d ∪ Hf n |B ) states that the program cd n e is compiled into the pair (Hf d ∪ Hf n |B ), where Hf d ∪ Hf n is a Horn formula (that is, a set of Horn clauses), and B is a goal. 5

  class Square { ... equals ( s ){ return this . side == s . side ;} ... } class ColoredSquare extends Square { ... equals ( cs ){ return this . side == cs . side && this . color == cs . color ;} ... } According to our compilation scheme, the expression s1.equals(s2) has type Bool if s1 and s2 have type Square and Square∨ColoredSquare, respectively, but the same expression is not well-typed if s1 has type ColoredSquare (hence, ColoredSquare ≤Square), since s2 cannot contain an instance of Square for which field color is not defined. Subtyping is required for defining the predicates var upd and field upd for virtual register and field updates: the type of the source must be a subtype of the type of the destination. Type empty is the bottom of the subtyping relation. The predicates inter and diff (see below) can generate empty when a branch is unreachable. Of course, field accesses and method invocations on type empty are correct (in practice they can only occur in dead code).

Available at ftp://ftp.disi.unige.it/person/AnconaD/tcs12long.pdf

Such a constraint does not imply any loss of generality, since it is always possible to add new virtual registers and to insert a ϕ-function when the source code contains multiple returns.

The straightforward definitions of the auxiliary functions have been omitted.

For simplicity we use the same meta-variable B to denote conjunctions of atoms (that is, clause bodies), and goals, even though more formally goals are special clauses of the form false ← B .

A Proof of soundness

To sketch the proof of soundness of abstract compilation, abstract compilation of expressions has to be extended to cover also runtime expressions, hence we define the new judgment H, fr , e (t | B ) (defined in Figure 8) stating that the runtime expression e compiles to the type t and the conjunction of atoms B in the heap H and stack frame fr . Heaps and stack frames are needed for compiling object values and virtual registers. All rules obtained as straightforward extension of the corresponding rules in Figure 6 have been omitted.

In the sequel, all


Hongyu Liang
email: lianghy08@mails.tsinghua.edu.cn

The Algorithmic Complexity of k-Domatic Partition of Graphs ⋆

. In addition, we determine the exact values of the k-domatic number of some particular classes of graphs.

Introduction

In this paper we consider only simple and undirected graphs, and we follow [START_REF] Diestel | Graph Theory[END_REF] for notations and terminologies in graph theory. Let G = (V, E) be a simple and undirected graph. For a vertex v ∈ V , let N G (v) denote the set of neighbors of v, and deg G (v) = |N G (v)| is the degree of v. When no ambiguity arises, we sometimes drop the subscript G. Let δ(G) = min v∈V {deg(v)} be the minimum degree of G. For an integer k ≥ 1, a k-coloring of G is a mapping c : V → {1, 2, . . . , k} such that c(u) ̸ = c(v) whenever {u, v} ∈ E. We say G is k-colorable if G has a k-coloring.

Domination theory is a very important branch of graph theory which has found applications in numerous areas; see [START_REF] Haynes | Domination in Graphs: Advanced Topics[END_REF][START_REF] Haynes | Fundamentals of Domination in Graphs[END_REF] for a comprehensive treatment and some detailed surveys on (earlier) results of domination in graphs. A set of vertices S ⊆ V is called a dominating set of G if every vertex in V \ S has at least one neighbor in S. The domination number of G is the minimum size of a dominating set of G. A domatic partition of G is a partition of V into (disjoint) dominating sets of G. The domatic number of G, denoted by d(G), is the maximum number of dominating sets in a domatic partition of G. The concept of domatic number was introduced by Cockayne and Hedetniemi [START_REF] Cockayne | Towards a theory of domination in graphs[END_REF], which has been proven very useful in various situations such as locating facilities in a network [START_REF] Fujita | A study on r-configurations -a resource assignment problem on graphs[END_REF], clusterhead rotation in sensor networks [START_REF] Misra | Efficient clusterhead rotation via domatic partition in self-organizing sensor networks[END_REF], prolonging the lifetime and conserving energy of networks [START_REF] Islam | Maximizing the lifetime of wireless sensor networks through domatic partition[END_REF][START_REF] Pemmaraju | Energy conservation via domatic partitions[END_REF], and many others.

Let k ≥ 1 be a fixed integer. A k-dominating set of G is a set of vertices S ⊆ V with the property that every vertex in V \S has at least k neighbors in S. Clearly a 1-dominating set is just a dominating set. The notion of k-dominating set was proposed by Fink and Jacobson [START_REF] Fink | n-domination in graphs[END_REF][START_REF] Fink | On n-domination, n-dependence and forbidden subgraphs[END_REF], and has since then been extensively studied for both its theoretical interest and its practical applications in fault-tolerant domination in networks; see, e.g., [START_REF] Caro | A note on the k-domination number of a graph[END_REF][START_REF] Favaron | On k-domination and minimum degree in graphs[END_REF][START_REF] Fujisawa | Independence and 2-domination in bipartite graphs[END_REF][START_REF] Pepper | Implications of some observations about the k-domination number[END_REF][START_REF] Rautenbach | New bounds on the k-domination number and the k-tuple domination number[END_REF] and the references therein. It is known that deciding the size of the minimum k-dominating set of a graph is NP-hard [START_REF] Telle | Complexity of domination-type problems in graphs[END_REF]. (In the literature, some researchers use the name k-dominating set to refer to another variant of dominating set, namely the distance-k dominating set [START_REF] Hansberg | Distance domination and distance irredundance in graphs[END_REF][START_REF] Meir | Relations between packing and covering number of a tree[END_REF]

.) A k-domatic partition of G is a partition of V into (disjoint) k-dominating sets of G. The k-domatic number of G, denoted by d k (G), is the maximum num- ber of k-dominating sets in a k-domatic partition of G. Thus d 1 (G) = d(G).
The concept of k-domatic number was first studied by Zelinka [START_REF] Zelinka | On k-ply domatic numbers of graphs[END_REF] under the name "k-ply domatic number," and was later rediscovered and studied under its current name by Kämmerling and Volkmann [15]. This concept is useful for modeling networks that need domatic partitions with higher degree of domination. As an example, imagine that we wish to locate resources in a network to facilitate the users (i.e., nodes). A user in the network can access resources only from itself and his neighboring nodes. A user is surely happy if there is one resource at his location, but if not, he would only be satisfied if he could access at least k copies of resources from its neighbors, keeping the possibility of multiple choices as a compensation of distance. Then the set of nodes with resources satisfying all the users is exactly a k-dominating set of the network. Now suppose we wish to distribute different types of resources (to enhance the quality of life of users) with the natural constraint that at most one kind of resource can be placed at each node. Then the maximum number of resource types that can be put in the network is precisely the k-domatic number of its underlying graph.

Despite being a natural generalization of the domatic number whose combinatorial and algorithmic aspects have both been well understood, the k-domatic number lacks an investigation from a complexity viewpoint, which motivates our study.

In this paper, we explore the k-domatic number mainly from the algorithmic complexity point of view, and obtain several results that fill the blank in this line of research. In Section 2 we prove that for every k ≥ 1, it is N P-complete to decide whether the k-domatic number of a given bipartite graph is at least 3. This generalizes the NP-completeness result for the 1-domatic number [START_REF] Garey | Computers and Intractability: A Guide to the Theory of NP-Completeness[END_REF]. We then present in Section 3 a polynomial time algorithm that approximates the k-domatic number of a given graph of order n within factor ( 1 k +o(1)) ln n, which generalizes the (1 + o(1)) ln n approximation for the domatic number given in [START_REF] Feige | Approximating the domatic number[END_REF]. Finally, as a minor contribution, we determine in Section 4 the exact values of the k-domatic number of some special classes of graphs.

Complexity of Computing the k-Domatic Number

In this section we show the hardness of computing the k-domatic number of a graph. Our main theorem is as follows.

Theorem 1. For every fixed integer k ≥ 1, it is N P-complete to decide whether the k-domatic number of a given graph is at least 3.

To establish Theorem 1 we introduce a new variant of the coloring problem, which may have its own interest in other scenarios. Let k be a fixed positive integer and H = (V, E) be a 2k-uniform hypergraph, i.e., a hypergraph in which each edge contains exactly 2k vertices. A mapping c : V → {1, 2, 3} is called a balanced 3-coloring of H if for every e ∈ E, there exist 1 ≤ i < j ≤ 3 such that |c -1 (i) ∩ e| = |c -1 (j) ∩ e| = k; that is, every edge of H contains exactly k vertices of color i and k vertices of color j (and no vertices of the color other than i and j). Define the 2k-Uniform Hypergraph Balanced 3-Coloring Problem as follows:

2k-Uniform Hypergraph Balanced 3-Coloring Problem (2kHB3C, for short)

Instance: A 2k-uniform hypergraph H. Question: Does H have a balanced 3-coloring?

Lemma 1. For every fixed integer k ≥ 1, 2kHB3C is N P-complete.

Proof. Let k be a fixed positive integer. The 2kHB3C problem is clearly in N P, since we can verify in polynomial time whether a given mapping is a balanced 3-coloring of H by exhaustively checking all its edges. We now present a polynomial-time reduction from the Graph 3-Coloring problem (G3C for short), which is a classical N P-complete problem [START_REF] Garey | Computers and Intractability: A Guide to the Theory of NP-Completeness[END_REF], to 2kHB3C. An instance of G3C consists of a graph G, and the goal is to decide whether G is 3-colorable.

Let G = (V, E) be a graph serving as the input to G3C. We will construct a 2k-uniform hypergraph H from G. Informally speaking, the hypergraph H can be obtained as follows: For each edge e ∈ E, we associate it with a 2k-uniform hypergraph H e , where H e has vertex set X e ∪ Y e with |X e | = |Y e | = 3k, and contains all possible hyperedges that consist of exactly k vertices from X e and another k vertices from Y e . The number of such hyperedges is

( 3k k ) • ( 3k k ) < 2 6k
, which is a constant since k is a fixed integer. Let H be the union of all such (disjoint) hypergraphs. Finally, for each e ∈ E, add to H a hyperedge which consists of both vertices in e, the first k -1 vertices in X e , and the first k -1 vertices in Y e . This finishes the construction of H. It is clear that H can be constructed in polynomial time.

We now give a rigorous definition of H. For every e ∈ E, let

-X e = {x e,i | 1 ≤ i ≤ 3k} and Y e = {y e,i | 1 ≤ i ≤ 3k}; -E ′ e = {X ∪ Y | X ⊆ X e ; Y ⊆ Y e ; |X| = |Y | = k}; -e ′ = e ∪ {x e,i , y e,i | 1 ≤ i ≤ k -1}. Let V ′ = V ∪ ∪ e∈E (X e ∪ Y e )
, and

E ′ = {e ′ | e ∈ E} ∪ ∪ e∈E E ′ e . Finally let H = (V ′ , E ′ ). It is easy to verify that H is a 2k-uniform hypergraph with |V ′ | = |V | + 6k|E| and |E ′ | = (1 + ( 3k k ) • ( 3k k )
)|E|. We will prove that G is 3-colorable if and only if H has a balanced 3-coloring. First consider the "only if" direction. Assume that G is 3-colorable and c :

V → {1, 2, 3} is a 3-coloring of G. Define a function c ′ : V ′ → {1, 2, 3} as follows. First let c ′ (v) = c(v) for all v ∈ V . For each edge e = {u, v} ∈ E, suppose c(u) = a and c(v) = b where a, b ∈ {1, 2, 3} (note that a ̸ = b). Then, let c ′ (x) =
a for all x ∈ X e and c ′ (y) = b for all y ∈ Y e . We verify that the mapping c ′ defined above is a balanced 3-coloring of H. This can be seen as follows:

-For each hyperedge h = X ∪ Y with X ⊆ X e and Y ⊆ Y e for some e ∈ E, by our definition, h contains exactly k vertices of the same color with that of one endpoint of e, and another k vertices of the same color with that of the other endpoint of e. Since the two endpoints of e have different colors, h satisfies the property of balanced 3-coloring. -For each hyperedge e ′ = e ∪ {x e,i , y e,i | 1 ≤ i ≤ k -1} for some e, similar to the previous case, h consists of precisely k vertices of one color and the other k vertices of another color.

Therefore, c ′ is a balanced 3-coloring of H.

We next consider the "if" direction. Suppose that c ′ is a balanced 3-coloring of H. Let e = {u, v} be an arbitrary edge in E. We claim that all the vertices in X e have the same color i for some i ∈ {1, 2, 3}, all those in Y e have the same color j for some j ∈ {1, 2, 3}, and i ̸ = j. This will imply that u and v have different colors under c ′ , since otherwise the hyperedge e ′ = e ∪ {x e,i , y e,i | 1 ≤ i ≤ k -1} is not balanced. We now prove the above claim. As |X e | = 3k, there exists i ∈ {1, 2, 3} such that the number of vertices in X e with color i is at least k; without loss of generality we assume that c ′ (x e,1 ) = c ′ (x e,2 ) = . . . = c ′ (x e,k ) = i. Since the hyperedge {x e,1 , x e,2 , . . . , x e,k } ∪ Y exists for all Y ⊆ Y e with |Y | = k, we know that in every size-k subset of Y e , all the vertices have the same color. Thus, all vertices in Y e has the same color, say j, and obviously j ̸ = i. Analogously, all vertices in X e has the same color i, proving the claim. According to our previous analysis, the claim implies that c ′ (u) ̸ = c ′ (v) for all {u, v} ∈ E. Therefore, the mapping c :

V → {1, 2, 3} defined by c(v) = c ′ (v) for all v ∈ V is a 3-coloring of G, and hence G is 3-colorable.
This finishes the reduction from G3C to 2kHB3C, and thus concludes the proof of Lemma 1.

We now proceed to prove Theorem 1.

Proof (of Theorem 1).

Let k be a fixed positive integer. We reduce 2kHB3C to the problem of deciding whether d k (G) ≥ 3 for a given graph G. Note that the latter problem is clearly in N P. Let H = (V, E) be a 2k-uniform hypergraph given as an input to the 2kHB3C problem. We construct a graph G = (V ′ , E ′ ) as follows. Let We shall show that H has a balanced 3-coloring if and only if d k (G) ≥ 3, which will complete the reduction and prove the N P-completeness of the desired problem.

V ′ = X ∪ Y ∪ Z, where X = {x e | e ∈ E}, Y = {y v | v ∈ V }, and Z = {z i | 1 ≤ i ≤ 3k}. Let E ′ = {{x e , y v } | v ∈ e ∈ E} ∪ {{y v , z i } | v ∈ V ; 1 ≤ i ≤ 3k} ∪ {{z i , z j } | 1 ≤ i < j ≤ 3k}. Thus, G[X ∪ Y ] is the incidence graph of H, G[Y ∪ Z]
First consider the "only if" direction. Assume that H has a balanced 3-

coloring c : V → {1, 2, 3}. For each e ∈ E let C e = {i | ∃ v ∈ e s.t. c(v) = i}; clearly |C e | = 2. We now design a partition (V ′ 1 , V ′ 2 , V ′ 3 ) of V ′ as follows: For each i ∈ {1, 2, 3}, let V ′ i = {x e | i ̸ ∈ C e }∪ {y v | c(v) = i}∪ {z j | (i -1)k + 1 ≤ j ≤ ik}.
It is easy to see that this is indeed a partition of V ′ . Furthermore, we will prove that for each i ∈ {1, 2, 3},

V ′ i is a k-dominating set of G. Fix i ∈ {1, 2, 3}. Notice that V ′ \ V ′ i = {x e | i ∈ C e } ∪ {y v | c(v) ̸ = i} ∪ {z j | j ∈ {1, . . . , 3k} \ {(i -1)k + 1, . . . , ik}}. By our construction of G, every vertex in (Y ∪ Z) \ V ′ i is adjacent to k vertices in V ′
i , which are z (i-1)k+1 , . . . , z ik . For each x e ∈ X \ V ′ i , we have i ∈ C e by our definition of V ′ i . Thus, there exists u ∈ e for which c(u) = i. Because c is a balanced 3-coloring of H, there exist exactly k vertices in e that have value i under c, which indicates that those k vertices are all included in V ′ i . Therefore, x e is adjacent to at least k vertices in V ′ i . This proves that V ′ i , for every i ∈ {1, 2, 3}, is a k-dominating set of G, and hence d k (G) ≥ 3, finishing the proof of the "only if" direction of the reduction.

We now turn to the "if" direction. Assume that d k (G) ≥ 3 and (V ′ 1 , V ′ 2 , V ′ 3 ) is a k-domatic partition of G. Define a mapping c : V → {1, 2, 3} as follows: For every v ∈ V , let c(v) = i where i is the unique integer satisfying that y v ∈ V ′ i . We show that c is a balanced 3-coloring of H. Consider an arbitrary edge e ∈ E, and assume without loss of generality that x e ∈ V ′ 1 (and thus

x e ̸ ∈ V ′ 2 ∪ V ′ 3 )
. By the definition of k-dominating sets, for each j ∈ {2, 3},

|N G (x e ) ∩ V ′ j | ≥ k. As |N G (x e )| = |{y v | v ∈ e}| = 2k and V ′ 2 ∩ V ′ 3 = ∅, we have |N G (x e ) ∩ V ′ 2 | = |N G (x e ) ∩ V ′ 3 | = k.
Thus, c(y v ) = 2 for exactly k vertices v ∈ e, and c(y v ) = 3 for the other k ones, showing the validity of the coloring on edge e. Hence, c is indeed a balanced 3-coloring of H. This concludes the "if" direction of the reduction.

The proof of Theorem 1 is thus completed.

We remark that the N P-completeness result holds even if the input graph is bipartite. To see this, we modify the construction of G in the proof as follows: Add 3k vertices {z ′ i | 1 ≤ i ≤ 3k} to H, add an edge between every possible pair (z i , z ′ j ), and let H[Z] be an empty graph (instead of being a complete graph as in the previous proof). Then it is easy to verify that G is a bipartite graph. The remaining part of the proof goes through analogously. The only modification is that when proving the "only if" direction of the reduction, we define the partition (

V ′ 1 , V ′ 2 , V ′ 3 ) as V ′ i = {x e | i ̸ ∈ C e } ∪ {y v | c(v) = i} ∪ {z j , z ′ j | (i -1)k + 1 ≤ j ≤ ik}.
Therefore we obtain: Corollary 1. Deciding whether the k-domatic number of a bipartite graph is at least 3 is N P-complete for every fixed positive integer k.

The following corollary is immediate.

Corollary 2. For every fixed integer k ≥ 1, computing the k-domatic number of a bipartite graph is N P-hard.

Approximation Algorithm for k-Domatic Number

Since computing the k-domatic number is N P-hard, we are interested in designing approximation algorithms for it. In this section we present a logarithmicfactor approximation algorithm for computing the k-domatic number of a graph, generalizing the result of [START_REF] Feige | Approximating the domatic number[END_REF] for the 1-domatic number.

Theorem 2. For every fixed integer k ≥ 1, the k-domatic number of a given graph of order n can be approximated within a factor of ( 1 k + o( 1)) ln n in polynomial time.

Proof. Fix an integer k ≥ 1. Let G = (V, E) be a graph of order n ≥ N 0 , where N 0 is a sufficiently large but fixed integer (which may depend on k). (Note that the k-domatic number of a graph order n ≤ N 0 can be computed in constant time.) If δ(G) ≤ ln n + 3k ln ln n, due to Theorem 2.9 in [START_REF] Kämmerling | The k-domatic number of a graph[END_REF], we have 1)) ln n. In this case, a trivial k-domatic partition that consists of only V itself is already a ( 1 k + o( 1)) ln n approximate solution. Therefore, we assume in what follows that δ(G) > ln n + 3k ln ln n.

d k (G) ≤ δ(G) k + 1 ≤ ( 1 k + o(
Let t = δ(G)/(ln n + 3k ln ln n). For every vertex v ∈ V , assign a label l(v) ∈ {1, 2, . . . , t} to v uniformly at random; that is, l(v) = i with probability 1/t for all i ∈ {1, 2, . . . , t}. Let S i , 1 ≤ i ≤ t, be the set of vertices that receive label i. Evidently {S 1 , S 2 , . . . , S t } is a partition of V . For v ∈ V and i ∈ {1, 2, . . . , t}, let E(v, i) denote the event that at most k -1 neighbors of v have label i. If there is no v ∈ V for which E(v, i) holds, then every vertex v ∈ V has at least k neighbors in S i , and hence S i is a k-dominating set of G. For all v ∈ V and i ∈ {1, 2, . . . , t}, we have

P r[E(v, i)] = k-1 ∑ j=0 ( deg(v) j ) ( 1 t ) j ( 1 - 1 t ) deg(v)-j ≤ k-1 ∑ j=0 (deg(v)) j ( 1 t ) j ( 1 - 1 t ) deg(v)-j = ( 1 - 1 t ) deg(v) • k-1 ∑ j=0 ( deg(v) t ( 1 - 1 t ) -1 ) j ,
where the first inequality follows from the fact that

( n1 n2 ) ≤ n n2 1 for two positive integers n 1 ≥ n 2 . As deg(v) t (1 -1 t ) -1 = deg(v) t-1 ≥ deg(v) δ(G) ≥ 1, we have P r[E(v, i)] ≤ ( 1 - 1 t ) deg(v) • k-1 ∑ j=0 ( deg(v) t ( 1 - 1 t ) -1 ) k-1 = ( 1 - 1 t ) deg(v) • k • ( deg(v) t ) k-1 ( 1 - 1 t ) -k+1 = k ( 1 - 1 t ) deg(v)-k+1 ( deg(v) t ) k-1 ≤ k • exp ( - deg(v) -k + 1 t + (k -1) ln ( deg(v) t
))

(where we use 1 + x ≤ e x for all x ∈ R, and denote exp(m) := e m ).

Define a function f as f (x) = -x + (k -1) ln x. Clearly f is non-increasing on [X 0 , ∞) for some sufficiently large but fixed X 0 (depending on k only). As

deg(v) t ≥ δ(G) t = Ω(ln n), by choosing large enough n ≥ N 0 we have f ( deg(v) t ) ≤ f ( δ(G)
t ), and thus

P r[E(v, i)] ≤ k • exp ( - δ(G) -k + 1 t + (k -1) ln ( δ(G) t )) = k • exp ( - δ(G) -k + 1 δ(G)
= n -1 (ln n) -k .
Call a pair (v, i) bad if the event E(v, i) happens. By linearity of expectation, the expected number of bad pairs is

∑ v∈V ;1≤i≤t P r[E(v, i)] ≤ nt • n -1 (ln n) -k = t • o(1).
Recall that

S i = {v ∈ V | l(v) = i} for each i ∈ {1, 2, . . . , t}.
Notice that S i is a k-dominating set of G if and only if there is no v ∈ V such that (v, i) is a bad pair. Clearly a bad pair (v, i) can "prevent" at most one such set, namely S i , from being a k-dominating set of G. Hence, the expected number of k-dominating sets among {S i | i ∈ {1, 2, . . . , t}} is at least t -t • o(1) = (1 -o(1))t. By checking the t sets S 1 , S 2 , . . . , S t one by one, we can find all the k-dominating sets among them. Add the vertices not covered by these sets to them arbitrarily. Then, we obtain a k-domatic partition of G of (expected) size (1 -o(1))t. This solution has an approximation factor of 1)

d k (G) (1 -o(1))t ≤ δ(G) k + 1 (1 -o(1))δ(G)/(ln n + 3k ln ln n) ≤ ( 1 k + o(
) ln n .
Finally we show that this algorithm can be efficiently derandomized by the method of conditional probabilities. Order the vertices in V arbitrarily, say v 1 , v 2 , . . . , v n . We assign labels to the vertices according to this order, from v 1 to v n . Suppose we are dealing with v i , and the labels of v 1 , . . . , v i-1 have already been fixed to be l 1 , . . . , l i-1 , respectively. We try all the possible labels 1, 2, . . . , t one by one, and assign v i with the label l i that minimizes the expected number of bad pairs conditioned on that (∀1 ≤ s ≤ i) l(v s ) = l s . (Recall that l(v) is the label of v; here we regard it as a random variable.) This expected number can be computed in polynomial time, because it is equal to

∑ v∈V ;1≤j≤t P r[E(v, j) | (∀1 ≤ s ≤ i) l(v s ) = l s ],
where, denoting by r j the number of neighbors of v i that has already been given label j, we have

P r[E(v, j)] =      0, if r j ≥ k; 1, if r j < k and ∑ t q=1 r q = deg(v); ∑ k-1-rj j ′ =0 ( deg(v)- ∑ t q=1 rq j ′ ) ( 1 t ) j ′ ( 1 -1 t ) deg(v)- ∑ t q=1 rq-j ′ , otherwise.
Since k is fixed, we can compute every P r[E(v, j)] in polynomial time, and there are only |V | • t ≤ n 2 of them.

By our choice of labels, after all labels have been determined, the number of bad pairs does not exceed the expected number of bad pairs estimated before. The remaining arguments go through analogously as before, and we can obtain a solution of approximation factor ( 1 k + o( 1)) ln n. This completes the proof of Theorem 2.

k-Domatic Number of Special Graphs

In this section we determine the exact values of the k-domatic number of some special classes of graphs. By Theorem 2.9 in [START_REF] Kämmerling | The k-domatic number of a graph[END_REF],

d k (G) ≤ δ(G) k + 1. As d k (G) is a positive integer, we have d k (G) = 1 whenever k > δ(G).
V = {v 0 , v 1 , v 2 , . . . , v n } and edge set E = {v i v i+1 | 1 ≤ i ≤ n-1}∪{v 0 v i | 1 ≤ i ≤ n}. Obviously δ(F n ) = 2.
Theorem 3. Let n ≥ 2 be an integer. Then,

d 2 (F n ) = { 1 if n ∈ {2, 4}; 2 otherwise.
Proof. We have d 2 (F n ) ≤ δ(F n )/2 + 1 = 2. When n is odd, it can be verified that V 0 := {v i | 0 ≤ i ≤ n; i is even} and V 1 := {v i | 0 ≤ i ≤ n; i is odd} are both 2-dominating sets of F n , and clearly (V 0 , V 1 ) is a partition of V . Thus d 2 (F n ) = 2 when n is odd. If n = 2 or 4, it can be checked exhaustively that d 2 (F n ) = 1. Now consider the case where n is even and n ≥ 6. Let Z 0 = {v i | 0 ≤ i ≤ n -4; i is even} ∪ {v n-1 }, and Z 1 = V \ Z 0 . It is easy to see that for each j ∈ {0, 1}, every vertex in Z j is adjacent to at least two vertices in Z 1-j . Thus Z 0 and Z 1 are both 2-dominating sets of G, indicating that d 2 (F n ) ≥ 2. Hence d 2 (F n ) = 2, and the proof of Theorem 3 is complete.

For every integer n ≥ 3, let W n denote the wheel graph with vertex set V = {v 0 , v 1 , v 2 , . . . , v n } and edge set Proof. First note that d 3 (W n ) ≤ ⌊δ(W n )/3⌋ + 1 = 2. Assume that d 3 (W n ) = 2 and (V 0 , V 1 ) is a 3-domatic partition of G. Also assume without loss of generality that v 0 ∈ V 0 . If v i ̸ ∈ V 1 for some 1 ≤ i ≤ n, then all the three neighbors of v i must belong to V 1 , implying that v 0 ∈ V 1 which is a contradiction. Thus V 1 = {v 1 , v 2 , . . . , v n } and V 0 = {v 0 }. But then V 0 is not a 3-dominating set of G. Therefore d 3 (W n ) = 2 cannot hold, and thus d 3 (W n ) = 1.

E = {v i v i+1 | 1 ≤ i ≤ n -1} ∪ {v n v 1 } ∪ {v 0 v i | 1 ≤ i ≤ n}. Clearly δ(W n ) = 3.

  contains a complete bipartite subgraph with partition (Y, Z), and G[Z] is a clique. It is clear that the construction of G can be finished in polynomial time.

  /(ln n + 3k ln ln n) + (k -1) ln ( δ(G) δ(G)/(ln n + 3k ln ln n) )) = k • exp (-(ln n + 3k ln ln n)(1 -O(1/ ln n)) + (k -1) ln (ln n + 3k ln ln n)) (where we use δ(G) > ln n and k = O(1)) ≤ exp (-ln n -2k ln ln n + o(ln ln n)) ≤ exp (-ln n -k ln ln n)

  Therefore, when considering d k (G) we only care those k for which 2 ≤ k ≤ δ(G). (The case k = 1 corresponds to the domatic number, which has been extensively studied in the literature.)For every integer n ≥ 2, let F n denote the fan graph with vertex set

Theorem 4 .

 4 d 2 (W n ) = 2 for every integer n ≥ 3. Proof. Let V 0 = {v i | 0 ≤ i ≤ n; i is even} and V 1 = {v i | 0 ≤ i ≤ n; i is odd}.It is easy to verify that V 0 and V 1 are both 2-dominating sets of W n (regardless of the parity of n), and thus d 2 (W n ) ≥ 2. On the other hand, we haved 2 (W n ) ≤ ⌊δ(W n )/2⌋ + 1 = 2. Hence d 2 (W n ) = 2.Theorem 5. d 3 (W n ) = 1 for every integer n ≥ 3.

Acknowledgement

The author is grateful to the anonymous referees for their helpful suggestions on improving the presentation of this paper.

⋆ This work was supported in part by the National Basic Research Program of China Grant 2011CBA00300, 2011CBA00301, and the National Natural Science Foundation of China Grant 61033001, 61061130540, 61073174.