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 -