-
Musical Phrase Segmentation via Grammatical Induction
Authors:
Reed Perkins,
Dan Ventura
Abstract:
We outline a solution to the challenge of musical phrase segmentation that uses grammatical induction algorithms, a class of algorithms which infer a context-free grammar from an input sequence. We analyze the performance of five grammatical induction algorithms on three datasets using various musical viewpoint combinations. Our experiments show that the LONGESTFIRST algorithm achieves the best F1…
▽ More
We outline a solution to the challenge of musical phrase segmentation that uses grammatical induction algorithms, a class of algorithms which infer a context-free grammar from an input sequence. We analyze the performance of five grammatical induction algorithms on three datasets using various musical viewpoint combinations. Our experiments show that the LONGESTFIRST algorithm achieves the best F1 scores across all three datasets and that input encodings that include the duration viewpoint result in the best performance.
△ Less
Submitted 29 May, 2024;
originally announced May 2024.
-
Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
Authors:
Temur Kutsia,
Daniel Ventura,
David Monniaux,
José F. Morales
Abstract:
This volume contains
* The post-proceedings of the Eighteenth Logical and Semantic Frameworks with Applications (LSFA 2023). The meeting was held on July 1-2, 2023, organised by the Sapienza Università di Roma, Italy. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include pr…
▽ More
This volume contains
* The post-proceedings of the Eighteenth Logical and Semantic Frameworks with Applications (LSFA 2023). The meeting was held on July 1-2, 2023, organised by the Sapienza Università di Roma, Italy. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include proof theory, type theory and rewriting theory, specification and deduction languages, and formal semantics of languages and systems.
* The post-proceedings of the Tenth Workshop on Horn clauses for Verification and Synthesis (HCVS 2023). The meeting was held on April 23, 2023 at the Institut Henri Poincaré in Paris. HCVS aims to bring together researchers working in the two communities of constraint/ logic programming (e.g., ICLP and CP), program verification (e.g., CAV, TACAS, and VMCAI), and automated deduction (e.g., CADE, IJCAR), on the topics of Horn clause based analysis, verification, and synthesis.
△ Less
Submitted 21 April, 2024;
originally announced April 2024.
-
Towards Reliable Assessments of Demographic Disparities in Multi-Label Image Classifiers
Authors:
Melissa Hall,
Bobbie Chern,
Laura Gustafson,
Denisse Ventura,
Harshad Kulkarni,
Candace Ross,
Nicolas Usunier
Abstract:
Disaggregated performance metrics across demographic groups are a hallmark of fairness assessments in computer vision. These metrics successfully incentivized performance improvements on person-centric tasks such as face analysis and are used to understand risks of modern models. However, there is a lack of discussion on the vulnerabilities of these measurements for more complex computer vision ta…
▽ More
Disaggregated performance metrics across demographic groups are a hallmark of fairness assessments in computer vision. These metrics successfully incentivized performance improvements on person-centric tasks such as face analysis and are used to understand risks of modern models. However, there is a lack of discussion on the vulnerabilities of these measurements for more complex computer vision tasks. In this paper, we consider multi-label image classification and, specifically, object categorization tasks. First, we highlight design choices and trade-offs for measurement that involve more nuance than discussed in prior computer vision literature. These challenges are related to the necessary scale of data, definition of groups for images, choice of metric, and dataset imbalances. Next, through two case studies using modern vision models, we demonstrate that naive implementations of these assessments are brittle. We identify several design choices that look merely like implementation details but significantly impact the conclusions of assessments, both in terms of magnitude and direction (on which group the classifiers work best) of disparities. Based on ablation studies, we propose some recommendations to increase the reliability of these assessments. Finally, through a qualitative analysis we find that concepts with large disparities tend to have varying definitions and representations between groups, with inconsistencies across datasets and annotators. While this result suggests avenues for mitigation through more consistent data collection, it also highlights that ambiguous label definitions remain a challenge when performing model assessments. Vision models are expanding and becoming more ubiquitous; it is even more important that our disparity assessments accurately reflect the true performance of models.
△ Less
Submitted 16 February, 2023;
originally announced February 2023.
-
Node Replication: Theory And Practice
Authors:
Delia Kesner,
Loïc Peyrot,
Daniel Ventura
Abstract:
We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.
We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.
△ Less
Submitted 19 January, 2024; v1 submitted 14 July, 2022;
originally announced July 2022.
-
A Subexponential View of Domains in Session Types
Authors:
Daniele Nantes,
Carlos Olarte,
Daniel Ventura
Abstract:
Linear logic (LL) has inspired the design of many computational systems, offering reasoning techniques built on top of its meta-theory. Since its inception, several connections between concurrent systems and LL have emerged from different perspectives. In the last decade, the seminal work of Caires and Pfenning showed that formulas in LL can be interpreted as session types and processes in the pi-…
▽ More
Linear logic (LL) has inspired the design of many computational systems, offering reasoning techniques built on top of its meta-theory. Since its inception, several connections between concurrent systems and LL have emerged from different perspectives. In the last decade, the seminal work of Caires and Pfenning showed that formulas in LL can be interpreted as session types and processes in the pi-calculus as proof terms. This leads to a Curry-Howard interpretation where proof reductions in the cut-elimination procedure correspond to process reductions/interactions. The subexponentials in LL have also played an important role in concurrent systems since they can be interpreted in different ways, including timed, spatial and even epistemic modalities in distributed systems. In this paper we address the question: What is the meaning of the subexponentials from the point of view of a session type interpretation? Our answer is a pi-like process calculus where agents reside in locations/sites and they make it explicit how the communication among the different sites should happen. The design of this language relies completely on the proof theory of the subexponentials in LL, thus extending the Caires-Pfenning interpretation in an elegant way.
△ Less
Submitted 8 April, 2022; v1 submitted 8 October, 2021;
originally announced October 2021.
-
On the balanceability of some graph classes
Authors:
Antoine Dailly,
Adriana Hansberg,
Denae Ventura
Abstract:
Given a graph $G$, a 2-coloring of the edges of $K_n$ is said to contain a balanced copy of $G$ if we can find a copy of $G$ such that half of its edges are in each color class. If, for every sufficiently large $n$, there exists an integer $k$ such that every 2-coloring of $K_n$ with more than $k$ edges in each color class contains a balanced copy of $G$, then we say that $G$ is balanceable. Balan…
▽ More
Given a graph $G$, a 2-coloring of the edges of $K_n$ is said to contain a balanced copy of $G$ if we can find a copy of $G$ such that half of its edges are in each color class. If, for every sufficiently large $n$, there exists an integer $k$ such that every 2-coloring of $K_n$ with more than $k$ edges in each color class contains a balanced copy of $G$, then we say that $G$ is balanceable. Balanceability was introduced by Caro, Hansberg and Montejano, who also gave a structural characterization of balanceable graphs.
In this paper, we extend the study of balanceability by finding new sufficient conditions for a graph to be balanceable or not. We use those conditions to fully characterize the balanceability of graph classes such as rectangular and triangular grids, as well as a special class of circulant graphs.
△ Less
Submitted 17 November, 2020; v1 submitted 10 March, 2020;
originally announced March 2020.
-
A Quantitative Understanding of Pattern Matching
Authors:
Sandra Alves,
Delia Kesner,
Daniel Ventura
Abstract:
This paper shows that the recent approach to quantitative ty** systems for programming languages can be extended to pattern matching features. Indeed, we define two resource aware type systems, named U and E, for a lambda-calculus equipped with pairs for both patterns and terms. Our ty** systems borrow some basic ideas from [BKRDR15], which characterises (head) normalisation in a qualitative w…
▽ More
This paper shows that the recent approach to quantitative ty** systems for programming languages can be extended to pattern matching features. Indeed, we define two resource aware type systems, named U and E, for a lambda-calculus equipped with pairs for both patterns and terms. Our ty** systems borrow some basic ideas from [BKRDR15], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But in contrast to [BKRDR15], our (static) systems also provides quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs, instead of the disjoint unions in [BKRDR15], thus avoiding an overlap between "being a pair" and "being duplicable", resulting in an essential tool to reason about quantitativity. Secondly, ty** sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (c.f. length) and space (c.f. size). Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors. Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta reduction, substitution and matching steps are counted separately.
△ Less
Submitted 4 December, 2019;
originally announced December 2019.
-
Principal Ty**s in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices
Authors:
Daniel Ventura,
Mauricio Ayala-Rincón,
Fairouz Kamareddine
Abstract:
The lambda-calculus with de Bruijn indices assembles each alpha-class of lambda-terms in a unique term, using indices instead of variable names. Intersection types provide finitary type polymorphism and can characterise normalisable lambda-terms through the property that a term is normalisable if and only if it is typeable. To be closer to computations and to simplify the formalisation of the at…
▽ More
The lambda-calculus with de Bruijn indices assembles each alpha-class of lambda-terms in a unique term, using indices instead of variable names. Intersection types provide finitary type polymorphism and can characterise normalisable lambda-terms through the property that a term is normalisable if and only if it is typeable. To be closer to computations and to simplify the formalisation of the atomic operations involved in beta-contractions, several calculi of explicit substitution were developed mostly with de Bruijn indices. Versions of explicit substitutions calculi without types and with simple type systems are well investigated in contrast to versions with more elaborate type systems such as intersection types. In previous work, we introduced a de Bruijn version of the lambda-calculus with an intersection type system and proved that it preserves subject reduction, a basic property of type systems. In this paper a version with de Bruijn indices of an intersection type system originally introduced to characterise principal ty**s for beta-normal forms is presented. We present the characterisation in this new system and the corresponding versions for the type inference and the reconstruction of normal forms from principal ty**s algorithms. We briefly discuss the failure of the subject reduction property and some possible solutions for it.
△ Less
Submitted 25 January, 2010;
originally announced January 2010.
