Re: Realizability and Partial Combinatory Algebras

[Peter Lietz <lietz@mathematik.tu-darmstadt.de>]

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,

....