Episciences.org
Not a member yet
6707 research outputs found
Sort by
Profinite lambda-terms and parametricity
No full textCombining ideas coming from Stone duality and Reynolds parametricity, weformulate in a clean and principled way a notion of profinite lambda-termwhich, we show, generalizes at every type the traditional notion of profiniteword coming from automata theory. We start by defining the Stone space ofprofinite lambda-terms as a projective limit of finite sets of usuallambda-terms, considered modulo a notion of equivalence based on the finitestandard model. One main contribution of the paper is to establish that,somewhat surprisingly, the resulting notion of profinite lambda-term comingfrom Stone duality lives in perfect harmony with the principles of Reynoldsparametricity. In addition, we show that the notion of profinite lambda-term iscompositional by constructing a cartesian closed category of profinitelambda-terms, and we establish that the embedding from lambda-terms modulobeta-eta-conversion to profinite lambda-terms is faithful using Statman'sfinite completeness theorem. Finally, we prove that the traditional Churchencoding of finite words into lambda-terms can be extended to profinite words,and leads to a homeomorphism between the space of profinite words and the spaceof profinite lambda-terms of the corresponding Church type.Comment: For the proceedings of MFPS202
Interactive Analysis and Visualisation of Annotated Collocations in Spanish (AVAnCES)
No full textPhraseology studies have been enhanced by Corpus Linguistics, which has become an interdisciplinary field where current technologies play an important role in its development. Computational tools have been implemented in the last decades with positive results on the identification of phrases in different languages. One specific technology that has impacted these studies is social media. As researchers, we have turned our attention to collecting data from these platforms, which comes with great advantages and its own challenges. One of the challenges is the way we design and build corpora relevant to the questions emerging in this type of language expression. This has been approached from different angles, but one that has given invaluable outputs is the building of linguistic corpora with the use of online web applications. In this paper, we take a multidimensional approach to the collection, design, and deployment of a phraseology corpus for Latin American Spanish from Twitter data, extracting features using NLP techniques, and presenting it in an interactive online web application. We expect to contribute to the methodologies used for Corpus Linguistics in the current technological age. Finally, we make this tool publicly available to be used by any researcher interested in the data itself and also on the technological tools developed here
A Spatial Logic for Simplicial Models
No full textCollective Adaptive Systems often consist of many heterogeneous componentstypically organised in groups. These entities interact with each other byadapting their behaviour to pursue individual or collective goals. In thesesystems, the distribution of these entities determines a space that can beeither physical or logical. The former is defined in terms of a physicalrelation among components. The latter depends on logical relations, such asbeing part of the same group. In this context, specification and verificationof spatial properties play a fundamental role in supporting the design ofsystems and predicting their behaviour. For this reason, different tools andtechniques have been proposed to specify and verify the properties of space,mainly described as graphs. Therefore, the approaches generally use modelspatial relations to describe a form of proximity among pairs of entities.Unfortunately, these graph-based models do not permit considering relationsamong more than two entities that may arise when one is interested indescribing aspects of space by involving interactions among groups of entities.In this work, we propose a spatial logic interpreted on simplicial complexes.These are topological objects, able to represent surfaces and volumesefficiently that generalise graphs with higher-order edges. We discuss how thesatisfaction of logical formulas can be verified by a correct and completemodel checking algorithm, which is linear to the dimension of the simplicialcomplex and logical formula. The expressiveness of the proposed logic isstudied in terms of the spatial variants of classical bisimulation andbranching bisimulation relations defined over simplicial complexes
Computing with Infinite Objects: the Gray Code Case
No full textInfinite Gray code has been introduced by Tsuiki as a redundancy-freerepresentation of the reals. In applications the signed digit representation ismostly used which has maximal redundancy. Tsuiki presented a functional programconverting signed digit code into infinite Gray code. Moreover, he showed thatinfinite Gray code can effectively be converted into signed digit code, but theprogram needs to have some non-deterministic features (see also H. Tsuiki, K.Sugihara, "Streams with a bottom in functional languages"). Berger and Tsuikireproved the result in a system of formal first-order intuitionistic logicextended by inductive and co-inductive definitions, as well as some new logicalconnectives capturing concurrent behaviour. The programs extracted from theproofs are exactly the ones given by Tsuiki. In order to do so, co-inductivepredicates \bS and \bG are defined and the inclusion \bS \subseteq \bG isderived. For the converse inclusion the new logical connectives are used tointroduce a concurrent version of and \bG \subseteq \bS_{2} isshown. What one is looking for, however, is an equivalence proof of theinvolved concepts. One of the main aims of the present paper is to close thegap. A concurrent version \bG^{*} of \bG and a modification \bS^{*} of\bS_{2} are presented such that \bS^{*} = \bG^{*}. A crucial tool in U.Berger, H. Tsuiki, "Intuitionistic fixed point logic" is a formulation of theArchimedean property of the real numbers as an induction principle. Weintroduce a concurrent version of this principle which allows us to prove that\bS^{*} and \bG^{*} coincide. A further central contribution is theextension of the above results to the hyperspace of non-empty compact subsetsof the reals
Propagation of chaos in mean field networks of FitzHugh-Nagumo neurons
No full textIn this article, we are interested in the behavior of a fully connectednetwork of neurons, where tends to infinity. We assume that the neuronsfollow the stochastic FitzHugh-Nagumo model, whose specificity is thenon-linearity with a cubic term. We prove a result of uniform in timepropagation of chaos of this model in a mean-field framework. We also exhibitexplicit bounds. We use a coupling method initially suggested by A. Eberle(arXiv:1305.1233), and recently extended in (1805.11387), known as thereflection coupling. We simultaneously construct a solution of the -particlesystem and independent copies of the non-linear McKean-Vlasov limit in sucha way that, considering an appropriate semi-metric that takes into account thevarious possible behaviors of the processes, the two solutions tend to getcloser together as increases, uniformly in time. The reflection couplingallows us to deal with the non-convexity of the underlying potential in thedynamics of the quantities defining our network, and show independence at thelimit for the system in mean field interaction with sufficiently smallLipschitz continuous interactions.Comment: 50 pages, published versio
HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
No full textHyperproperties are system properties that relate multiple computation pathsin a system and are commonly used to, e.g., define information-flow policies.In this paper, we study a novel class of hyperproperties that allow reasoningabout strategic abilities in multi-agent systems. We introduce HyperATL*, anextension of computation tree logic with path variables and strategyquantifiers. Our logic supports quantification over paths in a system - as ispossible in hyperlogics such as HyperCTL* - but resolves the paths based on thestrategic choices of a coalition of agents. This allows us to capture manypreviously studied (strategic) security notions in a unifying hyperlogic.Moreover, we show that HyperATL* is particularly useful for specifyingasynchronous hyperproperties, i.e., hyperproperties where the execution speedon the different computation paths depends on the choices of a scheduler. Weshow that finite-state model checking of HyperATL* is decidable and present amodel checking algorithm based on alternating automata. We establish that ouralgorithm is asymptotically optimal by proving matching lower bounds. We haveimplemented a prototype model checker for a fragment of HyperATL* that cancheck various security properties in small finite-state systems
De l’exhibition dans les expositions coloniales au nouveau Musée national aïnou: La voix des autochtones est-elle impénétrable dans l’espace muséal ?
No full textHas the inauguration of the first Ainu National Museum in Japan in 2020, which follows the recognition of their indigenous status in 2019, redefined the actors at play in discussing Ainu history? The study of this new museum will serve as a case study to analyse the elaboration of discourses defining Self and Other, as well as the relationship between those who produce knowledge about the Ainu and the Ainu themselves.L’inauguration en 2020 au Japon du premier Musée national aïnou, qui fait suite à la reconnaissance officielle de leur autochtonie en 2019, a-t-il rebattu les cartes de ceux qui ont voix au chapitre ? L’étude de ce nouveau musée sera l’occasion de revenir sur la construction des discours portés sur l’Autre et sur Soi et les rapports entretenus entre les producteurs de savoir et les personnes sur qui portaient et qui portent aujourd’hui ce savoir
Conceptions des étudiants des classes préparatoires en Tunisie sur l'intégrale de Riemann
No full textThe integral is one of the most important topics in Calculus that is difficult to be understood by many students. When solving definite integral application problems, previous research emphasizes that students found the antiderivative procedure more useful and easier than the approximation process or area (Akrouti, 2020). This paper focuses on students' conceptions of the definite integral in the first year of preparatory class. Data were collected from students' written responses to questions that relate to their views of integration. The analysis shows that the majority of students choose the algebraic process to evaluate the proposed integrals. Participants were first-semester calculus students enrolled in a public university
The Variance and the Asymptotic Distribution of the Length of Longest -alternating Subsequences
No full textWe obtain an explicit formula for the variance of the number of -peaks ina uniformly random permutation. This is then used to obtain an asymptoticformula for the variance of the length of longest -alternating subsequencein random permutations. Also a central limit is proved for the latterstatistic.Comment: Typos and errors correcte
Bridging Causal Reversibility and Time Reversibility: A Stochastic Process Algebraic Approach
No full textCausal reversibility blends reversibility and causality for concurrentsystems. It indicates that an action can be undone provided that all of itsconsequences have been undone already, thus making it possible to bring thesystem back to a past consistent state. Time reversibility is insteadconsidered in the field of stochastic processes, mostly for efficient analysispurposes. A performance model based on a continuous-time Markov chain is timereversible if its stochastic behavior remains the same when the direction oftime is reversed. We bridge these two theories of reversibility by showing theconditions under which causal reversibility and time reversibility are bothensured by construction. This is done in the setting of a stochastic processcalculus, which is then equipped with a variant of stochastic bisimilarityaccounting for both forward and backward directions