[Agda] Termination proof in partiality monad

[Dan Doel]

Greetings.

I've been playing a bit with this since your initial mail, and thought I'd 
show you what I have so far. Unfortunately, I haven't found a way to prove 
termination of factorial defined with the fixed point combinator. However, a 
recursive factorial written directly in the partiality monad is fairly simple. 
Code follows. The module Prelim contains definitions for the natural numbers 
and sigma types. I split up the modules because otherwise Agda gobbles up all 
my memory. :)

------------------

module Partial where

codata D (a : Set) : Set where
  now   : (x : a)    -> D a
  later : (dx : D a) -> D a

never : {a : Set} -> D a
never ~ later never

return : {a : Set} -> a -> D a
return = now

infixl 40 _>>=_
_>>=_ : {a b : Set} -> D a -> (a -> D b) -> D b
now a    >>= f ~ f a
later da >>= f ~ later (da >>= f)

race : {a : Set} -> D a -> D a -> D a
race (now a)    _           ~ now a
race (later da) (now a)     ~ now a
race (later da) (later da') ~ later (race da da')

map-D : {a b : Set} -> (a -> b) -> D a -> D b
map-D f (now x)    ~ now (f x)
map-D f (later dx) ~ later (map-D f dx)

fix-aux : {a b : Set} -> (a -> D b) -> ((a -> D b) -> a -> D b) -> a -> D b
fix-aux k f a with f k a
...           | now b   ~ now b
...           | later d ~ later (fix-aux (f k) f a)

fix : {a b : Set} -> ((a -> D b) -> a -> D b) -> a -> D b
fix = fix-aux (\_ -> never)

------------------

module Convergence where

open import Prelim
open import Partial

mutual
  _↓_ : {a : Set} -> (x : D a) -> (v : a) -> Set
  now v    ↓ v' = ConvergeNow (now v) v'
  later dv ↓ v  = ConvergeLater dv v

  data ConvergeNow {a : Set} : D a -> a -> Set where
    converge-now : (x : a) -> ConvergeNow (now x) x

  data ConvergeLater {a : Set} (dv : D a) (v : a) : Set where
    converge-later : (pf : dv ↓ v) -> ConvergeLater dv v

_↓ : {a : Set} -> D a -> Set
_↓ {a} dx = Σ a (_↓_ dx)

map-D-↓ : {a b : Set} {dx : D a} {v : a}
        -> (f : a -> b) -> dx ↓ v -> map-D f dx ↓ f v
map-D-↓ {a}{b}{now v}{.v} f (converge-now .v) = converge-now (f v)
map-D-↓ {a}{b}{later dv} {v} f (converge-later pf)
  = converge-later (map-D-↓ f pf)

>>=-↓ :  {a b : Set} {f : a -> D b} {dx : D a} {v : a} {v' : b}
      -> dx ↓ v -> f v ↓ v' -> (dx >>= f) ↓ v'
>>=-↓ {a}{b}{f}{now v}    (converge-now .v)   pf  = pf
>>=-↓ {a}{b}{f}{later dv} (converge-later pf) pf' 
    = converge-later (>>=-↓ pf pf')

------------------

module Factorial where

open import Prelim
open import Partial
open import Convergence

-- A direct factorial
fac' : Nat -> D Nat
fac' 0       ~ return 1
fac' (suc n) ~ later (map-D (_*_ (suc n)) (fac' n))

fac'-↓ : forall {n} -> fac' n ↓
fac'-↓ {0}     = (1 , converge-now 1)
fac'-↓ {suc n} with fac'-↓ {n}
...            | (n! , pf-n!-↓) = let suc-n! = suc n * n!
                                      pf' = map-D-↓ (_*_ (suc n)) pf-n!-↓
                                  in (suc-n! , converge-later pf')

fac-aux : (Nat -> D Nat) -> Nat -> D Nat
fac-aux _   zero    = return 1
fac-aux fac (suc n) = map-D (_*_ (suc n)) (fac n)

fac : Nat -> D Nat
fac = fix fac-aux

fac-↓ : forall {n} -> fac n ↓
fac-↓ {0}     = (1 , converge-now 1)
fac-↓ {suc n} with fac-↓ {n}
...           | (n! , pf-n!-↓) = let suc-n! = suc n * n!
                                     pf' = map-D-↓ (_*_ (suc n)) pf-n!-↓
                                  in (suc-n! , converge-later ?  )

------------------

So, there you have it so far. fac'-↓ is a relatively easy proof. I've tried a 
similar scheme for fac-↓, but get stuck in the inductive case. The blank needs 
to be filled with something of type:

    fix-aux (fac-aux (\_ -> never)) fac-aux (suc n) ↓ n! + n * n!

And my pf' is merely an:

    map-D (_*_ (suc n)) (fix-aux (\_ -> never) fac-aux n ↓ n! + n * n!

Which looks like an unfolding issue, but probably one that's complex enough to 
require some lemmas to work through.

On a related note, I'm seeing things like this in my lower buffer:

   fix-aux (\_ -> never) fac-aux n | fac-aux (\_ -> never) n)

(In the 'type' in the error message for instance). What does 'foo | bar' mean? 
I don't recall ever seeing that before.

Cheers,
-- Dan