Comparing models of higher type computation

Abstract

Models of higher type computation appear basically in two avours as real izability models partial equivalence relations over some appropriate weak al gebraic model of function application and as some kind of limit preserving functionals for some suitably weakened notion of topology The aim of this presentation is to show that the two approaches are no di erent in the sense that provided a certain theorem can be proved about the limit structures the higher order structures de ned via the limit preserving functionals coincides with one de ned in terms of PER s Glimpses of this fact can be found in various guises in the literature see