Hong Nam Nguyen
email: nguyen-hong.nam@usth.edu.vn

Hoai Son Nguyen

Minh Ha-Duong
email: minh.haduong@gmail.com

Laurent Van De Steene
email: laurent.van_de_steene@cirad.fr

Biomass gasification in Southeast Asia: Factors influencing technology adoption in Cambodia

Keywords: biomass, Cambodia, gasification, national grid, rice husk

Electricity price in Cambodia is among the highest in the region due to limited fossil resources. The national grid provides electricity with cheapest tariff, from $0.11 to $0.27 per kWh, but only 25% of Cambodians are having access to it. Since 2003, scores of rice mills have installed rice husk gasification systems (RHGs) to produce electricity with a cost from $0.06 to $0.27 per kWh. RHG development is showing signs of slowing down while national grid is continuing to expand its supply area. The study was carried out to identify some factors influencing RHG adoption in Cambodian rice mills, based on data of rice mills (n=396) and report on power sector of the Kingdom of Cambodia in 2015. Field trips to rice mills (n=8) and interviews with RHG stakeholders (n = 66)

were also conducted. Results indicated that technical support for RHG and annual production of rice mills had positively influenced adoption of RHG. In contrarily, results showed an insignificant correlation between the presence of national grid and RHG adoption. This study will help planners, policy makers, researchers and farmers prioritize factors affecting RHG adoption decisions and hence provide insight on pathways to increase RHG adoption.

Introduction

The price of electricity in Cambodia is among the highest in the Southeast Asia region due to limited domestic fossil fuel resources. The state-owned electricity provider Electricité du Cambodia (EDC) provides electricity with cheapest tariffs, ranging from $0.09 to $0.25 per kilowatt-hour (kWh). However, only 25% of Cambodians are having access to EDC national grid (Electricity Authority of Cambodia, 2015). Other domestic suppliers use diesel as fuel and supply electricity at tariffs between $0.75 and $1 per kWh. This has led people living in areas without access to the EDC grid to try new technologies to produce electricity at a lower cost.

Since 2003, scores of Cambodian rice mills have installed rice husk gasification systems (RHGs) in rural areas to produce electricity to run their milling machinery with a cost from $0.06 to $0.27 per kWh [START_REF] Ngin | Status of rice husk gasifiers; rice husk and rice husk char from gasifiers in 12 provinces of Cambodia[END_REF][START_REF] Nguyen | A critical look at rice husk gasification in Cambodia: technology and sustainability[END_REF]. Rice husk, a by-product of the milling process, is an abundant source of biomass in Cambodia, with 2 million tons produced in 2014 [START_REF] Pode | Sustainable rural electrification using rice husk biomass energy: A case study of Cambodia[END_REF]. Biomass gasification is a thermochemical conversion process that converts biomass into a carbon monoxide and hydrogen rich-gas called synthesis gas, or syngas. Syngas can be utilized to produce heat, electricity or fuel transportation. Some different generic types of gasifiers have been developed for the conversion of biomass feedstock, namely fixed bed, fluidized, entrained flow and mutistage gasifier. All RHGs in Cambodian rice mills are down-draft fixed bed gasification systems [START_REF] Ha-Duong | Rice husk gasification for electricity generation in Cambodia[END_REF][START_REF] Ngin | Status of rice husk gasifiers; rice husk and rice husk char from gasifiers in 12 provinces of Cambodia[END_REF], imported or manufactured locally. The RHG technology has been showing a high potential for small and medium power production.

Nevertheless, the technology development proceeds slowly because of both technical and nontechnical brakes.

RHGs arrived on off-grid regions where electricity was produced by using diesel with a very high price. But recently the Cambodian government is doing efforts to expand the national grid network. Prices are more or less the same between electricity from national grid and RHG. Does national grid then affect RHG adoption? It is less interesting to produce electricity independently if it can be bought. Very few researches have been carried out on electrification using RHGs in Cambodia (Abdul [START_REF] Salam | The status of biomass gasification in Thailand and Cambodia[END_REF][START_REF] Akgün | Extension of rice husk gasification technology for electricity generation in Cambodia[END_REF][START_REF] Pode | Sustainable rural electrification using rice husk biomass energy: A case study of Cambodia[END_REF], and literature data seems to be lacking in identifying the factors influencing the adoption of this technology. The aim of this paper thus was to identify factors influencing RHG adoption in Cambodian rice mills with the focus on the presence of the national grid.

Methodology

Data source

The data on Cambodian national grid used to examine the RHG adoption model was obtained from the report on power sector of the Kingdom of Cambodia in 2014 provided by Electricity of Cambodia (Electricity Authority of Cambodia, 2015). For Cambodian rice mills, we used the cross-sectional data of 396 rice mills provided by the Federation of Cambodian Rice Millers Associations. This data provides a wide range of characteristics of rice mills as well as RHG installations.

Modelling RHG adoption

Binary logistic regression is a popular statistical technique in which the probability of a dichotomous outcome (e.g. adoption or non-adoption) is related to a set of explanatory variables and has been widely applied in adoption studies [START_REF] Adesina | Determinants of farmers' adoption and adaptation of alley farming technology in Nigeria[END_REF][START_REF] Chianu | Determinants of farmers' decision to adopt or not adopt inorganic fertilizer in the savannas of northern Nigeria[END_REF]. In this research, rice mills' adoption of RHG is based on an assumed underlying utility function. According to this theory RHG will be adopted by the rice mill, if the utility obtained from RHG adoption exceeds that of non-adoption. The rice mills' behaviour towards RHG is described by Eq.1:

ln ( 𝑃𝑖 1 -𝑃𝑖 ) = ln(𝑜𝑑𝑑𝑠) = 𝛽 0 + ∑ 𝛽 𝑘 𝑋 𝑘𝑖 𝑛 𝑘=1 + 𝜀 𝑖 (1)
where 0 is the intercept term, and 1, 2,…, i are coefficients associated with each explanatory variable X1, X2,…, Xk. Gathered in a vector X, these factors explain the RHG adoption decision, or the probability that the ith rice mill adopts RHG. For adoption analysis, adoption is usually defined in terms of a binary variable (adoption/not adoption). The dependent variable ADOP was defined as a binary variable with a value of 1 for rice mills who have adopted RHG and 0 for those who have not adopted it.

The explanatory variable GRID is a dummy variable which measures whether or not the rice mill is found in the district where the grid is available (1 if yes, 0 if no). The arrival of RHG in Cambodian rice mills in 2003 was originally due to the lack of national grid in many regions, and the high prices of electricity production from diesel (Abdul Salam, Kumar and Siriwardhana, 2010; Nguyen, Ha-Duong and Van de Steene, 2015). However, in 2014, some rice mills have switched from RHGs to national grid for electricity source to run their milling machinery [START_REF] Ngin | Status of rice husk gasifiers; rice husk and rice husk char from gasifiers in 12 provinces of Cambodia[END_REF]. The Cambodian national grid continues to expand, thus it is hypothesized that GRID has an impact on RHG adoption.

The explanatory variable ANNU_PROD measures the annual production of the rice mill, e.g. the volume of rice milled per year. During the field trip, owners of rice mills having small annual production claimed that they were less interested in RHGs because of the high investment cost and the shortage in rice husk supply since their production was not continuous.

In contrarily, large rice mills are generally associated with a greater volume of rice husk available along the year and a greater electricity demand. It is thus hypothesized that ANNU_PROD has an impact on the adoption of RHG in this study.

The explanatory variable TECH_AVAI is a dummy variable which measures whether or not the rice mill is found in the district where the technical support for RHG is available (1 if yes, 0 if no). RHGs in Cambodia can be imported by SME Renewable Energy Ltd., from Ankur Scientific Energy Ltd., a leading gasifier manufacturer based in India, or produced locally.

There are approximately 5 manufacturers competing with SME [START_REF] Nguyen | A critical look at rice husk gasification in Cambodia: technology and sustainability[END_REF]. During the field trips, RHG manufacturers, users and owners all claimed that RHGs often require maintenance or replacement of spare-parts several times per year. Each time doing maintenance, the Ta Uou Seng rice mill owner in Kompong Speu province "has to contact the manufacturer in Phnompenh and wait for them to send a technician from 200 kilometres away". Therefore TECH_AVAI is expected to have an effect on the adoption of RHG.

The description and statistics of the variables specified in the empirical logistic model is presented in Table 1.

Results and discussion

The coefficients of the binary logistic regression model were estimated by maximum likelihood methods using Stata 13. The Pearson's Chi2 and the Hosmer and Lemeshow statistic are the most reliable tests of model fit for binary regression [START_REF] Sidibé | Farm-level adoption of soil and water conservation techniques in northern Burkina Faso[END_REF]. The results of the model are given in Table 2. We fail to reject the null hypothesis that there is no difference between the observed and predicted values of the dependent, implying that the model's estimates very well fit the data at an acceptable level. support near the rice mill, it can shorten the maintenance time and therefore do not need to interrupt the rice mill's operations. This will enhance the willingness to adopt RHG systems.

Results also indicated that and ANNU_PROD was positively correlated with RHG adoption and significant at the 1% level. The more the annual production of the rice mill is, the more fuel stability for RHG and electricity demand. Generally, large rice mills have greater amounts of rice husk available on the spot and more stable throughout the year compared to small rice mills. Large rice mills' owners also have to get rid of rice husk more often, since this residue needs much space to store. Their demand for a technology that can take advantage of these existing amounts of rice husk are therefore more important.

In contrarily, results showed an insignificant correlation between the presence of national grid (GRID) and the adoption of RHG in Cambodian rice mills. Even in regions where grid is available, people still use gasifiers. This may suggest that gasifier development is reaching a certain beneficial level in terms of economy, and may not be dependent on possible expansion of national grid if the electricity price doesn't change over time.

Conclusion

Our study examined factors influencing RHG adoption in Cambodian rice mills with the focus on the presence of the national grid. The technical support availability and annual production of rice mills are positively correlated with RHG adoption. In contrarily with our hypothesis, results showed an insignificant correlation between national grid and RHG adoption, suggesting that this technology that gasifier development is reaching an economically profitable level. That led us to stress the environmental un-sustainability of RHGs in Cambodia that may be costly in the near future when standards for RHG installations in Cambodia will be implemented, and the need to improve technology in our previous study [START_REF] Nguyen | A critical look at rice husk gasification in Cambodia: technology and sustainability[END_REF].

Our results also suggest a dynamic analysis to analyse further the relation between national grid and RHG adoption by taking into account changes in grid tariff over time, especially in the context of fluctuation of oil and diesel prices, as well as changes in price of rice husk feedstock, when rice husk does not remain waste but becomes a commodity.

This study will help planners, policy makers, researchers, extension officers and farmers prioritize the factors that affect adoption decisions and provide insight on pathways to increase the adoption of RHG.

Figure 1 :

 1 Figure 1: Map of Cambodia and national grid distribution (Atlas of Cambodia, 2013)

Table 1 . Description and statistics of variables specified in empirical logistic model

 1 𝛽 1 . 𝐺𝑅𝐼𝐷 𝑖 + 𝛽 2 . 𝑇𝐸𝐶𝐻_𝐴𝑉𝐴𝐼 𝑖 + 𝛽 2 . 𝐴𝑁𝑁𝑈_𝑃𝑅𝑂𝐷 𝑖 + 𝜀 𝑖 (2)

	Variable Description

Table 2 . Parameter estimates of binary logistic regression model for factors influencing RHG adoption

 2

	Variable	Coef.	Std. Err.	P>|z|
	GRID	0.7721	0.58821	0.189
	TECH_AVAI*	1.6059	0.52661	0.002
	ANNU_PROD*	1.4206	0.22825	0.000
	Constant*	-14.8028 2.14329	0.000
	Pearson Chi-square Test: 176.11, Sig., 0.9995. Hosmer and
	Lemeshow Test: Chi-square, 1.88; Sig., 0.9845.

* Significance at 1%

Table 2

 2 showed that the variable TECH_AVAI was positively correlated with RHG adoption and significant at the 1% level. Rice mills found in the district with technical support available have a greater likelihood in adopting RHGs. If the RHG owner can find a technical

Acknowledgement:

We are grateful to the SNV Netherlands in Cambodia, Cambodian rice mill owners and the Federation of Rice Millers' Association and informants for providing very helpful data, information and feedback.


Ran Chen

Jean-Jacques Lévy

Formal proofs of two algorithms for strongly connected components in graphs

We present formal proofs for the two classical Tarjan-1972 and Kosaraju-1978 algorithms for finding strongly connected components in directed graphs. We describe the two algorithms in a functional programming style with abstract values for vertices in graphs, with functions between vertices and their successors, and with data types such that lists (for representing immutable stacks) and sets. We use the Why3 system and the Why3-logic to express these proofs and fully check them by computer. The Why3-logic is a simple multi-sorted first-order logic augmented by inductively defined predicates. Furthermore it provides useful libraries for lists and sets. The Why3 system allows description of programs in a Why3-ML programming language (a first-order programming language with ML syntax) and provides interfaces to various state-ofthe-art automatic provers and to manual interactive proof-checkers (we use mainly Coq). One important point of our article is that our proofs are intuitive and human readable.

Introduction

There is a growing interest in programs proofs checked by computer. Proofs about programs are often very long and have to face a huge amount of cases due to the multiplicity of programs variables and the precise details of the programs. This is very frustrating since we would like to explain the proofs of correctness and publish them in scientific articles. However if one considers simple algorithms, we would expect to explain their proofs of correctness in the same way as we explain a mathematical proof for a non too complex theorem. This surely can be done on algorithms dealing with simple structures, such as arrays, lists or trees [START_REF] Lévy | Essays for the Luca Cardelli Fest, chapter Simple proofs of simple programs in Why3[END_REF]. But we take here the examples of algorithms on graphs where sharing and combinatorial properties holds.

We provide formal proofs for the two classical Tarjan-1972 [START_REF] Sedgewick | Algorithms[END_REF][START_REF] Cormen | Introduction to Algorithms[END_REF] and Kosaraju-1978 [START_REF] Sharir | A strong-connectivity algorithm and its applications in data flow analysis[END_REF] algorithms for finding strongly connected components in directed graphs. Tarjan's algorithm consists in an efficient one-pass depth-first search traversal in graphs which traces the bases of strongly connected components. Kosaraju's algorithm works with two depth-first searchs on a graph and its reversed companion. It uses a post-order traversal allowing to output the strongly connected components one-by-one by considering them in the reversed order of their interconnectivity. We describe these two algorithms in a functional programming style with abstract values for vertices in graphs, with functions between vertices and their successors, and with data types such that lists (for representing immutable stacks) and sets.

We use the Why3 system [START_REF] Filliâtre | Why3 -where programs meet provers[END_REF][START_REF] Bobot | The Why3 platform, version 0.86.1[END_REF] and the Why3-logic to express these proofs and fully check them by computer. The Why3-logic is a simple multi-sorted first-order logic augmented by inductively defined predicates. Furthermore it provides useful libraries for lists and sets. The Why3 system allows description of programs in a Why3-ML programming language (a first-order programming language with ML syntax) and provides interfaces to various state-of-the-art automatic provers and manual interactive proof-checkers (we use mainly Coq with a few ssreflect features).

Our proofs are rather short, namely 244 lines for Tarjan (45 lemmas), 312 lines for Kosaraju (34 lemmas) including the program texts. Most of the 89 proof obligations generated by the Why3 system for our Tarjan Why3-ML program are proved automatically, except 5 of them which are manually checked by Coq with a few ssreflect features [START_REF]The coq 8.5 standard library[END_REF][START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF]. For Kosaraju, the figures are 59 proof obligations, 2 Coq proofs. There is in fact a balance between automatic proofs and the manual ones in order to keep the readability of these formal proofs.

Our claim is that the details of our formal proofs are human readable and rather intuitive. They will all be explained in our paper. The programs are directly inspired by the ones of the textbooks, but we replaced imperative features by immutable program states. This avoids the cumbersome treatment of memory states and restricts attention to the most important data structures of these algorithms. For instance, we do not consider serial numbers for vertices in graphs; we just keep the active parts of the spanning trees, kept in stacks by these two algorithms. But our programs could be refined to the textbooks imperative implementations by several steps that we also indicate in this article. We do think that similar techniques can be applied to many other algorithms on graphs.

Finally our article can present a useful step to compare with other formal methods, for instance within Isabelle or Coq [START_REF] Pottier | Depth-first search and strong connectivity in Coq[END_REF][START_REF] Lammich | A framework for verifying depth-first search algorithms[END_REF][START_REF] Wengener | A simplified correctness proof for a well-known algorithm computing strongly connected components[END_REF][START_REF] Théry | Formally-proven Kosaraju's algorithm[END_REF][START_REF] Gonthier | Finite graphs in mathematical components[END_REF][START_REF] Charguéraud | Program verification through characteristic formulae[END_REF][START_REF] Charguéraud | Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation[END_REF][START_REF] Charguéraud | Higher-order representation predicates in separation logic[END_REF][START_REF] Appel | Verified Functional Algorithms[END_REF][START_REF] Poskitt | Hoare logic for graph programs[END_REF][START_REF] Mehta | Proving pointer programs in higher-order logic[END_REF].

The program may look quite inefficient since it deals with lists and sets, but the imperative version is quite efficient as discussed in the conclusion. The next section will present the first algorithm; section 3 presents the pre-/postconditions and assertions inserted in the program and section 4 will discuss the proof of various lemmas; section 5 shows the possible refinement to imperative programs. In section 6 we present and prove the Kosaraju's algorithm. We conclude in section 7.

A first algorithm

We consider Tarjan-1972 algorithm [START_REF] Sedgewick | Algorithms[END_REF][START_REF] Cormen | Introduction to Algorithms[END_REF] for finding strongly connected components in a directed graph. This algorithm consists in a one-pass depth-first search traversal on graphs. It maintains a stack of visited vertices and the rank of the oldest vertex accessible by at most one back-edge in the spanning tree of every vertex. The usual presentation uses the already cited stack and a serial number for each vertex. In this paper, we adopt a functional programming style and associate to every vertex its rank in the stack of visited vertices.

Our Why3-ML program is based on two mutually recursive functions dfs1 and dfs' which respectively take as arguments a vertex x and a set of vertices roots and which return the rank m of the oldest vertex accessible by at most one back-edge. Both functions work with a state with three components: the set of black vertices, the working stack and the set of already computed strongly connected components. A set of gray vertices is an extra ghost argument used in the correctness proof, but irrelevant for the algorithm [START_REF] Filliâtre | The spirit of ghost code[END_REF]. Thus the state is given by three extra parameters and is returned as the last three components of the quadruple resulting from both functions. Each vertex is white (not visited), gray (under visit), or black (visited). White vertices are defined as non black nor gray. Graphs are represented by a finite set vertices of vertices and a function successors which associates to each vertex the finite set of vertices directly accessed from it by an edge. The working stack is a list of vertices whose head is the top of the stack. The program also uses functions of the Why3 library on sets (add adds an element to a set, mem tests membership to a set, choose picks randomly an element in a set, remove removes an element from a set, and is_empty, union, inter, diff, subset, cardinal all with an intuitive meaning on finite sets) and on lists (Nil, Cons. lmem tests membership to a list, length gives the length of a list, elements returns the set of elements in a list, num_occ gives their number of occurrences). We have two auxiliary functions: rank which provides the order of an element in a reversed list, split which returns the pair of sublists produced by decomposing a list with respect to the first occurrence of an element. Finally max_int() returns +∞ (here the cardinal of the set of all vertices) and min gives the minimum of two integers.

The main program calls dfs' with the set vertices of all vertices, with empty sets of blacks and grays vertices and an empty set sccs of strongly connected components. Then dfs' picks randomly a vertex in roots. If that vertex x is white, the function dfs1 is called on it. Then x is pushed into the stack and dfs' is called on the direct successors of x after turning it to gray. If the returned value is greater than (in fact equal to) the rank of x in the stack, an additional strongly connected component is added to the result by popping from the stack all elements until x. If the returned value is smaller than the rank of x, we return that value after turning x to black. In dfs', for a non-white vertex, we return the minimum of its rank in the stack and the results from other vertices in the set of roots. If the non-white vertex is already in the set of presently discovered strongly connected components, we return +∞ (namely max_int()).

3 Pre-/Post-conditions Our graphs are represented by an abstract type vertex, a global constant vertices, and a successors function which gives for any vertex the set of its successors. An axiom specifies that successors of a vertex in vertices stay in vertices. The predicate edge states that two vertices are joinable by an edge. The intuitive proof notices that vertices are stored in the stack in the preorder of the spanning trees. So for each vertex, the dfs1 function minimizes the rank of vertices accessible from its descendants in the spanning tree by at most one back-edge. When that rank is equal to the rank of its argument, the function dfs1 has met the first vertex of a new strongly connected component the elements of which were pushed in the stack after x. But that proof needs to be formalized. In our paper, we do not introduce spanning trees. We only The formal proof relies on two invariants and four post-conditions. The latter ones express the properties of the returned value m in terms of reachability with at most a single back-edge. The former ones are more subtle. They state the relations between colors of the vertices in the working stack and the color of the already computed strongly connected components. Furthermore these invariants show the known reachability between vertices in this stack as illustrated in figure 1. In the Why3-ML language, the first invariant states that the predicate wff_color holds. That means that blacks and grays are disjoint sets of vertices, and that the elements of stack are formed by the union of gray vertices and the blacks which are not in the set sccs of strongly connected components (set_of flattens a set of sets by making the union of all its elements). Furthermore the predicate no_black_to_white says that there is no edge from a black vertex to a white one (i.e. a black vertex can only point to a black or gray vertex). In terms of spanning trees, an equivalent statement is that no node can point directly to a right cousin. The rest of the invariant wff_stack states that gray vertices can reach every vertex with higher rank in the stack and conversely that any vertex in stack can reach a gray vertex with smaller rank. Reachability is defined in terms of paths in the graph by an inductive predicate as in the Why3 library. An additional information simplelist expresses that the stack does not contain repetitions. So the length of the stack is always less or equal to the number of vertices max_int(). A second invariant characterizes the value of the sccs component in the current state, namely sccs is the set of black strongly connected components. Strongly connected components are naturally defined as maximal sets of vertices connected in both ways by paths.

predicate in_same_scc (x y: vertex) = reachable x y ∧ reachable y x predicate is_subscc (s: set vertex) = ∀x y. mem x s → mem y s → in_same_scc x y predicate is_scc (s: set vertex) = is_subscc s ∧ (∀s'. subset s s' → is_subscc s' → s == s')

The function dfs1 has three pre-conditions expressing that the x parameter is a white vertex in vertices which can be reached from any gray vertex. That function has four post-conditions. The last one says that x is turned to black at end of function. The other three provide properties on the integer m returned by dfs1. Firstly it is less than the rank of x. Secondly it is the rank of a vertex reachable from x. Thirdly if there is an edge from a vertex in the new part of the stack to a vertex y in the old part of the stack, then the returned value m must be less or equal to the rank of that y. These three post-conditions state that the returned value is either the rank of x or of some y in the stack at the beginning of dfs1. We have finally three monotonic post-conditions on the state at end of dfs1. The final stack is a black extension of the initial one, the sets of blacks and strongly connected components are enlarged. The function dfs' has the same invariants and pre-/post-conditions, upto the set extension to capture the set of roots instead of a single vertex. In fact dfs1 could have been inlined in dfs', but we feel it is more readable to separate the two functions. Several features about the Why3 syntax: "requires" and "ensures" are keywords for pre-and post-conditions; "assert" is for assertions in function bodies; "result" is the returned value of a function; "returns" is an abbreviation for "ensures" with pattern matching when the result is a t-uple.

The formal proof

There are a few assertions in the text of dfs1. Most of them are after the split of the stack with respect to the parameter x, which is the critical part of the program since we have to show that we then get a new strongly connected component in the stack on top of x. The first two ones are easily proved. First, the old part of the stack s3 is same as the initial stack, since there are no repetitions in the working stack. The second assertion states that the new part of the stack s2 (which starts with x ) is all black in the final state of black vertices. The next two are more subtle.

In the third assertion, we prove that the elements of s2 are a subset of a strongly connected component. Indeed take two vertices y and z in s2. Both of them are strongly connected with x since as x is gray in dfs', we know that x reaches y and z and these two can reach back gray vertices by one invariant at end of dfs'. These gray vertices are with ranks smaller than (or equal to) the rank of x. Therefore they loop back to x.

In the fourth assertion, we prove maximality of s2 as a sub-strongly connected component. So let us consider a vertex y in same strongly connected component as x. We have to show that y belongs to s2. This is a manual proof in Coq that we could not fully automatize. First two automatically proved lemmas implies that if y is not in s2, there is an edge from x' to y' both in same strongly component as x such that x' is in s2 and y' is not in s2. Furthermore there are three cases. Case 1: y' in stack. Then either x' is x, but we know that the result of dfs' is smaller than the rank of any successors of x, therefore less than the rank of y' which is then strictly less than the rank of x. Impossible! Either x' is in the rest of s2, and then there is a cross-edge to y', contradicting by post-condition of dfs' that its result is larger than the rank of x. Case 2: y' in sccs. Then x which is in same strongly connected components as y' would have to be inside one set of sccs. But the working stack is disjoint from the union of the elements of sccs by invariant wff_color. Case 3: y' is white. Impossible since x' in s1 is black and there is no edge from black to white.

The other assertions are proved by automatic provers (Alt-Ergo, E-prover, CVC4, Z3, Spass). The fifth assertion states that s2 is a strongly connected component. The sixth assertion is a property of boolean algebra on subset ordering that our provers cannot discover. This assertion is used to prove the invariant about colors.

In the other alternative of the conditional statement, there is a single assertion. At that point as mentioned above, we know that the corresponding elements of s2 in s1 form a subset of a strongly connected component. But the assertion says that this subset is strict since there is a gray element in it, outside of s2. In fact, we could have called the split function before the test on ranks and made that argument more explicit. But the program would have been further from the textbooks presentation.

The proof obligations in dfs' are simpler. No assertion is necessary in the body of the function. Only two proofs are to be done in Coq. These are proofs (in two different cases) of the same post-condtion, i.e. m is less than the rank of the ranks of all vertices in roots. There are then many cases because of the min function and the possible +∞ result.

Besides the two functions dfs1 and dfs', we use lemmas: 5 lemmas about the rank function, 6 lemmas about lists, 17 lemmas about sets(!), 8 lemmas about strongly connected components, 7 lemmas very special to our program.

Detailed proofs can be found at http:jeanjacqueslevy.net/why3/. As an appendix, we give the exact definitions of four predicates used in our program assertions, although their names are very explicit. Notice that ++ is the infix operator to append two lists. We do not consider the main program which calls dfs' with vertices all white. It remains to show that the black strongly connected components found by our algorithm are the ones accessible from roots. It is the standard proof of depthfirst-search that we already proved by itself. Notice too that when the set vertices of all vertices is empty, the empty set is then a strongly connected component, which invalidates our requirement about sccs. So it means that the main program has to check if the set vertices is empty and then returns directly the correct value instead of calling dfs'.

Towards imperative programs

It remains to show the proof of the imperative version of this algorithm as exposed in algorithms textbooks. We have to suppress membership tests for stack, the calculations about ranks and the operations on sets. The usual technique is to associate serial numbers to vertices in the preorder of the spanning trees, and by giving two exceptional values: -1 for non-visited vertices, +∞ for vertices already in the sets of discovered strongly connected components. Therefore each vertex x has a value num[x], initially set to -1.

We then can refine our program and aim a functional version of the true imperative programs. The state is augmented with the function num and an integer sn providing the next available serial number for the next visited vertex. We return two results m and n respectively the rank and the serial number of the oldest vertex visited with at most one back-edge by the descendants of x. The program flow is identical to the one of the previous functional version since the following invariant relates the ordering on ranks and the ordering on serial numbers.

predicate wff_num (sn: int) (num: map vertex int) (s:

list vertex) = (∀x. num[x] < sn ≤ max_int()) ∧ (∀x y. lmem x s → lmem y s → num[x] ≤ num[y] ↔ rank x s ≤ rank y s)
In fact it is convenient to refine the functional program in two steps to the imperative version. First to introduce serial numbers and the num function as we just presented. The second one to modify the split function and modify then the function num as an extra result of split and setting the serial number of popped elements to +∞. We can then test efficiently if a visited vertex is not in the working stack.

Another algorithm

Kosaraju's algorithm is a different way of discovering strongly connected components in a directed graph. It works with two passes. A first traversal of the graph stores in a stack all vertices in the post-order of their visits. This means that the successors of a vertex are pushed into the stack before that vertex. A second phase iterates on the stack by popping it until a non-visited vertex and performs a depth-first search starting from that vertex on the mirror image of the graph. Then all the vertices encountered by that search form a new strongly connected component. This algorithm may look magic, but its principle is quite simple. It works on the dag of the strongly connected components, and it makes a topological sort on that dag. However it needs to be formalized, and we want here to make a simple publishable proof.

We therefore consider two graphs G1 and G2, each graph is the mirror image of the other one. So the two graphs have the same set of vertices and opposite edges. (We use the module notation of Why3) axiom reverse_graph: G1.vertices == G2.vertices ∧ (∀x y. G1.edge x y ↔ G2.edge y x)

The function dfs1 performs depth-first search in graph G1, the function dfs2 performs depth-first search in graph G2. Notice that we inlined the recursive calls to the direct successors of a vertex unlike in section 2. The result of dfs1 is a pair the first component of which is the set b of visited vertices. The function works with a state, namely a stack represented by the list stack as argument and returned as s in the second component of the result. We call dfs1 on the let rec dfs1 roots blacks grays stack = if is_empty roots then (blacks, stack) else let x = choose roots in let roots' = remove x roots in let (b1, s1) = if mem x (union blacks grays) then (blacks, stack) else let (b2, s2) = dfs1 (G1.successors x) blacks (add x grays) stack in (add x b2, Cons x s2) in dfs1 roots' b1 grays s1 let rec dfs2 roots blacks grays = if is_empty roots then blacks else let x = choose roots in let roots' = remove x roots in let b1 = if mem x (union blacks grays) then blacks else add x (dfs2 (G2.successors x) blacks (add x grays)) in dfs2 roots' b1 grays Notice that the vertex x is pushed into the stack at the end of dfs1, namely after the visited vertices from the successors of x (see figure 2). We now decorate these two functions with the corresponding pre-/post-condtions and the assertions.

let rec dfs1 roots blacks grays stack = requires{subset roots G1.vertices} requires{wff_stack_G1 blacks grays stack} returns{(b, s) → wff_stack_G1 b grays s} returns{(b, _) → subset roots (union b grays)} returns{(_, s) → ∃s'. s = s' ++ stack ∧ G1.access_from_set roots (elements s')} returns{(b, _) → subset blacks b} if is_empty roots then (blacks, stack) else let x = choose roots in let roots' = remove x roots in let (b1, s1) = if mem x (union blacks grays) then (blacks, stack) else let (b2, s2) = dfs1 (G1.successors x) blacks (add x grays) stack in assert{not lmem x s2}; (* help provers *) assert{∃s'. Cons x s2 = s' ++ stack ∧ G1.access_from x (elements s')}; assert{no_edge_out_of stack (Cons x s2)}; assert{no_path_out_of_in stack (Cons x s2)};

(add x b2, Cons x s2) in dfs1 roots' b1 grays s1

The pre-/post-conditions of that function give the properties of the working stack. This is crucial for the correctness of the overall algorithm. We first require that the set of vertices in the argument roots is contained in the set of all vertices of graph G1 (which are the same as the ones of graph G2 ). The last (monotonic) post-condition states that the set b of visited vertices contains the initial set blacks of already visited vertices given as argument of dfs1. Another (monotonic) post-condition states that the resulting stack s is an extension of the initial stack stack and moreover the extension contains vertices accessible from some vertices in roots. The second post-condition states that this set roots argument of dfs1 is either gray or black at the end of the function. These pre-/post-conditions are just standard properties of any depth-first search on graphs.

predicate wff_color (blacks grays: set vertex) = inter blacks grays = empty ∧ no_black_to_white blacks grays predicate wff_stack_G1 (blacks grays: set vertex) (s: list vertex) = G1.wff_color blacks grays ∧ simplelist s ∧ elements s == blacks ∧ subset (elements s) G1.vertices ∧ reachable_before_same_scc s

The important property of dfs1 is that the invariant wff_stack_G1 holds. It states that a property on colors is respected as seen in section 3. Black and gray sets are disjoint and there is no edge in G1 from a black vertex to a white vertex. Moreover the elements of the working stack are vertices in G1. These are again standard properties of depth-first search. But there is an important additional property about reachability within the working stack. Let say that a path starting at a vertex x can reach a vertex y before it within a stack s if each vertex z in that path has a rank in the stack s less or equal to the rank of the final destination y. (The rank function is defined as in section 3). Then the order in which vertices are stored in the working stack implies that any "path before" has to stay within the same strongly connected component.

predicate reachable_before (x y: vertex) (s: list vertex) = ∃l. G1.path x l y ∧ (∀z. lmem z l → lmem z s ∧ rank z s ≤ rank y s) predicate reachable_before_same_scc (s: list vertex) = ∀x y. lmem x s → lmem y s → reachable_before x y s → in_same_scc x y

That reachable_before_same_scc property is a fundamental property of spanning trees with respect to their post-order traversal. The proof of that invariant on the working stack relies on four assertions in the body of dfs1. The first one is just a hint for automatic provers to show the absence of repetitions in the stack. The third assertion states that there could not be an edge from a vertex in stack to another one in s2 not in stack. This is due to the post-order traversal, i.e. no black to white edge in our terminology (see figure 2 where s2 is s1 without x ). So there cannot be a path from a vertex in the old part stack of the working stack to a vertex in its new part s' with all its intermediate vertices inside s1. This is expressed by our fourth assertion.

Then we can show that reachable_before_same_scc holds in s1. Indeed any "path before" was either already existing in s2 and post-condition of dfs1 called on successors of x was validating the predicate. Either it is a new path in s1, which means involving x. This "path before" needs have x as its last vertex. The fourth assertion implies that that path is totally inside the new part s' of s1. We know by the second assertion that the elements of s' are accessible from x. Therefore all elements of the path are in the same strongly connected components.

let rec dfs2 roots blacks grays = requires{subset roots G2.vertices} requires{G2.wff_color blacks grays} ensures{G2.wff_color result grays} ensures{subset roots (union result grays)} ensures{G2.access_from_set roots (diff result blacks)} ensures{subset blacks result} if is_empty roots then blacks else let x = choose roots in let roots' = remove x roots in let b1 = if mem x (union blacks grays) then blacks else add x (dfs2 (G2.successors x) blacks (add x grays)) in dfs2 roots' b1 grays

The function dfs2 just performs a depth-first search from the vertices in the roots argument and returns the set result of vertices visited by its recursive calls. A post-condition says that the newly visited vertices are accessible from roots. Moreover the following invariant G2.wff_color is verified in a similar way it was holding in function dfs1 for graph G1. The last function iter2 iterates on the stack computed by dfs1. It pops the stack until its first non black vertex x. Then it makes the singleton set containing x and calls dfs2 with that singleton as roots of the depth-first search. We call cc1 the set of newly visited vertices. Then this set is a new strongly connected component which is stored in the argument sccs which accumulates the set of already discovered strongly connected components. This function iter2 has a few pre-/post-conditions. In fact, the function just requires that the set of white (i.e. non black) vertices are in the argument stack. And it has two invariants, one on the set sccs of strongly connected components (as in section 3). A second invariant wff_stack_G2 is about the structure of the stack. It is similar to the one for dfs1. The only differences are that the stack is not fully black and that the non-black-to-white predicate refers now to G2. Notice that at the end of iter2 the stack is empty and is thus Nil. In the body of the iter2 function, we have five assertions with an overall structure similar to the ones of the split case in section 3. The first one says that the set cc1 of visited vertices by dfs2 is contained in the vertices contained in stack. Indeed by post-condition of dfs2, the set cc1 is accessible from the singleton containing x. As x is in stack, it is in vertices by predicate wff_stack_G2. Thus cc1 is a non black subset of vertices, therefore contained in stack by the first pre-condition. The second assertion relies on a lemma which says that any path between any vertices y and z in cc1 can only go through vertices in cc1. This is due to the closing property of reachability induced by depth-first search. Indeed if the path goes through one vertex in sccs, it cannot come back to a vertex in cc1 and similarly if the path cannot go through a white vertex at end of dfs2 since all the reachable vertices from vertices in cc1 have been blackened. In our terminology, this is due to the non-black-to-white predicate before the call to dfs1 and after that call. Now if we take any vertex y in cc1, we know that y is reachable from x by the post condition of dfs2. Therefore there is a path from x to y both in cc1. By the previous lemma, all its intermediate vertices are also in cc1, therefore in stack. This a path of graph G2, therefore a path from y to x in graph G1. But all elements of stack have a rank smaller than the rank of x. So there is a "path before" from y to x, which is the statement of the second assertion.

The third assertion in the body of iter2 is a direct consequence of the invariant wff_stack_G2 which is true at the beginning of iter2. As there is a "path before" from any vertex y in cc1, we know by the invariant that y is in same strongly connected component as x. Therefore cc1 is a subset of a strongly connected component containing x.

The fourth assertion states the maximality of cc1 as a subset of a strongly connected component. We may use the same lemma as for the second assertion. Let y be in same strongly connected component as x. There are paths from x to y and conversely. So there is a path from x to itself. Since x is inside cc1, all the intermediate vertices on that path are in cc1. Therefore y is in cc1.

The post-conditions of iter2 are shown as in section 3. We did not consider the main program. It is a call to dfs1 with as arguments the set G1.vertices of all vertices, empty sets of black and gray vertices and an empty stack Nil. The resulting path is then passed as argument of iter2 with empty sets of black vertices and empty set of strongly connected components. The result is the set of strongly connected components of all graph G1 (which are the same as the ones of G2 ). Notice that unlike Tarjan's algorithm, we could not start with a distinguished set roots of vertices since reachability in G2 is very distinct from reachability in G1.

An appendix of our proof is the following exact definitions of predicates used in our assertions, although their names were very meaningful. Besides the assertions and pre-/post-conditions for functions dfs1, dfs2 and iter2, we use lemmas: 1 lemma about the rank function, 1 lemma about lists, 10 lemmas about sets, 6 lemmas about strongly connected components, 7 new lemmas on paths (reversed graph, path before, path out), 2 lemmas on crossed sets, 3 lemmas very special to our program. In Coq we proved 4 lemmas (3 lemmas about reversed paths and lemma about transitivity of paths), 1 assertion and 1 post-condition (in fact the same assertion about stack extension as in dfs1 for Tarjan's algorithm).

An imperative version of that algorithm is not difficult to envision although it is slightly technical. Clearly the function dfs1 can be turned into an imperative program by getting mutable maps to describe the colors of any vertex, and the resulting stack can also be constructed in an imperative way. For the second pass, the imperative version is a bit more subtle. We have to give as arguments of dfs2 an existing set sccs of strongly connected components (a set of sets that we may implement as a list of lists) and a connected component cc under construction which would be represented by a list of vertices that we modify when visiting a new vertex in dfs2. Then iter2 stores that list cc into sccs at end of the call of dfs2. Then iter2 goes on calling dfs2. We do not present here the assertions and invariants needed by this imperative version, but it is an interesting development to mimic the textbook algorithm.

Conclusion

We presented formal correctness proofs of two algorithms in graphs for calculating strongly connected components. These proofs are checked by computer. Most of them are automatically proved. To achieve this, we had to simplify the details of the proofs, which made them publishable in a single article. We think that the details of our proofs are explainable to students who learn algorithms and formal methods. This is because of the simplicity of our logic (first-order logic and inductive types), but this is also due to the need for automatization, which demands simplification. We however have small bits of these proofs written in Coq and have to check them interactively. Most of the Coq proofs were short, except one in Tarjan's algorithm. We also took benefits of the functional programming style when presenting these two algorithms. We tried direct proofs of imperative versions and had to face more complexity together with lack of readability. It would be interesting to compare our proofs to other formal proofs for these algorithms. Several are existing; they could use spanning trees and therefore be further than our proofs from the real programs and real data structures, but programs might be extracted from these proofs. We also avoided the complexity of separation logic by presenting our functional programs, notwithstanding they are not far from the imperative versions.

Altogether, our approach is quite successful. The proofs are not long, not much sophisticated. We know that there are several flaws with this approach: lack of abstraction, erratic behaviour of automatic provers, uneasy incremental development, no proofs certificates. But we do think that we gained in readability, which is a very important criterion in formal proofs of programs.

  type vertex constant vertices: set vertex function successors vertex : set vertex axiom successors_vertices:∀x. mem x vertices → subset (successors x) vertices predicate edge (x y: vertex) = mem x vertices ∧ mem y (successors x)

Fig. 1 .

 1 Fig. 1. Invariants on colors and stack

  predicate no_black_to_white (blacks grays: set vertex) = ∀x x'. edge x x' → mem x blacks → mem x' (union blacks grays) predicate wff_color (blacks grays: set vertex) (s: list vertex) (sccs: set (set vertex)) = inter blacks grays = empty ∧ (elements s) == union grays (diff blacks (set_of sccs)) ∧ (subset (set_of sccs) blacks) ∧ no_black_to_white blacks grays

  inductive path vertex (list vertex) vertex = | Path_empty: ∀x: vertex. path x Nil x | Path_cons: ∀x y z: vertex, l: list vertex. edge x y → path y l z → path x (Cons x l) z predicate reachable (x z: vertex) = ∃l. path x l z predicate wff_stack (blacks grays: set vertex) (s: list vertex) (sccs: set (set vertex)) = wff_color blacks grays s sccs ∧ simplelist s ∧ subset (elements s) vertices ∧ (∀x y. mem x grays → lmem y s → rank x s ≤ rank y s → reachable x y) ∧ (∀y. lmem y s → ∃x. mem x grays ∧ rank x s ≤ rank y s ∧ reachable y x)

  let rec dfs1 x blacks (ghost grays) stack sccs = requires{mem x vertices} requires{access_to grays x} requires{not mem x (union blacks grays)} (* invariants *) requires{wff_stack blacks grays stack sccs} requires{∀cc. mem cc sccs ↔ subset cc blacks ∧ is_scc cc} returns{(_, b, s, sccs_n) → wff_stack b grays s sccs_n} returns{(_, b, _, sccs_n) → ∀cc. mem cc sccs_n ↔ subset cc b ∧ is_scc cc} (* post conditions *) returns{(m, _, s, _) → m ≤ rank x s} returns{(m, _, s, _) → m = max_int() ∨ rank_of_reachable m x s} returns{(m, _, s, _) → ∀y. crossedgeto s y stack → m ≤ rank y stack} returns{(_, b, _, _) → mem x b} (* monotony *) returns{(_, b, s, _) → ∃s'. s = s' ++ stack ∧ subset (elements s') b} returns{(_, b, _, _) → subset blacks b} returns{(_, _, _, sccs_n) → subset sccs sccs_n} let m = rank x (Cons x stack) in let (m1, b1, s1, sccs1) = dfs' (successors x) blacks (add x grays) (Cons x stack) sccs in assert{inter grays (add x b1) = empty}; (* help provers *) if m1 ≥ m then begin let (s2, s3) = split x s1 in assert{s3 = stack}; assert{subset (elements s2) (add x b1)}; assert{is_subscc (elements s2) ∧ mem x (elements s2)}; assert{∀y. in_same_scc y x → mem y (elements s2)}; assert{is_scc (elements s2)}; assert{inter grays (elements s2) = empty}; (* help provers *) (max_int(), add x b1, s3, add (elements s2) sccs1) end else begin assert{∃y. mem y grays ∧ rank y s1 < rank x s1 ∧ reachable x y}; (m1, add x b1, s1, sccs1) end

  with dfs' roots blacks (ghost grays) stack sccs = requires{subset roots vertices} requires{∀x. mem x roots → access_to grays x} (* invariants *) requires{wff_stack blacks grays stack sccs} requires{∀cc. mem cc sccs ↔ subset cc blacks ∧ is_scc cc} returns{(_, b, s, sccs_n) → wff_stack b grays s sccs_n} returns{(_, b, _, sccs_n) → ∀cc. mem cc sccs_n ↔ subset cc b ∧ is_scc cc} (* post conditions *) returns{(m, _, s, _) → ∀x. mem x roots → m ≤ rank x s} returns{(m, _, s, _) → m = max_int() ∨ ∃x. mem x roots ∧ rank_of_reachable m x s} returns{(m, _, s, _) → ∀y. crossedgeto s y stack → m ≤ rank y stack} returns{(_, b, _, _) → subset roots (union b grays)} (* monotony *) returns{(_, b, s, _) → ∃s'. s = s' ++ stack ∧ subset (elements s') b} returns{(_, b, _, _) → subset blacks b} returns{(_, _, _, sccs_n) → subset sccs sccs_n} if is_empty roots then (max_int(), blacks, stack, sccs) else let x = choose roots in let roots' = remove x roots in let (m1, b1, s1, sccs1) = if lmem x stack then (rank x stack, blacks, stack, sccs) else if mem x blacks then (max_int(), blacks, stack, sccs) else dfs1 x blacks grays stack sccs in let (m2, b2, s2, sccs2) = dfs' roots' b1 grays s1 sccs1 in (min m1 m2, b2, s2, sccs2) let rec split (x : α) (s: list α) : (list α, list α) = returns{(s1, s2) → s1 ++ s2 = s} returns{(s1, _) → lmem x s → is_last_of x s1} match s with | Nil → (Nil, Nil) | Cons y s' → if x = y then (Cons x Nil, s') else let (s1', s2) = split x s' in ((Cons y s1'), s2) end

  predicate rank_of_reachable (m: int) (x: vertex) (s: list vertex) = ∃y. lmem y s ∧ m = rank y s ∧ reachable x y predicate access_to (s: set vertex) (y: vertex) = ∀x. mem x s → reachable x y predicate crossedgeto (s1: list vertex) (y: vertex) (s3: list vertex) = lmem y s3 ∧ ∃s2. (s1 = s2 ++ s3 ∧ ∃x. lmem x s2 ∧ edge x y) predicate simplelist (s: list α) = ∀x. num_occ x s ≤ 1 predicate is_last_of (x: α) (s: list α) = ∃s'. s = s' ++ Cons x Nil

  let rec dfs1 x blacks (ghost grays) stack sccs sn num = requires{sn = cardinal (union grays blacks) ∧ subset (union grays blacks) vertices} (* invariants *) requires{wff_num sn num stack} returns{(_, _, _, s, _, sn_n, num_n) → wff_num sn_n num_n s} (* post conditions *) returns{(sn_n, m, _, s, _, _, num_n) → sn_n = m = max_int() ∨ ∃y. lmem y s ∧ sn_n = num_n[y] ∧ m = rank y s} let m = rank x (Cons x stack) in let (n1, m1, b1, s1, sccs1, sn1, num1) = dfs' (successors x) blacks (add x grays) (Cons x stack) sccs (sn + 1) num[x ← sn] in if n1 ≥ sn then begin let (s2, s3) = split x s1 in (max_int(), max_int(), add x b1, s3, add (elements s2) sccs1, sn1, num1) end else (n1, m1, add x b1, s1, sccs1, sn1, num1)

Fig. 2 .

 2 Fig. 2. Invariants on colors and stack in function dfs1

  predicate wff_stack_G2 (blacks grays: set vertex) (s: list vertex) = G2.wff_color blacks grays ∧ simplelist s ∧ subset (elements s) G2.vertices ∧ reachable_before_same_scc s

  let rec iter2 stack blacks sccs = requires{subset (diff G1.vertices blacks) (elements stack)} requires{wff_stack_G2 blacks empty stack} requires{∀cc. mem cc sccs ↔ is_scc cc ∧ subset cc blacks} returns{(b, _) → wff_stack_G2 b empty Nil} returns{(b, sccs_n) → ∀cc. mem cc sccs_n ↔ is_scc cc ∧ subset cc b} match stack with | Nil → (blacks, sccs) | Cons x s → if mem x blacks then iter2 s blacks sccs else let b1 = dfs2 (add x empty) blacks empty in let cc1 = diff b1 blacks in assert{subset cc1 (elements stack)}; assert{∀y. mem y cc1 → reachable_before y x stack}; assert{is_subscc cc1 ∧ mem x cc1}; assert{∀y. in_same_scc y x → mem y cc1}; assert{is_scc cc1}; iter2 s b1 (add cc1 sccs) end

  predicate access_from (x: vertex) (s: set vertex) = ∀y. mem y s → reachable x y predicate access_from_set (roots b: set vertex) = ∀y. mem y b → ∃x. mem x roots ∧ reachable x y predicate no_edge_out_of (s3 s1: list vertex) = ∀s2. s1 = s2 ++ s3 → ∀x y. lmem x s3 → lmem y s2 → not G1.edge x y predicate path_in (l: list vertex) (s: list vertex) = ∀x. lmem x l → lmem x s predicate no_path_out_of_in (s3 s1: list vertex) = ∀x y l s2. s1 = s2 ++ s3 → lmem x s3 → lmem y s2 → G1.path x l y → path_in l s1 → false

Acknowledgments

We thanks the Why3 group at Inria-Saclay/LRI-Orsay for valuable advices.


Pierre Thuéry
email: pierre.thuery@cea.fr

Jack Harrowfield
email: harrowfield@unistra.fr

Complexation of Uranyl Ion with Sulfonates: One-to Three-Dimensional Assemblies with 1,5-and 2,7-Naphthalenedisulfonates

Keywords: Uranium(VI), Sulfonic acids, Cucurbiturils, Structure elucidation, Metal-organic frameworks

Complexation of Uranyl Ion with Sulfonates: One-to

Three-Dimensional Assemblies with 1,5-and 2,7-Naphthalenedisulfonates

Pierre Thuéry, Jack Harrowfield

Introduction

Although considered as a relatively weak O-donor entity, one reason the sulfonate group has been widely investigated is precisely because this characteristic renders it of potential interest for the construction of flexible coordination networks. [1][2][3][4] Aromatic sulfonates, which occupy an intermediate range of the donor strength of known systems, [5] have been a particular focus in the form of divergently-substituted polysulfonates which can give rise to "pillared" layer structures in their metal ion complexes [1][2][3][4] analogous to those seen in hydrogen bonded systems such as guanidinium organosulfonates. [6] As a donor group, RSO3 -is most commonly found in unidentate or O,Oʹ-bridging modes, with O,Oʹ-chelation (and, rarely, tripodal-bridging coordination) only being found, as might be expected, with larger metal ions. [1][2][3][4] Although aromatic sulfonates do not appear to be particularly good ligands for the lighter lanthanide(III) ions, [7] it is significant that in mixed Ln/uranyl ion (Ln = Ce, Eu) complexes of p-sulfonatocalix [4]arene, [8] the uranyl ions do form in part O,Oʹ-chelate rings with sulfonate while the Ln(III) ions show only unidentate coordination, indicating potential utility of sulfonates in actinide/lanthanide separation. While larger sulfonated calixarenes are considered to be "uranophiles", [9][10][11] there is no structural information on the complexes involved or certainty as to how or even if the sulfonate groups coordinate to U VI . The aliphatic ethane-1,2-disulfonate gives crystalline uranyl ion complexes in which it is either doubly unidentate [12,13] or O,Oʹ-bridging bidentate, [14] the latter coordination mode being seemingly preferred for methane-and ethanesulfonates, [15][16][17][18] although tripodal O,Oʹ,Oʹʹcoordination is also known in the former case. [18] In contrast, the common trifluoromethanesulfonate anion is unidentate in all its uranyl complexes reported in the Cambridge Structural Database (CSD, Version 5.37). [19] The aromatic monosulfonates, 4-methylbenzene (toluene) sulfonate and 2,4,6-trimethyl (mesityl) sulfonate, behave as unidentate donors to uranyl ion, [16,20] but it was recently found that the former could also act as an O,Oʹ-bridging ligand. [21] Various aromatic monosulfonates with additional carboxylate or hydroxyl coordinating groups also display unidentate sulfonate coordination (as part of a chelate ring), although O,Oʹ-bridging is also observed in some cases. [13,14,[22][23][24][25][26] Bridging of uranyl centers by disulfonate or mixed hydroxyl-or carboxylate-sulfonate ligands is propitious for the formation of uranyl-organic coordination polymers or frameworks (UOFs), [27][28][29] a domain in which they are much less investigated than phosphonates. [26] Among the examples of such compounds previously reported, several include cucurbit [6]uril (CB6) as coligands or templating species, [12,14,22] thus giving architectures that are often quite intricate, as well as, in some cases, enabling isolation of uranyl complexes with sulfonate ligands that resist crystallization in the absence of CB6. [14,22] This interest of sulfonates for the building of UOFs, coupled with the somewhat uncertain overall view of sulfonate binding to uranyl ion led to our present efforts to characterise the situation in crystalline uranyl ion complexes of aromatic disulfonates, namely 1,5-and 2,7-naphthalenedisulfonates (1,5-and 2,7nds 2-), capable of bridging, but not chelation through both sulfonate groups. In extension of recent work, of particular interest was how uranyl-sulfonate coordination might be influenced by the presence of other metal ions, so that our initial experiments were directed towards the possible synthesis of mixed-metal species, although success was limited in this regard. The crystal structures of six complexes obtained in the course of this work, one of them including CB6 molecules, with dimensionalities ranging from one to three, are reported herein, as well as, in most cases, their emission spectrum in the solid state at room temperature.

Results and Discussion

Crystal Structures

The complex [UO2(1,5-nds)(H2O)] (1) crystallizes in the orthorhombic space group Pbcn, with the uranium atom located on a two-fold rotation axis (Wyckoff position 4c) and the disulfonate ligand being centrosymmetric (Figure 1). The uranyl group is bound to four sulfonate oxygen atoms pertaining to four different anions [U-O bond lengths 2.403(2) and 2.428(2) Å; the average value for structures reported in the CSD is 2.40(4) Å] and to one water molecule located on the two-fold rotation axis [U1-O5 2.375(4) Å]. The uranium atom environment is thus pentagonal bipyramidal.

: i = 1 -x, y, 1/2 -z; j = 3/2 -x, y -1/2, z; k = x -1/2, y -1/2, 1/2 -z; l = x + 1/2, y + 1/2, 1/2 -z; m = 2 -x, 1 -y, 1 -z; n = 3/2 -x, 1/2 -y, z + 1/2.
The disulfonate ligand is doubly O,Oʹ-bridging (bis(2- 1 : 1 ) coordination mode) and thus bound to four metal cations. The assembly formed is three-dimensional (3D), with the point (Schläfli) symbol {6 5 .10}{6 5 .8} (symbols for ligand and uranium four-fold nodes, respectively), and views of the lattice and its nodal representation are shown in Figure 1. The framework has a layered appearance and the naphthalene units can be considered as "pillars" linking two-dimensional (2D) polymeric sheets parallel to (0 0 1), in which connection of UO2(O2SO)4(H2O) units generates an array of fused 16-membered rings; this 2D array has the topology of a square grid with four-fold uranium nodes and the sulfonate groups being simple links (Figure 1). The uranyl oxo atom O1 is at 3.09 Å from one naphthalene carbon atom, and at 2.80 Å from the corresponding hydrogen atom, a weak interaction which is apparent in the Hirshfeld surface [30] obtained using CrystalExplorer. [START_REF] Wolff | CrystalExplorer[END_REF] The coordinated water molecule is hydrogen bonded to the uncoordinated sulfonate atom O4 [O5O4 ii 2.669(3) Å, HO4 ii 1.74 Å, O5-HO4 ii 164°; symmetry code ii = x -1/2, y + 1/2, 1/2

z] and its image by the rotation axis, which is also apparent from the Hirshfeld surface, as well as a further interaction of O4 with one naphthalene hydrogen atom (2.51 Å). Within the organic layer, the shortest contacts between centroids of aromatic rings are at 4.4 Å (the corresponding dihedral angle being 23°), and analysis of the Hirshfeld surfaces confirms that there is no evidence of significant -stacking of the aromatic planes. The Kitaigorodski packing index (KPI, estimated with PLATON [START_REF] Spek | [END_REF] ) of 0.76 is indicative of a compact packing with no significant free space left. The U-O(sulfonate) bond lengths are in the range 2.385(4)-2.424(2) Å [average 2.409( 15) Å] and they are thus close to those in complex 1. As always in uranyl complexes including chelating bipy or phen molecules, or their derivatives, the equatorial environment is far from planar, the two nitrogen donors being displaced out of the plane defined by the other donors, the latter plane being approximately perpendicular to the uranyl axis, thus inducing chirality at the uranium centre. [33] In the present cases, the out-of-plane displacements of nitrogen atoms are in the range 0.119(9)-0.592(5) Å, being most reduced in the phen-containing complex 4, and the dihedral angles between the bipy or phen average plane and the mean plane defined by uranium and the three oxygen donors are 19.40(9)/15.69 (12), 23.78 (7) and 19.08(17)° in 2-4, respectively. The latter values are smaller than those observed in more crowded eight-coordinate complexes, in which dihedral angles of more than 40° have been measured, but it is notable that, both in seven-and eight-coordinate complexes, the tilting of phen is generally smaller than that of bipy. [33] In all three compounds, hydroxide bridging gives rise to uranyl dimers (centrosymmetric in 3 and 4) and further bridging by in the formation of weak CHO hydrogen bonds, [34,35] with HO distances as short as 2. are considered as single, six-fold nodes, the topology is of the kagome-dual (kgd) type, with the point symbol {4 3 }2{4 6 .6 6 .8 3 }. The wide inter-layer spaces (with a distance of 14 Å between the mean planes of the sheets) accommodate the counter-ions, the KPI being 0.70. Several short contacts indicate the possible presence of parallel-displaced -stacking interactions between 2,7nds . However, such interactions in an ionic species represent at most very minor contributions to the cohesion of the packing, which is predominantly the result of electrostatic interactions. [36] The hydroxide anion and the free water molecule are hydrogen bonded to uncoordinated sulfonate oxygen atoms [OO distances 2.842(3)-2.994(4) Å, O-HO angles 150-169°]. As in the previous cases, some weak CHO(sulfonate) hydrogen bonding interactions may be present as well.

The last complex, [(UO2)4Na4(2,7-nds)2(CB6)Cl4O2(H2O)10]5H2O (6), also involves the 2,7-nds 2-ligand, as well as cucurbit [6]uril (CB6) as coligand. This is the only complex in the present series to include Na + cations, which are retained through complexation to CB6. As in complex 5, chloride anions were probably introduced in the reaction mixture as impurities in the 2,7-ndsNa2 sample. The asymmetric unit contains two independent uranyl ions which give rise to a bis(3-oxo)-bridged tetranuclear species with two-fold rotation symmetry (Figure 6). Atom U1 is bound to one bridging oxo, one sulfonate and two 2-bridging chloride anions, and to a water molecule, while atom U2 is bound to two bridging oxo and two chloride anions and a water molecule, both being thus in pentagonal bipyramidal environments. The resulting (UO2)4Cl4O2 moiety has previously been described, [37][38][39] one example including uncoordinated CB6 molecules, [38] and it is a particular case of the common (UO2)4O2 4+ motif, with diverse additional lateral donors, which has previously been obtained in particular with 2-sulfobenzoate [13] and CB6 [40] as co-ligands. CB6 and water oxygen acceptors, as well as one chloride ion. Although uranyl ion binding to cucurbiturils has been achieved, [14,22,[40][41][42][43][44][45] it is often reduced to looser associations, either secondsphere or mediated by hydrogen bonds, when alkali or alkaline-earth cations are present, [14,22,43,45] due to the high affinity of cucurbiturils for the latter. In the particular case of the uranyl/alkali cation/sulfonate/CB6 system, several complexes have been obtained which display arrangements different from the present one. Three of the complexes described include either Na + or K + and 4,5dihydroxy-1,3-benzenedisulfonate and crystallize as 1D, 2D or 3D coordination polymers, with in all cases the alkali metal cations occupying the CB6 portals, and the disulfonate ligand bridging both cations. 22 In another series, uranyl dimers formed with 2-sulfobenzoate are either hydrogen bonded to discrete Na(CB6)(H2O)4 + moieties, or generate a 1D polymer through water-bridging to CB6-bound cesium cations; in contrast, 3-sulfobenzoate acts as a bridge between uranium and CB6-bound cesium cations, thus allowing the formation of a 3D framework. [14] These and the present results would indicate that disulfonate or carboxysulfonate ligands unable to chelate uranyl through both their functional groups would offer a better prospect for the formation of 3D lattices, but this is not always verified since, although 4-sulfobenzoate is able to bridge uranyl and potassium ions, a discrete heterometallic species only is formed in this case. [14] Luminescence Properties

The emission spectra of complexes 2-5 in the solid state were recorded at room temperature under excitation at a wavelength of 420 nm, a value suitable for excitation of the uranyl chromophore, [46] and they are shown in Figure 7. Only in the cases of complexes 2 and 4 are intense and well-resolved spectra obtained showing the typical vibronic progression corresponding to the S11  S00 and S10  S0 ( = 0-4) electronic transitions. [47] The spectrum of complex 2, with main maxima at 495, 518, 542 and 568 nm is blue-shifted by 8 nm with respect to that of complex 4, with maxima at 503, 526, 550 and 576 nm, although the uranyl ion environment is nearly the same in both compounds. The lower resolution in the spectrum of 4 may be a reflection of the superposition of more than one vibronic progression associated with the unique uranyl centre in the lattice. In simpler systems, multiple progressions for single centres have been resolved in lowtemperature measurements. [48] Uranyl emission in complexes 3 and 5 is largely quenched, which is less surprising in the latter case since the presence of d-block metal cations is known to have such an effect, probably through providing nonradiative relaxation pathways. [49] The maxima positions in complex 3, 502, 524, 547 and 574 nm, are close to those in complex 4, but here the peaks are weak and appear to be superimposed on a broader emission which may be due to the free bipy molecule, indicating that there may be two pathways for deactivation of the excited state produced by irradiation at 420 nm. The discernible maxima for compound 5 are at approximate values of 483, 504 and 522 nm and thus appear strongly blue-shifted with respect to those in the other complexes, although uranium environment is here also pentagonal bipyramidal (but with an equatorial array closer to planarity). While the maxima positions in uranyl emission spectra are known to be dependent on the number and nature of equatorial donors, [50,51] subtle factors are nevertheless obviously at play here since significant shifts are observed even in a series of closely related species. The average vibronic splitting energies for the S10  S0 transitions are in the range 821-897 cm -1 for complexes 2 and 4, these values being in the range usually observed. [48,[52][53][54][55][56]

Conclusions

We have described six novel complexes formed by the uranyl ion with two sulfonate ligands, 1,5-and 2,7-naphthalenedisulfonates. Although the complexing properties of this family of positional isomers of naphthalenedisulfonate ligands toward lanthanide(III) cations have been investigated, [57][58][59] the present results are the first to involve an actinide cation. The solvothermal syntheses conducted in the present work, despite being designed with the objective of obtaining mixed uranyl/metal ion species, provided such complexes in only two of the six cases where crystals were obtained and in only one case (complex 6) was the sulfonate ligand involved in bridging the two metal ions. While what is seen in the solid state may bear no relationship to what takes place in solution, these results are consistent with broader indications that sulfonate coordination is more favourable for uranyl ion than, in particular, transition metal ions. The fact that the sodium arenesulfonates used in the present work are the conjugate bases of relatively strong acids means that they have little influence on the basicity of their aqueous solutions and this is consistent with the observation that only in the presence of an additional base (bipy or phen) was there evidence for uranyl ion hydrolysis in the products presently characterized. Since, in addition, these sodium salts are quite water-soluble, advantages to the use of solvothermal methods for the synthesis of their uranyl complexes are less obvious than in the case, for example, of polycarboxylates, where hydrolysis can only be minimised by the use of the water-insoluble acids and a mixed organic-aqueous solvent is preferable to pure water.

In the whole series of complexes reported here, the sulfonate groups are bound to either one or two cations (uranyl, sodium, or a mixture thereof in the latter case), and three-fold O,Oʹ,Oʹʹcoordination is never observed, although it is known with 1,5-and 2,6-naphthalenedisulfonates in the case of lanthanide cations, [58,59] and also with the simple methanesulfonate ligand in the case of the uranyl cation. [18] 1,5-Naphthalenedisulfonate appears suitable for the building of a 3D framework with uranyl, as exemplified in the stoichiometrically simplest complex obtained (1), in which both metal and ligand are four-fold nodes. The lattice in 1 does have a layered form, with the layers "pillared" by naphthalene units apparently too close to permit guest intrusion in the pillared regions, despite the fact that the naphthalene units do not seem to be involved in significant interactions with one another. Addition of a chelating N-donor, bipy or phen, and the concomitant presence of double hydroxide bridges (possibly due to the increased basicity of the reaction medium), reduce the dimensionality and 1D coordination polymers are formed, in which each sulfonate group is unidentate (complexes 2-4). In the presence of copper(II) as counter-ion,

Crystallography:

The data were collected at 150(2) K on a Nonius Kappa-CCD area detector diffractometer [60] using graphite-monochromated Mo K radiation ( = 0.71073 Å). The crystals were introduced into glass capillaries with a protective coating of Paratone-N oil (Hampton Research). The unit cell parameters were determined from ten frames, then refined on all data. The data (combinations of -and -scans with a minimum redundancy of 4 for 90% of the reflections)

were processed with HKL2000. [61] Absorption effects were corrected empirically with the program SCALEPACK. [61] The structures were solved by intrinsic phasing with SHELXT, [62] expanded by subsequent difference Fourier synthesis and refined by full-matrix least-squares on F 2 with SHELXL-2014. [63] All non-hydrogen atoms were refined with anisotropic displacement parameters. The hydrogen atoms bound to hydroxyl and water oxygen atoms were found on difference Fourier maps (except for those of a disordered water molecule in complex 6), and the carbon-bound hydrogen atoms were introduced at calculated positions; all hydrogen atoms were treated as riding atoms with an isotropic displacement parameter equal to 1.2 times that of the parent atom. Crystal data and structure refinement parameters are given in Table 1. The molecular plots were drawn with ORTEP-3 [64] and the polyhedral representations with VESTA. [65] The topological analyses were made with TOPOS. [66] CCDC-15154301515435 contain the supplementary crystallographic data for this paper. These data can be obtained free of charge from The Cambridge Crystallographic Data Centre via www.ccdc.cam.ac.uk/data_request/cif.

Figure 1 .

 1 Figure 1. Top left: View of complex 1. Displacement ellipsoids are drawn at the 50% probability level. The carbon-bound hydrogen atoms are omitted. Symmetry codes: i = 1x, y, 1/2z; j = 3/2x, y -1/2, z; k = x -1/2, y -1/2, 1/2z; l = x

  Top right: View of the 3D framework with uranium coordination polyhedra colored yellow. Bottom left: Nodal representation of the framework down an axis slightly inclined from that in the previous view (yellow: uranium, red: oxygen, blue: disulfonate ligand). Bottom right: View of the 2D subunit with only one SO3 -group shown for each ligand.

  OH)2(bipy)2]bipy(3) and [(UO2)2(1,5-nds)(OH)2(phen)2] (4) all contain an additional chelating N-donor, either 2,2ʹ-bipyridine (bipy) or 1,10-phenanthroline (phen), as well as hydroxide ions. The consequences of the presence of these N-donors (and also that of Mn II , Ni II or Pb II , although they are not present in the final compounds) instead of 18-crown-6 in the reaction mixture proved to be quite dramatic in several ways, although the yield of crystallization of these three compounds remains low, possibly indicating that again a rather complicated mixture was present in the solution phase. The presence of the hydroxo ligands is presumably a reflection of the higher pH of the reaction mixture due to the addition of bipy or phen. The asymmetric unit contains either two uranium atoms (2) or only one (3 and 4); views of the three complexes are shown in Figures2-4, respectively. In all three

Figure 2 .

 2 Figure 2. Top: View of complex 2. Displacement ellipsoids are drawn at the 50% probability level. The solvent molecule and carbon-bound hydrogen atoms are omitted. Symmetry codes: i = 2 -x, 1 -y, 1 -z; j = -x, 1 -y, 2 -z. Bottom: Packing of the 1D polymeric chains.

Figure 3 .

 3 Figure 3. Top: View of complex 3. Displacement ellipsoids are drawn at the 50% probability level. The free bipy molecule and carbon-bound hydrogen atoms are omitted. The hydrogen bond is shown as a dashed line. Symmetry codes: i = 1 -x, 1 -y, 1 -z; j = 1 -x, 2 -y, 1 -z. Bottom: Packing of the 1D polymeric chains.

Figure 4 .

 4 Figure 4. Top: View of complex 4. Displacement ellipsoids are drawn at the 50% probability level. The carbon-bound hydrogen atoms are omitted and the hydrogen bond is shown as a dashed line. Symmetry codes: i = -x, 1 -y, 1 -z; j = 1 -x, 1 -y, -z. Bottom: Packing of the 1D polymeric chains.

  centrosymmetric sulfonate ligands produces one-dimensional (1D) heterochiral polymers directed along the [2 0 -1], [0 1 0] or [1 0 -1] axes in 2-4, respectively. While all 1,5-nds 2-ligands in one chain are parallel to one another in 3 and 4, two different orientations are present in 2. In complexes 2 and 4, the chains are arranged side-by-side to form sheets parallel to (0 1 0), with the bipy or phen molecules pointing outward on the two faces of the layers, so that inter-sheet contacts possibly associated with parallel-displaced -stacking interactions between bipy or phen molecules are present [centroidcentroid distances 3.653(3)-4.293(3) Å, dihedral angles 0-9.1(3)° in 2; 3.845(3) and 3.998(3) Å, 0 and 2.4(3)° in 4]. A weaker, intra-chain -stacking interaction between bipy and 1,5-nds 2-is also possibly present in 2 [centroidcentroid distance 4.275(3) Å, dihedral angle 22.6(3)°]. However, consideration of the Hirshfeld surfaces shows that only the two shortest of these contacts in 2, and none in 4, reveal interactions beyond dispersion. The presence of a free bipy molecule in complex 3, reflecting the higher concentration of bipy in the reaction mixture, modifies this arrangement so that both coordinated and free bipy molecules are located within the sheets parallel to (0 0 1

4 . 2 - 4 ,

 424 26 Å, which are either intra-or inter-sheet. The packings are slightly more compact in 2 and 4 (KPI 0.73) than in 3 (0.70), which is probably related to the extra bipy molecule in the latter compound and the ensuing different sheet arrangement. The complex [Cu(bipy)2Cl][UO2(2,7-nds)(OH)]H2O (5) involves a positional isomer of the ligand different from that in complexes 1-In this case, the additional metal cation present in the reaction mixture is incorporated as a counter-ion in the final compound. The unique uranium atom, in a pentagonal bipyramidal environment, is bound to two bridging hydroxide ions, as in complexes giving a centrosymmetric dimeric unit [U-O bond lengths 2.310(2) and 2.331(2) Å, U-O-U angle 113.04(8)], and to three sulfonate oxygen atoms pertaining to three different ligands [U-O bond lengths 2.384(2)-2.4636(19) Å] (Figure5). The 2,7-nds 2-ligand is thus bound to three metal cations, one of the sulfonate groups being O,Oʹ-bridging bidentate and the other unidentate. The peculiarity of the counter-ion is its inclusion of a chloride anion which must have arisen from an impurity in one reagent; since chloride anions were also found in complex 6 (see below), it is most probable that they were present in the sample of 2,7-ndsNa2 used. The [Cu(bipy)2Cl] + species is however a common one, with 30 examples reported in the CSD. The coordination polymer formed is 2D and parallel to (0 0 1), and, if the double hydroxide bridge is considered as a single link, the uranium atoms are four-fold nodes and the 2,7-nds 2-ligands three-fold ones. The point symbol, {4 2 .6 3 .8}{4 2 .6} is characteristic of the V2O5 topological type. Alternatively, if the uranyl dimers

Figure 5 .

 5 Figure 5. Top left: View of complex 5. Displacement ellipsoids are drawn at the 50% probability level. The solvent molecule and carbon-bound hydrogen atoms are omitted, and the hydrogen bond is shown as a dashed line. Symmetry codes: i = 2 -x, -y, 1 -z; j = x, y -1, z; k = 1 -x, -y, 1 -z; l = x, y + 1, z. Top right: View of the 2D assembly. Bottom left: View of the packing with layers viewed edge-on. Uranyl coordination polyhedra are yellow and those of copper(II) blue. Bottom right: Nodal representation of the 2D assembly (yellow: uranium, red: oxygen, blue: disulfonate ligand).

Figure 6 .

 6 Figure 6. Top: View of complex 6. Displacement ellipsoids are drawn at the 50% probability level. The solvent molecules and carbon-bound hydrogen atoms are omitted, and the hydrogen bonds are shown as dashed lines. Symmetry codes: i = 2 -x, y, 3/2 -z; j = 3/2 -x, 3/2 -y, z + 1/2; k = 1 -x, y, 3/2 -z; l = 3/2 -x, y -1/2, z; m = 3/2x, 3/2 -y, z -1/2; n = 3/2 -x, y + 1/2, z. Bottom: Two views of the 3D framework with solvent molecules and hydrogen atoms omitted. Uranyl coordination polyhedra are yellow and sodium(I) cations are shown as blue spheres.

Figure 7 .

 7 Figure 7. Solid state emission spectra of complexes 2-5. Excitation wavelength 420 nm.

  ). Intra-sheet parallel-displaced -stacking interactions involving either two coordinated bipy molecules pertaining to adjacent chains, or coordinated and free moieties may be

	distances 2.632(5)-2.832(5) Å, O-HO angles 158-170°], and the water molecule in 2 forms a
	hydrogen bond with two sulfonate groups [OO distances 2.788(5) and 2.914(5) Å, O-HO
	angles 171 and 149°], thus bridging adjacent chains in the sheets. The presence of uncoordinated
	sulfonate oxygen atoms not involved in OHO hydrogen bonding in all three compounds results
	present [centroidcentroid distances 3.5853(19) and 3.969(2) Å, dihedral angles 0 and 8.26(19)°],
	but examination of the Hirshfeld surfaces indicates that, in this case also, they are no greater than
	dispersion. Hydroxide ions are involved in hydrogen bonds with the solvent water molecule in 2,

and with uncoordinated sulfonate oxygen atoms pertaining to the same chain in 3 and 4 [OO

  manner that both sulfonate groups are O,Oʹ-bridging bidentate. The two independent sodium atoms, both in octahedral environments (very distorted in the case of Na1), are bound to

	either two (Na1) or one (Na2) sulfonate oxygen atoms [Na-O bond lengths 2.398(6)-2.439(5) Å,
	average 2.421(17) Å; average value for similar bonds in the CSD 2.41(15) Å], two adjacent
	carbonyl groups from CB6 [2.256(5)-2.456(6) Å, average 2.35(7) Å; 2.19-3.01 Å, average
	2.49(18) Å from the CSD], and two (Na1) or three (Na2) water molecules (two of them bridging).
	One group of two sodium ions is thus held at each CB6 portal, the CB6 molecule having two-fold
	structures reported in the CSD [2.81(2) Å and 89.55(16)°]. The bond length of 2.467(4) Å between

U1 and the sulfonate atom O8 is in the upper part of the range measured in the other complexes.

The 2,7-nds 2-ligand is bound to only one uranium atom, but it also connects three sodium(I) cations in such a rotation symmetry. This multi-component, intricate arrangement gives rise to the formation of a 3D framework. When viewed down the b axis, the assembly displays thick layers in which uranyl tetranuclear motifs and CB6 molecules are arranged in staggered rows, separated by thin layers of 2,7-nds 2-ligands, all parallel to (1 0 0). The large number of water molecules, both coordinated and free, results in many hydrogen bonding interactions being present, which involve sulfonate,

Table 1

 1 Crystal data and structure refinement details

		1	2	3	4	5	6
	Empirical formula	C10H8O9S2U	C30H26N4O13S2U2	C40H32N6O12S2U2	C34H24N4O12S2U2	C30H25ClCuN4O10S2U C56H78Cl4N24Na4O49S4U4
	M/g mol 1	574.31	1190.73	1328.89	1220.75	1002.68	3185.54
	Crystal system	Orthorhombic	Triclinic	Monoclinic	Triclinic	Triclinic	Orthorhombic
	Space group	Pbcn	Pī	P21/n	Pī	Pī	Pbcn
	a/Å	8.3036(5)	9.9948(5)	10.7903(5)	8.4226(5)	8.9368(3)	25.7129(10)
	b/Å	8.1107(3)	11.9666(8)	13.3237(7)	9.5647(6)	13.1629(7)	17.2549(4)
	c/Å	19.4518(10)	14.2331(9)	14.4850(6)	11.1317(10)	14.0127(7)	20.4342(8)
	/°	90	73.879(3)	90	106.763(4)	95.343(2)	90
	/°	90	89.140(4)	99.684(3)	97.503(5)	93.436(3)	90
	/°	90	85.100(4)	90	98.967(4)	91.245(3)	90
	V/Å 3	1310.04(11)	1629.35(17)	2052.79(17)	833.43(11)	1637.64(13)	9066.1(5)
	Z	4	2	2	1	2	4
	calcd/g cm 3	2.912	2.427	2.150	2.432	2.033	2.334
	(Mo-K)/mm 1	12.756	10.130	8.053	9.903	5.860	7.468
	F(000)	1056	1108	1252	568	966	6072
	Reflections collected	30519	88499	69485	35254	82945	184947
	Independent reflections	1688	6194	6251	3162	8446	8585
	Observed reflections [I > 2(I)]	1385	5122	5113	2901	7447	6017
	Rint	0.015	0.064	0.037	0.054	0.043	0.047
	Parameters refined	101	460	280	244	442	658
	R1	0.023	0.029	0.029	0.027	0.027	0.039
	wR2	0.056	0.065	0.068	0.066	0.061	0.082
	S	1.100	1.028	0.991	1.081	1.022	1.003
	min/e Å 3	1.29	1.63	1.80	2.33	1.67	1.09
	max/e Å 3	0.62	2.51	0.86	0.94	0.64	1.11

Luminescence measurements: Emission spectra were recorded on solid samples using a Horiba-Jobin-Yvon Fluorolog spectrofluorometer. The powdered complex was pressed between two silica plates which were mounted such that the faces were oriented vertically and at 45° to the incident excitation radiation. An excitation wavelength of 420 nm was used in all cases and the emissions monitored between 450 and 650 nm.

Experimental Section

General: UO2(NO3)2•6H2O (depleted uranium, R. P. Normapur, 99%), Ni(NO3)2•6H2O and AgNO3 were purchased from Prolabo, the di-sodium salt of 2,7-naphthalenedisulfonic acid (2,7-ndsNa2), cucurbit [6]uril pentahydrate, and 2,2ʹ-bipyridine (bipy) were from Fluka, Cu(NO3)2•2.5H2O, the di-sodium salt of 1,5-naphthalenedisulfonic acid (1,5-ndsNa2) and 1,10phenanthroline (phen) were from Aldrich. Elemental analyses were performed by MEDAC Ltd. at Chobham, UK.

Caution! Uranium is a radioactive and chemically toxic element, and uranium-containing samples must be handled with suitable care and protection.

Table of Contents