Romain David
email: romain.david@imbe.fr

Jean-Pierre Feral
email: jean-pierre.feral@imbe.fr

Anne-Sophie Archambeau
email: archambeau@gbif.fr

Nicolas Bailly
email: nbailly@hcmr.gr

Cyrille Blanpain
email: cyrille.blanpain@osupytheas.fr

Vincent Breton
email: breton@idgrilles.fr

Aurélien De Jode
email: aurelien.dejode@imbe.fr

Aurélie Delavaud
email: aurelie.delavaud@fondationbiodiversite.fr

Alrick Dias
email: alrick.dias@imbe.fr

Sophie Gachet
email: sophie.gachet@imbe.fr

Jean-Pierre Féral

Dorian Guillemain
email: dorian.guillemain@imbe.fr

Julien Lecubin
email: julien.lecubin@osupytheas.fr

Geneviève Romier
email: genevieve.romier@idgrilles.fr

Christian Surace
email: christian.surace@lam.fr

Laure Thierry De Ville D'avray

Christos Arvanitidis
email: arvanitidis@hcmr.gr

Anne Chenuil
email: anne.chenuil@imbe.fr

Melih Ertan Ҫinar

Drosos Koutsoubas
email: drosos@aegean.gr

Stéphane Sartoretto
email: stephane.sartoretto@ifremer.fr

Thierry Tatoni
email: thierry.tatoni@imbe.fr

IndexMed projects: new tools using the CIGESMED DataBase on Coralligenous for indexing, visualizing and data mining based on graphs

Keywords: data qualification, graph, thesaurus, distributed information system, coralligenous habitats 1

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Context: big data and interoperability in ecology

Data mining emerged in the late 90s [START_REF] Fayyad | From data mining to knowledge discovery in databases[END_REF] as a discipline to extract relevant novel and understandable knowledge from the analysis of pre-existing datasets and evolved to an increasingly complex approach which includes ecology, among other disciplines. Although currently it is considered, by most information producers and users in scientific disciplines and industry, as the most promising way for making progress and leading to discovery, the use of big data in ecology is still lagging behind other disciplines [START_REF] Peters | Harnessing the power of big data: infusing the scientific method with machine learning to transform ecology[END_REF]. Regarding marine biodiversity and its connection with the coastal socio-ecological systems (SES), data production is still very expensive and with a low level of automation. Studies on long term data series and/or large spatial areas are difficult to conduct, and when several observers need to be involved, the robustness and reproducibility of the observation is very often more difficult to obtain. In a framework production multi-source data in ecology, the equivalence of observation systems and inter-calibration become crucial. Increasingly, integrative transdisciplinary approaches become necessary in the study of systems where information in each discipline is patchy, imprecise and poorly distributed. Yet all variables (biotic, abiotic, anthropogenic and natural pressures, perceived and recognized ecosystem services, societal perception, etc.) of these systems interact in a wide range of spatio-temporal scales [START_REF] Féral | CIGESMED, Coralligenous based Indicators to evaluate and monitor the « Good Environmental Status » of the MEDiterranean coastal waters, a SeasEra project[END_REF][START_REF] Gachet | BASECO: a floristic and ecological database of Mediterranean French flora[END_REF], [START_REF] Conruyt | Moving from biodiversity information systems to biodiversity information services[END_REF]. Some research systems tried to bring out logical interdependencies in socio-ecological systems to facilitate the building of biodiversity and ecosystems services [START_REF] Laporte | A semantic web faceted search system for facilitating building of biodiversity and ecosystems services[END_REF]. Several authors and international initiatives also tried to specify, through a hierarchical approach of biodiversity [START_REF] Noss | Indicators for monitoring biodiversity: a hierarchical approach[END_REF], a common minimum set of variables to be measured, complementary to one another and covering the interlinked biodiversity organization levels. They should allow to capture, with current means and tools, the maximum possible information on biodiversity state and trends with the least effort [START_REF] Pereira | Essential biodiversity variables[END_REF], [START_REF] Kissling | Towards global interoperability for supporting biodiversity research on essential biodiversity variables (EBVs)[END_REF]. Similar initiatives are ongoing for climate, weather and ocean [Connecting GEO] to foster the discovery and the analysis of complementary data across spatial and temporal scales. New opportunities are created by open data formats in ecology [Reichman etal., 2011] and qualification standards usable in data management are developed with the Biodiversity Informatics Standards (formerly Taxonomic Database Working Group) consortium <www.tdwg.org> (Darwin Core Task Group) [START_REF] Wieczorek | Darwin Core: An evolving community-developed biodiversity data standard[END_REF]. Other studies focus on the integration of declarative knowledge with numerical and qualitative data [START_REF] Gibert | Introducing semantic variables in mixed distance measures: Impact on hierarchical clustering[END_REF] or on the post-process of results required to provide understandable knowledge to the end-user [Cortez et al., 2012[START_REF] Gibert | Assisting the end-user in the interpretation of profiles for decision support. an application to wastewater treatment plants[END_REF].

Finally, methods for linking biodiversity and environmental data exist, but they are often limited to an "inventory" aspect of biodiversity (collection, observations, repositories and distribution) and neglect functional aspects. [START_REF] Féral | L'environnement, un système global dynamique. Zone côtière et développement durable, une équation à résoudre[END_REF].

Coralligenous habitat's case

The "coralligenous habitat", an endemic bioherm of the Mediterranean Sea, offers such a particularly complex case of data management. Coralligenous habitats are difficult to study because they are patchy, not easily accessible (between 20 m and 120 m deep) and highly variable in local contexts [START_REF] Ballesteros | Mediterranean coralligenous assemblages: a synthesis of present knowledge[END_REF]. Due to these difficulties and the intrinsic complexity of this habitat type, comprehensive studies were rare until the 2000s [START_REF] Laborel | Le concrétionnement algal "coralligène" et son importance géomorphologique en Méditerranée[END_REF], [START_REF] Laubier | Le Coralligène des Albères. Monographie biocénotique. Adaptations chez les Annélides Polychètes interstitielles[END_REF], [START_REF] Hong | Contribution to the study of populations of the coralligenous concretionary bottom from the Marseille region on the northwestern Mediterranean coast[END_REF], [START_REF] Sartoretto | Structure et dynamique d'un nouveau type de bioconstruction à Mesophyllum lichenoides (Ellis) Lemoine (Corallinales, Rhodophyta)[END_REF]. Most of the proposed monitoring protocols / indicators for its ecological health are developed locally or regionally [START_REF] Deter | A rapid photographic method detects depth gradient in coralligenous assemblages[END_REF], [START_REF] Sartoretto | An integrated approach to evaluate and monitor the conservation state of coralligenous habitats: the Index-Cor approach[END_REF], on a single type of this habitat [START_REF] Pergent-Martini | New data concerning the coralligenous atolls of cap corse: an attempt to shed light on their origin[END_REF], [START_REF] Sini | The Yellow Gorgonian Eunicella cavolini: demography and disturbance levels across the Mediterranean Sea[END_REF]] and use rapid assessment techniques [START_REF] Bianchi | Coralligenous formations in the Marine Protected Area of Tavolara Punta Coda Cavallo(N-E Sardinia, Italy)[END_REF], [START_REF] Kipson | Rapid biodiversity assessment and monitoring method for highly diverse benthic communities: a case study of Mediterranean coralligenous outcrops[END_REF], [START_REF] Deter | A rapid photographic method detects depth gradient in coralligenous assemblages[END_REF], [START_REF] Gatti | Coralligenous reefs state along anthropized coasts: Application and validation of the COARSE index, based on a rapid visual assessment (RVA) approach[END_REF], depending on prevailing environmental conditions.

Coralligenous habitats have been systematically studied at a larger scale within the CIGESMED ERANET'S program (Coralligenous based Indicators to evaluate and monitor the "Good Environmental Status" of the MEDiterranean coastal waters). The main CIGESMED's goal was to understand the connections between pressures (natural or anthropogenic) and the ecosystem functioning in order to define and maintain the Good Environmental Status (GES) of the Mediterranean Sea, by studying the typical, complex and poorly known habitats built by calcareous encrusting algae: the coralligenous habitats. This program is in support of the implementation of the Directive 2008/56/EC of the European Parliament and of the Council of the 17th June 2008. It participates establishing a framework for stakeholders community action in the field of marine environmental policy (Marine Strategy Framework Directive -MSFD), and highlighting descriptors 1 (biological diversity), 2 (non-indigenous species) and 6 (seafloor integrity). The Marine Strategy Framework Directive (MSFD) is directing European Member States towards an implementation of the assessment of marine environmental status. Due to their very high specific richness, including commercial species, and the number of aesthetically important seascapes they hold, coralligenous habitats are one of the most popular marine environments [START_REF] Ballesteros | Mediterranean coralligenous assemblages: a synthesis of present knowledge[END_REF]. The community of CIGESMED redefined it as: "reefs in dim-light conditions mainly bio-constructed on hard substratum by calcifying coralline algae widespread throughout the Mediterranean Sea, including patchwork of habitats complicated by the action of bio-eroders. These complex biogenic formations provide a number of different conditions of light, food and shelter. They are often considered as biodiversity hotspots gathering numerous sessile and sedentary species such as sponges, bryozoans, corals and gorgonians depending on the region and on the depth, to which hundreds of sciaphilic species are associated. These complex environments are a reservoir of natural resources (fisheries, red coral) and form highly valued landscapes sought by divers". The data provided by CIGESMED are now used by the IndexMed consortium as a model, for developing data mining and decision support.

IndexMed, an open consortium

IndexMed is a new consortium in charge of indexing Mediterranean biodiversity data, building and analyzing graphs from heterogeneous databases. It aims to develop new ways for data mining in ecology. This consortium aims to identify and overcome the scientific barriers encountered when working on the quality and heterogeneity of data. The use of emerging data mining methods like graphbased models and analyses allows us to address these issues for improving decision-making support. These methods enable us to detect new patterns of contexts factors, invisible when using multidimensional analyses that have an accurate capacity to indicate particular situations [Klemes, 2015].

DATA INTEGRATOR SYSTEM

The challenge of quality data management to enhance results of data mining

Besides theoretical scientific issues (such as the intrinsic heterogeneity and complexity of biodiversity data, from genes to ecosystems, and their links to environmental parameters), the improvement of data quality is hindered by data management issues, such as: i) the dynamic update of voluminous datasets, ii) the update of reference repositories and standards supporting data management, iii) the heterogeneity of data producers and their motivation to maintain and supply their information systems, and iv) the diversity of the targeted end-users and their skills.

An integrated approach was implemented to mutualize heterogeneous dataset from different scales and disciplinary fields, to allow visualizing large data collections, and to extract new multidisciplinary knowledge in order to study complexity of coralligenous ecosystems. Health quality Indicators, targeting different levels of biodiversity (from communities to genomes), were co-constructed and tested by scientists, stakeholders, and by a citizen science network. Within the CIGESMED program, an upgrade of the design of each protocol and the inter-calibration exercises between various observers, materials, methods and organizations allowed to obtain: i) an assessment of the data variability due to natural or anthropogenic conditions and ii) a comparison of the different methods or observers and their efficiency. It showed that, under the above consensual definition of coralligenous, coralligenous habitats are made of a large panel of different species assemblages. For instance, coralligenous habitats from the Eastern and Western Mediterranean basins may share only 2 or 3 conspicuous species. Comparisons between regions are complicated by this lack of common species and the environmental conditions that can deeply change. Other links between typical environments and species (e.g. traits, contexts, structures, etc.) should be used to build indicators and to compare the environmental status between regions at a Mediterranean scale. Only multi-criteria contextualization by common factor value level allows constructing and adapting the indicators at a local scale and highlighting the significance of this indicator. Finally, it was decided to use competencies and tools developed by the IndexMed consortium to analyse all heterogeneous data, and integrate multidisciplinary data related to coralligenous habitats within the same multi-criterial approach but considering them at a comparable level of importance.

Coralligenous habitats are under anthropogenic uses and threats [START_REF] Ballesteros | Mediterranean coralligenous assemblages: a synthesis of present knowledge[END_REF]. Elaborating and testing "co-interpretation methods" of analyses (i.e. different datasets from different disciplines in the same time, at a same level of integration) is thought to be a keystone to mix in the same studies these heterogeneous data from different socio-economics disciplines and biodiversity disciplines, from the genome to the seascapes level. The ultimate goal is to propose scenarios to reach the sustainable management of biodiversity balancing exploitation and conservation. Data mining methods will be able to bring new perspectives to the disciplinary researches that finally examine interrelated objects (e.g. environmental chemistry, genomics, transcriptomics, metabolomics, population ecology / landscape, socio-ecological systems).

Workflow and e-services

To be able to use different and distributed datasets for data mining, a prototype of "object resolution service" (i.e. a web service that finds links and dependencies among indexed objects, based on unique objects identification (Figure 1)) that can be replicated by stakeholders is shared on a nodal point. It is intended to be replicable as a free software and a free service from European grids (EGI and others).

The aims of this prototype are to i) list available data and data stream, ii) analyse content of datasets and data streams with standards referential, iii) qualify streams, datasets with unique identifiers if there is no identifiers, iv) suggest matches between fields to users /matches between equivalent data rows.

The role of this object resolution service is to establish links between data row with different "unique identifiers" (e.g. different versions of data raw, interdependencies between raw data and transformed data, etc.). Heterogeneity in datasets may be the result of a lack of standards to name and describe data [START_REF] Kattge | A generic structure for plant trait databases[END_REF][START_REF] Madin | Advancing ecological research with ontologies[END_REF]. Thus, attention must be paid to the characterisation of concepts by using "controlled vocabulary" (i.e. with a shared definition commonly choose) and semantic links between these concepts, which implies building a thesaurus in the first place. Thesaurus appears more appropriate than ontology because of its flexibility. Several eco-informatics initiatives attempted to build such thesaurus (see [START_REF] Michener | Ecoinformatics: supporting ecology as a data-intensive science[END_REF][START_REF] Laporte | ThesauForm-Traits: A web based collaborative tool to develop a thesaurus for plant functional diversity research[END_REF]) and it is expected to take them in account.

New data qualifications generated by IndexMed prototypes aim at following the "guidelines on Data Management in Horizon 2020" (V2.

CASE STUDY

The first tool, developed commonly by the CIGESMED and the IndexMed communities for scientists working on biodiversity, is a prototype web interface building dynamic maps of data and their possible links based on the graphs theory [START_REF] David | A First Prototype for Indexing, Visualizing and Mining Heterogeneous Data in Mediterranean Ecology: Within the IndexMed Consortium Interdisciplinary Framework[END_REF]. It can be used to establish links between objects of different disciplines and is able to connect data without centralizing them. The first aim is to teach the community on how to use the graph approach, featuring a didactic and ergonomic interface (Figure 2) with the aims to improve by step user level. It allows evaluating the data quality level and identifying the best ways to improve their efficiency (e.g. density, sensibility, velocity, accuracy, etc.). A tool permits to keep the new models designed by users (i.e. link and node selections) and new items (more than 1 object in a node) and produces a single stream usable by data centers at different formats (NoSQL exports in RDF, Json, XML formats) with a persistent URL. In the case presented in figure 2, photo quadrats selected by the interface are the nodes of the graph, species frequency selected by the user build 1000 links between photo quadrats, the colours of nodes highlight different elements of contexts (here, different observers). Node legends are the names of the observed sites. The more photo quadrats contain similar species assemblages, the more they are attracted. We can observe that some photo quadrats of different sites are attracted, thus similar in term of species frequencies, and very ubiquitous (cluster 2 in the centre of the graph). In cluster 3 photo quadrats are homogeneous and typical of the site. In the rim of cluster 3, some photo quadrats of other sites constitute a particular group. Cluster 1 shows another type of photo quadrats, less present in each site but represented everywhere.

In the example of figure 2, datasets come from 3 different protocols and data production systems, including one based on photo quadrats analyses with the software photoQuad [Trigonis and Sini, 2012],

a cartography of ecological/physical contexts and genetic data. Data objects represented on the graph are photos coming from different sites. Objects can be selected using the context control panel. Clusters visible in figure 2 can be modified by selection of context or species choice for the links. The relative importance of each species can be modified in the links (e.g. depending of the status or a specific trait) and some context elements can be selected to participate to links between nodes. Observers, highlighted by colours of nodes are not evenly distributed. Experience of observers is reflected in the size of nodes.

This interface uses indexed data, data qualification, and data traceability for discovering patterns in the conjunctions of data values with scientific significance. The graph design can be manipulated on a web browser interface, the request and manipulations steps can be stored on a personal account and the result allows installing a flux at XML or JSON format available on a web service for data mining or another indexing service.

4

OUTPUT AND SERVICES

organizing data means organizing access and improving quality

The description of data quality is an objective of the IndexMed consortium <http://www.indexmed.eu> that can be useful for data about coralligenous, based on an analysis of both similarities and differences between databases. Descriptions as metadata form a set of criteria used for data mining. The graphbased model is an abstraction tool that enables the comparison of various databases despite their differences and that improves decision support using emerging data mining methods. Practically, it is intended to give the equivalence of data, based on data dictionaries, thesauri and ontologies. From the established logical relationships, new qualifiers can be deduced including across data heterogeneity.

This work on CIGESMED data quality and their equivalence with other observatory systems involves first the analysis and description of the common elements of each piece of information, and of what differentiates them (fields name, formats, update rate, precision, observers or sensors, etc.). These descriptions are added to the data, and form a supplementary set of criteria used for data mining.

Standard formats and protocols are used to interconnect CIGESMED data with other databases.

Standardization makes possible such a work, as well as a special task on interoperability qualities and accessibility of non-centralized data. It uses aggregation and new visualizations for public display, multiinterface, multi-use and multi-format, and must allow (i) the connection between many databases, and (ii) the preparation of inter-calibration works. Equivalencies are used to link heterogeneous objects and construct graphs, where objects are nodes and attribute's modalities are links. The main output is a new model of dataset, stored in a graph database (graph matrix) and accessible with web-services for visualization and integrated flux. A second output is the improving of multicommunity thesaurus necessary to build new common ecological concepts. The next step of this project is the recognition of patterns of context in the graph matrix that will contribute to decision criteria.

Semantic approaches greatly increase their interoperability and some initiatives using Semantic Web technologies for retrieving Biodiversity data [START_REF] Amanqui | Improving biodiversity data retrieval through semantic search and ontologies[END_REF] and developing methods for linking biodiversity and environmental data already exist, but they often concern only an "inventory" aspect. However, it remains that specific scientific objectives, organizational logic of projects and collection of information are leading to a decentralized data distribution which may hamper environmental research development. In such a heterogeneous system footed on different organizations and data formats, not everything can be homogenized. The IndexMed workflow is a support to implement an iterative quality approach (Figure 3) increasing step by step the capacity of each data to be connected to others (i.e. contextual data like biotic, abiotic, anthropogenic and natural pressures, etc.)

The resulting cluster and their correlations to context patterns can be compared with other kinds of analyses: supervised clustering results, statistical ecology approach [START_REF] Gimenez | Statistical ecology comes of age[END_REF] and collaborative clustering methods [START_REF] Forestier | Multisource images analysis using collaborative clustering[END_REF] are planned to be used at each part (e.g. a group of nearby nodes with similar patterns of context) of the graph, using job middleware (DIRAC3, [START_REF] Tsaregorodtsev | DIRAC3 . The New Generation of the LHCb Grid Software[END_REF]). Another issue is to use "unsupervised" mode, raising the possibility to compare the results of different algorithms to achieve consensus, which acts / results in the most likely scenario. The data mining helps finding managerial values of qualifiers to propose scenarios, and provides new standardized descriptors essential for approaches such as machine learning.

Efficiency for data mining approach and links with decision support

The chain between data and decision making can be superimposed to the DIKW (u) hierarchy: Data, Information, Knowledge, Wisdom, Understanding [START_REF] Zeleny | Management support systems: towards integrated knowledge management[END_REF][START_REF] Ackoff | From data to wisdom[END_REF], replacing Wisdom by Management. In a simplistic view, scientists produce knowledge by analysing data into information and by elaborating theories from information. Data constitute the primary material from which hypotheses are 1) elaborated, and 2) tested. However, even if biodiversity data have been produced in the common framework of the theory of evolution, it has often been done independently in different domains from genes to ecosystems; moreover, biodiversity data are historical in essence, they have a time component: species have been observed at a given location at a given time, and this is not reproducible as it could be done easier for physico-chemical experiments. Consequently, every piece of data in each domain may be of importance, and for older ones, they may need to be re-expressed to fit under their current conceptual and standard forms, in particular to use them all in a common approach like here. We are thus dealing with millions of pages of scientific literature and the increasing number of data repositories since Aristotle [START_REF] Voultsiadou | Sponges: An historical survey of their knowledge in Greek antiquity[END_REF]. The Biodiversity Heritage Library <http://www.biodiversitylibrary.org/> is already making available almost 50 million pages (and still increasing), mainly up to 1930s because of copyright issues: since the scientific production progresses exponentially, we may talk here about billions of pages. Even narratives of travels and expeditions can be used to extract biodiversity semi-quantitative data [START_REF] Al-Abdulrazzak | Gaining perspective on what we've lost: the reliability of encoded anecdotes in historical ecology[END_REF].

The development of new data mining tools becomes crucial to explore automatically all sources of biodiversity data, or currently more reasonably semi-automatically, in order to produce the most complete knowledge that constitutes the decision support material (but not the decision-making tools by themselves!). This knowledge is the basis for developing alternative future scenarios about the biodiversity management among which decision and policy-makers will make a political choice. The graph approach may allow going a step further by integrating socio-economic knowledge in these scientifically supported scenarios. Currently, this integration is made at the decision making level, where biodiversity and socio-economics scenarios are on the contrary put in competition, most often to the benefit of the socio-economics scenarios, with too many examples from the domain of fisheries [START_REF] Froese | Fishery reform slips through the net[END_REF].

CONCLUSIONS AND RECOMMENDATIONS

Compared with dimensional and multidimensional analyses, which are often used for ecological and environmental purposes, such innovative approaches make possible the investigation of complex research questions and the emergence of new scientific hypotheses. Regarding the first results, environmental scientists and environmental managers from CIGESMED and from the IndexMed consortium have to face different challenges about links between data and well understanding of the meaning of new objects and their variation. For better analysing heterogeneously distributed data spread in different databases and for identifying statistical relationships between observed data and the emergence of contextual patterns, it will be necessary to create matches and incorporate some approximations.

The area of Decision Support Systems (DSS) focuses on development of interactive software that can use data mining export of IndexMed prototypes. This prototype aims to provide qualifiers that can be interpreted in patterns as answers to relevant decisional questions from the users, thus enhancing a person or a group to make better decisions. Till now, important efforts to develop links between Indexmed and dedicated DSS are required and possible for every particular application [Varanon et al., 2007[START_REF] Power | A Brief History of Decision Support Systems[END_REF]. Specific DSS linked to IndexMed must be experimented where some successful experiences appear in several fields, like self-care management [START_REF] Marschollek | Decision support at home (DS@ HOME)-system architectures and requirements[END_REF], water management [START_REF] Pallottino | A DSS for water resources management under uncertainty by scenario analysis[END_REF], forest ecosystems [START_REF] Nute | NED-2: an agent-based decision support system for forest ecosystem management[END_REF] or air pollution [START_REF] Oprea | A case study of knowledge modelling in an air pollution control decision support system[END_REF]. IndexMed community is open to contribution. IndexMed software are open source and privileged case studies are open data, and the involved teams plan to set up a forge and a contributory platform for expanding testing graph approaches.

Multidisciplinary approaches are a key as well as the most difficult way to improve data mining and DSS. At a "human" level, it is seriously necessary to encourage the data openness and data sharing, as the only way to give value to data after their primary use [START_REF] Mcnutt | Liberating field science samples and data[END_REF]. A good start might be to organize more events dedicated to the sharing of experience and expertise, the acquisition of practical methods to construct graphs and value data through "metadata and data papers".

  Initiatives like CoL [Catalogue of Life], Data-ONE [Data Observation Network for Earth], EMODnet [European Marine Observation and Data Network], GEO-BON [Group On Earth Observations Biodiversity Observation Network], EU-BON [European Biodiversity Observation Network], GBIF [Global Biodiversity Information Facilities], LifeWatch, OBIS [Ocean Biogeographic Information System], and TDWG [Biodiversity Information Standards] along with Darwin Core and ABCD [Access to Biological Collections Data], are well-known examples for achieving interoperability and standardizing data collection. However, integrative approaches in the coastal management zone need more interoperability at each scale

Figure 1 -

 1 Figure 1 -IndexMed Workflow and eservices:The resolution service is able to compare the index with storage data in einfrastructures and other distant XML, JSON Flux from different databases. When necessary/possible, it creates a persistent identifier or links datasets or data records with existing identifiers. A scientist interface, adapted to the level and needs of each user allows a qualification process. The indexing service accept/manages data for computing services like data mining and graph analyses, and statistical results and graph models are stored and proposed as a new persistent flux. When it is possible, data qualification uses tools, standards and recommendations at both national (SINP [National Information System on Biodiversity], RBDD [Network of Research Databases]) and international levels (MedOBIS [Mediterranean Ocean Biogeographic Information System], OBIS, GBIF [Cryer et al., 2009], Life-Watch, GEO-BON, etc.) or shared by other research entities (i.e. IRD [Institute of Research for the Development] or MNHN [National Museum of Natural History, Paris]).Heterogeneity in datasets may be the result of a lack of standards to name and describe data[START_REF] Kattge | A generic structure for plant trait databases[END_REF][START_REF] Madin | Advancing ecological research with ontologies[END_REF]. Thus, attention must be paid to the characterisation of concepts by using "controlled vocabulary" (i.e. with a shared definition commonly choose) and semantic links between these concepts, which implies building a thesaurus in the first place. Thesaurus appears more appropriate than ontology because of its flexibility. Several eco-informatics initiatives attempted to build such thesaurus (see[START_REF] Michener | Ecoinformatics: supporting ecology as a data-intensive science[END_REF][START_REF] Laporte | ThesauForm-Traits: A web based collaborative tool to develop a thesaurus for plant functional diversity research[END_REF]) and it is expected to take them in account.

Figure 2 :

 2 Figure 2: Example of an application of the prototype graph to a data set of 100 photo-quadrats made on coralligenous habitats in Marseille.

Figure 3 :

 3 Figure 3: Iterative quality approach and IndexMed Output.

  data maintenance and curation (Horizon 2020 Annotated Grant Agreement for articles 29.2 and 29.3, IP/12/790 on open access in Horizon 2020. <http://ec.europa.eu/research/participants/docs/h2020-funding-guide/cross-cutting-issues/openaccess-data-management/open-access_en.htm>)

1, 15 Feb. 2016

) and cover, as recommended, the handling of research data during and after the project : data type, data collection (processed or generated), methodology of collect, standards used, post project data availability and access (open access as it is possible),

ACKNOWLEDGMENTS

The construction of the first prototype for IndexMed consortium is funded by the CNRS défi "VIGI-GEEK (VIsualisation of Graph In transdisciplinary Global Ecology, Economy and Sociology data-Kernel)" and CNRS INEE through the "CHARLIEE" project. Data used for this article were obtained through the European CIGESMED project <www.cigesmed.eu> (ANR conventions n° 12-SEAS-0001-01, 02 and 03 for France; GSRT -12SEAS-12-C2 for Greece; TUBITAK Project No: 112Y393 for Turkey). The authors acknowledge the support of France Grilles for providing computing resources on the French National Grid Infrastructure. Supplementary acknowledgement to Gergely Sipos, Jan Bot and Roberta Piscitelli for the helpful support provided at "design your e-infrastructure" EGI <www.egi.eu> workshop. We acknowledge all the field helpers and students who have participated in data collection in the field and in the lab, as well as in data management.


Beniamino Accattoli
email: beniamino.accattoli@inria.fr

The Complexity of Abstract Machines

The λ -calculus is a peculiar computational model whose definition does not come with a notion of machine. Unsurprisingly, implementations of the λ -calculus have been studied for decades. Abstract machines are implementations schemas for fixed evaluation strategies that are a compromise between theory and practice: they are concrete enough to provide a notion of machine and abstract enough to avoid the many intricacies of actual implementations. There is an extensive literature about abstract machines for the λ -calculus, and yet-quite mysteriously-the efficiency of these machines with respect to the strategy that they implement has almost never been studied.

This paper provides an unusual introduction to abstract machines, based on the complexity of their overhead with respect to the length of the implemented strategies. It is conceived to be a tutorial, focusing on the case study of implementing the weak head (call-by-name) strategy, and yet it is an original re-elaboration of known results. Moreover, some of the observations contained here never appeared in print before.

Cost Models & Size-Explosion

The λ -calculus is an undeniably elegant computational model. Its definition is given by three constructors and only one computational rule, and yet it is Turing-complete. A charming feature is that it does not rest on any notion of machine or automaton. The catch, however, is that its cost model are far from being evident. What should be taken as time and space measures for the λ -calculus? The natural answers are the number of computational steps (for time) and the maximum size of the terms involved in a computation (for space). Everyone having played with the λ -calculus would immediately point out a problem: the λ -calculus is a nondeterministic system where the number of steps depends much on the evaluation strategy, so much that some strategies may diverge when others provide a result (but fortunately the result, if any, does not depend on the strategy). While this is certainly an issue to address, it is not the serious one. The big deal is called size-explosion, and it affects all evaluation strategies. Size-Explosion. There are families of terms where the size of the n-th term is linear in n, evaluation takes a linear number of steps, but the size of the result is exponential in n. Therefore, the number of steps does not even account for the time to write down the result, and thus at first sight it does not look as a reasonable cost model. Let's see examples.

The simplest one is a variation over the famous looping λ -term Ω := (λ x.xx)(λ x.xx) → β Ω → β . . .. In Ω there is an infinite sequence of duplications. In the first size-exploding family there is a sequence of n nested duplications. We define both the family {t n } n∈N of size-exploding terms and the family {u n } n∈N of results of the evaluation t 0 := y u 0 := y t n+1 := (λ x.xx)t n u n+1 := u n u n

We use |t| for the size of a term, i.e. the number of symbols to write it, and say that a term is neutral if it is normal and it is not an abstraction. Proof. By induction on n. The base case is immediate. The inductive case: t n+1 = (λ x.xx)t n → n β (λ x.xx)u n → β u n u n = u n+1 , where the first sequence is obtained by the i.h. The bounds on the sizes are immediate, as well as the fact that u n+1 is neutral.

Strategy-Independent Size-Explosion. The example relies on rightmost-innermost evaluation (i.e. the strategy that repeatedly selects the rightmost-innermost β -redex) and open terms (the free variable t 0 = y). In fact, evaluating the same family in a leftmost-outermost way would produce an exponentially long evaluation sequence. One may then believe that size-explosion is a by-product of a clumsy choice for the evaluation strategy. Unfortunately, this is not the case. It is not hard to modify the example as to make it strategy-independent, and it is also easy to get rid of open terms. Let the identity combinator be I := λ z.z (it can in fact be replaced by any closed abstraction). Define The size-exploding family is {r n I} n∈N , i.e. it is obtained by applying r n to the identity I = p 0 . The statement we are going to prove is in fact more general, about r n p m instead of just r n I, in order to obtain a simple inductive proof. The family {r n I} n∈N is interesting because no matter how one looks at it, it always explodes: if evaluation is weak (i.e. it does not go under abstraction) there is only one possible derivation to normal form and if it is strong (i.e. unrestricted) all derivations have the same length (and are permutatively equivalent). To our knowledge this family never appeared in print before.

2 The λ -Calculus is Reasonable, Indeed Surprisingly, the isolation and the systematic study of the size-explosion problem is quite recent-there is no trace of it in the classic books on the λ -calculus, nor in any course notes we are aware of. Its essence, nonetheless, has been widespread folklore for a long time: in practice, functional languages never implement full β -reduction, considered a costly operation, and theoretically the λ -calculus is usually considered a model not suited for complexity analyses.

A way out of the issue of cost models for the λ -calculus, at first sight, is to take the time and space required for the execution of a λ -term in a fixed implementation. There is however no canonical implementation. The design of an implementation in fact rests on a number of choices. Consequently, there are a number of different but more or less equivalent machines taking a different number of steps and using different amounts of space to evaluate a term. Fixing one of them would be arbitrary, and, most importantly, would betray the machine-independent spirit of the λ -calculus.

Micro-

Step Operational Semantics. Luckily, the size-explosion problem can be solved in a machineindependent way. Somewhat counterintuitively, in fact, the number of β -steps can be taken as a reasonable cost model. The basic idea is simple: one has to step out of the λ -calculus, by switching to a different setting that mimics β -reduction without literally doing it, acting on compact representations of terms to avoid size-explosion. Essentially, the recipe requires four ingredients:

1. Statics: λ -terms are refined with a form of sharing of subterms; 2. Dynamics: evaluation has to manipulate terms with sharing via micro-operations; The recipe leaves also some space for improvisation: λ -calculus can in fact be enriched with first-class sharing in various ways. Mainly, there are three approaches: abstract machines, explicit substitutions, and graph rewriting. They differ in the details but not in the essence-they can be grouped together under the slogan micro-step operational semantics.

Reasonable Strategies. An evaluation strategy → for the λ -calculus is reasonable if there is a microstep operational semantics M mimicking → and such that the number of micro-steps to evaluate a term t is polynomial in the number of →-steps to evaluate t (and in the size of t, we will come back to this point later on). If a strategy → is reasonable then its length is a reasonable cost model, despite sizeexplosion: the idea is that the λ -calculus is kept as an abstract model, easy to define and reason about, while complexity-concerned evaluation is meant to be performed at the more sophisticated micro-step level, where the explosion cannot happen.

Of course, the design of a reasonable micro-step operational semantics depends much on the strategy and the chosen flavor of micro-steps semantics, and it can be far from easy. For weak strategies-used to model functional programming languages-reasonable micro-steps semantics are based on a simple form of sharing. The first result about reasonable strategies was obtained by Blelloch and Greiner in 1995 [START_REF] Blelloch | Parallelism in Sequential Functional Languages[END_REF] and concerns indeed a weak strategy, namely the call-by-value one. At the micro-step level it relies on abstract machines. Similar results were then proved again, independently, by Sands, Gustavsson, and Moran in 2002 [START_REF] Sands | Lambda Calculi and Linear Speedups[END_REF] and by Dal Lago and Martini in 2006 [START_REF] Dal | An Invariant Cost Model for the Lambda Calculus[END_REF]. For strong strategies-at work in proof assistant engines-quite more effort and care are required. A sophisticated second-level of sharing, called useful sharing, is necessary to obtain reasonable micro-step semantics for strong evaluation. The first such semantics has been introduced by Accattoli and Dal Lago in 2014 [START_REF] Accattoli | Beta reduction is invariant, indeed[END_REF] for the leftmost-outermost strategy, and its study is still ongoing [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF][START_REF] Accattoli | The Useful MAM, a Reasonable Implementation of the Strong λ -Calculus[END_REF].

The Complexity of Abstract Machines. To sum up, various techniques, among which abstract machines, can be used to prove that the number of β -steps is a reasonable time cost model, i.e. a metric for time complexity. The study can then be reversed, exploring how to use this metric to study the relative complexity of abstract machines, that is, the complexity of the overhead of the machine with respect to the number of β -steps. Such a study leads to a new quantitative theory of abstract machines, where machines can be compared and the value of different design choices can be measured. The rest of the paper provides a gentle introduction to the basic concepts of the new complexity-aware theory of abstract machines being developed by the author in joint works [START_REF] Accattoli | Distilling abstract machines[END_REF][START_REF] Accattoli | On the Value of Variables[END_REF][START_REF] Accattoli | A Strong Distillery[END_REF][START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF][START_REF] Accattoli | The Useful MAM, a Reasonable Implementation of the Strong λ -Calculus[END_REF] with Damiano Mazza, Pablo Barenbaum, and Claudio Sacerdoti Coen, and resting on tools and concepts developed beforehand in collaborations with Delia Kesner [START_REF] Accattoli | The Structural λ -Calculus[END_REF] and Ugo Dal Lago [START_REF] Accattoli | On the Invariance of the Unitary Cost Model for Head Reduction[END_REF], as well as Kesner plus Eduardo Bonelli and Carlos Lombardi [START_REF] Accattoli | A nonstandard standardization theorem[END_REF].

Case Study: Weak Head Strategy. The paper focuses on a case study, the weak head (call-by-name) strategy, also known as weak head reduction (we use reduction and strategy as synonymous, and prefer strategy), and defined as follows:

(root β ) (λ x.t)u → wh t{x u} t → wh u (@l) tr → wh ur (1)
This is probably the simplest possible evaluation strategy. Of course, it is deterministic. Let us mention two other ways of defining it, as they will be useful in the sequel. First, the given inductive definition can be unfolded into a single synthetic rule (λ x.t)ur 1 . . . r k → wh t{x u}r 1 . . . r k . Second, the strategy can be given via evaluation contexts: define E := • | Er and define → wh as E (λ x.t)u → wh E t{x u} (where E t is the operation of plugging t in the context E, consisting in replacing the hole • with t). Sometimes, to stress the modularity of the reasoning, we will abstract the weak head strategy into a generic strategy →. Last, a derivation is a possibly empty sequence of rewriting steps.

Introducing Abstract Machines

Tasks of Abstract Machines. An abstract machine is an implementation schema for an evaluation strategy → with sufficiently atomic operations and without too many details. A machine for → accounts for 3 tasks:

1. Search: searching for →-redexes; 2. Substitution: replace meta-level substitution with an approximation based on sharing; 3. Names: take care of α-equivalence.

Dissecting Abstract Machines. To guide the reader through the different concepts to design and analyze abstract machines, the next two subsections describe in detail two toy machines that address in isolation the first two mentioned tasks, search and substitution. They will then be merged into the Milner Abstract Machine (MAM). In Sect. 7 we will analyze the complexity of the MAM. Next, we will address names and describe the Krivine Abstract Machine, and quickly study its complexity.

Abstract Machines Glossary.

• An abstract machine M is given by states, noted s, and transitions between them, noted ;

• A state is given by the code under evaluation plus some data-structures to implement search and substitution, and to take care of names;

• The code under evaluation, as well as the other pieces of code scattered in the data-structures, are λ -terms not considered modulo α-equivalence; • Codes are over-lined, to stress the different treatment of α-equivalence;

• A code t is well-named if x may occur only in u (if at all) for every sub-code λ x.u of t;

• A state s is initial if its code is well-named and its data-structures are empty;

• Therefore, there is a bijection • • (up to α) between terms and initial states, called compilation, sending a term t on the initial state t • on a well-named code α-equivalent to t;

• An execution is a (potentially empty) sequence of transitions s * s from an initial state s obtained by compiling a(n initial) term t 0 ;

• A state s is reachable if it can be obtained as the end state of an execution;

• A state s is final if it is reachable and no transitions apply to s.

• A machine comes with a map • from states to terms, called decoding, that on initial states is the inverse (up to α) of compilation;

• A machine M has a set of β -transitions that are meant to be mapped to β -redexes (and whose name involves β ) by the decoding, while the remaining overhead transitions are mapped on equalities;

• We use |ρ| for the length of an execution ρ, and |ρ| β for the number of β -transitions in ρ.

Implementations. For every machine one has to prove that it correctly implements the strategy it was conceived for. Our notion, tuned towards complexity analyses, requires a perfect match between the number of β -steps of the strategy and the number of β -transitions of the machine execution. Definition 3.1 (Machine Implementation). A machine M implements a strategy → on λ -terms when given a λ -term t the following holds 1. Executions to Derivations: for any M-execution ρ : t Note that if a machine implements a strategy than the two are weakly bisimilar, where weakness is given by the fact that overhead transitions do not have an equivalent on the calculus (hence their name). Let us point out, moreover, that the β -matching requirement in our notion of implementation is unusual but perfectly reasonable, as all abstract machines we are aware of do satisfy it.

The Searching Abstract Machine

Strategies are usually specified through inductive rules as those in [START_REF] Accattoli | An Abstract Factorization Theorem for Explicit Substitutions[END_REF]. The inductive rules incorporate in the definition the search for the next redex to reduce. Abstract machines make such a search explicit and actually ensure two related subtasks:

1. Store the current evaluation context in appropriate data-structures.

Search incrementally, exploiting previous searches.

For weak head reduction the search mechanism is basic. The data structure is simply a stack π storing the arguments of the current head subterm.

Searching Abstract Machine. The searching abstract machine (Searching AM) in Fig. 1 has two components, the code in evaluation position and the argument stack. The machine has only two transitions, corresponding to the rules in (1), one β -transition ( rβ ) dealing with β -redexes in evaluation position and one overhead transition ( @l ) adding a term on the argument stack. Compilation of a (well-named) term t into a machine state simply sends t to the initial state (t, ε). The decoding given in Fig. 1 is defined inductively on the structure of states. It can equivalently be given contextually, by associating an evaluation context to the data structures-in our case sending the argument stack π to a context π by setting ε := • , u :: π := π • u , and (t, π) := π t . It is useful to have both definitions since sometimes one is more convenient than the other. Implementation. We now show the implementation theorem for the Searching AM with respect to the weak head strategy. Despite the simplicity of the machine, we provide a quite accurate account of the proof of the theorem, to be taken as a modular recipe. The proofs of the other implementation theorems in the paper will then be omitted as they follow exactly the same structure, mutatis mutandis.

The Complexity of Abstract Machines

The executions-to-derivations part of the implementation theorem always rests on a lemma about the decoding of transitions, that in our case takes the following form. 2. Overhead Transition: if s @l s then s = s .

Proof. The first point is more easily proved using the contextual definition of decoding.

1. s = (λ x.t, u :: π) = u :: π λ x.t = π (λ x.t)u → β π t{x u} = s . 2. s = (t, u :: π) = (tu, π) = s.
Transitions decoding extends to a projection of executions to derivations (via a straightforward induction on the length of the execution), as required by the implementation theorem. For the derivationsto-executions part of the theorem, we proceed similarly, by first proving that single weak head steps are simulated by the Searching AM and then extending the simulation to derivations via an easy induction. There is a subtlety, however, because, if done naively, one-step simulations do not compose.

Let us explain the point. Given a step t → wh u there exists a state s such that t • * @l rβ s and s = u, as expected. This property, however, cannot be iterated to build a many-steps simulation, because s = u does not imply s = u • , i.e. s in general is not the compilation of u. To make things work, the simulation of t → wh u should not start from t • but from a state s such that s = t. Now, the proof of the step simulation lemma we just described relies on the following three properties: 1. Vanishing Transitions Terminate: @l terminates; 2. Determinism: the Searching AM is deterministic; 3. Progress: final Searching AM states decode to → wh -normal terms.

Proof. Termination: @l -sequences are bound by the size of the code. Determinism: rβ and @l clearly do not overlap and can be applied in a unique way. Progress: final states have the form (λ x.t, ε) and (x, π), that both decode to → wh -normal forms. Proof. Let nf @l (s) be the normal form of s with respect to @l , that exists and is unique by termination of @l (Lemma 4.2.1) and determinism of the machine (Lemma 4.2.2). Since @l is mapped on identities (Lemma 4.1.2) one has nf @l (s) = s. By hypothesis s → wh -reduces, so that by progress (Lemma 4.2.3) nf @l (s) cannot be final. Then nf @l (s) rβ s , and nf @l (s) = s → wh s by the one-step simulation lemma (Lemma 4.1.1). By determinism of → wh , one obtains s = u.

Environments E := ε | [x t] :: E Compilation t • := (t,
Finally, we obtain the implementation theorem.

The Micro-Substituting Abstract Machine

Decomposing Meta-Level Substitution. The second task of abstract machines is to replace meta-level substitution t{x u} with micro-step substitution on demand, i.e. a parsimonious approximation of metalevel substitution based on:

1. Sharing: when a β -redex (λ x.t)u is in evaluation position it is fired but the meta-level substitution t{x u} is delayed, by introducing an annotation [x u] in a data-structure for delayed substitutions called environment;

2. Micro-Step Substitution: variable occurrences are replaced one at a time;

3. Substitution on Demand: replacement of a variable occurrence happens only when it ends up in evaluation position-variable occurrences that do not end in evaluation position are never substituted.

The purpose of this section is to illustrate this process in isolation via the study of a toy machine, the Micro-Substituting Abstract Machine (Micro AM) in Fig. 2, forgetting about the search for redexes.

Environments. We are going to treat environments in an unusual way: the literature mostly deals with local environments, to be discussed in Sect. 9, while here we prefer to first address the simpler notion of global environment, but to ease the terminology we will simply call them environments. So, an environment E is a list of entries of the form [x u]. Each entry denotes the delayed substitution of u for x. In a state (t, E :: [x u] :: E ) the scope of x is given by t and E , as it is stated by forthcoming Lemma 5.1. The (global) environment models a store. As it is standard in the literature, it is a list, but the list structure is only used to obtain a simple decoding and a handy delimitation of the scope of its entries. These properties are useful to develop the meta-theory of abstract machines, but keep in mind that (global) environments are not meant to be implemented as lists.

Code. The code under evaluation is now a λ -term hr 1 . . . r k expressed as a head h (that is either a βredex (λ x.t)u or a variable x) applied to k arguments-it is a by-product of the fact that the Micro AM does not address search.

Transitions. There are two transitions:

• Delaying β : transition dβ removes the β -redex (λ x.t)u but does not execute the expected substitution {x u}, it rather delays it, adding [x u] to the environment. It is the β -transition of the Micro AM.

• Micro-Substitution On Demand: if the head of the code is a variable x and there is an entry [x t] in the environment then transition var replaces that occurrence of x-and only that occurrencewith a copy of t. It is necessary to rename the new copy of t (into a well-named term) to avoid name clashes. It is the overhead transition of the Micro AM.

Implementation. Compilation sends a (well-named) term t to the initial state (t, ε), as for the Searching AM (but now the empty data-structure is the environment). The decoding simply applies the delayed substitutions in the environment to the term, considering them as meta-level substitutions. The implementation of weak head reduction → wh by the Micro AM can be shown using the recipe given for the Searching AM, and it is therefore omitted. The only difference is in the proof that the overhead transition var terminates, that is based on a different argument. We spell it out because it will be useful also later on for complexity analyses. It requires the following invariant of machine executions: Lemma 5.1 (Name Invariant). Let s = (t, E) be a Micro AM reachable state.

1. Abstractions: if λ x.u is a subterm of t or of any code in E then x may occur only in u;

2. Environment: if E = E :: [x u] :: E then x is fresh with respect to u and E .

Proof. By induction on the length of the execution ρ leading to s. If ρ is empty then s is initial and the statement holds because t is well-named by hypothesis. If ρ is non-empty then it follows from the i.h. and the fact that transitions preserve the invariant, as an immediate inspection shows.

Lemma 5.2 (Micro-Substitution Terminates). var terminates in at most |E| steps (on reachable states).

Proof. Consider a var transition copying u from the environment E :: [x u] :: E . If the next transition is again var , then the head of u is a variable y and the transition copies from an entry in E because by Lemma 5.1 y cannot be bound by the entries in E . Then the number of consecutive var transitions is bound by E (that is not extended by var ).

Theorem 5.3. The Micro AM implements the weak head strategy.

Environments E := ε | [x t] :: E Stacks π := ε | t :: π Compilation t • := (t, ε, ε) Decoding (t, ε, ε) := t (t, u :: π, E) := (tu, π, E) (t, ε, [x u] :: E) := (t{x

Search + Micro-Substitution = Milner Abstract Machine

The Searching AM and the Micro AM can be merged together into the Milner Abstract Machine (MAM), defined in Fig. 3. The MAM has both an argument stack and an environment. The machine has one βtransition rβ inherited from the Searching AM, and two overhead transitions, @l inherited from the the Searching AM and var inherited from the Micro AM. Note that in var the code now is simply a variable, because the arguments are supposed to be stored in the argument stack.

For the implementation theorem once again the only delicate point is to prove that the overhead transitions terminate. As for the Micro AM one needs a name invariant. A termination measure can then be defined easily by mixing the size of the codes (needed for @l ) and the size of the environment (needed for var ), and it is omitted here, because it will be exhaustively studied for the complexity analysis of the MAM. Therefore, we obtain that: Theorem 6.1. The MAM implements the weak head strategy.

Introducing Complexity Analyses

The complexity analysis of abstract machines is the study of the asymptotic behavior of their overhead. Note that our notion of implementation allows to forget about the strategy while studying the complexity of the machine, because the two fundamental parameters are internalized: the input is simply the initial code and the length of the strategy is simply the number of β -transitions.

The relevance of the subterm invariant goes in fact well beyond abstract machines, as it is typical of most instances of micro-step operational semantics. And for complexity analyses of the λ -calculus it is absolutely essential, playing a role analogous to that of the cut-elimination theorem in the study of sequent calculi or of the sub-formula property for proof search.

Number of Transitions.

The next lemma bounds the global number of overhead transitions. For the micro-substituting transition var it relies on an auxiliary bound of a more local form. For the searching transition @l the bound relies on the subterm invariant. We denote with |ρ| β , |ρ| @l , and |ρ| var the number of rβ , @l , and var transitions in ρ, respectively.

@l ≤ |t 0 | • (|ρ| var + 1) ≤ |t 0 | • (|ρ| 2 β + 1).
Proof.

1. Reasoning along the lines of Lemma 5.2 one obtains that var transitions in σ have to use entries of E from left to right ( @l and var do not modify E), and so |σ | var ≤ |E|. Now, |E| is exactly |ρ| β , because the only transition extending E, and of exactly one entry, is rβ .

2. The fact that a linear local bound induces a quadratic global bound is a standard reasoning. We spell it out to help the unacquainted reader. The execution ρ alternates phases of β -transitions and phases of overhead transitions, i.e. it has the shape:

t • 0 = s 1 * rβ s 1 * @l,var s 2 * rβ s 2 * @l,var . . . s k * rβ s k * @l,var s
Let a i be the length of the segment s i * rβ s i and b i be the number of var transitions in the segment s i * @l,var s i+1 , for i = 1, . . . , k. By Point 1, we obtain b i ≤ ∑ i j=1 a j . Then

|ρ| var = ∑ k i=1 b i ≤ ∑ k i=1 ∑ i j=1 a j . Note that ∑ i j=1 a j ≤ ∑ k j=1 a j = |ρ| β and k ≤ |ρ| β . So |ρ| var ≤ ∑ k i=1 ∑ i j=1 a j ≤ ∑ k i=1 |ρ| β ≤ |ρ| 2 β . 3.
The length of σ is bound by the size of the code in the state s because rβ ,@l strictly decreases the size of the code, that in turn is bound by the size |t 0 | of the initial term by the subterm invariant (Lemma 8.1).

4. The execution ρ alternates phases of rβ and @l transitions and phases of var transitions, i.e. it has the shape:

t • 0 = s 1 * rβ ,@l s 1 * var s 2 * rβ ,@l s 2 * var . . . s k * rβ ,@l s k * var * rβ ,@l s
By Point 3 the length of the segments s i * rβ ,@l s i is bound by the size |t 0 | of the initial term. The code may grow, instead, with var transitions. So |ρ| @l is bound by |t 0 | times the number |ρ| var of micro-substitution transitions, plus |t 0 | once more, because at the beginning there might be rβ ,@l transitions before any var transition-in symbols, |ρ| @l ≤ |t 0 | • (|ρ| var + 1). Finally,

|t 0 | • (|ρ| var + 1) ≤ |t 0 | • (|ρ| 2 β + 1) by Point 2.
Cost of Single Transitions. To estimate the cost of concretely implementing single transitions we need to make some hypotheses on how the MAM is going to be itself implemented on RAM:

1. Codes, Variable (Occurrences), and Environment Entries: abstractions and applications are constructors with pointers to subterms, a variable is a memory location, a variable occurrence is a reference to that location, and an environment entry [x t] is the fact that the location associated to x contains (the topmost constructor of) t.

2. Random Access to Global Environments: the environment E of the MAM can be accessed in constant time (in var ) by just following the reference given by the variable occurrence under evaluation, with no need to access E sequentially, thus ignoring its list structure.

It is now possible to bound the cost of single transitions. Note that the case of var transitions relies on the subterm invariant. Proof. According to our hypothesis on the concrete implementation of the MAM, @l just moves the pointer to the current code on the left subterm of the application and pushes the pointer to the right subterm on the stack-evidently constant time. Similarly for rβ . For var , the environment entry [x t] is accessed in constant time by hypothesis, but t has to be α-renamed, i.e. copied. It is not hard to see that this can be done in time linear in |t| (the naive algorithm for copying carries around a list of variables, and it is quadratic, but it can be easily improved to be linear) that by the subterm invariant (Lemma 8.1) is bound by the size |t 0 | of the initial term.

Complexity of the Overhead. By composing the analysis of the number of transitions (Lemma 8.2) with the analysis of the cost of single transitions (Lemma 8.3) we obtain the main result of the paper. The Efficient MAM. According to the terminology of Sect. 3, the MAM is reasonable but it is not efficient because micro-substitution takes time quadratic in the length of the strategy. The quadratic factor comes from the fact that in the environment there can be growing chains of renamings, i.e. of substitutions of variables for variables, see [START_REF] Accattoli | On the Value of Variables[END_REF] for more details on this issue. The MAM can actually be optimized easily, obtaining an efficient implementation, by replacing rβ with the following two β -transitions:

λ x.t y :: π E rβ 1 t{x y} π E λ x.t u :: π E rβ 2 t π [x u] :: E if u is not a variable
Search is Linear and the Micro AM is Reasonable. By Lemma 8.2 the cost of search in the MAM is linear in the number of transitions for implementing micro-substitution. This is an instance of a more general fact: search turns out to always be bilinear (in the initial code and in the amount of microsubstitutions). There are two consequences of this general fact. First, it can be turned into a design principle for abstract machines-search has to be bilinear, otherwise there is something wrong in the design of the machine. Second, search is somewhat negligible for complexity analyses.

The Micro AM can be seen as the MAM up to search. In particular, it satisfies a subterm invariant and thus circumvents size-explosion. The Micro AM is however quite less efficient, because at each step it has to search the redex from scratch. An easy but omitted analisys shows that its overhead is nonetheless polynomial. Therefore, it makes sense to consider very abstract machines as the Micro AM that omit search. In fact, they already exist, in disguise, as strategies in the linear substitution calculus [START_REF] Accattoli | An Abstract Factorization Theorem for Explicit Substitutions[END_REF][START_REF] Accattoli | A nonstandard standardization theorem[END_REF], a recent approach to explicit substitutions modeling exactly micro-substitution without search (the traditional approach to explicit substitutions instead models both micro-substitution and search) and they were used for the first proof that a strong strategy (the leftmost-outermost one) is reasonable [START_REF] Accattoli | Beta reduction is invariant, indeed[END_REF].

The Searching AM is Unreasonable. It is not hard to see that the Searching AM is unreasonable. Actually, the number of transitions is reasonable. The projection of MAM executions on Searching AM executions, indeed, shows that the number of searching transitions of the Searching AM is reasonable. It is the cost of single transitions that becomes unreasonable. In fact, the Searching AM does not have a subterm invariant, because it rests on meta-level substitution, and the size of the terms duplicated by the rβ transition can explode (it is enough to consider the size-exploding family of Proposition 1.2).

The moral is that micro-substitution is more fundamental than search. While the cost of search can be expressed in terms of the cost of micro-substitution, the converse is in fact not possible. 9 Names: Krivine Abstract Machine Accounting for Names. In the study presented so far we repeatedly took names seriously, by distinguishing between terms and codes, by asking that initial codes are well-named, and by proving an invariant about names (Lemma 5.1). The process of α-renaming however has not been made explicit, the machines we presented rather rely on a meta-level renaming, used as a black box.

The majority of the literature on abstract machines, instead, pays more attention to α-equivalence, or rather to how to avoid it. We distinguish two levels:

1. Removal of on-the-fly α-equivalence: in these cases the machine works on terms with variable names but it is designed in order to implement evaluation without ever α-renaming. Technically, the global environment of the MAM is replaced by many local environments, each one for every piece of code in the machine. The machine becomes more complex, in particular the non-trivial concept of closure (to be introduced shortly) is necessary.

2. Removal of names: terms are represented using de Bruijn indexes (or de Bruijn levels), removing the problem of α-equivalence altogether but sacrificing the readability of the machine and reducing its abstract character. Usually this level is built on top of the previous one. We are now going to introduce Krivine Abstract Machine (keeping names, so at the first level), yet another implementation of the weak head strategy. Essentially, it is a version of the MAM without onthe-fly α-equivalence. The complexity analysis will show that it has exactly the same complexity of the MAM. The further removal of names is only (anti)cosmetic-the complexity is not affected either. Consequently, the task of accounting for names is-as for search-negligible for complexity analyses. Krivine Abstract Machine. The machine is in Fig. 4. It relies on the mutually inductively defined concepts of local environment, that is a list of closures, and closure, that is a list of pairs of a code and a local environment. A state is a pair of a closure and a stack, but in the description of the transitions we write it as a triple, by spelling out the two components of the closure. Let us explain the name closure: usually, machines are executed on closed terms, and then a closure decodes indeed to a closed term.

While essential in the study of call-by-value or call-by-need strategies, for the weak head (call-by-name) strategy the closed hypothesis is unnecessary, that is why we do not deal with it-so a closure here does not necessarily decode to a closed term. Two remarks:

1. Garbage Collection: transition var , beyond implementing micro-substitution, also accounts for some garbage collection, as it throws away the local environment e associated to the replaced variable x. The MAM simply ignores garbage collection. For time analyses garbage collection can indeed be safely ignored, while it is clearly essential for space (both the KAM and the MAM are however desperately inefficient with respect to space).

2. No α-Renaming and the Length of Local Environments: names are never renamed. The initial code, as usual, is assumed to be well-named. Then the entries of a same local environment are all on distinguished names (formally, a name invariant holds). Then the length of a local environment e is bound by the number of names in the initial term, that is, by the size of the initial term (formally, |e| ≤ |t 0 |). This essential quantitative invariant is used in analisys of the next paragraph.

Implementation and Complexity Analysis. The proof that the KAM implements the weak head strategy follows the recipe for these proofs and it is omitted. For the complexity analysis, the bound of the number of transitions can be shown to be exactly as for the MAM. A direct proof is not so simple, because the bound on var transitions cannot exploit the size of the global environment. The bound can be obtained by relating the KAM with the Searching AM (for which the exact same bound of the MAM holds), or by considering the depth (i.e. maximum nesting) of local environments. The proof is omitted. The interesting part of the analysis is rather the study of the cost of single transitions. As for the MAM, we need to spell out the hypotheses on how the KAM is concretely implemented on RAM. Variables cannot be implemented with pointers, because the same variable name can be associated to different codes in different local environments. So they have to simply be numbers. Then there are two choices for the representation of environments, either they are represented as lists or as arrays. In both cases rβ can be implemented in constant time. For the other transitions:

1. Environments as Arrays: we mentioned that there is a bound on the length of local environments (|e| ≤ |t 0 |) so that arrays can be used. The choice allows to implement var in constant time, because e can be accessed directly at the position described by the number given by x. Transition @l however requires to duplicate e, and this is necessary because the two copies might later on be modified differently. So the cost of a @l transition becomes linear in |t 0 | and @l transitions all together cost O(|t 0 | 2 • (|ρ| 2 β + 1)), that also becomes the complexity of the whole overhead of the KAM. This is worse than the MAM.

2. Environments as Lists: implementing local environments as lists provides sharing of environments, overcoming the problems of arrays. With lists, transition @l becomes constant time, as for the MAM, because the copy of e now is simply the copy of a pointer. The trick is that the two copies of the environment can only be extended differently on the head, so that the tail of the list can be shared. Transition var however now needs to access e sequentially, and so it costs |t 0 | as for the MAM. Thus globally we obtain the same overhead of the MAM. Summing up, names can be pushed at the meta-level (as in the MAM) without affecting the complexity of the overhead. Thus, names are even less relevant than search at the level of complexity. The moral of this tutorial then is that substitution is the crucial aspect for the complexity of abstract machines.

Proposition 1 . 1 (

 11 Open and Rightmost-Innermost Size-Explosion). Let n ∈ N. Then t n → n β u n , moreover |t n | = O(n), |u n | = Ω(2 n ),and u n is neutral.

r 1 :

 1 = λ x.λ y.(yxx) p 0 := I r n+1 := λ x.(r n (λ y.(yxx))) p n+1 := λ y.(yp n p n )

Proposition 1 . 2 (

 12 Closed and Strategy-Independent Size-Explosion). Let n>0. Then r n p m → n β p n+m , and in particular r n I → n β p n . Moreover,|r n I| = O(n), |p n | = Ω(2 n ),r n I is closed, and p n is normal. Proof. By induction on n. The base case: r 1 p m = λ x.λ y.(yxx)p m → β (λ y.(yp m p m )) = p m+1 . The inductive case: r n+1 p m = λ x.(r n (λ y.(yxx)))p m → β r n (λ y.(yp m p m )) = r n p m+1 → n β p n+m+1 , where the second sequence is obtained by the i.h. The rest of the statement is immediate.

3 .

 3 Cost: these micro-step operations have constant cost; 4. Result: micro-evaluation stops on a shared representation of the result.

Figure 1 :

 1 Figure 1: Searching Abstract Machine (Searching AM).

Lemma 4 . 1 (

 41 Transitions Decoding). Let s be a Searching AM state. 1. β -Transition: if s rβ s then s → β s .

Lemma 4 . 2 (

 42 Bricks for Step Simulation).

Figure 2 :

 2 Figure 2: Micro-Substituting Abstract Machine (Micro AM).

Lemma 4 . 3 (

 43 One-Step Simulation). Let s be a Searching AM state. If s → wh u then there exists a state s such that s * @l rβ s and s = u.

Theorem 4 . 4 .

 44 The Searching AM implements the weak head strategy.Proof. Executions to Derivations: by induction on the length |ρ| of ρ using Lemma 4.1. Derivations to Executions: by induction on the length |d| of d using Lemma 4.3 and noting that t • = t.

Figure 3 :

 3 Figure 3: Milner Abstract Machine (MAM).

1 . 2 .

 12 Parameters for Complexity Analyses. Let us reason abstractly, by considering a generic strategy → in the λ -calculus and a given machine M implementing →. By the derivations-to-executions part of the implementation (Definition 3.1), given a derivation d : t 0 → n u there is a shortest execution ρ : t • 0 M s such that s = u. Determining the complexity of M amounts to bound the complexity of a concrete implementation of ρ, say on a RAM model, as a function of two fundamental parameters: Input: the size |t 0 | of the initial term t 0 of the derivation d; Strategy the length n = |d| of the derivation d, that coincides with the number |ρ| β of β -transitions in ρ by the β -matching requirement for implementations.

Lemma 8 . 3 .

 83 Let ρ : t • 0 MAM s be a MAM execution. Then: 1. Each @l transition in ρ has constant cost; 2. Each rβ transition in ρ has constant cost; 3. Each var transition in ρ has cost bounded by the size |t 0 | of the initial term.

Theorem 8 . 4 (

 84 The MAM is Reasonable). Let ρ : t • 0 MAM s be a MAM execution. Then: 1. @l transitions in ρ cost all together O(|t 0 | • (|ρ| 2 β + 1)); 2. rβ transitions in ρ cost all together O(|ρ| β ); 3. var transitions in ρ cost all together O(|t 0 | • (|ρ| 2 β + 1)); Then ρ can be implemented on RAM with cost O(|t 0 | • (|ρ| 2β + 1)), i.e. the MAM is a reasonable implementation of the weak head strategy.

Figure 4 :

 4 Figure 4: Krivine Abstract Machine (KAM).

  E where t α denotes t where bound names have been freshly renamed.

			Decoding		(t, ε) := t
	ε)			(t, [x u] :: E) := (t{x u}, E)
	Code	Env	Trans	Code	Env
	(λ x.t)ur 1 . . . r k	E	dβ	tr 1 . . . r k	[x u] :: E
	xr 1 . . . r k

E :: [x t] :: E var t α r 1 . . . r k E :: [x t] ::

  u}, ε, E) E where t α denotes t where bound names have been freshly renamed.

	Code Stack	Env	Trans Code Stack	Env
	tu	π	E	@l	t	u :: π	E
	λ x.t u :: π	E	rβ	t	π	[x u] :: E
	x	π	E :: [x t] :: E	var	t α	π	E :: [x t] ::

  Lemma 8.2. Let ρ : t • 0 MAM s be a MAM execution. Then: 1. Micro-Substitution Linear Local Bound: if σ : s * @l,var s then |σ | var ≤ |E| = |ρ| β ; 2. Micro-Substitution Quadratic Global Bound: |ρ| var ≤ |ρ| 2 β ; 3. Searching (and β ) Local Bound: if σ : s * rβ ,@l s then |σ | ≤ |t 0 |; 4. Searching Global Bound: |ρ|

The Complexity of Abstract Machines Types of Machines. The bound on the overhead of the machine is then used to classify it, as follows.

Definition 7.1. Let M an abstract machine implementing a strategy →. Then

• M is reasonable if the complexity of M is polynomial in the input |t 0 | and the strategy |ρ| β ;

• M is unreasonable if it is not reasonable;

• M is efficient if it is linear in both the input and the strategy (we sometimes say that it is bilinear).

Recipe for Complexity Analyses. The estimation of the complexity of a machine usually takes 3 steps: Here it is usually necessary to go beyond the abstract level, making some (high-level) assumption on how codes and data-structure are concretely represented (our case study will provide examples).

3. Complexity of the Overhead: obtain the total bound by composing the first two points, that is, by taking the number of each kind of transition times the cost of implementing it, and summing over all kinds of transitions.

The Complexity of the MAM

In this section we provide the complexity analysis of the MAM, from which analyses of the Searching and Micro AM easily follow.

The Crucial Subterm Invariant. The analysis is based on the following subterm invariant.

Lemma 8.1 (Subterm Invariant). Let ρ : t • 0 MAM (u, π, E) be a MAM execution. Then u and any code in π and E are subterms of t 0 .

Note that the MAM copies code only in transition var , where it copies a code from the environment E. Therefore, the subterm invariant bounds the size of the subterms duplicated along the execution.

Let us be precise about subterms: for us, u is a subterm of t 0 if it does so up to variable names, both free and bound (and so the distinction between terms and codes is irrelevant). More precisely: define t -as t in which all variables (including those appearing in binders) are replaced by a fixed symbol * . Then, we will consider u to be a subterm of t whenever u -is a subterm of t -in the usual sense. The key property ensured by this definition is that the size |u| of u is bounded by |t|.

Proof. By induction on the length of ρ. The base case is immediate and the inductive one follows from the i.h. and the immediate fact that the transitions preserve the invariant.

The subterm invariant is crucial, for two related reasons. First, it linearly relates the cost of duplications to the size of the input, enabling complexity analyses. With respect to the length of the strategy, then, micro-step operations have constant cost, as required by the recipe for micro-step operational semantics in Sect. 2. Second, it implies that size-explosion has been circumvented: duplications are linear, and so the size of the state can grow at most linearly with the number of steps, i.e. it cannot explode. In particular, we also obtain the compact representation of the results required by the recipe.


Keywords:

We developed a rapid and green synthesis of various isocyanurates by cyclotrimerization of isocyanates using TDAE (tetrakis(dimethylamino)ethylene). TDAE displays excellent performance in catalytic quantities, affording the corresponding trimer of isocyanates very rapidly, under air and at room temperature with good to excellent yields.

Tetrahedron Letters

--- * Corresponding author. Tel.: +0-000-000-0000; fax: +0-000-000-0000; e-mail: author@university.edu 1,3,5-Triazinane-2,4,6-triones or isocyanurates, with their high thermal stability, are used to enhance the physical properties of polyurethanes and coating materials. 1 Incorporation of isocyanurates into the framework of polyurethanes increases thermal and chemical resistance, flame retardation, as well as film-forming characteristics. [START_REF] Nicholas | [END_REF] Isocyanurates are also employed in other areas such as chiral discrimination, 3 selective ion bonding 4 and drug delivery. 5 Triaryl isocyanurates are often used as activators for the polymerization and postpolymerization of εcaprolactam in the production of nylons with high melt viscosities. 6 The general route for the preparation of isocyanurates is the cyclotrimerization of the corresponding isocyanates. A number of reports have been published concerning this method using a variety of different Lewis-basic catalysts, including phosphines, 7 amines, 8 NO, 9 alkoxyallenes, 10 fluoride anions, 11 ptoluenesulfinates, 12 carbamate anions, 13 cyanates, 14 and Nheterocyclic carbenes. 15 Organometallic catalysts such as lithium amides, 16 alkylzinc amines and alkoxides, 17 tin complexes, 18 palladium(0), 19 copper(II) and nickel(II) halides 9 also allowed the cyclotrimerization of isocyanates. But, many of the known cyclotrimerization procedures suffer from low catalyst activity, diazetidine byproduct formation, lengthy reaction times, product separation difficulties and the use of toxic solvents. 15,20 Therefore, developing catalysts which promote cyclotrimerization selectively is of great importance due to wide application of isocyanurate structure in both industry and academic studies. [1][START_REF] Nicholas | [END_REF][START_REF] Sugimoto | [END_REF][4][5][6] Tetrakis(dimethylamino)ethylene 21 (Figure 1) is an electronrich organic reductant, which reacts with halogenated derivatives to generate an anion under mild conditions via two sequential single electron transfers.

Figure 1. Structure of TDAE

During our investigation of 9-bromofluorene addition to phenyl isocyanate in the presence of TDAE, we discovered that TDAE allowed the cyclotrimerization of isocyanates to their respective isocyanurates. Herein, we report further details about this efficient and straightforward isocyanurates synthesis using commercially available TDAE.

Phenyl isocyanate 1a was used as model substrate for the optimization of the cyclotrimerization conditions and the results are summarized in Table 1. We first carried out a reaction using an equimolar amount of TDAE and phenyl isocyanate in anhydrous THF at room temperature. The conversion, monitored by TLC, was complete after 15 min. A complex mixture was obtained and triphenylisocyanurate 2a was isolated in only 25% yield (Entry 1). Using 40 mol% of TDAE resulted in a small decrease of the by-products proportions and allowed 2a in 35% yield (Entry 2). With 15 mol% of TDAE, a dramatic improvement was observed and 2a was isolated in 69% yield (Entry 3). A variety of solvents were screened (Entries 4-7) and ethyl acetate gave the best result (71% yield, Entry 7).

A R T I C L E I N F O A B S T R A C T Table 1. Optimization of the cyclotrimerization of phenyl isocyanate initiated by TDAE

a Isolated yields. b Reactions were performed under nitrogen at room temperature using 2 mL of anhydrous non-degassed solvent. c Reactions were performed under air at room temperature. d Reaction was performed with 0.5 mL of ethyl acetate.

Then, we explored the possibility to run the reaction without solvent under air with 15 mol% of TDAE. After 10 seconds, the mixture became completely solid, so the reaction was stopped. Interestingly, the trimer 2a was isolated with a yield similar to those obtained with ethyl acetate as solvent (Entry 8 vs 9). This encouraging finding prompted us to investigate the influence of TDAE amount in solvent-free conditions under air. Decreasing the amount of TDAE from 15 mol% to 5 mol% resulted in a slightly improvement (80% yield, Entry 10). No significant effect was between 5 mol% and 2 mol% of TDAE (Entry 10 vs 11). Using a small amount of ethyl acetate as solvent resulted in a slightly lower yield of trimer 2a (Entry 12). A control experiment without catalyst (Entry 13) showed the importance of TDAE to achieve good yields.

So, the method developed here is very simple, fast and environmentally-friendly as it allowed the formation of the trimer under air at room temperature in only 10 seconds without solvent. Furthermore, separation of the desired product was achieved by simply triturating and filtering the crushed reaction mixture with cold diethyl ether and water, successively.

With the optimized conditions in hand, we proceeded to investigate the substrate scope of the reaction. The results are shown in Table 2. Under the optimized solvent-free reaction conditions, a variety of liquid isocyanates were converted to the corresponding isocyanurates in very good yields (Entry 1-7). Both electron-donating and electron-withdrawing substituents on the aryl group are well tolerated. Interestingly, a benzyl substituent gave also a very good 93% yield of the corresponding isocyanurate 2g (Entry 7).

The reactivity of solid isocyanates was then studied with the optimized conditions. But, our preliminary attempt with nitrophenyl isocyanate, previously powdered in a mortar with a pestle, and 2 mol% of TDAE at room temperature, did not allow the formation of the corresponding isocyanurate 2h. So, we further investigated the use of a minimum amount of solvent. When 2 mol% of TDAE was added to a solution of nitrophenyl isocyanate in 0.5 mL of ethyl acetate under air, the corresponding trimer 2h was isolated in 81% yield (Entry 8). With these new conditions for solid isocyanates in hand, the scope of the cyclotrimerization using a variety of solid isocyanates was explored and gave good to excellent yields of the corresponding isocyanurates 2i-k (Entry 9-11). Based on the ability of TDAE to give electrons and on a recent paper showing that the trimerization of isocyanates can be initiated by an electron, 22 we propose a similar mechanism involving an anion radical intermediate formed by donation of an electron of TDAE to the isocyanate.

In conclusion, commercially available TDAE has been used for the first time to catalyze the cyclotrimerization of a wide range of aryl isocyanates and benzyl isocyanate to isocyanurates in high yield. The important features of our method are: solventfree conditions with liquid isocyanates, mild reaction conditions under air, very short time reaction and simple purification procedure.

  j o u r n a l h o m e p a g e : w w w . e l s e v i e r . c o m An expeditious method for the selective cyclotrimerization of isocyanates initiated by TDAE Alain G. Giuglio-Tonolo, Cédric Spitz, Thierry Terme, Patrice Vanelle * Aix-Marseille Université, Institut de Chimie Radicalaire (ICR)-UMR CNRS 7273-Equipe de Pharmacochimie Radicalaire (LPCR), Faculté de Pharmacie, 27 Bd Jean Moulin, 13385 Marseille-CS30064-cedex 05, France.

a

  Isolated yields. b Reactions were performed under air at room temperature. c 0.5 mL of EtOAc was used and the reaction was stirred for 15 min.

Table 2 .

 2 Scope of the cyclotrimerization of various isocyanates.

Acknowledgments

This work was supported by the Centre National de la Recherche Scientifique and the Aix-Marseille Université. The authors thank V. Remusat for 1 H and 13 C spectra recording and T. Schembri for mass spectra recording.