-
A Construction of Optimal Quasi-cyclic Locally Recoverable Codes using Constituent Codes
Authors:
Gustavo Terra Bastos,
Angelynn Alvarez,
Zachary Flores,
Adriana Salerno
Abstract:
A locally recoverable code of locality $r$ over $\mathbb{F}_{q}$ is a code where every coordinate of a codeword can be recovered using the values of at most $r$ other coordinates of that codeword. Locally recoverable codes are efficient at restoring corrupted messages and data which make them highly applicable to distributed storage systems. Quasi-cyclic codes of length $n=m\ell$ and index $\ell$…
▽ More
A locally recoverable code of locality $r$ over $\mathbb{F}_{q}$ is a code where every coordinate of a codeword can be recovered using the values of at most $r$ other coordinates of that codeword. Locally recoverable codes are efficient at restoring corrupted messages and data which make them highly applicable to distributed storage systems. Quasi-cyclic codes of length $n=m\ell$ and index $\ell$ are linear codes that are invariant under cyclic shifts by $\ell$ places. %Quasi-cyclic codes are generalizations of cyclic codes and are isomorphic to $\mathbb{F}_{q} [x]/ \langle x^m-1 \rangle$-submodules of $\mathbb{F}_{q^\ell} [x] / \langle x^m-1 \rangle$. In this paper, we decompose quasi-cyclic locally recoverable codes into a sum of constituent codes where each constituent code is a linear code over a field extension of $\mathbb{F}_q$. Using these constituent codes with set parameters, we propose conditions which ensure the existence of almost optimal and optimal quasi-cyclic locally recoverable codes with increased dimension and code length.
△ Less
Submitted 17 June, 2024;
originally announced June 2024.
-
A Formalization of Operads in Coq
Authors:
Zachary Flores,
Angelo Taranto,
Eric Bond,
Yakir Forman
Abstract:
What provides the highest level of assurance for correctness of execution within a programming language? One answer, and our solution in particular, to this problem is to provide a formalization for, if it exists, the denotational semantics of a programming language. Achieving such a formalization provides a gold standard for ensuring a programming language is correct-by-construction. In our effor…
▽ More
What provides the highest level of assurance for correctness of execution within a programming language? One answer, and our solution in particular, to this problem is to provide a formalization for, if it exists, the denotational semantics of a programming language. Achieving such a formalization provides a gold standard for ensuring a programming language is correct-by-construction. In our effort on the DARPA V-SPELLS program, we worked to provide a foundation for the denotational semantics of a meta-language using a mathematical object known as an operad. This object has compositional properties which are vital to building languages from smaller pieces. In this paper, we discuss our formalization of an operad in the proof assistant Coq. Moreover, our definition within Coq is capable of providing proofs that objects specified within Coq are operads. This work within Coq provides a formal mathematical basis for our meta-language development within V-SPELLS. Our work also provides, to our knowledge, the first known formalization of operads within a proof assistant that has significant automation, as well as a model that can be replicated without knowledge of Homotopy Type Theory.
△ Less
Submitted 15 March, 2023;
originally announced March 2023.
-
A Formal Algebraic Framework for DSL Composition
Authors:
Zachary Flores,
Angelo Taranto,
Eric Bond
Abstract:
We discuss a formal framework for using algebraic structures to model a meta-language that can write, compose, and provide interoperability between abstractions of DSLs. The purpose of this formal framework is to provide a verification of compositional properties of the meta-language. Throughout our paper we discuss the construction of this formal framework, as well its relation to our team's work…
▽ More
We discuss a formal framework for using algebraic structures to model a meta-language that can write, compose, and provide interoperability between abstractions of DSLs. The purpose of this formal framework is to provide a verification of compositional properties of the meta-language. Throughout our paper we discuss the construction of this formal framework, as well its relation to our team's work on the DARPA V-SPELLS program via the pipeline we have developed for completing our verification tasking on V-SPELLS. We aim to give a broad overview of this verification pipeline in our paper. The pipeline can be split into four main components: the first is providing a formal model of the meta-language in Coq; the second is to give a specification in Coq of our chosen algebraic structures; third, we need to implement specific instances of our algebraic structures in Coq, as well as give a proof in Coq that this implementation is an algebraic structure according to our specification in the second step; and lastly, we need to give a proof in Coq that the formal model for the meta-language in the first step is an instance of the implementation in the third step.
△ Less
Submitted 1 February, 2023;
originally announced February 2023.
-
Using Known Words to Learn More Words: A Distributional Analysis of Child Vocabulary Development
Authors:
Andrew Z. Flores,
Jessica Montag,
Jon Willits
Abstract:
Why do children learn some words before others? Understanding individual variability across children and also variability across words, may be informative of the learning processes that underlie language learning. We investigated item-based variability in vocabulary development using lexical properties of distributional statistics derived from a large corpus of child-directed speech. Unlike previo…
▽ More
Why do children learn some words before others? Understanding individual variability across children and also variability across words, may be informative of the learning processes that underlie language learning. We investigated item-based variability in vocabulary development using lexical properties of distributional statistics derived from a large corpus of child-directed speech. Unlike previous analyses, we predicted word trajectories cross-sectionally, shedding light on trends in vocabulary development that may not have been evident at a single time point. We also show that whether one looks at a single age group or across ages as a whole, the best distributional predictor of whether a child knows a word is the number of other known words with which that word tends to co-occur. Keywords: age of acquisition; vocabulary development; lexical diversity; child-directed speech;
△ Less
Submitted 21 November, 2021; v1 submitted 14 September, 2020;
originally announced September 2020.
