open import 1Lab.Prelude

open import Data.Partial.Total
open import Data.Partial.Base
open import Data.Fin.Base hiding (_<_ ; _≤_)
open import Data.Vec.Base

module Realisability.PCA where

Partial combinatory algebras🔗

private variable
  ℓ : Level
  A : Type ℓ
  n : Nat

A partial combinatory algebra (PCA) $\mathbb{A}$ is a set equipped with enough structure to model universal computation: a partial application operator¹ and a notion of abstraction elimination, which will be defined below. This structure is enough for $\mathbb{A}$ to model a simple programming language in the spirit of the untyped lambda calculus.

While the definition of PCA is austere, adapting traditional encoding techniques from untyped lambda calculus lets us show that PCAs support encoding booleans, pairs, sums, and even primitive recursion.

module _ {ℓ} (𝔸 : Type ℓ) where

  _ = 𝔸 → 𝔸 → ↯ 𝔸

  PAS : Type ℓ
  PAS = ↯ 𝔸 → ↯ 𝔸 → ↯ 𝔸

The inhabitants of a PCA🔗

If $\mathbb{A}$ is a partial combinatory algebra (or, more generally, a partial applicative structure), the inhabitants of the type $x:\mathbb{A}$ often serve dual purposes: they can be values or they can be programs. Of course, since PCAs implement a simple higher-order programming language, programs are a type of value. However, there are still situations where it is important to be clear which of these two roles a given $x:\mathbb{A}$ is serving.

Applying a program to a given value may not result in a value— execution could diverge, for example. We think of an arbitrary application like $\mathtt{f}\mathtt{x}$ as a computation, which may or may not produce a value— if it does produce a value, then it comes from exactly one value in $\mathbb{A}\text{.}$

Abstraction elimination🔗

The type of terms over $\mathbb{A}$ with $n$ free variables is defined inductively: A term is either one of the variables, a value drawn from $\mathbb{A}\text{,}$ or the application of a term to another.

data Term (A : Type ℓ) (n : Nat) : Type (level-of A) where
  var   : Fin n → Term A n
  const : ↯⁺ A → Term A n
  app   : Term A n → Term A n → Term A n

If we are given a term in $n$ variables and an environment, a list of $n$ values, we can define the evaluation of a term to be the computation obtained by looking each variable up in the environment, preserving embedded values, and using the partial applicative structure to interpret the app constructor. Moreover, if we have a term $t$ in $n+1$ variables and a term $x$ in $n$ variables, we can instantiate $t$ with $x$ to obtain a term in $n$ variables, where the zeroth variable used in $t$ has been replaced with $x$ throughout.

module eval (_%_ : PAS A) where
  eval : Term A n → Vec (↯⁺ A) n → ↯ A
  eval (var x)   ρ = lookup ρ x .fst
  eval (const x) ρ = x .fst
  eval (app f x) ρ = eval f ρ % eval x ρ

  inst : Term A (suc n) → Term A n → Term A n
  inst (var x) a with fin-view x
  ... | zero = a
  ... | suc i = var i
  inst (const a) _ = const a
  inst (app f x) a = app (inst f a) (inst x a)

These two operations are connected by the following lemma: evaluating a term instantiated with a value is the same as evaluating the original term in an extended environment.

  abstract
    eval-inst
      : (t : Term A (suc n)) (x : ↯⁺ A) (ρ : Vec (↯⁺ A) n)
      → eval (inst t (const x)) ρ ≡ eval t (x ∷ ρ)
    eval-inst (var i) y ρ with fin-view i
    ... | zero  = refl
    ... | suc j = refl
    eval-inst (const a) y ρ = refl
    eval-inst (app f x) y ρ = ap₂ _%_ (eval-inst f y ρ) (eval-inst x y ρ)

A partial applicative structure is a partial combinatory algebra when we have an operation abs sending terms $t$ in $n+1$ variables to terms $⟨x⟩t$ in $n$ variables which behave, under evaluation, as “functions of $x$”. In particular, functions should always be defined values (abs↓), and we have a restricted $\beta \text{-reduction}$ law (abs-β) saying that applying a function to a value should be the same as evaluating the body of the function instantiated with that value, or equivalently in an environment extended with that value.

record is-pca (_%_ : PAS A) : Type (level-of A) where
  open eval _%_ public
  field
    abs   : Term A (suc n) → Term A n
    abs↓  : (t : Term A (suc n)) (ρ : Vec (↯⁺ A) n) → ⌞ eval (abs t) ρ ⌟
    abs-β : (t : Term A (suc n)) (ρ : Vec (↯⁺ A) n) (a : ↯⁺ A)
          → eval (abs t) ρ % a .fst ≡ eval (inst t (const a)) ρ

  absₙ : (k : Nat) → Term A (k + n) → Term A n
  absₙ zero    e = e
  absₙ (suc k) e = absₙ k (abs e)

  _%ₙ_ : ∀ {n} → ↯ A → Vec (↯⁺ A) n → ↯ A
  a %ₙ []       = a
  a %ₙ (b ∷ bs) = (a %ₙ bs) % b .fst

  abstract
    abs-βₙ
      : {k n : Nat} {e : Term A (k + n)}
      → (ρ : Vec (↯⁺ A) n) (as : Vec (↯⁺ A) k)
      → (eval (absₙ k e) ρ %ₙ as) ≡ eval e (as ++ ρ)
    abs-βₙ ρ [] = refl
    abs-βₙ {e = e} ρ (x ∷ as) = ap (_% x .fst) (abs-βₙ ρ as) ∙ abs-β _ (as ++ ρ) x ∙ eval-inst e x (as ++ ρ)

record PCA-on (A : Type ℓ) : Type ℓ where
  infixl  _%_

  field
    has-is-set : is-set A
    _%_        : ↯ A → ↯ A → ↯ A
    has-is-pca : is-pca _%_

  open is-pca has-is-pca public

PCA : (ℓ : Level) → Type (lsuc ℓ)
PCA ℓ = Σ[ X ∈ Set ℓ ] PCA-on ∣ X ∣

module PCA {ℓ} (A : PCA ℓ) where
  open PCA-on (A .snd) public