module Realisability.Data.Bool {ℓ} (𝔸 : PCA ℓ) where
Booleans in a PCA🔗
We construct booleans in a partial combinatory algebra by defining boolean values to be functions which select one of their two arguments. In effect, we are defining booleans so that the program is simply Therefore, we have:
`true : ↯⁺ 𝔸 `true = val ⟨ x ⟩ ⟨ y ⟩ x `false : ↯⁺ 𝔸 `false = val ⟨ x ⟩ ⟨ y ⟩ y
We define an overloaded notation for constructing terms which case on a boolean.
`if_then_else_ : ⦃ _ : To-term V A ⦄ ⦃ _ : To-term V B ⦄ ⦃ _ : To-term V C ⦄ → A → B → C → Termʰ V `if x then y else z = x `· y `· z
We can prove the following properties: applying `true
and `false
to a single argument
results in a defined value; `true
selects its first
argument; and `false
selects its second
argument.
abstract `true↓₁ : ⌞ a ⌟ → ⌞ `true ⋆ a ⌟ `true↓₁ x = subst ⌞_⌟ (sym (abs-βₙ [] ((_ , x) ∷ []))) (abs↓ _ _) `false↓₁ : ⌞ a ⌟ → ⌞ `false ⋆ a ⌟ `false↓₁ ah = subst ⌞_⌟ (sym (abs-βₙ [] ((_ , ah) ∷ []))) (abs↓ _ _) `true-β : ⌞ a ⌟ → ⌞ b ⌟ → `true ⋆ a ⋆ b ≡ a `true-β {a} {b} ah bh = abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ []) `false-β : ⌞ a ⌟ → ⌞ b ⌟ → `false ⋆ a ⋆ b ≡ b `false-β {a} {b} ah bh = abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ [])
We can define negation using `if_then_else_
, and show
that it computes as expected.
`not : ↯⁺ 𝔸 `not = val ⟨ x ⟩ `if x then `false else `true abstract `not-βt : `not ⋆ `true ≡ `false .fst `not-βt = abs-β _ [] `true ∙ abs-βₙ [] (`true ∷ `false ∷ []) `not-βf : `not ⋆ `false ≡ `true .fst `not-βf = abs-β _ [] `false ∙ abs-βₙ [] (`true ∷ `false ∷ [])