tag:blogger.com,1999:blog-11295132.post181530249390420345..comments2018-03-30T14:19:07.317-07:00Comments on A Neighborhood of Infinity: The Type that Should Not BeDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger14125tag:blogger.com,1999:blog-11295132.post-88503715322903432462018-01-23T01:59:40.969-08:002018-01-23T01:59:40.969-08:00I know this post is ten years old, so this might n...I know this post is ten years old, so this might not be much use to you, but there can be no universes as you have defined them. Given a universe C, is nonSelfContaining included in it? As C is a universe, for all x, y in C, y `e` x terminates. In particular, x `e` x terminates, so x `e` nonSelfContaining also terminates for all x. But this means that nonSelfContaining is in C, and so nonSelfContaining `e` nonSelfContaining ought to terminate, a contradiction.qbt937https://www.blogger.com/profile/14951573161901401933noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-88593875570739168232010-03-20T20:21:46.408-07:002010-03-20T20:21:46.408-07:00Good stuff, thanks.
Actually, if we don't car...Good stuff, thanks.<br /><br />Actually, if we don't care about keeping ZF as it is, foundation axiom may be extended without breaking any logic up to something like Karoubian closures... but not everything there has been proven yet.Vlad Patryshevhttps://www.blogger.com/profile/13466586996802181998noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-12688123776152347662009-10-11T12:55:50.509-07:002009-10-11T12:55:50.509-07:00Pseudonym,
The isomorphism of the Cantor–Bernstei...Pseudonym,<br /><br />The isomorphism of the Cantor–Bernstein–Schröder theorem is itself not computable. So X=2^X is not an isomorphism in the category of computable functions.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-55171343627938311962009-09-20T14:03:27.860-07:002009-09-20T14:03:27.860-07:00http://en.wikibooks.org/wiki/Haskell/Denotational_...http://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Na.C3.AFve_Sets_are_unsuited_for_Recursive_Data_Typesghttps://www.blogger.com/profile/04686862403622560424noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-76047678156479198912009-05-03T18:31:00.000-07:002009-05-03T18:31:00.000-07:00It's over a year later, but I have one more co...It's over a year later, but I have one more comment.<br /><br />U -> Bool is not the same as 2^U in set theory, because it is <I>not</I> the collection of all functions from U to Bool. Rather, it's only the collection of all such <I>computable</I> functions.<br /><br />Any computable function can be G&oump;del-encoded into an Integer, so the collection of all computable functions are isomorphic to some subset of Integers. Moreover, all Integers are computable. Therefore, by the Cantor–Bernstein–Schröder theorem, the collection of all computable functions is isomorphic to Integer.<br /><br />So X = 2^X has a solution: X = Integer.<br /><br />This is an important point for people learning category theory. The category of computable sets with computable functions is not the same as the category of sets with functions, and the main difference is the exponential objects.Pseudonymhttps://www.blogger.com/profile/04272326070593532463noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-52976412032869141912009-05-03T08:54:00.000-07:002009-05-03T08:54:00.000-07:00You could also define
cbar a = U $ \x -> not (a...You could also define<br />cbar a = U $ \x -> not (a `e` x)<br /><br />and compose arbitrary sequences of c and cbar. I wonder how interesting a program can be written in a restricted subset of Haskell where only the types U, Bool, and functions thereof are allowed. Is it Turing-complete?janoshttps://www.blogger.com/profile/09674723547841998121noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-47915940390667399102008-04-22T11:05:00.000-07:002008-04-22T11:05:00.000-07:00Hmm, some of these lines aren't wrapping right in ...Hmm, some of these lines aren't wrapping right in IE6 -- at least, not in the normal view or in google reader, but the "show original post" link displays it with the lines wrapped properly (but in a different font).Samuel Bronsonhttps://www.blogger.com/profile/06560268240719951351noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-54168887152249601932008-02-08T11:15:00.000-08:002008-02-08T11:15:00.000-08:00I may be talking out of my a$$ on this one, but th...I may be talking out of my a$$ on this one, but the first type you have defined seems to be a resonable computationnal model of ordinals: an ordinal is the set of ordinals smaller than it. Non well founded definition? No problem! the empty set satisfies every propriety we through at it (at least proprieties defined in terms of those of it's elements). You can then form the ordinal that contains only the empty set, etc. You can only form finite ordinals in this fashion, forming an infinite structure requires a special axiom (the infamous axiom of infinity in ZF!). But i digress.<BR/><BR/>The type U seems to be a well known example of inductive type without a positivity condition. The computationnal significance of this type is known to be connected to Russel's paradox, and thus a strongly typed system which enjoys termination can lose it in presence of this structure. This would even allow one to prove a false statement in a type-theory based theorem prover!<BR/><BR/>Unfortunately i have no very relevent references for all of this. You might want to try Coq'Art, by Yves Bertot and Pierre Casteran (not free :( ... )<BR/><BR/>P.S. Please excuse my speling mestakes...Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-21212619542965798382008-01-27T19:26:00.000-08:002008-01-27T19:26:00.000-08:00Peter Mc,The point is that you've shown that vario...Peter Mc,<BR/><BR/>The point is that you've shown that various values in U are actually distinct from each other and the whole type doesn't just collapse down to something trivial.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-28669949941380597552008-01-27T17:41:00.000-08:002008-01-27T17:41:00.000-08:00Eager chap that I am, I drew a diagram of the doma...Eager chap that I am, I drew a diagram of the domain. Rather than subject you to my ASCII art skills, I'll just describe what came out:<BR/><BR/>for all n >= m >= 0:<BR/><BR/>(c^n) (neg phi) `e` (c^m) (neg phi) ==> True<BR/>(c^m) (neg phi) `e` (c^n) (neg phi) ==> True<BR/><BR/>for all n > m >= 0:<BR/><BR/>(c^n) phi `e` (c^m) (neg phi) ==> True<BR/>(c^m) (neg phi) `e` (c^n) phi ==> True<BR/><BR/>for all n >= 0<BR/><BR/>(c^n) phi `e` (c^n) (neg phi) ==> True<BR/><BR/>every other statement of the form:<BR/><BR/>(c^n) ([neg]? phi) `e` (c^m ([neg]? phi))<BR/><BR/>evaluates to False.<BR/><BR/>So is the set (c^n) ([neg]? phi) a computable element of U, or am I missing the point here?Peter Mchttps://www.blogger.com/profile/05863206648734186476noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-57952406252014568892008-01-27T14:04:00.000-08:002008-01-27T14:04:00.000-08:00This is just a basic Haskell question, but I'm a l...This is just a basic Haskell question, but I'm a little confused. If I load everything up to the definition of phi into ghci, I get the following:<BR/><BR/>*Main> :t f<BR/>f :: U -> U -> Bool<BR/><BR/>*Main> :t U<BR/>U :: (U -> Bool) -> U<BR/><BR/>I don't understand why f is that type. Why isn't it U -> Bool?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-9557735137146848732008-01-27T11:17:00.000-08:002008-01-27T11:17:00.000-08:00I usually find it illuminating to try and draw the...I usually find it illuminating to try and draw the domain for a type like U to understand it better. Well, draw an approximation of it since it's infinite.<BR/><BR/>I've not tried in this case, because I'm lazy.augustsshttps://www.blogger.com/profile/07327620522294658036noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-47456842030352076972008-01-26T20:24:00.000-08:002008-01-26T20:24:00.000-08:00Pseudonym,Aha! That looks like the chapter in Pier...Pseudonym,<BR/><BR/>Aha! That looks like the chapter in Pierce's Basic Category Theory that I skipped. I guess I'll have to read it as soon as I get it back from the guy I lent it to.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-56186725894543827622008-01-26T18:00:00.000-08:002008-01-26T18:00:00.000-08:00The question is actually what does it mean to "sol...The question is actually what does it mean to "solve" a recursive equation like X = 2^X. I recommend Chapter 10 (and hell, the rest of the book too) of Asperti and Longo's book, "Categories, Types and Structures". You can download it here:<BR/><BR/>http://www.di.ens.fr/users/longo/download.htmlPseudonymhttps://www.blogger.com/profile/04272326070593532463noreply@blogger.com