1,720,976 research outputs found
Allegories of Symbolic Manipulations
Full text linkMoving from the mathematical theory of (abstract) syntax, we develop a general relational theory of symbolic manipulation parametric with respect to, and accounting for, general notions of syntax. We model syntax relying on categorical notions, such as free algebras and monads, and show that a general theory of symbolic manipulation in the style of rewriting systems can be obtained by extending such notions to an allegorical setting. This way, we obtain an augmented calculus of relations accounting for syntax-based rewriting. We witness the effectiveness of the relational approach by generalising and unifying milestones results in rewriting, such as the parallel moves and the TaitMartin-Lof techniques
Effectful Normal Form Bisimulation
No full textNormal form bisimulation, also known as open bisimulation, is a coinductive technique for higher-order program equivalence in which programs are compared by looking at their essentially infinitary tree-like normal forms, i.e. at their Böhm or Lévy-Longo trees. The technique has been shown to be useful not only when proving metatheorems about ⋋-calculi and their semantics, but also when looking at concrete examples of terms. In this paper, we show that there is a way to generalise normal form bisimulation to calculi with algebraic effects, à la Plotkin and Power. We show that some mild conditions on monads and relators, which have already been shown to guarantee effectful applicative bisimilarity to be a congruence relation, are enough to prove that the obtained notion of bisimilarity, which we call effectful normal form bisimilarity, is a congruence relation, and thus sound for contextual equivalence. Additionally, contrary to applicative bisimilarity, normal form bisimilarity allows for enhancements of the bisimulation proof method, hence proving a powerful reasoning principle for effectful programming languages
Differential logical relations, part II increments and derivatives
Full text linkWe study the deep relation existing between differential logical relations and incremental computing by showing how self-differences in the former precisely correspond to derivatives in the latter. The byproduct of such a relationship is twofold: on the one hand, we show how differential logical relations can be seen as a powerful meta-theoretical tool in the analysis of incremental computations, enabling an easy proof of soundness of differentiation. On the other hand, we generalize differential logical relations so as to be able to interpret full recursion, something not possible in the original system
A relational theory of effects and coeffects
Full text linkGraded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent, usage-sensitive computations, especially when combined with computational effects. From a semantic perspective, effectful and coeffectful languages have been studied mostly by means of denotational semantics and almost nothing has been done from the point of view of relational reasoning. This gap in the literature is quite surprising, since many cornerstone results-such as non-interference, metric preservation, and proof irrelevance-on concrete coeffects are inherently relational. In this paper, we fill this gap by developing a general theory and calculus of program relations for higher-order languages with combined effects and coeffects the relational calculus builds upon the novel notion of a corelator (or comonadic lax extension) to handle coeffects relationally. Inside such a calculus, we define three notions of effectful and coeffectful program refinements: contextual approximation, logical preorder, and applicative similarity these are the first operationally-based notions of program refinement (and, consequently, equivalence) for languages with combined effects and coeffects appearing in the literature. We show that the axiomatics of a corelator (together with the one of a relator) is precisely what is needed to prove all the aforementioned program refinements to be precongruences, this way obtaining compositional relational techniques for reasoning about combined effects and coeffects
Effectful program distancing
Full text linkSemantics is traditionally concerned with program equivalence, in which all pairs of programs which are not equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program metrics have been introduced such that the distance between non-equivalent programs is measured as an element of an appropriate quantale. By letting the underlying quantale vary as the type of the compared programs become more complex, the recently introduced framework of differential logical relations allows for a new contextual form of reasoning. In this paper, we show that all this can be generalised to effectful higher-order programs, in which not only the values, but also the effects computations produce can be appropriately distanced in a principled way. We show that the resulting framework is flexible, allowing various forms of effects to be handled, and that it provides compact and informative judgments about program differences
Elements of Quantitative Rewriting
Full text linkWe introduce a general theory of quantitative and metric rewriting systems, namely systems with a rewriting relation enriched over quantales modelling abstract quantities. We develop theories of abstract and term-based systems, refining cornerstone results of rewriting theory (such as Newman's Lemma, Church-Rosser Theorem, and critical pair-like lemmas) to a metric and quantitative setting. To avoid distance trivialisation and lack of confluence issues, we introduce non-expansive, linear term rewriting systems, and then generalise the latter to the novel class of graded term rewriting systems. These systems make quantitative rewriting modal and context-sensitive, this way endowing rewriting with coeffectful behaviours
Resource transition systems and full abstraction for linear higher-order effectful programs
Full text linkWe investigate program equivalence for linear higher-order (sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear γ-calculus with explicit copying and algebraic effects à la Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, extensional. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviours of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems
Effectful applicative similarity for call-by-name lambda calculi
Full text linkWe introduce a notion of applicative similarity in which not terms but monadic values arising from the evaluation of effectful terms, can be compared. We prove this notion to be fully abstract whenever terms are evaluated in call-by-name order. This is the first full-abstraction result for such a generic, coinductive methodology for program equivalence
Monadic Intersection Types, Relationally
No full textWe extend intersection types to a computational.-calculus with algebraic operations a la Plotkin and Power. We achieve this by considering monadic intersections-whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting
- …
