← Back to branch summary

~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to src/Induction/Lexicographic.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Induction/Lexicographic.agda
 
1
------------------------------------------------------------------------
 
2
-- Lexicographic induction
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
module Induction.Lexicographic where
 
8
 
 
9
open import Induction
 
10
open import Data.Product
 
11
 
 
12
-- The structure of lexicographic induction.
 
13
 
 
14
_⊗_ : ∀ {ℓ} {A B : Set ℓ} →
 
15
      RecStruct A → RecStruct B → RecStruct (A × B)
 
16
_⊗_ RecA RecB P (x , y) =
 
17
  -- Either x is constant and y is "smaller", ...
 
18
  RecB (λ y' → P (x , y')) y
 
19
    ×
 
20
  -- ...or x is "smaller" and y is arbitrary.
 
21
  RecA (λ x' → ∀ y' → P (x' , y')) x
 
22
 
 
23
-- Constructs a recursor builder for lexicographic induction.
 
24
 
 
25
[_⊗_] : ∀ {ℓ} {A B : Set ℓ}
 
26
          {RecA : RecStruct A} → RecursorBuilder RecA →
 
27
          {RecB : RecStruct B} → RecursorBuilder RecB →
 
28
        RecursorBuilder (RecA ⊗ RecB)
 
29
[_⊗_] {RecA = RecA} recA {RecB = RecB} recB P f (x , y) =
 
30
  (p₁ x y p₂x , p₂x)
 
31
  where
 
32
  p₁ : ∀ x y →
 
33
       RecA (λ x' → ∀ y' → P (x' , y')) x →
 
34
       RecB (λ y' → P (x , y')) y
 
35
  p₁ x y x-rec = recB (λ y' → P (x , y'))
 
36
                      (λ y y-rec → f (x , y) (y-rec , x-rec))
 
37
                      y
 
38
 
 
39
  p₂ : ∀ x → RecA (λ x' → ∀ y' → P (x' , y')) x
 
40
  p₂ = recA (λ x → ∀ y → P (x , y))
 
41
            (λ x x-rec y → f (x , y) (p₁ x y x-rec , x-rec))
 
42
 
 
43
  p₂x = p₂ x
 
44
 
 
45
------------------------------------------------------------------------
 
46
-- Example
 
47
 
 
48
private
 
49
 
 
50
  open import Data.Nat
 
51
  open import Induction.Nat as N
 
52
 
 
53
  -- The Ackermann function à la Rózsa Péter.
 
54
 
 
55
  ackermann : ℕ → ℕ → ℕ
 
56
  ackermann m n = build [ N.rec-builder ⊗ N.rec-builder ]
 
57
                        AckPred ack (m , n)
 
58
    where
 
59
    AckPred : ℕ × ℕ → Set
 
60
    AckPred _ = ℕ
 
61
 
 
62
    ack : ∀ p → (N.Rec ⊗ N.Rec) AckPred p → AckPred p
 
63
    ack (zero  , n)     _                   = 1 + n
 
64
    ack (suc m , zero)  (_         , ackm•) = ackm• 1
 
65
    ack (suc m , suc n) (ack[1+m]n , ackm•) = ackm• ack[1+m]n