Showing 1–50 of 89 results for author: Lago, U D

On Separation Logic, Computational Independence, and Pseudorandomness (Extended Version)

Authors: Ugo Dal Lago, Davide Davoli, Bruce M. Kapron

Abstract: Separation logic is a substructural logic which has proved to have numerous and fruitful applications to the verification of programs working on dynamic data structures. Recently, Barthe, Hsu and Liao have proposed a new way of giving semantics to separation logic formulas in which separating conjunction is interpreted in terms of probabilistic independence. The latter is taken in its exact form,… ▽ More Separation logic is a substructural logic which has proved to have numerous and fruitful applications to the verification of programs working on dynamic data structures. Recently, Barthe, Hsu and Liao have proposed a new way of giving semantics to separation logic formulas in which separating conjunction is interpreted in terms of probabilistic independence. The latter is taken in its exact form, i.e., two events are independent if and only if the joint probability is the product of the probabilities of the two events. There is indeed a literature on weaker notions of independence which are computational in nature, i.e. independence holds only against efficient adversaries and modulo a negligible probability of success. The aim of this work is to explore the nature of computational independence in a cryptographic scenario, in view of the aforementioned advances in separation logic. We show on the one hand that the semantics of separation logic can be adapted so as to account for complexity bounded adversaries, and on the other hand that the obtained logical system is useful for writing simple and compact proofs of standard cryptographic results in which the adversary remains hidden. Remarkably, this allows for a fruitful interplay between independence and pseudorandomness, itself a crucial notion in cryptography. △ Less

Submitted 20 May, 2024; originally announced May 2024.

Comments: to be published in CSF'24

On Basic Feasible Functionals and the Interpretation Method

Authors: Patrick Baillot, Ugo Dal Lago, Cynthia Kop, Deivid Vale

Abstract: The class of basic feasible functionals $(\mathtt{BFF})$ is the analog of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. $\mathtt{BFF}$ can be defined through Oracle Turing machines with running time bounded by second-order polynomials. On the other hand, higher-order term rewriting provides an elegant form… ▽ More The class of basic feasible functionals $(\mathtt{BFF})$ is the analog of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. $\mathtt{BFF}$ can be defined through Oracle Turing machines with running time bounded by second-order polynomials. On the other hand, higher-order term rewriting provides an elegant formalism for expressing higher-order computation. We address the problem of characterizing $\mathtt{BFF}$ by higher-order term rewriting. Various kinds of interpretations for first-order term rewriting have been introduced in the literature for proving termination and characterizing (first-order) complexity classes. In this paper, we consider a recently introduced notion of cost-size interpretations for higher-order term rewriting and see definitions as ways of computing functionals. We then prove that the class of functionals represented by higher-order terms admitting a certain kind of cost-size interpretation is exactly $\mathtt{BFF}$. △ Less

Submitted 25 January, 2024; v1 submitted 22 January, 2024; originally announced January 2024.

ACM Class: F.1.3

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories

Authors: Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, Paolo Pistone

Abstract: We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory à la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sens… ▽ More We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory à la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPP_T and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in the theory T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPP_T where T=$\mathrm{I}Δ_0+\mathrm{Exp}$ is a well-studied theory based on bounded induction. △ Less

Submitted 25 November, 2023; originally announced November 2023.

ACM Class: F.4.1; F.1.3

Circuit Width Estimation via Effect Ty** and Linear Dependency (Long Version)

Authors: Andrea Colledan, Ugo Dal Lago

Abstract: Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, w… ▽ More Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present Proto-Quipper-R, a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. We also show that our approach is expressive enough to verify realistic quantum algorithms. △ Less

Submitted 31 October, 2023; v1 submitted 29 October, 2023; originally announced October 2023.

Comments: 21 pages (excluding references), 21 figures

ACM Class: D.3.1; F.3.1; D.2.4

On Model-Checking Higher-Order Effectful Programs (Long Version)

Authors: Ugo Dal Lago, Alexis Ghyselen

Abstract: Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be applicable to functional programs with higher-order types against properties expressed by formulas of monadic second-order logic. What happens when the program in question, in addition to higher-order functions, also exhib… ▽ More Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be applicable to functional programs with higher-order types against properties expressed by formulas of monadic second-order logic. What happens when the program in question, in addition to higher-order functions, also exhibits algebraic effects such as probabilistic choice or global store? The results in the literature range from those, mostly positive, about nondeterministic effects, to those about probabilistic effects, in the presence of which even mere reachability becomes undecidable. This work takes a fresh and general look at the problem, first of all showing that there is an elegant and natural way of viewing higher-order programs producing algebraic effects as ordinary higher-order recursion schemes. We then move on to consider effect handlers, showing that in their presence the model checking problem is bound to be undecidable in the general case, while it stays decidable when handlers have a simple syntactic form, still sufficient to capture so-called generic effects. Along the way we hint at how a general specification language could look like, this way justifying some of the results in the literature, and deriving new ones. △ Less

Submitted 31 August, 2023; originally announced August 2023.

Contextual Behavioural Metrics (Extended Version)

Authors: Ugo Dal Lago, Maurizio Murgia

Abstract: We introduce contextual behavioural metrics (CBMs) as a novel way of measuring the discrepancy in behaviour between processes, taking into account both quantitative aspects and contextual information. This way, process distances by construction take the environment into account: two (non-equivalent) processes may still exhibit very similar behaviour in some contexts, e.g., when certain actions are… ▽ More We introduce contextual behavioural metrics (CBMs) as a novel way of measuring the discrepancy in behaviour between processes, taking into account both quantitative aspects and contextual information. This way, process distances by construction take the environment into account: two (non-equivalent) processes may still exhibit very similar behaviour in some contexts, e.g., when certain actions are never performed. We first show how CBMs capture many well-known notions of equivalence and metric, including Larsen's environmental parametrized bisimulation. We then study compositional properties of CBMs with respect to some common process algebraic operators, namely prefixing, restriction, non-deterministic sum, parallel composition and replication. △ Less

Submitted 5 September, 2023; v1 submitted 14 July, 2023; originally announced July 2023.

Comments: Extended version of a paper accepted for publication in proc. CONCUR 2023

On the Lattice of Program Metrics

Authors: Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone

Abstract: In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the… ▽ More In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i.e., whether and in which cases one such metric refines another, in analogy with corresponding well-studied problems about program equivalences. The results we obtain are twofold. We first show that the metrics of semantic origin, i.e., the denotational and interactive ones, lie \emph{in between} the observational and equational metrics and that in some cases, these inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, revealing that the former is less discriminating than the latter. All our results are given for a linear lambda-calculus, and some of them can be generalized to calculi with graded comonads, in the style of Fuzz. △ Less

Submitted 9 February, 2023; originally announced February 2023.

A Log-Sensitive Encoding of Turing Machines in the $λ$-Calculus

Authors: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

Abstract: This note modifies the reference encoding of Turing machines in the $λ$-calculus by Dal Lago and Accattoli, which is tuned for time efficiency, as to accommodate logarithmic space. There are two main changes: Turing machines now have *two* tapes, an input tape and a work tape, and the input tape is encoded differently, because the reference encoding comes with a linear space overhead for managing… ▽ More This note modifies the reference encoding of Turing machines in the $λ$-calculus by Dal Lago and Accattoli, which is tuned for time efficiency, as to accommodate logarithmic space. There are two main changes: Turing machines now have *two* tapes, an input tape and a work tape, and the input tape is encoded differently, because the reference encoding comes with a linear space overhead for managing tapes, which is excessive for studying logarithmic space. △ Less

Submitted 29 January, 2023; originally announced January 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:2203.00362

An Arithmetic Theory for the Poly-Time Random Functions

Authors: Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, Paolo Pistone

Abstract: We introduce a new bounded theory RS^1_2 and show that the functions which are Sigma^b_1-representable in it are precisely random functions which can be computed in polynomial time. Concretely, we pass through a class of oracle functions over string, called POR, together with the theory of arithmetic RS^1_2. Then, we show that functions computed by poly-time PTMs are arithmetically characterized b… ▽ More We introduce a new bounded theory RS^1_2 and show that the functions which are Sigma^b_1-representable in it are precisely random functions which can be computed in polynomial time. Concretely, we pass through a class of oracle functions over string, called POR, together with the theory of arithmetic RS^1_2. Then, we show that functions computed by poly-time PTMs are arithmetically characterized by a class of probabilistic bounded formulas. △ Less

Submitted 6 February, 2023; v1 submitted 27 January, 2023; originally announced January 2023.

Comments: 37 pages, pre-print

Open Higher-Order Logic (Long Version)

Authors: Ugo Dal Lago, Francesco Gavazzo, Alexis Ghyselen

Abstract: We introduce a variation on Barthe et al.'s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-or… ▽ More We introduce a variation on Barthe et al.'s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-order logic in distinct flavors, and in particular in its relational and local versions, the latter being tailored for situations in which properties hold only in part of the underlying function's domain of definition. △ Less

Submitted 19 November, 2022; v1 submitted 12 November, 2022; originally announced November 2022.

On Feller Continuity and Full Abstraction (Long Version)

Authors: Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo

Abstract: We study the nature of applicative bisimilarity in $λ$-calculi endowed with operators for sampling from continuous distributions. On the one hand, we show that bisimilarity, logical equivalence, and testing equivalence all coincide with contextual equivalence when real numbers can be manipulated only through continuous functions. The key ingredient towards this result is a novel notion of Feller-c… ▽ More We study the nature of applicative bisimilarity in $λ$-calculi endowed with operators for sampling from continuous distributions. On the one hand, we show that bisimilarity, logical equivalence, and testing equivalence all coincide with contextual equivalence when real numbers can be manipulated only through continuous functions. The key ingredient towards this result is a novel notion of Feller-continuity for labelled Markov processes, which we believe of independent interest, being a broad class of LMPs for which coinductive and logically inspired equivalences coincide. On the other hand, we show that if no constraint is put on the way real numbers are manipulated, characterizing contextual equivalence turns out to be hard, and most of the aforementioned notions of equivalence are even unsound. △ Less

Submitted 21 July, 2022; originally announced July 2022.

Multi Types and Reasonable Space (Long Version)

Authors: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

Abstract: Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space… ▽ More Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space used by the Space KAM, capturing into a type system the space complexity of the abstract machine. Additionally, we show how to capture also the time of the Space KAM, which is a reasonable time cost model, via minor changes to the type system. △ Less

Submitted 18 July, 2022; originally announced July 2022.

On Session Ty**, Probabilistic Polynomial Time, and Cryptographic Experiments (Long Version)

Authors: Ugo Dal Lago, Giulia Giusti

Abstract: A system of session types is introduced as induced by a Curry Howard correspondence applied to Bounded Linear Logic, and then extending the thus obtained type system with probabilistic choices and ground types. The obtained system satisfies the expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This ma… ▽ More A system of session types is introduced as induced by a Curry Howard correspondence applied to Bounded Linear Logic, and then extending the thus obtained type system with probabilistic choices and ground types. The obtained system satisfies the expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This makes the system suitable for modelling experiments and proofs from the so-called computational model of cryptography. △ Less

Submitted 7 July, 2022; originally announced July 2022.

On Quantitative Algebraic Higher-Order Theories

Authors: Ugo Dal Lago, Furio Honsell, Marina Lenisa, Paolo Pistone

Abstract: We explore the possibility of extending Mardare et al. quantitative algebras to the structures which naturally emerge from Combinatory Logic and the lambda-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results which clearly delineate to which extent categories of metric spaces c… ▽ More We explore the possibility of extending Mardare et al. quantitative algebras to the structures which naturally emerge from Combinatory Logic and the lambda-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results which clearly delineate to which extent categories of metric spaces can be models of such theories. We conclude by giving several examples of non-trivial higher-order quantitative algebras. △ Less

Submitted 28 April, 2022; originally announced April 2022.

ACM Class: D.3.1; F.3.2; F.4.1

On Reinforcement Learning, Effect Handlers, and the State Monad

Authors: Ugo Dal Lago, Francesco Gavazzo, Alexis Ghyselen

Abstract: We study the algebraic effects and handlers as a way to support decision-making abstractions in functional programs, whereas a user can ask a learning algorithm to resolve choices without implementing the underlying selection mechanism, and give a feedback by way of rewards. Differently from some recently proposed approach to the problem based on the selection monad [Abadi and Plotkin, LICS 2021],… ▽ More We study the algebraic effects and handlers as a way to support decision-making abstractions in functional programs, whereas a user can ask a learning algorithm to resolve choices without implementing the underlying selection mechanism, and give a feedback by way of rewards. Differently from some recently proposed approach to the problem based on the selection monad [Abadi and Plotkin, LICS 2021], we express the underlying intelligence as a reinforcement learning algorithm implemented as a set of handlers for some of these algebraic operations, including those for choices and rewards. We show how we can in practice use algebraic operations and handlers -- as available in the programming language EFF -- to clearly separate the learning algorithm from its environment, thus allowing for a good level of modularity. We then show how the host language can be taken as a lambda-calculus with handlers, this way showing what the essential linguistic features are. We conclude by hinting at how type and effect systems could ensure safety properties, at the same time pointing at some directions for further work. △ Less

Submitted 29 March, 2022; originally announced March 2022.

Curry and Howard Meet Borel

Authors: Melissa Antonelli, Ugo Dal Lago, Paolo Pistone

Abstract: We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event lambda-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. Remarkably, proofs (respectively, types) do not only guarantee that vali… ▽ More We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event lambda-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. Remarkably, proofs (respectively, types) do not only guarantee that validity (respectively, termination) holds, but also reveal the underlying probability. We finally show that by endowing the type system with an intersection operator, one obtains a system precisely capturing the probabilistic behavior of lambda-terms. △ Less

Submitted 21 March, 2022; originally announced March 2022.

ACM Class: F.4.1; F.3.2; D.3.1

Reasonable Space for the $λ$-Calculus, Logarithmically

Authors: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

Abstract: Can the $λ$-calculus be considered a reasonable computational model? Can we use it for measuring the time $\textit{and}$ space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the $λ$-calculus, based on a variant over the Krivine abstract machine. For the first time, this… ▽ More Can the $λ$-calculus be considered a reasonable computational model? Can we use it for measuring the time $\textit{and}$ space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the $λ$-calculus, based on a variant over the Krivine abstract machine. For the first time, this cost model is able to accommodate logarithmic space. Moreover, we study the time behavior of our machine and show how to transport our results to the call-by-value $λ$-calculus. △ Less

Submitted 8 May, 2024; v1 submitted 1 March, 2022; originally announced March 2022.

On Dynamic Lifting and Effect Ty** in Circuit Description Languages (Extended Version)

Authors: Andrea Colledan, Ugo Dal Lago

Abstract: In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, itself modeling the core features of the quantum circuit description languag… ▽ More In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, itself modeling the core features of the quantum circuit description language Quipper. The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting. This is made possible by the introduction of a rich type and effect system in which not only computations, but also the very types are effectful. The main results we give for the introduced language are the classic type soundness results, namely subject reduction and progress. △ Less

Submitted 15 February, 2022; originally announced February 2022.

Comments: 26 pages, 21 figures

Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications

Authors: Ugo Dal Lago, Valeria de Paiva

Abstract: This volume contains a selection of papers presented at Linearity&TLLA 2020, namely the Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, held on June 29-30, 2020 online. (The workshop was supposed to take place in Paris as part of FSCD 2020, but due to the COVID pandemic it was decided not to hold the event live.) Linearity is a central concept in many th… ▽ More This volume contains a selection of papers presented at Linearity&TLLA 2020, namely the Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, held on June 29-30, 2020 online. (The workshop was supposed to take place in Paris as part of FSCD 2020, but due to the COVID pandemic it was decided not to hold the event live.) Linearity is a central concept in many theoretical and practical approaches to computer science. On the theoretical side, there is much work stemming from linear logic and dealing with resource control, complexity classes, and more recently quantum computation. On the practical side there is certainly work on program analysis, operational semantics, logic programming languages, program transformations, and efficient implementation techniques. Linear logic is not only a theoretical tool for the analysis of resource usage in logic and computation. It is also a corpus of distinct approaches and methodologies (e.g., proof nets, geometry of interaction, coherent spaces, relational models) that were originally developed for the study of linear logic's syntax and semantics have nowadays found applications in several other fields. △ Less

Submitted 28 December, 2021; originally announced December 2021.

Journal ref: EPTCS 353, 2021

Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Systems

Authors: Ugo Dal Lago, Francesco Gavazzo

Abstract: We 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 \emph{à la} Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are… ▽ More We 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 \emph{à 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, \emph{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 behaviors of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems. △ Less

Submitted 24 June, 2021; originally announced June 2021.

The Space of Interaction (long version)

Authors: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

Abstract: The space complexity of functional programs is not well understood. In particular, traditional implementation techniques are tailored to time efficiency, and space efficiency induces time inefficiencies, as it prefers re-computing to saving. Girard's geometry of interaction underlies an alternative approach based on the interaction abstract machine (IAM), claimed as space efficient in the literatu… ▽ More The space complexity of functional programs is not well understood. In particular, traditional implementation techniques are tailored to time efficiency, and space efficiency induces time inefficiencies, as it prefers re-computing to saving. Girard's geometry of interaction underlies an alternative approach based on the interaction abstract machine (IAM), claimed as space efficient in the literature. It has also been conjectured to provide a reasonable notion of space for the lambda-calculus, but such an important result seems to be elusive. In this paper we introduce a new intersection type system precisely measuring the space consumption of the IAM on the typed term. Intersection types have been repeatedly used to measure time, which they achieve by drop** idempotency, turning intersections into multisets. Here we show that the space consumption of the IAM is connected to a further structural modification, turning multisets into trees. Tree intersection types lead to a finer understanding of some space complexity results from the literature. They also shed new light on the conjecture about reasonable space: we show that the usual way of encoding Turing machines into the lambda calculus cannot be used to prove that the space of the IAM is a reasonable cost model. △ Less

Submitted 28 April, 2021; originally announced April 2021.

On Measure Quantifiers in First-Order Arithmetic (Long Version)

Authors: Melissa Antonelli, Ugo Dal Lago, Paolo Pistone

Abstract: We study the logic obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This new kind of quantification allows us to express that the argument formula is true in a certain portion of all possible interpretations of the quantified variable. We show that first-order arithmetic with measure quantifiers is capable of formalizing simple results from probabi… ▽ More We study the logic obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This new kind of quantification allows us to express that the argument formula is true in a certain portion of all possible interpretations of the quantified variable. We show that first-order arithmetic with measure quantifiers is capable of formalizing simple results from probability theory and, most importantly, of representing every recursive random function. Moreover, we introduce a realizability interpretation of this logic in which programs have access to an oracle from the Cantor space. △ Less

Submitted 25 April, 2021; originally announced April 2021.

ACM Class: F.1.1; F.1.2; F.4.1

On Counting Propositional Logic

Authors: Melissa Antonelli, Ugo Dal Lago, Paolo Pistone

Abstract: We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagner's counting hierarchy, but also that the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is deriv… ▽ More We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagner's counting hierarchy, but also that the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science. △ Less

Submitted 3 June, 2021; v1 submitted 23 March, 2021; originally announced March 2021.

ACM Class: F.4.1; F.1.3; D.3.1

Modal Reasoning = Metric Reasoning, via Lawvere

Authors: Ugo Dal Lago, Francesco Gavazzo

Abstract: Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent computations where code usage plays a central role. The theory of program equivalence for modal and coeffectful languages, however, is considerably underdeveloped if compared to the denotational and operational semantics of such languages. This raises the question of how much of the theory of… ▽ More Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent computations where code usage plays a central role. The theory of program equivalence for modal and coeffectful languages, however, is considerably underdeveloped if compared to the denotational and operational semantics of such languages. This raises the question of how much of the theory of ordinary program equivalence can be given in a modal scenario. In this work, we show that coinductive equivalences can be extended to a modal setting, and we do so by generalising Abramsky's applicative bisimilarity to coeffectful behaviours. To achieve this goal, we develop a general theory of ternary program relations based on the novel notion of a comonadic lax extension, on top of which we define a modal extension of Abramsky's applicative bisimilarity (which we dub modal applicative bisimilarity). We prove such a relation to be a congruence, this way obtaining a compositional technique for reasoning about modal and coeffectful behaviours. But this is not the end of the story: we also establish a correspondence between modal program relations and program distances. This correspondence shows that modal applicative bisimilarity and (a properly extended) applicative bisimilarity distance coincide, this way revealing that modal program equivalences and program distances are just two sides of the same coin. △ Less

Submitted 5 March, 2021; originally announced March 2021.

ACM Class: D.3.1

The (In)Efficiency of Interaction

Authors: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

Abstract: Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce $\textit{space}$ efficiencies, the price being $\textit{time}$ performances often poorer than those obtainable with traditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latt… ▽ More Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce $\textit{space}$ efficiencies, the price being $\textit{time}$ performances often poorer than those obtainable with traditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latter do exist, it is currently unknown how \emph{general} this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known abstract machines inside a common definitional framework, this way being able to give sharp results about the relative time efficiencies. We also prove that non-idempotent intersection type theories are able to precisely reflect the time performances of the interactive abstract machine, this way showing that its time-inefficiency ultimately descends from the presence of higher-order types. △ Less

Submitted 24 October, 2020; originally announced October 2020.

Intersection Types and (Positive) Almost-Sure Termination

Authors: Ugo Dal Lago, Claudia Faggian, Simona Ronchi Della Rocca

Abstract: Randomized higher-order computation can be seen as being captured by a lambda calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the probability of obtaining any given result, rather than the possibility or the necessity of obtaining it, like in (non)deterministic computation. Termination, arguably the sim… ▽ More Randomized higher-order computation can be seen as being captured by a lambda calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the probability of obtaining any given result, rather than the possibility or the necessity of obtaining it, like in (non)deterministic computation. Termination, arguably the simplest kind of reachability problem, can be spelled out in at least two ways, depending on whether it talks about the probability of convergence or about the expected evaluation time, the second one providing a stronger guarantee. In this paper, we show that intersection types are capable of precisely characterizing both notions of termination inside a single system of types: the probability of convergence of any lambda-term can be underapproximated by its type, while the underlying derivation's weight gives a lower bound to the term's expected number of steps to normal form. Noticeably, both approximations are tight -- not only soundness but also completeness holds. The crucial ingredient is non-idempotency, without which it would be impossible to reason on the expected number of reduction steps which are necessary to completely evaluate any term. Besides, the kind of approximation we obtain is proved to be optimal recursion theoretically: no recursively enumerable formal system can do better than that. △ Less

Submitted 23 December, 2020; v1 submitted 23 October, 2020; originally announced October 2020.

Journal ref: Proc. ACM Program. Lang. 5, POPL (2021)

On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem

Authors: Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo

Abstract: Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions… ▽ More Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we study a generalization of the concept of a logical relation, called \emph{open logical relation}, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed $λ$-calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any such a collection of functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations. △ Less

Submitted 19 February, 2020; originally announced February 2020.

Decomposing Probabilistic Lambda-calculi

Authors: Ugo Dal Lago, Giulio Guerrieri, Willem Heijltjes

Abstract: A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculu… ▽ More A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation. △ Less

Submitted 19 February, 2020; originally announced February 2020.

ACM Class: F.3.2; D.3.1

On Higher-Order Cryptography (Long Version)

Authors: Boaz Barak, Raphaëlle Crubillé, Ugo Dal Lago

Abstract: Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes themselves higher-order? This paper gives an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, t… ▽ More Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes themselves higher-order? This paper gives an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, then showing how the concept of probabilistic polynomial time algorithm can be generalized so as to encompass algorithms of order strictly higher than two, and finally proving some positive and negative results about the existence of higher-order cryptographic primitives, namely authentication schemes and pseudorandom functions. △ Less

Submitted 17 February, 2020; originally announced February 2020.

The Abstract Machinery of Interaction (Long Version)

Authors: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

Abstract: This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine, not relying on environments, presented on linear logic proof nets, and whose soundness proof is convoluted and passes through various other formalisms. Here we provide a new direct proof of its correctness, based on a v… ▽ More This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine, not relying on environments, presented on linear logic proof nets, and whose soundness proof is convoluted and passes through various other formalisms. Here we provide a new direct proof of its correctness, based on a variant of Sands's improvements, a natural notion of bisimulation. Moreover, our proof is carried out on a new presentation of the IAM, defined as a machine acting directly on $λ$-terms, rather than on linear logic proof nets. △ Less

Submitted 9 July, 2020; v1 submitted 13 February, 2020; originally announced February 2020.

Comments: Accepted at PPDP 2020

A Diagrammatic Calculus for Algebraic Effects

Authors: Ugo Dal Lago, Francesco Gavazzo

Abstract: We introduce a new diagrammatic notation for representing the result of (algebraic) effectful computations. Our notation explicitly separates the effects produced during a computation from the possible values returned, this way simplifying the extension of definitions and results on pure computations to an effectful setting. Additionally, we show a number of algebraic and order-theoretic laws on d… ▽ More We introduce a new diagrammatic notation for representing the result of (algebraic) effectful computations. Our notation explicitly separates the effects produced during a computation from the possible values returned, this way simplifying the extension of definitions and results on pure computations to an effectful setting. Additionally, we show a number of algebraic and order-theoretic laws on diagrams, this way laying the foundations for a diagrammatic calculus of algebraic effects. We give a formal foundation for such a calculus in terms of Lawvere theories and generic effects. △ Less

Submitted 7 January, 2020; v1 submitted 5 January, 2020; originally announced January 2020.

Differential Logical Relations, Part I: The Simply-Typed Case (Long Version)

Authors: Ugo Dal Lago, Francesco Gavazzo, Akira Yoshimizu

Abstract: We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between terms not (necessarily) by a numerical value, but by a mathematical object which… ▽ More We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between terms not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity, i.e. the type, of the compared terms. We exemplify this concept in the simply-typed lambda-calculus, and show a form of soundness theorem. We also see how ordinary logical relations and metric relations can be seen as instances of differential logical relations. Finally, we show that differential logical relations can be organised in a cartesian closed category, contrarily to metric relations, which are well-known not to have such a structure, but only that of a monoidal closed category. △ Less

Submitted 27 April, 2019; originally announced April 2019.

On the Taylor Expansion of Probabilistic $λ$-Terms (Long Version)

Authors: Ugo Dal Lago, Thomas Leventis

Abstract: We generalise Ehrhard and Regnier's Taylor expansion from pure to probabilistic $λ$-terms through notions of probabilistic resource terms and explicit Taylor expansion. We prove that the Taylor expansion is adequate when seen as a way to give semantics to probabilistic $λ$-terms, and that there is a precise correspondence with probabilistic Böhm trees, as introduced by the second author. We generalise Ehrhard and Regnier's Taylor expansion from pure to probabilistic $λ$-terms through notions of probabilistic resource terms and explicit Taylor expansion. We prove that the Taylor expansion is adequate when seen as a way to give semantics to probabilistic $λ$-terms, and that there is a precise correspondence with probabilistic Böhm trees, as introduced by the second author. △ Less

Submitted 21 April, 2019; originally announced April 2019.

The Geometry of Bayesian Programming

Authors: Ugo Dal Lago, Naohiko Hoshino

Abstract: We give a geometry of interaction model for a typed lambda-calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The model is based on the category of measurable spaces and partial measurable functions, and is proved adequate with respect to both a distribution-based and a sam… ▽ More We give a geometry of interaction model for a typed lambda-calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The model is based on the category of measurable spaces and partial measurable functions, and is proved adequate with respect to both a distribution-based and a sampling based operational semantics. △ Less

Submitted 15 April, 2019; originally announced April 2019.

Journal ref: Math. Struct. Comp. Sci. 31 (2021) 633-681

On the Termination Problem for Probabilistic Higher-Order Recursive Programs

Authors: Naoki Kobayashi, Ugo Dal Lago, Charles Grellois

Abstract: In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study on the probabilistic higher-order model checking problem, by giving some first theoretical and experi… ▽ More In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study on the probabilistic higher-order model checking problem, by giving some first theoretical and experimental results. As a first step towards our goal, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higher-order programs. The model of PHORS may alternatively be viewed as a higher-order extension of recursive Markov chains. We then investigate the probabilistic termination problem -- or, equivalently, the probabilistic reachability problem. We prove that almost sure termination of order-2 PHORS is undecidable. We also provide a fixpoint characterization of the termination probability of PHORS, and develop a sound (but possibly incomplete) procedure for approximately computing the termination probability. We have implemented the procedure for order-2 PHORSs, and confirmed that the procedure works well through preliminary experiments that are reported at the end of the article. △ Less

Submitted 1 October, 2020; v1 submitted 5 November, 2018; originally announced November 2018.

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 4 (October 2, 2020) lmcs:5919

On randomised strategies in the $λ$-calculus (long version)

Authors: Ugo Dal Lago, Gabriele Vanoni

Abstract: In this work we study randomised reduction strategies,a notion already known in the context of abstract reduction systems, for the $λ$-calculus. We develop a simple framework that allows us to prove a randomised strategy to be positive almost-surely normalising. Then we propose a simple example of randomised strategy for the $λ$-calculus that has such a property and we show why it is non-trivial w… ▽ More In this work we study randomised reduction strategies,a notion already known in the context of abstract reduction systems, for the $λ$-calculus. We develop a simple framework that allows us to prove a randomised strategy to be positive almost-surely normalising. Then we propose a simple example of randomised strategy for the $λ$-calculus that has such a property and we show why it is non-trivial with respect to classical deterministic strategies such as leftmost-outermost or rightmost-innermost. We conclude studying this strategy for two sub-$λ$-calculi, namely those where duplication and erasure are syntactically forbidden, showing some non-trivial properties. △ Less

Submitted 8 November, 2019; v1 submitted 10 May, 2018; originally announced May 2018.

On Probabilistic Term Rewriting

Authors: Martin Avanzini, Ugo Dal Lago, Akihisa Yamada

Abstract: We study the termination problem for probabilistic term rewrite systems. We prove that the interpretation method is sound and complete for a strengthening of positive almost sure termination, when abstract reduction systems and term rewrite systems are considered. Two instances of the interpretation method - polynomial and matrix interpretations - are analyzed and shown to capture interesting and… ▽ More We study the termination problem for probabilistic term rewrite systems. We prove that the interpretation method is sound and complete for a strengthening of positive almost sure termination, when abstract reduction systems and term rewrite systems are considered. Two instances of the interpretation method - polynomial and matrix interpretations - are analyzed and shown to capture interesting and nontrivial examples when automated. We capture probabilistic computation in a novel way by way of multidistribution reduction sequences, this way accounting for both the nondeterminism in the choice of the redex and the probabilism intrinsic in firing each rule. △ Less

Submitted 27 February, 2018; originally announced February 2018.

Comments: Technical Report of our FLOPS'18 paper

Encoding Turing Machines into the Deterministic Lambda-Calculus

Authors: Ugo Dal Lago, Beniamino Accattoli

Abstract: This note is about encoding Turing machines into the lambda-calculus. This note is about encoding Turing machines into the lambda-calculus. △ Less

Submitted 27 November, 2017; originally announced November 2017.

Automating Sized Type Inference for Complexity Analysis (Technical Report)

Authors: Martin Avanzini, Ugo Dal Lago

Abstract: This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation, and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which ca… ▽ More This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation, and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to the choice of adopting an abstract index language and index polymorphism at higher ranks. A prototype implementation is available. △ Less

Submitted 28 June, 2017; originally announced June 2017.

Comments: Technical report of http://dx.doi.org/10.1145/3110287

Automated Sized-Type Inference and Complexity Analysis

Authors: Martin Avanzini, Ugo Dal Lago

Abstract: This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three components: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and a concrete tool for constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of… ▽ More This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three components: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and a concrete tool for constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available. △ Less

Submitted 18 April, 2017; originally announced April 2017.

Comments: In Proceedings DICE-FOPARA 2017, arXiv:1704.05169

ACM Class: I.2.2

Journal ref: EPTCS 248, 2017, pp. 7-16

Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)

Authors: Ugo Dal Lago, Francesco Gavazzo, Paul Blain Levy

Abstract: We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $λ$-calculi with algebraic effects. We first of all endow a computational $λ$-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which… ▽ More We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $λ$-calculi with algebraic effects. We first of all endow a computational $λ$-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract. △ Less

Submitted 15 April, 2017; originally announced April 2017.

Comments: 30 pages

The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens (Long Version)

Authors: Ugo Dal Lago, Ryo Tanaka, Akira Yoshimizu

Abstract: We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation as embodied by process algebras like the $π$-calculus. The introduced model is based on token machines in which not one but multiple tokens are allowed to traverse the underlying net at the same time. We prove soundness a… ▽ More We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation as embodied by process algebras like the $π$-calculus. The introduced model is based on token machines in which not one but multiple tokens are allowed to traverse the underlying net at the same time. We prove soundness and adequacy of the introduced model. The former is proved as a simulation result between the token machines one obtains along any reduction sequence. The latter is obtained by a fine analysis of convergence, both in nets and in token machines. △ Less

Submitted 15 April, 2017; originally announced April 2017.

Metric Reasoning About $λ$-Terms: The General Case (Long Version)

Authors: Raphaëlle Crubillé, Ugo Dal Lago

Abstract: In any setting in which observable properties have a quantitative flavour, it is natural to compare computational objects by way of \emph{metrics} rather than equivalences or partial orders. This holds, in particular, for probabilistic higher-order programs. A natural notion of comparison, then, becomes context distance, the metric analogue of Morris' context equivalence. In this paper, we analyze… ▽ More In any setting in which observable properties have a quantitative flavour, it is natural to compare computational objects by way of \emph{metrics} rather than equivalences or partial orders. This holds, in particular, for probabilistic higher-order programs. A natural notion of comparison, then, becomes context distance, the metric analogue of Morris' context equivalence. In this paper, we analyze the main properties of the context distance in fully-fledged probabilistic $λ$-calculi, this way going beyond the state of the art, in which only affine calculi were considered. We first of all study to which extent the context distance trivializes, giving a sufficient condition for trivialization. We then characterize context distance by way of a coinductively defined, tuple-based notion of distance in one of those calculi, called $Λ^\oplus_!$. We finally derive pseudometrics for call-by-name and call-by-value probabilistic $λ$-calculi, and prove them fully-abstract. △ Less

Submitted 19 January, 2017; originally announced January 2017.

On Higher-Order Probabilistic Subrecursion

Authors: Flavien Breuvart, Ugo Dal Lago, Agathe Herrou

Abstract: We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like Gödel's $\mathbb{T}$ with various forms of probabilistic choice operators may result in calculi which are not equivalent as for the class of distributions they give rise to, although they all guarantee almost-sure termination. Alon… ▽ More We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like Gödel's $\mathbb{T}$ with various forms of probabilistic choice operators may result in calculi which are not equivalent as for the class of distributions they give rise to, although they all guarantee almost-sure termination. Along the way, we introduce a probabilistic variation of the classic reducibility technique, and we prove that the simplest form of probabilistic choice leaves the expressive power of $\mathbb{T}$ essentially unaltered. The paper ends with some observations about the functional expressive power: expectedly, all the considered calculi capture the functions which $\mathbb{T}$ itself represents, at least when standard notions of observations are considered. △ Less

Submitted 22 December, 2021; v1 submitted 17 January, 2017; originally announced January 2017.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 4 (December 23, 2021) lmcs:4226

Probabilistic Termination by Monadic Affine Sized Ty** (Long Version)

Authors: Ugo Dal Lago, Charles Grellois

Abstract: We introduce a system of monadic affine sized types, which substantially generalise usual sized types, and allows this way to capture probabilistic higher-order programs which terminate almost surely. Going beyond plain, strong normalisation without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing s… ▽ More We introduce a system of monadic affine sized types, which substantially generalise usual sized types, and allows this way to capture probabilistic higher-order programs which terminate almost surely. Going beyond plain, strong normalisation without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility, but requires a substantial adaptation of the technique. △ Less

Submitted 15 January, 2017; originally announced January 2017.

Comments: 63 pages. To appear in ESOP 2017

The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects

Authors: Ugo Dal Lago, Claudia Faggian, Benoit Valiron, Akira Yoshimizu

Abstract: We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a full quantum programming language in which entanglement, duplication, and recursion are all available. Our model comes with a multi-token machine, a proof net system, and a PCF-style language. The approach we develop is not specific to quantum computation, and our model is an instance of… ▽ More We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a full quantum programming language in which entanglement, duplication, and recursion are all available. Our model comes with a multi-token machine, a proof net system, and a PCF-style language. The approach we develop is not specific to quantum computation, and our model is an instance of a new framework whose main feature is the ability to model commutative effects in a parallel setting. Being based on a multi-token machine equipped with a memory, it has a concrete nature which makes it well suited for building low-level operational descriptions of higher-order languages. △ Less

Submitted 15 July, 2017; v1 submitted 30 October, 2016; originally announced October 2016.

Comments: 21 pages, extended version of the conference paper ; July 2017: removed a spurious and unused lemma

Infinitary $λ$-Calculi from a Linear Perspective (Long Version)

Authors: Ugo Dal Lago

Abstract: We introduce a linear infinitary $λ$-calculus, called $\ellΛ_{\infty}$, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the infinitary applicative $λ$-calculus and is universal for computations over infinite strings. What is particularly interesting about… ▽ More We introduce a linear infinitary $λ$-calculus, called $\ellΛ_{\infty}$, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the infinitary applicative $λ$-calculus and is universal for computations over infinite strings. What is particularly interesting about $\ellΛ_{\infty}$, is that the refinement induced by linear logic allows to restrict both modalities so as to get calculi which are terminating inductively and productive coinductively. We exemplify this idea by analysing a fragment of $\ellΛ$ built around the principles of $\mathsf{SLL}$ and $\mathsf{4LL}$. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary $λ$-calculi. △ Less

Submitted 27 April, 2016; originally announced April 2016.

(Leftmost-Outermost) Beta Reduction is Invariant, Indeed

Authors: Beniamino Accattoli, Ugo Dal Lago

Abstract: Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent a… ▽ More Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent and based over a standard notion in the theory of lambda-calculus: the length of a leftmost-outermost derivation to normal form is an invariant cost model. Such a theorem cannot be proved by directly relating lambda-calculus with Turing machines or random access machines, because of the size explosion problem: there are terms that in a linear number of steps produce an exponentially long output. The first step towards the solution is to shift to a notion of evaluation for which the length and the size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modeled after linear logic proof nets and admitting a decomposition of leftmost-outermost derivations with the desired property. Thus, the LSC is invariant with respect to, say, random access machines. The second step is to show that LSC is invariant with respect to the lambda-calculus. The size explosion problem seems to imply that this is not possible: having the same notions of normal form, evaluation in the LSC is exponentially longer than in the lambda-calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction, deemed useful. Useful evaluation avoids those steps that only unshare the output without contributing to beta-redexes, i.e. the steps that cause the blow-up in size. The main technical contribution of the paper is indeed the definition of useful reductions and the thorough analysis of their properties. △ Less

Submitted 8 March, 2016; v1 submitted 6 January, 2016; originally announced January 2016.

Comments: arXiv admin note: substantial text overlap with arXiv:1405.3311

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 1 (March 9, 2016) lmcs:1627

A Lambda-Calculus Foundation for Universal Probabilistic Programming

Authors: Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak

Abstract: We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approxi… ▽ More We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integrating over all traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language. △ Less

Submitted 23 January, 2017; v1 submitted 30 December, 2015; originally announced December 2015.

Applicative Bisimulation and Quantum $λ$-Calculi (Long Version)

Authors: Ugo Dal Lago, Alessandro Rioli

Abstract: Applicative bisimulation is a coinductive technique to check program equivalence in higher-order functional languages. It is known to be sound, and sometimes complete, with respect to context equivalence. In this paper we show that applicative bisimulation also works when the underlying language of programs takes the form of a linear $λ$-calculus extended with features such as probabilistic binary… ▽ More Applicative bisimulation is a coinductive technique to check program equivalence in higher-order functional languages. It is known to be sound, and sometimes complete, with respect to context equivalence. In this paper we show that applicative bisimulation also works when the underlying language of programs takes the form of a linear $λ$-calculus extended with features such as probabilistic binary choice, but also quantum data, the latter being a setting in which linearity plays a role. The main results are proofs of soundness for the obtained notions of bisimilarity. △ Less

Submitted 22 June, 2015; originally announced June 2015.