Episciences.org
Not a member yet
6707 research outputs found
Sort by
A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct
No full textWe study the expressiveness and succinctness of history-deterministicpushdown automata (HD-PDA) over finite words, that is, pushdown automata whosenondeterminism can be resolved based on the run constructed so far, butindependently of the remainder of the input word. These are also known asgood-for-games pushdown automata. We prove that HD-PDA recognise more languagesthan deterministic PDA (DPDA) but not all context-free languages (CFL). Thisclass is orthogonal to unambiguous CFL. We further show that HD-PDA can beexponentially more succinct than DPDA, while PDA can be double-exponentiallymore succinct than HD-PDA. We also study HDness in visibly pushdown automata(VPA), which enjoy better closure properties than PDA, and for which we showthat deciding HDness is ExpTime-complete. HD-VPA can be exponentially moresuccinct than deterministic VPA, while VPA can be exponentially more succinctthan HD-VPA. Both of these lower bounds are tight. We then compare HD-PDA withPDA for which composition with games is well-behaved, i.e. good-for-gamesautomata. We show that these two notions coincide, but only if we considerpotentially infinitely branching games. Finally, we study the complexity ofresolving nondeterminism in HD-PDA. Every HDPDA has a positional resolver, afunction that resolves nondeterminism and that is only dependant on the currentconfiguration. Pushdown transducers are sufficient to implement the resolversof HD-VPA, but not those of HD-PDA. HD-PDA with finite-state resolvers aredeterminisable
Coloring Groups
No full textWe introduce coloring groups, which are permutation groups obtained from aproper edge coloring of a graph. These groups generalize the generalized togglegroups of Striker (which themselves generalize the toggle groups introduced byCameron and Fon-der-Flaass). We present some general results connecting thestructure of a coloring group to the structure of its graph coloring, providinggraph-theoretic characterizations of the centralizer and primitivity of acoloring group. We apply these results particularly to generalized togglegroups arising from trees as well as coloring groups arising from theindependence posets introduced by Thomas and Williams
Hypergraphs with Polynomial Representation: Introducing -splits
No full textInspired by the split decomposition of graphs and rank-width, we introducethe notion of -splits. We focus on the family of -splits of a graph oforder , and we prove that it forms a hypergraph with several properties. Weprove that such hypergraphs can be represented using only of its hyperedges, despite its potentially exponential number of hyperedges. Wealso prove that there exist hypergraphs that need at least hyperedges to be represented, using a generalization of set orthogonality
A new sufficient condition for a 2-strong digraph to be Hamiltonian
No full textIn this paper we prove the following new sufficient condition for a digraphto be Hamiltonian: {\it Let be a 2-strong digraph of order . If vertices of have degrees at least and the remaining vertexhas degree at least , where is a non-negative integer, then isHamiltonian}. This is an extension of Ghouila-Houri's theorem for 2-strong digraphs and isa generalization of an early result of the author (DAN Arm. SSR (91(2):6-8,1990). The obtained result is best possible in the sense that for thereis a digraph of order (respectively, ) with the minimum degree (respectively, with the minimum ) whose vertices havedegrees at least , but it is not Hamiltonian. We also give a new sufficient condition for a 3-strong digraph to beHamiltonian-connected.Comment: 20 pages, 2 figure
The PORTSEA (Portuguese School of Extremes and Applications) and a few personal scientific achievements
No full textThe Portuguese School of Extremes and Applications is nowadays wellrecognised by the international scientific community, and in my opinion, theorganisation of a NATO Advanced Study Institute on Statistical Extremes andApplications, which took place at Vimeiro in the summer of 1983, was a landmarkfor the international recognition of the group. The dynamic of publication hasbeen very high and the topics under investigation in the area of Extremes havebeen quite diverse. In this article, attention will be paid essentially to someof the scientific achievements of the author in this field.Comment: 70 pages, 8 figure
Non-local fatigue criterion based on standard deviation for notches and defects in Ti-6Al-4V
No full textThe aim of this study is to propose a non local multiaxial fatigue criterion in order to assess the fatigue limit of stress concentrator such as notches or defects in Ti-6Al-4V. This criterion is based on the standard deviation of the stresses integrated over a given volume around the hot spot point. Up to now, the standard deviation has never been tested as an indicator of stress heterogeneity to assess fatigue life of notch components. Four parameters are necessary to identify the criterion. The criterion is first validated on notched samples based on literature results and shows very good results. A set of experimental tests is conducted on natural and artificial defects including clustering defects and demonstrates the flexibility and accuracy of the criterion
Higher-Order Asynchronous Effects
No full textWe explore asynchronous programming with algebraic effects. We complementtheir conventional synchronous treatment by showing how to naturally alsoaccommodate asynchrony within them, namely, by decoupling the execution ofoperation calls into signalling that an operation's implementation needs to beexecuted, and interrupting a running computation with the operation's result,to which the computation can react by installing interrupt handlers. Weformalise these ideas in a small core calculus and demonstrate its flexibilityusing examples ranging from a multi-party web application, to pre-emptivemulti-threading, to (cancellable) remote function calls, to a parallel variantof runners of algebraic effects. In addition, the paper is accompanied by aformalisation of the calculus's type safety proofs in Agda, and a prototypeimplementation in OCaml.Comment: Extended journal version of a POPL 2021 paper and thus substantial text overlap with arXiv:2003.0211
Наталья Головкина как посредница во франко-русском культурном взаимодействии: Mесто одного женского эпистолярного романа в истории русской литературы XIX века
No full textIt is generally admitted that the epistolary novel genre does not exist in Russian romantic and pre-romantic literature. As the exception to prove the rule, the novel The Letters of Ernest and Doravra (1766) by Fyodor Emin, an emigrant of uncertain origin who arrived in Russia in 1761, is sometimes mentioned. Natalia Golovkina’s Elisabeth de S***, or the History of a Russian girl narrated by one of her compatriots , which appeared in its original French version in Paris in 1802 and in Russian in Moscow in 1803-1804, is cited even more rarely and always as an example of a weak or insignificant work. In the context of the recent revaluation of the place of women in Russian literary history, this opinion hardly seems justified. Among the Russian fiction of the 1800s, Golovkina’s novel stands out for its innovative character. First, Elisabeth de S*** is an original example of Franco-Russian cultural mediation: the writer created a novel about Russian life based on French (and European) literary models and published it in two different countries. Golovkina’s work is also characterized by an interest in the psychology of her characters and in the evolution of love. Finally, it is a vast novel (some 600 pages), remarkable for its complex plot and the number of characters. In paying tribute to this unjustly forgotten writer, we will seek to understand why her work did not become part of the Russian literary canon.Il est généralement admis que le genre du roman épistolaire n’existe pas dans la littérature romantique et préromantique russe. Comme l’exception qui confirme la règle, on évoque parfois le roman Les Lettres d’Ernest et de Doravra (1766) de Fiodor Emine, un émigré d’origine incertaine arrivé en Russie en 1761. Le roman de Natalia Golovkina Elisabeth de S***, ou L’Histoire d’une Russe publiée par une de ses compatriotes , qui paraît dans sa version originale française à Paris en 1802 et en russe à Moscou en 1803-1804, est cité encore plus rarement et toujours en tant qu’exemple d’œuvres faibles ou insignifiantes. Dans le contexte de la réévaluation récente de la place des femmes dans l’histoire littéraire russe, cette critique semble peu justifiée. Parmi les œuvres russes de la première décennie du XIXe siècle, le roman de Golovkina se distingue par son caractère novateur. Tout d’abord, Elisabeth de S*** est un exemple original de médiation culturelle franco-russe : l’écrivaine crée un roman consacré à la vie russe d’après les modèles littéraires français (et européens) et elle le publie dans deux pays différents. L’œuvre de Golovkina se caractérise, ensuite, par l’intérêt pour la psychologie des personnages et pour les sentiments amoureux. Enfin, c’est un roman d’envergure (quelque 600 pages) remarquable pour son intrigue complexe ainsi que pour un personnel romanesque important. En rendant hommage à l’écrivaine injustement oubliée, nous chercherons à comprendre pourquoi son œuvre n’a pas été intégrée dans le canon littéraire russe.Общепризнанно, что в русской романтической и преромантической литературе жанр романа в письмах не получил распространения. В качестве исключения, подтверждающего правило, упоминают иногда роман «Письма Эрнеста и Доравры» Федора Эмина, эмигранта, приехавшего в Россию в 1761 году, чье происхождение в настоящее время точно не установлено. Роман Натальи Головкиной «Елизавета из С***, или История одной россиянки, рассказанная её соотечественницей», опубликованный на французском языке в Париже в 1802 и на русском языке в Москве в 1803-1804 годах, упоминается ещё реже, и всегда в качестве примера произведений слабых и незначительных. В контексте недавней переоценки места женского творчества в истории русской литературы такая критика кажется малообоснованной. Среди произведений первого десятилетия XIX века роман Головкиной выделяется скорее своим новаторским характером, чем недостатками. В первую очередь, он является примером культурной медиации, поскольку писательница создает роман, рассказывающий о жизни в России, опираясь на французские (европейские) литературные модели, и публикует его в двух странах. Произведение также характеризуется интересом к психологии персонажей и к эволюции любовного чувства. Наконец, роман отличается своими размерами (около 600 страниц), замысловатой интригой, а также сложной системой персонажей. Отдавая дань уважения незаслуженно забытой писательнице, мы пытаемся ответить на вопрос, почему её роман не вошёл в русский литературный канон
Sharing proofs with predicative theories through universe-polymorphic elaboration
No full textAs the development of formal proofs is a time-consuming task, it is importantto devise ways of sharing the already written proofs to prevent wasting timeredoing them. One of the challenges in this domain is to translate proofswritten in proof assistants based on impredicative logics to proof assistantsbased on predicative logics, whenever impredicativity is not used in anessential way. In this paper we present a transformation for sharing proofswith a core predicative system supporting prenex universe polymorphism. Itconsists in trying to elaborate each term into a predicativeuniverse-polymorphic term as general as possible. The use of universepolymorphism is justified by the fact that mapping each universe to a fixed onein the target theory is not sufficient in most cases. During the elaboration,we need to solve unification problems in the equational theory of universelevels. In order to do this, we give a complete characterization of when asingle equation admits a most general unifier. This characterization is thenemployed in a partial algorithm which uses a constraint-postponement strategyfor trying to solve unification problems. The proposed translation is of coursepartial, but in practice allows one to translate many proofs that do not useimpredicativity in an essential way. Indeed, it was implemented in the toolPredicativize and then used to translate semi-automatically many non-trivialdevelopments from Matita's library to Agda, including proofs of Bertrand'sPostulate and Fermat's Little Theorem, which (as far as we know) were notavailable in Agda yet
QBF Merge Resolution is powerful but unnatural
No full textThe Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorffet al. in 2019, explicitly builds partial strategies inside refutations. Theoriginal motivation for this approach was to overcome the limitationsencountered in long-distance Q-Resolution proof system (LD-Q-Res), where thesyntactic side-conditions, while prohibiting all unsound resolutions, also endup prohibiting some sound resolutions. However, while the advantage of M-Resover many other resolution-based QBF proof systems was already demonstrated, acomparison with LD-Q-Res itself had remained open. In this paper, we settlethis question. We show that M-Res has an exponential advantage over not onlyLD-Q-Res, but even over LQU-Res and IRM, the most powerful among currentlyknown resolution-based QBF proof systems. Combining this with results fromBeyersdorff et al. 2020, we conclude that M-Res is incomparable with LQU-Resand LQU-Res. Our proof method reveals two additional and curious featuresabout M-Res: (i) M-Res is not closed under restrictions, and is hence not anatural proof system, and (ii) weakening axiom clauses with existentialvariables provably yields an exponential advantage over M-Res withoutweakening. We further show that in the context of regular derivations,weakening axiom clauses with universal variables provably yields an exponentialadvantage over M-Res without weakening. These results suggest that M-Res isbetter used with weakening, though whether M-Res with weakening is closed underrestrictions remains open. We note that even with weakening, M-Res continues tobe simulated by eFrege red (the simulation of ordinary M-Res wasshown recently by Chew and Slivovsky)