Episciences.org
Not a member yet
6707 research outputs found
Sort by
Multiparty testing preorders
No full textVariants of the must testing approach have been successfully applied inservice oriented computing for analysing the compliance between (contractsexposed by) clients and servers or, more generally, between two peers. It hashowever been argued that multiparty scenarios call for more permissive notionsof compliance because partners usually do not have full coordinationcapabilities. We propose two new testing preorders, which are obtained byrestricting the set of potential observers. For the first preorder, calleduncoordinated, we allow only sets of parallel observers that use differentparts of the interface of a given service and have no possibility ofintercommunication. For the second preorder, that we call individualistic, weinstead rely on parallel observers that perceive as silent all the actions thatare not in the interface of interest. We have that the uncoordinated preorderis coarser than the classical must testing preorder and finer than theindividualistic one. We also provide a characterisation in terms of decoratedtraces for both preorders: the uncoordinated preorder is defined in terms ofmust-sets and Mazurkiewicz traces while the individualistic one is described interms of classes of filtered traces that only contain designated visibleactions and must-sets
Revisiting Decidable Bounded Quantification, via Dinaturality
No full textWe use a semantic interpretation to investigate the problem of defining anexpressive but decidable type system with bounded quantification. Typecheckingin the widely studied System Fsub is undecidable thanks to an undecidablesubtyping relation, for which the culprit is the rule for subtyping boundedquantification. Weaker versions of this rule, allowing decidable subtyping,have been proposed. One of the resulting type systems (Kernel Fsub) lacksexpressiveness, another (System Fsubtop) lacks the minimal typing property andthus has no evident typechecking algorithm. We consider these rules as defining distinct forms of bounded quantification,one for interpreting type variable abstraction, and the other for typeinstantiation. By giving a semantic interpretation for both in terms ofunbounded quantification, using the dinaturality of type instantiation withrespect to subsumption, we show that they can coexist within a single typesystem. This does have the minimal typing property and thus a simpletypechecking procedure. We consider the fragments of this unified type system over types whichcontain only one form of bounded quantifier. One of these is equivalent toKernel Fsub, while the other can type strictly more terms than System Fsubtopbut the same set of beta-normal terms. We show decidability of typechecking forthis fragment, and thus for System Fsubtop typechecking of beta-normal terms.Comment: In Mathematical Semantics of Programming Languages (MFPS) '2
L’autopraxéographie, une méthode pour construire des savoirs à partir de son expérience dans une perspective complexe et interdisciplinaire
No full textThe objective of this paper is to explain autopraxeography and to show how this method uses interdisciplinarity to understand lived situations in a complex way. This method is based on the human experience of at least one of the co-researchers. It is situated in a pragmatic co-constructivist epistemological paradigm. It uses a wide range of theories, regardless of their original disciplines, to step back from the lived experience. It is a dialogue between the lived experience and each point of view that can be found through multidisciplinary scientific writings, co-researchers, reviewers, etc. The fact of digging into one's own experiences without being locked into a discipline can allow one to answer disciplinary questions in a way that accepts the complexity of the lived reality. Furthermore, this method, when used by students in a continuing education, process can facilitate their opportunity to become reflective practitioners aware of the need to break down disciplinary barriers.L'objectif de cet article est d'expliquer l'autopraxeographie et de montrer comment cette méthode utilise l'interdisciplinarité pour appréhender de manière complexe les situations vécues. Cette méthode, illustrée par un exemple où elle a été utilisée, est basée sur l'expérience humaine d'au moins un des cochercheurs. Elle se situe dans un paradigme épistémologique coconstructiviste pragmatique. Elle utilise un large spectre de théories quelles que soient leurs disciplines originelles pour prendre du recul sur l'expérience vécue. Il s'agit d'un dialogue reliant le vécu, et chaque point de vue que l'on retrouve via des écrits scientifiques pluridisciplinaires, des cochercheurs, des reviewers,… Le fait de creuser ses propres expériences sans s'enfermer dans une discipline peut permettre de répondre à des questionnements disciplinaires de façon à accepter la complexité de la réalité du vécu. De plus, cette méthode, quand elle est utilisée par des étudiants dans un processus de formation continue, peut permettre de faciliter leur possibilité de devenir des praticiens réflexifs conscients de la nécessité de briser les barrières disciplinaires
One-step closure, weak one-step closure and meet continuity
No full textThis paper studies the weak one-step closure and one-step closure propertiesconcerning the structure of Scott closures. We deduce that everyquasicontinuous domain has weak one-step closure and show that aquasicontinuous poset need not have weak one-step closure. We also constructeda non-continuous poset with one-step closure, which gives a negative answer toan open problem posed by Zou et al.. Finally, we investigate the relationshipbetween weak one-step closure property and one-step closure property and provethat a poset has one-step closure if and only if it is meet continuous and hasweak one-step closure
On the Convergence of Random Fourier-Jacobi Series of Continuous functions
No full textThe interest in orthogonal polynomials and random Fourier series in numerousbranches of science and a few studies on random Fourier series in orthogonalpolynomials inspired us to focus on random Fourier series in Jacobipolynomials. In the present note, an attempt has been made to investigate thestochastic convergence of some random Jacobi series. We looked into the randomseries in orthogonalpolynomials with random variables The randomcoefficients are the Fourier-Jacobi coefficients of continuousstochastic processes such as symmetric stable process and Wiener process. The are chosen to be the Jacobi polynomials and their variantsdepending on the random variables associated with the kind of stochasticprocess. The convergence of random series is established for differentparameters of the Jacobi polynomials with corresponding choiceof the scalars which are Fourier-Jacobi coefficients of a suitable classof continuous functions. The sum functions of the random Fourier-Jacobi seriesassociated with continuous stochastic processes are observed to be thestochastic integrals. The continuity properties of the sum functions are alsodiscussed.Comment: 13 page
Rewriting with Acyclic Queries: Mind Your Head
No full textThe paper studies the rewriting problem, that is, the decision problemwhether, for a given conjunctive query and a set of views,there is a conjunctive query over that is equivalent to ,for cases where the query, the views, and/or the desired rewriting are acyclicor even more restricted. It shows that, if itself is acyclic, an acyclicrewriting exists if there is any rewriting. An analogous statement also holdsfor free-connex acyclic, hierarchical, and q-hierarchical queries. Regardingthe complexity of the rewriting problem, the paper identifies a border betweentractable and (presumably) intractable variants of the rewriting problem: forschemas of bounded arity, the acyclic rewriting problem is NP-hard, even ifboth and the views in are acyclic or hierarchical. However,it becomes tractable if the views are free-connex acyclic (i.e., in a nutshell,their body is (i) acyclic and (ii) remains acyclic if their head is added as anadditional atom)
(k − 2)-linear connected components in hypergraphs of rank k
No full textWe define a q-linear path in a hypergraph H as a sequence (e_1,...,e_L) of edges of H such that |e_i ∩ e_i+1 | ∈ [[1, q]] and e_i ∩ e_j = ∅ if |i − j| > 1. In this paper, we study the connected components associated to these paths when q = k − 2 where k is the rank of H. If k = 3 then q = 1 which coincides with the well-known notion of linear path or loose path. We describe the structure of the connected components, using an algorithmic proof which shows that the connected components can be computed in polynomial time. We then mention two consequences of our algorithmic result. The first one is that deciding the winner of the Maker-Breaker game on a hypergraph of rank 3 can be done in polynomial time. The second one is that tractable cases for the NP-complete problem of "Paths Avoiding Forbidden Pairs" in a graph can be deduced from the recognition of a special type of line graph of a hypergraph
Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
No full textA classic result in formal language theory is the equivalence amongnon-counting, or aperiodic, regular languages, and languages defined throughstar-free regular expressions, or first-order logic. Past attempts to extendthis result beyond the realm of regular languages have met with difficulties:for instance it is known that star-free tree languages may violate thenon-counting property and there are aperiodic tree languages that cannot bedefined through first-order logic. We extend such classic equivalence resultsto a significant family of deterministic context-free languages, theoperator-precedence languages (OPL), which strictly includes the widelyinvestigated visibly pushdown, alias input-driven, family and other structuredcontext-free languages. The OP model originated in the '60s for definingprogramming languages and is still used by high performance compilers; its richalgebraic properties have been investigated initially in connection withgrammar learning and recently completed with further closure properties andwith monadic second order logic definition. We introduce an extension ofregular expressions, the OP-expressions (OPE) which define the OPLs and, underthe star-free hypothesis, define first-order definable and non-counting OPLs.Then, we prove, through a fairly articulated grammar transformation, thataperiodic OPLs are first-order definable. Thus, the classic equivalence ofstar-freeness, aperiodicity, and first-order definability is established forthe large and powerful class of OPLs. We argue that the same approach can beexploited to obtain analogous results for visibly pushdown languages too
Geometrical description of equations related to the E8 affine Weyl group
No full textWe present a method for the construction of the trajectory of a discrete Painlev\'e equation associated with the affine Weyl group E on the weight lattice of said group. The method is based on the geometrical description of the lattice and the construction of the fundamental Miura relation. To this end we introduce the relation between the nonlinear variables and the corresponding functions. Our approach is heuristic and makes use of some simple rules of thumb in order to derive the result. Once the latter is obtained, verifying that it does indeed correspond to the equation at hand is elementary. We apply our approach to the explicit construction of the trajectory of well-known, E associated, discrete Painlev\'e equations derived in previous works of ours. For each of them we investigate the possibility of defining an evolution by periodically skipping up to four intermediate points in the trajectory and identifying the resulting equation to one previously obtained, whenever the latter exists
Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
No full textWe apply program verification technology to the problem of specifying andverifying automatic differentiation (AD) algorithms. We focus on define-by-run,a style of AD where the program that must be differentiated is executed andmonitored by the automatic differentiation algorithm. We begin by asking, "whatis an implementation of AD?" and "what does it mean for an implementation of ADto be correct?" We answer these questions both at an informal level, in preciseEnglish prose, and at a formal level, using types and logical assertions. Afteranswering these broad questions, we focus on a specific implementation of AD,which involves a number of subtle programming-language features, includingdynamically allocated mutable state, first-class functions, and effecthandlers. We present a machine-checked proof, expressed in a modern variant ofSeparation Logic, of its correctness. We view this result as an advancedexercise in program verification, with potential future applications to theverification of more realistic automatic differentiation systems and of othersoftware components that exploit delimited-control effects