module Realisability.Data.Nat {β„“} (𝔸 : PCA β„“) where

Natural numbers in a PCAπŸ”—

We define an encoding of natural numbers in a partial combinatory algebra using Curry numerals, which uses the encoding of booleans in a PCA and pairs in a PCA. The number zero is simply the identity function, and the successor of a number is given by pairing `false with that number. The first component of the pair thus encodes whether the number is zero.

`zero : ↯⁺ 𝔸
`zero = val ⟨ x ⟩ x

`suc : ↯⁺ 𝔸
`suc = val ⟨ x ⟩ `false `, x

Note that while the identity function may not look like a pair, since in our encoding projection from is implemented by applying itself to either `true (for the first component) or `false (for the second), the identity function actually behaves extensionally like the pairing of `true and `false.

`iszero : ↯⁺ 𝔸
`iszero = `fst

By recursion we can encode any number as a value of

`num : Nat β†’ ↯⁺ 𝔸
`num zero    = `zero
`num (suc x) = record
  { fst = `pair ⋆ `false ⋆ `num x
  ; snd = `pair↓₂ (abs↓ _ _) (`num x .snd)
  }

We can define the predecessor function succinctly using a conditional:

`pred : ↯⁺ 𝔸
`pred = val ⟨ x ⟩ `if (`fst `· x) then `zero else (`snd `· x)
The usual arguments show that these functions all compute as expected.
abstract
  `num-suc : βˆ€ x β†’ `num (suc x) .fst ≑ `suc ⋆ `num x
  `num-suc x = sym (abs-Ξ² _ _ (`num x))

  `suc↓₁ : ⌞ x ⌟ β†’ ⌞ `suc ⋆ x ⌟
  `suc↓₁ ah = subst ⌞_⌟ (sym (abs-Ξ²β‚™ [] ((_ , ah) ∷ []))) (`pair↓₂ (`false .snd) ah)

  `iszero-zero : `iszero ⋆ `zero ≑ `true .fst
  `iszero-zero = abs-Ξ² _ _ `zero βˆ™ abs-Ξ² _ _ (_ , abs↓ _ _)

  `iszero-suc : ⌞ x ⌟ β†’ `iszero ⋆ (`suc ⋆ x) ≑ `false .fst
  `iszero-suc {x} xh =
    `iszero ⋆ (`suc ⋆ x)           β‰‘βŸ¨ ap (`iszero ⋆_) (abs-Ξ² _ _ (_ , xh)) βŸ©β‰‘
    `iszero ⋆ (`pair ⋆ `false ⋆ x) β‰‘βŸ¨ `fst-Ξ² (`false .snd) xh βŸ©β‰‘
    `false .fst                    ∎

  `pred-zero : `pred ⋆ `zero ≑ `zero .fst
  `pred-zero =
    `pred ⋆ `zero                             β‰‘βŸ¨ abs-Ξ² _ _ `zero βŸ©β‰‘
    ⌜ `fst ⋆ `zero ⌝ ⋆ `zero ⋆ (`snd ⋆ `zero) β‰‘βŸ¨ ap (Ξ» e β†’ e ⋆ `zero ⋆ (`snd ⋆ `zero)) (`iszero-zero) βŸ©β‰‘
    `true ⋆ `zero ⋆ (`snd ⋆ `zero)            β‰‘βŸ¨ abs-Ξ²β‚™ [] ((_ , subst ⌞_⌟ (sym rem₁) (abs↓ _ _)) ∷ `zero ∷ []) βŸ©β‰‘
    `zero .fst                                ∎
    where
      rem₁ : `snd ⋆ `zero ≑ `false .fst
      rem₁ = abs-Ξ² _ _ `zero βˆ™ abs-Ξ² _ _ `false

  `pred-suc : ⌞ x ⌟ β†’ `pred ⋆ (`suc ⋆ x) ≑ x
  `pred-suc {x} xh =
    `pred ⋆ (`suc ⋆ x)                                   β‰‘βŸ¨ abs-Ξ² _ _ (_ , `suc↓₁ xh) βŸ©β‰‘
    ⌜ `fst ⋆ (`suc ⋆ x) ⌝ ⋆ `zero ⋆ (`snd ⋆ (`suc ⋆ x))  β‰‘βŸ¨ ap (Ξ» e β†’ e ⋆ `zero ⋆ (`snd ⋆ (`suc ⋆ x))) (ap (`fst ⋆_) (abs-Ξ² _ _ (_ , xh)) βˆ™ `fst-Ξ² (`false .snd) xh) βŸ©β‰‘
    `false ⋆ `zero ⋆ ⌜ `snd ⋆ (`suc ⋆ x) ⌝               β‰‘βŸ¨ ap (Ξ» e β†’ (`false ⋆ `zero) ⋆ e) (ap (`snd ⋆_) (abs-Ξ² _ _ (_ , xh)) βˆ™ `snd-Ξ² (`false .snd) xh) βŸ©β‰‘
    `false ⋆ `zero ⋆ x                                   β‰‘βŸ¨ abs-Ξ²β‚™ [] ((_ , xh) ∷ `zero ∷ []) βŸ©β‰‘
    x                                                    ∎

Primitive recursionπŸ”—

We define a recursor for natural numbers using the `Z fixed-point combinator. This will be a program which satisfies

First we define a worker function which is parametrised over both the β€˜recursive reference’ and all the arguments of the recursor (the zero and successor β€˜cases’ and the number itself). We can then apply `Z to everything to β€˜tie the knot’.

Note that, to ensure everything is properly defined, our `worker function produces cases that take an extra dummy argument; and our invocation of both its fixed point and its β€˜recursive reference’ pass `zero to get rid of this.

private
  `worker : ↯⁺ 𝔸
  `worker = val ⟨ rec ⟩ ⟨ zc ⟩ ⟨ sc ⟩ ⟨ num ⟩
    `if (`iszero `Β· num)
      then (`true `Β· zc)
      else (⟨ y ⟩ sc `· (`pred `· num) `· (rec `· zc `· sc `· (`pred `· num) `· `zero))

`primrec : ↯⁺ 𝔸
`primrec = val ⟨ z ⟩ ⟨ s ⟩ ⟨ n ⟩ `Z `· `worker `· z `· s `· n `· `zero
The typical PCA calculation fanfare shows us that `primrec is defined when applied to both one and two arguments, and that it computes as stated.
abstract
  `primrec↓₁ : ⌞ z ⌟ β†’ ⌞ `primrec ⋆ z ⌟
  `primrec↓₁ zh = subst ⌞_⌟ (sym (abs-Ξ²β‚™ [] ((_ , zh) ∷ []))) (abs↓ _ _)

  `primrec↓₂ : ⌞ z ⌟ β†’ ⌞ f ⌟ β†’ ⌞ `primrec ⋆ z ⋆ f ⌟
  `primrec↓₂ zh fh = subst ⌞_⌟ (sym (abs-Ξ²β‚™ [] ((_ , fh) ∷ (_ , zh) ∷ []))) (abs↓ _ _)

  `primrec-zero : ⌞ z ⌟ β†’ ⌞ f ⌟ β†’ `primrec ⋆ z ⋆ f ⋆ `zero ≑ z
  `primrec-zero {z} {f} zh fh =
    `primrec ⋆ z ⋆ f ⋆ `zero                                     β‰‘βŸ¨ abs-Ξ²β‚™ [] (`zero ∷ (_ , fh) ∷ (_ , zh) ∷ []) βŸ©β‰‘
    ⌜ `Z ⋆ `worker ⋆ z ⌝ ⋆ f ⋆ `zero ⋆ `zero                     β‰‘βŸ¨ ap (Ξ» e β†’ e ⋆ f ⋆ `zero ⋆ `zero) (`Z-Ξ² (`worker .snd) zh) βŸ©β‰‘
    ⌜ `worker ⋆ (`Z ⋆ `worker) ⋆ z ⋆ f ⋆ `zero ⌝ ⋆ `zero         β‰‘βŸ¨ ap (Ξ» e β†’ e ⋆ `zero) (abs-Ξ²β‚™ [] (`zero ∷ (_ , fh) ∷ (_ , zh) ∷ (_ , `Z↓₁ (`worker .snd)) ∷ [])) βŸ©β‰‘
    ⌜ `iszero ⋆ `zero ⋆ (`true ⋆ z) ⌝ % _ % `zero .fst           β‰‘βŸ¨ apβ‚‚ _%_ (apβ‚‚ _%_ (apβ‚‚ _%_ `iszero-zero refl) refl βˆ™ `true-Ξ² (`true↓₁ zh) (abs↓ _ _)) refl βŸ©β‰‘
    `true ⋆ z ⋆ `zero .fst                                       β‰‘βŸ¨ `true-Ξ² zh (`zero .snd) βŸ©β‰‘
    z                                                            ∎

  `primrec-suc : ⌞ z ⌟ β†’ ⌞ f ⌟ β†’ ⌞ x ⌟ β†’ `primrec ⋆ z ⋆ f ⋆ (`suc ⋆ x) ≑ f ⋆ x ⋆ (`primrec ⋆ z ⋆ f ⋆ x)
  `primrec-suc {z} {f} {x} zh fh xh =
    `primrec ⋆ z ⋆ f ⋆ (`suc ⋆ x)                                                 β‰‘βŸ¨ abs-Ξ²β‚™ [] ((_ , `suc↓₁ xh) ∷ (_ , fh) ∷ (_ , zh) ∷ []) βŸ©β‰‘
    ⌜ `Z ⋆ `worker ⋆ z ⌝ ⋆ f ⋆ (`suc ⋆ x) ⋆ `zero                                 β‰‘βŸ¨ ap (Ξ» e β†’ e ⋆ f ⋆ (`suc ⋆ x) ⋆ `zero) (`Z-Ξ² (`worker .snd) zh) βŸ©β‰‘
    `worker ⋆ (`Z ⋆ `worker) ⋆ z ⋆ f ⋆ (`suc ⋆ x) ⋆ `zero                         β‰‘βŸ¨ ap (Ξ» e β†’ e % `zero .fst) (abs-Ξ²β‚™ [] ((_ , `suc↓₁ xh) ∷ (_ , fh) ∷ (_ , zh) ∷ (_ , `Z↓₁ (`worker .snd)) ∷ [])) βŸ©β‰‘
    `iszero ⋆ (`suc ⋆ x) ⋆ (`true ⋆ z) % _ % `zero .fst                           β‰‘βŸ¨ apβ‚‚ _%_ (apβ‚‚ _%_ (apβ‚‚ _%_ (`iszero-suc xh) refl) refl βˆ™ `false-Ξ² (`true↓₁ zh) (abs↓ _ _)) refl βˆ™ abs-Ξ²β‚™ ((`suc ⋆ x , `suc↓₁ xh) ∷ (f , fh) ∷ (z , zh) ∷ (`Z ⋆ `worker , `Z↓₁ (`worker .snd)) ∷ []) (`zero ∷ []) βŸ©β‰‘
    f % `pred ⋆ (`suc ⋆ x) % `Z ⋆ `worker ⋆ z ⋆ f ⋆ (`pred ⋆ (`suc ⋆ x)) ⋆ `zero  β‰‘βŸ¨ ap (Ξ» e β†’ f % e % `Z ⋆ `worker ⋆ z ⋆ f ⋆ e ⋆ `zero) (`pred-suc xh) βŸ©β‰‘
    f ⋆ x ⋆ (`Z ⋆ `worker ⋆ z ⋆ f ⋆ x ⋆ `zero)                                    β‰‘βŸ¨ apβ‚‚ _%_ refl (sym (abs-Ξ²β‚™ [] ((_ , xh) ∷ (_ , fh) ∷ (_ , zh) ∷ []))) βŸ©β‰‘
    f ⋆ x ⋆ (`primrec ⋆ z ⋆ f ⋆ x)                                                ∎