termination metric for recursive functions on nested data types

[yiyunliu]

Given the following definition of a general tree:

data GTree = GTree Int [GTree]

I'd like to perform induction based on the following treeSize function:

treeSize :: GTree -> Int
treeSize (GTree _ []) = 0
-- recursive call to treeSize h is fine, but treeSize (GTree x hs) gives termination error
treeSize (GTree x (h:hs)) = 1 + treeSize h + treeSize (GTree x hs)

However, it is impossible to define treeSize as a measure since the second recursive call: treeSize (GTree x hs) is not structural.

The second approach is to define two mutually recursive functions:

treeSize' :: GTree -> Int
treeSize' (GTree _ hs) = 1 + treesSize hs

treesSize :: [GTree] -> Int
treesSize [] = 0
treesSize (h:hs) = treeSize' h + treesSize hs

This fails termination check as well. In fact, it is kind of circular: we want to use treeSize as a termination metric because it enables us to define other mutually recursive functions (GTree -> a, [GTree] -> a).

In Coq, it is possible to inline the treesSize helper function so the recursive call to treeSize' is still structural:

treeSize'' :: GTree -> Int
treeSize'' (GTree _ hs) =
  let f hs =
        case hs of
          [] -> 0
          (h:hs') -> treeSize'' h + f hs' in
  f hs + 1

This is not possible in LH since recursive helper function such as f is not supported (even if it's non-recursive, LH can reflect but still won't be able to reason about it).

Is there any workaround for this issue or do I have to disable termination check? Thanks!

[ranjitjhala]

Hmm take a look here

https://github.com/pzp1997/liquid-heaps/blob/master/BinomialHeap.hs

they seem to have resolved this problem?

On Mon, Jun 8, 2020 at 2:31 PM Yiyun Liu notifications@github.com wrote:

Given the following definition of a general tree:

data GTree = GTree Int [GTree]

I'd like to perform induction based on the following treeSize function:

treeSize :: GTree -> Int treeSize (GTree _ []) = 0-- recursive call to treeSize h is fine, but treeSize (GTree x hs) gives termination error treeSize (GTree x (h:hs)) = 1 + treeSize h + treeSize (GTree x hs)

However, it is impossible to define treeSize as a measure since the second recursive call: treeSize (GTree x hs) is not structural.

The second approach is to define two mutually recursive functions:

treeSize' :: GTree -> Int treeSize' (GTree _ hs) = 1 + treesSize hs treesSize :: [GTree] -> Int treesSize [] = 0 treesSize (h:hs) = treeSize' h + treesSize hs

This fails termination check as well. In fact, it is kind of circular: we want to use treeSize as a termination metric because it enables us to define other mutually recursive functions (GTree -> a, [GTree] -> a).

In Coq, it is possible to inline the treesSize helper function so the recursive call to treeSize' is still structural:

treeSize'' :: GTree -> Int treeSize'' (GTree _ hs) = let f hs = case hs of [] -> 0 (h:hs') -> treeSize'' h + f hs' in f hs + 1

This is not possible in LH since recursive helper function such as f is not supported (even if it's non-recursive, LH can reflect but still won't be able to reason about it).

Is there any workaround for this issue or do I have to disable termination check? Thanks!

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1685__;!!Mih3wA!W3ZqI6hiKlIkOIdG66D1aCKOWZKGIcAq7wJALzQLMQk1PjWrXZzK8b7Zqa95P8_s$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OEYM6KOZSRCD5SILS3RVVKCXANCNFSM4NYZFKFA__;!!Mih3wA!W3ZqI6hiKlIkOIdG66D1aCKOWZKGIcAq7wJALzQLMQk1PjWrXZzK8b7Zqa4jkdLt$ .

[yiyunliu]

Interesting. If I make an explicit field for size with proper refinements, then it's possible to prove termination:

{-@ LIQUID "--reflection" @-}
module Term where
{-@ data GTree =
      GTree { elem :: Int, subtrees :: [GTree]
            , treeSize :: {v:Int | v > 0 && v == treeListSize subtrees + 1}} @-}
data GTree = GTree {elem :: Int, subtrees :: [GTree], treeSize :: Int}

{-@ measure treeListSize @-}
{-@ treeListSize :: [GTree] -> Nat @-}
treeListSize :: [GTree] -> Int
treeListSize [] = 0
treeListSize (h:hs) = treeSize h + treeListSize hs

-- using the termination metric we defined

-- the simplest proof combinator
{-@ reflect cast @-}
cast :: a -> b -> b
cast _ x = x

-- mutually recursive functions
{-@ reflect sumGTree @-}
{-@ sumGTree :: w:GTree -> Int / [treeSize w, 0] @-}
sumGTree :: GTree -> Int
sumGTree (GTree x subtrees _) = x + sumGTreeList subtrees

{-@ reflect sumGTreeList @-}
{-@ sumGTreeList :: xs:[GTree] -> Int / [treeListSize xs, len xs]@-}
sumGTreeList :: [GTree] -> Int
sumGTreeList [] = 0
sumGTreeList (x:xs) = treeSize x `cast`
                      sumGTree x + sumGTreeList xs

I wonder if there is a way to achieve the same without using an additional field? For some reason, I have to make sure the exported interface remains the same (without the extra size field). I can achieve that by using pattern synonyms (in a separate file which isn't checked by LH since it's not supported according to 1334 )

[yiyunliu]

As an update, Coq's termination checker is able to tell that the following functions terminate:

treeSize :: GTree -> Int
treeSize (GTree _ hs) = 1 + f treeSize hs

f :: (a -> Int) -> [a] -> Int
f g [] = 0
f g (h:hs') = g h + f g hs'

It is obvious why f terminates. In order to show that treeSize terminates, Coq expands the higher order function f in treeSize to obtain the inlined version (per http://adam.chlipala.net/cpdt/html/InductiveTypes.html)

treeSize :: GTree -> Int
treeSize (GTree _ hs) =
  let f hs =
        case hs of
          [] -> 0
          (h:hs') -> treeSize h + f hs' in
  f hs + 1

Coq somehow knows that the treeSize recursive calls are invoked on subterms of GTree (with the knowledge of how the GTree data type is defined). I wonder if it's possible to do the same in LH's structural termination checker. I can look deeper into this in the future.

[ranjitjhala]

Very interesting, thanks for digging this up Yiyun!

On Thu, Jun 11, 2020 at 7:23 AM Yiyun Liu notifications@github.com wrote:

As an update, Coq's termination checker is able to tell that the following functions terminate:

treeSize :: GTree -> Int treeSize (GTree _ hs) = 1 + f treeSize hs f :: (a -> Int) -> [a] -> Int f g [] = 0 f g (h:hs') = g h + f g hs'

It is obvious why f terminates. In order to show that treeSize terminates, Coq expands the higher order function f in treeSize to obtain the inlined version (per http://adam.chlipala.net/cpdt/html/InductiveTypes.html https://urldefense.com/v3/__http://adam.chlipala.net/cpdt/html/InductiveTypes.html__;!!Mih3wA!QTlpr1ITqgz1CeTBzDuNJ83LfVUSjgcvs-S9bqhgif5-gtbGX3Gia2gf4LScSDwo$ )

treeSize :: GTree -> Int treeSize (GTree _ hs) = let f hs = case hs of [] -> 0 (h:hs') -> treeSize h + f hs' in f hs + 1

Coq somehow knows that the treeSize recursive calls are invoked on subterms of GTree (with the knowledge of how the GTree data type is defined). I wonder if it's possible to do the same in LH's structural termination checker. I can look deeper into this in the future.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1685*issuecomment-642691661__;Iw!!Mih3wA!QTlpr1ITqgz1CeTBzDuNJ83LfVUSjgcvs-S9bqhgif5-gtbGX3Gia2gf4AuGhJ5c$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OECZMBBQWCP5ENT3F3RWDSF3ANCNFSM4NYZFKFA__;!!Mih3wA!QTlpr1ITqgz1CeTBzDuNJ83LfVUSjgcvs-S9bqhgif5-gtbGX3Gia2gf4KOW8IlX$ .