module Realisability.Base {β„“A} (pca@(𝔸 , _) : PCA β„“A) where

Realisability predicates over setsπŸ”—

If we have a fixed notion of computation given by a partial combinatory algebra we can think of the type of functions valued in the power set of as a type of β€œnonstandard predicates over ”, where some nonstandard predicate over assigns to each a set of values that witness the truth of .

More importantly, these realisability predicates can be equipped with a notion of entailment, again relative to Moreover, we can define this entailment relative to a function for a predicate over and a predicate over 1 We define the type of entailment witnesses to consist of programs which associate to each of a of

record
  [_]_⊒_ (f : X β†’ Y) (P : X β†’ ℙ⁺ 𝔸) (Q : Y β†’ ℙ⁺ 𝔸)
    : Type (level-of X βŠ” level-of Y βŠ” β„“A) where

  field
    realiser : ↯⁺ 𝔸
    tracks   : βˆ€ {x} {a : β†― ⌞ 𝔸 ⌟} (ah : a ∈ P x) β†’ realiser ⋆ a ∈ Q (f x)

Basic structural rulesπŸ”—

We can now investigate the basic rules of this realisability logic, which work regardless of what the chosen PCA is. First, we have that entailment is reflexive (the β€˜axiom’ rule) and transitive (the β€˜cut’ rule). These are witnessed by the identity program and, if witnesses and witnesses then the composition witnesses

id⊒ : [ id ] P ⊒ P
id⊒ {P = P} = record where
  realiser = val ⟨ x ⟩ x

  tracks ha = subst-∈ (P _) ha (abs-β _ [] (_ , P _ .def ha))

_∘⊒_ : βˆ€ {f g} β†’ [ g ] Q ⊒ R β†’ [ f ] P ⊒ Q β†’ [ g ∘ f ] P ⊒ R
_∘⊒_ {R = R} {P = P} α β = record where
  realiser = val ⟨ x ⟩ α `· (β `· x)

  tracks {a = a} ha = subst-∈ (R _) (α .tracks (β .tracks ha)) $
    (val ⟨ x ⟩ Ξ± `Β· (Ξ² `Β· x)) ⋆ a β‰‘βŸ¨ abs-Ξ² _ [] (a , P _ .def ha) βŸ©β‰‘
    Ξ± ⋆ (Ξ² ⋆ a)                   ∎

ConjunctionπŸ”—

As a representative example of logical realisability connective, we can define the conjunction of over a common base type. Fixing we define the set of for to be that is, a value witnesses if it is a pair and its first component witnesses and its second component witnesses We think of this as a strict definition, since it demands the witness to be literally, syntactically, a we could also have a lazy definition, where all we ask is that the witness be defined and its first and second projections witness and respectively, i.e.Β the set

_∧T_ : (P Q : X β†’ ℙ⁺ 𝔸) β†’ X β†’ ℙ⁺ 𝔸
(P ∧T Q) x .mem a = elΩ $
  Ξ£[ u ∈ β†― ⌞ 𝔸 ⌟ ] Ξ£[ v ∈ β†― ⌞ 𝔸 ⌟ ]
    a ≑ `pair ⋆ u ⋆ v Γ— u ∈ P x Γ— v ∈ Q x
(P ∧T Q) x .def = rec! Ξ» u v Ξ± rx ry β†’
  subst ⌞_⌟ (sym Ξ±) (`pair↓₂ (P _ .def rx) (Q _ .def ry))

With this strict definition, we can show that the conjunction implies both conjuncts, and these implications are tracked by the `fst and `snd projection programs respectively.

Ο€β‚βŠ’ : [ id ] (P ∧T Q) ⊒ P
Ο€β‚βŠ’ {P = P} {Q = Q} = record where
  realiser = `fst

  tracks {a = a} = elim! Ξ» p q Ξ± pp qq β†’ subst-∈ (P _) pp $
    `fst ⋆ a               β‰‘βŸ¨ ap (`fst ⋆_) Ξ± βŸ©β‰‘
    `fst ⋆ (`pair ⋆ p ⋆ q) β‰‘βŸ¨ `fst-Ξ² (P _ .def pp) (Q _ .def qq) βŸ©β‰‘
    p                      ∎

Ο€β‚‚βŠ’ : [ id ] (P ∧T Q) ⊒ Q
Ο€β‚‚βŠ’ {P = P} {Q = Q} = record where
  realiser = `snd

  tracks {a = a} = elim! Ξ» p q Ξ± pp qq β†’ subst-∈ (Q _) qq $
    `snd ⋆ a               β‰‘βŸ¨ ap (`snd ⋆_) Ξ± βŸ©β‰‘
    `snd ⋆ (`pair ⋆ p ⋆ q) β‰‘βŸ¨ `snd-Ξ² (P _ .def pp) (Q _ .def qq) βŸ©β‰‘
    q                      ∎

  1. If we think of and as contexts for the definitions of and then this 3-place entailment relation is defined relative to a substitution β†©οΈŽ