From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2193 Path: news.gmane.org!not-for-mail From: Newsgroups: gmane.science.mathematics.categories Subject: Re: Realizability and Partial Combinatory Algebras Date: Thu, 20 Feb 2003 17:44:57 +0100 (CET) Message-ID: <200302201644.RAA15105@kodder.math.uu.nl> NNTP-Posting-Host: main.gmane.org X-Trace: ger.gmane.org 1241018479 2949 80.91.229.2 (29 Apr 2009 15:21:19 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:21:19 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Feb 20 12:53:02 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 12:53:02 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ltu6-00023c-00 for categories-list@mta.ca; Thu, 20 Feb 2003 12:50:34 -0400 X-Sun-Charset: US-ASCII X-Virus-Scanned: by AMaViS snapshot-20020300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 49 Original-Lines: 33 Xref: news.gmane.org gmane.science.mathematics.categories:2193 Archived-At: Dear Peter and John, Peter correctly pointed out the error in my message: the problem was in the use of the "if then .. else .." syntax, not in any form of combinatorial completeness. Answering John: I was using a construction of \lambda x.t where \lambda x.M is KM whenever M is any term not containing x free (this works just as well); so in my construction, \lambda vz. if v then xkzk(ykz) else false DOES contain subterms xk and yk. Anyway, I do now believe that John's latest version is correct. This is really very nice, and a surprise (for me, at least). I stand corrected and must apologize for my first posting in this discussion, casting doubt on PTJ's message. One little point, regarding Combinatorial Completeness. I believe the following form is valid (in the situation with the weak S-axiom): suppose t is a term, x a variable. There is a term \lambda x.t such that for all a,a_1,...,a_n in A: ((\lambda x.t)[a_1,...,a_n])a ~ t[a,a_1,...,a_n] So this is just like the ordinary form, except for the assertion that (\lambda x.t)[a_1,...,a_n] is always defined. We have that (\lambda x.t)[a_1,...,a_n] is defined whenever for some a in A, t[a,a_1,...,a_n] is defined. Best, Jaap