Hostname: page-component-7bb8b95d7b-wpx69 Total loading time: 0 Render date: 2024-10-04T01:20:09.810Z Has data issue: false hasContentIssue false
  • English
  • Français

A note on inequivalence of realizability toposes

Published online by Cambridge University Press:  24 October 2008

P. T. Johnstone  and
E. P. Robinson
P. T. Johnstone
Affiliation:
Department of Pure Mathematics, University of Cambridge, Cambridge CB2 1SB
E. P. Robinson
Affiliation:
Department of Computing and Information Science, Queen's University, Kingston, Ont. K7L 3N6, Canada
Get access Rights & Permissions [Opens in a new window]

Extract

The general construction of realizability toposes was first described in [3]. The data from which such a topos is constructed (called a partial applicative structure in [3]) consists of a set A equipped with a partial binary operation (called application and denoted by juxtaposition, with the convention that unbracketed expressions are evaluated from left to right) and two constants K, S satisfying

for all x, y, z ∈ A (where, as usual, an equality between possibly undefined terms means ‘one side is defined iff the other is, and then they are equal’). Following Lambek [6], we now call such a structure a partial Schönfinkel algebra, or a global Schönfinkel algebra if application is defined on the whole of A × A. (The name ‘combinatory algebra’ is also in common use.) We write for the realizability topos constructed from A.

Type
Research Article
Information
Mathematical Proceedings of the Cambridge Philosophical Society , Volume 105 , Issue 1 , January 1989 , pp. 1 - 3
Copyright
Copyright © Cambridge Philosophical Society 1989

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Carboni, A., Freyd, P. J. and Scedrov, A.. A categorical approach to realizability and polymorphic types. In Mathematical Foundations of Programming Language Semantics 3, New Orleans 1987. (To appear.)Google Scholar
[2]Hyland, J. M. E.. The effective topos. In The L. E. J. Brouwer Centenary Symposium. Studies in Logic vol. 110 (North-Holland, 1982), pp. 165–216.Google Scholar
[3]Hyland, J. M. E., Johnstone, P. T. and Pitts, A. M.. Tripos theory. Math. Proc. Cambridge Philos. Soc. 88 (1980), 205–232.CrossRefGoogle Scholar
[4]Hyland, J. M. E., Robinson, E. P. and Rosolini, G.. The discrete objects in the effective topos. (To appear.)Google Scholar
[5]Johnstone, P. T.. Topos Theory. London Math. Soc. Monographs no. 10 (Academic Press, 1977).Google Scholar
[6]Lambek, J.. From λ-calculus to cartesian closed categories. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (Academic Press, 1980), pp. 375–402.Google Scholar