[Aldor-l] Aldor-Meet and meets in general

[David Casperson]

On 2007-11-20, Jacques Carette wrote:

> Date: Tue, 20 Nov 2007 11:26:12 -0500
> From: Jacques Carette <carette at mcmaster.ca>
> To: Bill Page <bill.page at newsynthesis.org>
> Cc: aldor-l <aldor-l at aldor.org>
> Subject: Re: [Aldor-l] Aldor-Meet
> 
> Bill Page wrote:
>> In general I would not simply accept any as the "authority". I think
>> that would lead to the kind of subjective idiosyncrasies that we see
>> in most other languages. Rather I would very much rather that the
>> language be based on some commonly accepted theory - the more general
>> the better (e.g. category theory :-).
> In which case I would argue that Meet should be either some kind of
> pullback or (co)cone in the category of theories and theory morphism
> over an appropriate logic.
>
> See any of:
> 1) Bart Jacob's book "Categorical Logic and Type Theory",
> http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html
> 2) Jose Fiadeiro's book "Categories for Software Engineering"
> http://www.fiadeiro.org/jose/CATBook/
> 3) Joseph Goguen's "Types as theories"
> http://portal.acm.org/citation.cfm?id=135134
> 4) Tom Maibaum's "Theories as Types",
> de Queiroz R J G B, Maibaum, T S E, "Abstract Data Types and Type
> Theory: Theories as Types" Zeitschrift fur Mathematische Logik und
> Grundlagen der Mathematik, Vol 37, (1991), 149-166.
>
> along these lines,
> 5) Zhaohui Luo's "A higher order calculus and theory abstraction" is
> also relevant, http://portal.acm.org/citation.cfm?id=106148.106154
>
> But of course pushouts (called Join in Aldor) have much clearer use
> cases.   In the  "little theories" approach,  which  the  designers of
> Axiom/Aldor seemed that have intuitively rediscovered (but never
> properly formalized),  most Categories and Domains would be done via
> Joins and other means of assembly from smaller pieces.
>
> Jacques

The question of meets and joins of categories has also been
studied in some detail in the universal algebra community, the
seminal work being done by Walter Taylor on the Lattice of
Interpretability Types of Varieties.

Here the elements of the (BIG) lattice are equivalence classes,
and the elements of the equivalence classes are varieties, that
is classes of algebras that satisfy a common equational theory.
Groups, Abelian Groups, Rings, Distributive Lattices, Boolean
Algebras, Boolean Rings, etc., are examples of varieties.
Birkhoff's theorem gives an equivalent definition of a variety:
it is a collection of algebras closed under homomorphic images,
cartesian products, and subalgebras.

The equivalence relation is mutual interpretability: without
going into details it should come as no surprise that Boolean
Rings and Boolean Algebras are mutually interpretable.  There are
some surprises:  Sets and Semigroups are mutually interpretable,
as pi1(x,y)=x gives an acceptable associative multiplication for
any set.

In this lattice join means bigger theories (more equations) and
smaller varieties (less algebras === models).  The language of
the join is the union of the languages of the varieties involved,
and the models must obey the unions of the theories.  This idea
is exemplified by LinearlyOrderedGroups being simultaneously
LinearlyOrdered and Group.  Here, all that Aldor misses is the
ability to insist that the domains of the join simultaneously
satisfy axioms of both joinands.

However, in this lattice the meet operation is not so simple to
describe.  There are more models, in fact the models are exactly
the set-theoretic cartesian product of a model from the first
category and a model from the second.  BUT, the language of
the meet is also BIGGER, consisting of the union of the languages
of the meetands, TOGETHER WITH a new * operation.  (Strictly
speaking it is not correct to speak of the language of the meet,
as the meet really takes place on equivalence classes, and I am
talking about the language of a particular variety in that class.)

All of this suggests that simply intersecting the lists of
operations of categories is likely to be naive.  We should avoid
trying to add Meet to the Aldor language machinery (or at least
calling it Meet) until we have a reasonably clear idea of what
kind of category theoretic idea we are trying to capture.

David
-- 
Dr. David Casperson, Assistant Professor     |  casper at unbc.ca
Department of Computer Science               |  (250)   960-6672 Fax 960-5544
College of Science and Management            |  3333 University Way
University of Northern British Columbia      |  Prince George, BC   V2N 4Z9
                                              |  CANADA