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  [])