Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic

2013 ◽  
Author(s):  
Marcelo Fiore ◽  
Makoto Hamana
Keyword(s):  
Equational Logic ◽  
Algebraic Theories

scholarly journals On generalized algebraic theories and categories with families

2021 ◽  
pp. 1-18
Author(s):  
Marc Bezem ◽  
Thierry Coquand ◽  
Peter Dybjer ◽  
Martín Escardó
Keyword(s):  
Type Theory ◽  
Algebraic Theory ◽  
Completeness Theorem ◽  
Small Category ◽  
Equational Logic ◽  
Algebraic Theories ◽  
Semantic Notion ◽  
Finitely Presented ◽  
Extra Structure

Abstract We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwFΣ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwFΣ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Löf type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.

Elgot’s Analysis of Monadic Computation

1982 ◽  
Vol 5 (2) ◽  
pp. 171-186
Author(s):  
Stephen L. Bloom
Keyword(s):  
Algebraic Theories

A review is given of some of the late C.C. Elgot’s ideas on the syntax and semantics of monadic flowchart algorithms. In particular, the motivation for his “iterative algebraic theories” is explained.

Remarks on remarks on many-sorted equational logic

1987 ◽  
Vol 22 (4) ◽  
pp. 41-48 ◽  
Author(s):  
J A Goguen ◽  
J Meseguer
Keyword(s):  
Equational Logic

Interpolation in Conditional Equational Logic1

1991 ◽  
Vol 15 (1) ◽  
pp. 80-85
Author(s):  
P.H. Rodenburg
Keyword(s):  
Interpolation Theorem ◽  
Equational Logic ◽  
Craig’S Interpolation Theorem ◽  
Natural Formulation

In a natural formulation, Craig’s interpolation theorem is shown to hold for conditional equational logic.

Completeness of many-sorted equational logic

1982 ◽  
Vol 17 (1) ◽  
pp. 9-17 ◽  
Author(s):  
J. A. Goguen ◽  
J. Meseguer
Keyword(s):  
Equational Logic

Dagger extension theorem

2011 ◽  
Vol 21 (5) ◽  
pp. 1035-1066 ◽  
Author(s):  
Z. ÉSIK ◽  
T. HAJGATÓ
Keyword(s):  
Unique Solution ◽  
Extension Theorem ◽  
Sufficient Condition ◽  
Iteration Theory ◽  
Additive Structure ◽  
Algebraic Theories ◽  
Constant Morphism

Partial iterative theories are algebraic theories such that for certain morphisms f the equation ξ = f ⋅ 〈ξ, 1p〉 has a unique solution. Iteration theories are algebraic theories satisfying a certain set of identities. We investigate some similarities between partial iterative theories and iteration theories.In our main result, we give a sufficient condition ensuring that the partially defined dagger operation of a partial iterative theory can be extended to a totally defined operation so that the resulting theory becomes an iteration theory. We show that this general extension theorem can be instantiated to prove that every Elgot iterative theory with at least one constant morphism 1 → 0 can be extended to an iteration theory. We also apply our main result to theories equipped with an additive structure.

Fuzzy equational logic

2002 ◽  
Vol 41 (1) ◽  
pp. 83-90 ◽  
Author(s):  
Radim Bělohlávek
Keyword(s):  
Equational Logic

Algebraic theories and algebraic categories

2011 ◽  
pp. 10-20
Author(s):  
J. Adamek ◽  
J. Rosicky ◽  
E. M. Vitale ◽  
F. W. Lawvere
Keyword(s):  
Algebraic Theories
Sign in / Sign up

Export Citation Format

Share Document