Lambda the Ultimate

Well, in category we are familiar with repesenting sketches both as figures on paper, and as formal constructions. But the purpose of the theory of sketches is to validate the reasoning category theorists actually do with commutative diagrams.

It is key that an instance of a geometrically valid inference might be a construction drawn by hand on a piece of paper. That drawing has a form that might or might not be valid in this Euclidean system.

Put this another way: one might say one has constructed in Coq a proof of the fundamental theorem of arithmetic. Would you say that this way of speaking is incorrect, because one has only really constructed a digital artefact that is hanging on the side of the true proof?

I wasn't arguing that there is no such thing as diagrammatic reasoning, but rather that in this case, diagrams aren't playing such a big role. I don't see this as akin to reading a map or commutative diagram, where certain properties can be read off from the diagram directly. Here, in geometry, we can have A < B < C < D shown on a line, with that relative ordering fixed by construction except the relative order of B and C. The geometrical relations of interest aren't captured by any particular diagram.

If you'll look at section 3.3, you'll see a list of symbolic inferences that are permitted. That they are justified by consideration of diagrams seems irrelevant to me - the rules of most formal systems are ultimately justified by informal reasoning about the thing the system is supposed to model. The formal system itself is, nonetheless, symbolic. I don't object to calling this diagrammatic reasoning because I don't think such a thing could exist. On the contrary, it's because I can think it can exist, and don't think this is it.

my experiences with model-driven development have led me to believe Jon Barwise was the logician who has had the largest impact on this field, but also as a group the Visual Inference Laboratory at Indiana University that he led. Barwise, from what I can tell, has had a huge impact on systems theorists disguised as UML weenies.

Barwise and Etchemendy's seminal paper on the theory of visual inferences is probably the best starting point. See: Visual information and valid reasoning. Purchaseable via a book of collected works, like this one. If anybody knows of an online copy to share, please reply to this.

How exactly did Barwise influence UML? There are definitely some influences on UML from the 'visual reasoning' community, particularly the use of higraphs for state diagrams (and UML 1.x activity diagrams). However, UML was clearly never intended to be a platform for rigorous inference: even the most 'basic' "UML infrastructure" metamodel is an elephantine monstrosity.

Barwise's paper is not available online AFAICT, but searching for papers which reference it turns up several interesting articles.

Re: searching for papers which reference it turns up several interesting articles..

Note to self: This looks interesting: Computers, visualization, and the nature of reasoning by Barwise and Etchemendy.

How exactly did Barwise influence UML?

Not noticeably, as you say. His work has a bigger influence on formal diagrammatic systems like constraint diagrams: e.g. Stapleton's A Decidable Constraint Diagram Reasoning System. These diagrams are intended to take the place of OCL for specifying invariants etc. They've not taken off in that domain, of course, but are an interesting topic in their own right, and we can but hope. (I'm a student with the Visual Modelling Group at Brighton, which has had a big part in producing the theoretical framework for constraint diagrams, and also interesting work on generating and drawing diagrams based on Euler circles...if anyone's interested, our publications page gives a flavour, although it's out of date.)

I've noticed you've replied a couple of times to things I've said regarding visual languages, and you generally have bright things to say. Maybe you should be a contributing editor for LtU and post some of the more interesting diagrammatic reasoning papers you come across.

Thanks for mentioning where you do your work, too. I tried looking you up about a year ago but Jim Burton is an exceedingly common name.

I don't think Barwise has had much influence on the UML, but he has influenced people who are interested in modeling languages and tend to use UML just because (a) it is object-oriented [as opposed to modeling notations like IDEF which are mainly brain damaged government contraptions from the era when structured programming with COBOL vision where the supermarket grocery clerk would be your "coder"] (b) it is ubiquitous.

As for activity diagrams, I think those are pure and utter crap and feel bad for anyone who has ever had to look at one, especially an IBM-esque one with utter nonsense like "conditional threads". My opinion on activity diagrams is mainly methodological, since they are inherently non-OO (from a methodology standpoint, they encourage functional decompositions that lead to sequential coupling, and decrease re-use and composition of what otherwise could be autonomous entities). However, they also contain a ton of feature bloat that mainly exists to model 3GL code visually. Let me re-assert, as I have many times here before, that going down this reverse engineering route is a slippery slope and probably a guaranteed bad idea.

EDIT: I also don't think UML 2.x is that much worse than any other metalevel modeling tool, such as the Common Lisp Object System. UML is simply purely bigger than CLOS (which is itself enormous), and so as complexity tends to increase combinatorically with feature count, UML is correspondingly complex and bug-ridden. That's why you use Profiles to limit the scope of UML, thus reducing the feature count and likelihood of interacting with "bugs" in the specification. The major downside of UML is increasing generality in the execution model removes some elegance from using a simpler methodology directly. Subsetting then becomes a burden. To loosely quote belated comedian Mitch Hedburg, I don't like Pepperidge Farm, because that stuff is too fancy. It's wrapped twice. I don't need another step between me and toast.

Can't remember now if I liked Logic and Visual Information by Eric M. Hammer, but given how short it is, I heartily recommend it to anyone interested in the subject.

For instances of 'formal diagrammatic reasoning' in actual VPLs, you might be interested in the work I pointed out earlier by John Baez and others about string diagrams in monoidal categories. There were also useful pointers in the thread about 'function concatenation'(link).

Dan Piponi has pointed out that similar diagrams can apply to commutative monads [slides] [video]. (ISTM that extending them to the non-commutative case should be straightforward by adding a notation for 'barriers').

That Selinger paper is really nice! I should look for a warm and friendly introduction to monoidal categories, so that I can post it as a prequel to the Selinger.

Anyway, a variant of sigfpe's observation is in Benton and Wadler's 1996 paper on monads and linear logic: any commutative monad gives rise to a model of intuitionistic logic (ie, a symmetric monoidal closed category). But if you see an easy way to extend that to the noncommutative case, I urge you to write it up -- it wasn't until just last year that Alex Simpson & co. figured out what linear-logic-ish term language corresponds to noncommutative monads.

I should look for a warm and friendly introduction to monoidal categories

The Baez paper seems warm and friendly enough (and it gives a notation for the cartesian closed case, which Selinger doesn't!) but I suppose you could find something even friendlier in Baez's other writings, including old issues of This Week's Finds

it wasn't until just last year that Alex Simpson & co. figured out what linear-logic-ish term language corresponds to noncommutative monads.

If a proper correspondence wasn't given until last year, that probably means I was thinking about a very special case. But since most practical uses of monads boil down to 'forcing function calls w/ side effects to be sequenced in the order you want', even ad-hoc special-case support could be very useful.