* Realizibility and Partial Combinatory Algebras @ 2003-02-04 2:29 Galchin Vasili 2003-02-05 18:19 ` John Longley ` (2 more replies) 0 siblings, 3 replies; 9+ messages in thread From: Galchin Vasili @ 2003-02-04 2:29 UTC (permalink / raw) To: categories Hello, I understand (to some degree) full combinatory algebra, but I don't understand the motivation behind the definition of a partial combinatory algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x? Regards, Bill Halchin ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Realizibility and Partial Combinatory Algebras 2003-02-04 2:29 Realizibility and Partial Combinatory Algebras Galchin Vasili @ 2003-02-05 18:19 ` John Longley 2003-02-12 19:28 ` Thomas Streicher 2003-02-06 10:44 ` Prof. Peter Johnstone 2003-02-07 15:26 ` John Longley 2 siblings, 1 reply; 9+ messages in thread From: John Longley @ 2003-02-05 18:19 UTC (permalink / raw) To: categories Bill Halchin writes: > I understand (to some degree) full combinatory algebra, but I > don't > understand the motivation behind the definition of a partial > combinatory > algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x? 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] (This is easiest to understand in the case n=0.) A similar statement holds for full combinatory algebras where everything is always defined. The term (\lambda x.e) can be constructed via the Curry translation from lambda calculus to combinatory logic. The condition "Sxy is defined" is needed for this to work. Also, I should say the whole theory of realizability models goes through much more smoothly with this condition, otherwise one has to keep making tiresome exemptions for the case of the object 0. I imagine the condition becomes strictly necessary at some point, e.g. in the proof that PER is an internal category. As for Kxy ~ x, that's the same as saying Kxy=x, because all elements x of A are of course defined. Cheers, John ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Realizibility and Partial Combinatory Algebras 2003-02-05 18:19 ` John Longley @ 2003-02-12 19:28 ` Thomas Streicher 0 siblings, 0 replies; 9+ messages in thread From: Thomas Streicher @ 2003-02-12 19:28 UTC (permalink / raw) To: categories 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Realizibility and Partial Combinatory Algebras 2003-02-04 2:29 Realizibility and Partial Combinatory Algebras Galchin Vasili 2003-02-05 18:19 ` John Longley @ 2003-02-06 10:44 ` Prof. Peter Johnstone 2003-02-07 12:57 ` Peter Lietz 2003-02-07 15:26 ` John Longley 2 siblings, 1 reply; 9+ messages in thread From: Prof. Peter Johnstone @ 2003-02-06 10:44 UTC (permalink / raw) To: categories On Mon, 3 Feb 2003, Galchin Vasili wrote: > > Hello, > > I understand (to some degree) full combinatory algebra, but I don't > understand the motivation behind the definition of a partial combinatory > algebra. E.g. why do we have Sxy converges/is defined? I'd like to know the answer to this too. Why does *everyone*, in writing down the definition of a PCA, include the assumption that Sxy is always defined? As far as I can see, the only answer is "because everyone else does so"; the condition is never used in the construction of realizability toposes, or in establishing any of their properties. In every case where you need to know that a particular term Sab is defined, it's easy to find a particular c such that Sabc is provably defined. Peter Johnstone ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Realizibility and Partial Combinatory Algebras 2003-02-06 10:44 ` Prof. Peter Johnstone @ 2003-02-07 12:57 ` Peter Lietz 0 siblings, 0 replies; 9+ messages in thread From: Peter Lietz @ 2003-02-07 12:57 UTC (permalink / raw) To: categories Hello, On Thu, 6 Feb 2003, Prof. Peter Johnstone wrote: > I'd like to know the answer to this too. Why does *everyone*, in writing > down the definition of a PCA, include the assumption that Sxy is always > defined? As far as I can see, the only answer is "because everyone else > does so"; the condition is never used in the construction of > realizability toposes, or in establishing any of their properties. > In every case where you need to know that a particular term Sab is > defined, it's easy to find a particular c such that Sabc is provably > defined. I'd like to vehemently contradict the claim that the condition "sab is always defined" is never used in the construction of realizability toposes. In the paper "Modified Realizability Toposes and Strong Normalization Proofs (Extended Abstract)" by Martin Hyland and Luke Ong, a weaker notion of combinatory algebra, called "conditionally partial combinatory algebra c-pca)", in which the requirement in question is actually dropped, is thoroughly examined. The axioms for a c-pca are that (K) kxy = y (S) sxyz ~= xz(yz) where by "~=" I mean Kleene-equality (i.e. the r.h.s. is defined iff the l.h.s. is defined in which case they are equal). It is not required for a c-pca that "sxy" exists, but if z exists such that xz(yz) exists then sxyz and hence sxy exists by the axiom (S). The motivation for introducing the notion of a c-pca in the paper is that there is a very relevant c-pca which is not a pca. It consists of strongly normalizing lambda terms modulo closed beta equivalence and can be used for providing a categorical point of view on the "candidates of reducibility" method for strong normalization proof. It is shown in the paper that the standard realizability tripos construction will fail to actually deliver a tripos: The set of subsets of the c-pca taken as the set of truth-values won't even model minimal logic, which is why a "modified realizability topos" construction is used in the paper. So there is a strong reason for stipulating the existence of sxy. One relaxation of the notion of pca which won't break the usual constructions but is nevertheless rarely employed (exception is e.g. Longley's work) is the following: instead of sxyx ~= xz(yz) one might merely require sxyz ~> xz(yz), i.e., sxyz is allowed to be more defined than xz(yz). However, I don't know of any interesting models which do not satisfy (S) with Kleene equality anyway. Respectfully yours, Peter Lietz ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Realizibility and Partial Combinatory Algebras 2003-02-04 2:29 Realizibility and Partial Combinatory Algebras Galchin Vasili 2003-02-05 18:19 ` John Longley 2003-02-06 10:44 ` Prof. Peter Johnstone @ 2003-02-07 15:26 ` John Longley 2 siblings, 0 replies; 9+ messages in thread From: John Longley @ 2003-02-07 15:26 UTC (permalink / raw) To: categories > I understand (to some degree) full combinatory algebra, but I don't > understand the motivation behind the definition of a partial combinatory > algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x? Here's another way to motivate the definition of PCAs, which I believe also shows (in response to Peter Johnstone's message) where the definedness condition is used in the standard realizability construction. Let A be any set with a partial binary operation (thought of as "application"). Let PA be the powerset of A. The idea is that we want to use PA as a little model for minimal implicational logic. We think of sets X \in PA as "propositions", and elements a \in X as "proofs" or "witnesses" for X. We think of the empty set as "false" since it has no witnesses. We next define an operation => on PA, corresponding to "implication", as follows: X => Y = { a \in A | for all b \in X. ab defined and ab \in Y } [Idea: a proof of X=>Y should map any proof of X to a proof of Y.] The basic idea here is often attributed to Dana Scott. Now, given any formula \phi built up from propositional variables p_1,...,p_n using implication, and any valuation v assigning elements of PA to these variables, we can interpret \phi in PA to get an element [[\phi]]_v \in PA. Let us say \phi holds in our model ( A |= \phi ) if there's some a \in A such that for all valuations v we have a \in [[\phi]]_v. [In other words, there's a uniform proof that all instances of \phi are true.] We'd like this model to be sound for the (intuitionistic) logic of pure implication. As is well known, the two axioms p -> q -> p (p -> q -> r) -> (p -> q) -> (p -> r) and the modus ponens rule suffice for deriving all theorems of this logic. Since modus ponens is clearly sound for the above interpretation, we just need to assume we have "uniform proofs" in A of the above two formulae. Now suppose A contains elements k,s satisfying the axioms of a PCA. Then it is simple to show that k,s respectively provide realizers for the above two formulae, and hence A soundly models minimal implicational logic. The condition "sxy defined" is important here, as can be seen by interpreting p as \emptyset, and q and r as A. The question of the converse is quite interesting. I have occasionally suggested that the definition of PCA should be weakened to allow sxyz >~ (xz)(yz), where >~ means "if the RHS is defined then so is the LHS and they are equal". Some support for this proposal could perhaps be drawn from the following result, which I had not noticed before: Let A be any partial applicative structure. Then (PA,=>) as above soundly models minimal implicational logic iff there exist k,s \in A satisfying kxy = x, sxy defined, sxyz >~ (xz)(yz) (I do have examples of structures that are PCAs in this weaker sense but not in the standard sense, but they are a little obscure.) Anyhow, the "PA construction" above is an important part of the tripos-theoretic construction of realizability models, so I think this shows that "sxy defined" is needed even to ensure the realizability model is a model for implicational logic. (My suggestion regarding internal categories in my previous message was overkill!) Incidentally, a few years ago, Hyland and Ong considered structures called "conditionally partial combinatory algebras", where one assumes sx defined but not sxy defined. They observed that the standard realizability construction does not in general work for CPCAs, but (in certain interesting cases) a modified realizability construction does. Cheers, John ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Realizibility and Partial Combinatory Algebras
@ 2003-02-07 9:57 jvoosten
2003-02-07 23:43 ` Prof. Peter Johnstone
0 siblings, 1 reply; 9+ messages in thread
From: jvoosten @ 2003-02-07 9:57 UTC (permalink / raw)
To: categories
> Date: Thu, 6 Feb 2003 10:44:33 +0000 (GMT)
> From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
> Subject: categories: Re: Realizibility and Partial Combinatory Algebras
>
> On Mon, 3 Feb 2003, Galchin Vasili wrote:
>
> >
> > Hello,
> >
> > I understand (to some degree) full combinatory algebra, but I don't
> > understand the motivation behind the definition of a partial combinatory
> > algebra. E.g. why do we have Sxy converges/is defined?
>
> I'd like to know the answer to this too. Why does *everyone*, in writing
> down the definition of a PCA, include the assumption that Sxy is always
> defined? As far as I can see, the only answer is "because everyone else
> does so"; the condition is never used in the construction of
> realizability toposes, or in establishing any of their properties.
> In every case where you need to know that a particular term Sab is
> defined, it's easy to find a particular c such that Sabc is provably
> defined.
>
> Peter Johnstone
Dear Peter,
I think the relevance of this condition (Sxy defined) is explained in the
Hyland-Ong paper "Modified Realizability Toposes and Strong Normalization
Proofs" (TLCA, LNCS 664, 1993; reference 466 in the Elephant) where they
have a definition of "c-pca" which is just omitting this requirement.
They show that the standard P(A)-indexed preordered set, for a c-pca A,
can fail to be a tripos. So the condition IS used.
Another condition which is often imposed is really redundant: it is the
requirement that, if sxyz defined, then xz(yz) defined and equal to sxyz.
There are important constructions of realizability toposes where this
fails to hold.
Jaap van Oosten
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Realizibility and Partial Combinatory Algebras 2003-02-07 9:57 jvoosten @ 2003-02-07 23:43 ` Prof. Peter Johnstone 2003-02-09 19:09 ` Peter Lietz 0 siblings, 1 reply; 9+ messages in thread From: Prof. Peter Johnstone @ 2003-02-07 23:43 UTC (permalink / raw) To: categories On Fri, 7 Feb 2003 jvoosten@math.uu.nl wrote: > > I think the relevance of this condition (Sxy defined) is explained in the > Hyland-Ong paper "Modified Realizability Toposes and Strong Normalization > Proofs" (TLCA, LNCS 664, 1993; reference 466 in the Elephant) where they > have a definition of "c-pca" which is just omitting this requirement. > They show that the standard P(A)-indexed preordered set, for a c-pca A, > can fail to be a tripos. So the condition IS used. > I hope Jaap and Peter will forgive me for saying that I think they missed the point of my message. (Perhaps it's my fault -- with hindsight, I wasn't as clear as I should have been. I really ought to stop trying to reply to things like this late at night -- although, as you'll see from the header of this message, I'm doing it again.) Of course I know about the Hyland--Ong paper: indeed, I reviewed it for Zentralblatt. However, the point I was trying to make was that the construction of the quasitopos of A-valued assemblies, and the proof that its effectivization is a topos, make no use whatever of the condition that Sxy is always defined. The fact that the tautology ((p => (q => r)) => ((p => q) => (p => r))) fails (or may fail) to be realized by S when p is empty has no effect on this construction, because one never has to deal with "propositions" having an empty set of realizers. So, whilst a tripos-theorist (if such a creature exists) may indeed have cause to worry about whether Sxy might be undefined, there seems to be no reason why a topos-theorist should do so. [Yes, yes, I know that I was responsible for inventing the term "tripos", and therefore that if anyone can legitimately be called a tripos-theorist then I can. But I don't believe that I am a tripos-theorist (which implies that no-one is).] Peter Johnstone ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Realizibility and Partial Combinatory Algebras 2003-02-07 23:43 ` Prof. Peter Johnstone @ 2003-02-09 19:09 ` Peter Lietz 0 siblings, 0 replies; 9+ messages in thread From: Peter Lietz @ 2003-02-09 19:09 UTC (permalink / raw) To: categories On Fri, 7 Feb 2003, Prof. Peter Johnstone wrote: > Of course I know about the Hyland--Ong paper: indeed, I reviewed it for > Zentralblatt. However, the point I was trying to make was that the > construction of the quasitopos of A-valued assemblies, and the proof > that its effectivization is a topos, make no use whatever of the > condition that Sxy is always defined. The fact that the tautology > ((p => (q => r)) => ((p => q) => (p => r))) fails (or may fail) to > be realized by S when p is empty has no effect on this construction, > because one never has to deal with "propositions" having an empty > set of realizers. Dear Professor Johnstone, I obviously assumed strongly that you know the Hyland-Ong paper and was hence rather puzzled by what I mistakenly took for your question. As to the question regarding A-valued assemblies when A is a c-pca, I think I can give a justification for the axiom "Sab exists" as well. I claim that if the axiom "Sab exists" is absent, then the resulting category of A-valued assemblies is not a quasi-topos. One can form the category of A-valued assemblies and it is regular and cartesian closed. However, the realizers for the evaluation maps and also the construction of a realizer for the transpose of a map may exist, but one has to make a case analysis as to whether the source object is inhabited or not. Therefore it seems unlikely that the category is locally cartesian closed, as these operations cannot be carried out in a uniform manner. If this is the case then the category's exact completion is not a topos. I am aware that this argument is pretty vague. For a rigorous proof I would try to show that IF the subobjects of the threefold product of Nabla(P(A)) do form a Heyting-algebra, which if I am right is one of the requirements for a quasi-topos, THEN "Sab always exists". I would go about it as follows. 1. Show that the exponent subobject of two subobjects of an object is - if it exists - constructed as in the "unconditional" pca case. 2. Define the subobject m:S->Nabla(P(A)) with S = {M\subseteq A | M inhabited} and the set of realizers of M w.r.t. S being M (and m being the obvious map). 3. Interpret the S-tautology of intuitionistic propositional logic taking u,v and w as the pullbacks of m along the 1st, 2nd and 3rd projection of Nabla(P(A)) x Nabla(P(A)) x Nabla(P(A)), respectively. 4. Observe that it is the full subobject and use the reasoning of the Hyland-Ong paper to show that "Sab always exists". Should I be wrong, this would also be good news in a way, because it would imply that the standard construction of A-valued assemblies could be used for semantic strong normalization proofs instead of the more complicated construction of modified assemblies. Best regards, Peter Lietz ^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2003-02-12 19:28 UTC | newest] Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2003-02-04 2:29 Realizibility and Partial Combinatory Algebras Galchin Vasili 2003-02-05 18:19 ` John Longley 2003-02-12 19:28 ` Thomas Streicher 2003-02-06 10:44 ` Prof. Peter Johnstone 2003-02-07 12:57 ` Peter Lietz 2003-02-07 15:26 ` John Longley 2003-02-07 9:57 jvoosten 2003-02-07 23:43 ` Prof. Peter Johnstone 2003-02-09 19:09 ` Peter Lietz
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).