Episciences.org
Not a member yet
6707 research outputs found
Sort by
Transpension: The Right Adjoint to the Pi-type
No full textPresheaf models of dependent type theory have been successfully applied tomodel HoTT, parametricity, and directed, guarded and nominal type theory. Therehas been considerable interest in internalizing aspects of these presheafmodels, either to make the resulting language more expressive, or in order tocarry out further reasoning internally, allowing greater abstraction andsometimes automated verification. While the constructions of presheaf modelslargely follow a common pattern, approaches towards internalization do not.Throughout the literature, various internal presheaf operators (,, , , ,, the strictness axiom and locally fresh names) can be found andlittle is known about their relative expressivenes. Moreover, some of theserequire that variables whose type is a shape (representable presheaf, e.g. aninterval) be used affinely. We propose a novel type former, the transpensiontype, which is right adjoint to universal quantification over a shape. Itsstructure resembles a dependent version of the suspension type in HoTT. We givegeneral typing rules and a presheaf semantics in terms of base categoryfunctors dubbed multipliers. Structural rules for shape variables and certainaspects of the transpension type depend on characteristics of the multiplier.We demonstrate how the transpension type and the strictness axiom can becombined to implement all and improve some of the aforementionedinternalization operators (without formal claim in the case of locally freshnames)
Normal forms for quasi-elliptic Enriques surfaces and applications
No full textWe work out normal forms for quasi-elliptic Enriques surfaces and giveseveral applications. These include torsors and numerically trivialautomorphisms, but our main application is the completion of the classificationof Enriques surfaces with finite automorphism groups started by Kondo, Nikulin,Martin and Katsura-Kondo-Martin.Comment: 32 pages; (epi)journal versio
Old Permic Universal Dependencies Treebank
No full textOld Permic, also known as Old Komi, is an extinct variety of Komi that was spoken in the late Middle Ages in the lower Vychegda river basin in Northeastern European Russia, in an area that currently is not Komi-speaking. This language variety is attested in fragmentary records from the 14th to 17th century written both in the Old Permic alphabet and in Cyrillic. These records are of significant importance for research on the history of the Komi language. Here we introduce our attempt towards a new Universal Dependencies treebank that will eventually contain the existing corpus of Old Permic in a structured and CoNLL-U annotated format. This will be the first time this material is being made openly available in digital format, and our contribution describes the current state of the art and remaining challenges
Extensions of curves with high degree with respect to the genus
No full textWe classify linearly normal surfaces of degree such that , where is the sectional genus (itis a classical result that for larger there are only cones). We apply thisto the study of the extension theory of pluricanonical curves and genus curves, whenever they verify Property , using and slightly expanding thetheory of integration of ribbons of the authors and E.~Sernesi. We compute thecorank of the relevant Gaussian maps, and we show that all ribbons over suchcurves are integrable, and thus there exists a universal extension. We carry out a similar program for linearly normal hyperelliptic curves ofdegree . We classify surfaces having such a curve as ahyperplane section, compute the corank of the relevant Gaussian maps, and provethat all ribbons over are integrable if and only if . In the lattercase we obtain the existence of a universal extension.Comment: v2: various complements with respect to v1; v3: correction in the statement of Hartshorne's Theorem 2.5: v4: final versio
L’approvisionnement en molasse dans les bâtiments savoyards du bord du Léman au Moyen Âge : l’exemple du château de Ripaille
No full textL’approvisionnement en molasse (grès tendre à ciment calcaire) est cité dans les comptes du château de Ripaille (Haute-Savoie). En étudiant l’évolution architecturale du château, les caractéristiques géologiques de la molasse dans la région, les aspects techniques et les informations sur les carrières, il est possible de reconstituer le travail des artisans et l’organisation des approvisionnements et du chantier. Depuis l’extraction et la pré-taille dans les carrières subaquatiques du lac Léman, les pierres sont transportées par voie d’eau puis par route. La molasse, bien que facile à extraire et à façonner, est une pierre de construction de piètre qualité car le ciment calcaire est peu cristallisé et la roche est poreuse et sensible aux intempéries. C’était cependant un matériau de prédilection au Moyen Âge en raison de sa facilité de mise en œuvre contrairement aux calcaires plus durs, pourtant fréquents et disponibles dans la région
Partial-dual genus polynomial as a weight system
No full textWe prove that the partial-dual genus polynomial considered as a function onchord diagrams satisfies the four-term relation. Thus it is a weight systemfrom the theory of Vassiliev knot invariants.Comment: Final version for publication in Communications in Mathematic
ArchEthno - a new tool for sharing research materials and a new method for archiving your own research
No full textThe archiving of ethnographic material is generally considered a blind spot in ethnographic working methods which place more importance on actual investigations and analysis than on how archives are constructed. A team of computer scientists and ethnographers has built an initial tool for sharing ethnographic materials, based on an SQL relational data model that suited the first survey processed but proved difficult to transpose to other surveys. The team developed a new tool based on dynamic vocabularies of concepts which breaks down archiving into three stages. Firstly ethnographers can select and contextualise their survey materials; secondly they structure them in a database according to the research question discovered during their survey; finally, they share this data with other researchers subject to the opinion of an ethics committee whose members are competent in ethnography
Strongly Sublinear Algorithms for Testing Pattern Freeness
No full textFor a permutation , a function contains a -appearance if there exists such that for all , if and only if. The function is -free if it has no -appearances.In this paper, we investigate the problem of testing whether an input function is -free or whether differs on at least valuesfrom every -free function. This is a generalization of the well-studiedmonotonicity testing and was first studied by Newman, Rabinovich,Rajendraprasad and Sohler (Random Structures and Algorithms 2019). We show thatfor all constants , , and permutation, there is a one-sided error -testing algorithmfor -freeness of functions that makes queries. We improve significantly upon the previous bestupper bound by Ben-Eliezer and Canonne (SODA 2018). Ouralgorithm is adaptive, while the earlier best upper bound is known to be tightfor nonadaptive algorithms.Comment: 28 pages, 2 figures; We thank anonymous reviewers for comments that helped us significantly improve the presentatio
Quantitative stability estimate for the inverse coefficients problem in linear elasticity
No full textIn this article we consider the inverse problem of reconstructing piece-wise Lamé coefficients from boundary measurements. We reformulate the inverse problem into a minimization one using a Kohn-Vogelius type functional. We study the stability of the parameters when the jump of the discontinuity is perturbed. Using tools of shape calculus, we give a quantitative stability result for local optimal solution.Dans cet article, nous considérons le problème inverse de reconstruction des coefficients de Lamé constants par morceaux à partir de mesures au bord. Nous reformulons le problème inverse en un problème de minimisation utilisant une fonctionnelle de type Kohn-Vogelius. Nous étudions la stabilité des paramètres lorsque le saut de la discontinuité est perturbé. En utilisant les outils du calcul de forme, nous donnons un résultat de stabilité quantitative pour une la solution optimale locale
Fair Asynchronous Session Subtyping
No full textSession types are widely used as abstractions of asynchronous message passingsystems. Refinement for such abstractions is crucial as it allows improvementsof a given component without compromising its compatibility with the rest ofthe system. In the context of session types, the most general notion ofrefinement is asynchronous session subtyping, which allows message emissions tobe anticipated w.r.t. a bounded amount of message consumptions. In this paperwe investigate the possibility to anticipate emissions w.r.t. an unboundedamount of consumptions: to this aim we propose to consider fair compliance overasynchronous session types and fair refinement as the relation that preservesit. This allows us to propose a novel variant of session subtyping thatleverages the notion of controllability from service contract theory and thatis a sound characterisation of fair refinement. In addition, we show that bothfair refinement and our novel subtyping are undecidable. We also present asound algorithm which deals with examples that feature potentially unboundedbuffering. Finally, we present an implementation of our algorithm and anempirical evaluation of it on synthetic benchmarks