T Zemach
email: tamar.zemach@yahoo.com

) M Ungarish

) A Martin

M E Negretti

Affiliations

On gravity currents of fixed volume that encounter a down-slope or up-slope bottom

We consider a gravity current released from a lock into an ambient flui of smaller density, that, from the beginning or after some horizontal propagation X 1 , propagates along an inclined (up-or down-) bottom. The flo (assumed in the inertial-buoyancy regime) is modeled by the shallow-water (SW) equations with a jump condition applied at the nose (front). The behavior of the current is dominated by the slope angle, θ, but is also affected by additional dimensionless parameters: the aspect ratio of the lock x 0 /h 0 , the height ratio of the ambient to lock, H/h 0 , and the distance of the backwall from the beginning of the slope, X 1 /x 0 . We show that the stability of the interface, reflecte by the value of the bulk Richardson number, Ri, is essential in the interpretation and modeling. In the upslope flow Ri increases and hence entrainment/mixing effects are unimportant. In the downslope flow the current firs accelerates and Ri decreases; this enhances entrainment and drag, which then decelerate the current. We show that the accelerating-decelerating downstream current is reproduced well by a SW model combined with a simple closure for the entrainment and drag. A comparison of the theoretical results with previously published experimental data for both upslope flo and downslope flo show fair agreement.

I. INTRODUCTION

Gravity currents (GCs) are ubiquitous in many geophysical and environmental flow such as salt intrusions into lakes and estuaries, glacial runoff into the ocean, turbidity currents in coastal regions, cold downhill airflow in mountain areas, or snow avalanches. In oceans, dense currents descend the continental slope for long distances before encountering the ocean bottom or interleaving at their level of neutral buoyancy (e.g., Ref. 1). In mountain areas, the dynamics of the atmospheric boundary layer is dominated by downslope currents. In enclosed mountain valleys, pollutants emitted by traffic heating/cooling systems, and industry transported by katabatic winds are mainly trapped at low altitudes (Ref. 11) with well-known important consequences on human health. Avalanches are natural hazards that are observed quite frequently in winter and spring and which cause relevant damages to our infrastructures such as buildings, roads, and electric power transmission and can cost life to humans. While the generating mechanism of avalanches remains quite unpredictable, their development is strongly dependent on the characteristics of the terrain as the slope angle variations (e.g., Ref. [START_REF] Hopfinger | Snow avalanche motion and related phenomena[END_REF].

The typical gravity current of one density (ρc) is released from a lock of length x 0 and height h 0 into another flui of a different density (ρa) and is driven by the reduced gravity g ′ = (ρc/ρa -1)g, where g is the gravitational acceleration and we assume ρc > ρa. Let xN(t) denote the horizontal distance of propagation as a function of time and uN(t) denote the corresponding speed of propagation of the nose (front).

In many cases of interest, the gravity current (GC) encounters a topography, i.e., an upslope or downslope. 2,5,10,16,28 These problems have received recent attention in the works of Refs. 22, 8, and 21. These studies emphasize the experimental observation and are therefore focused on a rather restricted range of parameters. Indeed, the dimensions of typical laboratory tanks pose severe limitations on the size of the lock, length of the inclined slope, and angle θ. For a comprehensive understanding and prediction of the flow a general model, built on clear-cut equations of motion, accepting realistic initial and boundary conditions, and not reliant on adjustable constants, is necessary. Unfortunately, such a model has not been presented and tested, to the best of our knowledge.

The experiments (e.g., Refs. 22 and 8) reveal that in downslope flow the current firs accelerates and then decelerates. These observations are routinely compared with the model (referred to as "power law" or "thermal theory") of Ref. [START_REF] Beghin | Gravitational convection from instantaneous sources on inclined boundaries[END_REF] xN ≙ ξ 0 +K(g ′ h 0 x 0 ) 1/3 (t+ τ 0 ) 2/3 (dimensional), where ξ 0 , τ 0 are adjustable constants, and the dimensionless K is given by a formula which contains the entrainment and drag coefficient E, C d and some adjustable shape-factors. Thermal theory describes both the acceleration phase and the equilibrium state of the current; herein, the common approach is based on a balance between the momentum and mass conservation equations of the finit volume released gravity current. This assessment is based on the following limiting assumptions: (1) geometric simplification of the shape of the finit volume released flo (e.g., halfellipse, rectangle), (2) self-similarity, and (3) empirical estimates of entrainment and drag coefficients For the upslope current, the authors of Ref. [START_REF] Marleau | Gravity currents propagating up a slope[END_REF] developed an approximation that predicts constant deceleration and hence provided a simple algebraic estimate to the position where the current stops (uN = 0), under the assumption that the speed at the base of the slope is known. This, again, employs some bold assumptions (e.g., the nose Froude number is a constant). It is worthy to emphasize the differences between the ingredients of the down-slope and up-slope propagation formulas of Refs. 3 and 21: the firs uses entrainment and drag but ignores the front Fr condition; the second uses the front Fr condition but discards entrainment and drag. This is intriguing because essentially this is the same gravity current, released from the same lock. Here, we attempt to close this gap of knowledge.

Our starting point is the horizontal current. There is evidence that for a high-Reynolds-number gravity current, the shallow-water (SW) theory with a Fr number jump condition at xN predicts well the dam-break process after release from the lock (see Ref. [START_REF] Ungarish | An Introduction to Gravity Currents and Intrusions[END_REF]). The SW equations can be applied to nonhorizontal boundaries. However, it turns out that the interpretation of the flo in the presence of |θ| > 0 and the elucidation of the differences between the up-and down-slope cases are not straightforward. To this end, solutions of the SW equations (by finit difference method) are needed, and, at a later stage, the reason for significan entrainment and the extension of the SW model must be addressed. Support to this unifie theoretical approach is sought in comparisons with available experimental data. This is the objective of our paper.

We note that SW models for an inclined bottom have been used by Ref. [START_REF] Lombardi | Gravity currents flowin upslope: Laboratory experiments and shallow-water simulations[END_REF]. However, that work was focused on a special configura tion of full-depth lock in a tank with an open top, incorporated from the beginning adjustable parameters, and lacked a clear-cut Fr jump condition. This precludes the insights and versatility attainable by the present simpler SW model.

The paper is organized as follows. The shallow-water formulation is presented in Sec. II, and the finite-differenc method used for the solution is presented in Sec. III. Theoretical predictions for down-slope and up-slope cases are discussed in Secs. III A and III B. Comparisons with experiments, presented in Sec. IV, show good agreement for the upslope case but less satisfactory performance for the downslope case. The reasons are discussed in Sec. IV B 1, and it is shown that the remedy for the downslope configuratio is an extended SW model which includes the effects of entrainment and drag. Concluding remarks are given in Sec. V.

II. FORMULATION

Consider a gravity current created by release of a fixe volume constant density ρc and kinematic viscosity ν into an ambient flui of constant density ρa. The system is sketched in Fig. 1. The current is propagating in the x-direction in a channel with a partially inclined FIG. 1. Schematic description of the current released from a lock of length x 0 and height h 0 in a channel of height H(x) with a horizontal top and a bottom slope starting at x = X 1 . tan θ = -dH/dx.

bottom. The height of the channel H(x) is dependent on x and is assumed to be constant for x ≤ X 1 and to be a linear function of x for x > X 1 .

The system under consideration is sketched in Fig. 1: the top and the bottom of the half-infinit channel are at z = 0 and z = H(x). Gravity acts in the z direction. At time t = 0, a given volume of flui of density ρc > ρa, initially at rest in reservoir of height h 0 and length x 0 , is instantaneously released into the ambient fluid A twodimensional {x, z} Cartesian coordinate system with corresponding {u, w} velocity components is employed. The fluid are assumed to be separated by a sharp, nonentraining interface (this will be reconsidered later). Let the subscripts c and a denote the current and the ambient domains. The height of the current is h(x, t), and that of the ambient flui is ha(x, t) = H(x)h(x, t). The SW approximation assumes that the current is thin (formally, h 0 /x 0 ≪ 1), and hence the motion can be represented by the z-averaged (over the thickness of the layer) velocity of the current u(x, t) and of the ambient flui ua(x, t). The task is to obtain the equations of motion. The methodology has been discussed in the literature (e.g., Refs. 30 and 31). Here, we briefl show some details which are of importance to the nonhorizontal bottom configuration Let p denote the pressure. The SW approximation implies that in the vertical direction, the velocity and acceleration are small, and therefore, the pressure (a) obeys the hydrostatic balance and (b) is continuous at the interface z = h(x, t). This can be expressed as

pa(x, z, t) ≙ Φ(x, t); pc(x, z, t) ≙ Δρg(z -ha) + Φ(x, t), ( 2.1)
where Δρ = ρcρa.

The pressure gradient in the current does not dependent on z, and it can be written as

∂pc ∂x ≙ -Δρg ∂ha ∂x + ∂Φ(x, t) ∂x . (2.2)
The Reynolds number of the flow Re = hNuN/ν, where the subscript N denotes value associated with the "nose" of the current, is assumed large. Since the viscous terms are negligible, the x-pressure gradient is balanced by the inertial terms. The resulting set of continuity equations and inertial-pressure (x-momentum balance) of the problem are

⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ∂h ∂t + ∂ ∂x (uh) ≙ 0, ∂ha ∂t + ∂ ∂x (uaha) ≙ 0, ∂u ∂t + ∂ ∂x ( 1 2 u 2 ) ≙ -1 ρc [-Δρg ∂ha ∂x + ∂Φ ∂x ], ∂ua ∂t + ∂ ∂x ( 1 2 u 2 a ) ≙ -1 ρa ∂Φ ∂x .
(2.

3)

The firs two equations in system (2.3) represent conservation of volume in each layer, and the next two equations represent balance of horizontal momentum in a hydrostatic pressure fiel in each layer.

A useful reduction of system (2.3) is obtained by the elimination of the ambient-layer variables. The upper boundary is considered a fixe top, and there is no flo through the x = 0 backwall. This yields

h + ha ≙ H(x)
(2.4) and uh + uaha ≙ 0.

(

Combining (2.3) with (2.4) and (2.5) provides, after some algebra, the set of governing equations for the variables h(x, t) and u(x, t) of the current,

⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ ∂h ∂t + ∂ ∂x (uh) ≙ 0, ∂u ∂t [1 + ρa ρc a 1 -a ] + u ∂u ∂x [1 - ρa ρc a(1 + a) (1 -a) 2 ] + ∂h ∂x [ Δρ ρc g - ρa ρc u 2 1 H(1 -a) 3 ] ≙ dH dx [ Δρ ρc g - ρa ρc u 2 a 2 H(1 -a) 3 ]. (2.
{x * , z * , h * , H * , t * , u * } ≙ {x 0 x, h 0 z, h 0 h, h 0 H, Tt, Uu}, (2.7)
where

U ≙ √ Δρ ρc gh 0 ; T ≙ x 0 U . (2.8)
In the characteristic dimensionless form, the equations become

( h u ) t + ( u h B (1 -2A)u )( h u ) x ≙ ⎛ ⎝ 0 C ⋅ dH dx ⎞ ⎠ . ( 2

.9)

Here, (2.11)

A ≙ 1 1 -a + Ra Ra 1 -a , B ≙ 1 1 -a + Ra [1 -a - R H(1 -a) 2 u 2 ], C ≙ 1 1 -a + Ra [1 -a - R H(1 -a) 2 u 2 a 2 ],
The Boussinesq system corresponds to R ≈ 1. In the formulation, we simply substitute R = 1. System (2.9) is hyperbolic. The relationships between the variables on the characteristics are as follows:

du ≙ u(1 -2A) -λ± h dh + C dH dx dt on dx dt ≙ λ± ≙ u(1 -A) ± √ A 2 u 2 + hB.
(2.12)

The left-hand side of (2.9) does not include H explicitly, and it is identical to this obtained for the horizontal, noninclined surface. However, it depends on a, which is a function of H(x). As a result, the eigenvalues and the eigenvectors are also identical to those obtained for the noninclined surface but again for a = a(x). An additional difference between the systems of equations is the presence of the source term in the momentum equation of the inclined surface. We note that when dH dx ≙ 0, Eq. (2.9) become a standard formulation of the noninclined two-layer system. Another simple case is for dH dx ≙ x 0 h 0 tan θ. This case will be discussed in detail later.

A. Initial and boundary conditions

The initial and boundary conditions are u = 0, h = 1 at t = 0 in the lock 0 ≤ x ≤ 1 and u = 0 at the backwall x = 0. To obtain realistic gravity current solutions, the system must be subjected to a boundary condition at the nose x = xN(t). The justificatio is provided by analogy to the horizontal noninclined dam-break problem. 19,30 Indeed, the dam-break activates the characteristics of the hyperbolic system. The forward-moving characteristics intersect and form a jump. The control-volume analysis about this thin jump is dominated by the volume flu and flow-forc on the vertical planes and is not affected by the inclination of the bottom (assuming a nonlarge |tan θ|). Consequently, the instantaneous jump condition for the nose is like in the horizontal case. 4 In dimensionless form, this reads

uN ≙ 1 R 1/2 Fr(aN)h 1/2 N , (2.13)
where aN = hN/H(xN) and Fr(aN) is the Froude number function, define by

Fr(aN) ≙ √ (2 -a)(1 -a) 1 + a . ( 2.14)

B. Critical nose region

The flui cannot travel faster than the perturbation (characteristic) that sustains the motion, i.e., uN ≤ λ+. The critical behavior occurs when uN = ucrit = λ+, and in general, the propagation is subcritical with hN ≤ hcrit and uN ≤ ucrit. The critical conditions are obtained by the analysis as used for 2L non-Boussinesq currents propagating in noninclined containers [see Ref. [START_REF] Ungarish | Two-layer shallow-water dam-break solutions for non-Boussinesq gravity currents in a wide range of fractional depth[END_REF]Eq. (3.19)]. The analysis is valid here, in particular, because as we already mentioned above, the eigenvalues and eigenvectors for the inclined or partially inclined problems are formally identical to those obtained for the noninclined container for a = a(x). The result is

hcrit ≙ 0.3473H(xN); ucrit ≙ 0.5273 √ H(xN) √ R . (2.15)
The difference with the horizontal case is the fact that H(x) varies. This implies that ucrit increases in a down-slope motion. In this configuration the critical conditions are important because the current tends to concentrate behind the nose.

C. Critical angles of validity and viscosity effects

The critical angles for the validity of the model depend on the transition of the dynamics from upslope current to an impact/splash (e.g., Refs. 13 and 27) for gravity currents flowin upslope. For the downslope currents, it has been shown by Beghin et al. 3 that the front speed continuously varies with the slope angle (ranged between 5 ○ and 90 ○ ). However, Baines 1 showed that for a continuously supplied gravity flow a transition from gravity current to turbulent plume depends on the slope angle and the buoyancy forces. By definition, the shallow water solution as presented here relies on the hydrostatic balance assumption which fails when the slope angle of the current becomes large: for instance, when θ = 30 ○ , the vertical velocity becomes of the same order as the mean stream velocity (factor 1/2). To our knowledge, no corresponding systematic study is available in the literature determining clearly a range of validity of the shallow water approach for increasing slope angles.

For this study, a large Reynolds number is assumed for the shallow water model; the prediction therefore neglects viscosity which exerts a nontrivial effect as the front approaches its maximum height for the upslope current. Marleau et al. 21 reported that viscous effects can be important in the last stage of the propagation of the upslope current on the slope when the current becomes thin. However, drag coefficien is also highly related to the Reynolds number. For a downslope flow the bottom friction is often neglected for a high Reynolds number. In a viscous boundary layer, C d is inversely proportional to Reynolds numbers as is also shown by Cenedese and Whitehead. 7 In Cenedese and Whitehead, the drag coefficien C d increases with the inverse of Re define from the peak velocity of the gravity current. For a wall jet (that has a velocity profil similar to a gravity current) of Reynolds number larger than 1000, C d is smaller than 5 × 10 -3 . 12 For a turbulent boundary layer, C d is given by the empirical relation

C d ≈ 0.0113, Re -0,178 ≈ 3 × 10 -3 , obtained from the classical relation C d ≙ 0.027/Re 1/7 x with x ≙ δRe 1/5
x /0.37, which is close to the bottom drag coefficien for a wall jet at the same Reynolds number.

III. FINITE-DIFFERENCE RESULTS

The solution of the equations must be obtained numerically. Since for the classical noninclined containers, efficien solutions were obtained with a two-step Lax-Wendroff method (see Ref. 6), we attempted an extension which incorporates the contributions of the slope of the container. Here, we use a two-step Lax-Wendroff finite difference method to calculate by time-marching from given initial conditions the height h(x, t), the velocity u(x, t), and the distance of propagation xN(t) of the current from the system of equations [(2.9) and (2.13)].

The present work is limited to a linear-inclined bottom for which in dimensionless form, H(x) can be represented by

H(x) ≙ ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ H 0 , 0 ≤ x ≤ X 1 , H 0 + (x -X 1 ) ⋅ tan θ ⋅ x 0 h 0 , X 1 < x ≤ xN. (3.1)
And therefore,

dH dx ≙ ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ 0, 0 ≤ x ≤ X 1 , tan θ ⋅ x 0 h 0 , X 1 < x ≤ xN. (3.2)
The free input parameters of the problem are (1) the density ratio R ≙ ρa ρc , (2) the height of the container nonslope part H 0 , (3) the length X 1 where the slope starts, (4) the sloping angle θ, and ( 5) the ratio between the initial height and length x 0 /h 0 . We note that X 1 is a non-negative value. The case X 1 = 0 reproduces a fully inclined bottom; the case X 1 = ∞ describes the standard noninclined configuration The present model covers two different configurations down slope with θ > 0 and increasing function H(x) (for x > X 1 ) and up slope with θ < 0 and decreasing function H(x) (for x > X 1 ). We wish to emphasize that the aspect ratio of the lock, x 0 /h 0 , enters the scaled balances for the inclined current. To be more precise, the scaled influenc of the slope is ∝(x 0 /h 0 )tan θ. The interpretation is geometric. When the nose propagates to x 0 , the vertical displacement is Δz = x 0 tan θ. The ratio Δz/h 0 is an estimate of the change of pressure driving force excess relatively to the horizontal motion.

The SW results displayed here were obtained with, typically, 200 grid points in the [0, xN] interval and time step of 1 × 10 -3 . (Convergence was tested also on fine grids.) We note that the numerical computation requires insignifican computer time and memory on a laptop.

For simplicity of analysis and interpretation, the results presented here are for Boussinesq systems, R = 1.

A. Downslope case, θ > 0

The system configuratio for this case is shown in Fig. 1.

1. The effect of the slope location X 1 Some results obtained for the θ = 10 ○ ; R = 1; H 0 = 1.2; x 0 /h 0 = 1 and various locations of the slope start position X 1 = 0, 0.5, 1, 2 are shown in Figs. 2345. We analyze the behavior of the current during the short times (t ≤ 2.5) until the back-moving perturbation approaches the left wall. We observe some wiggles in the numerical solution, which is a spurious by-product of the truncation errors (numerical diffusion and dispersion, see the work of Morton and Mayers 24 ) and has a negligible influenc on the accuracy of the solution at other points. As expected, as X 1 increases, the inclined bottom starts "later," so the current propagates slower. We note that for early times, the behavior of the currents in containers with X 1 = 2 and X 1 = 3 and θ = 10 ○ is identical to this obtained for the horizontal noninclined system with θ = 0 ○ . We speculate that the reason of such propagation is that during early stages, the current still "does not know" that the bottom is inclined because the back-moving front approaches the left wall before the current nose approaches X 1 . For X 1 < 2, however, the situation is different and the current is slightly faster than the one propagating in the horizontal case. Moreover, as expected, as X 1 decreases (until 0), the speed of propagation of the current increases. Figure 6 shows the distance of propagation of the current for various values of X 1 . Other parameters are as in Fig. 5.

FIG. 6.

Distance of propagation of the current for various locations of the sloping start positions X 1 = 0, 0.5, 1, 2 in the downslope case. Other parameters are as in Fig. 2. The lines for the noninclined container and for X 1 = 2 coincide.

An additional interesting effect is the behavior of the height h at around x ≈ X 1 . Usually, in the noninclined containers, at the beginning of the motion, the height of the current h is constant and equals to 1 in some area 0 ≤ x ≤ xc(t). This area decreases with time and disappears when the left-moving perturbation approaches the left wall. However, in inclined or bottom containers, the height of the current might not be constant already during the firs stages of propagation. The perturbation starts at the location which is very close to the beginning of the slope X 1 and is spreading to the left direction.

The firs stage of propagation of the current moving in the noninclined bottom case is the so-called "slumping" stage during which the height hN and the speed uN of the current nose are constant (for a significan period of time).

The behavior of the currents in the inclined bottom case, however, is different and depends on the position of the slope. Thus, for X 1 < 2, the speed of the nose uN increases from the beginning until the left-moving perturbation approaches the left wall by a moderate value of about 5%. The nose height hN also increases but much more dramatically by a rate of about 30% for X 1 = 0. The rate of increasing becomes more moderate as the position of slope, X 1 , moving right and finall in containers with bottom-slope starting at X 1 ≥ 2, hN, remains constant.

The effect of the slope angle θ

Results obtained for θ = 15 ○ (as before, H 0 = 1.2, R = 1, X 1 = 1) are shown in Fig. 7. In general, as expected, the current propagates faster than the corresponding θ = 10 ○ case since the increase in the slope accelerates the velocity of propagation. However, quantitatively, while θ increases by 50% (from 10 ○ to 15 ○ ), the height hN and the speed uN of the nose increase by few percents only.

The effect of the container height H(x) and spreading at the large times

Above we discussed the propagation of the current in containers with the height ratio H 0 close to 1. Here, we discuss the behavior of the currents in a deep-height container with H 0 = 3. In particular, our interest is the form of the currents obtained at the progressive times and their difference from those obtained in Sec. III A 1 and III A 2. Figure 8 shows the behavior of the current in the container with θ = 10 ○ ; X 1 = 1; H 0 = 3 during its propagation to progressive times t = 0.5-10.5. The initial stage of spreading is similar to that shown for H = 1.2 in Fig. 4. Then, after the leading left-moving edge approaches the left wall, the current continues to propagate during a transient stage to the fina stage. During the last stage, the height of the nose increases and the current has a thin tail which decreases with time. The most volume of the current is concentrated in the domain of the head. However, the behavior of the nose is peculiar: the front remains almost at constant height hN and speed uN. Indeed, Fig. 8 shows that from t ≈ 5.5 until ≈10.5, the height of the nose hN is close to ≈0.66 and its speed uN is close to ≈1.

Similar behavior was observed for θ = 15 ○ (see Fig. 9). During the last propagation stage, the height and the velocity of the nose are almost constant; however, the value of hN is greater by about 30% when compared to the one for θ = 10 ○ , while the velocity of the nose in both cases is very close to 1 and differs by less than 10%.

B. Upslope bottom, θ < 0

The system configuratio for this case is shown in Fig. 10. Gravity currents propagate up on the slope and are expected to approach the maximal distance of propagation xN max at height Zmax at some time tstop and to stop. Figure 11 shows results obtained for H 0 = 3.0; R = 1; X 1 = 1; x 0 /h 0 = 1. In Fig. 11

IV. COMPARISON WITH EXPERIMENTS

A. Upslope flow

We made comparisons with the recent experiments of Ref. 21. The system was Boussinesq of salt water in fresh water. Currents were released from horizontal locks, propagated on the horizontal bottom for a while (in the classical slumping phase), and then climbed on slopes of 14 ○ -49 ○ . During the upslope motion, uN decelerates and stops at the maximal height Zmax (measured from the bottom). The measured Zmax/h 0 increases slightly with H(0) (the height ratio of the channel to the lock). The SW equations reproduce well these observations: constant uN up to the beginning of the slope at X 1 than continuous deceleration to uN = 0.

Figure 12 shows a comparison between the SW prediction and experimental data for (a) H(0) = 1.33 and (b) H(0) = 2.0. We think that the agreement is good. The SW results overpredict the length of propagation by less than 10%. This type of discrepancy has been reported also for currents in horizontal propagation (e.g., Refs. 26, 19, and 30). This can be attributed to viscous friction at the bottom, which is expected to be more pronounced in domains with decelerated fluid An interesting observation of Ref. 21 is that the GC on the up-slope domain maintains a nearly self-similar shape during propagation. This observation is compared with the predictions of the SW model in Fig. 13. There is fair agreement. The discrepancies can be attributed to (1) the angle θ is large and (2) during the upslope motion, the speed decreases and the effect of viscous forces increases.

If the up-slope bottom is truncated by an abrupt descent before the point of uN = 0, a part of the dense flui will be drained over this edge (top), and the other part will develop reverse flow This effect, called overtopping in geophysical applications, is governed by a free critical u = (g ′ h) 1/2 condition at the edge, resembling the drainage of a reservoir discussed in Ref. [START_REF] Momen | Inertial gravity currents produced by flui drainage from an edge[END_REF]. The truncated upslope configuratio is out of the scope of the present study, and the interested reader is referred to Ref. 14 (note that the non-Boussinesq ρa/ρc = 0 case is considered there).

The observed agreement/disagreement between the model and experiments is the same as in classical horizontal configuration considered in the literature, e.g., Refs. 26, 17, 19, and 30. The conclusion is that the SW theory is a valuable approximation for calculating the propagation of the current in a configuratio with an up-slope.

B. Downslope case

The downslope current turns out to be a more challenging topic. For clarifications we performed comparisons with the experiments listed in Table I. The system was of salt solution in fresh water, in a tank of about 250 cm long and 60 cm height. These experiments cover a range of θ and aspect ratio of x 0 /h 0 , mostly in the Boussinesq domain; the last three experiments in the table are in the slightly non-Boussinesq domain ρc/ρa ≈ 1.17 (attained with sodium chloride solution in fresh water).

Figure 14 shows the data of xN vs t for the Boussinesq experiments, in the dimensionless form. The cases with θ ∈ [5.9 ○ , 9 ○ ] tend A closer inspection reveals an essential qualitative discrepancy: the experimental speed of propagation uN has an accelerationdeceleration pattern, while the SW uN lacks the deceleration phase. This indicates that a physical effect is missing in the SW modeling of the downstream current. The plausible candidates are entrainment and drag.

SWE model with entrainment and drag

The question is why are the entrainment and drag necessary in the downslope configuratio while fairly negligible in the upstream case. Our explanation is as follows. There is solid evidence that the entrainment effect is associated with an interfacial instability. 18,25 The relevant parameter is the Richardson number which is approximated by the "bulk" value Ri ≙ g ′ h * /(u * ) 2 (the asterisk denotes FIG. 14. x N vs t experimental data for Boussinesq downslope configurations M1, M2, M3, D1, D2, D3 of Table I. dimensional variables). For Ri > Ricrit ≈ 0.5, the interface is expected to be stable, but for smaller values of Ri, Kelvin-Helmholtz vortices appear, causing both entrainment/mixing of ambient flui into the current and drag. In the horizontal flow Ri ≈ 1/Fr 2 ∼ 1. In the up-slope flow u decreases during propagation, and hence, Ri increases. Consequently, the SW solution with no entrainment is a fair approximation to these flows

The downslope flo is different. The speed of the nose uN increases, while h in the tail behind is bound to decrease because of volume continuity, as shown in Figs. 8 and9. Small values of Ri are bound to appear after a modest downslope propagation (5 lock lengths, say). The simple SW equations, which assume a sharp stable smooth interface, become invalid. We therefore apply an extension.

We employ the model suggested by Ref. [START_REF] Johnson | Entraining gravity currents[END_REF]. The entrainment of the upper flui into the current is represented by the flu (speed) We(x, t) = E|u(x, t)|, where E is the entrainment coefficien given by the empirical formula

E ≙ E 0 1 + ψRi , ( 4.1)
where E 0 = 0.078 and ψ = 27. The entrainment is accompanied by a drag term C d u|u|, where the drag coefficien is a constant of the order 0.1 when Ri < 1 and zero otherwise. To proceed, we introduce additional simplifications the system is Boussinesq, and the current is deep. Also, the entrained flui is rapidly mixed across the thickness of the layer so that instead of ρc, the current has the diluted density ρ d (x, t) < ρc; consequently, the effective reduced gravity is g ′ e = (ρ d /ρa -1)g. The equations for the volume of the current, momentum of the current, and mass of the dense component (represented by g ′ e ), in the dimensional form, are

∂h ∂t + ∂ ∂x (uh) ≙ E|u|, ( 4.2)
∂ ∂t (uh) + ∂ ∂x (u 2 h + g ′ e 1 2 h 2 ) -g ′ e h tan θ ≙ -C d u|u|, ( 4.3)
∂g ′ e h ∂t + ∂ ∂x (g ′ e uh) ≙ 0. ( 4.4)
The calculation of g ′ e (x, t) is a part of the problem. In the characteristic form, this becomes

⎡ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎣ h u g ′ e ⎤ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎦ t + ⎡ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎣ u h 0 g ′ e u 1 2 h 0 0 u ⎤ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎦ ⎡ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎣ h u g ′ e ⎤ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎦ x ≙ ⎡ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎢ ⎣ E|u| g ′ e [tan θ -(C d + E) u|u| g ′ e h ] -g ′ e E |u| h ⎤ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎥ ⎦ . (4.5)
The system is hyperbolic. The relevant eigenvalues are

c± ≙ u ± √ hg ′ e , λ 3 ≙ u. (4.6)
The presence of the source terms on the RHS of (4.5) introduces a complex dependency on t along the c± characteristics, which defie clear-cut conclusions. The third characteristic is decoupled: along dx/dt = u, d(g ′ e ) = -g ′ e E|u|dt/h. The RHS term of the momentum equation merits attention. Assuming u > 0, we rewrite u|u|/(g ′ e h) = 1/Ri, and hence, the

FIG. 15.
x N vs t in the downslope configuration of experiment M1 (θ = 5.9 ○ ). SW solution (solid line) and experimental data (dots).

forcing term is ∝[tan θ -(C d + E)/Ri].
The insight is that drag and entrainment combine to oppose the downslope reduced gravity acceleration, and the magnitude of the opposition increases when Ri decreases. In other words, the effect of Ri is twofold: it controls the appearance of the significan entrainment and drag coefficient due to interface instability, but also attempts to slow-down the motion and stabilize it (a smaller u means a larger Ri). The presence of such a complex mechanism in our simple model must be treated with care and subject to further verification The front condition is uN ≙ Fr(g ′ eN hN) 1/2 . The usual Fr(a) can be used when θ, E, and C d are small. This is justifie by estimating the contribution of those effects in the control-volume derivation of Fr. Due to the entrainment, g ′ e decreases and h increases; therefore, the slow-down of uN due to entrainment may be small even during a significan dilution of g ′ e . This set of equations, supplemented by the closure (4.1), is referred to as the SW extended (SWE) model.

The standard SW formulation is given by E = C d = 0, with the front condition uN ≙ Fr(a)(g ′ hN) 1/2 , where Fr is given by HS or Benjamin's equation. The characteristics are

du ≙ ∓2 d(g ′ h) 1/2 + g ′ tan θ dt, on dx dt ≙ c± ≙ u ± (g ′ h) 1/2 . (4.7)
The finite-differenc solutions of the one-layer model are similar to those of the two-layer model when the depth ratio H is larger than 1.5, approximately. The results show (e.g., Fig. 8) that the simple SW current accelerates during the downslope flo and forms a prominent head followed by a thin tail. uN attains a maximum of about 0.8(g ′ h 0 ) 1/2 and then maintains this speed within small oscillations. Inspection of the characteristics indicates that the current cannot decelerate. Consider the behavior of Ri = g ′ h/u 2 . The value near the nose is about 1/Fr 2 ≈ 0.8. However, in the tail, h is small due to the spread-out of the fixe volume, and small values of Ri appear.

The experiments (see Refs. 22 and 8 and others cited within) confir the initial acceleration and formation of the head-tail shape. However, the realistic current, after attaining a maximum speed of about 0.8(g ′ h 0 ) 1/2 , enters into a phase of deceleration. When the deceleration appears the ratio of inertial to viscous effects is still large, and hence, this slow-down effect must be attributed to the appearance of entrainment and drag.

To model this behavior, the authors of Ref. 3 developed a momentum-integral analysis for the propagation, assuming that the motion is governed by a head of self-similar shape that contains a fixe amount of the buoyancy, counteracted by entrainment and drag with constant coefficients The result is, in the dimensional form,

xN ≙ ξ 0 + K(g ′ h 0 x 0 ) 1/3 (t + τ 0 ) 2/3 , (4.8)
where ξ 0 , τ 0 are adjustable constants and the dimensionless K is given by a formula which contains E, C d and some adjustable shapefactors. Here, g ′ is the value in the lock. We refer to (4.8) as the power-law model. This curve has been fitte well to various experimental data (e.g., Refs. 22 and 8). The qualitative insight is useful: the downslope current with entrainment and drag displays, after a while, xN ∼ t 2/3 like a standard horizontal CG in the self-similar stage. However, this is a not a reliable prediction tool because (1) the fact that no front condition can be applied and the assumptions of a selfsimilar head and constant E, C d lack theoretical justificatio and (2) adjustable constants are necessary. In particular, the value K in the experiments (≈2.7) differs significantl from theoretical evaluations.

(3) Moreover, this model is relevant only during the deceleration stage. This bring us to the suggestion that the SWE model is a more efficien tool. The disadvantage is that the solution must be calculated numerically. The advantage is that the SWE model is valid for both the acceleration and deceleration stages. The question is if we can achieve accurate predictions without adjustable parameters. The tests performed here provide support to the suggestion.

Figure 16 illustrates the SWE predictions for configuratio D3 of Table I (θ = 9 ○ ). The dilution is represented by α = g ′ e /g ′ given in the third panel. We see that the shape h(x) is triangular, and the most significan dilution occurs in the tail, while the buoyancy of the domain behind the nose decreases more slowly (to about 60% at t = 40). This is consistent with the observations in the experiments, but a quantitative comparison cannot be performed with the available data. The bulk Richardson number Ri decreases during the propagation, and this sustains the deceleration effect.

The available experimental data allow for a detailed comparison for the propagation. In Fig. 17

= C d = 0
) is in fair agreement with the measurements during some distance of propagation and then overestimates. The SWE model reproduces well the observed acceleration-deceleration pattern. According to this model, the volume increase due to entrainment is 7% at t = 10, 25% at t = 10, and 56% at t = 30. The predicted profile of h, u, and α = g ′ e /g ′ make sense. Qualitatively, they are in agreement with experimental observations, but a qualitative comparison is not possible because of the lack of dedicated data.

Figures 18192021show comparisons of propagation for the other configuration listed in Table I. We note that the overall agreement for the Boussinesq systems is fair. We must keep in mind that in general SW predictions (even for the simplest horizontal lock-release problem) deviate by 10%-20% from data. In the downslope config uration, there is big sensitivity to the initial conditions because they may affect the instability of the interface. Indeed, the authors of Ref. 22 reported "differences in velocity history for similar initial parameter values" (see Fig. 5 in that paper). Consequently, some of the discrepancies may be attributed to the fact that laboratory experiments contain a built-in uncertainty concerning the Richardson number. The non-Boussinesq experiments show, systematically, a delay in the initial propagation. However, the subsequent xN(t) displays the same behavior as in the Boussinesq case. This delay requires further investigation. The top of the tank was open to the atmosphere, and in non-Boussinesq systems, this introduces differences with the fixed-to assumed by the theory.

We argue that the extended SW model performs well. We admit that the entrainment and drag components lack rigor. However, we claim that our model is more advantageous as compared to the widely used model of Ref. 3. The firs advantage is practical: the SWE model (1) predicts the propagation of the current from given initial conditions without the need for adjustments of constants [the entrainment and drag functions are "off the shelf," and the same (for the parameters tested in this paper, at least)] and ( 2) is valid for both the acceleration and deceleration phases. The power-law model needs adjustable ξ 0 , τ 0 which depend on θ, g ′ , and x 0 /h 0 ; then, it applies only to the deceleration phase, starting at some t 1 which must also be determined empirically. The second advantage is conceptual: the downslope gravity current is the same flow-fie manifestation like the counterparts on a horizontal bottom or upslope bottom, and the difference is a clear-cut result of the internal Ri(x, t). The power-law model pictures the downslope current as a semicircular patch which has no counterpart in the accepted theory for the FIG. 18. x N vs t for downslope configuration M2 (θ = 10.6 ○ ). Note the short propagation because this experiment was with long x 0 = 20 cm.

FIG. 19.

x N vs t for downslope configuration M3 (θ = 10.6 ○ ). Note the long propagation because this experiment was with short x 0 = 5.5 cm.

horizontal gravity current (xN ∼ t 2/3 for large t is just a coincidence). The third advantage is concerned with the internal structure of the flow-fiel the SWE model provides h, u, g ′ e /g ′ , and Ri as functions of x, t. Although these are depth-averaged results not accurate pointwise values, they are expected to provide insights into the distribution of the momentum and mixing along the current.

The formal major advantage of the power-law model is the analytical simplicity of the xN(t) formula. However, this is an illusion because this formula cannot be used without experimental measurements of xN(t), and hence, the formula is more postprocessor than a predictor. Moreover, the finite-differenc solution of the SWE hyperbolic system for h, u, g ′ e as functions of x, t is nowadays a quick computation on a laptop computer. To summarize, we think that the analysis of the downslope current should be based on the SWE models (with possible modifi cations) and the power-law model can be dismissed with due credit for it being the backbone of numerous published studies.

V. CONCLUDING REMARKS

We have revisited the problem of a gravity current of fixe volume released from a lock, which then encounters a downslope or upslope bottom, in the inertial-buoyancy regime. The analysis uses the shallow-water (SW) approximation. The system of equations is hyperbolic, and a Froude-number jump condition is applied at the nose (front).

The obvious parameter of the problem is the slope angle, θ. However, we elucidated that the propagation of the current is affected by additional parameters: the aspect ratio of the lock x 0 /h 0 , the height ratio of the ambient to lock, H/h 0 , and the distance of the gate from the beginning of the slope. The SW model provides qualitative insights and quantitative data concerning the influenc of these parameters.

We performed comparisons of the theoretical results with previously published experimental data. For the up-slope current, the agreement is satisfactory: both the model and experiment show that the current decelerates up to a point where it stops uN = 0; the SW predictions slightly overestimate the maximum height.

The down-slope current system displays a different pattern. The SW results indicate that the current accelerates and then uN attains a constant value, ≈ (g ′ h 0 ) 1/2 . In experiments, the current firs accelerates and then decelerates. We showed that this can be attributed to the behavior of the Richardson number Ri: during the acceleration, Ri decreases, and eventually, an instability develops at the interface which produces entrainment/mixing and drag. We demonstrated that when these effects are added to the simple shallow-water balances (using an off-the-shelf closure for the entrainment coefficien and a constant drag coefficient) the shallow water extended model (SWE) indeed predicts an acceleratingdecelerating downslope which is in good agreement with previously published experimental data.

We think that, overall, this work improves the understanding and modeling of gravity currents. In particular, we demonstrate that the fact that Ri increases in the up-slope case and decreases in the down-slope case is the reason why simple SW formulation works well in the firs case but needs entrainment and drag extension in the second case. In our opinion, the extended SW model presented in this work is an efficien replacement to the widely used power-law xN ≙ ξ 0 + K(g ′ h 0 x 0 ) 1/3 (t + τ 0 ) 2/3 (dimensional) model of Ref. 3 because the latter model (1) uses adjustable constants ξ 0 , τ 0 , K and (2) applies only to the deceleration stage. More investigation is still needed to further assess the accuracy of the entrainment and drag closures needed in the extended SW model. This requires careful comparisons with more experimental data. Additional interesting direction is the study by Navier-Stokes simulation which might point out details of the motion (see the work of Qu 29 ) and must be left for future work.

FIG. 2 .FIG. 4 .FIG. 5 .

 245 FIG. 2. SW model results for the down-slope bottom case:(a) h and (b) u as functions of x at various t = 0.4(0.2)2.0. Here, θ = 10 ○ ; X 1 = 0; H 0 = 1.2; x 0 /h 0 = 1.

FIG. 7 .FIG. 8 .FIG. 9 .FIG. 10 .FIG. 11 .

 7891011 FIG. 7. SW model results in the downslope case: (a) h and (b) u as functions of x at various t = 0.4(0.2)1.8. Here, θ = 15 ○ ; X 1 = 1; H 0 = 1.2.

  (a), the maximal distance approached by the current is plotted as function of |θ|: the current propagates to longer distances as |θ| decreases and stops already at the beginning of the slope for quite large values of |θ| (|θ| ≥ 70). The maximal height approached by the current is also shown in Fig. 11(b): first the height increases with |θ|, and for |θ| ≈ 20 ○ , it approaches its maximum Zmax ≈ 1.2. Larger values of |θ| do not change this maximum of Zmax.

FIG. 12 .FIG. 13 .

 1213 FIG. 12.Comparison of maximal distance of propagation in the upslope case as a function of slope S = tan(-θ): SW numerical solution (solid line) and experimental results (dashed line) for (a) H 0 = 1.33 and (b) H 0 = 2.

  the same curve. Some data cover short propagation (xN ≈ 12), and some cover long propagation xN ≈ 42. The reason is the limitation of the experimental tank. The available run of the slope was L ≈ 240 cm, and hence, the maximum dimensionless xN is fixe by L/x 0 . In general, the curves show a significan deceleration of the current starting at xN ≈ 8-10 (the θ = 2 ○ case displays the strongest deceleration).A comparison of the SW results with the experimental data shows agreement for short propagation only, roughly xN < 5-10; afterward, the experimental xN(t) is significantl smaller. A typical result is shown in Fig.15.

FIG. 16 .

 16 FIG. 16. SWE predictions for the downslope configuration D3 (θ = 9 ○ ). Profiles of (a) h, (b) u, (c) α = g ′ e/g ′ and (d) Ri as functions of x at various times t = 2, 4, . . ., 40.

FIG. 17 .

 17 FIG. 17.x N vs t: experimental data and predictions of SW standard (E = C d = 0) and SWE models. Downslope configuration D3 (θ = 9 ○ ).

FIG. 20 .

 20 FIG. 20.x N vs t for downslope configurations D1 and Dnb1 (2 ○ ).

FIG

  FIG.x N vs t for downslope configurations (a) D2 and Dnb2 (6 ○ ) and (b) D3 and Dnb3 (9 ○ ).

TABLE I .

 I List of downslope experiments used for comparison. M denotes Ref. 22, D denotes Ref. 8, and Dnb denotes Ref. 9. The figure number in the appropriate paper is given in Remark. The units are cgs.

	Label	θ	x 0	h 0	x 0 /h 0	g ′	Remark
	M1 M2 M3 D1 D2 D3 Dnb1 Dnb2 Dnb3	5.9 10.6 10.6 2 6 9 2 6 9	5.5 20.01 5.5 10 10 10 10 10 10	2.5 9.7 9.7 8 8 8 8 8 8	2.2 2.06 0.67 1.25 1.25 1.25 1.25 1.25 1.	78.7 11.58 99.57 17.02 17.11 17.11 167.1 166.7	17 4 12 11 9 4 10 8

  , xN(t) is compared with experimental data reported by Ref. 8. xN(t) of the simple SW model (E 0


Jan Aldert Bergstra
email: j.a.bergstra@uva.nl

Jan Aldert
email: janaldertb@gmail.com

Bergstra Dual

The class of dual number meadows is introduced. By definition this class is a quasivariety. Dual number meadows contain a non-zero element the square of which is zero. These structures are non-involutive and coregular. Some properties of the equational theory of dual number meadows are discussed and an initial algebra specification is given for the minimal dual number meadow of characteristic zero which contains the dual rational numbers. Several open problems are stated.

Introduction

The idea of meadows is to introduce, on top of the signature of fields, a function symbol for inverse or for division and to insist, or prefer, that operations are total. On that basis the equational logic of known as well as novel structures and classes of structures is investigated. We call a datatype arithmetical if it models systems of numbers including well-known operators on numbers. Meadows are arithmetical datatypes which provide inverse or division or both. Within the informal notion of meadow various degrees of freedom still exist. For instance the underlying ring may or may not be commutative, inverse may or may not be an involution.

Md, the equational axiomatisation of (commutative, regular and involutive) meadows, consists of the equations for a Commutative Ring (CR) in Table 1 plus two more axioms concerning inverse: involution and regularity of Table 2. In [START_REF] Bergstra | Meadows and the equational specification of division[END_REF] a meadow is defined as a model of Md. In section 1.2 below, however, we will provide an alternative definition of meadows which serves as a preparation for various useful generalisations of the notion of a meadow.

Regularity in combination with involution ensures that a structure which meets these requirements is the expansion of a (von Neumann) regular ring. A prominent meadow is the meadow Q 0 of rational numbers. Q 0 is an arithmetical datatype, and an initial algebra specification was given for it in [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF], a 1 (x + y) + z = x + (y + z) [START_REF] Anderson | Perspecx Machine VIII, axioms of transreal arithmetic[END_REF] x + y = y + x

(2)

x + 0 = x

x + (-x) = 0 (4)

(x • y) • z = x • (y • z) (5)
x

• y = y • x (6) 1 • x = x (7)
x

• (y + z) = x • y + x • z (8)
Table 1: CR: axioms for a commutative ring (x -1 ) -1 = x (involution)

(x • x) • x -1 = x (regularity) (x -1 • x -1 ) • x = x -1 (coregularity) x = 0 → x • x -1 = 1 (strong regularity)
Table 2: Optional meadow properties paper which initiated work on arithmetical datatypes with multiplicative inverse and/or division.

In this paper we will discuss some structures which come about when introducing a non-zero element for which, like for 0: x • x = 0, i.e. such that • = 0, in the presence of a totalised inverse for multiplication, -1 . Because is nonzero and has no proper inverse (i.e. no y exists such that • y = 1) such structures are rings but not fields.

Preliminaries

Some preliminaries are useful. We will briefly discuss signatures, algebras, datatypes, and abstract datatypes.

Signatures

From the theory of abstract datatypes, (see e.g. [START_REF] Ehrich | Specification of Abstract Data Types[END_REF]), we will use the notion of a signature, that is a collection of one or more names for sorts and zero or more names for constants, with information of the sort to which these belong, plus zero or more names of functions equipped with an arity, i.e. a list of argument sorts and a target sort. In case there is just one sort, the signature is said to be single sorted otherwise it is many-sorted. Different signatures are isomorphic if a bijective renaming transforms the one into the other. Isomorphism classes of signatures are called similarity types, a preferred notion in logic, whereas datatype theory embodies a preference to work with signatures and to be explicit about categories of signatures when needed.

Below we will work with the following single sorted signature of rings Σ R : a single sort named V for values, constant names 0 and 1 and two place functions names • for multiplication and + for addition and a unary functionfor negation. The two place function name -is used as an abbreviation for subtraction x -y = x + (-y).

If Σ is a single sorted signature and M is a structure for that signature then with |M| we denote the domain (alternatively: carrier) of M. Thus if V is the name of the unique sort of Σ then |M| is the interpretation of V that comes with M.

Algebras, datatypes, and arithmetical datatypes

Algebras are combinations of sets and functions. An abstract datatype consists of an algebra and includes a signature which provides a name for each sort, constant, and function. Below we will assume that an algebra is a datatype and thereby is an interpretation of a signature. When considering datatypes that embody conventional number systems and variations thereof we will speak of arithmetical datatypes. An abstract datatype is the isomorphism class of a datatype, though with a fixed signature. A datatype is called minimal if it has no proper substructures.

On the definition of meadows

It has turned out not to be straightforward to develop a useful and flexible terminology about meadows which extends to modified but similar structures. This paper contributes to issues of nomenclature by proposing a uniform policy for defining meadow related classes of arithmetical datatypes. Instead of starting out with an axiomatic definition of meadows (models of CR enriched with an inverse function that satisfies involution and regularity) a model theoretic definition of the class of meadows is more amenable to various generalisations. We will provide the model theoretic definition of meadows and then discuss various related definitions of classes of arithmetical datatypes.

Below we will use t for the interpretation of term t in a structure if it is clear from the context which structure is meant. Otherwise, when more detail is required, t A denotes the interpretation of t in A. Moreover, we will use function symbols as well for the interpretation in a model, unless clarity requires further detail.

The signature of meadows Σ Md , by default with inversive notation, consists of the signature of unital rings (Σ R ) extended with a unary function --1 called inverse. A strongly regular meadow A is a field (A| Σ R ) expanded with a function --1 , we interpret --1 , in such a way that 0 -1 = 0 and for all a = 0 ∈ |A|, a• a -1 = 1. We write E srm for the equational theory of the class of all strongly regular meadows.

Definition 1.1. A meadow is a model of E srm .
The idea of this definition is that it expresses that meadows are as close to fields as can be expressed with equational logic under the assumption that the inverse of 0 is 0. It follows from results in [START_REF] Bergstra | Meadows and the equational specification of division[END_REF], as well as from results in [START_REF] Ono | Equational theories and universal theories of fields[END_REF], that the model theoretic definition coincides with the axiomatic definition mentioned above. An advantage of the model theoretic definition compared with the axiomatic definition, however, is that it can be more easily generalised and adapted. Below we will list some examples of generalisations and adaptations.

For more information regarding the equational theory of meadows we refer to [START_REF] Komori | Free algebras over all fields and pseudo-fields[END_REF][START_REF] Ono | Equational theories and universal theories of fields[END_REF][START_REF] Bergstra | The rational numbers as an abstract data type[END_REF][START_REF] Bergstra | Cancellation meadows: a generic basis theorem and some applications[END_REF]. For recent work on the mathematical aspects of zero totalised division we mention [START_REF] Michiwaki | Reality of the division by zero z/0 = 0[END_REF]. Proposition 1.1. A strongly regular meadow is a meadow that satisfies the conditional formula:

x = 0 → x • x -1 = 1.
A strongly regular meadow is called a cancellation meadow in [START_REF] Bergstra | Cancellation meadows: a generic basis theorem and some applications[END_REF] in view of the fact that among meadows it is also characterised by the following cancellation property:

x = 0 ∧ x • y = x • z → y = z.
In the presence of CR the axiom of strong regularity (i.e. equation strong regularity in Table 2) implies regularity (equation regularity in Table 2), and under the additional assumption that 0 -1 = 0 strong regularity also implies coregularity. Not every meadow is strongly regular. For instance the direct sum of non-trivial strongly regular meadows is not strongly regular.

Notational matters. Σ(A) denotes the signature of datatype A. For a signature Σ ⊆ A A| Σ denotes the reduct of A to the signature Σ. We will use constants (e.g. 0, 1 and ) also for the names of corresponding values (interpretations) in an arithmetical datatype. However, if the datatype is fixed, constants equipped with a hat (e.g. 0) always denote the interpretation of the constant, in that given datatype. When a risk of confusion is present, disambiguation by means of a subscript (e.g 1 A instead of 1) indicates that the interpretation of a constant in a certain datatype or sort is meant. Below we will often use the names of functions also as names for interpretations thereof (e.g. 0 + 1 instead of 0 + 1 or of 0 A + A 1 A ).

Variations on the theme of meadows

With a variation on the theme a different but related class of structures is meant. The difference may extend to differences of the underlying signature, but also with the same signature a lot of variation is possible. In this section we discuss four known variations of the class of meadows, each of which make use of the same signature of meadows, in some cases using new constants as appealing notations for existing terms.

Formally real meadow.

A structure which satisfies all equations that are true in all strongly regular meadows which are expansions of formally real fields is a formally real meadow. We refer to [START_REF] Bergstra | Equations for formally real meadows[END_REF] for further information on formally real meadows.

Skew meadow. Let a strongly regular skew meadow A be defined as a skew field (A| Σ R ) expanded with a function --1 , where the interpretation of --1 , is such that 0 -1 = 0 and for all a = 0 ∈ |A|, a• a -1 = 1. Now let E srsm be the equational theory of the class of strongly regular skew meadows, then a skew meadow is defined as a model of E srsm .

It is an unfortunate aspect of the terminology that a non-commutative skew meadow is not a meadow. We think that a flexible terminology about meadows is in need of such flexibility, however.

Common meadow. Common meadows, see [START_REF] Bergstra | Division by zero in common meadows[END_REF] can be defined as the structures which satisfy all equations true in expansions of an extension of a field with an additional element a which represents an element propagating through each operation (x + a = x • a = -a = a). Such an element is often denoted with ⊥ in work on abstract datatypes where it is considered an error element. In the terminology of transmathematics such an element, which must be unique, is called absorptive and the preferred notation for it is Φ.

Such structures with an absorptive element (say a) are expanded with a multiplicative inverse made total by setting 0 -1 = a. Upon adopting this model theoretic definition of common meadows the results of [START_REF] Bergstra | Division by zero in common meadows[END_REF] provide an alternative equational and axiomatic definition of common meadows under the additional constraint that the characteristic is zero.

Non-involutive meadow. Non-involutive meadows (see [START_REF] Bergstra | Division by zero in non-involutive meadows[END_REF] ) can be defined as models of the equational theory class of expansions of fields expanded with an inverse operation which has been made total by taking 0 -1 = f for some element of f of the field which may not be zero. A choice with some moderate popularity is f = 1.

Dual numbers

Dual numbers, as designed by William Clifford in 1873, constitute a ring extension of a field with a nilpotent element that is characterised by • = 0. For an introduction to dual numbers we refer to [START_REF] Veldkamp | On the use of dual numbers, vectors and matrices in instantaneous spatial kinematics[END_REF] and [START_REF] Brodsky | Dual numbers representation of rigid body dynamics[END_REF]. In the setting of dual numbers, like in Q 0 , the inverse, can be made total by requiring 1/0 = 0.

We will turn a dual field into a so-called dual number meadow by introducing a new constant to the signature and a name for the inverse function which is made total by taking value 0 in case the inverse in the dual field is undefined. We will provide an algebraic specification of the dual number meadow Q dn 0 . The result is a straightforward adaptation of the initial algebra specification of Q 0 as given in [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF].

Strongly regular dual number meadows

Let Σ Md,V, be the signature of meadows with sort name V and enriched with a constant . Consider a strongly regular meadow M 0 . We will construct a strongly regular dual number meadow M dn 0 based on M 0 . The carrier V dn of M dn 0 consists of the objects (a, b) for a, b ∈ |M 0 |. The interpretation of constants and functions is as follows, where 0, 1, + , • , -, , and -1 are taken from M 0 :

• 0 = (0, 0), • 1 = (1, 0), • ˆ = (0, 1), • -(a, b) = (-a, -b), • (a, b) + (c, d) = (a + c, b + d), • (a, b)• (d, e) = (a • d, a • e + b • d), • (a, b) -1 = (a -1 , -b • (a • a) -1 ).
Definition 2.1. For a strongly regular meadow M, M dn 0 is a strongly regular dual number meadow, and moreover, any structure isomorphic to a structure of the form M dn 0 is a strongly regular dual number meadow.

As a consequence, up to isomorphism, all strongly regular dual number meadows result from this construction. Examples of strongly regular dual number meadows are Q dn 0 , R dn 0 and C dn 0 . We notice that the elements of the form (a, 0) for a ∈ |M 0 | constitute a substructure which is an isomorphic copy of M 0 . Below we will identify (a, 0) with a. We will also write M 0 ⊕ • M 0 for M dn 0 in order to highlight the construction of its domain.

When reasoning in an arithmetical datatype of the form M 0 ⊕ • M 0 for some strongly regular meadow M 0 , rather than working formally on the basis of axioms, we will use functions re(-) and dual(-), both not mentioned in the signature, so that when x = (a, b), re(x) = a and and dual(x) = b. These functions play a similar role to re(-) and im(-) in the case of complex numbers.

When x = (a, b), upon identification of (a, 0) with a we may write x = re(x) + • dual(x) = a + • b. For ease of notation, in proofs we will frequently use a and b as abbreviations for re(x) and dual(x) respectively.

Proposition 2.1. (0, b) -1 = (0, 0). Proof. (0,b) -1 = (0 -1 , -b • (0 • 0) -1 ) = (0, -b • 0 -1 ) = (0, -b • 0) = (0, 0).

Dual number meadows

The class of dual number meadows with zero-totalised inverse is defined as follows:

Let K dn be the class of Σ Md,V, structures of the form M dn 0 as defined in Paragraph 2 with M 0 a strongly regular meadow. Eq srdnm is the equational theory of K dn . CEq srdnm is the conditional equational theory of K dn , i.e. the set of conditional equations true in all structures in K dn .

In Proposition 2.2 below it is shown that the conditional theory of strongly regular dual number meadows is stronger than the equational theory of that class.

Proposition 2.2. The conditional equation • x = 0 → x -1 = 0 (totalisation axiom of Table 4) is valid in all strongly regular dual number meadows while it is not a consequence of Eq srdnm .

Proof. We write Ψ t ≡ • x = 0 → x -1 = 0 for the totalisation axiom. If totalisation is a consequence of Eq srdnm then for some finite subset of it, say E t ⊆ E srdnm , Eq t |= Ψ t . Let Q 0, be the expansion of Q 0 with a constant which is made equal to 0. Now consider Q dn 0 and consider the mapping φ :

Q dn 0 → Q 0, defined by φ(a, b) = a (stated differently: φ( ) = 0). It is easy to verify that φ is a surjective homomorphism. Because homomorphisms preserve equations, Q 0, |= E t and thus by assumption Q 0, |= Ψ t . Now Q 0, |= • x = 0 • x = 0 and it follows that Q 0, |= x -1 =
0 which is not the case. This contradiction implies that Eq srdnm |= Ψ t .

For that reason we define the dual number meadows as the smallest quasivariety which contains all strongly regular dual number meadows.

Properties of strongly regular dual number meadows

Leaving aside the totalised inverse, the properties of structures M dn 0 are wellknown, e.g. see [START_REF] Veldkamp | On the use of dual numbers, vectors and matrices in instantaneous spatial kinematics[END_REF]. In particular structures of the form M dn 0 constitute a unital commutative ring. We will refrain from checking such matters below. Moreover, these structures satisfy the following equations, each of which, except the first, are sensitive to "division by zero".

Although we are working in a model (structure algebra), for ease of notation we will write 0 instead of 0, + instead of + etc. We use (a, b) and (a + • b) as equivalent and interchangeable descriptions of the same entities.

Proposition 2.3. • = 0. Proof. (0, 1) • (0, 1) = (0, 0 • 1 + 1 • 0) = (0, 0). Proposition 2.4. -1 = 0.
Proof. With Proposition 2.1 immediately (0, 1) -1 = (0, 0). Proposition 2.5.

• x = 0 → x -1 = 0.
Proof. With • x = (0, 1) • (re(x), dual(x)) = (0, re(x)) the assumption on x implies re(x) = 0, which implies, given that M 0 is a strongly regular meadow,

x -1 = (re(x), dual(x)) -1 = (0, dual(x)) -1 = (with Proposition 2.1) = 0. Proposition 2.6. (x • y) -1 = x -1 • y -1 . Proof. Let a = re(x), b = dual(x), c = re(y), d = dual(y). Now ((a + • b) • (c + • d)) -1 = (a • c + • (a • d + c • b)) -1 = (a • c -• (a • d + c • b)) • (a • c) -2 = ((a -• b) • (c -• d)) • a -2 • c -2 = (a + • b) -1 • (b + • d) -1 . Proposition 2.7. If re(x) = 0 then x • x -1 = 1. Proof. With a = re(x), b = dual(x): (a, b) • (a, b) -1 = (a, b) • (a -1 , -b • a -2 ) = (a • a -1 , b • a -1 -a • b • a -2 ) = (1, 0) = 1. Proposition 2.8. x • (x -1 • x -1 ) = x -1 . Proof. With a = re(x), b = dual(x): if re(x) = 0 then x -1 = 0 and the result is immediate. Otherwise x • (x -1 • x -1 ) = (x • x -1 ) • x -1 = (with Proposition 2.7) = 1 • x -1 = x -1 . Proposition 2.9. (x + • y) -1 = (x -• y) • x -2 .
Proof. Let a = re(x) and b = dual(x). If a = 0 then re(x + • y) = 0 and with Proposition 2.1 (x + • y) -1 = 0. Moreover x -1 = 0 whence (x -• y) • x -2 = 0. If a = 0 then we write re(y) = c and dual(y) = d.

Now (x + • y) -1 = (a + • (b + y)) -1 = (a + • b + (c + • d))) -1 = (a + • b + • c + • • d)) -1 = (a + • b + • c)) -1 = (a + • (b + c)) -1 = a -1 -• (b + c) • a -2 = (a -• (b + c)) • a -2 .
Next we consider the right hand side of the equation:

(x -• y) • x -2 = (x -• (c + • b)) • x -2 = (x -• c) • x -2 = (a + • (b -c)) • (a + • b) -2 = (a + • (b -c)) • (a -• b) 2 • a -4 = (a + • (b -c)) • (a 2 -• 2 • b • a) • a -4 = (a + • (b -c) • (a -• 2 • b) • a -3 = (a 2 + • a • (b -c -2 • b) • a -3 = (a + • (b -c -2 • b)) • a -2 = (a -• (b + c)) • a -2 . Proposition 2.10. • x = 0 → x • x = 0.
Proof. Let a = re(x) and b = dual(x). Then • x = 0 implies a = 0. Thus

x • x = (a + • b) • (a + • b) = a • a + • (a • b + b • a) = 0. Proposition 2.11. • x = 0 → (x -1 ) -1 = x. Proof. Let a = re(x) and b = dual(x). From • x = 0 it follows that a = 0. Now (x -1 ) -1 = ((a + • b) -1 ) -1 = (a -1 + • (-b) • a -2 ) -1 = (a -1 ) -1 + • -(-b • a -2 ) • (a -1 ) -2 = a + • b • a • a -1 = a + • b = x. Proposition 2.12. (x -1 ) -1 • x -1 = x • x -1 .
Proof. Let a = re(x) and b = dual(x). If a = 0 then x -1 = 0 so both sides vanish. If a = 0 then • x = • a = 0 and Proposition 2.11 applies.

Proposition 2.13. (x -1 ) -1 • x = x • x.
Proof. Let a = re(x) and b = dual(x). If a = 0 then (x -1 ) -1 = 0 and x • x = 0, and the equation holds. If a = 0 then x • = 0 and Proposition 2.11 applies.

Proposition 2.14.

• x = 0 → x • x -1 = 1.
Proof. From •x = 0 it follows that re(x) = 0. Now Proposition 2.7 applies.

Proposition 2.15.

(x + • y) • (x + • y) -1 = x • x -1 .
Proof. If • x = 0 then, by Proposition 2.5, x -1 = 0 and so x • x -1 = 0, moreover • (x + • y) = • x = 0 so that another application of Proposition 2.5 yields the required result. If, on the other hand, • x = 0 then two applications of Proposition 2.14 suffice.

Axioms for dual number meadows

Finding axioms for a class of algebras is a somewhat arbitrary exercise. In the case of dual number meadows it is plausible to require that all axioms are satisfied in all of K as defined above. This aspect amounts to the soundness of the axioms. Whether or not a finite complete set of axioms can be given is another matter (see problem 2.2 above).

In Table 3 some equational axioms for Eq srdnm have been collected. Each of these has been proven valid in all strongly regular dual number meadows. We do not know whether or not these axioms are complete for Eq srdnm .

The conditional equation (called totalisation) of Table 4, which specifies how the inverse is made total in strongly regular dual number meadows, constitutes the only significant conditional axiom which we have found.

import : CR (x • y) -1 = x -1 • y -1 (9) (x -1 ) -1 • x -1 = x • x -1 (10) (x -1 ) -1 • x = x • x (11)
• = 0 (12)

• x • x • x -1 = • x (13)
(x + • y) -1 = (x -• y) • (x -1 • x -1 ) (14)
Table 3: Md dn : equational axioms for a dual number meadow import : CR, Md dn

• x = 0 → x -1 = 0 (totalisation) Table 4: Md dn,t • x = 0 → x • x -1 = 1 Table 5: Dual strong regularity
The totalisation axiom is not true for all weakly totalising dual number meadows. Indeed the variety of weakly totalised dual number meadows contains a quasivariety (model class of the conditional equational theory CEq srdnm ), which better approximates the idea of dual numbers than is possible by means of equations only.

Below some consequences of the axioms will be derived. In these proofs no use is made of re(x) and dual(x). The standard property of a commutative ring that 0 • x = x • 0 = 0 will be used, however, and this fact merits a repetition of its well-known proof: (0 + 0) • x = 0 • x + 0 • x, and thus 0

• x + (-(0 • x)) = (0 • x + 0 • x) + (-(0 • x)) = 0 • x + (0 • x + (-(0 • x)) = 0 • x + 0 = 0 • x.

Some consequences of the axioms

The following consequences can be drawn from the axioms Md dn of Table 3.

Proposition 3.1. x • (x -1 • x -1 ) = x -1 .
Proof. Use axiom 14 of Md d (taking y = 0).

Proposition 3.2. 0 -1 = 0. Proof. In (x + • y) -1 = (x -• y) • (x -1 • x -1 ) (axiom 14) take x = y = 0. Then 0 -1 = 0 • 0 -1 • 0 -1 = 0. Proposition 3.3. 1 -1 = 1.
Proof. In (x -1 ) -1 • x = x • x (axiom 11) take x = 1 and obtain (1

-1 ) -1 = 1. Next in (x + • y) -1 = (x -• y) • (x -1 • x -1 ) take y = 0 and x = x -1 . Thus (x -1 ) -1 = x -1 • (x -1 ) -1 • (x -1 ) -1 . Now, with x = 1, 1 = x -1 • 1 • 1 so that 1 = x -1 . Proposition 3.4. (-1) -1 = -1. Proof. (-1) -1 = (by Proposition 3.1) = (-1) • ((-1) -1 • (-1) -1 ) = (-1) • ((-1) • (-1)) -1 = (-1) • (1) -1 = (-1) • 1 = -1. Proposition 3.5. (-x) -1 = -(x -1 ). Proof. (-x) -1 = ((-1) • x) -1 = (-1) -1 • x -1 = (-1) • x -1 = -(x -1 ). Proposition 3.6. x • y = 1 → y = x -1 . Proof. Assume x • y = 1 and first obtain x -1 • y -1 = 1 -1 = 1. Multiplying both sides with x • x -1 gives x • x -1 • x -1 • y -1 = x • x -1 , so that, with axiom 14 of Md d (taking y = 0), x -1 • y -1 = x • x -1 whence 1 = x • x -1 . Now multiplying both sides of x • y = 1 with x -1 yields x • y • x -1 = x -1
, and with commutativity and associativity of multiplication and 1 = x • x -1 we obtain y = x -1 . Proposition 3.7. ((x -1 ) -1 ) -1 = x -1 .

1(x) = x • x -1 (15) x 2 = x • x ( 16
)
Table 6: DO: axioms for defined operators import : CR, Md dn , DO

1(x 2 1 + x 2 2 + x 2 3 + x 2 4 + 1) = 1 (FR4)
Table 7: Initial algebra specification for rational dual numbers

Proof. ((x -1 ) -1 ) -1 = (with Proposition 3.1, and associativity and commutativity of

• ) = ((x -1 ) -1 ) -1 • ((x -1 ) -1 ) -1 • (x -1 ) -1 = (with axiom 9 of Md dn ) = ((x -1 ) -1 ) -1 • ((x -1 ) -1 • x -1 ) -1 = (with axiom 10 of Md dn ) = ((x -1 ) -1 ) -1 • (x • x -1 ) -1 = ((x -1 ) -1 • x) -1 • (x -1 ) -1 = (with axiom 11 of Md dn ) = (x • x) -1 • (x -1 ) -1 = x -1 • x -1 • (x -1 ) -1 (with axiom 10 of Md dn )= x -1 • x -1 • x = x -1 .
In the presence of dual strong regularity:

Proposition 3.8. • x = 0 → (x -1 ) -1 = x.
Proof. With • x = 0 → x • x -1 = 1 one finds x • x -1 = 1 and after application of inverse to both sides and distribution of inverse over multiplication:

x -1 • (x -1 ) -1 = 1. This implies x • (x -1 • (x -1 ) -1 ) = x • 1 and (x • x -1 ) • (x -1 ) -1 =
x from which one obtains 1 • (x -1 ) -1 = x and the desired identity.

Proposition 3.9.

• x = 0 ∧ • y = 0 → • x • y = 0. Proof. Suppose •x•y = 0 then •x•y•x -1
•y -1 = 0 and thus, with the assumptions on x and y, and strong regularity

•x•y•x -1 •y -1 = •x•x -1 •y•y -1 = •1•1 = = 0,
and thus • x = 0 in contradiction with the assumption on x.

Initial algebra specifications

The dual fracpairs constitute a transversal for Q dn 0 .

Definition 3.1. A dual fracpair is a closed expression of the form p • n -1 + • q • m -1 such that (i) n, m are integer expressions made up from 1 and + only (i.e. n and m represent positive integers), (ii) p, and q are integer expressions of the form 0, k or -k with k a positive integer expression made up from 1 and + only, and (iii) gcd(p, n) = gcd(q, m) = 1.

Proposition 3.10. For positive integer expressions n made up from 1 and

+ CR + Md dn + DO + FR4 n • n -1 = 1.
Proof. Write n as a sum of four squares plus 1 and apply FR4.

The following follows from the construction of Q dn 0 . Proposition 3.11. (i) different dual fracpairs have different interpretations in Q dn 0 and (ii) each element of Q dn 0 is the interpretation of a unique fracpair. Theorem 3.1. The equations of Table 7 constitute a finite equational initial algebra specification of Q dn 0 . Proof. The soundness of the equations is a matter of inspection. To establish that the specification is an initial algebra specification of Q dn 0 it suffices to show that each closed expression is provably equal to a dual fracpair. The proof is done by induction on the structure of expressions. Let t ≡ 1 then

t = 1 • 1 -1 + • 1 • 1 -1 . If t ≡ 0 then t = 0 • 1 -1 + • 0 • 1 -1 . The remaining cases are t ≡ -r, t ≡ r -1 , and t ≡ r + s, t ≡ r • s. Let r = p • n -1 + • q • m -1 then t ≡ -r = -(p•n -1 + •q •m -1 ) = (-p)•n -1 + •(-q)•m -1 = -[p]/n+ •-[q]/m, where -[0] ≡ 0, -[k] ≡ -k, -[-k] ≡ k. For the case = r -1 three subcases on p are distinguished. If p ≡ 0 then t -1 = (0-•q •m -1 )•0 -2 = 0 = 0•1 -1 + •0•1 -1 . If p is positive, say p = k, then t -1 = (k • n -1 + • q • m -1 ) -1 = (k • n -1 -• q • m -1 )•(k •n -1 ) -2 = k •n -1 •(k •n -1 ) -2 + •-[q]•m -1 •(k •n -1 ) -2 . Now k •n -1 •(k • n -1 ) -2 = k • n -1 • k -1 • k -1 • (n -1 ) -1 • (n -1 ) -1 = n -1 • k -1 • (n -1 ) -1 • (n -1 ) -1 = k -1 • n -1 • (n -1 ) -1 • (n -1 ) -1 = k -1 • n -1 • n • (n -1 ) -1 = k -1 • n -1 • n • n = n • k -1 . Next consider -[q] • m -1 • (k • n -1 ) -2 . If q ≡ 0 then r = n • k -1 + 0 • 1 -1 . If q is positive, then -[q] • m -1 • (k • n -1 ) -2 = (-q) • m -1 • k -1 • k -1 • (n -1 ) -1 • (n -1 ) -1 = (-q) • m -1 • k -1 • k -1 • (n -1 ) -1 • (n -1 ) -1 • n • n -1 = (-q) • m -1 • k -1 • k -1 • (n -1 ) -1 • n • n • n -1 = (-q) • m -1 • k -1 • k -1 • n • n = (-a) • b -1
for suitable positive integer expressions a and b with gcd(a, b) = 1, so that r = n • k -1 + (-a) • b -1 . The case that p is negative works similarly, and so do the notationally somewhat more involved cases for addition and multiplication. Following [START_REF] Bergstra | Inversive meadows and divisive meadows[END_REF] Theorem 2, the equation mentioned in Table 8, as a replacement of FR4 of Table 7 also provides an initial algebra specification in the case of Q 0 . That observation extends, eithout complications, to the context of dual rational numbers.

Proposition 3.12. The equations as mentioned Table 8 provide an equational initial algebra specification of Q dn 0 . In [START_REF] Bergstra | Subvarieties of the variety of meadows[END_REF] it is shown that an initial algebra specification of the meadow Q 0 of rationals can be given by adding to the equations Md of meadows a single equation with a single variable. The proof depends on some elementary consequences of Galois theory. This observation leads to the following question. Problem 3.1. Can Q dn 0 be given an initial algebra specification by complementing CR + Md d + DO with a single equation involving a single variable only.

Let FR = {1(X 2 1 + • • • + X 2 n + 1) = 1|n ∈ N + }.
As was shown in [START_REF] Bergstra | Equations for formally real meadows[END_REF] Md + FR constitutes a complete axiomatisation (also called a basis) of the meadow of reals R 0 . A corresponding question for dual number meadows reads thus:

import : CR, Md dn , DO 1(x 2 1 + x 2 2 + 1) = 1 (17)

Discussion and concluding remarks

In mathematics it is common practice to view numbers as elements of algebras.

The algebraic perspective on such mathematical entities leads to rings, fields, the algebra of quaternions, skew fields, dual numbers, and so on. From theoretical computer science we adopt the idea that one considers datatypes rather than algebras, or algebraic structures in the presence of relations (for instance an ordering) as well as functions. A datatype consists of an algebra coupled with a signature, that is a naming scheme for sorts, constants, and functions. In this manner the signature determines a formal language and different datatypes with the same signature correspond to the various algebras that constitute different semantic models for the signature at hand. With arithmetical datatype we will refer to datatypes which contain numbers or entities similar to numbers. For an introduction to datatypes we refer to the textbook [START_REF] Ehrich | Specification of Abstract Data Types[END_REF] and to [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF] and the references mentioned in [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF].

The transition from algebras to datatypes is quite significant for clarifying the relation, or rather the plurality of possible relations, between arithmetic and logic. At the same time the introduction of a signature is somehow counterintuitive from the perspective of conventional mathematics in which the notion of syntax is virtually absent. In the case of rational numbers for instance it is plausible, when contemplating an arithmetical datatype for rational numbers, to include inverse, or division, or both, in the signature. Doing so creates a setting in which 1/0 is a legal expression, quite independently of its meaning. Even if division is understood as a partial function and 1/0 has no defined value then still 1/0 is a legal expression and the question "what is 1/0?" is a valid question, which is entitled to an answer. The question is equally valid as the question whether or not Σ ∞ n=1 1/n exists. I consider the common practice to say that x -1 is a notation for the unique y such that x • y = 1, if it exists, is not entirely satisfactory, if only because through that convention the use of an expression already carries mathematical content as a side effect. By having inverse as a member of the signature such descriptions can be avoided.

In the context of datatypes, equations have been identified as a very useful method of specification of classes of datatypes. Finite sets of equations can be used as proof systems amenable to automation. Given a set of equations the class of its models (algebras) has an initial algebra which is unique up to isomorphism. A finite set of equations is called an equational specification of its initial algebra. Such specifications were found for natural numbers, and integers some 50 years ago, and have since been developed for many data structures that arise in computing.

Given a finite set of equations it is often possible to find an implementation of the initial algebra by means of fully automated term rewriting techniques. In [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF] a datatype for rational numbers is proposed by extending the signature with an inverse function -1 under the assumption that 0 -1 = 0. The main result of [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF] is to provide a finite equational specification of Q 0 , the datatype of rational numbers, with inverse made total by having 0 -1 = 0. The question whether or not the specification of Q 0 can be turned into a terminating and confluent term rewriting system has remained open, however.

The present paper provides an extension of the work in [START_REF] Bergstra | The rational numbers as an abstract data type[END_REF] to the case of dual numbers. As it turns out having p -1 = 0 in case the original definitions have p -1 undefined works quite well.

The use of equational logic opens two perspectives. On the one hand it leads to term rewriting and automatic implementation, on the other hand it leads to universal algebra where elementary classes, i.e. the model classes of sets of equations, play a key role. We define a meadow as an element of the smallest elementary class which contains all fields expanded with a zero totalised inverse operation. This approach to the definition of classes of arithmetical datatypes can be generalised in various directions, for instance dual numbers, transrational numbers, and transreal numbers.

We have thereby presented an informal format for defining classes of meadowlike structures. Technical details are provided regarding dual number meadows. In this format a definition of dual number meadow is given and some investigation of the equational theory of dual number meadows has been provided. For the case of dual rational numbers, the minimal dual number meadow of characteristic 0, an initial algebra specification is developed. A range of open questions concerning dual number meadows has been formulated.

Transmeadows

In the format for defining classes of meadow-like arithmetical datatypes, as outlined in Paragraph 1.3 above, many more generalisations can be imagined.

As a new generalisation/adaptation of meadows we propose the transmeadows. These constitute a generalisation of the transrational numbers as well as of the transreal numbers ( [START_REF] Anderson | Perspecx Machine VIII, axioms of transreal arithmetic[END_REF]) but not of the more sophisticated transcomplex numbers of [START_REF] Reis | Construction of the transcomplex numbers from the complex numbers[END_REF].

The signature of transmeadows is the same as for meadows. We will first define strongly regular transmeadows. We assume that A is an arbitrary ordered field with domain V . A is transformed into A tm by extending its domain and by defining (extending) all operations to the new domain. The domain V is extended to V tm by introducing three pairwise distinct and new elements +∞, -∞, and Φ and expanded with a function --1 . The latter function serves as the interpretation of the interpretation of --1 .

The elements +∞, -∞ serve as interpretations of 0 -1 , -(0 -1 ), and 0 • 0 -1 respectively.

For ease of notation constant names +∞, -∞ and Φ (the latter called nullity), are used for these entities ( +∞, -∞, and Φ respectively). The extension of the functions of A to V tm is given by the following requirements, thereby obtaining A tm :

• + and • are commutative

• -(x • y) = (-x) • y, -(x + y) = (-x) + (-y).

• x + Φ = x • Φ = -Φ = Φ -1 = 0 -1 = +∞, ∞ -1 = (-∞) -1 = 0, 0 • ∞ = Φ, -(+∞) = -∞, -(-∞) = +∞, +∞ + (-∞) = Φ, • x = 0 ∧ x = +∞ ∧ x = -∞ ∧ x = Φ → x • x -1 = 1, • x = Φ ∧ x = -∞ → x + (+∞) = +∞,
• and for all a > 0 ∈ V : a • (+∞) = +∞.

We write Σ Mdt for the mentioned signature expansion of Σ Md and we write Eq srtm for the equational theory of the class of all strongly regular transmeadows and CEq srtm for the conditional equational theory of the class of all strongly regular transmeadows. Here the ordering is not included in the signature and for that reason it does not occur in equations or in conditions of conditional equations.

Given these preparations a transmeadow can be defined to be a model of CEq srtm . Several questions about transmeadows remain open. We mention these questions for further research.

Concluding remarks

We conclude with restating two older outstanding open questions concerning meadows, both of which can be reformulated for the dual number meadow of rationals as well as for the transmeadow of transrational numbers. Problem 4.6. Is there a finite algebraic specification of Q 0 which is complete for its equational theory? Problem 4.7. Is there finite equational initial algebra specification of Q 0 which constitutes a complete (i.e. confluent and terminating) term rewrite system.

Conditional term rewriting is more involved than unconditional term rewriting and, as a consequence, a collection of conditional equations can be understood as a conditional term rewriting system in different ways. The following question represents a family of questions, corresponding to the different interpretations of systems of conditional equations as term rewrite systems. Problem 4.8. Is there a finite conditional equational initial algebra specification of Q 0 which gives rise to a complete (i.e. confluent and terminating) conditional term rewriting system.

Problem 4 . 1 .Problem 4 . 2 .Problem 4 . 3 .Problem 4 . 4 .Problem 4 . 5 .

 4142434445 Is the class of transmeadows a variety (i.e. is CEq srtm logically equivalent to Eq srtm )? Does the class of transmeadows have a finite (conditional) equational axiomatisation? Is the equational theory of transmeadows decidable? Find a suitable definition of dual number versions of transmeadows. Find a suitable definition of a transcomplex meadow.

  Definition 2.2. A dual number meadow is a structure A with signature Σ Md,V, such that A |= CEq srdnm . Definition 2.3. A weakly totalised dual number meadow is a structure A with signature Σ Md,V, such that A |= Eq srdnm . Proposition 2.2 establishes the existence of weakly totalised dual number meadows. This definition follows the pattern of definitions of meadow related classes as discussed in Paragraph 1.2 above. The following questions arise and are left open. Problem 2.1. Does Eq srdnm have a finite equational axiomatisation? Problem 2.2. Does CEq srdnm have a finite conditional equational axiomatisation? Problem 2.3. Is Eq srdnm decidable? Problem 2.4. Is CEq srdnm decidable?

Table 8 :

 8 Formal reality for sums of two squares Problem 3.2. Is CR + Md d + DO + FR a complete axiomatisation of the equational theory of R dn 0 ?

	Problem 3.3. Is the equational theory of R dn 0 decidable?

Acknowledgements

The author acknowledges both anonymous reviewers for useful suggestions for improvements, including a simplification of the proof of Proposition 2.8, and a remark that led to the observation that (unlike the case with meadows) dual number meadows constitute a quasivariety rather than a variety.