-
Scoped Effects as Parameterized Algebraic Theories
Authors:
Cristina Matache,
Sam Lindley,
Sean Moss,
Sam Staton,
Nicolas Wu,
Zhixuan Yang
Abstract:
Notions of computation can be modelled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equivalent expressions. However, many useful programming features depend on additional mechanisms such as delimited scopes…
▽ More
Notions of computation can be modelled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equivalent expressions. However, many useful programming features depend on additional mechanisms such as delimited scopes or dynamically allocated resources. Such mechanisms can be supported via extensions to algebraic effects including scoped effects and parameterized algebraic theories. We present a fresh perspective on scoped effects by translation into a variation of parameterized algebraic theories. The translation enables a new approach to equational reasoning for scoped effects and gives rise to an alternative characterization of monads in terms of generators and equations involving both scoped and algebraic operations. We demonstrate the power of our fresh perspective by way of equational characterizations of several known models of scoped effects.
△ Less
Submitted 20 May, 2024; v1 submitted 5 February, 2024;
originally announced February 2024.
-
Denotational semantics for languages for inference: semirings, monads, and tensors
Authors:
Cristina Matache,
Sean Moss,
Sam Staton,
Ariadne Si Suo
Abstract:
Computational effects are commonly modelled by monads, but often a monad can be presented by an algebraic theory of operations and equations. This talk is about monads and algebraic theories for languages for inference, and their connections to semirings and tensors.
A basic class of examples of algebraic theories comes from considering the theory of modules for a semiring, e.g. the theory of un…
▽ More
Computational effects are commonly modelled by monads, but often a monad can be presented by an algebraic theory of operations and equations. This talk is about monads and algebraic theories for languages for inference, and their connections to semirings and tensors.
A basic class of examples of algebraic theories comes from considering the theory of modules for a semiring, e.g. the theory of unnormalized distributions, where the semiring is that of the non-negative real numbers. We propose that an interesting perspective is given by studying theories via semirings, and to this end explore several examples of subtheories of module theories, mostly relating to probability. Our main contribution concerns the commutative combination of effects, as studied by Hyland, Plotkin and Power: we observe that while the semiring tensor does not in general determine the tensor of subtheories of module theories, it still does in several fundamental probabilistic examples.
△ Less
Submitted 27 December, 2023;
originally announced December 2023.
-
Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction)
Authors:
Cristina Matache,
Sean Moss,
Sam Staton
Abstract:
We study concrete sheaf models for a call-by-value higher-order language with recursion. Our family of sheaf models is a generalization of many examples from the literature, such as models for probabilistic and differentiable programming, and fully abstract logical relations models. We treat recursion in the spirit of synthetic domain theory. We provide a general construction of a lifting monad st…
▽ More
We study concrete sheaf models for a call-by-value higher-order language with recursion. Our family of sheaf models is a generalization of many examples from the literature, such as models for probabilistic and differentiable programming, and fully abstract logical relations models. We treat recursion in the spirit of synthetic domain theory. We provide a general construction of a lifting monad starting from a class of admissible monomorphisms in the site of the sheaf category. In this way, we obtain a family of models parametrized by a concrete site and a class of monomorphisms, for which we prove a general computational adequacy theorem.
△ Less
Submitted 31 May, 2022;
originally announced May 2022.
-
A Light-Weight Multi-Objective Asynchronous Hyper-Parameter Optimizer
Authors:
Gabriel Maher,
Stephen Boyd,
Mykel Kochenderfer,
Cristian Matache,
Dylan Reuter,
Alex Ulitsky,
Slava Yukhymuk,
Leonid Kopman
Abstract:
We describe a light-weight yet performant system for hyper-parameter optimization that approximately minimizes an overall scalar cost function that is obtained by combining multiple performance objectives using a target-priority-limit scalarizer. It also supports a trade-off mode, where the goal is to find an appropriate trade-off among objectives by interacting with the user. We focus on the comm…
▽ More
We describe a light-weight yet performant system for hyper-parameter optimization that approximately minimizes an overall scalar cost function that is obtained by combining multiple performance objectives using a target-priority-limit scalarizer. It also supports a trade-off mode, where the goal is to find an appropriate trade-off among objectives by interacting with the user. We focus on the common scenario where there are on the order of tens of hyper-parameters, each with various attributes such as a range of continuous values, or a finite list of values, and whether it should be treated on a linear or logarithmic scale. The system supports multiple asynchronous simulations and is robust to simulation stragglers and failures.
△ Less
Submitted 7 September, 2022; v1 submitted 15 February, 2022;
originally announced February 2022.
-
Recursion and Sequentiality in Categories of Sheaves
Authors:
Cristina Matache,
Sean Moss,
Sam Staton
Abstract:
We present a fully abstract model of a call-by-value language with higher-order functions, recursion and natural numbers, as an exponential ideal in a topos. Our model is inspired by the fully abstract models of O'Hearn, Riecke and Sandholm, and Marz and Streicher. In contrast with semantics based on cpo's, we treat recursion as just one feature in a model built by combining a choice of modular co…
▽ More
We present a fully abstract model of a call-by-value language with higher-order functions, recursion and natural numbers, as an exponential ideal in a topos. Our model is inspired by the fully abstract models of O'Hearn, Riecke and Sandholm, and Marz and Streicher. In contrast with semantics based on cpo's, we treat recursion as just one feature in a model built by combining a choice of modular components.
△ Less
Submitted 5 May, 2021;
originally announced May 2021.
-
Program Equivalence for Algebraic Effects via Modalities
Authors:
Cristina Matache
Abstract:
This dissertation is concerned with the study of program equivalence and algebraic effects as they arise in the theory of programming languages. Algebraic effects represent impure behaviour in a functional programming language, such as input and output, exceptions, nondeterminism etc. all treated in a generic way. Program equivalence aims to identify which programs can be considered equal in some…
▽ More
This dissertation is concerned with the study of program equivalence and algebraic effects as they arise in the theory of programming languages. Algebraic effects represent impure behaviour in a functional programming language, such as input and output, exceptions, nondeterminism etc. all treated in a generic way. Program equivalence aims to identify which programs can be considered equal in some sense. This question has been studied for a long time but has only recently been extended to languages with algebraic effects, which are a newer development. Much work remains to be done in order to understand program equivalence in the presence of algebraic effects. In particular, there is no characterisation of contextual equivalence using a logic. We define a logic whose formulas express properties of higher-order programs with algebraic effects. We then investigate three notions of program equivalence for algebraic effects: logical equivalence induced by the aforementioned logic, applicative bisimilarity and contextual equivalence. For the programming language used in this dissertation, we prove that they all coincide. Therefore, the main novel contribution of the dissertation is defining the first logic for algebraic effects whose induced program equivalence coincides with contextual equivalence.
△ Less
Submitted 12 February, 2019;
originally announced February 2019.
