1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283-------------------------------------------------------------------------- The Agda standard library---- Lexicographic induction------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Induction.Lexicographic where open import Data.Product.Base using (Σ; _,_; _×_)open import Inductionopen import Level -- The structure of lexicographic induction. Σ-Rec : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : A → Set b} → RecStruct A (ℓ₁ ⊔ b) ℓ₂ → (∀ x → RecStruct (B x) ℓ₁ ℓ₃) → RecStruct (Σ A B) _ _Σ-Rec RecA RecB P (x , y) = -- Either x is constant and y is "smaller", ... RecB x (λ y′ → P (x , y′)) y × -- ...or x is "smaller" and y is arbitrary. RecA (λ x′ → ∀ y′ → P (x′ , y′)) x infixr 2 _⊗_ _⊗_ : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} → RecStruct A (ℓ₁ ⊔ b) ℓ₂ → RecStruct B ℓ₁ ℓ₃ → RecStruct (A × B) _ _RecA ⊗ RecB = Σ-Rec RecA (λ _ → RecB) -- Constructs a recursor builder for lexicographic induction. Σ-rec-builder : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : A → Set b} {RecA : RecStruct A (ℓ₁ ⊔ b) ℓ₂} {RecB : ∀ x → RecStruct (B x) ℓ₁ ℓ₃} → RecursorBuilder RecA → (∀ x → RecursorBuilder (RecB x)) → RecursorBuilder (Σ-Rec RecA RecB)Σ-rec-builder {RecA = RecA} {RecB = RecB} recA recB P f (x , y) = (p₁ x y p₂x , p₂x) where p₁ : ∀ x y → RecA (λ x′ → ∀ y′ → P (x′ , y′)) x → RecB x (λ y′ → P (x , y′)) y p₁ x y x-rec = recB x (λ y′ → P (x , y′)) (λ y y-rec → f (x , y) (y-rec , x-rec)) y p₂ : ∀ x → RecA (λ x′ → ∀ y′ → P (x′ , y′)) x p₂ = recA (λ x → ∀ y → P (x , y)) (λ x x-rec y → f (x , y) (p₁ x y x-rec , x-rec)) p₂x = p₂ x [_⊗_] : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {RecA : RecStruct A (ℓ₁ ⊔ b) ℓ₂} {RecB : RecStruct B ℓ₁ ℓ₃} → RecursorBuilder RecA → RecursorBuilder RecB → RecursorBuilder (RecA ⊗ RecB)[ recA ⊗ recB ] = Σ-rec-builder recA (λ _ → recB) -------------------------------------------------------------------------- Example private open import Data.Nat.Base open import Data.Nat.Induction as ℕ -- The Ackermann function à la Rózsa Péter. ackermann : ℕ → ℕ → ℕ ackermann m n = build [ ℕ.recBuilder ⊗ ℕ.recBuilder ] (λ _ → ℕ) (λ { (zero , n) _ → 1 + n ; (suc m , zero) (_ , ackm•) → ackm• 1 ; (suc m , suc n) (ack[1+m]n , ackm•) → ackm• ack[1+m]n }) (m , n)