-
Compositional pre-processing for automated reasoning in dependent type theory
Authors:
Valentin Blot,
Denis Cousineau,
Enzo Crance,
Louise Dubois de Prisque,
Chantal Keller,
Assia Mahboubi,
Pierre Vial
Abstract:
In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones.
This paper discusses the design and the implementation of…
▽ More
In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones.
This paper discusses the design and the implementation of pre-processing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines.
△ Less
Submitted 21 February, 2024; v1 submitted 6 April, 2022;
originally announced April 2022.
-
Learning the Proximity Operator in Unfolded ADMM for Phase Retrieval
Authors:
Pierre-Hugo Vial,
Paul Magron,
Thomas Oberlin,
Cédric Févotte
Abstract:
This paper considers the phase retrieval (PR) problem, which aims to reconstruct a signal from phaseless measurements such as magnitude or power spectrograms. PR is generally handled as a minimization problem involving a quadratic loss. Recent works have considered alternative discrepancy measures, such as the Bregman divergences, but it is still challenging to tailor the optimal loss for a given…
▽ More
This paper considers the phase retrieval (PR) problem, which aims to reconstruct a signal from phaseless measurements such as magnitude or power spectrograms. PR is generally handled as a minimization problem involving a quadratic loss. Recent works have considered alternative discrepancy measures, such as the Bregman divergences, but it is still challenging to tailor the optimal loss for a given setting. In this paper we propose a novel strategy to automatically learn the optimal metric for PR. We unfold a recently introduced ADMM algorithm into a neural network, and we emphasize that the information about the loss used to formulate the PR problem is conveyed by the proximity operator involved in the ADMM updates. Therefore, we replace this proximity operator with trainable activation functions: learning these in a supervised setting is then equivalent to learning an optimal metric for PR. Experiments conducted with speech signals show that our approach outperforms the baseline ADMM, using a light and interpretable neural architecture.
△ Less
Submitted 4 April, 2022;
originally announced April 2022.
-
General Automation in Coq through Modular Transformations
Authors:
Valentin Blot,
Louise Dubois de Prisque,
Chantal Keller,
Pierre Vial
Abstract:
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first…
▽ More
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first-order statements that can be automatically discharged by automatic provers. The general idea is to write modular, pairwise independent transformations and combine them. Each of these eliminates a specific aspect of Coq logic towards first-order logic. As a proof of concept, we apply this methodology to a set of simple but crucial transformations which extend the local context with proven first-order assertions that make Coq definitions and algebraic types explicit. They allow users of Coq to solve non-trivial goals automatically. This methodology paves the way towards the definition and combination of more complex transformations, making Coq more accessible.
△ Less
Submitted 5 July, 2021;
originally announced July 2021.
-
Sequence Types and Infinitary Semantics
Authors:
Pierre Vial
Abstract:
We introduce a new representation of non-idempotent intersection types, using \textbf{sequences} (families indexed with natural numbers) instead of lists or multisets. This allows scaling up \textbf{intersection type} theory to the infinitary $λ$-calculus. We thus characterize hereditary head normalization, which gives a positive answer to a question known as \textbf{Klop's Problem}. On our way, w…
▽ More
We introduce a new representation of non-idempotent intersection types, using \textbf{sequences} (families indexed with natural numbers) instead of lists or multisets. This allows scaling up \textbf{intersection type} theory to the infinitary $λ$-calculus. We thus characterize hereditary head normalization, which gives a positive answer to a question known as \textbf{Klop's Problem}. On our way, we use \textbf{non-idempotent intersection} to retrieve some well-known results on infinitary terms.
△ Less
Submitted 15 December, 2021; v1 submitted 15 February, 2021;
originally announced February 2021.
-
Phase retrieval with Bregman divergences: Application to audio signal recovery
Authors:
Pierre-Hugo Vial,
Paul Magron,
Thomas Oberlin,
Cédric Févotte
Abstract:
Phase retrieval aims to recover a signal from magnitude or power spectra measurements. It is often addressed by considering a minimization problem involving a quadratic cost function. We propose a different formulation based on Bregman divergences, which encompass divergences that are appropriate for audio signal processing applications. We derive a fast gradient algorithm to solve this problem.
Phase retrieval aims to recover a signal from magnitude or power spectra measurements. It is often addressed by considering a minimization problem involving a quadratic cost function. We propose a different formulation based on Bregman divergences, which encompass divergences that are appropriate for audio signal processing applications. We derive a fast gradient algorithm to solve this problem.
△ Less
Submitted 25 November, 2020;
originally announced November 2020.
-
Phase recovery with Bregman divergences for audio source separation
Authors:
Paul Magron,
Pierre-Hugo Vial,
Thomas Oberlin,
Cédric Févotte
Abstract:
Time-frequency audio source separation is usually achieved by estimating the short-time Fourier transform (STFT) magnitude of each source, and then applying a phase recovery algorithm to retrieve time-domain signals. In particular, the multiple input spectrogram inversion (MISI) algorithm has shown good performance in several recent works. This algorithm minimizes a quadratic reconstruction error…
▽ More
Time-frequency audio source separation is usually achieved by estimating the short-time Fourier transform (STFT) magnitude of each source, and then applying a phase recovery algorithm to retrieve time-domain signals. In particular, the multiple input spectrogram inversion (MISI) algorithm has shown good performance in several recent works. This algorithm minimizes a quadratic reconstruction error between magnitude spectrograms. However, this loss does not properly account for some perceptual properties of audio, and alternative discrepancy measures such as beta-divergences have been preferred in many settings. In this paper, we propose to reformulate phase recovery in audio source separation as a minimization problem involving Bregman divergences. To optimize the resulting objective, we derive a projected gradient descent algorithm. Experiments conducted on a speech enhancement task show that this approach outperforms MISI for several alternative losses, which highlights their relevance for audio source separation applications.
△ Less
Submitted 9 February, 2021; v1 submitted 20 October, 2020;
originally announced October 2020.
-
Phase retrieval with Bregman divergences and application to audio signal recovery
Authors:
Pierre-Hugo Vial,
Paul Magron,
Thomas Oberlin,
Cédric Févotte
Abstract:
Phase retrieval (PR) aims to recover a signal from the magnitudes of a set of inner products. This problem arises in many audio signal processing applications which operate on a short-time Fourier transform magnitude or power spectrogram, and discard the phase information. Recovering the missing phase from the resulting modified spectrogram is indeed necessary in order to synthesize time-domain si…
▽ More
Phase retrieval (PR) aims to recover a signal from the magnitudes of a set of inner products. This problem arises in many audio signal processing applications which operate on a short-time Fourier transform magnitude or power spectrogram, and discard the phase information. Recovering the missing phase from the resulting modified spectrogram is indeed necessary in order to synthesize time-domain signals. PR is commonly addressed by considering a minimization problem involving a quadratic loss function. In this paper, we adopt a different standpoint. Indeed, the quadratic loss does not properly account for some perceptual properties of audio, and alternative discrepancy measures such as beta-divergences have been preferred in many settings. Therefore, we formulate PR as a new minimization problem involving Bregman divergences. Since these divergences are not symmetric with respect to their two input arguments in general, they lead to two different formulations of the problem. To optimize the resulting objective, we derive two algorithms based on accelerated gradient descent and alternating direction method of multipliers. Experiments conducted on audio signal recovery from spectrograms that are either exact or estimated from noisy observations highlight the potential of our proposed methods for audio restoration. In particular, leveraging some of these Bregman divergences induce better performance than the quadratic loss when performing PR from spectrograms under very noisy conditions.
△ Less
Submitted 13 January, 2021; v1 submitted 1 October, 2020;
originally announced October 2020.
-
Non-idempotent types for classical calculi in natural deduction style
Authors:
Delia Kesner,
Pierre Vial
Abstract:
In the first part of this paper, we define two resource aware ty** systems for the λμ-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head red…
▽ More
In the first part of this paper, we define two resource aware ty** systems for the λμ-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head reduction and the maximal reduction sequences to normal-form. In the second part of this paper, the λμ-calculus is refined to a small-step calculus called λμs, which is inspired by the substitution at a distance paradigm. The λμs-calculus turns out to be compatible with a natural extensionof the non-idempotent interpretations of λμ, i.e., λμs-reduction preserves and decreases ty** derivations in an extended appropriate ty** system. We thus derive a simple arithmetical characterization of strongly λμs-normalizing terms by means of ty**.
△ Less
Submitted 13 January, 2020; v1 submitted 15 February, 2018;
originally announced February 2018.
-
All the λ-Terms are Meaningful for the Infinitary Relational Model
Authors:
Pierre Vial
Abstract:
Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Ω, the auto- autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most infinitary frameworks, it is not difficult to define a type R that can be assigned to every λ-term. However, these observations do not say much about what coinductive (…
▽ More
Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Ω, the auto- autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most infinitary frameworks, it is not difficult to define a type R that can be assigned to every λ-term. However, these observations do not say much about what coinductive (i.e. infinitary) type grammars are able to provide: it is for instance very difficult to know what types (besides R) can be assigned to a given term in this setting. We begin with a discussion on the expressivity of different forms of infinite types. Then, using the resource-awareness of sequential intersection types (system S) and tracking, we prove that infinite types are able to characterize the order (arity) of every λ-terms and that, in the infinitary extension of the relational model, every term has a "meaning" i.e. a non-empty denotation. From the technical point of view, we must deal with the total lack of productivity guarantee for typable terms: we do so by importing methods inspired by first order model theory.
△ Less
Submitted 20 January, 2018; v1 submitted 20 December, 2016;
originally announced December 2016.
-
Infinitary Intersection Types as Sequences: a New Answer to Klop's Question
Authors:
Pierre Vial
Abstract:
We provide a type-theoretical characterization of weakly-normalizing terms in an infinitary lambda-calculus. We adapt for this purpose the standard quantitative (with non-idempotent intersections) type assignment system of the lambda-calculus to our infinite calculus. Our work provides a new answer to Klop's HHN-problem, namely, finding out if there is a type system characterizing the hereditary h…
▽ More
We provide a type-theoretical characterization of weakly-normalizing terms in an infinitary lambda-calculus. We adapt for this purpose the standard quantitative (with non-idempotent intersections) type assignment system of the lambda-calculus to our infinite calculus. Our work provides a new answer to Klop's HHN-problem, namely, finding out if there is a type system characterizing the hereditary head-normalizing (HHN) lambda-terms. Tatsuta showed that HHN could not be characterized by a finite type system. We prove that an infinitary type system endowed with a validity condition called approximability can achieve it.
△ Less
Submitted 20 October, 2016;
originally announced October 2016.
-
Representing permutations without permutations, or the expressive power of sequence types
Authors:
Pierre Vial
Abstract:
Recent works by Asada, Ong and Tsukada have championed a rigid description of resources. Whereas in non-rigid paradigms (e.g., standard Taylor expansion or non-idempotent intersection types), bags of resources are multisets and invariant under permutation, in the rigid ones, permutations must be processed explicitly and can be allowed or disallowed. Rigidity enables a fine-grained control of reduc…
▽ More
Recent works by Asada, Ong and Tsukada have championed a rigid description of resources. Whereas in non-rigid paradigms (e.g., standard Taylor expansion or non-idempotent intersection types), bags of resources are multisets and invariant under permutation, in the rigid ones, permutations must be processed explicitly and can be allowed or disallowed. Rigidity enables a fine-grained control of reduction paths and their effects on e.g., ty** derivations. We previously introduced a very constrained coinductive type system (system S) in which permutation is completely disallowed. One may wonder in what extent the absence of permutations causes a loss of expressivity w.r.t. reduction paths, compared to a usual multiset framework or a rigid one allowing permutations. We answer this question in the most general case i.e. coinductive type grammars without validity conditions. Our main contribution is to prove that not only every non-idempotent derivation can be represented by a rigid, permutation-free derivation, but also that any dynamic behavior may be captured in this way. In other words, we prove that system S has full expressive power over multiset/permutation-inclusive intersection.
△ Less
Submitted 24 January, 2018; v1 submitted 20 October, 2016;
originally announced October 2016.
