M Gudmundsson

D Fischer

N Haag

H A B Johansson

D Misra

P Reinhed

H Schmidt-Böcking

R Schuch

M Schöffler

K Støchkel

H T Schmidt

H Cederquist

Angular scattering in fast ion-atom electron-transfer collisions: Projectile wave diffraction and Thomas mechanisms

Keywords: numbers: 34, 70, +e, 42, 50, Xa

published or not. The documents may come     Angular scattering in fast ionatom electron transfer collisions: projectile wave diffraction and Thomas mechanisms

INTRODUCTION

Electron transfer reactions in fast ion-atom and fast ion-molecule collisions have been studied since the earliest days of quantum mechanics. During the last decade, research on fast ion-atom collisions have mainly been concentrated on investigations of ionization processes. For investigations of such processes, the invention of the reaction microscope [1], in which the momentum vectors of all outgoing particles (ions and electrons) are measured with high resolution and high efficiencies, represents a major breakthrough. For pure electron capture processes the corresponding experimental task is to measure the three momentum components for the recoiling target ions with high precision and high resolution. The COLTRIMS technique (Cold Target Recoil-Ion-Momentum Spectroscopy), a forerunner to reaction microscopy, is ideally suited for this task [2].

In 2006, Fischer et al. [3] reported on a COLTRIMS experiment in which two separate contributions to the recoil ion momentum distributions, and to the projectile angular scattering distributions dσ/dΩ, were fully resolved. The dominant feature in these distributions is due to projectile scattering in the forward direction which gives a peak centered at zero transversal momentum transfer (p ⊥ = 0) to the recoiling target. A corresponding peak appears already in a theoretical treatment based on the first Born approximation (in which the process is described as a single interaction between the projectile and the active electron in the field of the target nucleus or as an interaction between this electron and the target nucleus in the projectile field [4]). How-ever, for more quantitative comparisons it is clear that also second Born contributions have to be included in the theoretical treatment [5]. Fischer et al. [3] ascribed the smaller secondary peak in dσ/dΩ (first found experimentally by Horsdal-Pedersen et al. [6]) to the so called Thomas process, which may be accounted for by both classical [START_REF] Thomas | Proc. R. Soc[END_REF] and quantum mechanical (second Born) descriptions [START_REF] Drisko | [END_REF]. In the classical picture [START_REF] Thomas | Proc. R. Soc[END_REF], the H + projectile (p) scatters on one target electron (e) such that this electron (e) scatters on the target nucleus (N) and becomes bound to the projectile. Then, energy and momentum conservation requires that the electron (e), when initially at rest in the target frame, is scattered at 60 degrees with respect to the projectile trajectory and this binary (p-e) collision thus gives the characteristic proton (p-e-N) Thomas projectile scattering angle of 0.47 mrad. In general, the (p-e-N) Thomas angle for a projectile of mass M p and electron of mass m e is (θ

) p-e-N = √ 3 2 m e M p ( 1
)
which is independent of the projectile velocity v p and the target mass, while

(p ⊥ ) p-e-N = √ 3 2 v p m e (2)
(m e = 1 in atomic units). In Ref. [START_REF] Fischer | [END_REF], the separate velocity dependencies of the total pure non-radiative single-electron capture cross section and the resolved parts of these cross sections due to the secondary peaks in dσ/dΩ (Thomas processes [START_REF] Fischer | [END_REF]) were discussed for 1.3 -12.5 MeV H + + He collisions. In Confidential: not for distribution. Submitted to IOP Publishing for peer review 4 August 2010 this paper, we report on various detailed features (peak positions and widths) of the corresponding differential cross sections dσ/dΩ , dσ/dθ and dσ/dp ⊥ and compare them with the same type of information from measurements on

He 2+ + He → He + He 2+ (3)
processes in which fast He 2+ projectiles with kinetic energies of 6.0 MeV capture both electrons from He target atoms essentially at rest. For these measurements we have used a He gas-jet target [10,11] and a recoil ion momentum spectrometer (cf. [12][13][14]) mounted inside the ion storage ring CRYRING [15]. Surprisingly, in view of what is expected for Rutherford scattering, we find that the widths of the forward scattering peaks in dσ/dΩ are close to the same constant value in the energy range between 1.3 and 12.5 MeV regardless of the number of active electrons (one or two) where we also have included the double electron capture data by Schuch et al.

[16] at 1.6 MeV in the comparison. The peak positions and widths of the forward peaks for the corresponding dσ/dp ⊥ cross sections are found to depend linearly on the longitudinal momentum transfer p -but with different linear behaviours for single-and double-electron capture. Unlike in the cases of H + + He single-electron capture, it was not possible to isolate separate secondary maxima in dσ/dΩ for 6.0 MeV He 2+ + He double electron capture. Here, we will discuss possible ways to interpret the measured shapes of the differential cross sections and we will then consider both Thomas capture mechanisms and diffraction of H + and He 2+ projectile de Broglie waves on "apertures" corresponding to limited spatial regions for single-and double-electron capture close to the He target nuclei. As we will show below, the latter description may account for many of the presently observed features, in particular it can explain the constant angular widths of the forward scattering peaks and the appearances of a third maximum at large angles for single-electron capture. At the same time, we find that the p ⊥ -positions of the secondary maxima in dσ/dp ⊥ depend on v p as suggested by Eq. 2, which was deduced for the (p-e-N) Thomas process.

EXPERIMENT

The experiment was performed at the synchrotron, cooler and heavy ion storage ring CRYRING [15] at Stockholm University. The experimental procedure used for the H + + He measurements has been reported in ref. [START_REF] Fischer | [END_REF] and here we give a description of the pure doubleelectron capture He 2+ + He measurements, focusing on some special precautions and steps that had to be taken in this particular case.

The He 2+ projectile ions were produced in an Electron Cyclotron Resonance (ECR) ion source, accelerated to 300 keV/u by a radio-frequency quadrupole, and injected in CRYRING. Ions were accumulated in the ring through series of injections before they were accelerated to 6.0 MeV. Stored ion beam currents were typically 20 µA and the ion beam diameter was reduced to about 1.5 mm by means of electron cooling [17]. The overlap between the He 2+ ion beam and the 1.5 mm diameter supersonically cooled He gas jet [10,11] was optimized by moving the jet horizontally and in the direction perpendicular to the ion beam while measuring the recoil ion count rate. The gas jet target itself consists of four differentially pumped jet forming stages above the ring chamber and three differentially pumped jet-dump stages below [10]. In the present experiment, the temperature of the gas-jet nozzle was set to 160 K with a driving pressure of 2.5 bar, which gave typical jet-target densities of 10 8 atoms/mm 3 in the interaction region. The jet was collimated by means of two skimmers to limit its diameter and the initial momentum definition of the He target atoms before the collisions [10].

The recoil ion momentum spectrometer (cf. [12][13][14]) consists of an extraction region, a drift tube and a position sensitive microchannel plate detector with a resistive anode. The ion beam in CRYRING is very wide during the injection phase and therefore the opening for the circulating beam in the extraction stage of the spectrometer has to be large. The geometry is very open (7 x 5 cm 2 ) for the circulating beam and the extraction field is provided by a series of electrodes mounted in pairs above and below (and far from) the center of the fast circulating beam. The homogeneity of the extraction field in the central part of the extraction volume was achieved by means of two square shaped plates ('Deflection plates' in fig. 1) with bias voltages, mounted at the entrance and exit for the fast circulating He 2+ beam. At the same time these plates shielded the insulator rods on which the extraction plates were mounted from exposure to the stored beam and by adjusting the difference between the plate biases the recoil ion beam could also be steered horizontally. We used the conventional Wiley-McLaren, or "time-focusing", spectrometer geometry in which the drift tube has twice the length of the active part of the extraction region [18]. In the drift region we also had an electrostatic lens which by switching could be used to prevent recoil ions with certain mass to charge ratios from entering the drift region. An overview of the experimental setup and the data acquisition system is shown in fig. 1.

The fast He 0 product atoms, formed in double-electron capture reactions (3), are detected by a second position sensitive microchannel plate (MCP) detector (with a resistive anode) mounted in the straight section behind the first dipole magnet after the gas-jet target and 3.2 meters downstream of the jet-beam interaction region. A fast signal from the back of the projectile MCP serves as the start for the time-of-flight measurement (after it has been amplified, discriminated and delayed -see fig. 1). The corresponding four resistive anode corner signals are amplified and registered in list mode together with information on the time-of-flight (stop signals provided by the recoil ions) and the four recoil-detector corner signals.

At the present projectile energy of 6.0 MeV, the pure He 2+ + He double-electron capture cross section is in the 10 -26 cm 2 range [16]. Thus, special measures have to be taken in order to minimize random coincidence rates due to much more likely ionization processes. Such random rates are strongly reduced by means of a foil (10 mm diameter) mounted centrally on a grid in front of the recoil detector. This prevents recoil ions with low momenta (such as the ones from ionization) to reach the detector, while those due to pure non-radiative capture events have substantial longitudinal momenta p and do not hit the foil. This technique was used for the H + + He measurements [START_REF] Fischer | [END_REF] and in the present He 2+ + He measurement. For the latter we did, in addition, switch the spectrometer lens voltage such that only ions within a narrow time window for the He 2+ recoil ions are allowed to pass [19]. The corresponding time-of-flight spectra with and without gates on the positions on the projectile and recoil ion detectors are shown in fig. 2. Note the strong contribution from double ionization events below the double-electron capture peak in the upper spectrum without position gates, even when we use the blocking foil and switch the lens voltage on a timing gate for the He 2+ recoil ions only. A further difficulty which had to be overcome was the narrow time window (about 200 ns) available to record the recoil ion position (deduced from the relatively slow resistive anode signals) before the increase in count rate due to single ionization random events (cf. fig. 2, 'He + randoms'). This short time is insufficient for position detection by means of the spectroscopic amplifiers which we normally use for the resistive anode corner signals and, instead, much faster timing filter amplifiers were used. In the lower spectrum of fig. 2 we have used gates on the projectile detector and on the position for the double electron capture events on the recoil detector (lower inset to the right). This greatly improves the signal to noise ratio in the time of flight spectrum making the He 2+ peak due to pure double-electron capture events clearly visible (cf. the lower time-of-flight spectrum in fig. 2).

DATA ANALYSIS

The momentum transfer resulting from double (or single) electron capture can be separated in one component p along the direction of the fast, projectile ion beam and one component p ⊥ in the perpendicular direction. The longitudinal component along the beam can be expressed as a function of v p , the inelasticity Q and the number of transferred electrons, n, according to p ≈ -n × v p /2 + Q/v p (in atomic units). This may be approximated by p ≈ -n × v p /2 as the inelasticity, given by the difference in binding energies between the initial target state and the final projectile capture state, is very small (Q/v p << nv p /2). The recoil ion momentum components in the y-and z-directions (see the upper inset in fig. 2 where the coordinate system is defined) are obtained from the position on the detector and the time of flight whereas the momentum in the x-direction is calculated from the extraction voltage and the time of flight. The instrumental resolution in p x i.e. along the time-of-flight axis is about 0.3 a.u. with the present time resolution of about 3 ns [3], and is limited by electronics and fringe field effects. The resolutions in p y , which is determining our resulting projectile angular resolution, and p z depend on the image size on the detector and therefore on the extraction voltage. From the width of the double-electron capture p z distribution (cf. lower inset of fig. 2) we find that the p z (and p y ) resolution is about 15% of the longitudinal momentum transfer. This corresponds to scattering angle resolutions of 0.02 mrad for He 2+ + He double-electron capture and 0.04 mrad for H + + He single-electron capture. The scattering angle θ of the projectiles can in principle be measured directly on the projectile detector, or -as is the case here -it can be deduced through θ ≈ p ⊥ /(M p v p ). The benefit of the latter method is related to the high recoil ion momentum resolution, which only depends very weakly on the size of the ion-beam/gas-jet interaction volume, and the ion beam divergence. Thus, high intensity ion beams may be used in order to reach high luminosities without degrading the resolution in the p ⊥ measurement, which then also gives high resolution in the determination of θ.

RESULTS AND DISCUSSION

In figure 3, we compare the angular differential cross sections, dσ/dθ for the total non-radiative H + + He single-electron capture process at 7.5 MeV and for the total non-radiative He 2+ + He double-electron capture process at 6.0 MeV. In these measurements, the small contributions from radiative electron-capture processes are strongly discriminated against by means of the foil blocking the central part of the recoil-ion detector as described in the experimental section. In the single-electron capture data in fig. 3, additional maxima in dσ/dθ appear around 0.5 mrad and 0.75 mrad. The 0.5 mrad maximum is at the angle expected for the projectile-electron-(target) Nucleus, or p-e-N Thomas mechanism (cf. Ref. [3,4]), while the small but significant maximum at the larger scattering angle has not been predicted theoretically.

For He 2+ + He double electron capture two independent single-electron Thomas transfer processes, 2×(p-e-N) or a single (p-e-N) process combined with a forward (p ⊥ ≈ 0) process could in principle contribute and their expected characteristic angles are indicated by arrows in figure 3. In addition, the angle for another doubleelectron capture process "p-e-e-N", which would also involve scattering between the He-target electrons such that both would become bound to the projectile [20] is indicated in fig. 3. Clearly, none of these three capture processes could be isolated in the present 6.0 MeV He 2+ + He measurement.

In the upper panel of figure 4, we show characteristic scattering angles θ as functions of the collision energy defined as the the angular positions of the three maxima in dσ/dθ for H + + He electron capture and for the single maxima in dσ/dθ for He 2+ + He double-electron capture at 6.0 MeV and 1.6 MeV (the latter double-electron capture result from Ref. [16]). All forward peaks (including those for double-electron capture) are close to a common value of θ = 0.08 mrad. In the lower panel of figure 4, we show the corresponding angular widths and with the exception of the secondary maxima for H + + He there is very little variation with the projectile energy andas it seems -the number of transferred electrons n. The observed decrease in the angular widths of the secondary maxima is consistent with the results of quantum calculations of the Thomas process [4,[START_REF] Thomas | Proc. R. Soc[END_REF]. In the classical picture, the Thomas angle is θ p-e-N = √ 3/(2M p ) for an electron initially at rest in the target frame (cf. Eq. 1) and the corresponding angular width can then be expected to be given directly by the Compton profiles of the initial (target) and final (projectile capture) states. Thus, the width of the Thomas peak in p ⊥ should not change with v p while the corresponding θ-width in dσ/dθ thus is expected to scale with 1/v p consistent with the data in fig. 4.

In figure 5, we show the measured transversal momentum transfers, p ⊥ to He-target ions as functions of the corresponding longitudinal momentum transfers p ≈ -n × v p /2. Note that the secondary peaks for H + + He single-electron capture fall on a common straight line with a slope very close to √ 3 as expected for Thomas capture [START_REF] Thomas | Proc. R. Soc[END_REF] as

(p ⊥ ) p-e-N = √ 3 p , ((p ⊥ ) p-e-N = v p √ 3
2 , p = v p /2). The single-and double-electron capture forward scattering peaks follow separate linear p ⊥ = p ⊥ (p )scalings in the upper panel of fig. 5. The p ⊥ momentum widths (fig. 5, lower panel) of the forward peaks also scale linearly with p (and v p ) and again with different such scalings for single-and double-electron capture.

While the linear increase of p with v p is a trivial consequence of the overall momentum and energy conser-vation, the reason why p ⊥ also in the forward capture cases (1 st maxima in dσ/dθ) is proportional to v p is not immediately clear. From the description in [4] where forward capture is described as a single projectile-electron interaction in the field of the nucleus, it appears that the strength of the interaction with the nucleus would have to increase with v p to facilitate the larger longitudinal momentum transfers needed for electron-capture at higher velocities. However, if we now for a moment assume that the presently transversal momentum transfers are dominated by proton-He nuclear scattering without screening, the classical Rutherford formula would e.g. indicate an impact parameter distribution peaking at about 0.015 au to give a peak at the observed angle in dσ/dθ for 7.5 MeV protons. Such a strong localization of projectile trajectories in the plane perpendicular to vp would however according to the uncertainty principle lead to a spread in p ⊥ of more than 30 au -much larger than the measured value of p ⊥ = 2.65 ± 0.03 au. Thus, we conclude that the Rutherford scattering, as predicted by Miraglia et al. [21], is not the dominating contributor to the transverse momentum transfer.

With less strict localization in the impact parameter plane, the minimum transverse momentum transfer allowed by the uncertainty principle will be smaller and may reproduce the observed distributions. In the following we deduce the electron-transfer probabilities as functions of impact parameter under the assumption that the shapes of the measured transverse momentum transfer distributions are due to diffraction of projectile de Broglie waves.

Here an analogy with classical optics is helpful. If we consider light diffracted when passing a small aperture, we expect that the width of the primary diffraction maximum is inversely proportional to the size of the aperture. In the present analogy an aperture would correspond to having an electron-transfer probability, P(b), which is constant for values of b smaller than a certain effective capture radius and zero for larger b [ †] . The optical analogy of a more realistic continuous electron transfer probability function P(b) would be a screen, not with a hole, but with a position-dependent transmission function, T(b). For the optical case, the light intensity distribution on a distant observation screen when a plane light wave is diffracted through the partially transparent screen is related to this transmission function. Specifically, the function describing the damping of the wave amplitude is related to the amplitude distribution of the outgoing wave through a Fourier transform. The same [ †] Note that in this analogy P(b) corresponds to the transmission of the light since we are considering projectiles that come in charged and leave the interaction region as neutrals, whereas in the optical case we would observe the light that was merely transmitted.

formal relation exists between the measured angular differential cross sections, dσ/dΩ and the electron-transfer probability, P(b), and we can therefore deduce the latter directly from our data under the assumption that the shapes of the forward peaks are governed by diffraction phenomena. Conceptually, this approach is equivalent to the one which has been used to rationalize observations of projectile wave interference in electron transfer to fast projectiles, H + and He 2+ , from molecular hydrogen targets [22,23]. Impact parameter dependent electron transfer probabilities P(b) that reproduce the shapes and magnitudes of the forward peaks in the electron-transfer angular differential cross sections are calculated in this way from the cross section data in the range θ ≤ 0.32 mrad for singleelectron capture and θ ≤ 0.28 mrad for double-electron capture. In fig. 6, we show such P(b) distributions for 1.3 -12.5 MeV H + + He single-electron capture and for 6.0 MeV He 2+ + He double-electron capture. We first note that the values of these P(b) are very small and decrease rapidly with increasing projectile velocity v p . Further, the widths of the P(b) distributions decrease with increasing v p . Via the Heisenberg uncertainty principle this stronger localization translates to the observed increase in the transverse momentum transfer with increasing v p .

For the double-capture case (lowest panel, fig. 6) we find that impact parameters smaller than about 0.15 au contribute most to the cross section. This range is about four times narrower than for the H + + He SC at similar velocities most likely due to the fact that both electrons are transferred to the projectile.

In fig. 6, we also show P(b) step functions corresponding to sharply defined 'apertures', corresponding to optical diffraction through a hole in a screen. The sizes of these apertures are chosen as to reproduce positions of the first minima in the angular differential cross sections and the constant value of P(b) for b smaller than the aperture radii are chosen as to fit the measured cross sections. When we take the step function for the 7.5 MeV H + + He case to calculate the full angular differential cross section, we get the result shown in fig. 7, where we in addition to the central peak, also have higher order diffraction peaks. Here, the secondary diffraction peak is close to the Thomas peak and therefore a clear separation of the two contributions is not possible. However, we note that the secondary peak in dσ/dθ is measured to have the precisely the scaling of p ⊥ with p as we expect for the p-e-N Thomas process. Further it has been demonstrated experimentally that the cross section corresponding to the secondary maximum scales as v -11 p [START_REF] Fischer | [END_REF] in agreement with the prediction of Thomas [START_REF] Thomas | Proc. R. Soc[END_REF]. The third peak at 0.75 mrad cannot be related to any multiple scattering mechanism in an obvious way and is likely to be dominated by diffraction effects. Clearly the true P(b) is not a step function, but on the other hand, higher-order diffraction maxima of reduced magnitude are to be expected from other non-Gaussian functional forms of P(b) as well.

CONCLUSION

In this paper, we have reported that the positions and shapes of the forward (primary) scattering peaks in dσ/dθ are essentially independent of the collision energy and the number of transferred electrons in fast H + + He → H + He + (1.3-12.5 MeV) and He 2+ + He → He + He 2+ (1.6 [16] and 6.0 MeV) collisions. This observation is also reflected in the results of direct mea- surements of the variation of the transversal momentum transfer to the projectile, p ⊥ , with the projectile velocity v p and we deduce separate linear p ⊥ (v p ) scalings for the one-and two-electron transfer processes. These results are markedly different from what would be expected for pure projectile-target nucleus Rutherford scattering. We have shown that it is possible to rationalize these findings by considering diffractions of projectile de Broglie waves in small "apertures" corresponding to electron transfer probabilities, P(b), in narrow regions of impact parameters. The sizes of these regions decrease with increasing projectile velocities. This picture thus readily accounts for the constant widths of the forward scattering peaks and for the appearances of second and third maxima in dσ/dθ in the H + + He case. The secondary maxima, and their positions and widths, are however also accounted for through the Thomas p-e-N mechanism and we have shown that there is a quantitative agreement between how the secondary peak is expected to change with v p [4] and our measurement. In this work, we have nevertheless clearly demonstrated that projectile wave diffraction phenomena have to be considered when describing projectile angular scattering of electron capture in fast ion-atom collisions and that the diffraction actually dictate several main features of the corresponding differential cross sections.

Single-aperture diffraction has not been much discussed before in connection with electron capture in fast ion-atom collisions (an exception is [21]) and this is, to our knowledge, the first time that such effects have been demonstrated experimentally. This was possible due to the high resolution and the high luminosity of our recoil ion momentum spectrometer mounted inside the ion stor-age ring CRYRING at the Manne Siegbahn Laboratory, Stockholm University.

FIG. 1 :

 1 FIG.1: Experimental setup for the He 2+ + He double electron capture measurements. The electrostatic lens is on a high positive voltage most of the time in order limit the random coincidence rate due to ionization processes. The lens voltage is switched to zero at a certain time after the registration of a neutral particle on the projectile detector in order to allow He 2+ ions to pass and be detected first (cf. text).

FIG. 2 :

 2 FIG. 2: Time of flight spectrum for double electron capture in 6.0 MeV He 2+ + He collisions without position gates on the recoil and projectile detectors (upper curve) and with such gates (squares below). The shaded area shows the time of flight gate. Insets to the right show recoil detector images without (above) and with gates (below) in the time-of-flight and on the projectile detector (cf. text).

FIG. 3 :

 3 FIG.3: Absolute angular differential cross section for 6.0 MeV He 2+ double capture (DC) from He (black boxes) and 7.5 MeV proton single capture (SC) from He (grey diamonds). Arrows indicate the expected angular positions for maxima of various hypothetical Thomas processes (cf. text).

FIG. 4 :

 4 FIG.4: Above: peak positions in dσ/dθ plotted as functions of the projectile energy. Below: widths (FWHM) in θ of Gaussian peaks fitted to dσ/dΩ plotted as functions of projectile energy.

FIG. 5 :

 5 FIG. 5: Above: positions of the three maxima in dσ/dp ⊥ for H + + He single-electron capture and He 2+ + He doubleelectron capture. Below: widths (FWHM) in p ⊥ of Gaussian peaks fitted to the first two peaks of dσ/dΩ as a function of | p |.

FIG. 6 :

 6 FIG.6: Impact parameter distributions, deduced from the shapes of the forward peaks in dσ/dΩ (cf. text) for 1.3 -12.5 MeV H + + He single-electron capture (full, grey line) and 6.0 MeV He 2+ + He double-electron capture (full, black line). Step function for P(b) giving the first diffraction minima coinciding with first experimental minima at the experimental values of 0.32 mrad and 0.28 mrad for SC and DC, respectively (dotted lines).

FIG. 7 :

 7 FIG. 7: Measured cross section dσ/dΩ (open diamonds) and cross section resulting from a step-function P(b) (full squares) with radius chosen as to give a minimum in dσ/dΩ at 0.32 mrad.

ACKNOWLEDGMENTS

This work is supported by the Knut and Alice Wallenberg Foundation, the Swedish Research Council (VR) and the German Research Council (DFG).


D J Szwer

S C Webster

A M Steane

D M Lucas

Keeping a

Keywords: numbers: 03, 67, Pp, 37, 10, Ty

Dynamic decoupling (DD) is a general technique for maintaining the phase coherence of a quantum state, with particular importance for protecting the quantum information stored in the memory qubits of a quantum computer [START_REF] Viola | Dynamical suppression of decoherence in two-state quantum systems[END_REF]. The simplest example is the Hahn spin-echo [START_REF] Hahn | Spin echoes[END_REF], a single π-pulse which protects against an arbitrary and unknown constant offset in the qubit's precession frequency [START_REF] Chiaverini | Implementation of the semiclassical quantum fourier transform in a scalable system[END_REF][START_REF] Lucas | A long-lived memory qubit on a low-decoherence quantum bus[END_REF]. When the state is subject to a time-varying offset due to, for example, magnetic field noise, it can be protected by a sequence of many π-pulses. One of these, the Carr-Purcell-Meiboom-Gill (CPMG) sequence, is well known in the field of nuclear magnetic resonance [START_REF] Freeman | Spin Choreography: Basic Steps in High Resolution NMR[END_REF]. More recently, other sequences have been investigated specifically for their dynamic decoupling properties, such as Periodic DD, Concatenated DD [START_REF] Khodjasteh | Fault-tolerant quantum dynamical decoupling[END_REF], random decoupling [START_REF] Viola | Random decoupling schemes for quantum dynamical control and error suppression[END_REF], composite schemes [START_REF] Kern | Controlling quantum systems by embedded dynamical decoupling schemes[END_REF], and local optimisation [START_REF] Michael | Optimized dynamical decoupling in a model quantum memory[END_REF][START_REF] Uys | Optimized noise filtration through dynamical decoupling[END_REF]; a recent review by Yang, Wang and Liu contains further information and references [START_REF] Yang | Preserving qubit coherence by dynamical decoupling[END_REF].

In this paper, we derive a dynamic decoupling sequence in a particularly intuitive manner, as an extension to the spin-echo [START_REF] Hahn | Spin echoes[END_REF]. We prove that with n pulses, the sequence can cancel out all the dephasing that would be caused by the frequency varying as an (n -1)th order polynomial function of time, without knowledge of the polynomial coefficients. This sequence is identical to the Uhrig Dynamic Decoupling (UDD) sequence [START_REF] Götz | Keeping a quantum bit alive by optimized π-pulse sequences[END_REF][START_REF] Götz | Exact results on dynamical decoupling by π pulses in quantum information processes[END_REF], which was originally derived by considering the interaction of a spin qubit with a bosonic bath. We implement the sequence on a single 43 Ca + ion, demonstrating that the coherence time of this qubit is significantly increased, and compare it with the CPMG sequence.

Suppose an arbitrary qubit state is prepared at time 0, and we want to recover it at time τ . The pulse sequence is a series of (assumed ideal and instantaneous) π-pulses at times α 1 τ, α 2 τ, . . . , α n τ, where the α i are to be found. We have remarked that a single Hahn spin-echo will correct for a constant frequency offset. If the offset varies linearly with time, we can correct the phase error with two π-pulses at t = 1 4 and 3 4 , where t = time/τ (Figure 1a). To generalise further, postulate that n pulses suffice to correct for a frequency variation δ(t) that is an (n -1)th-order polynomial in time (Figure 1b):

δ(t) = p 0 + p 1 t + p 2 t 2 + • • • + p n-1 t n-1 .
(

) 1
The phase error φ err is given by integrating δ(t) over time. But each π-pulse reverses the direction of the qubit's precession, so between pulses i and i + 1, if i is odd, we multiply the acquired phase by (-1). The resulting integral is thus

π π π π b) π τ 0 0.07τ 2
φ err = n i=0 (-1) i αi+1 αi δ(t) dt = n i=0 (-1) i αi+1 αi n j=1 p j-1 t j-1 dt = n i=0 (-1) i   n j=1 p j-1 t j j   αi+1 αi (2)
where α 0 = 0 and α n+1 = 1. Collecting terms for each polynomial coefficient p j :

φ err = n j=1 p j-1 j (-1) n -2 n i=1 (-1) i α j i . (3)
We require φ err to be 0 for any choice of the p j , and so we obtain a set of n simultaneous equations for the α i

(-1) n -2 n i=1 (-1) i α j i = 0 ∀j = 1, 2, . . . , n (4)
These are solved by

α i = sin 2 π 2 i n + 1 (5)
which can be proved directly by substituting ( 5) into ( 4) and applying a series of trigonometric identities [START_REF] Szwer | High Fidelity Readout and Protection of a 43 Ca + Trapped Ion Qubit[END_REF]. The sequence is independent of τ ; however in practice the frequency offset δ(t) is only approximated by a polynomial, and as τ increases we need more polynomial terms (and hence more π-pulses) for the approximation to be valid.

This sequence was previously and independently discovered by Uhrig [START_REF] Götz | Keeping a quantum bit alive by optimized π-pulse sequences[END_REF][START_REF] Götz | Exact results on dynamical decoupling by π pulses in quantum information processes[END_REF], by considering the spectral properties of a qubit coupled to a bath of bosons that cause decoherence. The echo sequence was treated as a filter in frequency space. Uhrig demanded that the first n derivatives of the filter function vanish at zero frequency, because this gives the strongest suppression of the noise at low frequencies, and this condition leads to the simultaneous equations ( 4) and hence the sequence (5). Lee, Witzel and Das Sarma have shown [START_REF] Lee | Universal pulse sequence to minimize spin depahasing in the central spin decoherence problem[END_REF] that this sequence is optimal for any dephasing Hamiltonian, where "optimal" means that it is the sequence that maximises the qubit fidelity in the small τ limit, for a given number of pulses §. While this paper was in preparation, Hall et al. have independently published a derivation equivalent to ours [START_REF] Hall | Ultrasensitive diamond magnetometry using optimal dynamic decoupling[END_REF].

In a 1988 paper [START_REF] Keller | Gradient moment nulling through the nth moment. application of binomial expansion coefficients to gradient amplitudes[END_REF], Keller and Wehrli suggest using a theoretical procedure similar to ours, to cancel the effects of successive polynomial orders of fluid flow in MRI. However, this "gradient moment nulling" allows δ(t) to be controllably scaled by the experimenter; Keller and Wehrli concentrate on this parameter rather than pulse timing and so do not find the UDD sequence.

The first experimental tests of UDD were by Biercuk et al., who applied a variety of dynamic decoupling schemes to ensembles of ∼ 1000 9 Be + ions in a Penning trap [START_REF] Michael | Experimental Uhrig dynamical decoupling using trapped ions[END_REF]. Dynamic decoupling was demonstrated in a solid by Du et al. (using electron paramagnetic resonance of ensembles of unpaired carbon valence electrons in irradiated malonic acid crystals) [START_REF] Du | Preserving electron spin coherence in solids by optimal dynamical decoupling[END_REF], and in a dense atomic gas by Sagi, Almog and Davidson (∼ 10 6 87 Rb atoms in a dipole trap) [START_REF] Sagi | Process tomography of dynamical decoupling in a dense cold atomic ensemble[END_REF]. And recently, Ryan, Hodges and Cory implemented sequences using single nitrogen vacancy centres in diamond [START_REF] Ryan | Extending quantum coherence in diamond[END_REF].

We have applied dynamic decoupling to a single 43 Ca + trapped-ion qubit, held in a radio-frequency Paul trap [START_REF] Pa Barton | Measurement of the lifetime of the 3d 2 D 5/2 state in 40 Ca +[END_REF]. The qubit is stored in two hyperfine states in the ground level, |↓ = 4S (where the superscripts indicate the quantum numbers F, M F ); these states are separated by a 3.2 GHz M1 transition. The transition's sensitivity to the external magnetic field is 2.45 MHz G -1 at low field; we apply a field of 2.2 G to define a quantization axis and to increase the ion's fluorescence rate (by destabilising dark states [START_REF] Berkeland | Destabilization of dark states and optical spectroscopy in Zeeman-degenerate atomic systems[END_REF]). Rabi oscillations are driven on the qubit transition at Rabi frequency 2π×18 kHz, using microwaves. These are generated using a versatile synthesizer, amplified with a solid-state amplifier (to ≈ 750 mW) and broadcast inside the vacuum chamber using a trap electrode as the antenna. To improve the fidelity of the dynamic decoupling π-pulses we apply a small 50 Hz signal, synchronized with the AC line, to a magnetic field coil which cancels the dominant component of the magnetic field fluctuations experienced by the ion; the remaining noise has amplitude up to ±3 kHz. Each experimental sequence is also line-triggered.

Each experiment (Figure 2a) starts with the ion optically pumped into state |↓ . A decoupling sequence is tested by sandwiching it between two π 2 -pulses. The second pulse has a phase offset φ relative to the first; scanning this phase leads to Ramsey fringes. Any loss of phase coherence in the Ramsey gap leads to fringes of reduced contrast, so generally the contrast falls as the gap is made longer. We aim to show that this fall becomes slower when dynamic decoupling is used. Finally the qubit state is measured by electron shelving and fluorescence detection, with accuracy up to 99.8% [START_REF] Myerson | High-fidelity readout of trapped-ion qubits[END_REF].

The sequence is repeated 200 times for each value of φ, which is typically scanned from -450 • to +450 • in 20 steps resulting in the measured state varying sinusoidally with φ. A sine curve is fitted to the data to measure the contrast; example data is shown in figure 2b. Typically 10-20 such runs are taken for a given decoupling sequence, with τ chosen to be different for each, and with the decoupling pulse timings being scaled accordingly.

Figure 3 shows the results for different numbers of π-pulses. With no dynamic decoupling π-pulses, the fringe contrast drops to 1/e of its initial value in a time τ c = 0.51(5) ms; with a 20-pulse UDD sequence, this time is extended to τ c = 33(1) ms. We also compared UDD and CPMG (equally spaced π-pulses, at times α i = (i-1/2)/n for i = 1 . . . n) sequences, with results shown in figure 4. It can be seen that, in our noise environment, UDD performs no better than CPMG; indeed, CPMG is slightly better, extending the coherence time to τ c = 37(1) ms for a 20-pulse sequence, an increase over the unprotected qubit by a factor ≈ 73, or 1.9 orders of magnitude. The similar performance of UDD and CPMG is expected if the noise spectrum extends to high frequencies; UDD would be superior if the noise spectrum had a sharp highfrequency cutoff [START_REF] Michael | Experimental Uhrig dynamical decoupling using trapped ions[END_REF][START_REF] Pasini | Optimized dynamical decoupling for power-law noise spectra[END_REF]. We also performed experiments both with and without a 90 • phase shift on the UDD π-pulses , which is equivalent to testing the dynamic i.e. we tested both CP and CPMG sequences [START_REF] Carr | Effects of diffusion on free precession in nuclear magnetic resonance experiments[END_REF][START_REF] Meiboom | Modified spin-echo method for measuring nuclear relaxation times[END_REF].

decoupling for two different qubit states on the equator of the Bloch sphere; there was no significant difference between the results.

To fit the data in figures 3 and 4, we perform a simulation based on the filter function formalism of Cywiński et al. [START_REF] Cywiński | How to enhance dephasing time in superconducting qubits[END_REF]. Suppose that the noise power spectrum is given by S(ω). We multiply the noise spectrum by the pulse-sequence's filter function F (ωt) (F also depends on the number and finite duration of the π-pulses [START_REF] Michael | Experimental Uhrig dynamical decoupling using trapped ions[END_REF]), and calculate the integral over angular frequency ω:

χ(t) = ∞ 0 S(ω)F (ωt) πω 2 dω ( 6
)
The qubit coherence C(t) is then given by [START_REF] Cywiński | How to enhance dephasing time in superconducting qubits[END_REF] where N is a normalization constant that accounts for effects such as imperfections in the π-pulses themselves. In our experiment, C(t) is the contrast of the Ramsey fringes.

C(t) = N e -χ(t) (7) π 2 π 2 π π π π Readout Optical Pumping
The noise spectrum of the magnetic field measured outside the ion trap vacuum system did not give a good fit to the data when used to calculate C(t), presumably because it differs too greatly from the noise at the position of the ion. However, we can reverse the process; the dynamically-decoupled ion acts as a spectrometer to measure the field fluctuations [START_REF] Du | Preserving electron spin coherence in solids by optimal dynamical decoupling[END_REF][START_REF] Hall | Ultrasensitive diamond magnetometry using optimal dynamic decoupling[END_REF]. We model the noise spectrum S(ω) by a piecewise cubic spline in log-log space, use it to calculate C(t), and find the spectrum which gives the best fit to the experimental data; the fit attempts to match all our UDD and CPMG data with the same S(ω) (though each data set is allowed its own fitted normalization constant N ). The calculated contrast C(t) is not very sensitive to the detailed shape of S(ω), but the procedure does yield a noise spectrum which is close to a power law for 100 Hz (ω/2π) 100 kHz, with S(ω) ∝ ω -5±1 . This is consistent with the S(ω) ∝ ω -4 spectrum measured by Biercuk et al. inside a superconducting solenoid [START_REF] Michael | Optimized dynamical decoupling in a model quantum memory[END_REF]. The curves in figures 3 and 4 show the calculated C(t) using this noise spectrum, and fit the experimental data reasonably well.

The fitted 1/e coherence times are shown in figure 5. The data is matched well by a straight line, similar to the observations of Ryan, Hodges and Cory [START_REF] Ryan | Extending quantum coherence in diamond[END_REF].

It is clear from figure 3 that although the UDD sequence significantly extends the coherence time of the qubit, the coherence at short time is actually degraded due to imperfections in the π-pulses which are more significant the larger the number of pulses used. We estimate the typical π-pulse fidelity (based on the fits extrapolated to τ = 0) to be 98.7%. This fidelity could be improved significantly by increasing the Rabi frequency so that it is well above the amplitude δ(t) of the dominant noise sources, for example by driving the qubit transition with near-field microwaves from electrodes much closer to the ion, as proposed in [START_REF] Ospelkaus | Trapped-ion quantum logic gates based on oscillating magnetic fields[END_REF].

In conclusion, we have shown that extending the Hahn spin-echo to correct for frequency offsets which vary polynomially in time yields the Uhrig dynamic decoupling sequence, and that applying this sequence (or the CPMG sequence) to a single physical qubit stored in a trapped 43 Ca + ion increases the coherence time by nearly two orders of magnitude, to τ c ≈ 35 ms. In order to demonstrate the increase in coherence time, we chose qubit states in the S 1/2 manifold which had the greatest sensitivity to magnetic field fluctuations. For a qubit stored in the magnetic field-insensitive "clock" states (4S 3,0 1/2 and 4S 4,0 1/2 ) we have previously measured a coherence time T 2 = 1.2(2) s [START_REF] Lucas | A long-lived memory qubit on a low-decoherence quantum bus[END_REF]; since this was also limited by magnetic field noise, it should be possible to extend the coherence time of such a qubit to several minutes using dynamic decoupling techniques, at which point it becomes practically difficult to measure using a single qubit. The memory qubit coherence time would then exceed the typical timescale for trappedion quantum logic gates (∼ 20 µs [START_REF] Kirchmair | Deterministic entanglement of ions in thermal states of motion[END_REF]) by many orders of magnitude, an essential prerequisite for implementing fault-tolerant quantum computation. [START_REF] Viola | Random decoupling schemes for quantum dynamical control and error suppression[END_REF], is plotted against the number of π-pulses for UDD and CPMG data. A straight line fit to all the data is shown. When the Ramsey delay τ is equal to the coherence time, the finite-length π-pulses occupy a total duration < 0.02τ in all cases.

Figure 1 .

 1 Figure 1. Illustration of the effect of dynamic decoupling sequences on the acquired phase, as calculated by (2). a): Frequency offset δ varies linearly with time, and the phase shift can be completely corrected by a sequence with two π-pulses (for n = 2, CPMG and UDD are identical). b): δ varies as a (arbitrary, unknown) quartic polynomial, and is perfectly corrected by n = 5 pulse UDD.

Figure 2 .Figure 3 .

 23 Figure 2. a) Experimental sequence: the qubit coherence after time τ is measured by a Ramsey experiment in which the phase φ of the second π 2pulse is scanned relative to that of the first. An n = 4 pulse UDD dynamic decoupling sequence is shown in the example (the π 2 -pulse and π-pulse durations are exaggerated for clarity). b) Data (with shot noise error bars) and fitted Ramsey fringes for n = 3 and n = 6 pulse UDD sequences, both at τ = 7 ms. The dramatic improvement in the qubit coherence given by the 6-pulse sequence is clear.

Figure 4 .

 4 Figure 4. Comparing UDD and CPMG sequences for six and twenty π-pulses.Solid symbols (error bars omitted for clarity) and dotted lines are the results and fits from UDD sequences as shown in Figure3. Hollow symbols represent CPMG sequences, with solid lines the theoretical prediction using the same fitted noise spectrum S(ω) as for the UDD sequences. Data points with the same τ have been combined for clarity.

Figure 5 .

 5 Figure 5. The 1/e coherence time, as measured by[START_REF] Viola | Random decoupling schemes for quantum dynamical control and error suppression[END_REF], is plotted against the number of π-pulses for UDD and CPMG data. A straight line fit to all the data is shown. When the Ramsey delay τ is equal to the coherence time, the finite-length π-pulses occupy a total duration < 0.02τ in all cases.

§ We note that (5) also gives the locations of the zeros of Chebyshev polynomials of the second kind Un(2t -1) (where the polynomials have been scaled and shifted from the domain x ∈ [-1, 1] to t ∈ [0, 1]).

Acknowledgments

We thank M. J. Curtis and D. N. Stacey for helpful comments on the manuscript, other members of the Oxford ion trap group for useful discussions, and C. A. Ryan for drawing our attention to additional references. This work was funded by EPSRC (QIP IRC), IARPA (ref. 47968-PH-QC), the European Commission (SCALA network) and the Royal Society.


Anne Preller
email: preller@lirmm.frmehrs@comlab.ox.ac.uk

Mehrnoosh Sadrzadeh

Semantic Vector Models and Functional Models for Pregroup Grammars

Keywords: compositional semantics, quantum logic, pregroup grammars, semantic vector models, symmetric compact closed categories, two-sorted functional first order logic

We show that vector space semantics and functional semantics in twosorted first order logic are equivalent for pregroup grammars. An algorithm translates functional expressions to vector expressions and viceversa. The semantics is compositional, variable free and invariant under change of order or multiplicity. It includes the semantic vector models of Information Retrieval Systems and has an interior logic admitting a comprehension schema. A sentence is true in the interior logic if and only if the 'usual' first order formula translating the sentence holds. The examples include negation, universal quantifiers and relative pronouns.

Introduction

Pregroup grammars, [START_REF] Lambek | Type grammar revisited[END_REF], are based on compact bilinear logic, [START_REF] Lambek | Substructural Logics, chapter From categorial grammar to bilinear logic[END_REF], a simplification of the Syntactic Calculus, [START_REF] Lambek | The mathematics of sentence structure[END_REF]. Compact bilinear logic or Pregroup Calculus places pregroup grammars in the family of categorial grammars where 'the grammar is in the lexicon'. The pregroup grammars proposed so far cover a variety of languages, but most of them with no reference to semantics. Indeed, giving up Syntactic Calculus meant giving up higher order logic, i.e. the Montague semantics of traditional categorial grammars. The semantic structures appropriate for pregroup grammars had to be rediscovered.

To fill this gap, compact 2 -categories are proposed in [START_REF] Preller | Category theoretical semantics for pregroup grammars[END_REF], followed by functional models in two-sorted first order logic in [START_REF] Preller | Toward discourse representation via pregroup grammars[END_REF]. This semantics views verbs as predicates defined on individuals and sets of individuals.

On the other hand, [START_REF] Sadrzadeh | High-level quantum structures in linguistics and multiagent systems[END_REF] and [START_REF] Clark | A compositional distributional model of meaning[END_REF] consider the category of finite-dimensional real vector spaces and linear maps, with the explicit aim to add compositionality to distributive semantic vector models. They define the meaning of a transitive verb as a vector in the tensor product of three vector spaces. The basis vectors of two of the spaces are identified with nouns. The basis vectors of the third space are the pairs of these nouns. The value of a subject-object sentence formed by the verb and two nouns is computed with the help of the interior product. Later this method has been extended to negated sentences in [START_REF] Preller | Bell states and negated sentences in the distributed model of meaning[END_REF].

The starting point for this paper is the observation that the category of finitedimensional real vector spaces and the category of sets and two-sorted functions are compact closed symmetric monoidal categories, or equivalently, symmetric compact 2 -categories. We prove the equivalence of the two approaches relating two-sorted first order logic to the theory of compact 2 -categories and thus to quantum logic. Indeed, [START_REF] Abramsky | A categorical semantics of quantum protocols[END_REF] formulate quantum protocols in the theory of compact 2 -categories. The logic for Information Retrieval Systems of [START_REF] Van Rijsbergen | The Geometry of Information Retrieval[END_REF] uses the lattice of projectors in finitedimensional Hilbert spaces, also a compact 2 -category. A study by [START_REF] Clarke | Context-theoretic Semantics for Natural Language, an algebraic framework[END_REF] of context-theoretical semantics states that it is the lattice structure of real numbers that works best for semantic vector models. Here we show that the compact 2 -category of finite-dimensional semi-modules over a bounded lattice of real numbers handles both the quantum logic of semantic vector models and the functional models.

Section 2 introduces pregroup semantics in both the functional and the categorical versions. Section 3 presents an algorithm transforming one into the other. Section 4 gives an isomorphic embedding of the category of two-sorted functions into the category of semantic vector models over the lattice of real numbers. Follows in Section 5 a sketch of quantum logic in the category of semantic vector models over the lattice of real numbers. Section 6 motivates functions of two-sorted first order logic by their relevance to natural language and defines the structure of a symmetric compact 2 -category of the category of sets and two-sorted functions. In Section 7, we define the interior logic and show by examples that the vector of a sentence is true in the interior logic if and only if the 'usual' first order formula interpreting the sentence holds. The examples include universal quantifiers, negation and relative pronouns. In particular, the interpretation of the relative pronoun introduces a comprehension schema based on the interior truth of the sentence vectors, in accordance with an observation by [Benthem and Doets, 1983] that the comprehension schema holds in two-sorted first order logic for certain families of expressions.

The two semantics

Pregroup grammars are based on compact bilinear logic, also known as pregroup calculus. The set of pregroup types generated by a partially ordered set B = B, ≤ is the free monoid T B generated by the following set whose elements are called simple types

S B = a (z) : a ∈ B, z ∈ Z .
The notation a (z) designates the ordered pair formed by the element a of B and the integer z . A simple type of the form a (0) is identified with a ∈ B and called a basic type. Strings of simple types are called types. By convention, if a type T is given in the form T = t 1 . . . t n , the t i 's are simple types for 1 ≤ i ≤ n .

In the case where n = 0, the string t 1 . . . t n is empty, denoted ǫ . It is the unit for the binary operation of concatenation in the free monoid. Moreover, there are two unary operations ( ) ℓ and ( ) r , called left and right adjoints, defined by (a

(z1) 1 . . . a (zn) n ) ℓ = a (zn-1) n . . . a (z1-1) 1 (a (z1) 1 . . . a (zn) k ) r = a (zn+1) n . . . a (z1+1) 1 .
This definition includes the case where n = 0 . Hence the equalities ǫ ℓ = ǫ = ǫ r hold for the empty string. It follows that a ℓ = (a (0) ) ℓ = a (-1) and a r = (a (0) ) r = a (1) Finally, the binary derivability relation on types, denoted →, is the smallest reflexive and transitive relation satisfying

(Induced step) T x (z) T ′ → T y (z) T ′ (Generalised contraction) T x (z) y (z+1) T ′ → T T ′ (Generalised expansion) T T ′ → T x (z+1) y (z) T ′
where either z is even and x ≤ y or z is odd and y ≤ x. Capitals T , T ′ etc. designate arbitrary types, bold face letters x, y etc. basic types.

It follows that a type T ′ is derivable from type T , if either they are identical strings or there is a sequence T 1 , . . . , T n for which T 1 = T, T n = T ′ and T i → T i+1 is a deduction rule, i.e. an induced step, a generalised contraction or a generalised expansion.

A lexicon is a finite set of triples w : T :: m , where w is a word, T a type and m a meaning expression. The pairs w : T , called entries, are sufficient for syntactic analysis. Following [START_REF] Lambek | From word to sentence[END_REF], such a set of pairs is called a dictionary.

Intuitively, the basic types represent grammatically important notions. For example, the basic types s and n stand for sentences and noun phrases respectively.

A string of words w 1 , . . . , w n is a sentence, if there are entries w 1 : T 1 , . . . , w n :

T n such that T 1 . . . T n → s . Similarly, it is a noun phrase, if T 1 . . . T n → n .
For example, the sentences The boys left and The boys did not leave are recognised by a pregroup grammar with a dictionary containing, among others, the entries all /the : n

2 c 2 ℓ boys : c 2 left : n 2 r sn ℓ did : n 2 r si ℓ d not : d r ii ℓ d leave : d r in ℓ
The basic type c 1 stands for the singular and c 2 for the plural of count nouns, n 1 and n 2 for the singular and the plural of noun phrases. Moreover, n is the type of the noun phrase when the number does not matter, s is the sentence type 1 and i the type of the infinitive. The type d is a 'dummy' type. It incorporates the indices of phrase structure grammars into the syntactic types of pregroup grammars. Finally,

c 1 ≤ n 1 , c 2 ≤ n 2 and n 2 ≤ n so that c 2 n 2 r → ǫ, n ℓ c 2 → ǫ etc. are generalised contractions.
Derivations are presented in the form of a graph, for example

r 0 = all n 2 c 2 ℓ boys c 2 lef t n 2 r s a a d d s (1) r 1 = the n 2 c 2 ℓ boys c 2 did n r s i ℓ d not d r i i ℓ d leave d r i a a d d c c Y Y s (2)
The underlinks mark the generalised contractions. Derivations that use only generalised contractions are called reductions. It follows from a theorem in [START_REF] Lambek | Type grammar revisited[END_REF] that every derivation to a basic type is equivalent to a reduction.

Dictionary entries w : T are sufficient to recognise grammatical strings. To define semantics for pregroup grammars, a meaning expression has to be added to each dictionary entry.

The lexical entries below give two versions of the meaning expressions, namely vectors in the third column and functions in the fourth column. We recall that V and its dual space, V * , are isomorphic and that the basis vectors of W ⊗V * are the vectors b i ⊗a j , where the b i 's vary over the basis vectors of W and the a j 's over those of V . 2 Moreover, W ⊗ V * and V * ⊗ W are isomorphic. A vector v in space V is identified with a linear map v : I → V , where I is a fixed one-dimensional space. A linear map f : V → W is identified with a matrix, i.e. a vector

f ∈ W ⊗ V * . A linear map g : V 1 ⊗ V 2 → W is identified with the bilinear map (v 1 , v 2 ) → g(v 1 ⊗ v 2 ) ∈ W ,
which we also denote g . These identifications rewrite the vectors of the third column of (2) as vectors or maps in the fourth column. The isomorphism in Section 4 gives a more profound connection: The entries in the fourth column are two-sorted functions, namely functions that take elements and sets as arguments and return elements and 1 We ignore the tense here. 2 The 'tensor product' of two vectors is the same as the outer product of the vectors. sets as values. In particular, a 'function' with no arguments can be either an element or a set. The connection between the two versions and how to get from one to the other is the subject of the rest of this paper.

I leave ---→ E * ⊗ S leave(z) did : n 2 r si ℓ d :: I do -→ E * ⊗ S ⊗ S * ⊗ E do(y 2 ) id(y 1 ) not : d r ii ℓ d :: I not --→ E * ⊗ S ⊗ S * ⊗ E not Ω (z 2 ) id(z 1 )
leave: d r in ℓ ::

I leave ---→ E * ⊗ S ⊗ E * leave(x 1 , x 2 )
Here, E and S are distinguished vector spaces. The space E = V U is the finite dimensional space generated by the set U . The elements of U , i.e. the basis vectors of E, are called individuals. The space S = V Ω is two-dimensional. Its basis vectors, the elements of the set Ω = {⊤, ⊥}, are called truth-values. The vector ⊤ = (1, 0) stands for true, ⊥ = (0, 1) for false, -→ 0 = (0, 0) stands for no truth values and the vector -→ 1 = (1, 1) ∈ S for partly true and partly false. The syntactical type determines the space of the meaning vector. Each simple type corresponds to a factor of the tensor product and vice-versa. The basic types c i , n i , d correspond to the space E and the types s, i to S . Right and left adjoints of basic types correspond to the dual spaces, for example

n 2 c 2 ℓ E ⊗ E * n 2 r s i ℓ d E * ⊗ S ⊗ S * ⊗ E c 2 E n 2 r s E * ⊗ S
Suppose the meaning expressions of words are given as functions. The function symbols leave, all, not Ω , id and boy correspond to basic types, the variables to right or left adjoints of basic types

n 2 c 2 ℓ all x c 2 boy n 2 r s z leave .
In order to compute the meaning expression of a sentence replace every simple type in the reduction by the corresponding function symbol and substitute according to the links. For example, Apply the same method to the sentence The boys did not leave. Substitution according to the links results in the compound expression do(not Ω (leave(the(boy))) .

(3)

On the other hand, to construct the vector representing a sentence, form the tensor product of the word vectors and compose it with the reduction. 3 The composition is legitimate, because reductions define 2 -cells in the free compact 2 -category and in particular linear maps of vector spaces. The meaning expressions in vector notation identify with linear maps of domain I. Therefore they are morphisms of a compact closed category and as such are representable by graphs. Compute the meaning expression of a sentence by the following instructions

• replace the morphisms by their graphs

I all --→ E ⊗ E * I boy --→ E I leave ---→ E * ⊗ S I Ð Ð all E ⊗ E * I E boy I leave 1 1 E * ⊗ S
• join the graphs by the tensor product

Ð Ð all I 1 1 boy (E ⊗ E * ) ⊗ (E) ⊗ (E * ⊗ S) leave
• compose this product with the linear map r ′ 0 defined by the reduction ( 1)

m(all boys lef t) = r ′ 0 • (all ⊗ boy ⊗ leave) = Ð Ð all W W d d S I 1 1 boy (E ⊗ E * ) ⊗ (E) ⊗ (E * ⊗ S) leave = leave•all•boy I S = leave(all(boy))
The logical content of all is captured by the postulate all = id E , from which it follows that leave(all(boy)) = leave(boy) .

(4)

The graph of the is that of all except for the label. The graphical representation of the vectors do :

I → E * ⊗ S ⊗ S * ⊗ E and not : I → E * ⊗ S ⊗ S * ⊗ E are do = I 6 6 | | do E * ⊗ S ⊗ S * ⊗ E not = I 6 6 | | notΩ E * ⊗ S ⊗ S * ⊗ E
Again, we form the tensor product and compose it with the linear map corresponding to the reduction (2)

r ′ 1 • (the ⊗ boy ⊗ do ⊗ not ⊗ leave) = Ð Ð the X X 5 5 ~do S d d c c 5 5 Ð Ð I x x p p p p p p p p p p p p p p p p p p d d a a 2 2 boy E ⊗ E * ⊗ E ⊗ E * ⊗ S ⊗ S * ⊗ E ⊗ E * ⊗ S ⊗ S * ⊗ E ⊗ E * ⊗ S notΩ leave = do(not Ω (leave(the(boy)))
The righthand expression in the equality above coincides with the expression (3) computed by substitution, confirming the slogan 'substitution in logic is composition in categories'. The auxiliary do in the negated sentence has only a syntactic purpose, it does not influence the meaning. This is expressed by postulate do = id S .

(5) do(not Ω (leave(the(boy))) = not Ω (leave(the(boy))) .

Similarly, the logical content of the word not is captured by requiring that not Ω : S → S is the negation of truth-values

not Ω (⊤) = ⊥ not Ω (⊥) = ⊤ . ( 7
)
The semantics is clearly compositional in both versions. The vector approach does not require variables and is invariant under change of order. The latter is guaranteed by the following lemma Lemma 1. The meaning vector of a sentence is strictly invariant under permutation of the word meanings.

Proof. Indeed, the tensor product is symmetric up to isomorphism. If we compose the tensor product of the word vectors with the permutation σ, we must compose the inverse σ -1 with the reduction r to obtain a reduction of the permuted tensor product. Hence

r •(w 1 ⊗. . .⊗w n ) = (r •σ -1 )•(σ •(w 1 ⊗. . .⊗w n )) = (r •σ -1 )•(w σ(1) ⊗. . .⊗w σ(n) ) .
Variable-free functional expressions and invariance of the expression under change of order in the arguments are the first two postulates concerning compositional semantics formulated in [START_REF] Kracht | The emergence of syntactical structure[END_REF]. The third and last postulate, which says that arguments may not be repeated, is also satisfied. The example of the relative pronoun who in Section 7 illustrates how multiple occurrences are avoided.

Examples

The value of the meaning-expression of a sentence depends on the value of the meaning expressions of the words. Consider two examples and M 2 . The former represents a situation where all of the boys present in the room left, whereas in the latter, the boys did not leave. Let boy = {a 1 , . . . , a m } be the set of boys in question. The interpretations of leave differ in M 1 and M 2 , namely

M 1 M 2 leave 1 (a i ) = ⊤ leave 2 (a i ) = ⊥ 1 ≤ i ≤ m . (8)
We refer the reader to Section 7 to see that

leave 1 (boy) = ⊤ not Ω (leave 1 (boy)) = ⊥ leave 2 (boy) = ⊥ not Ω (leave 2 (boy)) = ⊤ .
In a third situation M 3 , only the boys a 1 and a 2 left and the others stayed behind.

M 3 leave 3 (a i ) = ⊤ leave 3 (a i ) = ⊥ 1 ≤ i ≤ 2 3 ≤ i ≤ m .
In this case, leave 3 (boy) = {⊤, ⊥} and not Ω (leave 3 (boy)) = {⊤, ⊥} .

3 An algorithm from functional semantics to vector semantics

The algorithm translates function expressions to vector expressions, preserving the meaning of grammatical strings of words. It decomposes into five routines, called 'Map', 'Glue', 'Diagonal', 'Name', 'Rearrange'. They are executed in that order, but the routines 'Glue', 'Diagonal' and 'Rearrange' do not always apply. The first example concerning sentence negation does not use the routine 'Diagonal'. The second example uses all five routines and concerns the relative pronoun.

3.1 The routines 'Map', 'Glue' , 'Name', 'Rearrange'

Recall the entries all : n 2 c 2 ℓ :: all(x) did : n r si ℓ d :: do(y 2 ) id(y 1 )

not : d r ii ℓ d :: not Ω (z 2 ) id(z 1 ) leave : d r i :: leave(z)
and the correspondence of simple types and symbols

n 2 c 2 ℓ all x n 2 r s i ℓ d y 1 do y 2 id d r i i ℓ d z 1 not Ω z 2 id d r i z leave Routine 'Map'
-read each function as map with domain and codomain, respecting the correspondence of simple types and spaces

c 2 ℓ n 2 x all I all --→ E i ℓ s n 2 r d y 2 do y 1 id S do -→ S E id -→ E i ℓ i d r d z 2 not Ω z 1 id S notΩ ---→ S E id -→ E d r i x leave E leave ---→ S Routine 'Glue'
-glue the maps arising in the same lexical entry together with the help of the tensor product, recopying the correspondence of simple types and spaces

S ⊗ E do⊗id ----→ S ⊗ E S ⊗ E notΩ⊗id -----→ S ⊗ E i ℓ n 2 r s d i ℓ d r i d
Routine 'Name' -replace the linear maps by their names, that is to say the vector designating the matrix associated to a linear map. Keep track of the correspondence between factors and simple types

I boy =boy ------→ E I do⊗id -----→ E * ⊗ S * ⊗ S ⊗ E c 2 n 2 r i ℓ s d I leave -----→ E * ⊗ S I notΩ⊗id -------→ E * ⊗ S * ⊗ S ⊗ E d r i d r i ℓ i d
Routine 'Rearrange' -rearrange the factors in the order in which the simple types occur in the syntactical type. To do so, compose the name with the appropriate permutation

all = c • all : I → E * ⊗ E c 2 ℓ n 2 do = c ′ • do ⊗ id : I → E * ⊗ S ⊗ S * ⊗ E n 2 r s i ℓ d not = c ′ • not Ω ⊗ id : I → E * ⊗ S ⊗ S * ⊗ E d r i i ℓ d
where c : E ⊗ E * → E * ⊗ E permutes the two factors and c ′ :

E * ⊗ S * ⊗ S ⊗ E → E * ⊗ S ⊗ S * ⊗ E
switches the second and the third factor.

The routine 'Diagonal'

The next example involves the relative pronoun who and uses the routine 'Diagonal'. The lexical entries concerning the noun-phrase the boys who left are the : n 2 c 2 ℓ :: the(x) boys : c 2 :: boy

who : c 2 r c 2 s ℓ n 2 :: who(x 1 , x 2 ) id(x 1 ) left : n 2 r s :: leave(z) .
Note that the interpretation of who : c 2 r c 2 s ℓ n 2 has a property not encountered previously. A variable, namely x 1 , occurs in more than one functional expression. The algorithm constructs the corresponding vector

who : I → E * ⊗ E ⊗ S * ⊗ E
with the help of the new routine 'Diagonal' below.

The correspondence between symbols and simple types is

the x n 2 c 2 ℓ boy c 2 x 1 who id x 2 c 2 r c 2 n 2 s ℓ z leave n 2 r s .
using the reduction, compute the meaning expression of the noun-phrase the boys who left the(who(boy, leave(id(boy)))) = the(who(boy, leave(boy))) .

The translation algorithm first executes 'Map' 'Glue'

E ⊗ S who --→ E E id --→ E c 2 r s ℓ c 2 c 2 r n 2 E ⊗E ⊗S id E ⊗who -----→ E ⊗E c 2 r c 2 r s ℓ n 2 c 2 .
The simple type c 2 r occurs twice in the tensor product, whereas it has only one occurrence in the lexical entry. Equivalently, the variable x 1 'lives' in two different factors of the argument space where there should be only one. This is [START_REF] Kracht | The emergence of syntactical structure[END_REF]'s requirement that arguments may not be repeated. The solution here is the diagonal, i.e. the linear map d E : E → E ⊗ E that maps each basis vector a to a ⊗ a .

Routine 'Diagonal' -form the tensor product of the diagonal d E with the identity of the other factor(s) so that the 'adjusted' the diagonal can be composed with id E ⊗ who

E ⊗ S d E ⊗id S -----→ E ⊗ E ⊗ S c 2 r s ℓ c 2 r c 2 r s ℓ E ⊗ S (id E ⊗who)•(d E ⊗id S ) -------------→ E ⊗ E c 2 r s ℓ c 2 n 2 .
The next two routines are 'Name' and 'Rearrange', namely

I (id⊗who)•(d E ⊗id S ) --------------→ E * ⊗ S * ⊗ E ⊗ E c 2 r s ℓ n 2 c 2 and who = c • (id ⊗ who) • (d E ⊗ id S⊗E ) : I → E * ⊗ E ⊗ S * ⊗ E , (9)
where c :

E * ⊗ S * ⊗ E ⊗ E → E * ⊗ E ⊗ S * ⊗ E c 2 r s ℓ n 2 c 2 c 2 r c 2 s ℓ n 2 .
makes two exchanges, namely first between the last two factors and then between the third and the second factor.

Noun-phrases formed with the relative pronoun

The strings boys who left and the boys who left have both a reduction to a basic type, namely

r 3 = a a c 2 d d boys who left ( c 2 ) (c 2 r c 2 s ℓ n 2 ) (n 2 r s)
and

r 4 = (n 2 c 2 ℓ ) ( c 2 ) (c 2 r c 2 s ℓ n 2 ) (n 2 r s) n 2 d d ` b b the boys who left .
Finally, the equality (9) above defines the representation of who by the graph

who : I → E * ⊗ E ⊗ S * ⊗ E = I id 5 5 5 5 who E * ⊗ E ⊗ S * ⊗ E .
Compose the tensor product of the word vectors with the reduction to obtain

m(boys who left) = r ′ 3 • (boy ⊗ who ⊗ leave) = W W id 5 5 4 4 E Ð Ð d d `4 4 leave I boy } } | | | | | | | | | | | | who (E ) ⊗ (E * ⊗ E ⊗ S * ⊗ E) ⊗ (E * ⊗ S
E ⊗ E * ⊗ E ⊗ E * ⊗ E ⊗ S * ⊗ E ⊗ E * ⊗ S
= the(who(boy, leave(boy))

The isomorphism

In Information Retrieval Systems, words are represented by vectors of some fixed finite dimensional space. The coordinates of the vector are in general obtained by a frequency count of occurrences of words in documents. Hence, without loss of generality, we may assume that the coordinates belong to the real interval I = [0, 1] . The linear order of real numbers induces a distributive and implication-complemented lattice structure on

I α ∨ β = max {α, β} α ∧ β = min {α, β} α → β = sup {γ ∈ I : α ∧ γ ≤ β} ¬α = α → 0 .
Clearly, α → β = 1 if and only if α ≤ β . I becomes a semi-ring with the operations

α + β = α ∨ β α • β = α ∧ β .
An I-space is an arbitrary finite-dimensional semi-module over I. The semi-ring I is identified with a one-dimensional space, also denoted I . The sum of vectors

v = α 1 a 1 +• • •+α n a n ∈ V and w = β 1 a 1 +• • •+β n a n ∈
V and the multiplication with a scalar α ∈ I are defined as usual, namely

v + w = (α 1 + β 1 )a 1 + • • • + (α n + β n )a n αw = (α • β 1 )a 1 + • • • + (α • β n )a n .
In particular, α(αv) = (α•α)v = αv = (α+α)v = αv+αv . An easy computation shows that every I-space V has a unique set A of basis vectors. We write V = V A . Orthogonality, inner and outer product of vectors are defined like in a vector space over the field of real numbers. As all coordinates are non-negative, vectors are orthogonal in the semi-module over I if and only if they are orthogonal in the vector space over the field of real numbers. The norm 4 of a vector is given by

α 1 a 1 + • • • + α n a n = sup {|α i |, 1 ≤ i ≤ n} = n i=1 α i .
The definitions of linear maps, matrix representation of linear maps and multiplication of matrices also remain unchanged. For example, a linear map f :

V A → V B satisfies f ( - → 0 ) = - → 0 f ( n i=1 α i a i ) = n i=1 α i f (a i ) .
Clearly, every linear map is defined by its values on the basis vectors. Its matrix is identified with a vector f ∈ V * A ⊗ V B , the tensor product of the dual space V * A of V A and V B . The coordinates of f , i.e. the entries of the matrix, are determined as usual. Indeed, let A = {a 1 , . . . , a n } and B = {b 1 , . . . , b m } . The dual space V * A is isomorphic to V A and therefore the vectors

a i ⊗ b j , 1 ≤ i ≤ n, 1 ≤ j ≤ m form a basis of V * A ⊗ V B . Then f = i,j γ i,j (a i ⊗ b j ) ,
where γ i,j is the j-th coordinate of the vector f (a i ).

Examples of linear maps are the identity id V A and the diagonal d V A : V A → V A ⊗ V A , namely the linear map that sends a basis vector to the outer product with itself

d V A (a) = a ⊗ a, for a ∈ A . Note that d V A (v) = v ⊗ v if v is not a basis vector. Indeed, d V A ( n i=1 α i a i ) = n i=1 α i (a i ⊗ a i ) whereas ( n i=1 α i a i ) ⊗ ( n i=1 α i a i ) = 1≤i,j≤n (α i α j )(a i ⊗ a j ) .
4 norm advocated for context-theoretical semantics in [START_REF] Clarke | Context-theoretic Semantics for Natural Language, an algebraic framework[END_REF] Linear maps of I-spaces are closely related to the functions interpreting lexical entries of pregroup grammars in two-sorted first order predicate logic. Definition 1. A function g : A → B is two-sorted if it maps elements and subsets of A to elements or subsets of B and satisfies Given an I-space V A , generated by a set of basis vectors A = {a 1 , . . . , a n }, define a map I A from V A to the set of subsets of A by

g({a}) = g(a) for a ∈ A g(∅) = ∅ g(X ∪ Y ) = g(X) ∪ g(Y ) for X, Y ⊆ A .
I A (β 1 a 1 + • • • + β n a n ) = {a i ∈ A : β i = 0} .
From the definition follows that

I A (v + w) = I A (v) ∪ I A (w) I A ( - → 0 ) = ∅ .
Conversely, given a set A = {a 1 , . . . , a m }, define a map J A from the set of subsets of A to the space V A thus

J A (X) = n i=1 α i a i , where α i = 1 if a i ∈ X and α i = 0 else . Clearly, for X, Y ⊆ A J A (X ∪ Y ) = J A (X) + J A (Y ) J A (∅) = - → 0 .
Finally, extend J A to elements by

J A (a) = J A ({a}) .
Given a set A and a two-sorted function g : A → B, let

J (A) = V A
and J (g) : J (A) → J (B) be the linear map defined on the basis A by

J (g)(a) = J B (g(a)
), for all a ∈ A .

Lemma 2. For every subset X ⊆ A and every two-sorted map g : A → B the following holds

I A • J A (X) = X (I • J )(g) = g .
Moreover, if the coordinates of v ∈ V A are 0 or 1 respectively the entries of the matrix of f : V A → V B are 0 or 1, then

J A • I A (v) = v (J • I)(f ) = f .
Proof. To see the first equality, let J A (X) = n i=1 α i a i . By definition of I A , a i ∈ I A (J A (X)) if and only if α i = 0. By definition of J A , the latter holds if and only if a i ∈ X .

It suffices to show the second equality for elements, because its left and right hand expressions are two-sorted functions. Let a ∈ A. Then

(I • J )(g)(a) = I(J (g))(a) = I B (J (g)(a)) by (11) = I B (J B (g(a)) by (12) = (I B • J B )(g(a)) = g(a)
by the first equality .

The other equalities are proved similarly.

The equalities J A • I A (v) = v and (J • I)(f ) = f do not hold in general. Vectors with coordinates different from 0 and 1 are 'lost' by the map J A • I A . Only the restriction of I A to vectors with coordinates in {0, 1} is a one-one map onto the set of subsets of A .

Theorem 1. J and I preserve identities, commute with composition, identify unions of sets with sums of spaces, products of sets with tensor products of spaces, the two-sorted diagonal with the linear diagonal and graphs of functions with matrices of linear maps.

The proof is straightforward, but notationally unpleasant, because there are only vectors in vector spaces, whereas the image of a space needs elements and subsets. The next section introduces a better notation for two-sorted functions and we come back to the proof then. In fact, natural language, where twosorted functions are ubiquitous, also uses them in a 'sloppy' way compared to set-theory.

5 Logic of concepts I-spaces accommodate both the functional logic of sentences and the propositional logic of semantic vector models. The link between the two is quantum logic of semi-modules over the lattice of real numbers. The point of view presented is taken from [START_REF] Preller | Quantum logic unites compositional functional semantics and distributional semantic models[END_REF].

According to [START_REF] Van Rijsbergen | The Geometry of Information Retrieval[END_REF], quantum logic for Information Retrieval Systems refers to the lattice structure of subspaces of a space over the field of real numbers. Every subspace is identified with a projector, namely the linear map that takes its values in the subspace and leaves every vector of the subspace invariant. Subspaces stand for words or combinations of words constructed with the help of the propositional connectives given by

¬E = E ⊥ , E ∨ F = E ⊕ F, E ∧ F = E • F, E → F = {v : F (E(v)) = E(v)} .
In general, the lattice structure is not distributive.

The same definitions in an I-space E = V A result in a distributive lattice of subspaces. Moreover, the order of the real interval I introduces a lattice structure on the vectors of V A , isomorphic to the lattice structure of subspaces of V A . The isomorphism J maps the Boolean algebra of subsets of A to the lattice of subspaces generated by subsets of A . Hence the lattice of subspaces for an arbitrary I-space includes a Boolean sublattice.

In a semantic vector model, words are represented by vectors of a finite dimensional space over the real numbers. One may assume without loss of generality that the coordinates belong to the interval I = [0, 1], because the number of words is finite. There are two kinds of semantic vector models. In one, the basis vectors are identified with words, in the other one with strings of words. In the first, the coordinates of the vectors result from a frequency count in context windows. In the second, they are given by a probability distribution on a set of strings. Both are used for detecting similarity of words or for choosing a particular meaning among the possible meanings of a word.

The string approach seems more appropriate for compositional semantics. In this case, arbitrary vectors can be viewed as concepts and the quantum connectives define the logic of concepts.

Indeed, the logical properties of quantum logic render faithfully the intuitive logical properties of words in the particular case where the I-space is a tensor product of two-dimensional spaces. Words are classified by a thesaurus, be it the mental thesaurus of the speaker or an explicit thesaurus. For a given set of key-words or basic concepts P = {p 1 , . . . , p n }, the vectors of the tensor product

C(P ) = V {p 1⊤ , p 1⊥ } ⊗ . . . ⊗ V {p n⊤ , p n⊥ }
represent concepts. In particular, the words classified by the thesaurus are Boolean combinations of basic concepts. The sublattice of subspaces generated by basis vectors is isomorphic to the free Boolean algebra B(P ) generated by P . The geometrical properties of C(P ) reflect faithfully the logical properties of words. Concept spaces are the linguistic analogue to the tensor products of two-dimensional Hilbert spaces representing compound systems in quantum mechanics.

Note that V {p i⊤ , p i⊥ } is a notational variant of V Ω . Moreover, Ω is identified with the two-element Boolean algebra B(∅) of truth values. Hence the isomorphism transforms the Boolean connectives to linear maps. For example, the truth-value negation

J (¬) = not Ω : V Ω → V Ω , which satisfies not Ω ( - → 0 ) = - → 0 , not Ω (⊤) = ⊥, not Ω (⊥) = ⊤, not Ω (⊤ + ⊥) = ⊥ + ⊤ .
Thus, the compact closed category of I-spaces includes both the functional models based on 2-sorted logic and the semantic vector models based on quantum logic.

6 Natural language in two-sorted first order logic It follows from Section 4 that the functional expressions in a pregroup lexicon are two-sorted functions. Functions in two-sorted first order logic were used in [START_REF] Preller | Toward discourse representation via pregroup grammars[END_REF] for pregroup semantics. Their relevance for natural language, however, goes back to the fact that two-sorted first order logic is equivalent to second order logic with general models, established in [Benthem and Doets, 1983].

Two-sorted first order logic, 2-FOL, has two sorts, one for elements and one for sets, a primitive relational symbol ∈ requiring elements on the left and sets on the right, and an equality symbol = accepting either sets on both sides or elements on both sides. Formulae are defined as usual, except that there are two sorts of quantifiers, namely ∃ x , ∀ x for elements and ∃ X , ∀ X for sets. The function(al symbol)s take elements and subsets as arguments and return elements or subsets. The two-sorts are reflect the fact that verbs may take singulars and plurals as arguments. 2-FOL provides a meta-language in which to define and prove the properties of the two-sorted functions interpreting words and grammatical expressions.

We introduce several operators on sets and elements and justify them by their use in natural language.

-The first operation is the two-sorted product defining both the ordered pair of elements and the Cartesian product of sets

prod(a, b) = a, b prod(a, B) = {a} × B prod(A, b) = A × {b} prod(A, B) = A × B
The two-sorted product is the counterpart of the tensor product, also a single operator defined both for vectors and spaces. The two-sorted product provides the argument set for transitive verbs.

-The second operator is the two-sorted union. It combines the set-theoretical operators 'unordered pair of elements' and 'union of sets' The single notation and stems from the meaning of the word and in Eva and Sue respectively boys and girls. It occurs in the lexical entries and : n 1 r n 2 n 1 ℓ :: and(x 1 , x 2 ), and : n 2 r n 2 n 2 ℓ :: and(x 1 , x 2 ) .

Note that and(a, a) = {a} and and(A, A) = A . Therefore and(A, A) = {A}. In fact, closure under the two-sorted union does not imply that a set exists which has the set A as element.

The operation of two-sorted union is the companion to the sum of vectors and spaces. Hence the property of commuting with two-sorted unions is the companion to the property of commuting the the sum in vector spaces. The established one-sorted set-theoretical notation is cumbersome when it comes to two-sorted logic. Here is an example what 'commuting with two-sorted unions' looks like in one-sorted notation.

Lemma 3. A function f that maps elements and sets to elements or sets commutes with the two-sorted union and if and only if it satisfies

f ({a}) = {f (a)} if f (a) is an element f ({a}) = f (a) if f (a) is a set f (A ∪ B) = f (A) ∪ f (B) if f (A) and f (B) are sets f (A ∪ B) = {f (A)} ∪ f (B) if f (A) is an element and f (B) a set f (A ∪ B) = f (A) ∪ {f (B)} if f (A) is a set and f (B) an element f (A ∪ B) = {f (A)} ∪ {f (B)} if f (A) and f (B) are elements
Proof. f (and(a, a)) = f ({a}) . On the other hand, and(f (a), f (a)) is equal to {f (a)} if f (a) is an element and to f (a) if it is a set. Hence, if f commutes with and the first two equalities hold. Similarly, f (and(A, B)) = f (A ∪ B) . Again, it suffices to express and(f (A), f (B)) in terms of union and unordered pair formation to see that the last four equalities hold if f commutes with and.

The problem is that f (a) can be an element or a set. Without the notational distinction between f (a) and {f (a)} the six equalities above are equivalent to the two equalities f ({a}) = f (a) and f (A ∪ B) = f (A) ∪ f (B) . We resolutely write f ({a}) = f (a) from now on, even if f (a) is an element. Hence the two-sorted functions of Definition (10) are exactly the functions which map the empty set to itself and commute with the two-sorted union.

The relative pronoun who is an example of a two-sorted function in natural language. The noun phrase the boys who entered the room may be refer to nobody, a single boy or several boys. Moreover, the boys and girls who entered the room is the union of the boys who entered the room and the girls who entered the room. We take the point of view that all meaning expressions in a pregroup lexicon refer either to elements or to sets or to two-sorted functions and illustrate this with some in particular, the quantifiers and determiners in the next section.

Before we can prove Theorem 4, we need an operation which transforms two-sorted function g : A → B into a set g , called the graph of g With the understanding that 'union' means 'two-sorted union' and 'product' means 'two-sorted product' in Theorem 1, its proof is indeed straight forward.

As an example, we show that I maps matrices to graphs:

Assume that f :

V A → V B is linear. Let f (a i ) = m j=1 β ij b j . From I(f )(a i ) = I B (f (a i )) follows that a i , b j ∈ I(f ) if and only if β ij = 0 . Hence I A * ⊗B ( f ) = I(f ) .
After identification of vectors in A * ⊗ B with linear maps from I to A * ⊗ B, this equality becomes

I( f ) = I(f ) .
Two-sorted functions are closed under composition. They include the constant functions, the unary functions obtained from the two-sorted union by making one argument equal to the empty set, and the projections of a product set onto the factors.

Remark : If A is finite every function that maps elements of A to elements of B extends uniquely into a two-sorted function from A to B. In particular, every relation of first order logic can be viewed as a two-sorted function that sends elements to truth-values, more precisely Definition 2. A predicate is a two-sorted function f : A → Ω such that

∀ x (x ∈ A =⇒ f (x) ∈ Ω) .
Note that the value of a predicate on a subset with more than two elements may be a set, namely {⊤, ⊥} . Moreover, predicates are closed under composition.

We conclude this section with a fundamental property of predicates. The interpretation of quantifiers by two-sorted functions is based on this property. Lemma 4. [Fundamental Lemma] Assume that f maps elements to elements. Then the following holds Fundamental Property For all finite X ⊆ A and all b ∈ f (A)

f (X) = b ⇔ (X = ∅ and f (a) = b for all a ∈ X) . (13)
Proof. If f (X) = b for some b ∈ f (A) then X is not the empty set, because two-sorted functions map the empty set to the empty set. Assume that

X = {a 1 , . . . , a n } . Then f (X) = f ({a 1 } ∪ • • • ∪ {a n }) = {f (a 1 )} ∪ • • • ∪ {f (a n )},
because f commutes with finite unions. By assumption, no f (a i ) is the empty set. Hence the equivalence follows.

7 The logic of sentences

The Fundamental Property provides the explanation how quantifiers can be captured by two-sorted functions. We explain this for universal quantifiers. A detailed development of the behaviour of quantifiers and determiners is beyond the scope of this paper. We use functional notation when discussing the meaning of sentences, vector notation when computing it. The first and second sentence have the same meaning and so do the third and fourth. Obviously, the meaning of the latter two sentences is not the logical negation of the meaning of the first two. Accordingly, the first order formulas rendering S 1 and S 2 are not equivalent.

S 1 ∀a(a ∈ boy =⇒ a ∈ leave) S 2 ∀a(a ∈ boy =⇒ a ∈ leave) .

In our formalisation, relations are represented by functions with values in Ω S 1 ∀a(a ∈ boy =⇒ leave(a)) = ⊤) S 2 ∀a(a ∈ boy =⇒ leave(a)) = ⊥) .

Recall the postulate all = id E . Similarly, we require the = id E .

Accordingly, the meaning expression m(All boys left) computes to leave(all(boy)) = leave(boy) = leave(the(boy)) .

Under the assumption that the set boy is not empty, the equivalence below is an instance of the Fundamental Property and therefore holds in 2-FOL leave(boy) = ⊤ ⇐⇒ ∀a(a ∈ boy =⇒ leave(a)) = ⊤) .

The assumption boy = ∅ cannot be proved. Telling someone that All/The boys left in a situation where there are no boys would provoke the question Which boys?. We ignore the problems arising when there is no obvious referent for the count-noun.

The sentences The boys do not leave and No boys left also have the same intuitive meaning. They are rendered by the first order formula ∀a(a ∈ boy =⇒ leave(a) = ⊥) .

The meaning expression of The boys did not leave is given by (6) in Section 2 as not Ω (leave(the(boy))) .

From ( 14) follows m(The boys did not leave) = not Ω (leave(boy)) .

The lexical entry for the word no also involves the universal quantifier id and the sentence negation not Ω no: ss ℓ n 1 c 1 ℓ ::

I no -→ S ⊗ S * ⊗ E ⊗ E * not Ω (z 1 ) id(z 2 ) no: ss ℓ n 2 c 2 ℓ :: I no -→ E * ⊗ S ⊗ S * ⊗ E not Ω (z 1 ) id(z 2 ) .
The graph of the vector no is

no : I → S ⊗ S * ⊗ E ⊗ E * = I Ò Ò notΩ Ñ Ñ S ⊗ S * ⊗ E ⊗ E *
The meaning expression of the sentence No boys left is computed by the following graph, where the underlinks are given by the reduction

m(No boys left) = r ′ 2 • (no ⊗ boy ⊗ leave) = S Ò Ò notΩ V V Ñ Ñ e e g g I Ø Ø ) ) (S ⊗ S * ⊗ E ⊗ E * ) ⊗ (E ) ⊗ (E * ⊗ S) boy leave
= not Ω (leave(boy)) .

We prove the equivalence not Ω (leave(boy)) = ⊤ ⇔ ∀a(a ∈ boy =⇒ leave(a) = ⊥) .

Consider the lefthand equality. It is equivalent to leave(boy)) = ⊥, because ⊤ is the only element or subset of Ω mapped by not Ω to ⊥ by (7). To conclude, it suffices to remark that the Fundamental Property (13) implies leave(boy)) = ⊥ ⇐⇒ ∀a(a ∈ boy =⇒ leave(a) = ⊥) .

Examples, continued

Return to the Examples (8) in Section 2. The statement All boys left holds in the interior logic of the model M 1 , whereas the statement The boys did not leave holds in M 2 . Indeed, leave 1 (boy) = leave 1 (

1≤i≤m a i ) = ⊤ .
Similarly, leave 2 (boy) = ⊥ and therefore not Ω (leave 2 (boy) = ⊤ .

In the third example M 3 , only the boys a 1 and a 2 left. In this case, leave 3 (boy) = {⊤, ⊥} and not Ω (leave 3 (boy)) = {⊤, ⊥} .

Indeed, the two-sorted functions leave and not Ω commute with unions leave 3 (boy) = leave 3 (({a 1 , a 2 } ∪ {a 3 , . . . , a m }) = leave 3 ({a 1 , a 2 }) ∪ leave 3 ({a 3 , . . . , a m }) = {⊤, ⊥} .

Therefore not Ω (leave 3 (boy)) = not Ω ({⊤, ⊥}) = {not Ω (⊤)} , {not Ω (⊥)} = {⊥, ⊤} .

The equality partitions boy in two non-empty sets, namely the part for which leave 3 is true and another part for which it is false. In fact, these parts are constructed by the two-sorted function (linear map) that interprets the relative pronoun who.

Comprehension

The logical meaning of the relative pronoun who is captured by the axiom

who(a, b) = a if b = ⊤ ∅ if b = ⊥
which defines the two-sorted map who : E × S → E entirely.

Lemma 5. For every predicate f : E → S, the following equivalence holds ∀x (x ∈ who(A, f (A)) ⇐⇒ (x ∈ A and f (x) = ⊤)) .

(15)

Proof. The functions who and f commute with two-sorted unions and so does the composed function

x → who(x, f (x)) = (who

• (id E × f ) • d E )(x).
By definition, who(a, f (a)) = a if f (a) = ⊤ who(a, f (a)) = ∅ else .

Let A = {a 1 , . . . , a n } = n i=1 {a i } . Then who(A, f (A)) = (who

• (id E × f ) • d E )( n i=1 a i ) = (who • (id E × f ))( n i=1 a i , a i ) = who( n i=1 a i , f (a i ) ) = n i=1 who(a i , f (a i )) .
It follows that x ∈ n i=1 who(a i , f (a i )) if and only if x = a i for some a i ∈ A such that f (a i ) = ⊤.

For example in M 3 who(boy, leave 3 (boy)) = {a 1 , a 2 } who(boy, not Ω (leave 3 (boy))) = {a 3 , . . . , a m } .

The property expressed in (15) can be reformulated thus Theorem 2. The comprehension schema holds for predicates Proof. Indeed, who(A, f (A)) is a well defined set. Hence it suffices to put {x ∈ A : f (x) = ⊤} = who(A, f (A)) .

Conclusion

The semantics proposed here is compositional. Its vectorial version satisfies the postulates of [START_REF] Kracht | The emergence of syntactical structure[END_REF], namely meanings do not involve variables and are invariant under change of order or multiplicity. Moreover, the meaning of a statement is true in the interior logic if and only if the corresponding closed first-order formula holds in two-sorted first order logic.

Compact closed categories unite the distributional semantic vector models based on concepts and the functional semantics based on individuals in a common frame. Work on the relation between the vectors given by pregroup semantics and the vectors given by a probability distribution shows promising results in [START_REF] Clark | Concrete compositional sentence spaces[END_REF].

The algorithm that computes the meaning of a string of words from the meanings of the words is proportional to the length of the string. The reduction intervening in the computation is provided by the cubic parsing algorithm for pregroup grammars. Hence, pregroup lexicons that list not only the syntactic types of words, but also the meaning expressions provide an efficient tool for transforming text to formal semantical expressions commonly used in knowledge representation. Admittedly, the fragments of natural language covered so far are insufficient for applications. However, meta-rules in the style of [START_REF] Lambek | From word to sentence[END_REF] make the creation of comprehensive lexicons quite efficient.

  [z| all(x)] and [x| boy]. The expression obtained is leave(z)[z|all(x)][x|boy] = leave(all(boy)) .

=

  who • (boy ⊗ (leave • boy)) = who(boy, leave(boy)) and m(the boys who left) = r ′ 4 • (the ⊗ boy ⊗ who ⊗ leave) =

  two-sorted function defined on a finite set is determined by the values on elements. Examples are two-sorted diagonal two-sorted identity d(a) = a, a d(A) = { a, a : a ∈ A} id(a) = a, id(A) = A .

  every linear map f : V A → V B , the two-sorted function I(f ) : I(V A ) → I(V B ) determined by I(f )(a) = I B (f (a)), for all a ∈ A .

  and(a, b) = {a, b} and(a, B) = {a} ∪ B and(A, b) = A ∪ {b} and(A, B) = A ∪ B .

g

  = { a, b ∈ A × B : a ∈ A, b ∈ B and either b = g(a) or b ∈ g(a)} .

  Definition 3. A sentence w 1 . . . w n is true in the interior logic if its meaning expression m(w1 . . . w n ) satisfies m(w 1 . . . w n ) = ⊤ holds in 2-FOL.Note that leave(boy) = ⊤ is not equivalent to leave(boy) = ⊥, because {⊤, ⊥} is another possible value. For all elements a ∈ boy, however, leave(a) = ⊤ is equivalent to leave(a) = ⊥ . Consider the sentences

	S 1	All boys left The boys left	S 2	The boys did not leave No boys left .

† Support by TALN/LIRMM is gratefully acknowledged ‡ Support by EPSRC is gratefully acknowledged

In a first approach, we could take the meaning of a sentence to be the tensor product of the meanings. But then every string of words would have a meaning.

Acknowledgement

The authors would like to thank two anonymous referees for constructive comments.