7
$\begingroup$

Goguen has popularized the initial algebra view of semantics via his "no junk, no confusion" slogan. By "no junk", he means that models of a theory presentation should not have unnecessary elements, and "no confusion" that terms should not be mapped to equal values unless they are provably equal. Sometimes, "no junk" is also interpreted as every element in the model is a denotation of a term, while "no confusion" as two different terms denote different elements in the model. [These are classically equivalent statements, but they are not intuinistically equivalent, so I mention both].

My questions are:

  1. What is a 'good' formalization of this slogan? By this I mean an explicit statement of "no junk, no confusion" in the meta-logic (since we're talking about models), where the logical strength of the corresponding statement is well understood.

  2. Are there logics in which these requirements can be internalized?

  3. What would be the corresponding slogan to "no junk, no confusion" for final coalgebras?

Improve this question
$\endgroup$
2
  • $\begingroup$ I don't understand this question. What are the "explicit" and "corresponding" statements? Your "sometimes" interpretation admits a familiar formalisation, so I assume that is not what you are after. The classical and intuitionistic renderings are both pi-0-2 properties, so it is quite likely that one is provable for a model iff the other is. $\endgroup$
    – Charles Stewart
    Feb 24, 2010 at 8:35
  • $\begingroup$ I tried to clarify by editing the question. I mean an explicit statement of "no junk, no confusion" - for example, your classical and intuinistics renderings as explicit pi-0-2 properties. Yes, a statement like 'every element in the model is a denotation of a term' is easy to formalize in the meta-theory -- but is it the 'right one? And is there some way to internalize that statement? $\endgroup$
    – Jacques Carette
    Feb 24, 2010 at 12:53

3 Answers 3

Reset to default
7
$\begingroup$

The way I understand each of the slogans is as follows:

  1. "No junk" I just take to mean that an appropriate induction principle is valid -- that is, we should look for initial models in the appropriate category of algebras for the theory. This also implies that every element of the model is in the image of the interpretation of the the algebraic theory.

    Presumably the dualization to coalgebras would just be the validity of using bisimilarity to prove equality.

  2. "No confusion" is traditionally interpreted to mean that we should look for models in which two elements of the model are semantically equal if and only if the corresponding syntaxes are provably equal. This is the really bizarre requirement, since it amounts to requiring that the model be isomorphic to the term model! And yet Goguen and the algebraic specification community were emphatically not happy with decreeing the term model to be the intended model -- they work very hard to get the "right" model.

    I personally (ie, I don't know that anyone else believes this) take the way this requirement is phrased to be an artifact of the history of algebraic specification. IIRC, they started out with purely algebraic theories -- that is, theories in which the equational axioms are all pure equalities. (E.g., the axioms for groups.) Now, of course every such algebraic theory has a degenerate model, since the one-element model validates all equalities. So the no-confusion principle is intended to rule out such degenerate models.

    These days, of course, the algebraic specification crowd has no problem with theories with inequalities (e.g., the field axioms), and I think this additional freedom lets us state the no-confusion principle in a better way. Namely, we should design algebraic theories whose models are categorical. That is, we want theories for which all models are isomorphic. This implies the traditional no-confusion criterion, and also explains why people try to adjust the signature when they can't prove it. (Of course, this is a non-first-order property in general, as you need higher-order logic or set theory to quantify over models.)

Improve this answer
$\endgroup$
4
  • $\begingroup$ A small point: when an induction principle is not available it may often be replaced by initiality or universality. What I mean is for example the universal property of classifying models in categorical logic. $\endgroup$
    – Andrej Bauer
    Feb 24, 2010 at 22:05
  • $\begingroup$ Thank you, this definitely answers some of my questions. My impression of the history of algebraic specifications is akin to yours: there was too much early emphasis on equational theories and equational logic. Luckily moving to institutions seemed to help in that respect. I am still looking for ideas on how to internalize (a proper interpretation of) as much of "no junk, no confusion" into a logic as possible [like Bill Farmer's Chiron, which allows one to talk about both syntax and semantics]. $\endgroup$
    – Jacques Carette
    Feb 25, 2010 at 0:17
  • $\begingroup$ "No junk" I just take to mean that an appropriate induction principle is valid - This isn't right for the most obvious interpretation of "appropriate": nonstandard models of PA satisfy the (first-order) induction principle, but they are the very picture of "has junk". You need something like "freely generated", I think. $\endgroup$
    – Charles Stewart
    Feb 25, 2010 at 8:42
  • $\begingroup$ "No confusion" - I like what you say very much. It's obviously analogous to the question of what role "abstractness" plays in the term "fully abstract model". $\endgroup$
    – Charles Stewart
    Feb 25, 2010 at 8:44
4
$\begingroup$

Belatedly, an answer in set-based situations to

  1. What would be the corresponding slogan to "no junk, no confusion" for final coalgebras?

Given an initial algebra, any algebra will have a special subobject which is the image of the initial structure. The subobject may have confused elements (terms) of the initial algebra, and the object may have extra junk. A map between objects will map the first special subobject to the second, possibly confusing more. The initial algebra has no confusion and no junk.

Given a final/terminal coalgebra, the elements of any coalgebra will have a special colouring in terms of images in the elements of the terminal structure. The object may have more than one element with the same colour, and the object may not use all the colours. A map between objects will preserve the colouring, the domain possibly using fewer colours. The terminal coalgebra colours without ambiguity and without redundancy. If two things behave the same way, they are the same; all behaviours are covered.

No junk, no confusion; No redundancy, no ambiguity.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Late, but a nice contribution. I like your co-slogan. $\endgroup$
    – Jacques Carette
    Mar 13, 2012 at 12:04
-4
$\begingroup$

The slogan is a meaningful english phrase. After removing negation, we may obtain this phrase: "stay clean, stay clear". So then, here is an actual theorem of quantified boolean formulas that describes both qualities formally:

Linear Corollary: Quantified monotone boolean formulas are linearly decidable.

That is, no matter how many alternating quantifiers are in the prefix, when the body of the formula has "zero negations," then the monotonicity of the formula makes any quantifier prefix linearly decidable; plug T for existentially quantified variables, NIL for universally quantified variables, then evaluate the boolean form, entirely linear in the size of the QBF.

Goguen may also enjoy the car/cdr Structure of Common Sense: Good ideas Usually have Two words.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ I do not think this is helpful/topical (although the linear corollary is interesting as a result on its own). And I do not believe that your negation-removal was meaning-preserving! $\endgroup$
    – Jacques Carette
    Feb 23, 2010 at 22:51
  • $\begingroup$ The Plus Transfrom gave a nearly equivalent english phrase; but the minus votes indicate an error somewhere...hmmm. "monotone" does also include formulas where every proposition is negative; however, I considered that presentation to be confusing junk, in a simple propositional formalism... I use monotone formulas for loop management in complex programs that solve QBFs; "correctness and clarity" are both of the utmost importance in such programs. Correctness is related to "no junk" and "clarity" allows code maintenance and improvements. Removing negation is standard treatment for me. $\endgroup$
    – daniel pehoushek
    Feb 26, 2010 at 18:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.