Realizibility and Partial Combinatory Algebras
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
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
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
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
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
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
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
Peter Johnstone wrote:
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.
As far as I can see, Peter Johnstone is essentially correct. Even without the condition "sxy is defined", Asm(A) is locally cartesian closed (though the correct construction of local exponentials is not quite the "obvious" one), and its exact/regular completion is a topos. Peter Lietz's argument (which is the one that occurred to me too) seems to fail at his point 1: to get a realizer for the mediating morphism from the true local exponential to the object he constructs, one actually needs the condition "sxy is defined". For the record, in Peter L's example, the true exponential m^m in the slice over Nabla(P(A)), for instance, may be described as follows: |T| = P(A) [|X \in T|] = {a | for all b \in X. akb \in X} (where k plays the role of an arbitrary element which forces the "thunked" operation X -> X to manifest itself.) I think I can now appreciate Peter Johnstone's point of view, though it seems to me that to follow it through consistently would require some substantial changes to the way one develops the whole theory. For instance, in defining the category Asm(A), one really ought to say e.g. that an element r \in A *tracks* f : X -> Y iff for all x \in X, a \in A. a \in [|x \in X|] => rka \in [|f(x) \in Y|] so as not to get mired down in case splits on whether X is inhabited, which (I humbly submit) are here an abomination and totally out of keeping with the spirit of realizability and topos theory in general. [Classically, of course, the above definition leads to exactly the same category as the usual one.] One can then do everything else in the same way, and it all works out - e.g. there is a perfectly respectable tripos over A (with Heyting implication defined as in the object T above), and the theory of internal categories such as PER also works fine. I don't think one can really call this "standard realizability" any more, in the sense of being derived from (a simple abstraction of) Kleene's realizability interpretation. Of course, one might say that doesn't matter much, but for my part, I feel one loses something of the directness of standard realizability, where application in the PCA corresponds immediately to function application in Asm(A) and also to Modus Ponens in the logic. There is also of course the evident analogy with the Brouwer-Heyting- Kolmogorov interpretation of intuitionistic logic. If one adopts the above alternative, there is less of a clear intuition about what the significance of application in the PCA is. However, no sooner has one reached this point, than one notices that doing realizability of the above kind over A is just tantamount to doing standard realizability over the "derived PCA" a la Freyd [?], where application is defined by a.b ~ akb. Indeed, one has the following easy proposition: For any PCA A (where we don't assume "sxy defined"), there is an applicatively equivalent PCA B (in the sense of my thesis) in which sxy is always defined. In particular, the realizability topos on A (constructed as outlined above) is equivalent to the (usual) standard realizability topos on B. Proof: Let B have the same set as A, and define application in B by a.b ~ akb. It's easy to construct K,S \in B such that K.a.b = a, S.a.b.c ~ a.c.(b.c), and with a little additional care one can arrange that S.a.b is always defined. Now, application in B is realized in A by \lambda ab. akb (constructed as normal); and application in A is realized in B by i=skk, since i.a.b = ikakb = kakb = ab. The equivalence of toposes can now most easily be seen by noticing that the categories Asm(A), Asm(B) are equal on the nose. So, it seems it's largely just a question of taste whether one adopts the definedness condition. For my money, I would rather adopt this condition, retain the directness of standard realizability and all the familiar constructions, do all the proofs in an "effective" spirit, and know that I'm not sacrificing any generality. Who could ask for anything more? (Quite a lot of the above was new to me, and was all good fun!) Finally, I'd like to remark briefly on the other issue in the definition of PCA, which Jaap, Peter L and myself have now all mentioned: whether one should require sxyz ~ xz(yz) or just sxyz >~ xz(yz). I know of no reason not to adopt the latter, more general condition, and it seems to me much more in the spirit of realizability: e.g. one never cares if a realizer for a morphism assemblies is defined on more elements than required. On the other hand, I do not have any particular use yet for any of the extra examples admitted by this definition. An interesting case in point is Kleene's second model, K_2. It is a PCA in the sense of the axiom with ~, but the "natural" construction of an element s gives one that only satisfies the axiom with >~. Some artificial hackery is needed to produce an element s satisfying the stronger axiom - and of course, my attitude would be: why bother? Best wishes, John
Dear John, would you please fill me in on either (or better yet, both) of the following points, as I failed to figure them out by myself: 1.) Let A be a c-pca. If I understand correctly, you say that the indexed poset that maps a set I to the set of maps from I to P(A), endowed with the usual entailment relation [ for phi,psi: I -> P(A), phi |- psi iff there is an r in A such that for all i in I and for all a in phi(i), ra exists and ra is in psi(i) ] is indeed an indexed Heyting-Algebra and that the implication of phi,psi : I -> P(A) is given by (phi=>psi)(i) = {r in A | forall a in phi(i). rka in psi(i)}. My question is: given phi, psi and theta such that theta /\ phi |- psi over I via some realizer r, what would be a realizer witnessing theta |- phi => psi with => defined in the way you indicated? 2.) Given a c-pca A, you say that A equipped with the application function a.b := akb is a (proper) pca. What exactly would be a good S combinator for the new algebra ? (You wrote that some additional care is needed to construct S) Many thanks in advance, Peter ps: in an attempt to give the shortest possible of the many reasons, why Heyting algebras do not form a CCC I suggest: The one-element poset is the terminal Heyting algebra. Therefore, every object has at most one global section. Hence, there can only be one morphism between each two Heyting algebras, as the global sections of the exponent correspond to the morphisms (which is absurd). pps: The one-element poset *is* a Heyting-algebra, in fact all topologies are. On Wed, 12 Feb 2003, John Longley wrote:
As far as I can see, Peter Johnstone is essentially correct. Even without the condition "sxy is defined", Asm(A) is locally cartesian closed (though the correct construction of local exponentials is not quite the "obvious" one), and its exact/regular completion is a topos. Peter Lietz's argument (which is the one that occurred to me too) seems to fail at his point 1: to get a realizer for the mediating morphism from the true local exponential to the object he constructs, one actually needs the condition "sxy is defined". For the record, in Peter L's example, the true exponential m^m in the slice over Nabla(P(A)), for instance,
....
Quoting Peter Lietz <lietz@mathematik.tu-darmstadt.de>:
1.) Let A be a c-pca. If I understand correctly, you say that the indexed poset that maps a set I to the set of maps from I to P(A), endowed with the usual entailment relation
Not quite - you have to define the entailment relation to match the definition of implication (put a k in there!). The cheating way to see that all this must work out is of course via the equivalence to a PCA for which the standard construction works!
2.) Given a c-pca A, you say that A equipped with the application function a.b := akb is a (proper) pca. What exactly would be a good S combinator for the new algebra ?
Note that we can find elements if,true,false \in A satisfying if true x y = x, if false x y = y, and furthermore we can arrange that true = k. (I'll use "if then else" syntax below). We want to construct S such that (in A), Skxkykz ~ (xkz)k(ykz), and Skxky is always defined. Take S to be \lambda txuyvz. if v then (xkz)k(ykz) else false using the usual Curry translation of lambda terms. To see that Skxky is always defined, note that, provably, Skxky(false)z = false. Clearly there are two versions of this result, one with the axiom sxyz ~ (xz)(yz) and one with sxyz >~ (xz)(yz). Thomas asks whether every PCA with >~ is equivalent to one with ~ (Gordon Plotkin has also asked me this natural question). At the moment, the best I can do is: for any PCA A with >~, there's a PCA B with ~ and an applicative inclusion A -> B (giving rise to a geometric inclusion of toposes). Cheers, John
Dear John,
Note that we can find elements if,true,false \in A satisfying if true x y = x, if false x y = y, and furthermore we can arrange that true = k. (I'll use "if then else" syntax below). We want to construct S such that (in A), Skxkykz ~ (xkz)k(ykz), and Skxky is always defined. Take S to be \lambda txuyvz. if v then (xkz)k(ykz) else false using the usual Curry translation of lambda terms. To see that Skxky is always defined, note that, provably, Skxky(false)z = false.
There is a point I don't understand. If I work out Skxky, then I find a term which contains subterms of the form xk, yk. So how can this be defined if x or y represent nowhere defined functions? It looks to me, that you are using a form of Combinatorial Completeness that is not valid with the weaker S-axiom. If I am correct, one has the following form of Combinatorial Completeness: For every term t and variable z, there is a term \lambda z.t with the property: If \lambda z.t is defined, then for each a, (\lambda z.t)a ~ t[a/z] (of course, a really correct version has more than one variable) Best, Jaap
Although in the meantime I was completely convinced by John's argument, I now believe that Jaap has indeed raised a serious point. However, I think that the flaw (if it indeed was) in John's argument is not in the form of combinatory completeness that he applies, but it is an illegal instance of substitution, which one has to be very careful with within a logic of partial terms where variables range over existing objects (as e.g. in E+ logic, presented in Troelstra & van Dalen, Vol. I). From IF FALSE x y >~ y one cannot conclude IF FALSE q r >~ r for q and r arbitrary terms. As to the definitive and correct form of combinatory completess in a c-pca I make the following proposition (which I have checked): Let A be a c-pca and t be a term built up using application from A-constants and variables. Then there is a term (\lambda x. t) that has the same free variables as t save x such that for all a\in A and all valuations of free variables (\lambda x. t) a >~ t[a/x] That means, if w.r.t. some valuation the right hand side denotes a value then the left hand side denotes the same value. In particular, if for some valuation and some a in A the right hand side exists (denotes a value) then so does the left hand side and hence (\lambda x. t) (for this particular valuation), as application is a strict function. The same is true for simultaneous abstraction (replace x and a by \vec{x} and \vec{a} resp.). One only needs to prove a little substitution lemma. This proposition is essentially in the Hyland-Ong paper (the small difference is that, in the paper all variables get abstracted away, but that is inessential). Best, Peter
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
Dear Jaap, John and Thomas, I am not yet convinced. What I do more or less believe is that the operation of `thunking' works for a c-pca. But it does *not* seem to be the case that the combinator S that John defined (using thunking) satisfies the equations Skxky(false)z = false and Skxkykz = (xkz)k(ykz) , even in a total combinatory algebra! As I do not trust my term manipulation skills so much any more in this context, I wrote a little Haskell Program to compute the normal forms. The left hand side terms are indeed normalizing but their normal forms are considerably longer than the respective right hand side terms. Oddly enough, the normal form of the former term even contains variables. Now it is very well possible that my program has a bug, programming is hardly my main occupation. If you like to play with it you are invited to access it via http://www.mathematik.tu-darmstadt.de/~lietz/cpca/cpca.hs and if you find a bug please do let me know. I cannot put my finger on exactly what is the gap in the proof. I think it has to do with the fact that thunk(e,c) does not commute with substitution in the way one might expect. Or put differently, the `thunk' algorithm and the Curry algorithm don't play along very well. Something in that direction. Finally, I should apologize for taxing the categories mailing list readers' patience with a subject that is likely only of marginal interest to most. have a nice weekend, Peter
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
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
participants (6)
-
Galchin Vasili -
John Longley -
jvoosten＠math.uu.nl -
Peter Lietz -
Prof. Peter Johnstone -
Thomas Streicher