module Realisability.Data.Nat {β} (πΈ : PCA β) where
open Realisability.PCA.Fixpoint πΈ open Realisability.PCA.Sugar πΈ open Realisability.Data.Pair πΈ open Realisability.Data.Bool πΈ private variable f g x y z : β― β πΈ β
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) β