============================
 =                          =
 =  Example: bar recursion  =
 =                          =
 ============================

    Chuangjie Xu, July 2019


Here we present only the construction of general-bar-recursion
functionals via the translation. The correctness proof is available at

    http://cj-xu.github.io/agda/BRCT/BRCT.html

References.

β–‘ Paulo Oliva and Silvia Steila.  A direct proof of Schwichtenberg's
  bar recursion closure theorem.  The Journal of Symbolic Logic 83 (1)
  (2018) 70–83.


\begin{code}

{-# OPTIONS --without-K --safe #-}

open import Preliminaries
open import T

module BarRecursion (Οƒ : Set) where

\end{code}

β–  Preliminaries

\begin{code}

data 𝟚 : Set where
 𝟎 𝟏 : 𝟚

minΒ² : 𝟚 β†’ 𝟚 β†’ 𝟚
min² 𝟎 b = 𝟎
min² 𝟏 b = b

Le : β„• β†’ β„• β†’ 𝟚
Le  n        0       = 𝟎
Le  0       (succ m) = 𝟏
Le (succ n) (succ m) = Le n m

data _* (A : Set) : Set where
 ⟨⟩  : A *
 _,_ : A β†’ A * β†’ A *

∣_∣ : {A : Set} β†’ A * β†’ β„•
∣ ⟨⟩ ∣ = 0
∣ _ , u ∣ = succ ∣ u ∣

_✢_ : {A : Set} β†’ A * β†’ A β†’ A *
⟨⟩       ✢ y = y , ⟨⟩
(x , xs) ✢ y = x , (xs ✢ y)

_^ : β„• * β†’ β„•α΄Ί
(⟨⟩ ^)        i       = 0
((n , ns) ^)  0       = n
((n , ns) ^) (succ i) = (ns ^) i

≀-dec : (n m : β„•) β†’ (n > m) + (n ≀ m)
≀-dec  0        m = inr ≀zero
≀-dec (succ n)  0 = inl (≀succ ≀zero)
≀-dec (succ n) (succ m) with ≀-dec n m
≀-dec (succ n) (succ m) | inl r = inl (≀succ r)
≀-dec (succ n) (succ m) | inr r = inr (≀succ r)

_-_ : β„• β†’ β„• β†’ β„•
0      - m      = 0
succ n - 0      = succ n
succ n - succ m = n - m

\end{code}

β–  A nucleus for general-bar-recursion functionals

\begin{code}

β„•α΅’ : Set
β„•α΅’ = (β„•α΄Ί β†’ β„•) Γ— (β„• * β†’ 𝟚) Γ— ((β„• * β†’ Οƒ) β†’ (β„• * β†’ (β„• β†’ Οƒ) β†’ Οƒ) β†’ β„• * β†’ Οƒ)

V : β„•α΅’ β†’ β„•α΄Ί β†’ β„•
V = pr₁

S : β„•α΅’ β†’ β„• * β†’ 𝟚
S = pr₁ ∘ prβ‚‚

B : β„•α΅’ β†’ (β„• * β†’ Οƒ) β†’ (β„• * β†’ (β„• β†’ Οƒ) β†’ Οƒ) β†’ β„• * β†’ Οƒ
B = prβ‚‚ ∘ prβ‚‚

Ξ· : β„• β†’ β„•α΅’
Ξ· n = (Ξ» Ξ± β†’ n) , (Ξ» s β†’ 𝟏) , (Ξ» G H β†’ G)

ΞΊ : (β„• β†’ β„•α΅’) β†’ β„•α΅’ β†’ β„•α΅’
ΞΊ g x = (Ξ» Ξ± β†’ V (g (V x Ξ±)) Ξ±)
      , (Ξ» s β†’ minΒ² (S x s) (S (g (V x (s ^))) s))
      , (Ξ» G H β†’ B x (Ξ» s β†’ B (g (V x (s ^))) G H s) H)

βŸͺ_⟫ʸ : Ty β†’ Set
βŸͺ ΞΉ ⟫ʸ     = β„•α΅’
βŸͺ Ο„ β‡Ύ ρ ⟫ʸ = βŸͺ Ο„ ⟫ʸ β†’ βŸͺ ρ ⟫ʸ

βŸͺ_⟫ˣ : Cxt β†’ Set
βŸͺ Ξ΅ ⟫ˣ = πŸ™
βŸͺ Ξ“ β‚Š ρ ⟫ˣ = βŸͺ Ξ“ ⟫ˣ Γ— βŸͺ ρ ⟫ʸ

_₍_β‚Žα΅’ : {Ξ“ : Cxt} {ρ : Ty} β†’ βŸͺ Ξ“ ⟫ˣ β†’ βˆ₯ ρ ∈ Ξ“ βˆ₯ β†’ βŸͺ ρ ⟫ʸ
(_ , a) ₍ zero β‚Žα΅’   = a
(Ξ³ , _) ₍ succ i β‚Žα΅’ = Ξ³ ₍ i β‚Žα΅’

KE : {ρ : Ty} β†’ (β„• β†’ βŸͺ ρ ⟫ʸ) β†’ β„•α΅’ β†’ βŸͺ ρ ⟫ʸ
KE {ΞΉ}     g = ΞΊ g
KE {Ο„ β‡Ύ ρ} g = Ξ» x a β†’ KE (Ξ» z β†’ g z a) x

βŸͺ_⟫ᡐ : {Ξ“ : Cxt} {ρ : Ty} β†’ T Ξ“ ρ β†’ βŸͺ Ξ“ ⟫ˣ β†’ βŸͺ ρ ⟫ʸ
βŸͺ Var i ⟫ᡐ Ξ³ = Ξ³ ₍ i β‚Žα΅’
βŸͺ Lam t ⟫ᡐ Ξ³ = Ξ» a β†’ βŸͺ t ⟫ᡐ (Ξ³ , a)
βŸͺ f Β· a ⟫ᡐ Ξ³ = βŸͺ f ⟫ᡐ Ξ³ (βŸͺ a ⟫ᡐ Ξ³)
βŸͺ Zero ⟫ᡐ  _ = Ξ· 0
βŸͺ Succ ⟫ᡐ  _ = ΞΊ (Ξ· ∘ succ)
βŸͺ Rec ⟫ᡐ   _ = Ξ» a f β†’ KE (rec a (f ∘ Ξ·))

_α΅’ : {ρ : Ty} β†’ T Ξ΅ ρ β†’ βŸͺ ρ ⟫ʸ
t α΅’ = βŸͺ t ⟫ᡐ ⋆

--
-- Ξ¨ k is a (T-definable) functional of bar recursion
-- for constant Y with value k
-- [Oliva&Steila2018, Lemma 2.1]
--
Ξ¨ : β„• β†’ (β„• * β†’ Οƒ) β†’ (β„• * β†’ (β„• β†’ Οƒ) β†’ Οƒ) β†’ β„• * β†’ Οƒ
Ξ¨ k G H s with ≀-dec ∣ s ∣ k
Ξ¨ k G H s | inl |s|>k = G s
Ξ¨ k G H s | inr |s|≀k = ψ G H (succ k - ∣ s ∣) s
 where
  ψ : (β„• * β†’ Οƒ) β†’ (β„• * β†’ (β„• β†’ Οƒ) β†’ Οƒ) β†’ β„• β†’ β„• * β†’ Οƒ
  ψ G H  0       = G
  ψ G H (succ n) = Ξ» s β†’ H s (Ξ» x β†’ ψ G H n (s ✢ x))

Ξ© : β„•α΅’ β†’ β„•α΅’
Ξ© = ΞΊ (Ξ» n β†’ (Ξ» Ξ± β†’ Ξ± n) , (Ξ» s β†’ Le n ∣ s ∣) , Ξ¨ n)

--
-- termination predicate
--
𝑆 : T Ξ΅ ((ΞΉ β‡Ύ ΞΉ) β‡Ύ ΞΉ)
  β†’ β„• * β†’ 𝟚
𝑆 Y = S ((Y α΅’) Ξ©)

--
-- 𝐡 Y is functional of general bar recursion for 𝑆 Y.
--
𝐡 : T Ξ΅ ((ΞΉ β‡Ύ ΞΉ) β‡Ύ ΞΉ)
  β†’ (β„• * β†’ Οƒ) β†’ (β„• * β†’ (β„• β†’ Οƒ) β†’ Οƒ) β†’ β„• * β†’ Οƒ
𝐡 Y = B ((Y α΅’) Ξ©)

\end{code}