Re: Realizibility and Partial Combinatory Algebras

Re: Realizibility and Partial Combinatory Algebras

[jvoosten]

> 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

Re: Realizibility and Partial Combinatory Algebras

[Prof. Peter Johnstone]

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

Re: Realizibility and Partial Combinatory Algebras

[Peter Lietz]

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

Re: Realizability and Partial Combinatory Algebras

[John Longley]

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

Re: Realizability and Partial Combinatory Algebras

[Peter Lietz]

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,

....

Re: Realizability and Partial Combinatory Algebras

[John Longley]

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

Realizibility and Partial Combinatory Algebras

[Galchin Vasili]

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

Re: Realizibility and Partial Combinatory Algebras

[John Longley]

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

Re: Realizibility and Partial Combinatory Algebras

[Thomas Streicher]

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

Re: Realizibility and Partial Combinatory Algebras

[Prof. Peter Johnstone]

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

Re: Realizibility and Partial Combinatory Algebras

[Peter Lietz]

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

Re: Realizibility and Partial Combinatory Algebras

[John Longley]

>  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