Dinh-Vu Nguyen

Ludivine Hugoni

Miriam Filippi

Francis Perton

Da Shi

Emilie Voirin

Laura Power

Geoffrey Cotin

Marie -Pierre Krafft

Arnaud Scherberich

Philippe Lavalle

Sylvie Begin-Colin

Delphine Felder-Flesch

Mastering bioactive coatings of metal oxide nanoparticles and surfaces through phosphonate dendrons

We reported herein an efficient method for constructing dendritic bisphosphonic acid tweezers of generations 1 and 2, which have been proven as versatile surface coatings for metal oxides implant or nanoparticles. These procedures delineated a practical and general route to a library of functional dendrons. Several of these dendritic architectures were successfully tested as biocompatible coverings for iron oxide nanoparticles through in vitro assays, but also as antifouling surface coatings for silica through Quartz Crystal Microbalance studies or as stabilizing structure for magnetic nanoparticles-microbubbles conjugates thanks to preliminary Langmuir monolayers studies.

Introduction

Medicine is changing. [START_REF] Shryock | [END_REF] New technologies are revolutionizing therapeutic treatments, in various domains such as preventive medicine or diagnosis, [2] management of diseases or medical implants. [3] A multidisciplinary research at the interface of materials and surface chemistry, biology, physics and medicine paves the way to a new era, in which innovative strategies could strongly improve early diagnosis of diseases, patient's comfort, with reduced intervention time and an unprecedented efficiency. Applications of nanoscience and nanotechnologies to biomedical and clinical purposes raise then strong expectations, [4] especially in three specific medical domains, namely: early diagnosis, [5] targeted drug delivery [6] and regenerative surgery. [7] Indeed, throughout the last decades, the development of nanosized objects has gathered significant attention from the scientific community. [8] For instance, in the field of medical imaging, many techniques (radiography, magnetic resonance imaging (MRI), scintigraphy, echography) could be implemented by the use of so called theranostic objects, [9] namely materials capable of combining diagnostic and therapeutic activity in one single platform. However, early diagnosis and effective treatment are not the only challenges that nanoscience may address. Indeed, many devices dedicated to medical implantation require robust surfaces [10] whose properties do not change over time, and in this regards, simple and effective solutions are still being sought by manufacturers. Moreover, the development of smart surfaces to avoid microbial colonization is also necessary, [11] for instance for engineering cardiac valves. It is therefore imperative to develop innovative strategies based on nanotechnologies in order to prevent infections related to implanted materials, facilitate diagnosis and improve patients' care. For such utilities, an efficient organic coating is highly essential to modulate the nanomaterials' properties. [12] In this perspective, the dendritic approach has been proven versatile thanks to the precisely defined structure and composition as well as the enhanced tunable surface chemistry of those arborescent architectures. [13] Thus, using a multifunctional approach based on the chemistry of dendritic macromolecules, we aim at meeting the challenges of early diagnosis of diseases and follow-up of implant placement. As these preliminary results show, this multifunctional approach enables to obtain a nanomedicine tool of nanoparticle (NP), implant or microbubble (MB)-type, endowed with increased in vivo stability, reduced toxicity as well as antifouling properties.

Results and Discussion

Preparation of starting building blocks Scheme 1 depicts the preparation of common building blocks that are used iteratively. Tosyl azide 15 is representative for the ethylene unit spacer between each generation (G) of dendron. It was obtained in two steps from 2-Bromoethanol, first by substitution of the bromine atom with sodium azide, then activation of the primary alcohol 14 with tosyl chloride. 15 was next linked to the phenol 16 [14] in a basic medium to afford the bisphosphonate 17 in 82% yield in three grams scale. Different oligoethylene glycol (OEG) chains were used to functionalize the library of dendrons. They were first converted into tosylate (18 to 21), then Filkelstein reaction allowed to obtain OEG with an iodide as leaving group (22 to 25).

Part 1: Development of dendritic coatings for implant surfaces

The first event during implantation of a biomaterial in the body is protein adsorption. This process can be the starting point of the foreign body reaction which leads to tissue encapsulation of the biomaterial. [15] The design of efficient antifouling surface is thus of primary interest when an implant is currently concerned by this type of phenomenon. Moreover such antifouling coatings can also limit the risk of infections and formation of biofilms which is a major issue for many implants. [16] We have previously reported the synthesis of the Gallate based bisphosphonates decorated with multiple OEG side chains. [14] In the course to the development of dendritic coatings for biomedical devices, these syntheses were thoroughly revised in order to generate a library of dendrons with an enhanced robustness. The synthesis of dendrons of first generation (G1) is similar to the one reported in the literature, except that azide function was selected as the latent amine. Thus the key amide coupling was conducted after two separate steps: i) generation of the corresponding amine from azide 17 by hydrogenation, ii) formation of acyl chloride from the carboxylic acid 26 [14] with oxalyl chloride and a catalytic amount of DMF. The key intermediate 26 obtained in four grams scale (79%) was carried to the known bisphosphonic acids 1 and 2 following our previously reported procedure (Scheme 2). The bisphosphonic acid 1 was primarily evaluated by biologist partners for the antimicrobial and antifouling properties. Although OEG is known as an efficient mean to prevent the nonspecific protein adsorption, [17] we sought to improve this ability by functionalizing the surface with molecules displaying antifouling properties, e.g. polycationic or zwitterionic molecule. This chemisorption is achieved via an amide coupling between the carboxylic acid group of 1 and the amine group in the biomolecule. Alternatively, the physical adsorption was also considered. The synthesis of model bisphosphonic acid 3 with three similar and unfunctional OEG side chains is depicted in Scheme 3. First Methyl gallate was fully functionalized with OEG 18 to afford methyl ester 30 which was transformed by a saponification into its carboxylic acid analog 31. The amide coupling with 17 was accomplished with EDCI and a catalytic amount of DMAP, and the final deprotection of phosphonate groups with trimethylsilyl bromide (TMSBr) afforded the desired model compound 3. Dendron of second generation (G2) required an additional 3,5-Dihydroxybenzoic acid methyl ester as connector (Scheme 4). Its synthesis began with double functionalization of this latter with tosyl azide 15, followed by saponification to afford carboxylic acid 34 in 83% overall yield. Then, amide coupling with azido 17, upon hydrogenation, yielded bisphosphonate 35 in 98% yield in two grams scale. The last dendron 8 belonging to the G2 series exhibits a full coverage of functional octaethyleneglycol side chain (Scheme 6).

The notable issue implied the compatibility of tert-butyl ester group toward the acidic or basic condition reported throughout the synthetic pathway (vide supra). As a result, Methyl gallate was substituted by Benzyl gallate whose deprotection can be chemoselectively conducted by hydrogenolysis in the presence of tert-butyl ester. The introduction of OEG side chain in the para position was first accomplished with KHCO3/DMF and OEG 24 having an iodide as leaving group, then two equivalents OEG 20 were subsequently added by using K2CO3 in reflux of Acetone. In this manner, the isolated yield was significantly improved, whilst the one-pot trisubstitution of Benzyl gallate surprisingly ended to the decomposition of starting materials. With compound 42 in hand, coupling with bis-azide 35 could be successfully executed under HATU/DIPEA conditions after removal of the Benzyl group by hydrogenation. Despite a full conversion determined by 1 H NMR analysis of the crude product, 44 was only isolated in an unoptimized yield of 59% after a reverse phase chromatography purification step. Finally, the concomitant deprotection of phosphonate and carboxylic groups with TMSBr afforded phosphonic acid 8.

a Benzyl gallate 41 c O O NH O O PO(OEt) 2 PO(OEt) 2 H N H N O O R 1 O OR 1 OR 1 R 1 O OR 1 OR 1 O O NH O O PO(OH) 2 PO(OH) 2 H N H N O O R 2 O OR 2 OR 2 R 2 O OR 2

Quartz Crystal Microbalance preliminary studies on SiO2

In order to characterize the dendritic coatings on oxide surfaces, Quartz Crystal Microbalance with Dissipation monitoring (QCM-D) experiments were performed with dendrons 2 to 7. In order to highlight the the molecular design, these latter were classified by generation and by the OEG peripheral derivatization, i.e. 2 versus 3, 4 versus 5, and 6 versus 7 (Figure 1). The kinetics of mass deposition on SiO2 crystals showed quasisteady state after 30 min of dendron injections, which could be related to surface saturation. After rinsing with pure water, a weak desorption was observed reaching rapidly a steady state (≈3min) indicating a strong anchoring of the dendrons on the surface. Figure 2 summarizes the density of the dendrons deposited on SiO2 surfaces after the rinsing steps. Concerning dendron 2 and 3, the mass adsorbed on the surface reached about 200 ng/cm². This density was about 2-fold higher for the other dendrons, reaching about 400 ng/cm² for 4 to 7, which correspond to G2 dendrons. Finally, in terms of mass density, lower amounts of G1 (2 and 3) than G2 dendrons (4 to 7) were deposited on the surface. However, taking into account their respective molecular weight, it appears that 10 14 molecules.cm -2 were deposited on the surfaces whatever the dendron. In other words, the increase of mass density observed for G2 dendrons 4 to 7 is related to their macroarchitecture: their greater bulkiness allows a more flexible conformation to be packed on the surface. Furthermore, the nature of their chemical end groups, -COOH or -OMe, does not influence the kinetic of deposition and final amount adsorbed, indicating that the adsorption on the SiO2 surface is probably mediated through the phosphonate tweezers as expected. [18]

Part 2: Development of dendritic coatings for metallic oxide nanoparticles

Research on inorganic nanoparticles (NPs) is rapidly expanding with a large variety of applications, as well as strategies for their synthesis. [19] Most often, the surface modification of the NPs is crucial, in particular to avoid their aggregation, make them dispersible in liquid media or derivatize them with functional end groups for further modification with targeting ligands or other bioactive molecules. Here again, the exceptional binding properties of phosphonic acids to oxide surfaces have attracted much attention, such that many examples of decorated magnetic metal oxide NPs using phosphonate terminated molecules have recently emerged in the literature. [20] Many research groups worldwide are actively developing superparamagnetic iron oxide (SPIO) NPs leading to a vast number of applications in health sciences, including for example combined in vivo MRI and optical imaging (OI) via multimodal NPs based on fluorescent probes conjugated to SPIO NPs, [21] hyperthermia heating of tumour, [22] and drug delivery. [23] In this context, biofunctionalization of NPs is most often required to avoid aggregation or rapid clearance by the Mononuclear Phagocyte System (MPS). [24] The evaluation of tumor perfusion and oxygenation status is very important in oncology since tumor hypoxia appears to be strongly associated with propagation, malignant progression, and resistance to therapy. [25] It is therefore important to develop efficient probes to perform in vivo imaging of the hypoxic tissue in order to increase the therapeutic efficacy in these resistant hypoxic cells. [26] Bioreductive compounds, which are selectively reduced in hypoxic tissue to reactive intermediates that bind to intracellular molecules, have been used for targeting hypoxic tumors. Even though also other functional groups in this category (such as nitroaromatics and N-oxides) have been extensively studied, the nitroimidazole is one of the preferred pharmacophores to develop probes for tumour hypoxia detection. [27] Indeed, under hypoxic conditions, a reduction step on the nitro group occurs and the so-derived moieties covalently bind to intracellular macromolecules. With this in mind, we decided to derivatize our bisphosphonic acids with Metronidazole groups. Our route to metronidazole-functionalized dendron 9 started with the preparation of the functional OEG 45 (Scheme 7). The metronidazole, prepared according to known procedure, [28] Taking advantage of the multiple OEG arms on the dendritic structures, we introduced additional hypoxic markers as shown in scheme 8 with a slight modification compared with the access to mono-functionalized dendron 9: Methyl gallate was first functionalized in para position with OEG 22 with KHCO3 in DMF, followed by two OEG chains 45 with K2CO3 in DMF. The purification by C18 reverse phase chromatography was necessary from this stage to obtain satisfactory yields. Then saponification of 48 provided carboxylic acid 49, which reacted with phosphonate 17 using EDCI in the presence of catalytic amount of DMAP to provide dendron 50 in 37% yield overall yield. Final deprotection with TMSBr afforded phosphonic acid 10.

Synthesis of dendronized NP@metronidazole

IO NPs with a mean diameter of 9.0 ± 0.9 nm were synthesized by thermal decomposition of Iron (II) stearate in the presence of oleic acid (OA) in dioctyl ether. [29] The functionalization of the NPs was performed by direct ligand exchange in THF for 24 h and the excess of dendron was removed by ultrafiltration. In order to investigate the influence of the metronidazole group on the physico-chemical properties of dendronized NPs, various weight ratio of dendrons 9 and 1 (1/0, 75/25, 50/50, 25/75, 0/1 w/w 1:9) were grafted on the surface of the NPs. The functionalization was assessed by Dynamic Light Scattering (DLS) measurements and by infrared spectroscopy (IR) (see ESI) showing the disappearance of the OA alkyl bands (2926-2850 cm -1 ) and the appearance of the OEG characteristic signal (1096 cm -1 ). High resolution magic angle spinning (HR-MAS) 1 H nuclear magnetic resonance (NMR) was also performed to assess the presence of 9 (see ESI). As shown by DLS (Figure 4), the colloidal stability was preserved for all ratio. A slight shift in hydrodynamic diameter was observed with the increasing ratio of 9, which can be attributed to the longer middle OEG chain.

Effects of Metro-NPs on the viability and proliferation of cells grown on monolayer

In the perspective of their potential use for biomedical applications, the impact of the dendronized NPs@9 on cell viability was assessed on human umbilical vein endothelial cells (HUVEC) grown on monolayer and exposed to different nanomaterial concentrations for various time durations. The NPs displayed a high level of biocompatibility; with short incubation times and low NP dosages, viability was always above 80% (Figure 5 and ESI), and even in the harshest conditions, namely the combination of the longest incubation time (two days) and the highest dosage (150 µg Fe/mL), the viability only dropped by 20%. The effects induced by the functional NPs were not substantially different from those caused by the control NPs@1.

Figure 5. Effects of NPs@9 and NPs@1 on cell viability. Viability of HUVEC cells after incubation at 37 °C with different dosages of functionalized NPs@9 and un-functionalized NPs@1 nanoparticles for various time ranges, as tested by MTT assay.

Part 3: Dendritic coatings for the development of hybrid microbubbles

Soft-shell (e.g. lipid-shell) microbubbles (MBs) are ideal soundwave reflectors, and several fluorocarbon-stabilized MB formulations are commercially available for diagnostic ultrasound (US) imaging. [30] MBs are also being involved in several applications including molecular imaging, surgical ablation, targeted drug and gene delivery.[31] In particular, they have been extensively used in conjunction with focused US and under MRI guidance, in order to achieve blood/brain and blood/tumor barrier crossing of drugs. [32] NPs can be attached to the MBs to extend their theranostic potential by combining multimodal imaging, drug or gene delivery, and/or enhancement of the acoustic signal. Magnetic MBs have been reported.[33] Taking advantage of the high colloidal stability of IO NPs when dendronized, we have designed MBs stabilized by combination of phospholipids and dendronized IO NPs. Various dendrons, some of which are fitted with fluorinated end groups (Scheme 9) were investigated. These MBs constitute potential bimodal contrast agents to be used for US and MRI, a valued strategy for improving the accuracy of diagnosis. [34] For the synthesis of fluorinated dendrons, the piperazine scaffold was selected as template to introduce the perfluoro side chain. It was installed by using HATU as coupling agent, upon a careful deprotection of 28 in acidic condition (Scheme 9). At this point, removal of the protecting group by simple hydrogenolysis of 51 afforded the secondary amine, ready to react with the requisite perfluoroalkyl iodide. This sequence allowed to produce bisphosphonates 52-54 in reasonable yield (55 to 80%), despite their high polarity. The synthesis was achieved by the usual deprotection of phosphonate group with TMSBr to generate bisphosphonic acids 11-13. In order to rationalize the design of phospholipid-based MBs fitted with dendronized NPs in their shell, it was essential to first investigate the ability of mixtures of phospholipids and dendrons to form stable Langmuir monolayers at the air/water interface. The compression isotherms of monolayers of dimyristoylphosphatidylcholine (DMPC), dendron labeled with a C2F5 end group, 55, and of a DMPC/dendron mixture (75:25 in molar ratio) are shown in Figure 6. The pressure/area isotherm of DMPC is monotonous, reflecting the liquid-expanded character of the monolayer throughout compression. By contrast, the isotherm of the dendron shows a transition at a surface pressure s of ~15 mN m -1 and a molecular area A of ~350 Å 2 . This transition can be assigned to the progressive solubilization of the OEG chains of the dendron in the aqueous sub-phase, which leads to the collapse of the monolayer at s ~32 mN m -1 . The presence of the dendron in the mixed monolayer is evidenced by the shift in s for A larger than ~70 Å 2 . For A < 70 Å 2 , the isotherm of the mixed monolayer is nearing that of the DMPC monolayer, reflecting progressive expulsion of the dendron, either by solubilization in the sub-phase or growth of 3D aggregates in the monolayer. The mixed DMPC/dendron monolayers were transferred on silicon wafers using the Langmuir Blodgett method, and analyzed with atomic force microscopy (AFM) in order to provide insights on their composition and morphology. When transferred at ~14 mN m -1 , that is, before the onset of the transition, domains of dendrons (170 ± 20 nm in size, ~1.2 nm in height) can be observed. These domains are embedded in the DMPC monolayer, and, occasionally a 3D crystal of dendron is detected (Fig. 6B). When the pressure of transfer is increased to 30 mN m -1 , significantly more numerous and larger chains of dendron crystals (~4.0 nm in height) are seen. These investigations provide the guidelines needed to prepare stable DMPC monolayers that incorporate dendrons. These results show that small domains of dendrons can be accommodated in the phospholipid monolayer as long as the surface pressure remains below the collapse pressure of the dendron. The latter can be controlled by adjusting the dendron structure, in particular by changing the length of the hydrophobic group at the end of the longest OEG chain. This opens new perspectives for synthesizing dendrons specifically adapted for the introduction of dendronized nanoparticles in the phospholipid shells of theranostic MBs as bimodal contrast agents for US and MR imaging.

Conclusions

We have reported the synthesis of a library of dendritic bis phosphonic acids. The practical protocols and robustness were also demonstrated as two of them (dendrons 1 and 4) were prepared in a gram scale with high synthetic yields. Moreover, a selection of them was also successfully grafted onto IO NPs or MBs surface as well as on flat silica surfaces. Surface pressure/molecular compression isotherms of DMPC/dendron mixed Langmuir monolayers were investigated, providing guidelines in the production of MBs fitted with dendronized NPs to be used both for US and MRI. Currently, our main objective is to bring these hybrid nanomaterials to a step further with assessment of their stability in physiological medium and biological in vivo studies.

Experimental Section

Synthesis and functionalization of iron oxide nanoparticles

10 nm spherical nanoparticles were synthesized by thermal decomposition. Briefly, iron II stearate (2.2 mmol), oleic acid (4.4 mmol) and dioctyl ether (20 mL) were mixed together in a 100 mL two necked round bottom flask. The mixture was magnetically stirred for 1 h at 100 °C to remove the excess of water. Then the solution was heated under reflux to the boiling point of the dioctyl ether for 2 h without any stirring. The solution was purified six times by centrifugation (14000 rpm, 5 min) with a mixture of chloroform/acetone (v/v 1:5).

In a 30 mL vial, a suspension of nanoparticles in 5 mL THF (5 mg of iron) was introduced together with 7 mg of the desired mixture of dendrons and the vial was completed with 10 mL of THF. The mixture was magnetically stirred for 24 h, then the particles were centrifuged, re-dispersed in water and washed by ultrafiltration.

Cell lines

Human umbilical vein endothelial cells (HUVEC) were obtained from American Type Culture Collection (ATCC, Manassass, VA, USA) and were tested for mycoplasma (MycoAlertTM Mycoplasma Detection Kit, Lonza AG, Basel, Switzerland). Cells were cultured in monolayer at 37 °C in a 5% CO2-containing humidified atmosphere in Dulbecco's modified Eagle's medium (DMEM), in M199 medium supplemented with 20% FBS, 100 mg/mL endothelial cell growth supplement, 50 IU/mL heparin, 100 IU/mL penicillin, and 100 mg/mL streptomycin (all from ThermoFischer Scientific, Switzerland).

Cell viability tests

HUVECs were incubated with the nanoparticles in the culture medium at different concentrations (ranging from 5 to 150 µg/ml) and for various time ranges (from 1 h to 2 days) at 37 °C. Then, the cell viability was estimated by the mitochondria-dependent reduction of MTT to formazan. After labeling, 2.0×10 4 cells/well were seeded in 48-well plates. 24 h later, cells were incubated with 1 mL/well of MTT (0.5 mg/mL) at 37 °C. Approximately 4 to 6 h were required to produce formazan; supernatants were discarded and formazan was then dissolved in DMSO. The solutions were transferred to a 96-well plate and the extent of MTT reduction to formazan within the cells was quantified by measurement of the optical density at 550 nm. Results are expressed as a percentage of the respective control (incubation in medium in the absence of nanoparticles). Duplicate measurements were performed in three independent experiments.

16 Scheme 1 .

 161 Scheme 1. Preparation of starting building blocks. (a) NaN3, H2O, 75%; (b) TsCl, Et3N, CH2Cl2, 76%; (c) KOH, KI, 16, DMSO, 82% ; (d) TsCl, Et3N, CH2Cl2, 82% for 18, 81% for 19, 99% for 21, 99% for 20; (e) KI, Acetone, 94% for 22, 96% for 23, 99% for 24, 89% for 25.

26 R 1 =Scheme 2 .

 2612 Scheme 2. Synthesis of bisphosphonic acids of first generation 1 and 2. (a) 17, Pd/C, H2, EtOAc then 26, (COCl)2, DMF, DIPEA, CH2Cl2, 79%; (b) H2, Pd/C, EtOAc, then K2CO3, KI, 19 (or 20), 96% for 28, 94% for 29; (c) TMSBr, CH2Cl2, 90% for 1, 94% for 2.

Scheme 3 .

 3 Scheme 3. Synthesis of bisphosphonic acid of first generation 3. (a) K2CO3, 18, Acetone, 87%; (b) NaOH, MeOH/H2O, 99%; (c) 17, Pd/C, H2, EtOAc then EDCI, DMAP, CH2Cl2, 86%; (d) TMSBr, CH2Cl2, 90%.

3 Scheme 4 .Scheme 5 .

 345 Scheme 4. Synthesis of bisphosphonic acid of second generation 4. (a) 15, KOH, KI, DMSO, 87%; (b) NaOH, MeOH/H2O, 95%; (c) 17, Pd/C, H2, EtOAc

8 Scheme 6 .

 86 Scheme 6. Synthesis of bisphosphonic acid of second generation 8. (a) KHCO3, 24, DMF, 88%; (b) K2CO3, KI, 20, Acetone, 80%; (c) H2, Pd(OH)2/C, MeOH, 93%, (d) 35, H2, Pd/C, MeOH, then HATU, DIPEA, DMF, 59%, (e) TMSBr, CH2Cl2, 67%.

Figure 1 .

 1 Figure 1. Kinetic of dendrons 2 to 7 deposition on SiO2 quartz crystal (ng/cm²) evaluated by Sauerbrey's modeling from QCM-D analysis (based on the variations of resonance frequency Δfν/ν, for ν = 3). Rinsing with H2O was applied after 31 min deposition. Experiment was repeated three times.

Figure 2 .

 2 Figure 2. Density of dendrons 2 to 7 on SiO2 quartz crystal (ng/cm²) evaluated by Sauerbrey's modeling from QCM-D analysis (based on the variations of resonance frequency Δfν/ν, for ν = 3). Each values corresponds to the mean value of three measurements performed on three samples and error bars correspond to standard deviations.

Figure 3 .

 3 Figure 3. Mass of serum protein adsorbed on dendron-coated SiO2 quartz crystal (ng/cm²) evaluated by Sauerbrey's modeling from QCM-D analysis (based on the variations of resonance frequency Δfν/ν, for ν = 3). Values are mean ± SD. Each values corresponds to the mean value of three measurements performed on three samples, and error bars correspond to standard deviations.

Scheme 7 .

 7 Scheme 7. Synthesis of bisphosphonic acid with one metronidazole group 9. (a) TFA, CH2Cl2, then (COCl)2, DMF, CH2Cl2, then Metronidazole, DIPEA, CH2Cl2, 56%; (b) 27, Pd/C, H2, EtOAc then K2CO3, KI, Acetone, 86%; (c) TMSBr, CH2Cl2, 81%.

10 Scheme 8 .

 108 Scheme 8. Synthesis of bisphosphonic acid with two metronidazole groups 10. (a) KHCO3, 22, DMF, 86%; (b) K2CO3, KI, 45, DMF, 88%; (c) NaOH, MeOH/H2O, 99%; (d) 17, Pd/C, H2, EtOAc, then EDCI, DMAP, CH2Cl2, 37%; (d) TMSBr, CH2Cl2, 72%.

Figure 4 .

 4 Figure 4. Dynamic light scattering (DLS) measurements in pure water (pH 7) performed on dendronized NPs of various ratios of 1:9. OA: oleic acid.

9 .

 9 Scheme 9. Synthesis of bisphosphonic acid 11-13 used to coat iron oxide nanoparticles. The dendronized nanoparticles are intended to be used in combination with phospholipids to form the shell of hybrid microbubbles. (a) TFA, CH2Cl2, then piperazine-NCbz, HATU, DIPEA, DMF, 99%; (b) H2, Pd/C, MeOH, then perfluoroalkyliodide, K2CO3, CH3CN, 62% for 52, 80% for 53, 55% for 54; (c) TMSBr, CH2Cl2, 78% for 11, 79% for 12, 80% for 13; (d) TFA, CH2Cl2, then 1,1,1,2,2-pentafluoro-6-iodohexane, K2CO3, CH3CN, 92%.

Figure 6 .

 6 Figure 6. A) Compression isotherms at 25°C of Langmuir monolayers of DMPC (black), and DMPC/dendron 55 (75:25 molar ratio; blue). Inset: isotherm of the fluorinated dendron 55 alone (green) and. B) atomic force micrographs of Langmuir monolayers of the DMPC/dendron 55 mixture after transfer on silicon wafers at a) 14 mN m -1 and b) 30 mN m -1 .

  Preparation of dendritic building blocks (See ESI) Quartz crystal microbalance with dissipation monitoring (QCM-D) Dendritic coatings were deposited on SiO2 quartz crystal sensors (QSX 303, Qsense®, Biolin Scientific AB, Sweden) and further analyzed using a quartz crystal microbalance with dissipation monitoring (QCM-D, E1 Qsense®, Biolin Scientific AB, Sweden). Firstly, bare SiO2 crystals were excited at their fundamental resonance frequency (ν = 0, corresponding to 5 MHz) at T = 25 °C and the variations of resonance frequency were measured at the first four odd overtones (noted -Δfν with ν = 3, ν = 5, ν = 7 and ν = 9 corresponding to 15, 25, 35 and 45 MHz, respectively). To perform the deposition, 400 µL of dendrons (1 mg.mL -1 in pure water) such as 2, 6 or 5, with -COOH or -OMe end groups, were loaded in the sensors for 30 min and rinsed with 400 µL H2O MilliQ® for 10 min at T = 25 °C. After dendron deposition, Sauerbrey's modeling was used to determine the mass adsorbed on the crystal surfaces. Sauerbrey approximation can be used as the normalized frequency shifts for the various overtones display almost identical values and slight shifts in dissipation were monitored. [35] Characterization of antifouling properties Following dendron deposition on the SiO2 crystal surfaces, 400 µL buffer containing 10 mM of Tris(hydroxymethyl)-aminomethane (TRIS) (Merck, Germany) and 150 mM NaCl (Fisher Scientific, France) at pH 7.4 were injected for 10 min in the sensor. 400 µL of fetal bovine serum (FBS, S1810 Dutscher, France) diluted at 10 % (v/v) in the Tris-NaCl buffer were deposited on the dendron-coated surfaces for 30 min. Then a flow of Tris-NaCl buffer (250 µL.min -1 ) rinsing solution was continuously applied during 200 min. Finally, serum protein adsorption was evaluated by Sauerbrey's approximation.

Acknowledgements

This research project was funded by CNRS, Unistra and the European Regional Development Fund (ERDF) in the framework of the INTERREG V Upper Rhine program "Transcending borders with every project", project NANOTRANSMED.

Keywords: dendron • surface coating • antifouling • iron oxide nanoparticles • microbubble


Brett Mclean

FREE KLEENE ALGEBRAS WITH DOMAIN

Keywords: 2020 Mathematics subject classification: primary 08B20; secondary 20M20 Kleene algebra, domain, binary relation, equational theory, decidable

First we identify the free algebras of the class of algebras of binary relations equipped with the composition and domain operations. Elements of the free algebras are pointed labelled finite rooted trees. Then we extend to the analogous case when the signature includes all the Kleene algebra with domain operations; that is, we add union and reflexive transitive closure to the signature. In this second case, elements of the free algebras are 'regular' sets of the trees of the first case. As a corollary, the axioms of domain semirings provide a finite quasiequational axiomatisation of the equational theory of algebras of binary relations for the intermediate signature of composition, union, and domain. Next we note that our regular sets of trees are not closed under complement, but prove that they are closed under intersection. Finally, we prove that under relational semantics the equational validities of Kleene algebras with domain form a decidable set.

Introduction

Reasoning about binary relations, and ways of combining them, has an extensive literature and a multitude of applications. Classically, in algebraic logic, binary relations model logical formulas with two free variables [START_REF] Tarski | On the calculus of relations[END_REF]. In computer science, we can find binary relations modelling the actions of programs [START_REF] Vaughan | Semantical considerations on Floyd-Hoare logic[END_REF][START_REF] Kozen | Kleene algebra with tests[END_REF], and elsewhere representing relationships between items of data that compose a tree [START_REF] Benedikt | XPath leashed[END_REF], or a graph [START_REF] Libkin | Querying graph databases with XPath[END_REF].

When an algebraic logician thinks of binary relations, the first signature to come to mind will always be that of Tarski's relation algebras. In computer science, the Kleene algebra signature has the greatest prominence. In the latter case, the operations are relational composition, union, and reflexive transitive closure, as well as constants for the empty relation and the identity relation.

Any set of binary relations closed under the five Kleene algebra operations/constants can be viewed as an algebra in the sense of universal algebra/model theory, that is, a structure over a signature of function symbols (but no predicate symbols). It is well known that this class of algebras contains its free algebras, and that the free algebra generated by a given finite set Σ is precisely the set of all regular languages over the alphabet Σ. The importance of regular languages in theoretical computer science goes almost without saying [START_REF] Sipser | Regular languages, Introduction to the Theory of Computation[END_REF]. The algebraic perspective on sets of regular languages was employed to great effect by Eilenberg in his celebrated variety theorem [START_REF] Eilenberg | Automata, languages, and machines[END_REF], and continues to yield valuable new insights to this day [START_REF] Gehrke | Duality and equational theory of regular languages[END_REF][START_REF] Gehrke | Stone duality, topological algebra, and recognition[END_REF].

In this paper, we identify the analogous free algebras in the case where the signature is expanded with one extra operation on binary relations: the unary domain operation D(R) = {(x, x) | ∃y : (x, y) ∈ R}, which provides a record of all points having at least one image under the given relation. This expanded signature is that of Kleene algebra with domain, a certain finite set of algebraic laws extending Kozen's theory of Kleene algebras with a domain operation and a small number of associated equations [START_REF] Desharnais | Internal axioms for domain semirings[END_REF].

One intended model for this theory is indeed algebras of binary relations, and there is a hope that the theory will prove useful for reasoning about the actions of nondeterministic computer programs [START_REF] Desharnais | Kleene algebra with domain[END_REF][START_REF] Desharnais | Domain axioms for a family of near-semirings[END_REF]. In this programs-as-relations formalism, a program P is modelled by a relation R on machine states, with R relating state x to state y precisely if, whenever the machine is in state x and P is executed, y is a possible resultant state. Hence relational composition models sequential composition of programs, union models nondeterministic choice, and reflexive transitive closure models the choice to iteratively execute a program any (finite) number of times. The expression D(R) then models a program that when run from certain states-those from which P would terminate-has no effect-and otherwise fails/does not terminate. Thus domain makes provision within the syntax for expressing certain types of 'tests'-an important component of all programming languages.

In addition to identifying the free algebras, we also show that it is decidable whether an equation in this Kleene algebra with domain signature is valid over all algebras of binary relations. Of course, when reasoning about programs, the validity of an equation s = t corresponds to the programs expressed by s and t always having precisely the same effect (independently of which ground programs the variables are instantiated with).

Structure of the paper

In Section 2 we give the necessary definitions and some context regarding algebras of binary relations, and their free algebras.

In Section 3 we introduce the trees that we use for describing our free algebras, and certain relations and operations on those trees.

In Section 4 we prove an intermediate result: we identify the free algebras for the reduced signature that omits the 'nondeterministic' union and reflexive transitive closure operators, and also the empty relation constant, that is, the signature with the composition and domain operations and the identity constant. For this signature the elements of the free algebras are 'reduced' pointed labelled finite rooted trees (Theorem 4.6).

In Section 5 we extend the result of the previous section to identify the free algebras for the full Kleene algebra with domain signature. In this case, elements of the free algebras are certain sets of the trees of the previous case (Theorem 5.6). We term these sets 'regular' sets of trees, by analogy with the regular languages of the Kleene algebra signature. By combining with an existing result, it follows as a corollary that the axioms of domain semirings provide a finite quasiequational axiomatisation of the equational theory of algebras of binary relations for the signature of composition, union, domain, and the two constants (but not reflexive transitive closure).

Section 6 is devoted to closure properties of regular sets of trees. We use automata to show the regular sets of trees are closed under intersection. We also note the regular sets of trees are not closed under complement and pose the questions of whether they are closed under implication or under residuation.

In Section 7 we again use automata to prove the decidability of validity for equations in the signature of Kleene algebra with domain under relational semantics (Theorem 7.2).

Algebras of binary relations

We begin by making precise what is meant by an algebra of binary relations. Throughout, we consider that 0 ∈ N. Definition 2.1. An algebra of binary relations of the signature {;, +, *, 0, 1} is a universal algebra A = (A, ;, +, *, 0, 1) where the elements of the universe A are binary relations on some (common) set X, the base, and the interpretations of the symbols are given as follows:

• the binary operation ; is interpreted as composition of relations:

R ; S {(x, y) ∈ X 2 | ∃z ∈ X : (x, z) ∈ R ∧ (z, y) ∈ S },
• the binary operation + is interpreted as set-theoretic union:

R + S {(x, y) ∈ X 2 | (x, y) ∈ R ∨ (x, y) ∈ S },
• the unary operation * is interpreted as reflexive transitive closure:

R* {(x, y) ∈ X 2 | ∃n ∈ N ∃x 0 . . . x n : (x 0 = x) ∧ (x n = y) ∧ (x 0 , x 1 ) ∈ R ∧ . . . ∧ (x n-1 , x n ) ∈ R},
• the constant 0 is interpreted as the empty relation:

0 ∅,
• the constant 1 is interpreted as the identity relation on X:

1 {(x, x) ∈ X 2 }.
We let Rel(;, +, *, 0, 1) denote the isomorphic closure of the class of all algebras of binary relations of the signature {;, +, *, 0, 1}.

To be clear: the universe of an algebra of binary relations is necessarily closed under the given operations, since the definition of a universal algebra requires the symbols be interpreted as total functions. Remark 2.2.

(i) It is easy to see that Rel(;, +, *, 0, 1) is not a first-order axiomatisable class, not even closed under elementary equivalence, by a simple argument showing that Rel(;, +, *, 0, 1) is not closed under ultrapowers. See the appendix for a proof of this well-known fact.

(ii) Despite Rel(;, +, *, 0, 1) being far from a variety, it is easily seen to be closed under subalgebras and products. (An element of a product of algebras of binary relations is the disjoint union of all its component binary relations.) Hence, by a basic theorem of universal algebra (see, for example, [3, Theorem 10.12]), the class Rel(;, +, *, 0, 1) contains its free algebras.

(iii) It is a folk theorem that the free Rel(;, +, *, 0, 1)-algebra generated by a finite set Σ is the set of all regular languages over the alphabet Σ (with the operations of language concatenation, union, and so on).

(iv) It is well known that the variety HS P Rel(;, +, *, 0, 1) generated by Rel(;, +, *, 0, 1) has no finite equational axiomatisation [START_REF] Volodymyr | On the determinative aggregate of relationships of the algebra of regular events[END_REF].

(v) We do however have Kozen's quasivariety of Kleene algebras [START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF], defined by a finite number of equations/quasiequations,1 intermediate to Rel(;, +, *, 0, 1) and HS P Rel(;, +, *, 0, 1). That is, Rel(;, +, *, 0, 1) ⊆ Kleene algebras ⊆ HS P Rel(;, +, *, 0, 1), and so HS P(Kleene algebras) = HS P Rel(;, +, *, 0, 1).

Of course, the operations of Definition 2.1 are not the only operations that can be defined on binary (endo)relations. In particular, various unary 'test' operations can be defined; here is a selection. Definition 2.3.

• The unary operation D is the operation of taking the diagonal of the domain of a relation:

D(R) = {(x, x) ∈ X 2 | ∃y ∈ X : (x, y) ∈ R}.
• The unary operation R is the operation of taking the diagonal of the range of a relation: R(R) = {(y, y) ∈ X 2 | ∃x ∈ X : (x, y) ∈ R}.

• The unary operation A is the operation of taking the diagonal of the antidomain of a relation-those points of X at which the image of the relation in empty:

A(R) = {(x, x) ∈ X 2 | ∃y ∈ X : (x, y) ∈ R}.
One can vary the operations from those of Definition 2.1 and/or restrict the binary relations to some particular form. The resulting class will again contain its free algebras. If the class is of interest, then it is useful to establish a description of these free algebras.

Restricting the binary relations to be some type of function (total functions, partial functions, or injective partial functions, for example) tends to yield free algebras whose elements are a 'single object', rather than a 'set of objects'. The class of semigroups, for example, is the variety generated by Tot(;)-algebras of total functions with composition-and an element of a free semigroup is a single string, rather than a set of strings as we have in the case Rel(;, +, *, 0, 1). Similarly, elements of free groups are also strings, with groups forming isomorphs of algebras of permutations, with the familiar operations.

There is also an observable pattern when test operations are added to the signature: strings are replaced by (labelled) trees. The following results are known.

1. The class Inj(;, -1 ), of isomorphs of algebras of injective partial functions with composition and inverse, is the class of inverse semigroups [START_REF] Viktor | Generalised groups[END_REF][START_REF] Preston | Inverse semi-groups[END_REF]. 2 (In this signature D and R are definable via D(R) R ; R -1 and R(R) R -1 ; R, respectively.) Elements of free inverse semigroups are certain trees, so-called Munn trees [START_REF] Walter | Free inverse semigroups[END_REF].

2. The class Par(;, D)-partial functions with composition and domain-is a variety [START_REF] Valentin | Menger's function systems[END_REF], most commonly known as the (left) restriction semigroups. A description of the free algebras has been given, and again, elements can be viewed as trees [START_REF] Fountain | Free right type A semigroups[END_REF].

3. The class Par(;, D, R)-partial functions with composition, domain, and rangeis a proper quasivariety; a finite quasiequational axiomatisation was given by Schein [START_REF] Schein | Restrictively multiplicative algebras of transformations[END_REF]. Once more, a description of the free algebras has been given, and elements can be viewed as trees [START_REF] Fountain | The free ample monoid[END_REF].

We should also mention at this stage Hollenberg's finite equational axiomatisation of the equational theory of the quasivariety Rel(;, A) (in which D, 0, and 1 are easily expressible) [START_REF] Hollenberg | An equational axiomatization of dynamic negation and relational composition[END_REF]. Of course, this result amounts to an implicit description of the corresponding free algebras, as quotients of term algebras by this theory. Another result involving binary relations (but not tests), is Bloom, Ésik, and Stefanescu's explicit description of the free algebras for the case Rel(;, +, *, 0, 1, ), where is the converse operation R {(x, y) ∈ X 2 | (y, x) ∈ R} [START_REF] Stephen | Notes on equational theories of relations[END_REF]. There, the elements of the algebras are sets of strings.

Having noted that binary relations ; sets, functions ; singletons, and tests ; trees, one can anticipate that when tests are added to the case Rel(;, +, *, 0, 1), elements of free algebras will be sets of labelled trees. We will prove that this is indeed the case (Theorem 5.6). On the way to doing this, we also identify the free algebras for the case without the 'nondeterministic' operators + and *, more precisely, for the case Rel(;, 1, D) (Theorem 4.6). The analogous results for signatures formed by adding/removing 0 and/or 1 follow as corollaries of these two theorems.

Remark 2.4. The term 'Kleene algebra with domain' was originally used for a certain quasiequational theory extending the two-sorted Kleene algebra with tests with a domain operation [START_REF] Desharnais | Kleene algebra with domain[END_REF]. It was subsequently redefined as a (strictly less expressive) one-sorted quasiequational theory extending Kleene algebra with a domain operation [START_REF] Desharnais | Internal axioms for domain semirings[END_REF].

Trees

The central objects we will be working with throughout will be labelled rooted trees. We will give two definitions of these. The first, Terminology 3.1, is the usual graph-theoretic definition, and we give it in order to make use of basic graph-theoretic terminology: vertex, edge, and so on. The second, Definition 3.2, is cleaner, in the sense that isomorphic trees are identical, and will serve as the 'official' definition in this paper. Terminology 3.1.

• A tree is a connected acyclic undirected graph (reflexive edges are prohibited).

All trees will be assumed to be finite unless otherwise stated.

• A rooted tree is a tree with a distinguished vertex called the root.

• By a labelled tree, we will mean an edge-labelled tree. That is, given a set Σ of labels, a labelled tree is a tree T together with a function from the edges of T to Σ.

Definition 3.2. Given a set Σ of labels, a labelled rooted tree is defined recursively as a set of pairs (a, T ), where a ∈ Σ and T is a labelled rooted tree. Some explanation may be helpful. According to Definition 3.2, the empty set is a labelled rooted tree (this is the base case of the definition). This empty set should be thought of as encoding what is, in the graph-theoretic view, the tree with a single vertex. Figure 1 illustrates how some simple examples of labelled rooted trees should be viewed. The reader may note that Definition 3.2 is more restrictive than the definition of labelled rooted trees obtained from Terminology 3.1-it cannot describe any tree having a vertex with two distinct but isomorphic child subtrees. However, we will have no need of such trees in this paper. Definition 3.3. A pointed tree is a tree with a distinguished vertex called the point.

We will primarily work with pointed labelled rooted trees. We will usually denote a pointed labelled rooted tree (T, p) by its underlying labelled rooted tree T . We define the notion of a homomorphism of (possibly pointed) labelled rooted trees by reference to homomorphisms of relational structures. Definition 3.4. A relational structure (X, f ) for a set Σ of labels is a set X and an assignment f giving for each element of a ∈ Σ a binary relation a f on X. A homomorphism from a relational structure (X, f ) to the relational structure (Y, g)

(both with label-set Σ) is a map θ : X → Y validating (x 1 , x 2 ) ∈ a f =⇒ (θ(x 1 ), θ(x 2 )) ∈ a g for each a ∈ Σ.
We can view any Σ-labelled rooted tree as a relational structure (X, f ) by taking X to be the set of vertices of the tree and for each a ∈ Σ setting a f to be the set of pairs (x, y) of vertices such that x is the parent of y and the edge {x, y} is labelled by a. When we speak of a homomorphism θ : S → T of possibly pointed labelled rooted trees, we mean a homomorphism of the trees viewed as relational structures that is also required to map the root of S to the root of T and, if it exists, the point of S to the (therefore extant) point of T .

Let A be an algebra of binary relations (in any of the signatures we take an interest in) with base set X. Let f be an assignment of members of A to the set Σ of variables. Then (A, f ) naturally defines a relational structure: (X, f ). Conversely, let (X, f ) be a relational structure and let A be any algebra of binary relations on X that includes {a f | a ∈ Σ} in its universe (that is, any algebra between the algebra generated by this set and the algebra of all binary relations on X × X). Then the standard model-theoretic interpretation t A, f of any Σ-term t is independent of the precise choice of A. Thus, when interpreting terms and evaluating equations, it is safe to conflate the concepts of algebra + assignment and relational structure, and we will often do so. For example, the following definition is stated in terms of an algebra and assignment, but we will mainly use it in contexts where we are ostensibly talking about a relational structure. Definition 3.5. Let A be an algebra of binary relations with base X, let t be a term, and let f be an assignment to the variables in t. We say that a pair (x, y) ∈ X × X satisfies t if (x, y) ∈ t A, f . We want to be able to reduce trees to forms without any redundant branches. In order to do that, we first define a preorder on trees.

Definition 3.6. The preorder ≤ on (possibly pointed) labelled rooted trees is defined recursively as follows. For trees T 1 and T 2 with roots r 1 and r 2 respectively, T 1 ≤ T 2 if and only if (a) if r 2 is the point vertex of T 2 , then r 1 is the point vertex of T 1 , (b) for each child v 2 of r 2 , there is a child v 1 of r 1 such that (i) the labels of the edges r 1 v 1 and r 2 v 2 are equal, (ii) T v 1 ≤ T v 2 , where T v 1 and T v 2 are the v 1 -rooted and v 2 -rooted subtrees respectively.

That ≤ is indeed a preorder is clear. In fact, by induction on the height of the trees, it is easy to see that

T 1 ≤ T 2 ⇐⇒ there exists a homomorphism θ : T 2 → T 1 . (3.1)
In the following definition and proposition, we continue to work with trees that may or may not be pointed. Definition 3.7. Let T be a labelled tree with root r. The reduced form of T is the tree formed recursively as follows. Proof. By induction on the maximum height of the two trees being compared. For the base case, take trees T 1 , T 2 of height 0, so both have just a single vertex. Suppose T 1 ≤ T 2 and T 2 ≤ T 1 . Then by Definition 3.6(a), the tree T 1 is pointed if and only if T 2 is pointed. Hence T 1 = T 2 . Now let T 1 and T 2 be of height at most n + 1, and assume antisymmetry of ≤ holds for all reduced trees of height at most n. Suppose T 1 ≤ T 2 and T 2 ≤ T 1 , and denote the roots by r 1 and r 2 , respectively. As before, T 1 has a point at r 1 if and only if T 2 has a point at r 2 . By Definition 3.7 the child subtrees of vertex r 1 are reduced, and for each a ∈ Σ the child subtrees linked by an a-labelled edge are pairwise ≤-incomparable. Likewise for the child subtrees of vertex r 2 .

Let v 2 be an arbitrary child of r 2 . Since T 1 ≤ T 2 , we can find a child v 1 of r 1 as in Definition 3.6(b), giving us T v 1 ≤ T v 2 . Then using T 2 ≤ T 1 and applying Definition 3.6(b) again, we obtain a child v 2 of r 2 and have T v 2 ≤ T v 1 ≤ T v 2 (with r 2 v 2 and r 2 v 2 having the same label). Hence by pairwise ≤-incomparability,

T v 2 = T v 2 . So T v 2 ≤ T v 1 ≤ T v 2 ,
which by the inductive hypothesis yields T v 1 = T v 2 . Since v 2 was arbitrary, we conclude that every child subtree of r 2 is present as a child subtree of r 1 . Symmetrically, every child subtree of r 1 is present as a child subtree of r 2 . Hence

T 1 = T 2 .
Note now that the partial order ≤ on reduced trees is Noetherian (converse wellfounded). Indeed, by structural induction there are a finite number of distinct labelled trees of any fixed depth, hence a finite number of reduced pointed labelled trees of that depth. And T 1 ≤ T 2 implies the depth of T 2 is at most the depth of T 1 .

Proposition 3.10. If a labelled rooted tree T reduces to T , then T ≤ T and T ≤ T .

Proof. Another induction on height. All trees of height 0 are already reduced, so this base case is trivial. Now assume the result holds whenever T is of height at most n. Let T be of height n + 1, with root r. It is clear that the root r of T is the point of T if and only if r is the point of T . So there is no obstruction to a homomorphism mapping r to r or vice versa.

First we show T ≤ T . Every child subtree of r is the reduced form T v of some child subtree T v of r (with rv and r v having the same label). Hence, by the inductive hypothesis and (3.1), there is a homomorphism θ v : T v → T v . By gluing together {θ v | v a child of r }, and mapping r to r, we obtain a homomorphism T → T . Hence T ≤ T . Now we show T ≤ T . Let T be the intermediate tree in the reduction of T to T , that is, T is the tree formed from T by reducing all child subtrees of r. Denote the root of T by r . Take an arbitrary child subtree T v of r, and let T v be its reduced form sitting as a subtree of T . So by the inductive hypothesis, there is a homomorphism T v → T v . Since ≤ is Noetherian on reduced trees, when T is formed from T by applying step (b) in the definition of reduction, a subtree T v with T v ≤ T v (and such that r v and r v have the same label) is retained. Thus there is a homomorphism T v → T v , and hence, by composition, a homomorphism T v → T v . Gluing together the homomorphisms for each child v of r, and mapping r to r , we obtain a homomorphism T → T . Hence T ≤ T .

Thus reduction selects a canonical member of every ≤-equivalence class. Informally, we can think of ≤ on reduced trees as corresponding to the inclusion relation on binary relations-if T 1 ≤ T 2 then T 1 is a more specific description than T 2 . Definition 3.11. Let Σ be a set and let T and S be reduced pointed Σ-labelled rooted trees.

• The pointed tree concatenation T ; S of T and S is the tree formed by 1. identifying the point of T and the root of S (the root is now the root of T and the point is the point of S ), 2. reducing the resulting tree to its reduced form.

• The domain D(T ) of T is the tree formed by 1. reassigning the point of T to the current root of T , 2. reducing the resulting tree to its reduced form.

Notation 3.12. For a symbol a from an alphabet, we write a for the pointed labelled rooted tree with two vertices, whose point is the child vertex and whose single edge is labelled by a. We write ε for the pointed labelled rooted tree with a single vertex.

Remark 3.13. A very similar setup to that presented in this section has already been used for investigating Kleene algebras with domain [START_REF] Diarra | Completeness for domain semirings and star-continuous Kleene algebras with domain[END_REF]. In that thesis, the graph-theoretic definition of trees is used, and pointed labelled finite rooted trees are called 'trees with a top'. There, the relation ≤ is termed 'simulates', and trees are only considered up to simulation equivalence. Thus there is no notion of a reduced form; the operations of Definition 3.11 are defined without their reduction steps. We will return to say more about the thesis [START_REF] Diarra | Completeness for domain semirings and star-continuous Kleene algebras with domain[END_REF] at the end of Section 5.

Composition, identity, and domain

In this section we will identify the free algebras of the class Rel(;, 1, D). From there, it is straightforward to accommodate the addition of + and * (and 0).

By a term we mean a raw syntactic object belonging to a term algebra/absolutely free algebra-no background theory is assumed. Thus equality of terms means literal equality.

Definition 4.1. We define the single-tree interpretation [ • ] of {;, 1, D}-terms as follows.

1. [a] a, for any variable a,

2. [1] ε, 3. [s ; t] [s] ; [t],

[D(s)] D([s]).

Here the operations and constants on the right-hand side are those defined for trees in Section 3. Definition 4.1 is well defined because if pressed for a formal definition of terms we would give one that satisfies unique readability, either by writing ; in prefix form, requiring parentheses, or defining terms directly as trees.

Lemma 4.2. The map [ • ] is a surjection from the {;, 1, D}-terms in variables Σ onto the reduced pointed Σ-labelled rooted trees. Hence [ • ] is a surjective homomorphism from the term algebra onto the reduced pointed Σ-labelled rooted trees, viewed as an algebra of the signature {;, 1, D} with the operations we have defined.

Proof. We show that every reduced tree is the single-tree interpretation of some term by induction on the size of the tree.

A tree whose root has no children is just ε-the interpretation of 1-so assume we have a tree T given by a nonempty set {(a 1 , T 1 ), . . . , (a n , T n )}, and a distinguished point p. First suppose p is the root of T . For each 1 ≤ i ≤ n, let t i be a term whose interpretation is the pointed tree whose tree is T i and whose point is its root. Then we can realise T by the term D(a 1 ; t 1 ) ; • • • ; D(a n ; t n ). (We write iterated ; without brackets because the positioning of the brackets turns out to be immaterial.)

Alternatively, suppose p is not the root of T ; so without loss of generality p is a vertex in T n . Let t 1 , . . . , t n-1 be as before and now let t n be a term whose interpretation is the pointed tree whose tree is T n and whose point is p. Then we can realise T by the term D(a 1 ; t 1 ) ; • • • ; D(a n-1 ; t n-1 ) ; a n ; t n .

The following lemma says that the single-tree interpretation of a term records for us a tree that, in a relational structure, 'connects' x and y if and only if the term is satisfied by (x, y). Lemma 4.3. Let A be a {;, 1, D}-algebra of binary relations, with base X. Let t be a {;, 1, D}-term, and let f be an assignment of elements of A-so, binary relations-to the variables in t. Then for any x, y ∈ X, the following are equivalent.

1. The pair (x, y) belongs to the model-theoretic interpretation of t under the assignment f .

2. There is a homomorphism of [t] into (X, f ) such that the root of [t] is mapped to x and the point of [t] is mapped to y.

Proof. By structural induction on terms. As before, we write t A, f for the modeltheoretic interpretation of t.

First, suppose t = a, for some variable a. Then [t] = a-consisting of an a-labelled edge linking the root r to the point p. Therefore (x, y) ∈ t A, f if and only if (x, y) ∈ f (a), so if and only if the map given by r → x and p → y is a homomorphism. The case t = 1 is similar.

Next, suppose t = s 1 ; s 2 and that the equivalence holds for s 1 and for s 2 . Then (x, y) ∈ t A, f if and only if there is a z ∈ X such that (x, z) ∈ s 1 A, f and (z, y) ∈ s 2 A, f . By the inductive hypotheses, the latter is equivalent to the existence of a homomorphism from [s 1 ] mapping its root r 1 to x and point p 1 to z, and a homomorphism from [s 2 ] mapping its root r 2 to z and point p 2 to y. This is equivalent to the existence of a homomorphism from [s 1 ; s 2 ], mapping the root to x and point to y, since there exist homomorphisms in both directions between a tree and its reduced form.

Finally, suppose t = D(s) and that the equivalence holds for s. Then (x, y) ∈ t A, f if and only if x = y and there exists z such that (x, z) ∈ s A, f . By the inductive hypothesis, this is equivalent to x = y and the existence of a homomorphism mapping the root of [s] to x and the point to z. Since [t] and [s] differ only by the position of their point, which for [t] is the root, the latest condition is equivalent to the existence of a homomorphism from [t] mapping both the root/point to x/y, as required. Theorem 4.6. Let Σ be an alphabet, and let R Σ be the set of reduced pointed Σ-labelled finite rooted trees. Then the free Rel(;, 1, D)-algebra over Σ is R Σ equipped with the operations of pointed tree concatenation and of domain from Definition 3.11 (and the constant ε).

Proof. Since R Σ is generated by Σ, it follows by the first isomorphism theorem of universal algebra that R Σ is isomorphic to a quotient Q of the term algebra (for signature {;, 1, D}) over variables Σ. The congruence relation ∼ defining the quotient is given by s ∼ t ⇐⇒ [s] = [t], for terms s and t over Σ. So by Corollary 4.4 and Lemma 4.5, the congruence ∼ is given by equational validity in Rel(;, 1, D). It is a basic result of universal algebra that Q is then precisely the free algebra over Σ of the class Rel(;, 1, D).

The inclusion of 1 and exclusion of 0 from the signature was in fact not essential. We can easily add and remove them according to our wishes. Corollary 4.7. Let Σ and R Σ (viewed as an algebra) be as in Theorem 4.6.

• The free Rel(;, D)-algebra over Σ is given by removing the tree ε from R Σ .

• The free Rel(;, 0, D)-algebra over Σ is given by the addition of a zero element-an element validating 0 ; T = T ; 0 = 0 and D(0) = 0-to the free Rel(;, D)-algebra over Σ.

• The free Rel(;, 1, 0, D)-algebra over Σ is given by the addition of a zero element to R Σ .

Proof. For Rel(;, D), first note that every nontrivial tree in R Σ is the single-tree interpretation of a {;, D}-term, and conversely, if a tree is the interpretation of a {;, D}term then it cannot be trivial-by induction, all such interpretations have at least one edge. Hence the nontrivial trees indeed form a {;, D}-algebra generated by (the interpretations of elements of) Σ. Since every {;, D}-algebra of relations embeds in a {;, 1, D}-algebra of relations, it follows from Corollary 4.4 that every equation validated by the nontrivial trees is validated by all {;, D}-algebras of relations. The converse follows immediately from Lemma 4.5. For Rel(;, 0, D) and Rel(;, 1, 0, D), note that by the definition of a zero element, a term is interpreted as the zero of the algebra if and only if the symbol 0 appears in the term, and similarly a term is interpreted as ∅ in every algebra of relations if and only if 0 appears in the term. These observations are sufficient to extend Corollary 4.4 and Lemma 4.5 to terms that may contain 0.

We remark that the class Rel(;, 1, D), as noted in [START_REF] Hirsch | Axiomatizability of representable domain algebras[END_REF], forms a quasivariety. 3 It has been shown that this quasivariety is not finitely axiomatisable in first-order logic [START_REF] Hirsch | Axiomatizability of representable domain algebras[END_REF]. Naturally, the same statements hold when we add/remove 0 and 1.

Expansion by union and reflexive transitive closure

In this section, we extend the result of the previous section to provide a description of the free algebras of the class of relational Kleene algebras with domain, that is, the free algebras of Rel(;, +, *, 0, 1, D). Definition 5.1. For a set K of reduced trees, let maximal(K) denote the set of ≤maximal elements of K. We lift the notation ; and D of Definition 3.11 to sets of trees by using elementwise application. We define the standard tree interpretation • of {;, +, *, 0, 1, D}-terms as follows.

1. For a ∈ Σ, a {a}, Note that a , for a ∈ Σ, 0 , and 1 , contain only reduced trees, and ∪ preserves this property on sets of trees (as do the lifted ; and D, by definition). Hence the maximal operation is applicable whenever it is used in Definition 5.1, and standard interpretations contain only reduced trees. Definition 5.2. Let Σ be an alphabet. A set of pointed Σ-labelled rooted trees is regular if it is the standard tree interpretation of some {;, +, *, 0, 1, D}-term. 4We can think of a regular set L of trees as a concise record of all the reduced trees in the downward-closed set ↓L (with respect to the ≤ ordering). In this view (thinking of L as ↓L), the operation + corresponds to the real set union operation, and ; and D correspond to pointwise application of the operations of Definition 3.11. The advantage of using the arrangement of Definition 5.1 is that regular sets remain finite until such time that Kleene star is used. That the partial order ≤ on reduced trees is Noetherian ensures there are 'enough' elements in maximal( ∞ i=1 s i ) for that to be a sensible definition of s * (as demonstrated in the proof of the next lemma).

2. 0 ∅, 3
The following lemma is the analogue of Lemma 4.3.

Lemma 5.3. Let A be a {;, +, *, 0, 1, D}-algebra of binary relations, with base X. Let t be a {;, +, *, 0, 1, D}-term, and let f be an assignment of elements of A to the variables in t. Then for any x, y ∈ X, the following are equivalent.

1. The pair (x, y) belongs to the model-theoretic interpretation of t under the assignment f .

2. There is a tree T in t and a homomorphism of T into (X, f ) such that the root of T is mapped to x and the point of T is mapped to y.

Proof. Structural induction on terms. We give the details for the * case in the direction 1 =⇒ 2, as this case is not entirely trivial. So suppose that t = s * , that condition 1 holds for t, and that whenever condition 1 holds for s, condition 2 holds for s. Then since (x, y) belongs to the model-theoretic interpretation of s * , there are z 0 , . . . , z n with z 0 = x, z n = y, and each (z i , z i+1 ) belonging to the interpretation of s. Hence there are trees S 1 , . . . , S n ∈ s and homomorphisms mapping each S i into (X, f ) with the root mapping to z i-1 and point mapping to z i . By (3.1), there is a homomorphism of the reduced tree (. . . (S 1 ;S 2 );• • •;S n ) into (X, f ) mapping the root to x and the point to y. By (3.1) again (and an induction up to n), there is a T ∈ s n with T ≥ (. . . (S 1 ;S 2 );• • •;S n ) and a homomorphism of T into (X, f ) mapping the root to x and the point to y. Then T ∈ ∞ j=1 s j , and since the partial order ≤ on reduced trees is Noetherian, there exists a T ∈ s * maximal( ∞ i=1 s i ) with T ≥ T . Such a T fulfils condition 2, so we are done.

Proposition 5.4 (soundness with respect to relations). For any pair s and t of {;, +, *, 0, 1, D}-terms

s = t =⇒ Rel(;, +, *, 0, 1, D) | = s = t.
Proof. Suppose s = t . Let A be a {;, +, *, 0, 1, D}-algebra of binary relations, with base X. Let f be an assignment of elements of A to the variables appearing in s = t. Write • A, f for the model-theoretic interpretations in A under f . Then by Lemma 5.3, for any x, y ∈ X, we have that (x, y) ∈ s A, f if and only if there is a T ∈ s with T connecting x and y. As s = t , this is equivalent to there being a T ∈ t with T connecting x and y, which in turn is equivalent, by Lemma 5.3 again, to having (x, y) ∈ t A, f . As x and y were arbitrary, we have s A, f = t A, f . As A and f were arbitrary, we conclude that Rel(;, +, *, 0, 1, D) | = s = t. Proposition 5.5 (completeness with respect to relations). For any pair s and t of {;, +, *, 0, 1, D}-terms

Rel(;, +, *, 0, 1, D) | = s = t =⇒ s = t .
Proof. Just like the proof of Lemma 4.5. Given S ∈ s , we obtain the existence of a T ∈ t with S ≤ T . By symmetry, there is an S ∈ s with T ≤ S . Since s is a ≤-antichain, S = T . Hence s ⊆ t . By symmetry, also t ⊆ s . With Proposition 5.4 and Proposition 5.5, we can now complete the proof of Theorem 5.6 in the familiar way.

Theorem 5.6. Let Σ be an alphabet, and let R Σ be the set of reduced pointed Σ-labelled rooted trees. Then the free Rel(;, +, *, 0, 1, D)-algebra over Σ has as its universe all the regular subsets of R Σ . The operations are the following, where L, L 1 , and L 2 , are regular sets of reduced trees.

1. 0 ∅, 2. 1 {ε}, 3. L 1 + L 2 maximal(L 1 ∪ L 2 ), 4. L 1 ; L 2 maximal(L 1 ; L 2 ), 5. L * maximal( ∞ i=1 L i )
, where L 0 {ε} and L i+1 L i ; L, 6. D(L) maximal(D(L)).

Proof. Similar to the proof of Theorem 4.6.

Corollary 5.7. Let Σ and R Σ be as in Theorem 5.6.

• The free Rel(;, +, *, 0, D)-algebra over Σ consists of the regular subsets of R Σ that do not contain the trivial tree ε.

• The free Rel(;, +, *, 1, D)-algebra over Σ consists of the nonempty regular subsets of R Σ .

• The free Rel(;, +, *, D)-algebra over Σ consists of the nonempty regular subsets of R Σ that do not contain ε.

Proof. Similar to the proof of Corollary 4.7.

Corollary 5.8. Let Σ and R Σ be as in Theorem 5.6. Then the free Rel(;, +, 0, 1, D)algebra over Σ consists of all finite regular subsets of R Σ .

Proof. First note that the regular subsets interpreting {;, +, 0, 1, D}-terms are precisely the finite regular subsets. Then soundness and completeness follow from Proposition 5.4 and Proposition 5.5 respectively.

In [START_REF] Diarra | Completeness for domain semirings and star-continuous Kleene algebras with domain[END_REF], Mbacke proves (Theorem 5.3.3 there) that a certain finite equational theory over the signature {;, +, 0, 1, D}-the theory of domain semirings-is complete for the equational validities of what amounts to the algebras of trees identified in Corollary 5.8. Hence, we obtain the following corollary.

Corollary 5.9. The axioms of domain semirings provide a finite equational axiomatisation of the equational theory of Rel(;, +, 0, 1, D).

In other words, the axioms of domain semirings are (sound and) equationally complete for algebras of binary relations. In [START_REF] Jipsen | The structure of the one-generated free domain semiring, Relations and Kleene Algebra in Computer Science[END_REF], Jipsen and Struth study the singlygenerated free domain semiring. Corollary 5.8 now subsumes the description of that paper, though that is not to say that these free algebras are uncomplicated objects.

The other main result of [START_REF] Diarra | Completeness for domain semirings and star-continuous Kleene algebras with domain[END_REF] (Theorem 5.3.12 there) is an axiomatisation of the equational validities of our algebras of regular sets of trees. The axiomatisation used consists of the second-order theory of star-continuous Kleene algebras, augmented with one additional second-order axiom: where indicates supremum. Unfortunately, this axiom is not sound for algebras of binary relations. (And so, in particular, it is not a consequence of the axioms of star-continuous Kleene algebras, which are sound for relations.) Hence, we do not obtain an analogue of Corollary 5.9 for the signature {;, +, *, 0, 1, D}.

Automata, and closure under intersection

It is well known that the set of regular languages over a finite alphabet Σ is closed under complement with respect to Σ * . It is clear that, over a (nonempty) finite alphabet, the regular sets of trees are not closed under the complement operation (with respect to the set of reduced trees). And, more meaningfully, this is true even in the view that a regular set L represents the downward-closed set ↓L (since complement does not preserve downward closure). However, as we will show, the regular sets of trees are closed under the following 'intersection' operation.

L 1 • L 2 maximal(↓L 1 ∩ ↓L 2 )
In [START_REF] Hellings | Relative expressive power of downward fragments of navigational query languages on trees and chains[END_REF], and its extended journal version [START_REF] Hellings | Comparing the expressiveness of downward fragments of the relation algebra with transitive closure on trees[END_REF], condition automata are defined. They are an extension of finite-state automata designed specifically for working with relational queries that may contain D (among other tests such as range and antidomain). In this section, we will use a slightly simplified definition of condition automata. Definition 6.1. A domain condition automaton is a 6-tuple (Σ, S , I, T, δ, c), where (Σ, S , I, T, δ) is a finite-state automaton (nondeterministic, with -transitions permitted), and c is a function that assigns a {;, +, *, 0, 1, D}-term (over Σ) to each state S .

A domain condition automaton accepts a path x 0

a 1 → x 1 a 2 → . . . a n →
x n in a relational structure precisely when it is accepted by the finite-state automaton with a trace such that at each step the condition D(c(s)), where s is the current state, is satisfied at the corresponding vertex x in the relational structure (or, to be correct, is satisfied by the pair (x, x)). Lemma 6.2. Let t be a {;, +, *, 0, 1, D}-term, and let T be a pointed labelled rooted tree, with root r and point p. Then the pair (r, p) in the relational structure T satisfies t if and only if there is a T ∈ t with T ≤ T .

Proof. This is just a specialisation of Lemma 5.3 (and the equivalence of the condition T ≤ T with the existence of a homomorphism from T into T ). Proposition 6.3. Let Σ be an alphabet and let L 1 and L 2 be two sets of reduced pointed Σ-labelled finite rooted trees. If L 1 and L 2 are regular, then L 1 • L 2 is regular.

Proof. Let L 1 = t 1 and L 2 = t 2 . Then by [START_REF] Hellings | Relative expressive power of downward fragments of navigational query languages on trees and chains[END_REF]Proposition 5], there is a domain condition automaton A 1 such that for any pointed labelled rooted tree T , with root r and point p, the pair (r, p) satisfies t 1 if and only if the path from r to p is accepted by A 1 . Similarly, there is such a domain condition automaton A 2 for t 2 . By [START_REF] Hellings | Relative expressive power of downward fragments of navigational query languages on trees and chains[END_REF]Proposition 6], there is a domain condition automaton A that accepts a path if and only if that path is accepted by both A 1 and A 2 . Then using [START_REF] Hellings | Relative expressive power of downward fragments of navigational query languages on trees and chains[END_REF]Proposition 5] in the other direction, applied to A, there is a {;, +, *, 0, 1, D}-term t such that for any pointed labelled rooted tree T , with root r and point p, the pair (r, p) satisfies t if and only if it satisfies both t 1 and t 2 .

Applying Lemma 6.

if T ∈ ↓L 1 ∩ ↓L 2 . Hence ↓ t = ↓L 1 ∩ ↓L 2 . So t = maximal(↓ t ) = maximal(↓L 1 ∩ ↓L 2 ) = L 1 • L 2 .
Let (O(R Σ ), ∪, ∩) be the lattice of downward-closed subsets of R Σ . We now know that the sets of the form ↓L, for regular L, form a sublattice of (O(R Σ ), ∪, ∩). Given that (O(R Σ ), ∪, ∩) is a Heyting algebra, this raises the further question of whether the sets of the form ↓L are closed under the implication operation of (O(R Σ ), ∪, ∩). Problem 6.4. Are the regular sets of reduced trees closed under the following implication operation? 5

L 1 → L 2 maximal{ {K ∈ O(Σ) | K ∩ ↓L 1 ⊆ ↓L 2 }}
We conjecture that the answer to this problem is yes. We pose one additional problem, relating to extra-order-theoretic composition structure of the regular sets. Problem 6.5. Are the regular sets of reduced trees closed under the following residuation operations?

L 1 \ L 2 maximal{T ∈ R Σ | ∀S ∈ ↓L 1 , S ; T ∈ ↓L 2 } L 1 / L 2 maximal{T ∈ R Σ | ∀S ∈ ↓L 2 , T ; S ∈ ↓L 1 }
5 Thanks go to one of the anonymous referees for posing this question.

Decidability of equational theory

In this section we describe how to decide the validity of a {;, +, *, 0, 1, D}-equation with respect to relational semantics.

First, we give a definition of condition automata closer to that found in [START_REF] Hellings | Relative expressive power of downward fragments of navigational query languages on trees and chains[END_REF] and [START_REF] Hellings | Comparing the expressiveness of downward fragments of the relation algebra with transitive closure on trees[END_REF]. Recall (Definition 2.3) that A is a unary function symbol whose relational interpretation is the antidomain operation. Definition 7.1. A condition automaton is a 6-tuple (Σ, S , I, T, δ, c), where (Σ, S , I, T, δ) is a finite-state automaton (nondeterministic, with -transitions permitted), and c is a function that assigns a {;, +, *, 0, 1, A}-term (over Σ) to each state S .

Acceptance for condition automata is defined just like acceptance for domain condition automata, where the symbol D is now shorthand for two applications of A.

Theorem 7.2. The equational theory of the class of algebras of binary relations of the signature {;, +, *, 0, 1, D} is decidable. Proof. Let s and t be {;, +, *, 0, 1, D}-terms, and let Σ be the set of variables appearing in either s or t. Now s = t is valid in Rel(;, +, *, 0, 1, D) if and only if the pointed Σlabelled rooted trees satisfying s are precisely those satisfying t-we proved the stronger statement involving reduced trees. In the equivalence just stated, we can temporarily use the usual graph-theoretic definition of a pointed Σ-labelled rooted tree; in particular we do not limit to finite trees. According to [START_REF] Hellings | Relative expressive power of downward fragments of navigational query languages on trees and chains[END_REF]Proposition 5], there are (domain) condition automata A s and A t that accept precisely the finite pointed trees satisfying s and t respectively. But in fact the finiteness condition plays no role, and hence can be dropped. The same remark can be made for the following statements and we will make no further mention of it. By [START_REF] Hellings | Relative expressive power of downward fragments of navigational query languages on trees and chains[END_REF]Corollary 3], there are condition automata A s-t and A t-s such that a pointed tree is accepted by A s-t precisely if it is accepted by A s but not by A t , and a tree is accepted by A t-s precisely if it is accepted by A t but not A s . By [15, Proposition 5], there exist {;, +, *, 0, 1, A}-terms τ s-t and τ t-s such that the pointed trees satisfying τ s-t and τ t-s are precisely those accepted by A s-t and A t-s respectively. Hence s = t is valid in Rel(;, +, *, 0, 1, D) if and only if the sets of pointed Σ-labelled rooted trees satisfying τ s-t and τ t-s are both empty. Finally, we reduce the problem of deciding if a {;, +, *, 0, 1, A}-term τ is satisfiable by a pointed labelled rooted tree to the problem of deciding the satisfiability of a formula of propositional dynamic logic. 6This latter problem is known to be decidable (in EXPTIME [START_REF] Vaughan | A near-optimal method for reasoning about action[END_REF]), so then we are done. See Figure 3 for a summary of the transformations we have outlined. We define a translation from {;, +, *, 0, 1, A}-terms to (propositional variable-free) formulas of propositional dynamic logic as follows. First we define the translation P from {;, +, *, 0, 1, A}-terms to program terms by structural induction as follows. P(a) a P(s ; t) P(s) ; P(t) P(s + t) P(s) + P(t) P(t * ) P(t) * P(0) ⊥? P(1) ? P(A(t)) (¬P(t))?

Then we simply define the translation ϕ(t) of a {;, +, *, 0, 1, A}-term t to be P(t) . It is clear that for any given regular frame, satisfiability of ϕ(t) is equivalent to satisfiability of t on the corresponding relational structure. Since propositional dynamic logic has the tree-model property (any frame with selected point can be 'unwound' to an equivalent labelled rooted tree), we obtain the equivalence of satisfiability of ϕ(t) on regular frames and satisfiability of t on tree-based relational structures. But if t is satisfied by a pair (x, y) of vertices in a tree-based relational structure, then clearly y is a descendent of x, and t is satisfied by the tree rooted at x and having point y. (And conversely, satisfaction by a pointed rooted tree implies satisfaction by a tree-based relational structure.) Hence we have the required equivalence between satisfaction of t with respect to pointed labelled rooted trees and satisfaction of ϕ(t) with respect to regular frames.

The procedure described in the proof of Theorem 7.2 hardly seems efficient. The best upper bound that can be obtained from it is a 3EXPTIME bound. The constructions of A s-t and A t-s rely on determinisations involving a subset construction, so can result in an exponential increase in problem size. Likewise, construction of the terms τ s-t and τ t-s from automata can also add an exponent in general. Lastly, we already mentioned that the final step, deciding satisfiability of propositional dynamic logic formulas, is in EXPTIME, and in fact this problem also has an exponential time lower bound (no O(2 n ε ) algorithm for any ε < 1 [START_REF] Michael | Propositional dynamic logic of regular programs[END_REF]).

We finish with the obvious problem.

Problem 7.3. Determine the precise complexity of deciding validity of {;, +, *, 0, 1, D}equations with respect to relational semantics.

Figure 1 .

 1 Figure 1. The labelled rooted trees encoded as ∅, {(a, ∅)}, and {(a, ∅), (a, {(b, ∅)})}, respectively (with roots at the top)

Figure 2 .

 2 Figure 2. Reduction of pointed labelled rooted trees

Corollary 4 . 4 (

 44 soundness with respect to relations). For any pair s and t of {;, 1, D}terms [s] = [t] =⇒ Rel(;, 1, D) | = s = t. Lemma 4.5 (completeness with respect to relations). For any pair s and t of {;, 1, D}terms Rel(;, 1, D) | = s = t =⇒ [s] = [t]. Proof. Suppose Rel(;, 1, D) | = s = t. We will show that [s] ≤ [t]. Then by symmetry, also [t] ≤ [s]. So [s] = [t] and we are done. Let r be the root and p the point of [s]. On [s] viewed as a relational structure, by using Lemma 4.3 and the identity homomorphism [s] → [s], the pair (r, p) belongs to the model-theoretic interpretation of s (under the evident variable assignment). Hence, by the assumption that Rel(;, 1, D) | = s = t, we have that (r, p) belongs to the modeltheoretic interpretation of t. Then by Lemma 4.3 there is a homomorphism of labelled trees from [t] into [s] mapping the root of [t] to r and the point of [t] to p. That is, there is a homomorphism of pointed labelled rooted trees from [t] into [s]. We know this is equivalent to the conclusion [s] ≤ [t] we seek, so we are done. With Corollary 4.4 and Lemma 4.5 available, we can now complete the proof that we have identified the free algebras of the class Rel(;, 1, D).

  b ; c) → a ; ( b∈B D(b)) ; c = b∈B (a ; D(b) ; c),

  s

  2, we have (for reduced T ) that T ∈ ↓ t if and only if (r, p) satisfies t if and only if (r, p) satisfies both t 1 and t 2 if and only if T ∈ ↓ t 1 and T ∈ ↓ t 2 if and only

  Figure 3. Transformations used to decide equality of t and s

	t	A t
		A s-t	τ s-t	ϕ(τ s-t )
		A t-s	τ t-s	ϕ(τ t-s )
		A s

A quasiequation is a conditional equation where the condition is a finite conjunction of equations. That is, a quasiequation is a formula of the forms 1 = t 1 ∧ • • • ∧ s n = t n → u = v.

In this signature, in which -1 is available, the inverse semigroups form a variety. To give an equational axiomatisation it suffices to replace, in the natural axiomatisation, the quasiequation 'inverses are unique' by the equation a ; a -1 ; a -1 ; a = a -1 ; a ; a ; a -1[START_REF] Schein | On the theory of generalized groups[END_REF].

The short proof of this using general model-theoretic results consists of noting that the class is both closed under direct products and-almost by definition-has a pseudouniversal axiomatisation. (See[START_REF] Hirsch | Relation algebras by games[END_REF] Section 9.2] for a definition of pseudouniversal.)

It is not claimed that this notion of regular sets of pointed trees is the same as the notion of a regular tree language coming from the theory of tree automata[START_REF] Gécseg | Tree languages, Handbook of Formal Languages[END_REF].

See, for example,[START_REF] Michael | Propositional dynamic logic of regular programs[END_REF], for a description of propositional dynamic logic, including the notion of a regular frame.

This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 670624).

A. Appendix

Theorem A.1. The class Rel(;, +, *, 0, 1) is not closed under elementary equivalence.

Proof. By the definition of * on relations, algebras in Rel(;, +, *, 0, 1) validate a * = sup i∈N a i (with respect to the ordering a ≤ b ⇐⇒ a + b = b). Take any relation R whose star R * differs from all finite approximants sup i<n R i -for example take R to be the immediate-successor relation in N. Let A be any algebra of relations containing R-for example the algebra generated by R. Let U be any non-principal ultrafilter on N, and let R be the element of the ultrapower A N /U represented by the constant sequence (R, R, . . . ). Then ( R) * is represented by (R * , R * , . . . ), but this is not a supremum for {R i | i ∈ N} since the strictly smaller element represented by (1, 1 + R, 1 + R + R 2 , . . . ) is also an upper bound. Hence the ultrapower does not validate a * = sup i∈N a i , so Rel(;, +, *, 0, 1) is not closed under ultrapowers. It follows by Łoś's theorem [START_REF] Łoś | Quelques remarques, théorèmes et problèmes sur les classes définissables d'algèbres[END_REF] that Rel(;, +, *, 0, 1) cannot be closed under elementary equivalence.