-
On the complexity of normalization for the planar $λ$-calculus
Authors:
Anupam Das,
Damiano Mazza,
Lê Thành Dũng Nguyên,
Noam Zeilberger
Abstract:
We sketch a tentative proof of P-completeness for the $β$-convertibility problem on untyped planar (a.k.a. ordered or non-commutative) $λ$-terms.
We sketch a tentative proof of P-completeness for the $β$-convertibility problem on untyped planar (a.k.a. ordered or non-commutative) $λ$-terms.
△ Less
Submitted 8 April, 2024;
originally announced April 2024.
-
The Invisible Map: Visual-Inertial SLAM with Fiducial Markers for Smartphone-based Indoor Navigation
Authors:
Paul Ruvolo,
Ayush Chakraborty,
Rucha Dave,
Richard Li,
Duncan Mazza,
Xierui Shen,
Raiyan Siddique,
Krishna Suresh
Abstract:
We present a system for creating building-scale, easily navigable 3D maps using mainstream smartphones. In our approach, we formulate the 3D-map** problem as an instance of Graph SLAM and infer the position of both building landmarks (fiducial markers) and navigable paths through the environment (phone poses). Our results demonstrate the system's ability to create accurate 3D maps. Further, we h…
▽ More
We present a system for creating building-scale, easily navigable 3D maps using mainstream smartphones. In our approach, we formulate the 3D-map** problem as an instance of Graph SLAM and infer the position of both building landmarks (fiducial markers) and navigable paths through the environment (phone poses). Our results demonstrate the system's ability to create accurate 3D maps. Further, we highlight the importance of careful selection of map** hyperparameters and provide a novel technique for tuning these hyperparameters to adapt our algorithm to new environments.
△ Less
Submitted 16 October, 2023;
originally announced October 2023.
-
Automatic Differentiation in PCF
Authors:
Damiano Mazza,
Michele Pagani
Abstract:
We study the correctness of automatic differentiation (AD) in the context of a higher-order, Turing-complete language (PCF with real numbers), both in forward and reverse mode. Our main result is that, under mild hypotheses on the primitive functions included in the language, AD is almost everywhere correct, that is, it computes the derivative or gradient of the program under consideration except…
▽ More
We study the correctness of automatic differentiation (AD) in the context of a higher-order, Turing-complete language (PCF with real numbers), both in forward and reverse mode. Our main result is that, under mild hypotheses on the primitive functions included in the language, AD is almost everywhere correct, that is, it computes the derivative or gradient of the program under consideration except for a set of Lebesgue measure zero. Stated otherwise, there are inputs on which AD is incorrect, but the probability of randomly choosing one such input is zero. Our result is in fact more precise, in that the set of failure points admits a more explicit description: for example, in case the primitive functions are just constants, addition and multiplication, the set of points where AD fails is contained in a countable union of zero sets of non-identically-zero polynomials.
△ Less
Submitted 12 January, 2021; v1 submitted 6 November, 2020;
originally announced November 2020.
-
Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Authors:
Alois Brunel,
Damiano Mazza,
Michele Pagani
Abstract:
Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field…
▽ More
Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field called differentiable programming, the aim of which is to express computational graphs more synthetically and modularly by resorting to actual programming languages endowed with control flow operators and higher-order combinators, such as map and fold. In this paper, we extend the backpropagation algorithm to a paradigmatic example of such a programming language: we define a compositional program transformation from the simply-typed lambda-calculus to itself augmented with a notion of linear negation, and prove that this computes the gradient of the source program with the same efficiency as first-order backpropagation. The transformation is completely effect-free and thus provides a purely logical understanding of the dynamics of backpropagation.
△ Less
Submitted 6 November, 2019; v1 submitted 27 September, 2019;
originally announced September 2019.
-
A Strong Distillery
Authors:
Beniamino Accattoli,
Pablo Barenbaum,
Damiano Mazza
Abstract:
Abstract machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bou…
▽ More
Abstract machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e., the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.
△ Less
Submitted 16 March, 2016; v1 submitted 3 September, 2015;
originally announced September 2015.
-
Distilling Abstract Machines (Long Version)
Authors:
Beniamino Accattoli,
Pablo Barenbaum,
Damiano Mazza
Abstract:
It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between big-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-bas…
▽ More
It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between big-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in call-by-name, call-by-value, and call-by-need, catching many machines in the literature. We start by distilling the KAM, the CEK, and the ZINC, and then provide simplified versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we also introduce some new machines with global environments. Moreover, we show that distillation preserves the time complexity of the executions, i.e. the LSC is a complexity-preserving abstraction of abstract machines.
△ Less
Submitted 9 June, 2014;
originally announced June 2014.
-
Computational Complexity of Interactive Behaviors
Authors:
Ugo Dal Lago,
Tobias Heindel,
Damiano Mazza,
Daniele Varacca
Abstract:
The theory of computational complexity focuses on functions and, hence, studies programs whose interactive behavior is reduced to a simple question/answer pattern. We propose a broader theory whose ultimate goal is expressing and analyzing the intrinsic difficulty of fully general interactive behaviors. To this extent, we use standard tools from concurrency theory, including labelled transition sy…
▽ More
The theory of computational complexity focuses on functions and, hence, studies programs whose interactive behavior is reduced to a simple question/answer pattern. We propose a broader theory whose ultimate goal is expressing and analyzing the intrinsic difficulty of fully general interactive behaviors. To this extent, we use standard tools from concurrency theory, including labelled transition systems (formalizing behaviors) and their asynchronous extension (providing causality information). Behaviors are implemented by means of a multiprocessor machine executing CCS-like processes. The resulting theory is shown to be consistent with the classical definitions: when we restrict to functional behaviors (i.e., question/answer patterns), we recover several standard computational complexity classes.
△ Less
Submitted 4 September, 2012;
originally announced September 2012.
-
An Abstract Approach to Stratification in Linear Logic
Authors:
Pierre Boudes,
Damiano Mazza,
Lorenzo Tortora de Falco
Abstract:
We study the notion of stratification, as used in subsystems of linear logic with low complexity bounds on the cut-elimination procedure (the so-called light logics), from an abstract point of view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is a generalization of the paragraph modality of Girard's light linear logic, arises from a…
▽ More
We study the notion of stratification, as used in subsystems of linear logic with low complexity bounds on the cut-elimination procedure (the so-called light logics), from an abstract point of view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is a generalization of the paragraph modality of Girard's light linear logic, arises from a general categorical construction applicable to all models of linear logic. We thus learn that stratification may be formulated independently of exponential modalities; when it is forced to be connected to exponential modalities, it yields interesting complexity properties. In particular, from our analysis stem three alternative reformulations of Baillot and Mazza's linear logic by levels: one geometric, one interactive, and one semantic.
△ Less
Submitted 14 February, 2013; v1 submitted 27 June, 2012;
originally announced June 2012.
-
Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators
Authors:
Damiano Mazza
Abstract:
The symmetric interaction combinators are an equally expressive variant of Lafont's interaction combinators. They are a graph-rewriting model of deterministic computation. We define two notions of observational equivalence for them, analogous to normal form and head normal form equivalence in the lambda-calculus. Then, we prove a full abstraction result for each of the two equivalences. This is…
▽ More
The symmetric interaction combinators are an equally expressive variant of Lafont's interaction combinators. They are a graph-rewriting model of deterministic computation. We define two notions of observational equivalence for them, analogous to normal form and head normal form equivalence in the lambda-calculus. Then, we prove a full abstraction result for each of the two equivalences. This is obtained by interpreting nets as certain subsets of the Cantor space, called edifices, which play the same role as Boehm trees in the theory of the lambda-calculus.
△ Less
Submitted 22 December, 2009; v1 submitted 1 June, 2009;
originally announced June 2009.
-
Linear Logic by Levels and Bounded Time Complexity
Authors:
Patrick Baillot,
Damiano Mazza
Abstract:
We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratifica…
▽ More
We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indexes, which allows us to extend Girard's systems while kee** the same complexity properties. In particular, it turns out that Girard's systems can be recovered by forcing depth and level to coincide. A consequence of the higher flexibility of levels with respect to depth is the absence of boxes for handling the paragraph modality. We use this fact to propose a variant of our polytime system in which the paragraph modality is only allowed on atoms, and which may thus serve as a basis for develo** lambda-calculus type assignment systems with more efficient ty** algorithms than existing ones.
△ Less
Submitted 26 July, 2009; v1 submitted 8 January, 2008;
originally announced January 2008.
