-
Cooperative learning of Pl@ntNet's Artificial Intelligence algorithm: how does it work and how can we improve it?
Authors:
Tanguy Lefort,
Antoine Affouard,
Benjamin Charlier,
Jean-Christophe Lombardo,
Mathias Chouet,
Hervé Goëau,
Joseph Salmon,
Pierre Bonnet,
Alexis Joly
Abstract:
Deep learning models for plant species identification rely on large annotated datasets. The PlantNet system enables global data collection by allowing users to upload and annotate plant observations, leading to noisy labels due to diverse user skills. Achieving consensus is crucial for training, but the vast scale of collected data makes traditional label aggregation strategies challenging. Existi…
▽ More
Deep learning models for plant species identification rely on large annotated datasets. The PlantNet system enables global data collection by allowing users to upload and annotate plant observations, leading to noisy labels due to diverse user skills. Achieving consensus is crucial for training, but the vast scale of collected data makes traditional label aggregation strategies challenging. Existing methods either retain all observations, resulting in noisy training data or selectively keep those with sufficient votes, discarding valuable information. Additionally, as many species are rarely observed, user expertise can not be evaluated as an inter-user agreement: otherwise, botanical experts would have a lower weight in the AI training step than the average user. Our proposed label aggregation strategy aims to cooperatively train plant identification AI models. This strategy estimates user expertise as a trust score per user based on their ability to identify plant species from crowdsourced data. The trust score is recursively estimated from correctly identified species given the current estimated labels. This interpretable score exploits botanical experts' knowledge and the heterogeneity of users. Subsequently, our strategy removes unreliable observations but retains those with limited trusted annotations, unlike other approaches. We evaluate PlantNet's strategy on a released large subset of the PlantNet database focused on European flora, comprising over 6M observations and 800K users. We demonstrate that estimating users' skills based on the diversity of their expertise enhances labeling performance. Our findings emphasize the synergy of human annotation and data filtering in improving AI performance for a refined dataset. We explore incorporating AI-based votes alongside human input. This can further enhance human-AI interactions to detect unreliable observations.
△ Less
Submitted 5 June, 2024;
originally announced June 2024.
-
A Program That Simplifies Regular Expressions (Tool paper)
Authors:
Baudouin Le Charlier
Abstract:
This paper presents the main features of a system that aims to transform regular expressions into shorter equivalent expressions. The system is also capable of computing other operations useful for simplification, such as checking the inclusion of regular languages. The main novelty of this work is that it combines known but distinct ways of representing regular languages into a global unified dat…
▽ More
This paper presents the main features of a system that aims to transform regular expressions into shorter equivalent expressions. The system is also capable of computing other operations useful for simplification, such as checking the inclusion of regular languages. The main novelty of this work is that it combines known but distinct ways of representing regular languages into a global unified data structure that makes the operations more efficient. In addition, representations of regular languages are dynamically reduced as operations are performed on them. Expressions are normalized and represented by a unique identifier (an integer). Expressions found to be equivalent (i.e. denoting the same regular language) are grouped into equivalence classes from which a shortest representative is chosen. The article briefly describes the main algorithms working on the global data structure. Some of them are direct adaptations of well-known algorithms, but most of them incorporate new ideas, which are really necessary to make the system efficient. Finally, to show its usefulness, the system is applied to some examples from the literature. Statistics on randomly generated sets of expressions are also provided.
△ Less
Submitted 12 July, 2023;
originally announced July 2023.
-
Identify ambiguous tasks combining crowdsourced labels by weighting Areas Under the Margin
Authors:
Tanguy Lefort,
Benjamin Charlier,
Alexis Joly,
Joseph Salmon
Abstract:
In supervised learning - for instance in image classification - modern massive datasets are commonly labeled by a crowd of workers. The obtained labels in this crowdsourcing setting are then aggregated for training, generally leveraging a per-worker trust score. Yet, such workers oriented approaches discard the tasks' ambiguity. Ambiguous tasks might fool expert workers, which is often harmful for…
▽ More
In supervised learning - for instance in image classification - modern massive datasets are commonly labeled by a crowd of workers. The obtained labels in this crowdsourcing setting are then aggregated for training, generally leveraging a per-worker trust score. Yet, such workers oriented approaches discard the tasks' ambiguity. Ambiguous tasks might fool expert workers, which is often harmful for the learning step. In standard supervised learning settings - with one label per task - the Area Under the Margin (AUM) was tailored to identify mislabeled data. We adapt the AUM to identify ambiguous tasks in crowdsourced learning scenarios, introducing the Weighted Areas Under the Margin (WAUM). The WAUM is an average of AUMs weighted according to task-dependent scores. We show that the WAUM can help discarding ambiguous tasks from the training set, leading to better generalization performance. We report improvements over existing strategies for learning with a crowd, both on simulated settings, and on real datasets such as CIFAR-10H (a crowdsourced dataset with a high number of answered labels),LabelMe and Music (two datasets with few answered votes).
△ Less
Submitted 30 November, 2023; v1 submitted 30 September, 2022;
originally announced September 2022.
-
Benchopt: Reproducible, efficient and collaborative optimization benchmarks
Authors:
Thomas Moreau,
Mathurin Massias,
Alexandre Gramfort,
Pierre Ablin,
Pierre-Antoine Bannier,
Benjamin Charlier,
Mathieu Dagréou,
Tom Dupré la Tour,
Ghislain Durif,
Cassio F. Dantas,
Quentin Klopfenstein,
Johan Larsson,
En Lai,
Tanguy Lefort,
Benoit Malézieux,
Badr Moufad,
Binh T. Nguyen,
Alain Rakotomamonjy,
Zaccharie Ramzi,
Joseph Salmon,
Samuel Vaiter
Abstract:
Numerical validation is at the core of machine learning research as it allows to assess the actual impact of new methods, and to confirm the agreement between theory and practice. Yet, the rapid development of the field poses several challenges: researchers are confronted with a profusion of methods to compare, limited transparency and consensus on best practices, as well as tedious re-implementat…
▽ More
Numerical validation is at the core of machine learning research as it allows to assess the actual impact of new methods, and to confirm the agreement between theory and practice. Yet, the rapid development of the field poses several challenges: researchers are confronted with a profusion of methods to compare, limited transparency and consensus on best practices, as well as tedious re-implementation work. As a result, validation is often very partial, which can lead to wrong conclusions that slow down the progress of research. We propose Benchopt, a collaborative framework to automate, reproduce and publish optimization benchmarks in machine learning across programming languages and hardware architectures. Benchopt simplifies benchmarking for the community by providing an off-the-shelf tool for running, sharing and extending experiments. To demonstrate its broad usability, we showcase benchmarks on three standard learning tasks: $\ell_2$-regularized logistic regression, Lasso, and ResNet18 training for image classification. These benchmarks highlight key practical findings that give a more nuanced view of the state-of-the-art for these problems, showing that for practical evaluation, the devil is in the details. We hope that Benchopt will foster collaborative work in the community hence improving the reproducibility of research findings.
△ Less
Submitted 28 October, 2022; v1 submitted 27 June, 2022;
originally announced June 2022.
-
Mercury's crustal thickness correlates with lateral variations in mantle melt production
Authors:
Mikael Beuthe,
Bernard Charlier,
Olivier Namur,
Attilio Rivoldini,
Tim Van Hoolst
Abstract:
Mercury's crust has a complex structure resulting from a billion years of volcanism. The surface variations in chemical composition have been identified from orbit by the spacecraft MESSENGER. Combining these measurements with laboratory experiments on partial melting, we estimate which variations in surface density and degree of mantle melting are required to produce surface rocks. If the surface…
▽ More
Mercury's crust has a complex structure resulting from a billion years of volcanism. The surface variations in chemical composition have been identified from orbit by the spacecraft MESSENGER. Combining these measurements with laboratory experiments on partial melting, we estimate which variations in surface density and degree of mantle melting are required to produce surface rocks. If the surface density is representative of the deep crustal density, more than one half of crustal thickness variations in the northern hemisphere are explained by lateral variations in mantle melting. The crust is thin below the magnesium-poor Northern Volcanic Plains whereas the thickest crust is found in the magnesium-rich region located at mid-northern latitudes in the Western Hemisphere. The magnesium-rich region is thus not due to an early impact but rather to extensive mantle melting. The thickness-melting relation has also been observed for the oceanic crust on Earth and might be a common feature of terrestrial planets.
△ Less
Submitted 30 November, 2020;
originally announced November 2020.
-
Kernel Operations on the GPU, with Autodiff, without Memory Overflows
Authors:
Benjamin Charlier,
Jean Feydy,
Joan Alexis Glaunès,
François-David Collin,
Ghislain Durif
Abstract:
The KeOps library provides a fast and memory-efficient GPU support for tensors whose entries are given by a mathematical formula, such as kernel and distance matrices. KeOps alleviates the major bottleneck of tensor-centric libraries for kernel and geometric applications: memory consumption. It also supports automatic differentiation and outperforms standard GPU baselines, including PyTorch CUDA t…
▽ More
The KeOps library provides a fast and memory-efficient GPU support for tensors whose entries are given by a mathematical formula, such as kernel and distance matrices. KeOps alleviates the major bottleneck of tensor-centric libraries for kernel and geometric applications: memory consumption. It also supports automatic differentiation and outperforms standard GPU baselines, including PyTorch CUDA tensors or the Halide and TVM libraries. KeOps combines optimized C++/CUDA schemes with binders for high-level languages: Python (Numpy and PyTorch), Matlab and GNU R. As a result, high-level "quadratic" codes can now scale up to large data sets with millions of samples processed in seconds. KeOps brings graphics-like performances for kernel methods and is freely available on standard repositories (PyPi, CRAN). To showcase its versatility, we provide tutorials in a wide range of settings online at \url{www.kernel-operations.io}.
△ Less
Submitted 8 April, 2021; v1 submitted 27 March, 2020;
originally announced April 2020.
-
Experimental Evaluation of a Method to Simplify Expressions
Authors:
Baudouin Le Charlier
Abstract:
We present a method to simplify expressions in the context of an equational theory. The basic ideas and concepts of the method have been presented previously elsewhere but here we tackle the difficult task of making it efficient in practice, in spite of its great generality. We first recall the notion of a collection of structures, which allows us to manipulate very large (possibly infinite) sets…
▽ More
We present a method to simplify expressions in the context of an equational theory. The basic ideas and concepts of the method have been presented previously elsewhere but here we tackle the difficult task of making it efficient in practice, in spite of its great generality. We first recall the notion of a collection of structures, which allows us to manipulate very large (possibly infinite) sets of terms as a whole, i.e., without enumerating their elements. Then we use this tool to construct algorithms to simplify expressions. We give various reasons why it is difficult to make these algorithms precise and efficient. We then propose a number of approches to solve the raised issues. Finally, and importantly, we provide a detailed experimental evaluation of the method and a comparison of several variants of it. Although the method is completely generic, we use (arbitrary, not only two-level) boolean expressions as the application field for these experiments because impressive simplifications can be obtained in spite of the hardness of the problem.
△ Less
Submitted 13 March, 2020;
originally announced March 2020.
-
Parallel transport in shape analysis: a scalable numerical scheme
Authors:
Maxime Louis,
Alexandre Bône,
Benjamin Charlier,
Stanley Durrleman
Abstract:
The analysis of manifold-valued data requires efficient tools from Riemannian geometry to cope with the computational complexity at stake. This complexity arises from the always-increasing dimension of the data, and the absence of closed-form expressions to basic operations such as the Riemannian logarithm. In this paper, we adapt a generic numerical scheme recently introduced for computing parall…
▽ More
The analysis of manifold-valued data requires efficient tools from Riemannian geometry to cope with the computational complexity at stake. This complexity arises from the always-increasing dimension of the data, and the absence of closed-form expressions to basic operations such as the Riemannian logarithm. In this paper, we adapt a generic numerical scheme recently introduced for computing parallel transport along geodesics in a Riemannian manifold to finite-dimensional manifolds of diffeomorphisms. We provide a qualitative and quantitative analysis of its behavior on high-dimensional manifolds, and investigate an application with the prediction of brain structures progression.
△ Less
Submitted 23 November, 2017;
originally announced November 2017.
-
Prediction of the progression of subcortical brain structures in Alzheimer's disease from baseline
Authors:
Alexandre Bône,
Maxime Louis,
Alexandre Routier,
Jorge Samper,
Michael Bacci,
Benjamin Charlier,
Olivier Colliot,
Stanley Durrleman
Abstract:
We propose a method to predict the subject-specific longitudinal progression of brain structures extracted from baseline MRI, and evaluate its performance on Alzheimer's disease data. The disease progression is modeled as a trajectory on a group of diffeomorphisms in the context of large deformation diffeomorphic metric map** (LDDMM). We first exhibit the limited predictive abilities of geodesic…
▽ More
We propose a method to predict the subject-specific longitudinal progression of brain structures extracted from baseline MRI, and evaluate its performance on Alzheimer's disease data. The disease progression is modeled as a trajectory on a group of diffeomorphisms in the context of large deformation diffeomorphic metric map** (LDDMM). We first exhibit the limited predictive abilities of geodesic regression extrapolation on this group. Building on the recent concept of parallel curves in shape manifolds, we then introduce a second predictive protocol which personalizes previously learned trajectories to new subjects, and investigate the relative performances of two parallel shifting paradigms. This design only requires the baseline imaging data. Finally, coefficients encoding the disease dynamics are obtained from longitudinal cognitive measurements for each subject, and exploited to refine our methodology which is demonstrated to successfully predict the follow-up visits.
△ Less
Submitted 23 November, 2017;
originally announced November 2017.
-
White Matter Fiber Segmentation Using Functional Varifolds
Authors:
Kuldeep Kumar,
Pietro Gori,
Benjamin Charlier,
Stanley Durrleman,
Olivier Colliot,
Christian Desrosiers
Abstract:
The extraction of fibers from dMRI data typically produces a large number of fibers, it is common to group fibers into bundles. To this end, many specialized distance measures, such as MCP, have been used for fiber similarity. However, these distance based approaches require point-wise correspondence and focus only on the geometry of the fibers. Recent publications have highlighted that using micr…
▽ More
The extraction of fibers from dMRI data typically produces a large number of fibers, it is common to group fibers into bundles. To this end, many specialized distance measures, such as MCP, have been used for fiber similarity. However, these distance based approaches require point-wise correspondence and focus only on the geometry of the fibers. Recent publications have highlighted that using microstructure measures along fibers improves tractography analysis. Also, many neurodegenerative diseases impacting white matter require the study of microstructure measures as well as the white matter geometry. Motivated by these, we propose to use a novel computational model for fibers, called functional varifolds, characterized by a metric that considers both the geometry and microstructure measure (e.g. GFA) along the fiber pathway. We use it to cluster fibers with a dictionary learning and sparse coding-based framework, and present a preliminary analysis using HCP data.
△ Less
Submitted 18 September, 2017;
originally announced September 2017.
-
Optimal Transport for Diffeomorphic Registration
Authors:
Jean Feydy,
Benjamin Charlier,
François-Xavier Vialard,
Gabriel Peyré
Abstract:
This paper introduces the use of unbalanced optimal transport methods as a similarity measure for diffeomorphic matching of imaging data. The similarity measure is a key object in diffeomorphic registration methods that, together with the regularization on the deformation, defines the optimal deformation. Most often, these similarity measures are local or non local but simple enough to be computat…
▽ More
This paper introduces the use of unbalanced optimal transport methods as a similarity measure for diffeomorphic matching of imaging data. The similarity measure is a key object in diffeomorphic registration methods that, together with the regularization on the deformation, defines the optimal deformation. Most often, these similarity measures are local or non local but simple enough to be computationally fast. We build on recent theoretical and numerical advances in optimal transport to propose fast and global similarity measures that can be used on surfaces or volumetric imaging data. This new similarity measure is computed using a fast generalized Sinkhorn algorithm. We apply this new metric in the LDDMM framework on synthetic and real data, fibres bundles and surfaces and show that better matching results are obtained.
△ Less
Submitted 16 June, 2017;
originally announced June 2017.
-
Metamorphoses of functional shapes in Sobolev spaces
Authors:
Nicolas Charon,
Benjamin Charlier,
Alain Trouvé
Abstract:
In this paper, we describe in detail a model of geometric-functional variability between fshapes. These objects were introduced for the first time by the authors in [Charlier et al. 2015] and are basically the combination of classical deformable manifolds with additional scalar signal map. Building on the aforementioned work, this paper's contributions are several. We first extend the original…
▽ More
In this paper, we describe in detail a model of geometric-functional variability between fshapes. These objects were introduced for the first time by the authors in [Charlier et al. 2015] and are basically the combination of classical deformable manifolds with additional scalar signal map. Building on the aforementioned work, this paper's contributions are several. We first extend the original $L^2$ model in order to represent signals of higher regularity on their geometrical support with more regular Hilbert norms (typically Sobolev). We describe the bundle structure of such fshape spaces with their adequate geodesic distances, encompassing in one common framework usual shape comparison and image metamorphoses. We then propose a formulation of matching between any two fshapes from the optimal control perspective, study existence of optimal controls and derive Hamiltonian equations and conservation laws describing the dynamics of geodesics. Secondly, we tackle the discrete counterpart of these problems and equations through appropriate finite elements interpolation schemes on triangular meshes. At last, we show a few results of metamorphosis matchings on synthetic and several real data examples in order to highlight the key specificities of the approach.
△ Less
Submitted 6 October, 2016; v1 submitted 5 August, 2016;
originally announced August 2016.
-
The matching problem between functional shapes via a BV penalty term: a $Γ$-convergence result
Authors:
G. Nardi,
B. Charlier,
A. Trouvé
Abstract:
This paper proves a $Γ$-convergence result for the discrete energy (to the continuous one) of the matching problem for signals defined on surfaces. In particular, we highlight some geometric properties that must be guaranteed in the discretization process to ensure the convergence of minimizers. The proof is given in the framework of functional shapes introduced in \cite{ABN}. In particular, we co…
▽ More
This paper proves a $Γ$-convergence result for the discrete energy (to the continuous one) of the matching problem for signals defined on surfaces. In particular, we highlight some geometric properties that must be guaranteed in the discretization process to ensure the convergence of minimizers. The proof is given in the framework of functional shapes introduced in \cite{ABN}. In particular, we consider a varifold-type attachment term, and a $BV$ penalty term is used instead of the original $L^2$ norm.
△ Less
Submitted 18 January, 2024; v1 submitted 26 March, 2015;
originally announced March 2015.
-
The fshape framework for the variability analysis of functional shapes
Authors:
Benjamin Charlier,
Nicolas Charon,
Alain Trouvé
Abstract:
This article introduces a full mathematical and numerical framework for treating functional shapes (or fshapes) following the landmarks of shape spaces and shape analysis. Functional shapes can be described as signal functions supported on varying geometrical supports. Analysing variability of fshapes' ensembles require the modelling and quantification of joint variations in geometry and signal, w…
▽ More
This article introduces a full mathematical and numerical framework for treating functional shapes (or fshapes) following the landmarks of shape spaces and shape analysis. Functional shapes can be described as signal functions supported on varying geometrical supports. Analysing variability of fshapes' ensembles require the modelling and quantification of joint variations in geometry and signal, which have been treated separately in previous approaches. Instead, building on the ideas of shape spaces for purely geometrical objects, we propose the extended concept of fshape bundles and define Riemannian metrics for fshape metamorphoses to model geometrico-functional transformations within these bundles. We also generalize previous works on data attachment terms based on the notion of varifolds and demonstrate the utility of these distances. Based on these, we propose variational formulations of the atlas estimation problem on populations of fshapes and prove existence of solutions for the different models. The second part of the article examines the numerical implementation of the models by detailing discrete expressions for the metrics and gradients and proposing an optimization scheme for the atlas estimation problem. We present a few results of the methodology on a synthetic dataset as well as on a population of retinal membranes with thickness maps.
△ Less
Submitted 24 April, 2014;
originally announced April 2014.
-
Consistent estimation of a mean planar curve modulo similarities
Authors:
Jérémie Bigot,
Benjamin Charlier
Abstract:
We consider the problem of estimating a mean planar curve from a set of $J$ random planar curves observed on a $k$-points deterministic design. We study the consistency of a smoothed Procrustean mean curve when the observations obey a deformable model including some nuisance parameters such as random translations, rotations and scaling. The main contribution of the paper is to analyze the influenc…
▽ More
We consider the problem of estimating a mean planar curve from a set of $J$ random planar curves observed on a $k$-points deterministic design. We study the consistency of a smoothed Procrustean mean curve when the observations obey a deformable model including some nuisance parameters such as random translations, rotations and scaling. The main contribution of the paper is to analyze the influence of the dimension $k$ of the data and of the number $J$ of observed configurations on the convergence of the smoothed Procrustean estimator to the mean curve of the model. Some numerical experiments illustrate these results.
△ Less
Submitted 31 October, 2012; v1 submitted 25 October, 2011;
originally announced October 2011.
-
Necessary and sufficient condition for the existence of a Fréchet mean on the circle
Authors:
Benjamin Charlier
Abstract:
Let $(§^1,d_{§^1})$ be the unit circle in $\R^2$ endowed with the arclength distance. We give a sufficient and necessary condition for a general probability measure $μ$ to admit a well defined Fréchet mean on $(§^1,d_{§^1})$. %This criterion allows to recover already known sufficient conditions of existence. We derive a new sufficient condition of existence $P(α,\varphi)$ with no restriction on th…
▽ More
Let $(§^1,d_{§^1})$ be the unit circle in $\R^2$ endowed with the arclength distance. We give a sufficient and necessary condition for a general probability measure $μ$ to admit a well defined Fréchet mean on $(§^1,d_{§^1})$. %This criterion allows to recover already known sufficient conditions of existence. We derive a new sufficient condition of existence $P(α,\varphi)$ with no restriction on the support of the measure. Then, we study the convergence of the empirical Fréchet mean to the Fréchet mean and we give an algorithm to compute it.
△ Less
Submitted 7 March, 2012; v1 submitted 9 September, 2011;
originally announced September 2011.
-
On the consistency of Fréchet means in deformable models for curve and image analysis
Authors:
Jérémie Bigot,
Benjamin Charlier
Abstract:
A new class of statistical deformable models is introduced to study high-dimensional curves or images. In addition to the standard measurement error term, these deformable models include an extra error term modeling the individual variations in intensity around a mean pattern. It is shown that an appropriate tool for statistical inference in such models is the notion of sample Fréchet means, which…
▽ More
A new class of statistical deformable models is introduced to study high-dimensional curves or images. In addition to the standard measurement error term, these deformable models include an extra error term modeling the individual variations in intensity around a mean pattern. It is shown that an appropriate tool for statistical inference in such models is the notion of sample Fréchet means, which leads to estimators of the deformation parameters and the mean pattern. The main contribution of this paper is to study how the behavior of these estimators depends on the number n of design points and the number J of observed curves (or images). Numerical experiments are given to illustrate the finite sample performances of the procedure.
△ Less
Submitted 22 August, 2011; v1 submitted 3 October, 2010;
originally announced October 2010.
-
Source-to-source optimizing transformations of Prolog programs based on abstract interpretation
Authors:
Francois Gobert,
Baudouin Le Charlier
Abstract:
Making a Prolog program more efficient by transforming its source code, without changing its operational semantics, is not an obvious task. It requires the user to have a clear understanding of how the Prolog compiler works, and in particular, of the effects of impure features like the cut. The way a Prolog code is written - e.g., the order of clauses, the order of literals in a clause, the use…
▽ More
Making a Prolog program more efficient by transforming its source code, without changing its operational semantics, is not an obvious task. It requires the user to have a clear understanding of how the Prolog compiler works, and in particular, of the effects of impure features like the cut. The way a Prolog code is written - e.g., the order of clauses, the order of literals in a clause, the use of cuts or negations - influences its efficiency. Furthermore, different optimization techniques may be redundant or conflicting when they are applied together, depending on the way a procedure is called - e.g., inserting cuts and enabling indexing. We present an optimiser, based on abstract interpretation, that automatically performs safe code transformations of Prolog procedures in the context of some class of input calls. The method is more effective if procedures are annotated with additional information about modes, types, sharing, number of solutions and the like. Thus the approach is similar to Mercury. It applies to any Prolog program, however.
△ Less
Submitted 31 October, 2007;
originally announced October 2007.
-
On the Design of a Tool for Supporting the Construction of Logic Programs
Authors:
Gustavo A. Ospina,
Baudouin Le Charlier
Abstract:
Environments for systematic construction of logic programs are needed in the academy as well as in the industry. Such environments should support well defined construction methods and should be able to be extended and interact with other programming tools like debuggers and compilers. We present a variant of the Deville methodology for logic program development, and the design of a tool for supp…
▽ More
Environments for systematic construction of logic programs are needed in the academy as well as in the industry. Such environments should support well defined construction methods and should be able to be extended and interact with other programming tools like debuggers and compilers. We present a variant of the Deville methodology for logic program development, and the design of a tool for supporting the methodology. Our aim is to facilitate the learning of logic programming and to set the basis of more sophisticated tools for program development.
△ Less
Submitted 27 November, 2001; v1 submitted 15 November, 2001;
originally announced November 2001.
-
Sequence-Based Abstract Interpretation of Prolog
Authors:
Baudouin Le Charlier,
Sabina Rossi,
Pascal Van Hentenryck
Abstract:
Many abstract interpretation frameworks and analyses for Prolog have been proposed, which seek to extract information useful for program optimization. Although motivated by practical considerations, notably making Prolog competitive with imperative languages, such frameworks fail to capture some of the control structures of existing implementations of the language.
In this paper we propose a n…
▽ More
Many abstract interpretation frameworks and analyses for Prolog have been proposed, which seek to extract information useful for program optimization. Although motivated by practical considerations, notably making Prolog competitive with imperative languages, such frameworks fail to capture some of the control structures of existing implementations of the language.
In this paper we propose a novel framework for the abstract interpretation of Prolog which handles the depth-first search rule and the cut operator. It relies on the notion of substitution sequence to model the result of the execution of a goal. The framework consists of (i) a denotational concrete semantics, (ii) a safe abstraction of the concrete semantics defined in terms of a class of post-fixpoints, and (iii) a generic abstract interpretation algorithm. We show that traditional abstract domains of substitutions may easily be adapted to the new framework, and provide experimental evidence of the effectiveness of our approach. We also show that previous work on determinacy analysis, that was not expressible by existing abstract interpretation frameworks, can be seen as an instance of our framework.
△ Less
Submitted 19 October, 2000;
originally announced October 2000.
