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 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)
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 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 β
If we think of and as contexts for the definitions of and then this 3-place entailment relation is defined relative to a substitution β©οΈ