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

PorJosé A. Alonso

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

PorJosé A. Alonso

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

PorJosé A. Alonso

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)

PorJosé A. Alonso

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

PorJosé A. Alonso

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.