Proving totality of a function taking at most n recursive calls

Question

Let's say we're writing an implementation of a lambda calculus, and as a part of that we'd like to be able to choose a fresh non-clashing name:

record Ctx where
  constructor MkCtx
  bindings : List String

emptyCtx : Ctx
emptyCtx = MkCtx []

addCtx : String -> Ctx -> Ctx
addCtx name = record { bindings $= (name ::) }

pickName : String -> Ctx -> (String, Ctx)
pickName = go Z
  where
    mkName : Nat -> String -> String
    mkName Z name = name
    mkName n name = name ++ show n

    go n name ctx = let name' = mkName n name in
                    if name' `elem` bindings ctx
                       then go (S n) name ctx
                       else (name', addCtx name' ctx)

Idris totality checker thinks pickName is not total due to the recursive path in go, and rightfully so: indeed, the proof of totality does not rely on any term getting syntactically smaller, but rather on the observation that if bindings has k elements, then it'll take no more than k + 1 recursive calls to find a fresh name. But how to express this in code?

I also tend towards external verification in the sense of first writing a function and then writing a (type-checking, but never executing) proof of it having the right properties. Is it possible in this case of totality for pickName?

---

Inspired by @HTNW, looks like the right way is just using a Vect instead of a list. Removing the elements from the vector will make its size (which is expressed in type) syntactically smaller, avoiding the need to prove it myself. So, the (slightly refactored) version of pickName would be

pickName : String -> Vect n String -> String
pickName name vect = go Z vect
  where
    mkName : Nat -> String
    mkName Z = name
    mkName n = name ++ show n

    go : Nat -> Vect k String -> String
    go {k = Z} n _ = mkName n
    go {k = (S k)} n vect' =
      let name' = mkName n in
      case name' `isElem` vect' of
           Yes prf => go (S n) $ dropElem vect' prf
           No _ => name'

Answer 1

In the Prelude, we have:

Smaller x y = size x `LT` size y
instance Sized (List a) where size = length
sizeAccessible : Sized a => (x : a) -> Accessible Smaller x
accRec : (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
         (z : a) -> Accessible rel z -> b

accRec allows you to use "nonstandard recursion patterns" in a way the compiler can understand as total. It is basically fix : ((a -> b) -> (a -> b)) -> (a -> b), except the open-recursive function is obligated to pass an extra proof term to prove that the recursive argument is somehow "smaller". The Accessible argument is what determines the recursion pattern used; here it's the simple "decreasing Nat-size" patten. Preferably, we'd use sizeRec instead of accRec + sizeAccessible, but I can't make it work. Feel free to edit this with the "correct" way.

Every iteration of your function, you can delete the name if you find it.

delFirst : DecEq a => (x : a) -> (xs : List a)
        -> Maybe (ys : List a ** length xs = S (length ys))
delFirst _ [] = Nothing
delFirst x (y :: xs) with (decEq x y)
  delFirst x (x :: xs) | Yes Refl = Just (xs ** Refl)
  delFirst x (y :: xs) | No _ with (delFirst x xs)
    | Nothing = Nothing
    | Just (ys ** prf) = Just (x :: ys ** cong prf)

Now you can use open, well-founded recursion in pickName:

pickName : String -> Ctx -> (String, Ctx)
pickName s ctx = let new = go s (bindings ctx) Z
                  in (new, addCtx new ctx)
  where mkName : Nat -> String -> String
        mkName Z name = name
        mkName n name = name ++ show n
        ltFromRefl : n = S m -> LT m n
        ltFromRefl Refl = lteRefl
        go : String -> List String -> Nat -> String
        go name binds = accRec (\binds, rec, n =>
                          let name' = mkName n name
                           in case delFirst name' binds of
                                   Nothing => name'
                                   Just (binds' ** prf) => rec binds' (ltFromRefl prf) (S n)
                          ) binds (sizeAccessible binds)

A Nat -> a is the same thing as a Stream a, so IMO, this is somewhat nicer:

findNew : DecEq a => (olds : List a) -> (news : Stream a) -> a
findNew olds = accRec (\olds, rec, (new :: news) =>
                        case delFirst new olds of
                             Nothing => new
                             Just (olds' ** prf) => rec olds' (ltFromRefl prf) news
                      ) olds (sizeAccessible olds)
  where ltFromRefl : n = S m -> LT m n
        ltFromRefl Refl = lteRefl

pickName : String -> Ctx -> (String, Ctx)
pickName name ctx = let new = findNew (bindings ctx)
                                      (name :: map ((name ++) . show) (iterate S 1))
                     in (new, addCtx new ctx)

Which, I think, captures the intuition behind the idea that if you have an infinite supply of names, but there are only finitely many old ones, you surely have infinitely many new ones.

(Also, the logic in your code seems wrong. Did you flip the branches of the if?)