Glodt Julie Workshop Implications of time 1

A surprising multiplicity of objects could flow into a church, differently associated or contextualized on the basis of a real semantic 'code' that was dictated by the liturgy, or rather by liturgical time. 1 An essential rhythm was embodied in the liturgical colors, that of the copes worn by the celebrant and his acolytes, but also, in unison, those of the cloths that cover the altar and adorn the church. Removing (mutare) and alternating (alternare) the vestments and the liturgical colors were the operations that supported this chromatic rhythm. 2 These quotations convey two different conceptions of the relationships between liturgical objects and time. In the first one, Paolo Piva asserts that the use of objects was "dictated" by liturgical time. There would therefore have a direct and explicit causal link between the two. In the second one, Jean-Claude Schmitt argues that what was meaningful in the medieval church did not rely on a semantic lecture, but on movements and rhythms. Whereas in the first quotation, objects are supposed to act like "signs" identifying liturgical time according to a "semantic code", in the second one, they are analyzed ornamentally. In brief, a cognitive reading is opposed to a sensory perception of objects.

Liturgical time, that remained the basic reference for the entire Christian society, relied on complex calculations (the computus), as well as on verbal discourses 3 . It combined solar cycles (the liturgical year), weekly cycles (Sundays and feriae) and connections between solar, lunar and weekly cycles (Easter and other movable feasts) 4 . This complex cyclicity produced both anachronism and repetition in order to commemorate events related to the life of Christ or saints. But time was not only a theoretical and learned question for scholars. As social construction and far from being just a scientifically measurable reality, time in the Middle Ages required sensorial or physical indicators. For example, Giles Constable has shown that the past 1 Paolo Piva, "Lo 'spazio liturgico': architettura, arredo, iconografia (secoli iv-xii)," in L'arte medievale nel contesto 300-1300 Funzioni, iconografia, tecniche, ed. Paolo Piva (Milan: Jaca Books, 2006), 141-180, 141: "In una chiesa poteva confluire una molteplicità sorprendente di oggetti, diversamente associati o contestualizzati sulla base du un vero e proprio 'codice' semantico che era dettato dalla liturgia, o meglio dal tempo liturgico."

2 Jean-Claude Schmitt, Les rythmes au Moyen Âge (Paris: Gallimard, 2016), 304: "Un rythme essentiel s'incarne dans les couleurs liturgiques, celle des chapes portées par le célébrant et ses acolytes, mais aussi, à l'unisson, celles des linges qui recouvrent l'autel et ornent l'église. Changer (mutare) et alterner (alternare) les habits et les couleurs liturgiques sont les opérations qui soutiennent ce rythme chromatique." 3

could have been "lived" through sensory experiences, by the means of figures, spolia or disjunctions 5 .

In this paper, I will focus on the way the clergy shaped liturgical time by displaying textiles around the main altar, which was the sacral epicenter of the church where the 'super sacrament' of the Eucharist took place6 . For feasibility reasons, I will focus on frontals and dossals. As flexible and movable materials, textiles were displayed around the altar so as to follow the circulus anni: for example, dossals and frontals were moved before feasts 7 . In this way, they constitute a perfect laboratory to examine the way objects could mark liturgical time.

In the first section, I will examine the first hypothesis given by Paolo Piva: textiles would function as codified devices, so that they would have formally been meant to identify the feast of the day in a semantic way. In the second part, I will try to demonstrate that liturgical time were in fact more expressed than signified by textiles surrounding the altar.

I.

A semantic system identifying liturgical time? Since the Fashion System of Roland Barthes, the sociological history generated a rich semantic analysis of garments8 . As Gil Bartholeyns explained: the garment "become an expressive sign, it transformed into a fact of communication"9 . While a global anthropological analysis of textiles has developed, the semantic analysis is still current in the (relatively young) research field of medieval textiles, as Kate Dimitrova and Margaret Goehring put it in the introduction of Dressing the Part: Textiles as Propaganda in the Middle Ages:

While much of textile studies continues to focus on necessary foundational questions concerning dating, workshop processes, stylistic development, vocabulary, and other technical details, the scholarship offered in this volume also questions how medieval textiles were used and invoked in the construction and display of power by addressing their semiotic functions10 .

The form of liturgical textiles, their shape, their color and their iconography are frequently analyzed as quasi-taxonomic or semantic elements 11 . Concerning liturgical time, colors are mostly analyzed as a key semantic element identifying them.

I-A. Colors as signs ?

In the as heraldic, colors would be organized according to a determined grammar: liturgical colors are supposed to follow the "ordo colorum." On this basis, the next step crossed by some art historians was to analyze colors as semantic signs, all the more efficient that they are seen as "abstract categories". Rudolph Suntrup for examples compares these colors with sign language ("Zeichensprache") as non-verbal form of the dialogical structure created by the ritual between God and mankind [START_REF] Suntrup | Liturgische farbenbedeutung im Mittelalter und die der frühen Neuzeit[END_REF] .

Nevertheless, this hypothesis does not stand up to analysis of late-medieval sources. First, what is written in expositiones missae did not perfectly reflect the medieval ritual. Most of these commentaries on the mass were based on a learned "figural though", according objects, places or celebrants were figures of another reality (most of time, a biblical reality). According the symbolic of numbers, the four colors had probably been chosen to refer to the four colors of the High Priest's garments described in Exodus, as Lothar of Segni put it very explicitly: "Quatuor autem sunt principales colores, quibus secundum proprietates dierum sacras vestes Ecclesia Romana distinguit, albus, rubeus, niger et viridis. Nam et in legalibus indumentis quatuor colores fuisse leguntur: byssus et purpura, hyacinthus et coccus" [START_REF] Of | [END_REF] . That is probably why violet, which is sometimes considered as a full-blown color in other liturgical texts [START_REF] Malabranca | Liber quando episcopus cardinalis missarum sollemnia celebraturus est[END_REF] , could not find its place within the quadrichromy of expositiones missae.

Moreover, colors were not abstract categories but they depended on their supports. Based on some texts of the 8 th century, Renate Kroos included curtains or frontals in her wide calendar of medieval liturgical colors 20 . Nevertheless, we must reassert that the ordo colorum concerned above all garments: curtains or carpets or even frontals were less implicated than other textiles by these distinctions 21 . The sacristan handbook of the cathedral of Mende endorsed several times a distinction between the colors of the clothes and that of the frontals. For the feast of Blaise, for example, the office was sung in red and the mass in purple, but the altar must be adorned with green if the feast fell during Septuagesima 22 .

Inventories of treasures also reveal a wide diversity of colors that cannot be integrated within the "quadrichromy", like blue, silver, braun, orange, grey… Such colors were also declined in several shades. In 1419, within the "ornamenta rubea" of the Amiens cathedral, we find some expressions ("violatum", "rubeo sive sanguineo", "rubeum obscurum", "rubea trahentia magis ad colorem croceum" 23 ) showing that the writer endeavored to describe the shades as precisely as possible. These numerous shades cannot be subsumed within larger and abstract categories. In the Mende cathedral again, the Christmas vigil must be sung in white common copes ("capis albis communes"), whereas for the matins of this solemnity, clerics wore whiter copes ("cape albiores") 24 . Nuances were thus used in an expressive way: the purest white meant the complete fulfillment of the feast. Here we see that we can't analyze the colors of liturgical textiles in a heraldic way: there were not pure abstraction functioning as sign.

I-B. Images and inscriptions: simultaneity factors

Sometimes, a frontal or a dossal could have been adorned with an image directly related to the feast of the day 25 : an angel saluting the Virgin for the Annunciation 26 , Christ rising from the grave for Easter 27 . The ordinary of the Speyer cathedral, written in German in the 15 th century, provides some obvious examples: for Easter, the main altar should be adorned with a white weft-faced compound twill ("samit") "mit bilden do Ressurectio" 28 . On Epiphany, the frontal bore the image of the three kings visiting the Child 29 . A red altarpiece with a cross was -First, we might think that the liturgical action would "dictate" (as Paolo Piva puts it) the aspect of textiles: this way, images or inscriptions would have only illustrated or commented the action.

-Second, we might wonder if adornment would not impulse the liturgical action in a performative way: for examples, inscriptions, by being read, would then fulfill a "liturgical function" as Robert Favreau put it in a pioneer paper on epigraphy and liturgy 34 .

But these two hypothesese seem too functionalist to be validated 35 . Moreover, the conjunction between iconography and time was rare. That is why we must find another interpretative model to analysis the relationship between images or inscriptions and time. More recently, Vincent Debiais analyzed inscriptions visible in church according to an "iconographic function" 36 . According to him, the letters displayed around the altar did not imply anything within the ritual, but it created an "amplified lecture" of the images or objects within the liturgical context. In the same way, we can also suppose that images or inscriptions bore by textiles would generate an "amplified lecture" of the feast of the day.

Let's consider an example taken outside the main altar's area. Concerning choir tapestries, Laura Weigert shows that in the late Middle Ages, donors made a point of controlling the time when the tapestry should be hung. In 1518, Jean Ruffault gave a choir tapestry depicting the life of Stephen to the collegiate church of Saint-Stephen in Lille. According to the deed of donation, the chapter had to display the tapestry on specified feast days: the Invention of his relics, the Assumption, the Dedication of the church, All Saints' Day, Christmas, Easter, Pentecost and Corpus Christi. If Laura Weigert speaks in terms of "liturgical signification"37 , it evidently did not depend on a restricted and functionalist conjunction between iconography and liturgical time (only the feast of the Stephen's relics and the Dedication could be somehow related to the images of the choir tapestry). Here, the point was in fact to establish a connection between the hung tapestries, the memory of the donor and the liturgical time. The more the time of hanging was restricted, the more this connection intensified.

It was probably the same with frontals or dossals. The images or the inscriptions were not aimed at elucidating or illustrating the events commemorated within the ritual. But, through simultaneity and time restriction, they could specify and particularize some of the highest feasts of the year. There was not a causal relationship between adornments and time, but a symbiotic one: images or inscriptions gave a visible form to the commemorated events. In return, they were "activated", endorsed with additional meanings by the liturgical context.

II. Expressing time in an ornamental way

For the late Middle Ages, the semantic hypothesis cannot be upheld. Whereas it is clear that some textiles were chosen for their color or iconography, the search for a strict conjunction between the aspect of the textile and time was in fact very rare. Simply put, even if there were some codes given by liturgical comments or ordinaries, it was not a coherent system transforming textiles into signage, that one could decipher according to their aspect. The textiles' contribution to the marking of liturgical time relied mostly on expressivity.

II-A. Textiles as temporal bridges

The liturgical sources provide several examples of discrepancies between the form of textiles and liturgical time. This cannot be clearer than in the sacristan handbook of Saint-Simon same notes for the Purification and the Assumption 47 . In 1230 in the cathedral of Florence, altars were adorned with "paschalibus ornamentis" since Holy Saturday, but also for Christmas [START_REF] Moreni | predicta die preparetur Altare S. Marci vestimentis Paschalibus, et mirtis et lauro et lampadibus circa ipsum[END_REF] . These textiles were also displayed around the secondary altar of Marc on the local feast of Crescentius of Florence, because his relics were preserved under this altar 49 . A similar principle was used at the end of our period, in the Holy-Chapel of Dijon, where the same ensemble of red textiles given by Philip III the Good were used for Christmas and for the feast of John the Evangelist, who was the patron saint of the church.

In the last two examples, by being used cyclically, the textiles displayed around the altar built bridges between the great solemnities of the year (Easter and Christmas for example) and certain local feasts (the Dedication, the feast of the patron saint for example). Thus, the shifting of textiles could redefine to a certain extend the highlights of the liturgical year at the local level. With a flexibility that the computus or ceremonials did not allow, textiles offer the possibility of establishing relationships between local festivals and universal solemnities insofar as they were not established explicitly (such image referring to a commemorated event), but in an ornamental way (the same object being used for two similar feasts). In the end, these relationships did not require a cognitive approach but were based on memory and diachrony.

II-B) A sense of contrasts

This expressivity was enriched by a strong sense of contrasts, based on increases or disruptions, which relied mostly on prestigious materials and various colors, even if they didn't follow the "ordo colorum". These ornamental contrasts were not only played on a binary mode between feasts and fasts. They can also mark different degrees of importance between feasts, as shown by the customs of the benedictine abbey of Saint-Augustine of Canterbury, which was copied around 1330-1340. For double feasts, this text prescribes placing a "pallio sive fronterio precioso" in front of the altar. But the solemnities are explicitly marked by an "augmentum pulcritudinis pallium sive fronterium deauratum" 50 . Hence also the complexity of certain ordinaries or sacristan guides whose purpose was to organize the ornamental hierarchies of liturgical time.

Conversely, after the increasing of the textile decorum for certain feasts, an ornamental deflation logically followed, which was more rarely expressed in texts. Although much earlier than the period studied, the ordinary of the Rheinau cathedral written at the beginning of the 12 th century specifies that after Compline on the Thursday after Easter, the frontal of the altar must be replaced by a humbler one: "Post completorium vel in crastino […], principalis quoque altaris pallium cum alio humiliori mutatur"51 .

Moreover, the solemnity of certain occasions could be manifested in contrast with silver or golden antependium. In 1410, in Châlons cathedral, the main altar must be covered with a dossal and a frontal made of black cendal (a kind of tabby) during Advent and Lent52 . However, on the solemnities, the main altar was stripped bare to reveal the golden tabula, adorned with gems and stones, which permanently enveloped its front face, while the two short sides of the altar were decorated with gilded and enameled copper53 . Here, the iconography mattered little (the inventory does not even describe it): the materials, colors and light effects had to be enough to demonstrate in a sensitive way the exceptional character of the feast. The clergy should also make great use of the movements of some textiles, covering or uncovering the altar, to punctuate liturgical time. We can easily imagine that the remotion of the black cendal led to a spectacular unveiling.

*

According to a common idea, the occasions of liturgical year should be above all identified by colors, playing the role of visual signs in the church. In this paper, I have shown that there was no semantic system associating textiles and liturgical time. It is essential to consider the marking of time by textiles in a dynamic and diachronic mode. In fact, the quality of time was less signified than expressed by textiles surrounding the altar. This expressivity was based on ornamental bridges and contrasting effects between certain occasions in the course of the circulus anni, which was very appropriate to translate the cyclicity of the liturgical time. The precise color or iconography of some frontals was less important than the general idea of abundance which they widely contributed and that they recreated in the course of the year. They were definitely involved in the 'chromatic rhythm' suggested by Jean-Claude Schmitt 54 , which was not supposed to be precisely analyzed but perceived as a whole 55 .

  used for the Invention and Exaltation of the Cross 30 . Lastly, a red frontal depicted with the images of the apostles covered the altar for the feasts of Andrew, Peter and Paul, Marc and Jacob 31 . Some inscriptions borne by textiles also quoted prayers said on specific feast's mass. The treasury of the Xanten cathedral preserve a red frontal, dated 1521, adorned with the images of the Virgin, Victor and Helen (Fig. 1) 32 . On the top of the textile, an inscription is written on a false super-frontal: "AVE MILES INVICTISSIME, AVE MARTYR SANCTISSIME, AVE PIE PROTECTOR SANCTE VICTOR". These words are the incipit of the antiphon sung during the feast of Victor, patron saint of the cathedral. From a semantic standpoint, we can hypothetically analyze those examples in two distinct ways 33 :

  Reallexikon zur deutschen Kunstgeschichte, Renate Kroos and Friedrich Kobler opened their article on liturgical colors in the catholic church by asserting that they should indicate or characterize liturgical times 12 . To support this idea, they cite the name of the rubric relative to that question in the De sacro altaris mysterio of Lothar of Segni: "De quatuor coloribus principalibus, quibus secundum proprietates dierum vestes sunt distinguendae".Nevertheless, in this title, it is colors that are qualified by times and there is no guarantee that the reverse is also true.

	system, colors are distinguished according to allegorical readings: white is used for solemnities
	(such as Easter or Christmas), for the feasts of the Virgin and those of other virgins. Red refers
	to apostles, martyrs and evangelists. Black signals penitential time. At last, green is used for
	common days.
	According to Michel Pastoureau: "as in heraldics, [the liturgical colors] are pure
	categories: they are abstract, conceptual colors, whose shades do not count" 16 . Moreover, just
	11 In the church, it is for example very well known that we can distinguish a priest from a deacon according to the
	shape of their garments (a chasuble or a dalmatic).
	12 Renate Kroos and Friedrich Kobler, "Liturgische Farbe in der katholische Kirche," in Reallexikon zur deutschen
	Kunstgeschichte, vol. 7 (Stuttgart and Munich, J. B. Metzler and in Komm: Bei der C. H. Beck'schen
	Verlagsbuchhandlung, 1981) col. 54-121.
	13 Michel Pastoureau, "Ordo colorum, notes sur la naissance des couleurs liturgiques," La Maison-Dieu 176,
	(1989): 54-66.
	14 Id., "Le temps mis en couleurs: des couleurs liturgiques aux modes vestimentaires (XII e -XIII e siècles),"
	Bibliothèque de l'école des chartes 157 (1999): 111-135 ; "Classer les couleurs au XII e siècle, liturgie et
	héraldique," Comptes rendus des séances de l'Académie des Inscriptions et Belles-Lettres 2, (2016): 845-864.
	15 Lothar of Segni, De sacro altaris mysterio, PL217 (Petit-Montrouge: J.-P. Migne, 1855), col. 763-916,
	799.
	16 Pastoureau, "Le temps mis en couleurs…," 113.

In a special issue of the Maison-Dieu, entitled 'Quand la liturgie donne à voir', Michel Pastoureau focused on the role of colors within the liturgy

13

. In 1999 and 2016, he re-asserted what he previously said in the 1980's 14 . Focusing on the way the adjectives relating to colors became nouns, Michel Pastoureau asserted the existence of an 'ordo colorum' that would have regulated in the church the use of four predetermined and pure colors - white, red, green and black -since the end of the twelfth century. According to him, Lothar of Segni would have solved hesitations and confusions and provided a centralized structure 15 , that would have been extended from Rome to the western Europe, a century later, by Durandus of Mende. In this

  Mémoires de la Société des antiquaires de Picardie, 10 (1950): 253-347, 322-330.24 Gousset, "Le coutumier de la sacristie de la cathédrale de Mende…," 217.25 On the iconography of liturgical textiles, see Iconography of Liturgical Textiles in the Middle Ages, ed. Evelin Wetter (Riggisberg: Abbeg-Stiftung, 2010).26 Ulysee Chevalier, Ordinaires de l'église cathédrale de Laon (XII e et XIII e siècle) suivis de deux mystères liturgiques (Paris: A. Picard, 1897), 260: "Tabule altaris non aperiuntur, sed paratur altare pannis sericis auro intextis, in quibus depictum est qualiter angelus salutat beatam Virginem".27 Louis Deschamps de Pas, "Inventaire des ornements, reliquaires, etc. de l'église collégiale de Saint-Omer en 1557," Bulletin archéologique du Comité des travaux historiques et scientifiques (1886): 78-98, 87: "Ung drap de velours rouge, avec l'imaige de la Résurrection, lequel sert à mettre devant la table d'aultel et au tombeau es festes de Pasques."

22 Marie-Thérèse Gousset, "Le coutumier de la sacristie de la cathédrale de Mende et les arts liturgiques," in Guillaume Durand: évêque de Mende, vers 1230-1296, canoniste, liturgiste et homme politique (Paris: Éd. du CNRS, 1992), 207-228, 222.

23

Jacques Garnier, "Inventaires de la cathédrale d'Amiens,"

28

Andreas Odenthal, Erwin Frauenknecht, Der Liber Ordinarius des Speyerer Domes aus dem 15. Jahrhundert (Münster: Aschendorff, 2012), fol. 24, 56: "eyn wyβ duch ruch samet duch mit bilden de Ressurectio." 29 Ibid., fol. 9, 29: "Item in festo Epiphanie domini, wan man die erste vesper lydet, so thut man das heuyligtum vff den altare und man thut eyn gryenes duch vor den altare mit den bylden der dryer kunige".

Giles Constable, "A living Past: the Historical Environment of the Middle Ages," Harvard Library Bulletin 1, no. 3 (autumn 1990): 49-70.

Miri Rubin, Corpus Christi: the Eucharist in the Late Medieval Culture (Cambridge: Cambridge University press, 1991).

This question is directly related to performance, see for example Laura Weigert, "Performance," Studies in Iconography 33 (2012, special issue: Medieval Art History Today): 61-72.

Roland Barthes, Système de la mode (Paris: Édition du Seuil, 1967).

Gil Bartholeyns, "Pour une histoire explicative du vêtement. L'historiographie, le XIII e siècle social et le XVI e siècle moral," in Fashion and Clothing in Late Medieval Europe/Mode und Kleidung im Europa des späten Mittelalters, ed Regula Schorta (Bâle and Riggisberg: Schwabe and Abegg-Stiftung, 2010), 209-230, 211.

Kate Dimitrova and Margaret Goehring, "Chapter 1: Introduction" in Dressing the Part: Textiles as Propaganda in the Middle Ages, ed. Kate Dimitrova and Margaret Goehring (Turnhout: Brepols, 2014), 7-10, 7.

Laura Weigert, Weaving Sacred Stories, French Choir Tapestries and the Performance of Clerical Identity (Ithaca: Cornell University Press, 2004), 80.

Anton Hänggi, Der Rheinauer Liber ordinarius (Zürich, Zentralbibliothek, Rh 80) (Fribourg: Éditions universitaires, 1957), 143.

Paul Pelicier and Alfred Darcel, "Inventaire des meubles et joyaux de la cathédrale de Châlons en 1410," Bulletin archéologique du Comité des travaux historiques et scientifiques 2 (1886): 135-188, 159, art. 138: "Item, duo paramenta de sendallo nigro, fourrata de tela crocea que ponuntur in Adventu et Quadragesima, unum ante tabulam et aliud ante dorsale majoris altaris."

Ibid., 155, art. 99: "Item tabula majoris altaris que discoperitur in totis et tertiis duplicibus, cooperta auro cum ymaginibus elevatis, ornata gemmis et lapidibus pretiosis et aliis, et duo latera cooperta sunt de cupro deaurato esmailliato."

and Saint-Jude of Goslar, written in 1435. This text commands that a frontal adorned with the image of the Virgin should be displayed in front of the main altar on the Virgin's Nativity [START_REF] Tillman Lohse | eine diachronisch vergleichende Geschichte des weltlichen Kollegiatstifts St. Simon und Judas[END_REF] , on the feasts of Dorothea, Barbara or on the feasts commemorating the action of another holy woman: the conversion of Magdalene and the Invention of the Cross by Helen 39 . For all these feasts, we might suppose that there was a metonymic link between these holy women and the Virgin, who could serve as a model. But the same frontal was more surprisingly used on the feasts of the bishop Valerius, Cosmas and Damian and the invention of Stephen's relics 40 .

Another frontal showing griffins and another image of the Virgin was displayed around the altar on the feasts of Ann, the king Oswald, but also the Transfiguration and the octave of All Saints 41 . Let's give a final example: a textile with the image of Jacob was not used for his feast, but for Barthelemy and Kathryn 42 .

All these examples invite us to rethink the links between iconography and time, as it is clear that clerics did not always favor simultaneity and correlation between the two. How can we understand these discrepancies? First, the choice of a textile was closely related to the specific devotions of a church. The sacristan handbook of Mende cathedral registered for example that the altar should be covered with a green or a red frontal for the feast of saint Andrew, because of the presence of relics [START_REF] Gousset | Le coutumier de la sacristie de la cathédrale de Mende[END_REF] . Even if the choice given between red or green is enigmatic, it is clear that having the relics played a role on the altar environment. In Saint-Martin-des-Champs in Paris, in 1342, the main altar was adorned with the image of Martin on horseback for the five feasts of the Virgin 44 , which was probably a way to place metonymically the priory under the protection of the Virgin [START_REF] Plagnieux | La Vierge à l'Enfant du prieuré parisien de Saint-Martin-des-Champs: son insertion dans le contexte architectural et liturgique[END_REF] .

In more general terms, textiles built bridges between feasts in an ornamental way. The ordinary of the Metz cathedral prescribe to reuse the same textiles for Easter and Christmas but also for the Dedication: "De altari dicimus quod debet sic parari: illud idem aurifrigium debet poni ante altare in Dedicatione quod apponitur in Natali et in Pascha" [START_REF] Pelt | Purificatione beate Marie debet poni illud idem aurifrigium quod positum ibi fuit in Natali Domini. Tres autem cruces debent poni retro altare, scilicet due minores et tercia maior[END_REF] . We find almost the


Maxime Amblard
email: amblard@labri.fr

Christian Retoré
email: retore@labri.fr

Natural Deduction and Normalisation for Partially Commutative Linear Logic and Lambek Calculus with Product

This paper provides a natural deduction system for Partially Commutative Intuitionistic Multiplicative Linear Logic (PCIMLL) and establishes its normalisation and subformula property. Such a system involves both commutative and non commutative connectives and deals with context that are series-parallel multisets of formulae. This calculus is the extension of the one introduced by de Groote presented by the second order for modelling Petri net execution, with a full entropy which allow order to be relaxed into any suborder -as opposed to the Non Commutative Logic of Abrusci and Ruet. Our result also includes, as a special case, the normalisation of natural deduction the Lambek calculus with product, which is unsurprising but yet unproved. Up to now PCIMLL with full entropy had no natural deduction. In particular for linguistic applications, such a syntax is much welcome to construct semantic representations from syntactic analyses.

Presentation

Non commutative logics arise naturally both in the mathematical perspective and in the modelling of some real world phenomena. Mathematically non commutativity is a natural both from the truth valued semantics viewpoint (phase semantics, based on monoids which can be non commutative) and from a syntactical one (sequent calculus with sequences rather than sets of formulae, proof nets which can have well bracketed axiom links). Non commutativity also appears from real world applications such as concurrency theory, like concurrent execution of Petri net, and in our favourite application, computational linguistic, and this goes back to the fifties and the apparition of the Lambek calculus. We first give a brief presentation of non commutative logics and then stress their interest for concurrency and computational linguistics.

.

Another kind of calculus was introduced as a sequent calculus by de Groote in [START_REF] De | Partially commutative linear logic: sequent calculus and phase semantics[END_REF], which has to be intuitionistic to work neatly. It consists in a superposition of the Lambek calculus (non commutative) and of Intuitionnistic Linear Logic (commutative). For making a distinction bewteen the two connectives it is necessary that the context includes two different commas mimicking the conjunctions, one being commutative and the other being non commutative. Hence we deal with series-parallel partial orders over multisets of formulae as sequent right hand side. Let us write (..., ...) for the parallel composition and ...; ... for the non commutative: hence {a, b}; {c, d} stands for the finite partial order a<c, b<c, a<d, b<d. Of course we would like the two conjunctions to be related. Either the commutative product is stronger than the non commutative one, or the other way round. Surprisingly, the two options work as well, provided one direction is fixed once and for all. This relationship between the two products results from a structural rule modifying the order. Now a difference should be underlined between the Abrusci-Ruet classical calculus [START_REF] Abrusci | Non-commutative logic I: The multiplicative fragment[END_REF] and the intuitionistic one of de Groote's and concern precisely the order rule. The Abrusci-Ruet definitely has an intuitionistic version by limiting it to sequents with a single formula on the right and intuitionistic connectives, namely implications and conjunctions. But there is an important difference with de Groote's calculus: what can be the order rule stigmatising the relation between the two conjunctions? As expected by its inventro an shown in [?] the calculus introduced by de Groote can use a general forgetful rule, which replace an order with a smaller one with respect to the inclusion of relations:

Γ ordered by I C entropy Γ ordered by J C
In de Groote's calculus J can be any order such that J ⊂ I (as set of ordered pairs of formulae in Γ ) while in Ruet J can only be obtained by turning some non commutative commas into commutative ones. This not equivalent to allowing as result any suborder as J. Indeed Bechet de Groote and the second author in [START_REF] Bechet | A complete axiomatisation of the inclusion of series-parallel partial orders[END_REF] showed that four rewriting rules are needed to obtained all possible seriesparallel partial suborders from some series parallel partial order. Here is a typical derivation that can be performed in de Groote's calculus and not in Ruet's.

({a, b}; {c, d}) (a ⊗ b) (c ⊗ d) {({a, b}; {c), d} (a ⊗ b) (c ⊗ d)
Abrusci-Ruet calculus admit a proof net syntax, which can be restricted to the intuitionistic case. Regarding the more flexible de Groote calculus, there neither exists proof nets, nor natural deduction: it only exists a sequent calculus which has been prove to enjoy cut-elimination in [START_REF] Retoré | A description of the non-sequential execution of petri nets in partially commutative linear logic[END_REF] (the semantic method of [START_REF] De | Partially commutative linear logic: sequent calculus and phase semantics[END_REF] for a simpler entropy can surely be adpated). This is what we propose in this paper, with normalisation. Firstly we thus obtain a calculus which is more convenient, in particular for computational linguistics applciations, because of the Curry-Howard isomorphism. Secondly normal deduction and the needed operations on orders might be a first step towards proof net syntax.

Motivation for such calculi in concurrency and computational linguistics Non commutativity in logic is rather natural in a resource consumption perspective. An hypothesis is viewed as a resource that can be use but then it is natural to think of how hypotheses are organised and accessible. As argued by Abrusci [START_REF] Abrusci | Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic[END_REF] and others, linearity is a mandatory condition for non commutativity. Observe that the first non commutative calculus, Lambek calculus [START_REF] Lambek | The mathematics of sentence structure[END_REF] which was invented long before linear logic, is a linear calculus, whose relation to oher logical system, in particular intuitionistic has only been understood after the invention of linear logic by Girard [START_REF] Girard | Linear logic[END_REF].

Concurrency, in which the order of the computations or of the resources matters, is of course a natural application. In the framework of proofs as programs, with normalisation as the computational process; it is rather the pomset logic and the calculus of structure which are of some use, because the order applies to cuts that are the computations to be performed [START_REF] Retoré | Pomset logic: a non-commutative extension of classical linear logic[END_REF][START_REF] Guglielmi | A system of interaction and structure[END_REF] But in the framework of proof search as computation, in the logic programming style of Miller, see e.g. [START_REF] Hodas | Logic programming in a fragment of intuitionistic linear logic[END_REF] or in planning, the calculus studied in this paper with an order on hypotheses is of course important. Indeed process calculi can be encoded in non commutative calculi and this was the main motivation for Ruet's work. The second author also provided a description of the parallel execution of a Petri net in the calculus we are studying -with the reverse entropy increasing order, but it does not change the properties of the calculus. It is a true concurrency approach, where a||b is not reduced to a; b ⊕ b; a (where ⊕ is the non deterministic choice). An execution according to a series parallel partial order corresponds to a proof in the partially commutative calculus that we study in this paper; in this order based approach of parallel computations any set of minimal transitions can be fired simultaneously. [START_REF] Retoré | A description of the non-sequential execution of petri nets in partially commutative linear logic[END_REF] Our main motivation for such calculi is computational linguistics and grammar formalisms. We are especially fond of logical description of grammar classes as introduced by Lambek because from a parse structure one is able to automatically compute the logical structure of the sentence. This especially true if the Lambek calculus or the partially commutative extensions, like the one we are studying, are given in a natural deduction format. Indeed, the syntactic categories can be turned into semantic categories on two types, individuals (e) and truth values (t), in such a way that the proof in the Lambek calculus (the syntactic analysis) can be turned into a proof intuitionistic logic, that is a lambda term describing a logical formula in Church's style.

Lambek calculus is definitely too restrictive as a syntactic formalism, in particular it only describes context free languages, and many common syntactic constructs are difficult to model: one would prefer the class of mildly context sensitive formalisms which are assumed to be large enough for natural language constructs, go beyond context-free languages, but admit polynomial parsing algorithms. This is the reason to use partially commutative calculi. In particular Lecomte and the second author managed to give a logical presentation [START_REF] Lecomte | Extending Lambek grammars: a logical account of minimalist grammars[END_REF] of Stabler's minimalist grammars [START_REF] Stabler | Derivational minimalism[END_REF] in this the de Groote calculus, presented in natural deduction to obtain semantic representation of the parsed sentences. In parsing as deduction paradigm and for other applications as well it is quite important to have normalisation, unicity of the normal form: indeed the normal form is the structure of the analysed sentence, and normalisation ensures the coherence of the calculus. The algorithm of normalisation, easily extracted from the proof is important as well: one define correct sentences as the ones such that some sequent can be proved, and both the parse structure and the semantic reading are obtained from the normal form.

Partially Commutative Linear Logic

The sequent calculus for Partially Commutative Linear Logic (PCIMLL) introduced by de Groote in [START_REF] De | Partially commutative linear logic: sequent calculus and phase semantics[END_REF] is a super imposition of commutative intuitionistic multiplicative linear logic and the Lambek calculus with product, that is non commutative intuitionistic multiplicative linear logic. Formulae are defined from a set of propositional variables p, by the commutative conjunction (⊗) , the non commutative conjunction ( ), the commutative implication ( ), the two non commutative implications (/ and \):

l ::= p | l l | l ⊗ l | l/l | l\l | l l
Right hand side, contexts are partially ordered multisets of formulae whose underlying order is series-parallel (sp). Such orders can be depicted by terms over formulae:

ctx ::= l| ctx; ctx | {ctx, ctx} Γ A ∆ A\C [\e] Γ ; ∆ C ∆ A/C Γ A [/e] Γ ; ∆ C Γ A ∆ A C [ e] {Γ, ∆} C A; Γ C [\i] Γ A\C Γ ; A C [/i] Γ C/A {A, Γ } C [ i] Γ A C ∆ A B Γ [ A; B ] C [ e] Γ [∆] C ∆ A ⊗ B Γ [{A, B}] C [⊗e] Γ [∆] C ∆ A Γ B [ i] ∆; Γ A B ∆ A Γ B [⊗i] {∆, Γ } A ⊗ B [axiom] A A Γ C [entropy -whenever Γ Γ ] Γ C
Fig. 1. The natural deduction rules for PCIMLL -Notice that for applying ⊗ e and e rules, A and B must be equivalent:

∀X = A, B X < A ⇔ x < B X > A ⇔ x > B
In the ⊗ e rule has A ≤ B and A ≥ B, while in the ⊗ e rule one has A < B. -Our formulation in a lambda calculus style of the elimination of the multiplicative linear logic conjunction is due Abramsky in [START_REF] Abramsky | Computational interpretations of linear logic[END_REF] -the corresponding term would be let x = (u, v)in t(u, v). -Although we do have normalisation and sub-formula property (next sections) we do not have complicated rules of the kind introduced in [START_REF] Negri | A normalizing system of natural deduction for intuitionistic linear logic[END_REF] for MLL.

We assume her rules are motivated by the exponential connectives and other properties.

3 Normalisation of PCMLL Proof. This is a case study, according to the rules above the product elimination. Observe that the product elimination rule only move upwards when both cancelled hypotheses are in the same premise and when their respective places in the order match the product elimination requirements. Here is one case.

∆ A ⊗ B Γ [{A, B}] D Φ D\C [\e] Γ [{A, B}]; Φ C [⊗e] Γ [∆]; Φ C ⇒ ∆ A ⊗ B Γ [{A, B}] D [⊗e] Γ [∆] D Φ D\C [\e] Γ [∆]; Φ C
We write S j for the occurrence of sequent inside a proof, |S j | for the corresponding sequent, and |S j | r for the formula on its right hand side.

In a proof δ , B(S 0 ) the principal branch issued from an occurrence S 0 of a sequent |S 0 | is the smallest upwards path containing S 0 and closed under the following operations:

1. if S ∈ B(S 0 ) is obtained by a unary rule R from an occurrence S of a sequent, then S ∈ B(S 0 ) as well; 2. if S ∈ B(S 0 ) is obtained by a product elimination rule e (resp. ⊗ e ) as depicted in figure 1 then the connective-marked premise which is S with

|S | = Γ [ A, B ] C (resp. |S | = Γ [{A, B}] C) is in B(S 0 ) as well. 3. if S ∈ B(S 0
) is obtained by an implication elimination rule \ e (resp. / e , e ) as depicted in figure 1 then the connective-marked premise S with

|S | = ∆ A \ C (resp. |S | = ∆ A / C, |S | = ∆ A C) is in B(S 0 ) as well.
Any initial subpath of a principal branch B(S 0 ) of length n from S 0 to S n with |S 0 | r = |S n | r , such that |S 0 | is the connective-marked premise of some elimination rule R e and S n is the conclusion of some introduction rule R i is called an n-extended redex. Observe that the rules R i and R e necessarly introduce and eliminate the same connective and are said to be conjoined. A 0-extended redex is called a redex, and there are seven redexes in PCIMLL see figure 3. A normal proof is defined as a proof without any k-extended-redex, for every k. Observe that there is at most one k-extented redex in a principal branch, because it's an initial path of S(B 0 ) and the rule above S n is an introduction.

Given an implication elimination rule R (resp. a product elimination rule R ), with connective-marked premise S 0 , the integer e(R) (resp. g(R )) is k if there is some (hence one) k-extended redex in B(S 0 ) called the k-extended redex above R (resp. above R ) and 0 otherwise. Given a proof δ let P ER(δ) and IER(δ) be respectively the of occurrences of product elimination rule in δ and of implication elimination rule in δ. We define e(δ) as min R∈P ER(δ) e(R) and g(δ) as min R∈IER(δ) g(R) and r(δ) as the number of rules in δ. The measure of δ denoted by |δ| is the triple (r(δ), e(δ), g(δ). A proof is normal if and only if its measure is r(δ, 0, 0).

Proposition 2 A k-extended-redex S 0 • • • S k containing an implication elimina- tion contains another k -extended-redex with k < k. • • • • • d1 ∆ D • • • D; Γ C [\i] Γ D\C [\e] D; Γ C • • • • • d1 ∆ D • • • ∆; Γ C • • • • • d1 ∆ D • • • (D, Γ ) C [ i] Γ D C [ e] (∆, Γ ) C • • • • • d1 ∆ D • • • (∆, Γ ) C • • • • • d1 ∆1 A • • • • • d2 ∆2 B [ i] ∆1; ∆2 A B Γ [ A A • • • A ; B B • • • B ] D [ Γ [ ∆1; ∆2 ] D Γ [ • • • d1 ∆1 A • • • ∆1 ; • • • d2 ∆2 B • • • ∆2 ] D • • • • • d1 ∆1 A • • • • • d2 ∆2 B [⊗i] {∆1, ∆2} A B Γ [{ A A • • • A , B B • • • B }] D [⊗e] Γ [{∆1, ∆2}] D Γ [{ • • • d1 ∆1 A • • • ∆1 , • • • d2 ∆2 B • • • ∆2 }] D • • • • • d1 Γ A ⊗ B A A B B [⊗i] (A, B) A ⊗ B [⊗e] Γ A ⊗ B • • • • • d1 Γ A ⊗ B • • • • • d1 Γ A B A A B B [ i] A; B A B [ e ] Γ A B • • • • • d1 Γ A B
Fig. 2. The seven redexes of PCIMLL Hence, a k-extended-redex which does not contain any k -extended-redex with k < k and in particular the extended redex associated with R such that e(R) = e(π) or g(R) = g(π), only contains entropy rules and product elimination rules.

Proposition 3 Product elimination and entropy can move below implication elimination rules.

Theorem 4 (Normalisation) Every proof π in PCMLL has a normal form.

Proof. We proceed by induction on the measure of the proof. We assume that for all proof π of size |π | < n, e, g has a normal form and let us show that any proof π with |π| = n, e, g can be turned into a normal proof. As every redex turns a proof into a proof with less rules, we can assume that π has no redex.

If e(π) = 0, then there exists an implication-elimination rule S with a e(π)extended redex. Since it's a minimal redex, this extended redex only contain product elimination rules and entropy rules by proposition 2. Consequently, by proposition 3 we can exchange S and the rule immediately above S because it's an entropy rule or a product elimination rule. The proof that we thus obtain π satifies n(π ) = n(π) and e(π ) < e(π) -in π e(S ) = e(S) -1. Hence, by induction π as a normal form and π as well.

If e(π) = 0 and g(π) = 0 then there exists a product-elimination rule S with a g(π)-extended redex. Since it's a minimal redex, this extended redex only contain product elimination rules and entropy rules by proposition 2. Consequently, we can exchange S and the rule immediately above S because it's an entropy rule or a product elimination rule. The proof that we thus obtain π satifies n(π ) = n(π) and still does not have any implication extended redex by checking that the modification does not create new principal branch -in n(π ) = n(π) g(π ) = g(π) = 0. Hence, by induction π as a normal form and π as well.

If e(π) = g(π) = 0, π is already normal.

Theorem 5 (Subformulae property) The sub-formula property holds for PCMLL: in a normal proof π of a sequent Γ C, every formulae of every sequent of π is a sub-formula of a formula of Γ or of the formula C.

Proof. We proceed by induction on the height of a normal proof showing the result and that whenever the last rule is some implication elimination, then C is a subformula of some formula of Γ . The entropy rule is ignored, both as a last rule and for measuring the height of a proof. Axioms enjoy this property.

Assuming the property holds for smaller proofs, and that our normal proofs ends with an introduction rule the result is clear. Assume the last rule is \ e -the other implication rules are handled mutatis mutandis. We successively inspect all possible rules above the connective-marked premise Γ A \ B:

axiom in this case the formula also appear in Γ as wished.

-\ i impossible there would exist a redex while the proof is in normal form.

all other introductions can not lead to Γ A \ B because of the \ in A \ B.

-\ e , / e and e : using the induction hypothesis.

-⊗ e and e which preserve the target of the sequent, namely A\B we consider the principal branch B(Γ A \ B). After a sequence of ⊗ e and e rules, yielding to a sequent ∆ A \ B we either find an axiom A \ B A \ B or any of the afore mentioned rules. In the first case A \ B is itself a formula of Γ and in the second one the induction hypothesis justifies the result.

Assume the last rule is ⊗ e with the connective marked sequent being Γ A ⊗ B, the other begin Θ[{A, B}] C and the conclusion Θ[Γ ] C. The only point to be checked is that A ⊗ B, which does not appear in the conclusion sequent, is a subformula of a formula of Γ . After a sequence of ⊗ e and e rules, yielding to a sequent ∆ A ⊗ B we either find an axiom A ⊗ B A ⊗ B or a proper rule R. In the first case A ⊗ B is itself a formula of Γ . In the second case R cannot be any implication introduction but it can neither be a product introduction since this initial part of the principal branch would be an extented redex. Hence it has to be an arrow elimination rule and thus A⊗B is a subformula of ∆, hence of Γ .

Observe that we have such results for a calculus with standard rules, as opposed to [START_REF] Negri | A normalizing system of natural deduction for intuitionistic linear logic[END_REF].

Lambek caculus with product is PCIMLL restricted to \, / and . Context only use ; ; as they are defined up to associativity, context are sequences of formulae and the entropy rule can safely be left out.

Theorem 4 implies that proofs in the L have a normal form enjoying the subformula property. In this particular case proofs have a unique normal proof which is reached when the algorithm underlying the normalisation proof is concluded by moving as high as possible the e as explained in proposition 1. The uniqueness of the normal proof is easily established from local confluence of the redex.

Conclusion and future work

Motivated by concurrency and computational linguistics we have been defining PCIMLL in natural deduction and proved normalisation. For Lambek calculus with product, a subcalculus of PCIMLL, we also characterized the unique normal proof. Regarding the full calculus, we characterized the normal proofs up to the permutation of commutative product elimination rules among them.

Next we'll look forward a proof net syntax for PCIMLL, which also allows to easily compute lambda terms. Despite the existence of proof nets for MLL andfor the Lambek calculus (of which PCMLL is the superimposition), and for intuitionistic NL of Abrusci and Ruet, because of the more flexible entropy rule that we are using, there is not yet any proof net calculus for PCNLL. This work in aprticular on normal proofs which split the entropy rules into canonical steps according to the rules used above and below can be viewed as a first step in this direction.

With respect to computational linguistic application, our results tighten the already explored connection between minimalist grammars and linear calculi in a natural deduction format, which is responsible for the automatic computing of semantic recipes. It also opens the possibility to have concurrent abstract machines for minimalist grammars, since their coding uses the same formulae as Petri nets coding. The linear deduction also enables a use of other semantics like ludics.

Proposition 1 (

 1 Product eliminations can move upwards) Let R be an ⊗ e rule (resp. an e rule) ofΓ [∆] C between a proof δ 0 of ∆ A ⊗ B and a proof of Γ [{A, B}] C (resp. Γ [ A; B ] C) obtained by a rule R from a proof δ 1 of some sequent Θ[{A, B}] X (resp. Θ[ A; B ] X) and possibly, if R is binary, of another proof δ 2 of some sequent Ψ U .Then one can obtain a proof of the same sequent Γ [∆] C by first applying an ⊗ e rule (resp. an e rule) between the proof δ 0 of ∆ A ⊗ B and the proof δ 1 of Θ[{A, B}] X (resp. Θ[ A; B ] X) yielding a proof of Θ[∆] X and then applying R to this proof and possibly the proof δ 2 of the sequent Ψ U .

For instance the context B; {A (B \ (D / C), A} ; C denotes the sp order Succ(B) = {A, A (B \ (D / C)}, Succ(A) = Succ(A (B \ (D / C)) = {C} -Succ(X) stands for the immediate successors of X and this fucntion from the domain to the parts of of the domain compeltely determines a finite order.The term denoting a given sp order is unique up to the associativity of series and parallel composition and to the commutativity of parallel composition and to avoid rewriting associated with associativity or commutativity we consider equal two contexts that are associated with the same sp orpder on the same multiset of formulae. Capital greek letters stand for contexts. An expression like Γ [] means a context with one distinguished element [ * , while an expression like Γ [∆] means that the special element [ * ] has been replaced with the context ∆. More details can be found in[START_REF] Bechet | A complete axiomatisation of the inclusion of series-parallel partial orders[END_REF][START_REF] Retoré | A description of the non-sequential execution of petri nets in partially commutative linear logic[END_REF].-Γ Γ means that the domains of the two sp orders, the set of occurrences of formulae, are the same and that A < B in Γ if and only if A < B in Γ as well -A and B being /emphoccurrences of formulae. The inclusion of series parallel partial orders can be simulated by term rewriting as shown in[START_REF] Bechet | A complete axiomatisation of the inclusion of series-parallel partial orders[END_REF].

Acknowledgement We would like to apologize to the reviewers for the mistakes and the poor style of the version that was sent to them.