Ordered combinatory algebras and realizability

TY - JOUR

T1 - Ordered combinatory algebras and realizability

AU - Santos, Walter Ferrer

AU - Frey, Jonas

AU - Guillermo, Mauricio

AU - Malherbe, Octavio

AU - Miquel, Alexandre

PY - 2017/3/1

Y1 - 2017/3/1

N2 - We propose the new concept of Krivine ordered combinatory algebra (κOCA) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013). We show that κOCA's are equivalent to Streicher's abstract Krivine structures for the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class of triposes. The difference between the two representations is that the elements of a κOCA play both the role of truth values and realizers, whereas truth values are sets of realizers in AKSs. To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a κOCA, which showcases the dual role that is played by the elements of the κOCA.

AB - We propose the new concept of Krivine ordered combinatory algebra (κOCA) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013). We show that κOCA's are equivalent to Streicher's abstract Krivine structures for the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class of triposes. The difference between the two representations is that the elements of a κOCA play both the role of truth values and realizers, whereas truth values are sets of realizers in AKSs. To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a κOCA, which showcases the dual role that is played by the elements of the κOCA.

U2 - 10.1017/S0960129515000432

DO - 10.1017/S0960129515000432

M3 - Journal article

SN - 0960-1295

VL - 27

SP - 428

EP - 458

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

IS - 3

ER -