From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2173 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Realizibility and Partial Combinatory Algebras Date: Wed, 12 Feb 2003 20:28:14 +0100 (CET) Message-ID: <200302121928.UAA01552@fb04209.mathematik.tu-darmstadt.de> References: <1044469182.3e4155bed0abd@mail.inf.ed.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018465 2853 80.91.229.2 (29 Apr 2009 15:21:05 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:21:05 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Feb 13 14:52:31 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 13 Feb 2003 14:52:31 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jONN-0006Su-00 for categories-list@mta.ca; Thu, 13 Feb 2003 14:46:25 -0400 In-Reply-To: <1044469182.3e4155bed0abd@mail.inf.ed.ac.uk> from John Longley at "Feb 5, 2003 06:19:42 pm" X-Mailer: ELM [version 2.4ME+ PL66 (25)] X-MailScanner: Found to be clean Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 28 Original-Lines: 62 Xref: news.gmane.org gmane.science.mathematics.categories:2173 Archived-At: John L. has recalled that the traditional definition of pca is motivated by functional completeness. > The somewhat mysterious definition of (partial or full) > combinatory algebras is really motivated by the fact that it > is equivalent to a "combinatory completeness" property, which is > a bit less mysterious but more cumbersome to state. Informally, > combinatory completeness says that all functions definable in the > language of A are themselves representable by elements of A. > More precisely: > > A is a PCA iff for every formal expression e (built up from > variables x,y_1,...,y_n and constants from A via juxtaposition), > there is a formal expression called (\lambda x.e), whose variables > are just y_1,...,y_n, such that > (\lambda x.e)[b_1/y_1,...,b_n/y_n] is defined for all b_1,...,b_n \in A, > (\lambda x.e) a [b_1/y_1,...,b_n/y_n] ~ e[a/x,b_1/y_1,...,b_n/y_n] He also has pointed out that in realizability one always may replace a realizer by one which is defined for more arguments. Thus, it appears as natural to weaken the notion of functional completeness to the following "asymmetric" variant: for every formal expression e (built up from variables x,y_1,...,y_n and constants from A via juxtaposition), there is a formal expression called (\lambda x.e), whose variables are just y_1,...,y_n, such that for all a, b_1,...,b_n in A (\lambda x.e) a [b_1/y_1,...,b_n/y_n] = e[a/x,b_1/y_1,...,b_n/y_n] whenever the right hand side is defined Certainly, this assymmetric version of functional completeness ensures the existence of a k (with the usual properties) and an s in A with the property that (*) sabc = ac(bc) whenever ac(bc) is defined Obviously, from a k and an s satisfying (*) one can prove the assymmetric version of functional completeness. Axiom (*) doesn't even exclude undefinedness of sa (if a.x undefined for all x in A). Probably, such very weak pca's are also equivalent to an ordinary one? In any case the notion of pca is somewhat intensional in character. As we know Asm(A) and Asm(A') are equivalent iff their categories of modest projectives are equivalent. Concretely, for a pca A the category MP(A) of modest projectives is nothing but the category of subsets of A and maps f : P -> Q such that for some r in A we have ra = f(a) for all a in P. Of course, we know from John L.'s work that MP(A) and MP(A') are equivalent iff A and A' are applicatively equivalent. What, alas, is not known is an intrinsic categorical characterisation of those categories equivalent to MP(A) for some pca A. If we had such a characterisation we would have arrived at a categorical characterisation of categories of assemblies and, this, also of realizability toposes. Thomas