Julien Chevallier
email: julien.chevallier@dauphine.fr

Carbon Prices during the EU ETS Phase II: Dynamics and Volume Analysis

Keywords: EU ETS, Carbon Price, Phase II, CER, Spot Price, Futures Price, Options Price

The European Union Emissions Trading Scheme (EU ETS) is the largest emissions trading scheme to date. This article summarizes the principle elements behind the trading system, and details the carbon price dynamics during Phase II (2008II ( -2012)), along with an analysis of traded volumes. The main findings emphasize that the EU ETS is a rapidly growing market, which yields to innovative learning process for all participants involved: policy makers, industrial operators, and financial analysts. Besides, these results shed some light on the usefulness of credit project mechanisms, which may result in the medium-term in integrated 'world' carbon markets between various regional and/or national ETS.

Introduction

When the EU ratified the Kyoto Protocol, it committed itself to reduce Greenhouse Gases emissions (GHGs) by 8% during the period 2008-2012 compared to 1990 levels. The EU therefore decided to set a ceiling on emissions from around 12,000 industrial installations in the most energy-intensive sectors, and to implement an emissions market with the aim of reducing CO 2 emissions and achieving the Kyoto Protocol target. The European Union Emissions Trading Scheme (EU ETS) was thus created by the Directive 2003/87/EC on January 1, 2005 with a pilot phase going from 2005 to 2007. We are currently under the Phase II of the EU ETS (2008)(2009)(2010)(2011)(2012), which has been confirmed until 2020 at least (Phase III goes indeed from 2013 to 2020). European Union Allowances (EUAs), which represent the right to emit one ton of CO 2 in the atmosphere, are traded under this scheme.

By doing so, the EU clearly indicated its will to take the lead in the fight against global warming. The EU ETS is a cap-and-trade scheme, which means that the overall level of emissions is capped and up to this limit participants are allowed to buy/sell allowances (emissions rights) according to their needs2 . The scheme covers nearly half of the EU's CO 2 (Carbon Dioxide) emissions, and 40% of the EU's total GHGs emissions. The EU ETS sets a price on carbon, which can be related to market fundamentals such as institutional events, weather events, other energy market prices' influences and macroeconomic determinants [START_REF] Alberola | Price Drivers and Structural Breaks in European Carbon Prices 2005-2007[END_REF], Alberola et al. (2009a,b), Chevallier (2009a)). Phase I was introduced as a "warm-up" period from 2005 to 2007 in order to put in place the policy infrastructure of permits trading. However, the early environmental benefits were limited because of overallocation concerns among Member States [START_REF] Ellerman | Over-Allocation or Abatement? A Preliminary Analysis of the EU ETS Based on 2005 Emissions Data[END_REF], [START_REF] Ellerman | Pricing Carbon: The European Union Emissions Trading Scheme[END_REF]) and the implementation of banking restrictions between 2007 and 2008 which caused carbon spot prices and futures of maturity December 2007 to plummet towards zero (Alberola and Chevallier (2009)). This first experience also highlighted the need for reliable verified emissions data, for harmonized monitoring and reporting rules, as well as potential distortions of competition between Member States. Despite these problems, Phase I was considered as a "success"3 , which fostered various initiatives for ETS schemes around the world.

Once the EU ETS's coming into force was secured, the EU recognized (under certain conditions) credits issued via flexibility mechanisms in the Kyoto Protocol: namely, the Clean Development Mechanism (CDM) and Joint Implementation (JI) projects. Limits on the import of Certified Emissions Reductions (CERs4 ) and Emission Reduction Units (ERUs5 ) within the EU trading system appeared rapidly as part of the scheme design [START_REF] Trotignon | How Many CERs by 2013? Mission Climat Working Paper #[END_REF], Chevallier (2010a)). Extensions, concerning the inclusion of additional sectors such as aviation and petrochemicals for instance, are expected from 2013 onwards. More details on the characteristics of the EU emissions market, including cap and period, the definition of emissions rights, allocation, registries, penalties, monitoring and reporting of emissions, may be found in [START_REF] Chevallier | The European carbon market (2005-2007): banking, pricing and riskhedging strategies[END_REF].

To reflect on the rapid development of the EU ETS, this article proposes a review of the current dynamics in carbon prices, as well as on the volumes exchanged on this market. Our central results feature that the EU emissions trading system is rapidly growing, with various emissions rights being traded simultaneously: spot, futures, and options prices. We also highlight the rise of CER credits issued from project mechanisms, which can be used in the medium-term to 'link' separate regional and/or national emissions trading schemes initatives.

The remainder of the article is structured as follows. Section 2 details carbon price dynamics during Phase II. Section 3 provides an analysis of traded volumes. Section 4 concludes.

Price Dynamics

During Phase I (2005-2007) of the scheme, the demand for allowances did not follow the actual level of emissions, as documented by [START_REF] Ellerman | Over-Allocation or Abatement? A Preliminary Analysis of the EU ETS Based on 2005 Emissions Data[END_REF] By contrast, Phase II carbon prices present a more stable and healthy price pattern. As shown in Table 1, spot allowances exchanged on BlueNext (BNX) have been oscillating between €10 and €30/ton of CO 2 , depending on the levels of allowances demand (Alberola et al. (2009a,b)) due to industrial production, and the likely depressive impact of the credit crunch crisis on all commodities markets (Chevallier (2009)). In this section, we have seen that all kinds of carbon prices (spot, futures, credits from project mechanisms) are relatively stable in 2010 (in the range of €10 to €15/ton of CO 2 ), awaiting for the economic recovery after a period of strong adjustment to the financial crisis during late 2008. We have also emphasized that these effects are somewhat more pronounced for CERs than for EUAs.

In the next section, we complement our analysis of the dynamics of carbon prices with an analysis of the volumes traded for each type of contract.

Volume Analysis

In Figure 8, we observe that Phase II BNX spot allowances have been actively traded during the period going from January to May 2009, which corresponds to the 2008 compliance event. Let us now have a look at the options markets for carbon prices, which have been introduced by ECX in October 2006 for EUA futures (see [START_REF] Chevallier | Risk Aversion and Institutional Information Disclosure on the European Carbon Market: a Case-Study of the 2006 Compliance Event[END_REF] As for any financial market, the emergence of liquid options markets constitute another derivative asset that may be used by energy companies, brokers and investment banks in order to insure themselves against unwanted price movements. Hence, option prices have the ability to reflect various levels of risk-aversion embedded within market participants' utility function (in economic terms). Risk-averse agents will tend to insure themselves against 'high' carbon price levels (according to their expectations) while risk-lover agents will tend to bet against sudden price changes in market participants' expectations (around compliance events) so as to generate net profits from arbitrage activities. Risk-neutral agents, such as utilities regulated by the scheme, may also neutralize the effects of carbon price changes during compliance events by buying/selling in advance a pre-determined quantity of carbon prices at a fixed price. (2009) explain this situation by the fact that the main fear on the carbon market is that prices increase. On such a market, the easiest way to hedge again this risk is by selling calls: call option prices are therefore more actively traded than puts.

Finally, we document that strike prices range from €10 to €100 for EUA Call Options, and from €0.95 to €26 for EUA Put Options. As discussed above, this variability reflects various levels of risk-aversion which are embedded within the trading of options prices, and can go as high as €100/ton of CO 2 for EUA futures. Similarly, strike prices from €10 to €50 for CER Call Options, and from €6 to €16 for CER Put Options. The level of uncertainty attached to CER options prices also appears quite high in a context of post-Kyoto negotiations (and the fact that CERs are not confirmed to be operating after 2013 to date).

Conclusion

The Despite these adjustments, this article shows that carbon markets have continued they rapid development, by achieving record activity levels since 2005. Our analysis highlighted that EUA futures prices tend to be more actively traded than spot allowances, while CER futures prices are useful mechanisms to 'link' carbon markets worldwide, in a context of rapid development of other schemes at the regional and/or national levels. 'Financial' fundamentals in carbon prices (as opposed to 'physical' fundamentals identified during Phase I) may also be underlined as being a salient characteristic of Phase II carbon prices, with strong adjustment to the financial crisis and new behaviours from installations to sell allowances for cash when the need for liquidities rises.

  . Between the launch of the market in January 2005 and the first consolidated results of verified emissions in April 2006, the carbon price has been rising continuously due to risk-averse behaviours from installations in excess of allowances and potentially to speculative activity from brokerage firms and investment banks. Against this background, the carbon prices of all maturities encountered a dramatic downward shift in April 2006 when the rumours of 'over-allocation' hit the market a few weeks before the official audit report from the European Commission by May 15, 2006. Carbon prices fell by more than 54% in a few days, as explained by Alberola et al. (2008). Then, due to the banking restrictions implemented between 2007 and 2008 (essentially not to report excess allowances towards Phase II which coincides with the start of the Kyoto Protocol), spot prices and futures prices of maturity December 2007 have been decreasing towards zero(Alberola and Chevallier (2009)).

Figure 1 :

 1 Figure 1: Price (in €/ton) of EUA Spot Allowances Source: BlueNext

Figure 2 :

 2 Figure 2: Price (in €/ton) and Volume (in million ton) of the December 2008 EUA Futures Contract Source: ECX

Figure 3 :

 3 Figure 3: Price (in €/ton) and Volume (in million ton) of the December 2009 EUA Futures Contract Source: ECX

Figure 4 :

 4 Figure 4: Price (in €/ton) and Volume (in million ton) of the December 2010 EUA Futures Contract Source: ECX

Figure 5 :

 5 Figure 5: Price (in €/ton) and Volume (in ton) of the December 2008 CER Futures Contract Source: ECX

Figure 6 :

 6 Figure 6: Price (in €/ton) and Volume (in ton) of the December 2009 CER Futures Contract Source: ECX

Figure 7 :

 7 Figure 7: Price (in €/ton) and Volume (in ton) of the December 2010 CER Futures Contract Source: ECX

Figure 8 :

 8 Figure 8: Volume (in ton) of EUA Spot Allowances Source: BlueNext

Figure 9 :

 9 Figure 9: Open Interest on EUA Futures Contracts from April 22, 2005 to February 22, 2010 Source: ECX

Figure 10 :Figure 11 :

 1011 Figure 10: Volumes of EUA Futures Call Option Prices exchanged from January 1, 2008 to February 22, 2010 Source: ECX

  figures for each installation are known, and installations that received initially a substantial

Table 1 : Number and volume of options contracts exchanged on ECX

 1 for a detailed presentation of the options market) and in May 2008 for CER futures.

	Contract	Total Options Volume (in ton)
	ECX Futures December 2008	243,166,000
	ECX Futures December 2009	415,567,000
	ECX Futures December 2010	79,446,000
	CER Futures December 2008	67,800,000
	CER Futures December 2009	91,930,000
	CER Futures December 2010	7,750,000

Source: ECX Note: The statistics are reported for the period going from January 1, 2008 to February 22, 2010 for ECX EUA Futures, and from May 16, 2008 to February 2010 for ECX CER Options.

Table 1

 1 highlights that the use of options prices has been steadily growing since their creation, going from 243 million ton in 2008 to 416 million ton in 2009 for EUA futures, and from 68 million ton in 2008 to 92 million ton in 2009 for CER futures.

See Chevallier (2009b) for more details on the functioning of cap-and-trade schemes.

Note the notion of success may be approximated by various effects (pre-existing regulatory environment, technology innovation and diffusion, reduction of regulatory uncertainty, aggregate cost savings, etc) but we will focus on the efficiency of the permits price, i.e. its ability to reflect current information on spot and future prices.

CER means a unit issued pursuant to Article 12 of the Kyoto Protocol. These are tradable units generated by projects in non-Annex B Parties under the Clean Development Mechanism. They may be counted by Annex B Parties towards compliance with their UN and EU emissions target and are equal to one tonne of carbon dioxide equivalent gases.

ERU is a unit issued pursuant to Article

of the Kyoto Protocol. These are tradable units generated by projects in Annex 1 Parties under Joint Implementation. Annex 1 Parties may count them towards compliance with their emissions target. Each ERU is equal to one tonne of carbon dioxide equivalent gases.

Available at http://www.pointcarbon.com/

During this period, installations need to surrender as many allowances as the amount of carbon dioxide emitted during the reference year. Therefore, installations in shortage (excess) of allowances with respect to their individual allocation level may purchase (sell) allowances on the spot market in order to meet their compliance requirement in the EU ETS [START_REF] Alberola | Price Drivers and Structural Breaks in European Carbon Prices 2005-2007[END_REF]). A penalty of €100/ton of CO 2 occurs if installations do not meet their target.

In Figures 2 to 4, we notice that EUA Futures prices have been traded actively during October 2008 (when companies were selling allowances for cash in order to cope with the financial crisis), February to May 2009 (which also corresponds to the 2008 compliance event in a context of decreasing carbon prices), and in February 2010 as well.

Figures 5 to 7 show that CER futures prices have been heavily traded during August 2008 (in a context of sharp decrease of CER prices), October to December 2008 (as an adjustment to the financial crisis), in October 2009 and in January 2010 as well. We may therefore identify similar patterns with the trading of EUA futures. This situation may be explained by the fact that CER prices are discounted with a "risk premium" from EUA prices by market participants due to their higher level of risk (as discussed previously) and their limited fungibility within the EU ETS (CER prices may be imported within the EU trading system up to 13.4% on average).


S De Brion

M Bonda

C Darie

P Bordet

I Sheikin

Magnetic phase diagram of the S=1/2 triangular layered compound NaNiO 2 : a single crystal study

Keywords: numbers: 71.27+a, 75.30.Gw, 73.30Kz

Using magnetic torque measurement on a NaNiO 2 single crystal, we have established the magnetic phase diagram of this triangular compound. It presents 5 different phases depending on the temperature (4 K -300 K) and magnetic field (0 -22 T) revealing several spin reorientations coupled to different magnetic anisotropies.

Introduction

In magnetic systems with a two dimensional triangular lattice, magnetic frustration may occur depending on the nature of the magnetic interactions and the orbitals involved. The case of LiNiO 2 , where Ni 3+ has half filled e g orbitals, has been studied for a long time both experimentally and theoretically [START_REF] De Brion | Frontiers in magnetic materials[END_REF]. Recent progress on the understanding of the orbital and magnetic properties of this compound has been achieved thanks to an appropriate control of the non stoichiometry or doping effects since no pure samples are available. Indeed magnetic Ni 2+ ions are substituted between the triangular planes on the Li sites creating new magnetic exchange paths. It has been shown that Li 1-x Ni 1+x O 2 with x=0.01 does not show long range magnetic order. Rather, a fluctuating state develops which is slowed down when Mg doping is introduced and no interplane Ni 2+ are presents [START_REF] Bonda | [END_REF]. When Li is deintercalated, in Li z NiO 2 , short range incommensurate antiferromagnetic order is observed for z=3/4 and 2/3 [3]. As for the orbital part, several experimental works are in favor of the |3z 2r 2 orbital occupancy for the e g electrons with finite range order [4] or dynamical effects [START_REF] Bonda | [END_REF]. Such an occupancy is indeed observed unambiguously in the parent compound NaNiO 2 , which seems to behave more classically. It orders ferro orbitally below ∼ 480 K [5] and antiferro magnetically below 20 K [6]. We present here the first single crystal study of its magnetic phase diagram up to 20 T using torque measurements. We show that several spin reorientations occur as a function of temperature or magnetic field with unusual magnetic anisotropy.

State of the art on NaNiO 2

NaNiO 2 crystallises in the R-3m space group and, below the ferro orbital ordering temperature, becomes monoclinic (C2/m) with a=5.3087 Å, b=2.8413 Å, c=5.5670 Å, and β = 110.45 • [7]. The two dimensional triangular network of Ni 3+ becomes then distorted to accommodate the collective elongation of the oxygen octahedra surrounding the Ni ions (figure 1). At room temperature, the distorted triangles are described by two angles at 56.3 • and 61.8 • and two Ni -Ni distances at 2.84 Åand 3.01 Å. From one triangular plane to the other, the Ni-Ni distance is 5.47 Å. The antiferromagnetic ground state observed below T N is of the A type with a ferromagnetic alinement of the Ni spins in the triangular plane and an antiferromagnetic alinement from one plane to the other. The magnetic moments point at 80 • from the triangular planes. The Curie Weiss behavior of the magnetic susceptibility above 100K leads to ferromagnetic dominant interactions with a Curie Weiss temperature θ=+36 K. Below the ordering temperature (T N =20 K), application of a magnetic field reveals a spin flop transition at µ 0 H c1 =1.8 T [6] forT=4 K and another transition at µ 0 H E =8 T [9,10]. Spin wave measurements agree with an easy plane A type antiferromagnet model although there are some discrepancies between the inelastic neutron measurements [8] and the electron spin resonance measurements [10]. In this model, H E describes the strength of the antiferromagnetic coupling between the Ni planes. A small anisotropy in the easy plane is then responsible for the spin flop transition at H c1 .

Synthesis of NaNiO 2 single crystals

NaNiO 2 single crystals have been grown by molten hydroxide flux method. The flux composition was NaOH and KOH, a Ni crucible played the role of Ni source. In a preliminary step, 61.6 g of a NaOH-KOH mixture (molar ratio 1:2) was melted in a separate Ni crucible at 400 • C. The molten mixture was then poured in another 40 mL Ni crucible and placed in a preheated open vertical furnace. The experiment was carried out at 650 • C. The evaporation of the NaOH-KOH mixture at the liquid surface induces a local saturation, then nucleation and crystal growth. Runs were stopped once an abundant "crust" was observed covering the flux surface (typically after 12 hours). The crystals were easily separated from the flux with water in an ultrasonic bath. They often take the shape of hexagonal small platelets (figure 2). The crystals were characterized using scanning electron microscopy equipped with EDX analysis (relative content: Na: 0.49 , Ni: 0.51). A mixture of crystals were crushed and studied by powder X-Ray diffraction: only stoichiometric NaNiO 2 was identified. Most of the crystals are twinned in the a, b plane so that the crystal platelets contain three kinds of domains with an average c ′ direction perpendicular to the platelets plane which coincides with the Ni planes.

Magnetic torque measurements

A sample with a magnetic moment -→ m placed in a magnetic field -→ H will experience a torque

-→ Γ = -→ m × -→
H that can be measured using a cantilever (see figure 2). One of the larger crystals was selected (typically 1 mm x 1 mm x 0.2 mm) and glued on a copper-beryllium cantilever with General Electric varnish. Care was taken to avoid contact with air and moisture. The large face of the crystal containing the Ni planes was parallel to the cantilever (x, y) plane so that the z axis coincides with the crystal c ′ axis (see figure 2). The magnetic field H lies in the yz plane, making an angle θ with the z axis. The cantilever could rotate as regards the magnetic field so that θ could be varied from 0 • to 90 • . The capacitive technique allows the measurement of the torque produced in the x direction: Γ x = m y H zm z H y where m is the sample magnetic moment. It is reduced to Γ x = ∆χH 2 sin(θθ 0 ) cos(θθ 0 ) when the sample magnetic moment has a linear dependence on magnetic field. ∆χ is the difference of the magnetic susceptibility parallel and perpendicular to the z axis; θ 0 is the spin direction in absence of torque. When the magnetization is saturated, the torque should vanish except for g factor anisotropy effects, which should be negligible compared to ∆χ effects in the ordered magnetic phase. The expected torque for θ = 0 • using the easy plane model with the small anisotropy described above is given in figure 3(a), assuming that the z direction coincides with the spin direction. In the experiment, there is a 10 • difference. Because of the crystal twinning, the x and y direction are not crystallographically well defined. This means that the measurement gives the average of Γ x and Γ y . In these calculations, the torque has a quadratic dependence on the magnetic field with a change of sign and magnitude at the spin flop field (µ 0 H c1 =1.8 T) and vanishes at either H c1 or H E . We expect then to observe three different regimes labelled (a), (b) and (c) in figure 3 (3), with similar magnetic field dependencies. Note that the quadratic field dependence for these regimes does not extrapolate to zero as calculated in regime (b) but rather there is an internal torque which has different values for regime (2) and ( 3). This unexpected zero field torque can exists if the extrapolated zero field magnetization is not zero (in a canted antiferromagnet for instance) or there exist local fields that are not collinear with the sample magnetization (dipolar fields due to twinning or other anisotropic fields due to crystal field effects for instance). The presence of two regimes instead of one suggests that there is a change in the anisotropy fields, i.e. a spin reorientation. The higher field regime observed, regime (4), does not saturate at all contrary to what has been calculated for regime (c). Rather, it has the following field dependence: Torque signal ( mV) a different value. Note that these internal torques do not exist at zero field since the corresponding magnetic phases exist only at higher field. A domain pattern would have developed to compensate it and have the crystal at rest. We have investigated more deeply each regime looking at their dependence on the magnetic field orientation (see figure 4). The low field regime, regime (1), does not follow at all the expected sin(θ -θ 0 ) cos(θ -θ 0 ) law. Rather, it behaves as (1-sin 3.2(θ -105 • )) with a periodicity of 110 • . The origin of such a weird periodicity remains unclear. The presence of an incommensurate magnetic phase is to ruled out since neutron diffraction data at zero field are unambiguously fitted within a commensurate magnetic structure. On the other hand, 110 • is exactly the monoclinic (a, c) angle of the crystal structure. Macroscopic effects linked to twinning are then probably responsible but difficult to evaluate due to the low symmetry of the system. Note that the critical field at which this regime disappears has the following angular dependence: H c1 (θ) = H c1 / cos(θθ 01 ) with µ 0 H c1 =1.7 T in agreement with previous measurements [START_REF] De Brion | Frontiers in magnetic materials[END_REF]6]. The free spin direction is at θ 01 = -10 • in agreement with the neutron diffraction data [7].

Γ x = Γ 0 + α(H -H c4 ) 2 with µ 0 H c4 = 20 T.
Regime (3) has the correct angular dependence: Γ ( θ) = Γ 0 sin(θθ 0 ) cos(θθ 0 ) with θ 0 close to 0 • . Regime (2) seems intermediate between regime (1) and (3) with a constant evolution of the angular periodicity. The critical fields H c2 and H c3 at which regime (2) and (3) disappear follow the same angular dependence: H c (θ) = H c / cos((θ-θ 0 )/2) with µ 0 H c.2 =5.1 T, µ 0 H c3 =7.4 T, θ 02 = -10 • and θ 03 = +30 • . This confirms the spin reorientation process from regime (2) to (3). H c3 is in agreement with the powder data ( [9,10,11]) while H c2 was not detected previously. Finally, regime (4) follow the sin(θθ 0 ) cos(θθ 0 ) law with θ 0 close to 0 • . We have checked that the field dependence remains the same for all angles, with a constant value for µ 0 H c4 around 20 T.

Discussion

These torque measurements on a twinned crystal reveal that the NaNiO 2 system presents several spin reorientations, and very unusual magnetic anisotropies depending on magnetic field. The modelization is quite complex due to the low crystal symmetry of the compound (monoclinic unit cell) and the presence of 3 types of twins. Nevertheless, we can establish a magnetic phase diagram using these torque measurements at different temperatures (see figure 5) . As the ordering temperature is approached, regime (1) disappears together while regime (2) and (3) merge into another regime. Note that the torque diminishes as the temperature increases but has still a non vanishing field dependence. We checked that it behaves as Γ x = ∆χH 2 sin(θθ 0 ) cos(θθ 0 ) and noticed that ∆χ decreases exponentially with an activation energy exactly equals to the Curie Weiss temperature +36 K (see insert of figure 5). One concludes that there is a magnetic anisotropy induced by the exchange energy. It is responsible for the high field torque observed at low temperature which tends to vanish only above H c4 .

We can now establish the magnetic phase diagram. We have plotted in figure 6 the critical fields obtained in this work as well as in previous studies mainly on powder samples [9,11] except for the first magnetization measurements which were taken on a twinned crystal up to 3 T [6]. At low temperature, 5 phases are present: phase [START_REF] De Brion | Frontiers in magnetic materials[END_REF] where the spin lies at 10 • from the Ni plane, phases (2) and ( 3) with different spin orientations, and finally phases (4) and ( 5) which are close to full saturation. Phases (1),( 2) and (3) disappear at T N = 20 K but a cross over line persists above. This phase diagram was obtained when the magnetic field was at 10 • from the z axis. All the boundary lines correspond, to a good approximation, to the phase diagram when the magnetic field lies in the free spin direction i.e. -10 • for phase (1), +30 • for phase (3), except for the transition between phase (4) and (0) where the border line shifts to lower temperatures when θ is changed, in agreement with the specific heat data on a powdered sample [9] where a quasi vertical line is observed. While most of the phase diagram was already established, we have shown, using torque measurements on a crystal, that two additional phases are present at low temperature, phases (3) and ( 5). The transition line to phase (5), H c4 (T ), is obtained from the fit of the torque field variations. Since it is not a direct experimental measurement, its uncertainty is wider than for H c1 , H c2 and H c3 . Note that H c4 ≃ 20 T corresponds to an energy for the S=1/2 Ni 3+ spin of the order of 20 K, the same order of magnitude as the observed anisotropy activation energy and Curie-Weiss temperature of 36 K. As for the transition lines H c2 (T ) and H c3 (T ), which are quite close, it is tempting to identify them with the two zero field modes at 6.5 cm -1 and 9.0 cm -1 observed in the electron spin resonance measurements on a powdered sample at 4 K [10]. The associated magnetic fields can be matched to H c2 and H c3 assuming a gyromagnetic factor g ≃=2.6, in reasonable agreement with the observed g value at 200 K : g =2.03 and g ⊥ =2.28. This suggests that both H c2 and H c3 are associated with the same crystallographic plane as g ⊥ (perpendicular to the elongation axis of the oxygen octahedra). Note also that the presence of these two modes at 6.5 cm -1 and 9.0 cm -1 cannot be explained in an easy plane A type antiferromagnetic model with only two magnetization sublattices [10]. The inadequacy of this model is confirmed by our torque measurements in regime (2) and (3) where an internal torque has to be added to the model.

Conclusion

The magnetic study of a millimeter size NaNiO 2 crystal was achieved successfully using torque measurements. We have established the presence of 5 different ordered phases

Figure 1 .

 1 Figure 1. The triangular layered structure of NaNiO 2 . The arrows indicate the spin directions in the zero field magnetic phase.

Figure 2 .

 2 Figure 2. characteristic hexagonal shape of a 0.5 mm NaNiO 2 crystal and experimental configuration.

Figure 3 .

 3 Figure 3. Magnetic field dependence of the torque on a NaNiO 2 crystal:(a) calculation within the easy plane model, (b) measurements and second order polynomial fits. Inserts : derivative of the torque.

Figure 4 .

 4 Figure 4. Angular dependence of the torque on the NaNiO 2 crystal at different field values

igure 5 .

 5 Magnetic field dependence of the torque at different temperatures. Insert: torque parameter ∆χ as a function of temperature, the red line is an exponential fit.

µ

(3) with different spin orientations and magnetic anisotropies. The corresponding critical magnetic fields are 1.8 T, 5.1 T, 7.4 T and ∼20 T at 4 K. These reflect the presence of several characteristic energies in the system at around 2.5 K,7.5 K, 11 K and 30 K. A more complex behavior is observed than a simple easy plane A type antiferromagnet with probably different possible magnetic ground states quite close in energy.


Gérard Ferrand

Willy Lesaint

Alexandre Tessier

Towards declarative diagnosis of constraint programs over finite domains

Keywords: declarative diagnosis, algorithmic debugging, CSP, local consistency operator, fix-point, closure, inductive definition

The paper proposes a theoretical approach of the debugging of constraint programs based on a notion of explanation tree. The proposed approach is an attempt to adapt algorithmic debugging to constraint programming. In this theoretical framework for domain reduction, explanations are proof trees explaining value removals. These proof trees are defined by inductive definitions which express the removals of values as consequence of other value removals. Explanations may be considered as the essence of constraint programming. They are a declarative view of the computation trace. The diagnosis consists in locating an error in an explanation rooted by a symptom.

Introduction

Declarative diagnosis [START_REF] Shapiro | Algorithmic Program Debugging[END_REF] (also known as algorithmic debugging) have been successfully used in different programming paradigms (e.g. logic programming [START_REF] Shapiro | Algorithmic Program Debugging[END_REF], functional programming [START_REF] Nilsson | Algorithmic debugging for lazy functional languages[END_REF]). Declarative means that the user has no need to consider the computational behavior of the programming system, he only needs a declarative knowledge of the expected properties of the program. This paper is an attempt to adapt declarative diagnosis to constraint programming thanks to a notion of explanation tree.

Constraint programs are not easy to debug because they are not algorithmic programs [START_REF] Meier | Debugging constraint programs[END_REF] and tracing techniques are revealed limited in front of them. Moreover it would be incoherent to use only low level debugging tools whereas for these languages the emphasis is on declarative semantics. Here we are interested in a wide field of applications of constraint programming: finite domains and propagation.

The aim of constraint programming is to solve Constraint Satisfaction Problems (CSP) [START_REF] Tsang | Foundations of Constraint Satisfaction[END_REF], that is to provide an instantiation of the variables which is solution of the constraints. The solver goes towards the solutions combining two different methods. The first one (labeling) consists in partitioning the domains. The second one (domain reduction) reduces the domains eliminating some values which cannot be correct according to the constraints. In general, the labeling alone is very expensive and domain reduction only provides a superset of the solutions. Solvers use a combination of these two methods until to obtain singletons and test them.

The formalism of domain reduction given in the paper is well-suited to define explanations for the basic events which are "the withdrawal of a value from a domain". It has already permitted to prove the correctness of a large family of constraint retraction algorithms [START_REF] Debruyne | Correctness of constraint retraction algorithms[END_REF]. A closed notion of explanations have been proved useful in many applications: dynamic constraint satisfaction problems, over-constrained problems, dynamic backtracking,. . . Moreover, it has also been used for failure analysis in [START_REF] Jussien | User-friendly explanations for constraint programming[END_REF]. The introduction of labeling in the formalism has already been proposed in [START_REF] Lesaint | Value withdrawal explanations: a theoretical tool for programming environments[END_REF]. But this introduction complicates the formalism and is not really necessary here (labeling can be considered as additional constraints). The explanations defined in the paper provide us with a declarative view of the computation and their tree structure is used to adapt algorithmic debugging to constraint programming.

From an intuitive viewpoint, we call symptom the appearance of an anomaly during the execution of a program. An anomaly is relative to some expected properties of the program, here to an expected semantics. A symptom can be a wrong answer or a missing answer. A wrong answer reveals a lack in the constraints (a missing constraint for example). This paper focuses on the missing answers. Symptoms are caused by erroneous constraints. Strictly speaking, the localization of an erroneous constraint, when a symptom is given, is error diagnosis. It amounts to search for a kind of minimal symptom in the explanation tree. For a declarative diagnostic system, the input must include at least (1) the actual program, (2) the symptom and (3) a knowledge of the expected semantics. This knowledge can be given by the programmer during the diagnosis session or it can be specified by other means but, from a conceptual viewpoint, this knowledge is given by an oracle.

We are inspired by GNU-Prolog [START_REF] Diaz | The GNU-Prolog system and its implementation[END_REF], a constraint programming language over finite domains, because its glass-box approach allows a good understanding of the links between the constraints and the rules used to build explanations. But this work can be applied to all solvers over finite domains using propagation whatever the local consistency notion used.

Section 2 defines the basic notions of CSP and program. In section 3, symptoms and errors are described in this framework. Section 4 defines explanations. An algorithm for error diagnosis of missing answer is proposed in section 5.

Preliminary notations and definitions

This section gives briefly some definitions and results detailed in [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF].

Notations

Let us assume fixed:

• a finite set of variable symbols V ;

• a family (D x ) x∈V where each D x is a finite non empty set, D x is the domain of the variable x.

We are going to consider various families f = (f i ) i∈I . Such a family can be identified with the function i → f i , itself identified with the set {(i,

f i ) | i ∈ I}.
In order to have simple and uniform definitions of monotonic operators on a power-set, we use a set which is similar to an Herbrand base in logic programming: we define the domain by D = x∈V ({x} × D x ).

A subset d of D is called an environment. We denote by d| W the restriction of d to a set of variables W ⊆ V , that is,

d| W = {(x, e) ∈ d | x ∈ W }. Note that, with d, d ⊆ D, d = x∈V d| {x} , and (d ⊆ d ⇔ ∀x ∈ V, d| {x} ⊆ d | {x} ).
A tuple (or valuation) t is a particular environment such that each variable appears only once: t ⊆ D and ∀x ∈ V, ∃e ∈ D x , t| {x} = {(x, e)}. A tuple t on a set of variables W ⊆ V , is defined by t ⊆ D| W and ∀x ∈ W, ∃e ∈ D x , t| {x} = {(x, e)}.

Constraint Satisfaction Problem

A Constraint Satisfaction Problem (CSP) on (V, D) is made of:

• a finite set of constraint symbols C;

• a function var : C → P(V ), which associates with each constraint symbol the set of variables of the constraint;

• a family (T c ) c∈C such that: for each c ∈ C, T c is a set of tuples on var(c), T c is the set of solutions of c.

Definition 1 A tuple t is a solution of the CSP if ∀c ∈ C, t| var(c) ∈ T c .
From now on, we assume fixed a CSP (C, var, (T c ) c∈C ) on (V, D) and we denote by Sol its set of solutions.

Example 1 The conference problem [START_REF] Jussien | User-friendly explanations for constraint programming[END_REF] Michael, Peter and Alan are organizing a two-day seminar for writing a report on their work. In order to be efficient, Peter and Alan need to present their work to Michael and Michael needs to present his work to Alan and Peter. So there are four variables, one for each presentation: Michael to Peter (MP), Peter to Michael (PM), Michael to Alan (MA) and Alan to Michael (AM). Those presentations are scheduled for a whole half-day each.

Michael wants to know what Peter and Alan have done before presenting his own work (MA > AM, MA > PM, MP > AM, MP > PM). Moreover, Michael would prefer not to come the afternoon of the second half-day because he has got a very long ride home (MA = 4, MP = 4, AM = 4, PM = 4). Finally, note that Peter and Alan cannot present their work to Michael at the same time (AM = PM). The solutions of this problem are: {(AM,2),(MA,3),(MP,3),(PM,1)} and {(AM,1),(MA,3),(MP,3),(PM,2)}.

The set of constraints can be written in GNU-Prolog [START_REF] Diaz | The GNU-Prolog system and its implementation[END_REF] as:

conf(AM,MP,PM,MA):- fd_domain([MP,PM,MA,AM],1,4), MA #> AM, MA #> PM, MP #> AM, MP #> PM, MA #\= 4, MP #\= 4, AM #\= 4, PM #\= 4, AM #\= PM.

Constraint Satisfaction Program

A program is used to solve a CSP, (i.e to find the solutions) thanks to domain reduction and labeling. Labeling can be considered as additional constraints, so we concentrate on the domain reduction. The main idea is quite simple: to remove from the current environment some values which cannot participate to any solution of some constraints, thus of the CSP. These removals are closely related to a notion of local consistency. This can be formalized by local consistency operators.

Definition 2 A local consistency operator r is a monotonic function r : P(D) → P(D).

Note that in [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF], a local consistency operator r have a type (in(r), out(r)) with in(r), out(r) ⊆ D. Intuitively, out(r) is the set of variables whose environment is reduced (values are removed) and these removals only depend on the environments of the variables of in(r). But this detail is not necessary here.

Example 2

The GNU-Prolog solver uses local consistency operators following the X in r scheme [START_REF] Codognet | Compiling constraints in clp(fd)[END_REF]: for example, AM in 0..max(MA)-1. It means that the values of AM must be between 0 and the maximal value of the environment of MA minus 1.

As we want contracting operator to reduce the environment, next we will consider d → d ∩ r(d). But in general, the local consistency operators are not contracting functions, as shown later to define their dual operators.

A program on (V, D) is a set R of local consistency operators.

Example 3 Following the X in r scheme, the GNU-Prolog conference problem is implemented by the following program:

From now on, we assume fixed a program R on (V, D). We are interested in particular environments: the common fix-points of the reduction operators d → d∩r(d), r ∈ R. Such an environment d verifies ∀r ∈ R, d = d ∩ r(d ), that is values cannot be removed according to the operators.

Definition 3 Let r ∈ R. We say an environment d is r-consistent if d ⊆ r(d).
We say an environment In general, we are interested in the closure of D by R (the computation starts from D), but sometimes we would like to express closures of subset of D (environments, tuples). It is also useful in order to take into account dynamic aspects or labeling [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF][START_REF] Debruyne | Correctness of constraint retraction algorithms[END_REF].

d is R-consistent if ∀r ∈ R, d is r-consistent.

Example 4

The execution of the GNU-Prolog program provides the following closure: {(AM,1),(AM,2),(MA,2),(MA,3),(MP,2),(MP,3),(PM,1),(PM,2)}.

By definition 4, since d ⊆ D:

Lemma 1 If d is R-consistent then d ⊆ CL ↓(D, R).

Links between CSP and program

Of course, the program is linked to the CSP. The operators are chosen to "implement" the CSP. In practice, this correspondence is expressed by the fact that the program is able to test any valuation. That is, if all the variables are bounded, the program should be able to answer to the question: "is this valuation a solution of the CSP ?". Definition 5 A local consistency operator r preserves the solutions of a set of constraints C if, for each tuple t,

(∀c ∈ C , t| var(c) ∈ T c ) ⇒ t is r-consistent.
In particular, if C is the set of constraints C of the CSP then we say r preserves the solutions of the CSP.

In the well-known case of arc-consistency, a set of local consistency operators R c is chosen to implement each constraint c of the CSP. Of course, each r ∈ R c preserves the solutions of {c}. It is easy to prove that if r preserves the solutions of C and C ⊆ C, then r preserves the solutions C. Therefore ∀r ∈ R c , r preserves the solutions of the CSP.

To preserve solutions is a correction property of operators. A notion of completeness is used to choose the set of operators "implementing" a CSP. It ensures to reject valuations which are not solutions of constraints. But this notion is not necessary for our purpose. Indeed, we are only interested in the debugging of missing answers, that is in locating a wrong local consistency operators (i.e. constraints removing too much values).

In the following lemmas, we consider S ⊆ Sol, that is S a set of solutions of the CSP and S (= t∈S t) its projection on D.

Lemma 2 Let S ⊆ Sol, if r preserves the solutions of the CSP then S is r-consistent.

Proof. ∀t ∈ S, t ⊆ r(t) so S ⊆ t∈S r(t). Now, ∀t ∈ S, t ⊆ S so ∀t ∈ S, r(t) ⊆ r( S).

Extending definition 5, we say R preserves the solutions of C if for each r ∈ R, r preserves the solutions of C. From now on, we consider that the fixed program R preserves the solutions of the fixed CSP.

Lemma 3 If S ⊆ Sol then S ⊆ CL ↓(D, R).
Proof. by lemmas 1 and 2.

Finally, the following corollary emphasizes the link between the CSP and the program.

Corollary 1

Sol ⊆ CL ↓(D, R).

The downward closure is a superset (an "approximation") of Sol which is itself the projection (an "approximation") of Sol. But the downward closure is the most accurate set which can be computed using a set of local consistency operators in the framework of domain reduction without splitting the domain (without search tree).

Expected Semantics

To debug a constraint program, the programmer must have a knowledge of the problem. If he does not have such a knowledge, he cannot say something is wrong in his program! In constraint programming, this knowledge is declarative.

Correctness of a CSP

At first, the expected semantics of the CSP is considered as a set of tuples: the expected solutions. Next definition is motivated by the debugging of missing answer.

Definition 6 Let S be a set of tuples. The CSP is correct wrt S if S ⊆ Sol.

Note that if the user exactly knows S then it could be sufficient to test each tuple of S on each local consistency operator or constraint. But in practice, the user only needs to know some members of S and some members of D \ S. We consider the expected environment S, that is the approximation of S.

By lemma 2:

Lemma 4 If the CSP is correct wrt a set of tuples S then S is R-consistent.

Symptom and Error

From the notion of expected environment, we can define a notion of symptom. A symptom emphasizes a difference between what is expected and what is actually computed.

Definition 7 h ∈ D is a symptom wrt an expected environment d if h ∈ d \ CL ↓(D, R).
It is important to note that here a symptom is a symptom of missing solution (an expected member of D is not in the closure). As we know, a solution of the conference problem contains (AM,1). But, the execution provides an empty closure. So, in particular, (AM,1) has been removed. Thus, (AM,1) is a symptom.

Definition 8 R is approximately correct wrt d if d ⊆ CL ↓(D, R).
Note that R is approximately correct wrt d is equivalent to there is no symptom wrt d. By this definition and lemma 1 we have:

Lemma 5 If d is R-consistent then R is approximately correct wrt d.
In other words, if d is R-consistent then there is no symptom wrt d. But, our purpose is debugging (and not program validation), so:

Lemma 6 CL ↑(d, R) = CL ↓(d, R). Proof. CL ↑(d, R) = min{d | d ⊆ d , ∀ r ∈ R, r(d ) ⊆ d } = min{d | d ⊆ d , ∀r ∈ R, d ⊆ r(d )} = max{d | d ⊆ d, ∀r ∈ R, d ⊆ r(d )}
Now, we associate rules in the sense of [START_REF] Aczel | An introduction to inductive definitions[END_REF] with these dual operators. These rules are natural to build the complementary of an environment and well suited to provide proof (trees) of value removals.

Definition 12 A deduction rule is a rule h ← B such that h ∈ D and B ⊆ D.
Intuitively, a deduction rule h ← B can be understood as follow: if all the elements of B are removed from the environment, then h does not participate in any solution of the CSP and it can be removed.

A very simple case is arc-consistency where the B corresponds to the wellknown notion of support of h. But in general (even for hyper arc-consistency) the rules are more intricate. Note that these rules are only a theoretical tool to define explanations and to justify the error diagnosis method. But in practice, this set does not need to be given. The rules are hidden in the algorithms which implement the solver.

For each operator r ∈ R, we denote by R r a set of deduction rules which defines r, that is, R r is such that:

r(d) = {h ∈ D | ∃B ⊆ d, h ← B ∈ R r }.
For each operator, this set of deduction rules exists. There possibly exists many such sets, but for classical notions of local consistency one is always natural [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF]. The deduction rules clearly appear inside the algorithms of the solver. In [START_REF] Apt | Automatic generation of constraint propagation algorithms for small finite domains[END_REF] the proposed solver is directly something similar to the set of rules (it is not exactly a set of deduction rules because the heads of the rules do not have the same shape that the elements of the body).

Example 6 With the GNU-Prolog operator AM in 0..max(MA)-1 are associated the deduction rules:

• (AM,1) ← (MA,2), (MA,3), (MA,4)

• (AM,2) ← (MA,3), (MA,4)

• (AM,3) ← (MA,4) • (AM,4) ← ∅
Indeed, for the first one, the value 1 is removed from the environment of AM only when the values 2, 3 and 4 are not in the environment of MA.

From the deduction rules, we have a notion of proof tree [START_REF] Aczel | An introduction to inductive definitions[END_REF]. We consider the set of all the deduction rules for all the local consistency operators of R: let R = r∈R R r .

We denote by cons(h, T ) the tree defined by: h is the label of its root and T the set of its sub-trees. The label of the root of a tree t is denoted by root(t). Definition 13 An explanation is a proof tree cons(h, T ) with respect to R; it is inductively defined by: T is a set of explanations with respect to R and

(h ← {root(t) | t ∈ T }) ∈ R.
Example 7 The explanation of figure 1 is an explanation for (AM,1). Note that the root (AM,1) of the explanation is linked to its children by the deduction rule (AM,1) ← (MA,2), (MA,3), (MA,4). Here, since each rule is associated with an operator which is itself associated with a constraint (arc-consistency case), the constraint is written at the right of the rule.

Finally we prove that the elements removed from the domain are the roots of the explanations.

Theorem 2 CL ↓(D, R) is the set of the roots of explanations with respect to R.

Proof. Let E the set of the roots of explanations wrt to R. By induction on explanations

E ⊆ min{d | ∀ r ∈ R, r(d) ⊆ d}. It is easy to check that r(E) ⊆ E. Hence, min{d | ∀ r ∈ R, r(d) ⊆ d} ⊆ E. So E = CL ↑(∅, R).
In [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF] there is a more general result which establishes the link between the closure of an environment d and the roots of explanations of R∪{h ← ∅ | h ∈ d}. But here, to be lighter, the previous theorem is sufficient because we do not consider dynamic aspects. All the results are easily adaptable when the starting environment is d ⊂ D.

Computed explanations

Note that for error diagnosis, we only need a program, an expected semantics, a symptom and an explanation for this symptom. Iterations are briefly mentioned here only to understand how explanations are computed in concrete terms, as in the PaLM system [START_REF] Jussien | The PaLM system: explanation-based constraint programming[END_REF]. For more details see [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF].

CL ↓(d, R) can be computed by chaotic iterations introduced for this aim in [START_REF] Fages | A reactive constraint logic programming scheme[END_REF].

The principle of a chaotic iteration [START_REF] Apt | The essence of constraint propagation[END_REF] is to apply the operators one after the other in a "fairly" way, that is such that no operator is forgotten. In practice this can be implemented thanks to a propagation queue. Since ⊆ is a wellfounded ordering (i.e. D is a finite set), every chaotic iteration is stationary. The well-known result of confluence [START_REF] Cousot | Automatic synthesis of optimal invariant assertions mathematical foundation[END_REF][START_REF] Fages | A reactive constraint logic programming scheme[END_REF] ensures that the limit of every chaotic iteration of the set of local consistency operators R is the downward closure of D by R. So in practice the computation ends when a common fix-point is reached. Moreover, implementations of solvers use various strategies in order to determine the order of invocation of the operators. These strategies are used to optimize the computation, but this is out of the scope of this paper.

We are interested in the explanations which are "computed" by chaotic iterations, that is the explanations which can be deduced from the computation of the closure. A chaotic iteration amounts to apply operators one after the other, that is to apply sets of deduction rules one after another. So, the idea of the incremental algorithm [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF] is the following: each time an element h is removed from the environment by a deduction rule h ← B, an explanation is built. Its root is h and its sub-trees are the explanations rooted by the elements of B.

Note that the chaotic iteration can be seen as the trace of the computation, whereas the computed explanations are a declarative vision of it.

The important result is that CL ↓(d, R) is the set of roots of computed explanations. Thus, since a symptom belongs to CL ↓(d, R), there always exists a computed explanation for each symptom.

Error Diagnosis

If there exists a symptom then there exists an erroneous operator. Moreover, for each symptom an explanation can be obtained from the computation. This section describes how to locate an erroneous operator from a symptom and its explanation.

From Symptom to Error

Definition 14 A rule h ← B ∈ R r is an erroneous rule wrt d if B ∩ d = ∅ and h ∈ d.
It is easy to prove that r is an erroneous operator wrt d if and only if there exists an erroneous rule h ← B ∈ R r wrt d. Consequently, theorem 1 can be extended into the next lemma.

Lemma 7 If there exists a symptom wrt d then there exists an erroneous rule wrt d.

We say a node of an explanation is a symptom wrt d if its label is a symptom wrt d. Since, for each symptom h, there exists an explanation whose root is labeled by h, it is possible to deal with minimality according to the relation parent/child in an explanation. Note that the user has to answer to only three questions whereas the explanation contains height nodes, there are sixteen removed values and eighteen operators for this problem. So, it seems an efficient way to find an error.

Note that it is not necessary for the user to exactly know the set of solutions, nor a precise approximation of them. The expected semantics is theoretically considered as a partition of D: the elements which are expected and the elements which are not. For the error diagnosis, the oracle only have to answer to some questions (he has to reveal step by step a part of the expected semantics). The expected semantics can then be considered as three sets: a set of elements which are expected, a set of elements which are not expected and some other elements for which the user does not know. It is only necessary for the user to answer to the questions.

It is also possible to consider that the user does not answer to some questions, but in this case there is no guarantee to find an error [START_REF] Tessier | Analysis and Visualisation Tools for Constraint Programming[END_REF]. Without such a tool, the user is in front of a chaotic iteration, that is a wide list of events. In these conditions, it seems easier to find an error in the code of the program than to find an error in this wide trace. Even if the user is not able to answer to the questions, he has an explanation for the symptom which contains a subset of the CSP constraints.

Conclusion

Our theoretical foundations of domain reduction have permitted to define notions of expected semantics, symptom and error.

Explanation trees provide us with a declarative view of the computation and their tree structure is used to adapt algorithmic debugging [START_REF] Shapiro | Algorithmic Program Debugging[END_REF] to constraint programming. The proposed approach consists in comparing expected semantics (what the user wants to obtain) with the actual semantics (the closure computed by the solver). Here, a symptom, which expresses a difference between the two semantics is a missing element, that is an expected element which is not in the closure. Since the symptom is not in the closure there exists an explanation for it (a proof if its removal). The diagnosis amounts to search for a minimal symptom in the explanation (rooted by the symptom), that is to locate the error from the symptom. The traversal of the tree is done thanks to an interaction with an oracle (usually the user): it consists in questions to know if an element is member of the expected semantics.

It is important to note that the user does not need to understand the computation of the constraint solver, unlike a method based on a presentation of the trace. A declarative approach is then more convenient for constraint programs. Especially as the user only has a declarative knowledge of its problem/program and the solver computation is too intricate to understand.

  Domain reduction from a domain d by R amounts to compute the greatest fix-point of d by R. Definition 4 The downward closure of d by R, denoted by CL ↓(d, R), is the greatest d ⊆ D such that d ⊆ d and d is R-consistent.

Example 5

 5 From now on, let us consider the new following CSP in GNU-Prolog: conf(AM,MP,PM,MA):-fd_domain([MP,PM,MA,AM],1,4), MA #> AM, MA #> PM, MP #> AM, PM #> MP, MA #\= 4, MP #\= 4, AM #\= 4, PM #\= 4, AM #\= PM.

Figure 1 :

 1 Figure 1: An explanation for (AM,1)

Definition 15 A

 15 symptom is minimal wrt d if none of its children is a symptom wrt d. associated to the constraint PM>MP. Indeed, Michael wants to know what Peter have done before presenting his own work would be written PM<MP.

This work is supported by the French RNTL project OADymPPaC. http://contraintes.inria.fr/OADymPPaC/

Corollary 2 Let S be a set of expected tuples. If R is not approximately correct wrt S then S is not R-consistent, thus the CSP is not correct wrt S.

The lack of an expected value is caused by an error in the program, more precisely a local consistency operator. If an environment d is not R-consistent, then there exists an operator r ∈ R such that d is not r-consistent.

Note that d is R-consistent is equivalent to there is no erroneous operator wrt d in R.

Theorem 1 If there exists a symptom wrt d then there exists an erroneous operator wrt d (the converse does not hold).

When the program is R = c∈C R c with each R c a set of local consistency operators preserving the solutions of c, if r ∈ R c is an erroneous operator wrt S then it is possible to say that c is an erroneous constraint. Indeed, there exists a value (x, e) ∈ S \ r( S), that is there exists t ∈ S such that (x, e) ∈ t \ r(t). So t is not r-consistent, so t| var(c) ∈ T c i.e. c rejects an expected solution.

Explanations

The previous theorem shows that when there exists a symptom there exists an erroneous operator. The goal of error diagnosis is to locate such an operator from a symptom. To this aim we now define explanations of value removals as in [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF], that is a proof tree of a value removal. If a value has been wrongly removed then there is something wrong in the proof of its removal, that is in its explanation.

Explanations

First we need some notations. Let d = D\d. In order to help the understanding, we always use the notation d for a subset of D if intuitively it denotes a set of removed values.

Definition 10 Let r be an operator, we denote by r the dual of r defined by: ∀d ⊆ D, r(d) = r(d).

We consider the set of dual operators of R: let R = { r | r ∈ R}.

Definition 11

The upward closure of d by R, denoted by CL ↑(d, R) exists and is the least d such that d ⊆ d and ∀r ∈ R, r(d ) ⊆ d (see [START_REF] Ferrand | Theoretical foundations of value withdrawal explanations for domain reduction[END_REF]).

Next lemma establishes the correspondence between downward closure of local consistency operators and upward closure of their duals.

Note that if h is a minimal symptom wrt d then h ∈ d and the set of its children B is such that B ⊆ d. In other words h ← B is an erroneous rule wrt d.

Theorem 3 In an explanation rooted by a symptom wrt d, there exists at least one minimal symptom wrt d and the rule which links the minimal symptom to its children is an erroneous rule.

Proof. Since explanations are finite trees, the relation parent/child is well-founded.

To sum up, with a minimal symptom is associated an erroneous rule, itself associated with an erroneous operator. Moreover, an operator is associated with, a constraint (e.g. the usual case of hyper arc-consistency), or a set of constraints. Consequently, the search for some erroneous constraints in the CSP can be done by the search for a minimal symptom in an explanation rooted by a symptom.

Diagnosis Algorithms

The error diagnosis algorithm for a symptom (x, e) is quite simple. Let E the computed explanation of (x, e).

The aim is to find a minimal symptom in E by asking the user with questions as: "is (y, f ) expected ?".

Note that different strategies can be used. For example, the "divide and conquer" strategy: if n is the number of nodes of E then the number of questions is O(log(n)), that is not much according to the size of the explanation and so not very much compared to the size of the iteration.

Example 8 Let us consider the GNU-Prolog CSP of example 5. Remind us that its closure is empty whereas the user expects (AM,1) to belong to a solution. Let the explanation of figure 1 be the computed explanation of (AM,1). A diagnosis session can then be done using this explanation to find the erroneous operator or constraint of the CSP.

Following the "divide and conquer" strategy, first question is: "Is (MA,3) a symptom ?". According to the conference problem, the knowledge on MA is that Michael wants to know other works before presenting is own work (that is MA>2) and Michael cannot stay the last half-day (that is MA is not 4). Then, the user's answer is: yes.

Second question is: "Is (PM,2) a symptom ?". According to the conference problem, Michael wants to know what Peter have done before presenting his own work to Alan, so the user considers that (PM,2) belongs to the expected environment: its answer is yes.

Third question is: "Is (MP,1) a symptom ?". This means that Michael presents his work to Peter before Peter presents his work to him. This is contradicting the conference problem: the user answers no.

So, (PM,2) is a minimal symptom and the rule (PM,2) ← (MP,1) is an erroneous one. This rule is associated to the operator PM in min(MP)+1..infinite,