Comments on A Neighborhood of Infinity: The Type that Should Not Be

Good stuff, thanks. Actually, if we don't car...

2010-03-20T20:21:46.408-07:00

Good stuff, thanks.

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.

Pseudonym, The isomorphism of the Cantor–Bernstei...

2009-10-11T12:55:50.509-07:00

Pseudonym,

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.

http://en.wikibooks.org/wiki/Haskell/Denotational_...

2009-09-20T14:03:27.860-07:00

http://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Na.C3.AFve_Sets_are_unsuited_for_Recursive_Data_Types

It's over a year later, but I have one more co...

2009-05-03T18:31:00.000-07:00

It's over a year later, but I have one more comment.

U -> Bool is not the same as 2^U in set theory, because it is not the collection of all functions from U to Bool. Rather, it's only the collection of all such computable functions.

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.

So X = 2^X has a solution: X = Integer.

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.

You could also define cbar a = U $ \x -> not (a...

2009-05-03T08:54:00.000-07:00

You could also define
cbar a = U $ \x -> not (a `e` x)

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?

Hmm, some of these lines aren't wrapping right in ...

2008-04-22T11:05:00.000-07:00

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).

I may be talking out of my a$$ on this one, but th...

2008-02-08T11:15:00.000-08:00

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.

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!

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 :( ... )

P.S. Please excuse my speling mestakes...

Peter Mc,

The point is that you've shown th...

2008-01-27T19:26:00.000-08:00

Peter Mc,

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.

Eager chap that I am, I drew a diagram of the doma...

2008-01-27T17:41:00.000-08:00

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:

for all n >= m >= 0:

(c^n) (neg phi) `e` (c^m) (neg phi) ==> True
(c^m) (neg phi) `e` (c^n) (neg phi) ==> True

for all n > m >= 0:

(c^n) phi `e` (c^m) (neg phi) ==> True
(c^m) (neg phi) `e` (c^n) phi ==> True

for all n >= 0

(c^n) phi `e` (c^n) (neg phi) ==> True

every other statement of the form:

(c^n) ([neg]? phi) `e` (c^m ([neg]? phi))

evaluates to False.

So is the set (c^n) ([neg]? phi) a computable element of U, or am I missing the point here?

This is just a basic Haskell question, but I'm a l...

2008-01-27T14:04:00.000-08:00

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:

*Main> :t f
f :: U -> U -> Bool

*Main> :t U
U :: (U -> Bool) -> U

I don't understand why f is that type. Why isn't it U -> Bool?

I usually find it illuminating to try and draw the...

2008-01-27T11:17:00.000-08:00

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.

I've not tried in this case, because I'm lazy.

Pseudonym,

Aha! That looks like the chapter...

2008-01-26T20:24:00.000-08:00

Pseudonym,

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.

The question is actually what does it mean to "sol...

2008-01-26T18:00:00.000-08:00

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:

http://www.di.ens.fr/users/longo/download.html