Showing 1–10 of 10 results for author: Vanoni, G

(Almost) Affine Higher-Order Tree Transducers

Authors: Lê Thành Dũng Tito Nguyên, Gabriele Vanoni

Abstract: We investigate the tree-to-tree functions computed by \enquote{affine$λ$-transducers}: tree automata whose memory consists of an affine $λ$-term instead of a finite state. They can be seen as variations on Gallot, Lemay and Salvati's Linear High-Order Deterministic Tree Transducers. When the memory is almost purely affine (\textit{à la} Kanazawa), we show that these machines can be translated to t… ▽ More We investigate the tree-to-tree functions computed by \enquote{affine$λ$-transducers}: tree automata whose memory consists of an affine $λ$-term instead of a finite state. They can be seen as variations on Gallot, Lemay and Salvati's Linear High-Order Deterministic Tree Transducers. When the memory is almost purely affine (\textit{à la} Kanazawa), we show that these machines can be translated to tree-walking transducers (and with a purely affine memory, we get a reversible tree-walking transducer). This leads to a proof of an inexpressivity conjecture of \titocecilia on \enquote{implicit automata} in an affine $λ$-calculus. The key technical tool in our proofs is the Interaction Abstract Machine (IAM), an operational avatar of the \enquote{geometry of interaction} semantics of linear logic. We work with ad-hoc specializations to (almost) affine $λ$-terms of a tree-generating version of the IAM. △ Less

Submitted 8 February, 2024; originally announced February 2024.

Monadic Intersection Types, Relationally (Extended Version)

Authors: Francesco Gavazzo, Riccardo Treglia, Gabriele Vanoni

Abstract: We extend intersection types to a computational $λ$-calculus with algebraic operations à 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 behavi… ▽ More We extend intersection types to a computational $λ$-calculus with algebraic operations à 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. △ Less

Submitted 23 January, 2024; originally announced January 2024.

Higher-Order Bayesian Networks, Exactly (Extended version)

Authors: Claudia Faggian, Daniele Pautasso, Gabriele Vanoni

Abstract: Bayesian networks (BNs) are graphical \emph{first-order} probabilistic models that allow for a compact representation of large probability distributions, and for efficient inference, both exact and approximate. We introduce a \emph{higher-order} programming language -- in the idealized form of a $λ$-calculus -- which we prove \emph{sound and complete} w.r.t. BNs: each BN can be encoded as a term,… ▽ More Bayesian networks (BNs) are graphical \emph{first-order} probabilistic models that allow for a compact representation of large probability distributions, and for efficient inference, both exact and approximate. We introduce a \emph{higher-order} programming language -- in the idealized form of a $λ$-calculus -- which we prove \emph{sound and complete} w.r.t. BNs: each BN can be encoded as a term, and conversely each (possibly higher-order and recursive) program of ground type \emph{compiles} into a BN. The language allows for the specification of recursive probability models and hierarchical structures. Moreover, we provide a \emph{compositional} and \emph{cost-aware} semantics which is based on factors, the standard mathematical tool used in Bayesian inference. Our results rely on advanced techniques rooted into linear logic, intersection types, rewriting theory, and Girard's geometry of interaction, which are here combined in a novel way. △ Less

Submitted 11 December, 2023; v1 submitted 8 November, 2023; originally announced November 2023.

Journal ref: Proc. ACM Program. Lang. 8, POPL, Article 84 (January 2024)

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

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.

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.

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.

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.

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

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.