In this paper a model for barrecursion is presented. It has as a novelty that it contains discontinuous functionals. The model is based on a concept called strong majorizability. This concept is a modification of Howard's majorizability notion; see [T, p. 456].

We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation.

The main result of this paper is the equivalence of several definition schemas of bar recursion occurring in the literature on functionals of finite type. We present the theory of functionals of finite type, in [T] denoted byqf-WE-HA ω, which is necessary for giving the equivalence proofs. Moreover we prove two results on this theory that cannot be found in the literature, namely the deduction theorem and a derivation of Spector's rule of extensionality from [S]: ifP→T 1=T 2 and Q[X∶≡T1], (...) then P→Q[X∶≡ T2], from the at first sight weaker rule obtained by omitting “P→”. (shrink)

The technical contribution of this paper is threefold.First we show how to encode functionals in a ‘flat’ applicative structure by adding oracles to untyped λ-calculus and mimicking the applicative behaviour of the functionals with an impredicatively defined reduction relation. The main achievement here is a Church-Rosser result for the extended reduction relation.Second, by combining the previous result with the model construction based on partial equivalence relations, we show how to extend a λ-closed simple type structure to a model of the (...) polymorphic λ-calculus.Third, we specialize the previous result to a counter model against a simple minimization. This minimization is realized by a bar recursive functional, which contrasts the results of Spector and Girard which imply that the bar recursive functions are exactly those that are definable in the polymorphic λ-calculus. As a spin-off, we obtain directly the non-conservativity of the extensions of Gödel's T with bar recursion, fan functional, and Luckhardt's minimization functional, respectively. For the latter two extensions these results are new. (shrink)

In this paper it will be shown that HEO and HRO E are isomorphic with respect to extensional equality. This answers a question of Troelstra [T, 2.4.12, p. 128]. The main problem is to extend effective operations to a larger domain. This will be achieved by a modification of the proof of the continuity of effective operations. Following a suggestion of A.S. Troelstra, similar results were obtained for ECF(U) and ICF E (U), where U is any universe of functions closed (...) under "recursive in". (shrink)

In this paper it will be shown that HEO and $HRO^E$ are isomorphic with respect to extensional equality. This answers a question of Troelstra [T, 2.4.12, p. 128]. The main problem is to extend effective operations to a larger domain. This will be achieved by a modification of the proof of the continuity of effective operations. Following a suggestion of A.S. Troelstra, similar results were obtained for ECF(U) and $ICF^E(U)$, where $U$ is any universe of functions closed under "recursive in".

The related fields of fractal image encoding and fractal image analysis have blossomed in recent years. This book, originating from a NATO Advanced Study Institute held in 1995, presents work by leading researchers. It is developing the subjects at an introductory level, but it also has some recent and exciting results in both fields. The book contains a thorough discussion of fractal image compression and decompression, including both continuous and discrete formulations, vector space and hierarchical methods, and algorithmic optimizations. The (...) book also discusses multifractal approaches to image analysis, segmentation, and recognition, including medical applications. (shrink)

We introduce a three-tiered framework for modelling and reasoning about agents who (i) can use possibly complete reasoning systems without any restrictions but who nevertheless are (ii) bounded in the sense that they never reach infinitely many results and, finally, who (iii) perform their reasoning in time. This last aspect does not concern so much the time it takes for agents to actually carry out their reasoning, as the time which can bring about external changes in the agents’ states such (...) as arriving of new information or discarding previously available information due to bounds of the agent’s resources. These three aspects are treated with the maximal possible degree of independence from each other. The treatment of layer (iii) can be combined with arbitrary logic at level (ii) which, in turn, can be combined with arbitrary agent logic at level (i). At the level (iii), we discuss briefly the duality (or rather, complementarity) of system descriptions based on actions and transitions, on the one hand, and states and their changes, on the other. We settle for the latter and present a simple language, for describing state changes, which is parameterized by an arbitrary language for describing properties of the states. The language can be viewed as a simple fragment of step logic, admitting however various extensions by appropriate choices of the underlying logic. Alternatively, it can be seen as a very specific fragment of temporal logic (with a variant of ‘until’ or ‘chop’ operator), and is interpreted over dense linear time. The reasoning system presented here is sound, as well as strongly complete and decidable (provided that so is the parameter logic for reasoning about single states). We give the main idea of the completeness proof and suggest a wide range of possible applications, which is a simple consequence of the parametric character of both the language and the reasoning system. We address then in more detail the case of non-omniscient rational agents, (ii). Their models are syntactic structures (sets of available formulae) similar in spirit, though not in the technical formulation, to the models used in other syntax oriented approaches and in active logic. We give a new sound, complete and decidable system for reasoning about such agents. Finally, we illustrate its extensions with the internal reasoning of agents, (i), by equipping them with some example logics. (shrink)