open import 1Lab.Prelude

open import Data.Partial.Total
open import Data.Partial.Base
open import Data.Vec.Base

open import Realisability.PCA

import Realisability.Data.Pair
import Realisability.PCA.Sugar

module Realisability.PCA.Fixpoint {ℓ} (𝔸 : PCA ℓ) where

open Realisability.PCA.Sugar 𝔸
open Realisability.Data.Pair 𝔸

private variable x y : ↯ ⌞ 𝔸 ⌟

Fixed-point combinators in a PCA🔗

Since partial combinatory algebras encode untyped higher-order computation, we can import the definition of fixed-point combinators from untyped lambda calculus to arbitrary programs in a PCA. The most useful of these will be the `Z combinator, which satisfies $$\mathtt{Z}\mathsf{f}\mathsf{a}=\mathsf{f}(\mathtt{Z}\mathsf{f})\mathsf{a}\text{,}$$ and is always defined when applied to a single argument — that is, it lets us compute ‘functions of at least one argument’ by arbitrary recursion, such that the recursive function itself is always defined— though of course applying the recursive function might still lead to something undefined.

We introduce an intermediate combinator `X, and define `Z as the self-application of `X.

`X : ↯⁺ 𝔸
`X = val ⟨ x ⟩ ⟨ y ⟩ ⟨ z ⟩ y `· (x `· x `· y) `· z

`Z : ↯⁺ 𝔸
`Z = record
  { fst = `X ⋆ `X
  ; snd = subst ⌞_⌟ (sym (abs-βₙ [] (`X ∷ []))) (abs↓ _ _)
  }

This lets us prove the desired properties of `Z.

abstract
  `Z↓₁ : ⌞ x ⌟ → ⌞ `Z ⋆ x ⌟
  `Z↓₁ {x} xh = subst ⌞_⌟ (sym (abs-βₙ [] ((x , xh) ∷ `X ∷ []))) (abs↓ _ _)

  `Z-β : ⌞ x ⌟ → ⌞ y ⌟ → `Z ⋆ x ⋆ y ≡ x ⋆ (`Z ⋆ x) ⋆ y
  `Z-β {x} {y} xh yh =
    `X ⋆ `X ⋆ x ⋆ y        ≡⟨ abs-βₙ [] ((y , yh) ∷ (x , xh) ∷ `X ∷ []) ⟩≡
    x ⋆ (`X ⋆ `X ⋆ x) ⋆ y  ≡⟨⟩
    x ⋆ (`Z ⋆ x) ⋆ y       ∎