open import 1Lab.Prelude

open import Data.Partial.Total
open import Data.Partial.Base
open import Data.Vec.Base

open import Realisability.PCA

import Realisability.Data.Pair
import Realisability.PCA.Sugar
import Realisability.Data.Sum

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

open Realisability.PCA.Sugar pca
open Realisability.Data.Pair pca
open Realisability.Data.Sum pca

private variable
  ℓ ℓ' ℓ'' : Level
  X Y Z : Type ℓ'
  n : Nat

Realisability predicates over sets🔗

If we have a fixed notion of computation given by a partial combinatory algebra $\mathbb{A}\text{,}$ we can think of the type of functions $X\to \mathbb{P}(\mathbb{A})$ valued in the power set of $\mathbb{A}$ as a type of “nonstandard predicates over $X$”, where some nonstandard predicate $P$ over $X$ assigns to each $x:X$ a set $P(x)\subseteq \mathbb{A}$ of values that witness the truth of $P$.

More importantly, these realisability predicates can be equipped with a notion of entailment, again relative to $\mathbb{A}\text{.}$ Moreover, we can define this entailment relative to a function $X\to Y\text{,}$ for $P$ a predicate over $X$ and $Q$ a predicate over $Y\text{.}$¹ We define the type of entailment witnesses $P{⊢}_{f}Q$ to consist of programs $\mathtt{r}:\mathbb{A}$ which associate to each $P\text{-realiser}$ $a$ of $x$ a $Q\text{-realiser}$ $\mathtt{r}\mathtt{a}$ of $fx\text{.}$

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)

  realiser↓ : ∀ {x} {a : ↯ ⌞ 𝔸 ⌟} (ah : a ∈ P x) → ⌞ realiser ⋆ a ⌟
  realiser↓ ah = Q _ .def (tracks  ah)

private unquoteDecl eqv' = declare-record-iso eqv' (quote [_]_⊢_)

open [_]_⊢_ public

instance
  tracks-to-term : ∀ {V : Type} {P : X → ℙ⁺ 𝔸} {Q : Y → ℙ⁺ 𝔸} {f : X → Y} → To-term V ([ f ] P ⊢ Q)
  tracks-to-term = record { to = λ x → const (x .realiser) }

  tracks-to-part : ∀ {P : X → ℙ⁺ 𝔸} {Q : Y → ℙ⁺ 𝔸} {f : X → Y} → To-part ([ f ] P ⊢ Q) ⌞ 𝔸 ⌟
  tracks-to-part = record { to-part = λ x → x .realiser .fst }

private
  variable P Q R : X → ℙ⁺ 𝔸

  subst-∈ : (P : ℙ⁺ 𝔸) {x y : ↯ ⌞ 𝔸 ⌟} → x ∈ P → y ≡ x → y ∈ P
  subst-∈ P hx p = subst (_∈ P) (sym p) hx

Basic structural rules🔗

We can now investigate the basic rules of this realisability logic, which work regardless of what the chosen PCA $\mathbb{A}$ 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 $\mathtt{f}$ witnesses $Q⊢R$ and $\mathtt{g}$ witnesses $P⊢Q\text{,}$ then the composition $$⟨x⟩\mathtt{f}(\mathtt{g}x)$$ witnesses $P⊢R\text{.}$

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 $\mathbb{A}\text{-predicates}$ over a common base type. Fixing $P,Q:X\to \mathbb{P}(\mathbb{A})\text{,}$ we define the set of $(P\wedge Q)\text{-realisers}$ for $x$ to be $$\{\mathtt{pair}uv|u,v:\mathbb{A},u\in P(x),v\in Q(x)\}$$ that is, a value $p:\mathbb{A}$ witnesses $(P\wedge Q)(x)$ if it is a pair and its first component witnesses $P(x)$ and its second component witnesses $Q(x)\text{.}$ We think of this as a strict definition, since it demands the witness to be literally, syntactically, a $\mathtt{pair}\text{;}$ we could also have a lazy definition, where all we ask is that the witness be defined and its first and second projections witness $P$ and $Q$ respectively, i.e. the set $$\{e|\mathtt{fst}e\in P(x),\mathtt{snd}e\in Q(x)\}\text{.}$$

_∧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                      ∎