------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic induction
------------------------------------------------------------------------

module Induction.Lexicographic where

open import Induction
open import Data.Product

-- The structure of lexicographic induction.

Σ-Rec :  {} {A : Set } {B : A  Set } 
        RecStruct A  (∀ 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

_⊗_ :  {} {A B : Set } 
      RecStruct A  RecStruct B  RecStruct (A × B)
RecA  RecB = Σ-Rec RecA  _  RecB)

-- Constructs a recursor builder for lexicographic induction.

Σ-rec-builder :
   {} {A : Set } {B : A  Set }
    {RecA : RecStruct A}
    {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 : Set } {RecA : RecStruct A} {RecB : RecStruct B} 
        RecursorBuilder RecA  RecursorBuilder RecB 
        RecursorBuilder (RecA  RecB)
[ recA  recB ] = Σ-rec-builder recA  _  recB)

------------------------------------------------------------------------
-- Example

private

  open import Data.Nat
  open import Induction.Nat as N

  -- The Ackermann function à la Rózsa Péter.

  ackermann :     
  ackermann m n =
    build [ N.rec-builder  N.rec-builder ]
           _  )
           { (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)