(Swansea University)

In JSL 63(2), Berardi, Bezem and Coquand proposed a realization PHI of the classical axiom of choice, that could be used to extract computational content from classical proofs. In order to prove correctness of PHI they introduced a rather ad-hoc and complicated notion of realizability based on an infinitary term system allowing to exploit PHI's intensional behavior.In the seminar I will give an alternative correctness proof in a purely extensional setting based on standard domain-theory, realizability and A-translation. I will concentrate on the technically somewhat simpler, but essentially equivalent problem of proving termination of the corresponding recursion.

The problem is illustrated by the following little story:

********************************************************************

Hackers on trial

A group of hackers, H_1, H_2, H_3, ... (infinitely many in fact), is accused of some offense.

The Professional Hacker's Investigation bureau, PHI, employs a panel, Y, questioning the hackers and deciding on how to penalize them.

Of course, the panel Y can only question finitely many hackers, but which and how many of them, will depend on the hackers' answers.

Together with the accusation the PHI office has received a record r = [(k1,a1),...,(kn,an)] saying that hacker H_ki has already given answer xi (i=1,...,n).

It is possible that Y can make a judgment on the basis of the given record r alone. If not, Y needs to question some further hacker H_k (where k is different from all ki).

H_k's answer will, of course, be the result of a hack: She breaks into PHI's computer system and sends faked requests to the PHI office for investigating the hackers with extended records of the form [(k1,x1),...,(kn,xn),(k,x)], where x is a possible answer. Based on PHI's reactions to these requests for various x, H_k will finally decide to give some answer.

Of course, also H_k can send only finitely many faked requests, but which and how many she will send will depend on PHI's reactions.

The question is: Will this trial ever end?

Mathematically, the panel Y and the hackers H_k can be modeled as continuous functionals

Y : [N -> A] -> P

H_k : [A -> P] -> A

where N = {1,2,3,...}, A is the type of possible answers given by hackers, and P is the type of possible penalties. The trial can now be described by the following recursive definition of a function

PHI : R -> P

where R is the type of records, that is, R = (N x A)^*. The definition of PHI reads

PHI [(k1,x1),...,(kn,xn)] =

Y ( lambda k if k = ki then xi else H_k ( lambda x PHI [(k1,x1),...,(kn,xn),(k,x)] ) endif )

Robert Recorde Room

Department of Computer Science