Ordered combinatory algebras and realizability
Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, Alexandre Miquel · Mathematical Structures in Computer Science · 2015
We propose the new concept ofKrivine ordered combinatory algebra( $\mathcal{^KOCA}$ ) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013). We show that $\mathcal{^KOCA}$ 's are equivalent to Streicher'sabstract Krivine structuresfor the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class oftriposes. The difference between the two representations is that the elements of a $\mathcal{^KOCA}$ play both the role of truth values and realizers, whereas truth values aresetsof realizers in $\mathcal{AKS}$ s. To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a $\mathcal{^KOCA}$ , which showcases the dual role that is played by the elements of the $\mathcal{^KOCA}$ .