Episciences.org
Not a member yet
6707 research outputs found
Sort by
A Complete V-Equational System for Graded lambda-Calculus
No full textModern programming frequently requires generalised notions of programequivalence based on a metric or a similar structure. Previous work addressedthis challenge by introducing the notion of a V-equation, i.e. an equationlabelled by an element of a quantale V, which covers inter alia (ultra-)metric,classical, and fuzzy (in)equations. It also introduced a V-equational systemfor the linear variant of lambda-calculus where any given resource must be usedexactly once. In this paper we drop the (often too strict) linearity constraint by addinggraded modal types which allow multiple uses of a resource in a controlledmanner. We show that such a control, whilst providing more expressivity to theprogrammer, also interacts more richly with V-equations than the linear orCartesian cases. Our main result is the introduction of a sound and completeV-equational system for a lambda-calculus with graded modal types interpretedby what we call a Lipschitz exponential comonad. We also show how to build suchcomonads canonically via a universal construction, and use our results toderive graded metric equational systems (and corresponding models) for programswith timed and probabilistic behaviour.Comment: Conference paper accepted at MFPS'23. Omitted proofs can be found in arXiv:2304.02082v
Dissecting power of intersection of two context-free languages
No full textWe say that a language is \emph{constantly growing} if there is aconstant such that for every word there is a word with. We say that a language is\emph{geometrically growing} if there is a constant such that for everyword there is a word with \vert u\vert<\vert v\vert\leqc\vert u\vert. Given two infinite languages , we say that \emph{dissects} if and \vertL_1\cap L_2\vert=\infty. In 2013, it was shown that for every constantlygrowing language there is a regular language such that dissects. In the current article we show how to dissect a geometrically growinglanguage by a homomorphic image of intersection of two context-free languages. Consider three alphabets , , and such that and . We prove that there are context-freelanguages , an erasing alphabetical homomorphism, and a nonerasing alphabetical homomorphism such that: If isa geometrically growing language then there is a regular language such that \varphi^{-1}\left(\pi\left(R\cap M_1\capM_2\right)\right) dissects the language
A model of stochastic memoization and name generation in probabilistic programming: categorical semantics via monads on presheaf categories
No full textStochastic memoization is a higher-order construct of probabilisticprogramming languages that is key in Bayesian nonparametrics, a modularapproach that allows us to extend models beyond their parametric limitationsand compose them in an elegant and principled manner. Stochastic memoization issimple and useful in practice, but semantically elusive, particularly regardingdataflow transformations. As the naive implementation resorts to the statemonad, which is not commutative, it is not clear if stochastic memoizationpreserves the dataflow property -- i.e., whether we can reorder the lines of aprogram without changing its semantics, provided the dataflow graph ispreserved. In this paper, we give an operational and categorical semantics tostochastic memoization and name generation in the context of a minimalprobabilistic programming language, for a restricted class of functions. Ourcontribution is a first model of stochastic memoization of constant Bernoullifunctions with a non-enumerable type, which validates data flowtransformations, bridging the gap between traditional probability theory andhigher-order probability models. Our model uses a presheaf category and a novelprobability monad on it.Comment: To be published in the MFPS 2023 Proceedings as part of the Electronic Notes in Theoretical Informatics and Computer Science (ENTICS) serie
Cartesian Differential Kleisli Categories
No full textCartesian differential categories come equipped with a differentialcombinator which axiomatizes the fundamental properties of the total derivativefrom differential calculus. The objective of this paper is to understand whenthe Kleisli category of a monad is a Cartesian differential category. Weintroduce Cartesian differential monads, which are monads whose Kleislicategory is a Cartesian differential category by way of lifting thedifferential combinator from the base category. Examples of Cartesiandifferential monads include tangent bundle monads and reader monads. We give aprecise characterization of Cartesian differential categories which are Kleislicategories of Cartesian differential monads using abstract Kleisli categories.We also show that the Eilenberg-Moore category of a Cartesian differentialmonad is a tangent category.Comment: For the proceedings of MFPS202
Optimal Control of a Viscous Two-Field Damage Model with Fatigue
No full textMotivated by fatigue damage models, this paper addresses optimal control problems governed by a non-smooth system featuring two non-differentiable mappings. This consists of a coupling between a doubly non-smooth history-dependent evolution and an elliptic PDE. After proving the directional differentiability of the associated solution mapping, an optimality system which is stronger than the one obtained by classical smoothening procedures is derived. If one of the non-differentiable mappings becomes smooth, the optimality conditions are of strong stationary type, i.e., equivalent to the primal necessary optimality condition
The Complexity of Aggregates over Extractions by Regular Expressions
No full textRegular expressions with capture variables, also known as regex-formulas,extract relations of spans (intervals identified by their start and endindices) from text. In turn, the class of regular document spanners is theclosure of the regex formulas under the Relational Algebra. We investigate thecomputational complexity of querying text by aggregate functions, such as sum,average, and quantile, on top of regular document spanners. To this end, weformally define aggregate functions over regular document spanners and analyzethe computational complexity of exact and approximate computation. Moreprecisely, we show that in a restricted case, all studied aggregate functionscan be computed in polynomial time. In general, however, even though exactcomputation is intractable, some aggregates can still be approximated withfully polynomial-time randomized approximation schemes (FPRAS)
The integer point transform as a complete invariant
No full textThe integer point transform \sigma_\PP is an important invariant of arational polytope \PP, and here we show that it is a complete invariant. Weprove that it is only necessary to evaluate \sigma_\PP at one algebraic pointin order to uniquely determine \PP, by employing the Lindemann-Weierstrasstheorem. Similarly, we prove that it is only necessary to evaluate the Fouriertransform of a rational polytope \PP at a single algebraic point, in order touniquely determine \PP. We prove that identical uniqueness results also holdfor integer cones. In addition, by relating the integer point transform to finite Fouriertransforms, we show that a finite number of \emph{integer point evaluations} of\sigma_\PP suffice in order to uniquely determine \PP. We also give anequivalent condition for central symmetry of a finite point set, in terms ofthe integer point transform, and prove some facts about its local maxima. Mostof the results are proven for arbitrary finite sets of integer points in.Comment: 16 pages, 3 figure
Positive First-order Logic on Words and Graphs
No full textWe study FO+, a fragment of first-order logic on finite words, where monadicpredicates can only appear positively. We show that there is an FO-definablelanguage that is monotone in monadic predicates but not definable in FO+. Thisprovides a simple proof that Lyndon's preservation theorem fails on finitestructures. We lift this example language to finite graphs, thereby providing anew result of independent interest for FO-definable graph classes: negationmight be needed even when the class is closed under addition of edges. Wefinally show that the problem of whether a given regular language of finitewords is definable in FO+ is undecidable.Comment: arXiv admin note: substantial text overlap with arXiv:2101.0196
On Presburger arithmetic extended with non-unary counting quantifiers
No full textWe consider a first-order logic for the integers with addition. This logicextends classical first-order logic by modulo-counting, threshold-counting andexact-counting quantifiers, all applied to tuples of variables (here, residuesare given as terms while moduli and thresholds are given explicitly). Our mainresult shows that satisfaction for this logic is decidable in two-foldexponential space. If only threshold- and exact-counting quantifiers areallowed, we prove an upper bound of alternating two-fold exponential time withlinearly many alternations. This latter result almost matches Berman's exactcomplexity of first-order logic without counting quantifiers. To obtain these results, we first translate threshold- and exact-countingquantifiers into classical first-order logic in polynomial time (which alreadyproves the second result). To handle the remaining modulo-counting quantifiersfor tuples, we first reduce them in doubly exponential time to modulo-countingquantifiers for single elements. For these quantifiers, we provide a quantifierelimination procedure similar to Reddy and Loveland's procedure for first-orderlogic and analyse the growth of coefficients, constants, and moduli appearingin this process. The bounds obtained this way allow to restrict quantificationin the original formula to integers of bounded size which then implies thefirst result mentioned above. Our logic is incomparable with the logic considered by Chistikov et al. in2022. They allow more general counting operations in quantifiers, but onlyunary quantifiers. The move from unary to non-unary quantifiers is non-trivial,since, e.g., the non-unary version of the H\"artig quantifier results in anundecidable theory
Finiteness for self-dual classes in integral variations of Hodge structure
No full textWe generalize the finiteness theorem for the locus of Hodge classes withfixed self-intersection number, due to Cattani, Deligne, and Kaplan, from Hodgeclasses to self-dual classes. The proof uses the definability of periodmappings in the o-minimal structure .Comment: v3: final versio