Menu Close

Categoría: Reseña

Reseña de artículos.

Reseña: Graph theory in Coq: minors, treewidth, and isomorphisms

Se ha publicado un artículo de razonamiento formalizado en Coq/Ssreflect sobre grafos titulado Graph theory in Coq: minors, treewidth, and isomorphisms.

Sus autores son

  • Christian Doczkal (Université Côte d’Azur, Inria Sopia Antipolis Méditerranée, France) y
  • Damien Pous (Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France).

Su resumen es

We present a library for graph theory in Coq/Ssreflect. This library covers various notions on simple graphs, directed graphs, and multigraphs. We use it to formalise several results from the literature: Menger’s theorem, the excluded-minor characterization of treewidth-two graphs, and a correspondence between multigraphs of treewidth at most two and terms of certain algebras.

El trabajo se ha publicado en el Journal of Automated Reasoning

El código de las correspondientes teorías se encuentra aquí.

Reseña: Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi

Sus autores son

Su resumen es

It is nowadays customary to organize libraries of machine checked proofs around hierarchies of algebraic structures. One influential example is the Mathematical Components library on top of which the long and intricate proof of the Odd Order Theorem could be fully formalized. Still, building algebraic hierarchies in a proof assistant such as Coq requires a lot of manual labor and often a deep expertise in the internals of the prover. Moreover, according to our experience, making a hierarchy evolve without causing breakage in client code is equally tricky: even a simple refactoring such as splitting a structure into two simpler ones is hard to get right. In this paper we describe HB, a high level language to build hierarchies of algebraic structures and to make these hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder and abbreviation that let the hierarchy developer describe an actual interface for their library. Behind that interface the developer can provide appropriate code to ensure retro compatibility. We implement the HB language in the hierarchy-builder addon for the Coq system using the Elpi extension language.

El código de HB se encuentra aquí.

Reseña: Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq

Se ha publicado un artículo de razonamiento formalizado en Coq sobre teoría de categorías titulado Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq

Sus autores son

Su resumen es

(co)Monads are used to encapsulate impure operations of a computation. A (co)monad is determined by an adjunction and further determines a specific type of adjunction called the (co)Kleisli adjunction. Mac Lane introduced the comparison theorem which allows comparing these adjunctions bridged by a (co)monad through a unique comparison functor. In this paper we specify the foundations of category theory in Coq and show that the chosen representations are useful by certifying Mac Lane’s comparison theorem and its basic consequences. We also show that the foundations we use are equivalent to the foundations by Timany. The formalization makes use of Coq classes to implement categorical objects and the axiom uniqueness of identity proofs to close the gap between the contextual equality of objects in a categorical setting and the judgmental Leibniz equality of Coq. The theorem is used by Duval and Jacobs in their categorical settings to interpret the state effect in impure programming languages.

El trabajo se ha publicado en Mathematics in Computer Science.

El código de las correspondientes teorías se encuentra aquí.

José A. Alonso

2020-02-16 dom 19:07

Reseña: A comprehensive framework for saturation theorem proving

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre lógica titulado A comprehensive framework for saturation theorem proving.

Sus autores son

Su resumen es

One of the indispensable operations of realistic saturation theorem provers is (backward and forward) deletion of subsumed formu- las. In presentations of proof calculi, however, this is usually discussed only informally, and in the rare cases where there is a formal exposition, it is typically clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but using a standard notion of redundancy, a clause C does not make an instance Cσ redundant.

We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It permits us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of, e.g., an Otter or DISCOUNT loop prover implementing the calculus. Our framework is mechanized in Isabelle/HOL.

El trabajo es parte del proyecto Matryoshka (Fast interactive verification through strong higher-order automation)

El código está incluido en el repositorio IsaFoL (Isabelle Formalization of Logic).

Reseña: A formalised polynomial-time reduction from 3SAT to Clique

Se ha publicado un artículo de razonamiento formalizado en Coq sobre SAT titulado A formalised polynomial-time reduction from 3SAT to Clique.

Sus autor es Lennard Gäher del Programming Systems Lab en la Universidad del Sarre (en inglés, Saarland University y en alemán Universität des Saarlandes) en Saarbrücken, Alemania.

Su resumen es

We present a formalisation of the well-known problems SAT and Clique from computational complexity theory. From there, a polynomial-time reduction from 3SAT, a variant of SAT where every clause has exactyly three literals, is developed and verified. All the results are constructively formalised in the proof assistant Coq, including the polynomial running time bounds. The machine model we use is the weak call-by-value lambda calculus.

El trabajo forma parte de su Bachelor’s Thesis y está dirigido por Fabian Kunze.

Reseña: A formal proof of the irrationality of ζ(3)

Se ha publicado un artículo de razonamiento formalizado sobre teoría de números titulado A formal proof of the irrationality of ζ(3).

Sus autores son

Su resumen es

This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant. This result was first presented by Apéry in 1978, and the proof we have formalized essentially follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations performed by computer algebra algorithms in a Maple session. The rest of the proof combines arithmetical ingredients and asymptotic analysis, which we conduct by extending the Mathematical Components libraries.

El código de las correspondientes teorías se encuentra aquí.

Reseña: The space of mathematical software systems

Se ha publicado recopilatorio sobre sistemas informáticos en matemática titulado The space of mathematical software systems.

Sus autores son

Su resumen es

Mathematical software systems are becoming more and more important in pure and applied mathematics in order to deal with the complexity and scalability issues inherent in mathematics. In the last decades we have seen a cambric explosion of increasingly powerful but also diverging systems.

To give researchers a guide to this space of systems, we devise a novel conceptualization of mathematical software that focuses on five aspects: inference covers formal logic and reasoning about mathematical statements via proofs and models, typically with strong emphasis on correctness; computation covers algorithms and software libraries for representing and manipulating mathematical objects, typically with strong emphasis on efficiency; tabulation covers generating and maintaining collections of mathematical objects conforming to a certain pattern, typically with strong emphasis on complete enumeration; narration covers describing mathematical contexts and relations, typically with strong emphasis on human readability; finally, organization covers representing mathematical contexts and objects in machine-actionable formal languages, typically with strong emphasis on expressivity and system interoperability.

Despite broad agreement that an ideal system would seamlessly integrate all these aspects, research has diversified into families of highly specialized systems focusing on a single aspect and possibly partially integrating others, each with their own communities, challenges, and successes. In this survey, we focus on the commonalities and differences of these systems from the perspective of a future multi-aspect system. Our goal is to give new researchers, existing researchers from each of these communities, or outsiders like mathematicians a basic overview that enables them to match practical challenges to existing solutions, identify white spots in the software space, and to deepen the integration between systems and paradigms.

Reseña: “Proof pearl: Braun trees”

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Proof pearl: Braun trees.

Sus autores son

Su resumen es

Braun trees are functional data structures for implementing extensible arrays and priority queues (and sorting functions based on the latter) efficiently. Some well-known functions on Braun trees have not yet been verified, including especially Okasaki’s linear time conversion from lists to Braun trees. We supply the missing proofs and verify all of these algorithms in Isabelle, including non-obvious time complexity claims. In particular we provide the first linear-time conversion from Braun trees to lists. We also state and verify a new characterization of Braun trees as the trees t whose index set is the interval {1,…, size of t}.

El trabajo se presentará en el POPL 2020 (47th ACM SIGPLAN Symposium on Principles of Programming Languages) el próximo 20 de enero.

El código de las correspondientes teorías se encuentra en AFP.

Reseña: Proving tree algorithms for succinct data structures

Se ha publicado un artículo de razonamiento formalizado en Coq sobre algorítmica titulado Proving tree algorithms for succinct data structures.

Sus autores son

Su resumen es

Succinct data structures give space efficient representations of large amounts of data without sacrificing performance. In order to do that they rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different succinct tree algorithms. One is the Level-Order Unary Degree Sequence (aka LOUDS), which encodes the structure of a tree in breadth first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary red-black trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient Insert and Delete. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.

El trabajo se ha presentado el 30 de agosto en el JSSST 2018 (The 35th Meeting of the Japan Society for Software Science and Technology).

El código de las correspondientes teorías se encuentra GitHub.

Reseña: Formal verification of a geometry algorithm (A quest for abstract views and symmetry in Coq proofs)

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs.

Su autor es Yves Bertot (del grupo MARELLE del INRIA, Sophia Antipolis).

Su resumen es

This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex notions are those of boundary and separating edges. When performing proofs about this algorithm, questions of symmetry appear and this exposition attempts to give an account of how these symmetries can be handled. All this work relies on formal developments made with Coq and the mathematical components library.

El trabajo se presentará el 16 de octubre en el ICTAC 2018 (15th International Colloquium on Theoretical Aspects of Computing).

El código de las correspondientes teorías se encuentra en GitLab.