tag:blogger.com,1999:blog-11295132.post114415968058557363..comments2015-09-16T20:54:40.355-07:00Comments on A Neighborhood of Infinity: Anti-Foundation and Strong ExtensionalityDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger9125tag:blogger.com,1999:blog-11295132.post-1144871161750285162006-04-12T12:46:00.000-07:002006-04-12T12:46:00.000-07:00jacobian,I had to look at that diagram several tim...jacobian,<BR/><BR/>I had to look at that diagram several times to see that the bottom right X should be a Y.<BR/><BR/>I might have to rewrite the whole thing at some point. It seems that the Haskell type system is flexible enough to unify all of the initial algebras as instances of one type parametrised by the functor F, and the same goes for the final coalgebras. I think fold and unfold just pop out automatically without me having to think hard about how to implement them - I'd just have to implement fmap for the functor. I'll have to work out the details. But it's hard to revisit something you thought was finished.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144869973741942842006-04-12T12:26:00.000-07:002006-04-12T12:26:00.000-07:00thedatabase,In effect you'd like to erase the obje...thedatabase,<BR/><BR/>In effect you'd like to erase the objects leaving just the arrows, just as you can do with many other kinds of coalgebraic structure. That might in fact be doable with AFA, but I'm no expert on category theory. Part of me thinks "what a cool idea!" and part of me is repelled by the thought :-)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144869716346834992006-04-12T12:21:00.000-07:002006-04-12T12:21:00.000-07:00Jacobian,Your intuition about erasing labels agree...Jacobian,<BR/><BR/>Your intuition about erasing labels agrees with mine. I'll get back to you on the typo...sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144576628032809882006-04-09T02:57:00.000-07:002006-04-09T02:57:00.000-07:00I think it just occured to me why bisimulation and...I think it just occured to me why bisimulation and removal of state labels is important here so let me try to explain it to see if I'm on the right track. <BR/><BR/>x = {x} can be thought of as an arrow from the state x to the state x, a loop. <BR/><BR/>x -> x <BR/><BR/>Now if we look at the simultaneous equations y={z},z={y} then we have <BR/><BR/>y->z->y a circle with two points. But in actuality, y and z are indistinguishable since the available transitions from y are the same as those from z, and therefor we collapse to the same graph as x={x}. Is this correct?Jacobianhttp://www.blogger.com/profile/03650584449231540008noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144576046204743242006-04-09T02:47:00.000-07:002006-04-09T02:47:00.000-07:00I think there is a typo in this diagram from your ...I think there is a typo in this diagram from your literate haskell at:<BR/><BR/>http://homepage.mac.com/sigfpe/Computing/fold.html<BR/><BR/> F(h)<BR/> F(X) --> F(Y)<BR/> | |<BR/>fin| | f<BR/> V h V<BR/> X --> X h = fold fJacobianhttp://www.blogger.com/profile/03650584449231540008noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144554411850848882006-04-08T20:46:00.000-07:002006-04-08T20:46:00.000-07:00Hello SIGFPE --- that's a coincidence... I searche...Hello SIGFPE --- that's a coincidence... I searched for "axiom anti-foundation" while reading This Weeks Finds, and up you pop, a This Weeks Finds reader who's just posted on the subject. Small internet!<BR/><BR/>Anyway, if you've been reading the tale of n-categories, 3-morphisms between 2-morphisms, 2-morphisms between morphisms, etc, don't you sometimes feel it's a shame that a theory that emphasises form and structure only up to isomorphism, should still depend on a very concrete "Level-1" case, ie some base category with objects?<BR/><BR/>In fact, the whole motivation for objects seems just to be to get morphisms off the ground, allowing us to start stepping up the (at least strict) n-category ladder in a quasi-inductive way<BR/><BR/>This got me thinking that objects in a category and the axiom of foundation play a very similar role.<BR/><BR/>If one were to attempt to do-away with objects, ie just have morphisms between morphisms between morphisms, one would quickly find oneself with either infinite or circular chains of descent, just as with unfounded sets<BR/><BR/>I've not paid this much thought, as evidenced by you being my first hit on google, but perhaps you may have some insight into:<BR/>- would a category theory without objects be doable at-all, and if so, would it share any features with unfounded set theory?<BR/>- how would you recover either natural transformations or n-category theory? My inital thought would be that there would only remain certain classes of "differences" or "quotients" between your unfounded categories (assuming you managed to recover anything resembling category theory!)thedatabasehttp://www.blogger.com/profile/00973795967472720213noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144332542850596562006-04-06T07:09:00.000-07:002006-04-06T07:09:00.000-07:00Kenny,Don't know what I was thinking. Having actua...Kenny,<BR/><BR/>Don't know what I was thinking. Having actually worked through the proof of Strong Extensionality I don't know why I went on to write about it as an axiom. I'll fix that in the main text.<BR/><BR/>Jacobian,<BR/><BR/>I think various papers on streams by <A HREF="http://homepages.cwi.nl/~janr/papers/" REL="nofollow">Rutten</A> give a good intro to bisimulation in certain contexts.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144323715520827592006-04-06T04:41:00.000-07:002006-04-06T04:41:00.000-07:00This looks similar to unification over rational tr...This looks similar to unification over rational trees. In the case of rational trees we are dealing with labeled directed graphs rather than simply directed graphs. Unifying over rational trees is nice because you can directly represent cyclic structures in logic programming.<BR/><BR/>In the case of rational trees we are restricted to finitary graphs (although, with higher order unifcation we might be able to eek out a lazy infinite structure, I'm not sure). <BR/><BR/>I assume that in the case of AFA we are talking about arbitrary directed graphs?<BR/><BR/>Also is there a recommended reference to bisimulation.Jacobianhttp://www.blogger.com/profile/03650584449231540008noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144296136014123332006-04-05T21:02:00.000-07:002006-04-05T21:02:00.000-07:00The presentation I had seen about anti-foundation ...The presentation I had seen about anti-foundation talked about directed graphs rather than systems of equations, but I think it works approximately the same.<BR/><BR/>Also, I believe the fact that anti-foundation says the solution is <I>unique</I> guarantees strong extensionality as a theorem. For instance, any solution to x={x} is also a solution to y={z} and z={y}, and since this is a solution, it must be the unique one.<BR/><BR/>Anyway, since I saw it in terms of directed graphs, I assume that you can just represent all these things as directed graphs within ordinary ZF, so you don't need urelements. And the consistency result is actually an equivalence - ZF is consistent iff AFA is, because you can start with any model of AFA and consider the subclass of well-founded sets, and they will satisfy ZF.<BR/><BR/>Anyway, it's neat to see the bisimulation stuff! I had only run into bisimulation in terms of frames for modal logic, so it's neat to see that the same relation works here to prove that two sets of equations have the same solutions.Kennyhttp://www.blogger.com/profile/12226268498253877151noreply@blogger.com