Lambda the Ultimate

This book clarifies it so much! I wasn't far off the mark after all!

Analogies and metaphors can be made implicit, even emergent if conceptual 'mappings' are treated as categories, by virtue that composition is associative.

An example:
grizzly bears can be thought of as being mapped maybe to ferocity and possibly strength, strength may be mappable to the idea of strong things, and strong things may map to steel bars. So one making a metaphor, grizzly's are the steel bars of the mountain, could be viewed as making an association of f: grizzly->strength, g: strength->strong things; h: strong things->steel bars such that h.g.f which equals (h.g).f = h.(g.f). which seems trivial in this small example, but blow the #functions to 100, 1000, 1000000. The point groups of composed functions could be partially triggered, results 'combined and it wouldn't matter' so let h.g = a; then a.f. The point is there is no 'hardwiring' of metaphors; they are naturally arising just from using categories.

thanks!

As to why category theory has been "more useful" (in parts of mathematics and computer science) than set theory has been, this is because sets are sort of "impoverished." They deliberately lack structure, being just bags or collections of points, with no implied connection between the points and relatively few tools for discussing how the collections may change (for example, over time, one of our most important "journey-like" mappings).

And that's where relations, functions, and predicates come in. Basically, then, category theory is a refined integration of both set theory and the world of functions.

. . .

So, I suppose natural transformations or functors can be used as a way to model dynamic (lower-order) morphisms.

. . .

So, I guess I need to figure out if category theory, compared to a higher-order predicate logic, would make both a better programming language and a better database model.

. . .

Thanks again.

And that's where relations, functions, and predicates come in. Basically, then, category theory is a refined integration of both set theory and the world of functions

In some sense, yes, but it can also be seen as more primitive than set theory with functions. Part of the usefulness fo category theory is in its abstraction; arrows (or morphisms, whichever name you prefer) are taken as primitives: we don't say what they are, simply that they exist and have certain properties. Certainly, if you think in terms of sets, then arrows look rather like functions, but that doesn't mean that arrows are functions, simply that they can be viewed that way in some contexts. If we are interested in the category of open sets in a topological space, then arrows are inclusion relations, not functions. In other contexts they can be more bizarre still. You don't need to think in terms of sets and functions to be able to use category theory, and in many ways that is where it's power comes from.

A more useful way to think about category theory compared to set theory is to view it as a kind of inversion of reasoning. In set theory everything is built up, and we understand objects by seeing what they are made of -- picking apart their internals. We relate two objects by comparing what they are made of. Category theory turns that on its head and takes relationships between objects as primitive. From CT's point of view objects are opaque; we understand an object not by peeking inside at it's internal structure, as we would if we were using set theoretic thinking, but rather by examining how the object relates to other objects.

I understand that might be high level and abstract, but I'm a mathematician, so I can't give you CS examples very easily.

I understand that might be high level and abstract, but I'm a mathematician, so I can't give you CS examples very easily.

The obvious CS analogy is an abstract data type. For example, a stack is some type 'S a' where we have operations:
empty : S a
push : a -> S a -> S a
pop : S a -> 1+S a
top : S a -> 1+a

with equations like:
top empty = pop empty = inl ()
pop (push x xs) = inr xs
top (push x xs) = inr x

Now any implementation of "stacks" that satisfies the above is acceptable.

Thanks for that explanation.

I think we and other creatures chunk the world into pieces we can understand by finding the mappings and functors and so on which allow us to grok the world. We are, I think, category theory engines.

If I'm reading you correctly, when it comes to how we perceive the world, psychologist J.J. Gibson called these "affordances." Google's telling me that the AI set's already delved into what affordance theory means for artificial intelligence, but I can't speak to much beyond that because my brain would melt.

Thank you for bringing up the issue of "affordances." This whole area is closely related to Heidegger's approach to being, being in the world, readiness to hand, thrownness, and to ontology. (The links to programming are not yet clear, or at least do not seem to be widely used by programmers. Even in AI. I think they will be, eventually.)

A very readable paper on the Heidegger/Gibson point of view is by two psychologists, Zahorik and Jenison:

http://wavelet.psych.wisc.edu/Zahorik_Jenison.pdf

This impinges on data bases and object ontologies, as this quote hints at:

"Instead of researchers building an artificial intelligence system in which properties of objects are construed as sets of atomistic, determinate features (the rationalist procedure), things in the world are instead incorporated into the system, or formalized according to their potentials for action/intereaction with the system itself, their "readiness-to-hand." A basketball is not represented by the features _round_, _orange_, and _rubber_, but instead is viewed for its _throwabiity_, its _rollability_, or its _bouncability_ by the system." (p. 7)

In Gibson/Norman terms, an actor encountering a basketball is more reactive, more _interested_ in, the latter features and not the purely physical or chemical properties.

I suspect this is the direction AI programming, and even Web ontologies (Web 3.0?), aka "the semantic Web" (Berners-Lee, etc.) will need to go. In terms of our kind of languages, this suggests:

-- much more than just "declarative" (a la logic or functional language)

-- more _process_ oriented (mappings) than _object_ oriented

-- categories, functors, and even n-categories

Languages which support very rich kinds of mappings/relations seem to have big advantages over even languages with "logic" (at the first order predicate calculus level) and "object" support.

One of the flaws in CYC is, I think, the almost completely "flat" data base of a vast number of logical assertions ("a basketball is round") without higher-level mappings of the sort that category theory may help to provide. Searle's "Chinese room" is another way to look at this.

To make a probably obvious point, the functional programming point of view may turn out to be much more useful than the object-oriented point of view, probably long anticipated by guys like McCarthy and Steele and all.

--Tim May

Also recommended is Haugeland's 1995 Mind Embodied and Embedded (which can be found in his collection Having Thought).

The problem with situatedness is that it can't be just defined "up to isomorphism". It is the opposite of a spiritual disembodied quality. Replacing object entities by relationships and naive facts about things by the way they might transform doesn't buy you much in this respect.

It raises the level of abstraction but I'm not sure it's just a revival of the old Bourbaki delusion: create an abstract framework ( burocracy ) and believe that it captures all relevant future efforts. Those will be just examples that fill gaps as special cases. In software development this delusion is expressed by the term "frameworkitis" that will always be attacked by more lightweight, situated and contextualized solutions that do not pretend to require states of a higher mind or other esoterica. I admit though it's hard to draw the lines between what is usefull and what is bogus - as always.

To make a probably obvious point, the functional programming point of view may turn out to be much more useful than the object-oriented point of view, probably long anticipated by guys like McCarthy and Steele and all.

I like that you finally talk about usefullness because this puts things on the ground. Otherwise I suspect some people will dismiss the usefullness of anything that wasn't built with the right attitude. So it might not bring anything further.

This direction sounds to me like it might be related to the Event Calculus, or to Transaction Logic. The Discrete Event Calculus Reasoner is a nice implementation of, of course, the Discrete Event Calculus and FLORA-2 is a very nice implementation of a combination of F-Logic, HiLog, and Transaction Logic in XSB Prolog, which can sit on top of any ODBC-compliant database. I'm quite impressed.

It seems very likely to me that, long term, what you're referring to will end up being an application of The Basic Intuitionistic Logic of Proofs (PDF) or something derived from it. A set of slides, also in PDF, giving a good overview can be found here. Related foundational papers would seem to include Explicit Provability and Constructive Semantics (PS) and Reflective lambda-calculus (PS). Note well: my impression derives from a regrettably superficial reading stemming from my near absolute ignorance of progress in logic (or, more accurately, logic education as a subset of computer science education in America) since the mid-1980's.

Ob. tie-in to LtU: I discovered the work on iBLP and related topics as a consequence of googling "constructive quantifiers" after Tim Sweeney used the phrase in a critique of A Very Modal Model of a Modern, Major, General Type System in private correspondence. To the extent that I understand Tim's critique at all, my interpretation is that he believes the type system in VMMMMGTS wouldn't be appropriate for a high-level language, but might be for the TILs and TALs that it is aimed at. In any case, I don't think it's entirely coincidental that "The technique... reduces mainly to defining a Kripke semantics of the Gödel-Löb logic of provability." (VMMMMGTS) and:

Brouwer-Heyting-Kolmogorov: a sentence is true if it has a proof, whereas proofs satisfy the following BHK conditions:

• A proof of A∧B consists of a proof of A and a proof of B,
• A proof of A∨B is given by presenting either a proof of A or a proof of B,
• A proof of A→B is a construction which, given a proof of A returns a proof of B,
• Absurdity ⊥ is a proposition which has no proof, ¬A is A→⊥

...
Major models for intuitionistic logic
...
8. Kripke models (1965)
...
None solves the original BHK problem!
...

• Big distraction and big help: Provability logic with []F ~ Provable(F) is modal system GL (Gödel-Löb—my emphasis) incompatible with S4. Though applications of GL have been mostly limited to Proof Theory, its mathematics provided a solid background for the solution of Gödel's problem.

...
The Logic of Proofs LP
...
Major features that differ LP from CL/λ-calculus.

• Polymorphism. Operation "+" yields multiple types, i.e. multi-conclusion proof terms.
• Dynamic typing. Collection of types assigned to a term can grow in a process of term building.
• A free mixture of types from different levels. CL/λ corresponds to a pure level 1 only.
• Self-referentiality of terms. In LP a type assignment t:F(t) is legal and supported by the standard arithmetical semantics.
• Internalization as an admissible rule. In CL/λ the Curry-Howard isomorphism relates level 0 (intuitionistic derivations) with the pure level 1 only.

...
Reflexive Combinatory Logic
...

from the slides linked above.

My apologies for the lengthy excerpting; I don't understand the material well enough to summarize effectively. I certainly intend to keep an eye on these developments.

Update: a more comprehensive set of slides seems to be attached to a course on Proof Polynomials that was part of the 9th Estonian Winter School in Computer Science.

It'll be too hard for me to snip-and-comment on Paul's points, so I'll just wing it freeform.

I agree that the likely trend is toward intuitionistic logic approaches. For example, the logic of "semidecidable propositions" (goes by several other names, and is associated with Abramsky, Hyland, Vickers, and several others). In these systems, one cannot prove a lot of things, only falsify them (by a counterexample). The classic case is of a black box emitting a stream of digits which look a lot like the digits of pi. One cannot prove that the box actually _is_ emitting the digits of pi (that is, that it will do to the end of time), only disprove that it is, by finding a case where it fails to emit what one knows (by other means) is some correct digit of pi.

This approach has much actual practical application: many systems behave as black boxes, at least to those other than the designers (the "God's eye view" that can look inside the box, and maybe prove things that external observers cannot--and even here, in something I hope to get to, there may be surprises, as in "But the laundry chute function was intended to accept bags of laundry as input and output them at the exit point...it was not intended to let prisoners escape!"....an example of "opportunistic typing," perhaps.

Systems of very real everyday importance which act as black boxes to many observers are financial systems (which can be gamed, broken, undermined, and which are of unprovable reliability), computers (which can have weird things done to them, such as buffer overruns), role-playing games, ecological systems, prisons (as above), Boeing 777s which may crash unexpectedly, etc.

In a financial system, for example, it is very important for users of the system to look for various ways the system may fail, and these can happen in a *lot* of ways. The random number generator may be flawed, or can be fed with certain numbers. The owners may have certain kinds of access. And so on. (These things have actually killed some digital banking and stock-trading systems. Users discovered "affordances" that allowed them to game the system, even trigger runaway inflation of digital currencies, etc.)

Some of these affordances were not intended by the original designer. (Schroeder calls this "thalience"--cf. Wiki--when systems form new types or categories different from what a designer considered. The connection with Heidegger is clear. A rock may not be typed in some object ontology as a hammer, it may not have "hammer methods" in an explicit sense, but some actor/player who picks up a rock and uses it as hammer in some online game has exploited its "hammerness"--possibly even breaking the intended rules of the game. An animal who crawls into a log for shelter is "opportunistically typing" a function or object for use in a different way. Heidegger calls this making use of "equipment."

This may be a direction for type systems to go, sort of a "super ad hoc polymorphic typing." (Different from static and dynamic typing, as this is more of an _iterated_ learning process, in the same sort of way the iterated prisoner's dilemma is different from a run once implementation.)

The black box (and intuitionistic logic) connection is that more and more of our software systems involve limited information about parts of the system, about legacy code, about other systems, as in networks, and about the goals/intentions/backstory of other players or agents or systems. (It is not surprising that many of these things come to the fore when we imagine _malicious_ opponents, in banks, games, voting systems, denial of service attacks, digital money, and so on. Attempts to break these systems, cheat them, find loopholes, crash 777s, etc. are cases where attackers are seeking to find the rules, find exceptions, and even find affordances (such as where using a particular number opens an account, or where a laundry chute, real or virtual, is an escape path).

Related to this of course is all the work on agents with bounded rationality or resources, game theory issues with bounded resources, and essentially all "big" systems where the God's eye view just plain isn't feasible.

Also related, but in ways I'm less sure about, are capability-based systems (as in E, etc.) and the connections with typing and affordances. (Capabilities are a way to severely constrain access to certain things or places, just as one might give a key only to the garden shed for a caretaker and not the keyring for the entire house, or give read/write access only to limited things in a system....this is to avoid certain affordances, such as the caretaker gaining access to the checkbook or the jewelry.)

Sorry for any scattershot conceptualizing here. They all seem closely related to me. Analyzing systems "in the large" seems to be a very practical topic.

in the Heidegerrian sense (sorry, couldn't resist). In particular I have seen no clear formal formulation of affordances.

An affordance appears to be, in some sense, the result of a change in point of view. This is not very useful analytically.

As you (Tim May) show in your post below, an item from one man's ontology can be the source of another man's (e.g., the malicious opponent's) affordance. I know how to formally express the ontology but not how to formally express an associated affordance, other than to say "It's something not in the ontology that, when added, causes no contradictions in the ontology". So in logical terms, an affordance would be a set of additional axioms to be added to our ontology's existing set of axioms. Unfortunately also the possible sets of additional axioms appear infinite.

But I don't see how that is more useful, since now we're back in logic and we're faced with the same old frame problem as before which IIRC was one of the reasons for bringing up Heideggerian affordances in the first place.

Does anyone know of any formal mathematical or logical expression of Heideggerian affordances?

...I think good programmers need more of this kind of mathematics than they do of calculus or numeric methods.

I heartily agree. Too often the fine points of mathematical thinking are lost in calculus and numerics classes. I remember real and complex calculus as a tangled hair ball of rules of thumb, abuses of notation and, of course, rote memorization. Somehow, I never managed to learn how the reals relate to the rationals...only years later am I patching in all the holes. (Actually, I just forgot everything -- I let that old building fall down, and now must build a new one!)

It's a real tragedy that calculus is required in disciplines where it's little used in comparison to the more fundamental skill of reasoning about relations. An emphasis on mathematical thinking, as opposed to mathematical techniques, would benefit not only our profession, but also the social sciences and business and economics, whose students are usually given a brief dip in stats and calc, with no effect on their general reasoning ability.

I heartily agree with your hearty agreement!

When we look at the kinds of mathematical thinking that most programming projects require, it's not usually (at least not now) about numerical recipes, array manipulation, finding roots. Sure, this was important in the 50s and even into the 70s, and is still important for graphics (splines, ray-tracing, etc.). Or bioinformatics (strings, alignment, etc.). But programmers doing these kinds of things are a small fraction of the total (and they are often first and foremost specialists in their respective areas, only programming to do specific kinds of orbital calculations, industrial processes, CAD, BLAST stuff in bioinformatics, etc.).

The argument I used to hear was that exposure to calculus and linear algebra would also teach basic reasoning. Ha. While linear algebra is really, really cool, and provides concepts that one ought to have (vectors, transforms, the base of a space, eigenvectors and fixed points in mappings), a lot of students never get exposed to conceptual stuff once they get to college.

I learned more logic and set theory in high school, from a great geometry teacher, than I did in my physics-oriented math classes later on. However, I also took some "analysis" classes which focussed on point set topology and gave me a lot to think about and use later on. Reading how point set topology can be implemented in Haskell, with properties of compactness, convergence, open sets, and even Tychonoff's Theorem having direct parallels (functorially speaking!) is just plain mind-blowing. (Cf. the long monograph by Martin Escardo, http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf )

I would love to see the undergraduate curriculum offer a class with coverage of these kinds of issues. For the mathematically sophisticated, they could jump right in on the issues above. For those with less mathematical sophistication, an introductory class covering set theory, Venn diagrams (*), different kinds of logic (including sequent logic), modal logic, the structure of the real line, what proof means, and so on. A later class, perhaps in the 3rd quarter (or late in the second semester) could touch on category theory, functional programming, and logic programming.

Alas, if the main debate in CS education seems to be about dropping the use of Scheme or similar languages and getting students doing Java or C their freshman year, then clearly the chances of teaching them some abstract math are nil. And C is not nil.

--Tim May

You might be interested in taking a look at the Beseme Project, assuming you haven't already seen it. The idea behind the project is to develop the kind of undergraduate curriculum you say you'd love to see. Indeed, quoting from the project description:

The Beseme Project (three syllables, all rhyming with "eh") seeks to support education in the application of mathematical reasoning to software development and to provide evidence that experience with these concepts makes software engineers more effective.

Beseme...I hadn't heard of it, but the proposed curriculum looks just about exactly what I think would be good. The principal investigator, Rex Page, I remember from various papers and even some ancient BASIC and FORTRAN books from the 70s (including "WATFIV For Humans"--I absolutely despised FORTRAN IV with WATFIV, but this could've had a lot to do with using an IBM 360/75 in 1971! I had no idea computers were even interesting until a few years later, when I joined Intel. (And Rex Page has been doing more FP kinds of stuff in recent years.)

Looks like the Beseme Project basically ran from 2000-2003. It may still exist, but, like a lot of funded programs, the focus of the people moves on to other things. I see that of the students is in Oregon, completing her Ph.D.; and she worked with Mark Jones on the Programmatica project.

Anyone out there teaching with the Beseme materials?

Beseme was discussed here several times, so searching the archives may prove useful.

I have -never- seen a "mutually recursive" definition of category

...

Absolutely nothing was said about what the objects and arrows "actually" were

Exactly. Obviously, at the time of OP, I hadn't made the intellectual leap, and I was seeing categories defined in terms of objects and arrows, and arrows defined in terms of morphisms: in mental terms, foreign concepts defined in terms of foreign concepts, which sounds like a recursive description to me!

"inferrable"? Usually the details abstracted away are irrelevant

Yes, inferrable, meaning that they can be automated via a compiler or interpreter, but never irrelevant to the machine--only to the domain model.

Usually category theory isn't "employed within a programming language", neither is set theory or predicate calculus

Ah, but what if they were?..(sigh) It wouldn't be too hard to do. I can think of serveral systems that strive for this.

Most introductions to category theory go to pains to explicitly point out that arrows are -not- necessarily (structured) functions

Quote from my OP (emphasis added):

a morphism seems to be a transformation (possibly represented by one or more functions)

Don't forget your modal logic.

Just because they (currently) go over your head, doesn't mean they go over "everybody else's".

You're right--all programmers are computer scientists. I forgot that. Anyways,

Category theory is a branch of mathematics, not a programming paradigm

Who said that has to be strictly true? I'm going to put this on my top 10 funniest quotes of the year. That strikes me as so funny! LOL

Again, where do these questions come from? How is set theory or predicate logic used to model "story problems"?

Well, you go ahead and try doing a proof of contradiction on that one. If you can prove that set theory and predicate calculus can't be used to create logical or mathematical models of a story problem and then be used to solve it, then I will stop wasting my time with them this instant! LOL!

have fun in your box; LOL!

(No hard feelings) :-)

Don't forget your modal logic.

You are very perceptive. I mentioned coalgebra above and it is indeed deeply linked to modal logic. A different set of ESSLLI notes.

Sounds like you're looking for n-categories. I'll let someone else fill in an explanation beyond "layering categories on top of each other so that each categories arrows are the objects in the category above it".

Has anyone noticed the similarity between those point-arrow diagrams commonly shown in category theory, and state transition diagrams?

Let S be the set of states of some state machine. Let T be the set of possible (possibly multi-step) transitions. In other words, let T consist of pairs (A,B) where the machine could go possibly go from state A to state B (after some, possibly zero, transitions).

Now look at Wikipedia.

We have a set of states. Call them objects. We have a set of transitions. Call them morphisms. Given any transition, we can extract two states from it, the initial state and the final state. Call the first the source and the second the target.

Keep working through the definition...

If there is a transition from a to b, and a transition from b to c, then there is a transition from a to c. So define (b,c)o(a,b) to be (c,a). Note how if u and v are transitions where the target of u is the source of v, then vou is also a transition. Note that we also have transitions (a,a) for every state a, corresponding to the zero step transition.

I'll leave checking for associativity as an exercise.

The point is, in computer science categories are everywhere. The notion of a category can be adapted to fit many things. The rule is, any time you see a diagram with lots of arrows and the heads of some arrows point to where the tails of arrow emerge there's a chance you have a category lurking there. Just check to see if the axioms fit. And any time they do fit, then any theorem of category theory may be applicable to these diagrams and may tell you something new or useful.

I'll leave checking for associativity as an exercise.

(c,d) o ((b,c) o (a,b))  =  (c,d) o (a,c)  =  (a,d)
((c,d) o (b,c)) o (a,b)  =  (b,d) o (a,b)  =  (a,d)

It wasn't much of an exercize -- am I missing something?

You're not missing a thing. I'm trying to convey the message that there's nothing weird or circular in the definition of a category and that the various clauses in the definition mesh perfectly with some ordinary everyday intuitions.

I'm not saying you're doing this, but I want to suggest some care in identifying categories and state transition systems. A typical way of formalizing a state transition system is to use an M-set where M is some monoid. In the descriptions above the category is being used in place of the monoid, not the whole M-set. This is indeed natural as a category can be viewed as a generalization of a monoid (a monoid is a one-object category). This suggests talking about C-sets where C is some category and indeed this is exactly what Barr and Wells do in the lecture notes I referenced above. If you go with this, it turns out that the various pieces correspond to very non-specialized ideas including a perspective on the Yoneda functor.

A quick glance at this paper shows that the authors rediscovered (in a very special case) the old concept of (bi)modules introduced by J. Benabou:

Let S : A -> A , T : B -> B be two monads in a bicategory W. The composition with S and T gives rise to a (standard) monad on Hom(A, B). A module from S to T is an object in the Elienberg-Moore category for this monad.

Best,
MRP