Artículo
Formalization of Universal Algebra in Agda
Fecha de publicación:
10/2018
Editorial:
Elsevier
Revista:
Electronic Notes in Theoretical Computer Science
ISSN:
1571-0661
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
In this work we present a novel formalization of universal algebra in Agda. We show that heterogeneous signatures can be elegantly modelled in type-theory using sets indexed by arities to represent operations. We prove elementary results of heterogeneous algebras, including the proof that the term algebra is initial and the proofs of the three isomorphism theorems. We further formalize equational theory and prove soundness and completeness. At the end, we define (derived) signature morphisms, from which we get the contravariant functor between algebras; moreover, we also proved that, under some restrictions, the translation of a theory induces a contra-variant functor between models.
Palabras clave:
EQUATIONAL LOGIC
,
FORMALIZATION OF MATHEMATICS
,
UNIVERSAL ALGEBRA
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(CCT - CORDOBA)
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Citación
Gunther, Emmanuel; Gadea, Alejandro Emilio; Pagano, Miguel Maria; Formalization of Universal Algebra in Agda; Elsevier; Electronic Notes in Theoretical Computer Science; 338; 10-2018; 147-166
Compartir
Altmétricas