Ryan Ingram schrieb:
2009/2/2 Luke Palmer lrpal...@gmail.com:
However! If we have a function f : Nat - Nat - Bool, we can construct the
diagonalization g : Nat - Bool as: g n = not (f n n), with g not in the
range of f. That makes Nat - Bool computably uncountable.
This is making my head
On Mon, Feb 2, 2009 at 3:55 PM, Benedikt Huber benj...@gmx.net wrote:
f is 'easy to implement' if it enumerates all functions, not just total
ones. Otherwise, f is hard to implement ;)
In the first case, if we have (f n n) = _|_, then g n = not (f n n) = _|_ as
well, so the diagonalization
I believe the original notion of type by Russell is most insightful,
bridging the semantic notion of type (type as a set of values) and the
syntactic notion (type system as a syntactic discipline, a statically
decidable restriction on terms).
That point is discussed at some length in Sec 3 (pp.
On Mon, Feb 2, 2009 at 11:14 PM, o...@okmij.org wrote:
I believe the original notion of type by Russell is most insightful,
bridging the semantic notion of type (type as a set of values) and the
syntactic notion (type system as a syntactic discipline, a statically
decidable restriction on
