Date: Mon, 22 May 1995 11:18:13 -0300 (ADT) Subject: The effective topos. Date: Mon, 22 May 1995 13:22:11 +0100 From: Justin Pearson Dear All, A question for people who know about the effective topos. I'm just feeling my way, so be gentle. In the effective topos (and any other realizability topos I assume, but I don't know since I haven't got hold of the tripos paper yet), one can make internal the combinators S and K. I assume that you define the functional relations: G_s(n,n') = {n'} if Sn = n' \emptyset otherwise. G_k(n,n') = {n') if Kn = n' \emptyset otherwise. (In all this S refers to the combinator S not the successor function). Now here is the bit I'm not sure about, if we stipulate in a category, that there must be an object N with a unique pair of maps S and K such that: for all x,y K;x;y = x for all x,y,z S;x;y;z = x;z;(y;z) Further every map from N to N can be factored into S and K, and for good measure that N is actually the natural number object to avoid degeneracy. Does this characterize N in the effective topos? and hence the modest sets? Regards Justin Pearson Date: Tue, 23 May 1995 00:53:50 -0300 (ADT) Subject: Combinators in the effective topos Date: Mon, 22 May 1995 14:55:23 -0400 From: Peter Freyd I'm having trouble interpreting the question posed by Justin Pearson. If N is the natural numbers object then it certainly has a fixed-point-free self-map, which gives me trouble in figuring out what's meant by "every map from N to N can be factored into S and K." Date: Thu, 25 May 1995 17:45:16 -0300 (ADT) Subject: Effective topos. Date: Thu, 25 May 1995 14:55:29 +0100 From: Justin Pearson Some people have been confused by my question. This probally reflects a confusion on my part. There are two seperat parts. i)In the effective topos, given the internal defn. of S and K on N. Can every map form N to N be written as arbitary (fintie) words over S and K. I.E. given f:N -> N, can f be writen as some word f=S^a;K^b;S^c;K^d ... for a,b,c,d, ... > 0? ii) If (i) is true, then can we turn it around on its head and use it as a definition of the natural number object N in Eff? But as Rosolini pointed out there is a problem, do I mean every PARTIAL map can be factored? Hope this helps, sorry about the confusion, but as I have said it is all probally due to me. Regards Justin Pearson Date: Fri, 26 May 1995 10:59:58 -0300 (ADT) Subject: S,K,N Date: Thu, 25 May 1995 22:19:00 -0400 From: Peter Freyd With respect to the question from Justin Pearson, my point remains. Since the 1930's it has been the case that if every function from A to A can be written as a combination of S's and K's then every function from A to A has a fixed point. (Note the word "combination" not just the special case thereof, "word".)