Re: On UA-CAT Workshop at MSRI - Empty Carriers
I'm glad to see this discussion. In the book that I am (still) writing, I went to some length to do all the universal algebra with explicit lists of variables. At times, I have wondered whether this was syntactic overkill. However, it makes for clean completeness theorems and existence of initial algebras. In addition, it meshes well with later chapters on typed lambda calculi, where contexts (lists of variables and their types) are needed. One minor question, while I am thinking of it. I used "sort" in the chapter on algebra, and "type" in the chapters on lambda calculi, etc. What do the UA-literate think about using "type" uniformly throughout? Would it be offensive to simplify terminology this way? BTW, there is not much math in the chapter on UA, just soundness, completeness, homomorphisms, initiality, and a number of CS examples (stacks, queues, trees, ...), ending with a brief overview of rewrite systems. John Mitchell ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
I, too, have been frustrated for many years at the proscription of empty algebras. However, I feel that there may be some movement in people's positions from time to time, which may continue if we all try to be diplomatic. I would add that I don't think universal algebraists are the only ones that have this particular opinion. The logicians tend to require structures to be nonempty. I believe this goes back to a decision by Tarski, although I certainly wasn't there. Given the strong allegiance some universal algebraists have to logic, I think that it would be important to try to have a dialog with the logicians about this. Thus, I was very interested in Dr. Barr's remarks concerning a better definition of ultraproducts. About _types_ and _sorts_: I think they are different. To me, a _type_ is an N-tuple of sets S_n, where elements of S_n are n-ary basic operations. There is a free functor from types to clones (or theories), and a forgetful functor the other way. However, in this situation, there would only be one _sort_. For what it's worth, I have a half-written paper that allows any category of sorts, with an additional structure of operations from limits of diagrams in the sort category (which limit might not exist!) back to objects in the sort category. I sent in an abstract about this to the UACT conference. Unfortunately, I seem to have put that project on the back burner. Bill Rowan ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
John Mitchell wrote
I'm glad to see this discussion. In the book that I am (still) writing, I went to some length to do all the universal algebra with explicit lists of variables. At times, I have wondered whether this was syntactic overkill. However, it makes for clean completeness theorems and existence of initial algebras. In addition, it meshes well with later chapters on typed lambda calculi, where contexts (lists of variables and their types) are needed.
You might have a look at my chapter on "Basic Category Theory" in the "Handbook of Logic in Computer Science (Abramsky, Gabbay, maibaum eds.), OUP, 92. There I follow your program to use an explicit list of free variables which gives a reasonable account how composition in categories relates to substitution on free variables (as opposed to application where bound variables are substituted) (mainly in sections 1,2, 8).
One minor question, while I am thinking of it. I used "sort" in the chapter on algebra, and "type" in the chapters on lambda calculi, etc. What do the UA-literate think about using "type" uniformly throughout? Would it be offensive to simplify terminology this way?
in principle not, but it seems that UAs use sorts for the syntactic entities and types for the semantic ones. In a way, type theory talks about both levels. Axel Poigne ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Bill Rowan says that -
...To me, a _type_ is an N-tuple of sets S_n, where elements of S_n are n-ary basic operations.
"Signature" is used for this notion (or many-sorted generalizations) often enough that I feel it could be standard. Steve Vickers. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
participants (4)
-
John C. Mitchell -
poigne＠gmd.de -
rowan＠garnet.berkeley.edu -
sjv＠doc.ic.ac.uk