Terminating Tricky Traversals

Posted on January 29, 2020

Part 8 of a 8-part series on Breadth-First Traversals

Tags:Agda, Haskell

<a id="192">{-#</a> <a id="196">OPTIONS</a> <a id="204">--cubical</a> <a id="214">--sized-types</a> <a id="228">#-}</a>

<a id="233">module</a> <a id="240" href="">Post</a> <a id="245">where</a>

<a id="252">open</a> <a id="257">import</a> <a id="264" href="../code/terminating-tricky-traversals/Post.Prelude.html">../code/terminating-tricky-traversals/Post.Prelude</a>

Just a short one today. I’m going to look at a couple of algorithms for breadth-first traversals with complex termination proofs.

Breadth-First Graph Traversal

In a previous post I talked about breadth-first traversals over graphs, and the difficulties that cycles cause. Graphs are especially tricky to work with in a purely functional language, because so many of the basic algorithms are described in explicitly mututing terms (i.e. “mark off a node as you see it”), with no obvious immutable translation. The following is the last algoirthm I came up with:

bfs :: Ord a => (a -> [a]) -> a -> [[a]]
bfs g r = takeWhile (not.null) (map fst (fix (f r . push)))
  where
    push xs = ([],Set.empty) : [ ([],seen) | (_,seen) <- xs ]
    f x q@((l,s):qs)
      | Set.member x s = q
      | otherwise = (x:l, Set.insert x s) : foldr f qs (g x)

As difficult as it is to work with graphs in a pure functional language, it’s even more difficult to work in a total language, like Agda. Looking at the above function, there are several bits that we can see right off the bat won’t translate over easily. Let’s start with fix .

We shouldn’t expect to be able to write fix in Agda as-is. Just look at its Haskell implementation:

fix :: (a -> a) -> a
fix f = f (fix f)

It’s obviously non total!

(this is actually a non-memoizing version of fix , which is different from the usual one )

We can write a function like fix , though, using coinduction and sized types.

<a id="1890">record</a> <a id="Thunk"></a><a id="1897" href="#1897">Thunk</a> <a id="1903">(</a><a id="1904" href="#1904">A</a> <a id="1906">:</a> <a id="1908" href="../code/terminating-tricky-traversals/Agda.Builtin.Size.html#179">Size</a> <a id="1913">→</a> <a id="1915" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="1920" href="../code/terminating-tricky-traversals/Post.Prelude.html#221">a</a><a id="1921">)</a> <a id="1923">(</a><a id="1924" href="#1924">i</a> <a id="1926">:</a> <a id="1928" href="../code/terminating-tricky-traversals/Agda.Builtin.Size.html#179">Size</a><a id="1932">)</a> <a id="1934">:</a> <a id="1936" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="1941" href="#1920">a</a> <a id="1943">where</a>
  <a id="1951">coinductive</a>
  <a id="1965">field</a> <a id="Thunk.force"></a><a id="1971" href="#1971">force</a> <a id="1977">:</a> <a id="1979">∀</a> <a id="1981">{</a><a id="1982" href="#1982">j</a> <a id="1984">:</a> <a id="1986" href="../code/terminating-tricky-traversals/Agda.Builtin.Size.html#211">Size<</a> <a id="1992" href="#1924">i</a><a id="1993">}</a> <a id="1995">→</a> <a id="1997" href="#1904">A</a> <a id="1999" href="#1982">j</a>
<a id="2001">open</a> <a id="2006" href="#1897">Thunk</a> <a id="2012">public</a>

<a id="fix"></a><a id="2020" href="#2020">fix</a> <a id="2024">:</a> <a id="2026">(</a><a id="2027" href="#2027">A</a> <a id="2029">:</a> <a id="2031" href="../code/terminating-tricky-traversals/Agda.Builtin.Size.html#179">Size</a> <a id="2036">→</a> <a id="2038" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="2043" href="../code/terminating-tricky-traversals/Post.Prelude.html#221">a</a><a id="2044">)</a> <a id="2046">→</a> <a id="2048">(∀</a> <a id="2051">{</a><a id="2052" href="#2052">i</a><a id="2053">}</a> <a id="2055">→</a> <a id="2057" href="#1897">Thunk</a> <a id="2063" href="#2027">A</a> <a id="2065" href="#2052">i</a> <a id="2067">→</a> <a id="2069" href="#2027">A</a> <a id="2071" href="#2052">i</a><a id="2072">)</a> <a id="2074">→</a> <a id="2076">∀</a> <a id="2078">{</a><a id="2079" href="#2079">j</a><a id="2080">}</a> <a id="2082">→</a> <a id="2084" href="#2027">A</a> <a id="2086" href="#2079">j</a>
<a id="2088" href="#2020">fix</a> <a id="2092" href="#2092">A</a> <a id="2094" href="#2094">f</a> <a id="2096">=</a> <a id="2098" href="#2094">f</a> <a id="2100">λ</a> <a id="2102">where</a> <a id="2108">.</a><a id="2109" href="#1971">force</a> <a id="2115">→</a> <a id="2117" href="#2020">fix</a> <a id="2121" href="#2092">A</a> <a id="2123" href="#2094">f</a>

Coinductive types are the dual to inductive types. Totality-wise, a coinductive type must be “productive”; i.e. a coinductive list can be infinitely long, but it must be provably able to evaluate to a constructor (cons or nil) in finite time.

Sized types also help us out here: they’re quite subtle, and a little finicky to use occasionally, but they are invaluable when it comes to proving termination or productivity of complex (especially higher-order) functions. The canonical example is mapping over the following tree type:

<a id="2670">module</a> <a id="NonTerminating"></a><a id="2677" href="#2677">NonTerminating</a> <a id="2692">where</a>
  <a id="2700">data</a> <a id="NonTerminating.Tree"></a><a id="2705" href="#2705">Tree</a> <a id="2710">(</a><a id="2711" href="#2711">A</a> <a id="2713">:</a> <a id="2715" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="2720" href="../code/terminating-tricky-traversals/Post.Prelude.html#221">a</a><a id="2721">)</a> <a id="2723">:</a> <a id="2725" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="2730" href="#2720">a</a> <a id="2732">where</a>
    <a id="NonTerminating.Tree._&_"></a><a id="2742" href="#2742">_&_</a> <a id="2746">:</a> <a id="2748" href="#2711">A</a> <a id="2750">→</a> <a id="2752" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="2757">(</a><a id="2758" href="#2705">Tree</a> <a id="2763" href="#2711">A</a><a id="2764">)</a> <a id="2766">→</a> <a id="2768" href="#2705">Tree</a> <a id="2773" href="#2711">A</a>

  <a id="2778">{-#</a> <a id="2782">TERMINATING</a> <a id="2794">#-}</a>
  <a id="NonTerminating.mapTree"></a><a id="2800" href="#2800">mapTree</a> <a id="2808">:</a> <a id="2810">(</a><a id="2811" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="2813">→</a> <a id="2815" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a><a id="2816">)</a> <a id="2818">→</a> <a id="2820" href="#2705">Tree</a> <a id="2825" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="2827">→</a> <a id="2829" href="#2705">Tree</a> <a id="2834" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a>
  <a id="2838" href="#2800">mapTree</a> <a id="2846" href="#2846">f</a> <a id="2848">(</a><a id="2849" href="#2849">x</a> <a id="2851" href="#2742">&</a> <a id="2853" href="#2853">xs</a><a id="2855">)</a> <a id="2857">=</a> <a id="2859" href="#2846">f</a> <a id="2861" href="#2849">x</a> <a id="2863" href="#2742">&</a> <a id="2865" href="../code/terminating-tricky-traversals/Post.Prelude.html#678">map</a> <a id="2869">(</a><a id="2870" href="#2800">mapTree</a> <a id="2878" href="#2846">f</a><a id="2879">)</a> <a id="2881" href="#2853">xs</a>

The compiler can’t tell that the recursive call in the mapTree function will only be called on subnodes of the argument: it can’t tell that it’s structurally recursive, in other words. Annoyingly, we can fix the problem by inlining map .

<a id="3141">mutual</a>
    <a id="NonTerminating.mapTree′"></a><a id="3152" href="#3152">mapTree′</a> <a id="3161">:</a> <a id="3163">(</a><a id="3164" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="3166">→</a> <a id="3168" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a><a id="3169">)</a> <a id="3171">→</a> <a id="3173" href="#2705">Tree</a> <a id="3178" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="3180">→</a> <a id="3182" href="#2705">Tree</a> <a id="3187" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a>
    <a id="3193" href="#3152">mapTree′</a> <a id="3202" href="#3202">f</a> <a id="3204">(</a><a id="3205" href="#3205">x</a> <a id="3207" href="#2742">&</a> <a id="3209" href="#3209">xs</a><a id="3211">)</a> <a id="3213">=</a> <a id="3215" href="#3202">f</a> <a id="3217" href="#3205">x</a> <a id="3219" href="#2742">&</a> <a id="3221" href="#3241">mapForest</a> <a id="3231" href="#3202">f</a> <a id="3233" href="#3209">xs</a>

    <a id="NonTerminating.mapForest"></a><a id="3241" href="#3241">mapForest</a> <a id="3251">:</a> <a id="3253">(</a><a id="3254" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="3256">→</a> <a id="3258" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a><a id="3259">)</a> <a id="3261">→</a> <a id="3263" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="3268">(</a><a id="3269" href="#2705">Tree</a> <a id="3274" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a><a id="3275">)</a> <a id="3277">→</a> <a id="3279" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="3284">(</a><a id="3285" href="#2705">Tree</a> <a id="3290" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a><a id="3291">)</a>
    <a id="3297" href="#3241">mapForest</a> <a id="3307" href="#3307">f</a> <a id="3309" href="../code/terminating-tricky-traversals/Post.Prelude.html#542">[]</a> <a id="3312">=</a> <a id="3314" href="../code/terminating-tricky-traversals/Post.Prelude.html#542">[]</a>
    <a id="3321" href="#3241">mapForest</a> <a id="3331" href="#3331">f</a> <a id="3333">(</a><a id="3334" href="#3334">x</a> <a id="3336" href="../code/terminating-tricky-traversals/Post.Prelude.html#556">∷</a> <a id="3338" href="#3338">xs</a><a id="3340">)</a> <a id="3342">=</a> <a id="3344" href="#3152">mapTree′</a> <a id="3353" href="#3331">f</a> <a id="3355" href="#3334">x</a> <a id="3357" href="../code/terminating-tricky-traversals/Post.Prelude.html#556">∷</a> <a id="3359" href="#3241">mapForest</a> <a id="3369" href="#3331">f</a> <a id="3371" href="#3338">xs</a>

The other solution is to give the tree a size parameter. This way, all submodes of a given tree will have smaller sizes, which will give the compiler a finite descending chin condition it can use to prove termination.

<a id="3606">data</a> <a id="Tree"></a><a id="3611" href="#3611">Tree</a> <a id="3616">(</a><a id="3617" href="#3617">A</a> <a id="3619">:</a> <a id="3621" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="3626" href="../code/terminating-tricky-traversals/Post.Prelude.html#221">a</a><a id="3627">)</a> <a id="3629">(</a><a id="3630" href="#3630">i</a> <a id="3632">:</a> <a id="3634" href="../code/terminating-tricky-traversals/Agda.Builtin.Size.html#179">Size</a><a id="3638">)</a> <a id="3640">:</a> <a id="3642" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="3647" href="#3626">a</a> <a id="3649">where</a>
  <a id="Tree._&_"></a><a id="3657" href="#3657">_&_</a> <a id="3661">:</a> <a id="3663" href="#3617">A</a> <a id="3665">→</a> <a id="3667">∀</a> <a id="3669">{</a><a id="3670" href="#3670">j</a> <a id="3672">:</a> <a id="3674" href="../code/terminating-tricky-traversals/Agda.Builtin.Size.html#211">Size<</a> <a id="3680" href="#3630">i</a><a id="3681">}</a> <a id="3683">→</a> <a id="3685" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="3690">(</a><a id="3691" href="#3611">Tree</a> <a id="3696" href="#3617">A</a> <a id="3698" href="#3670">j</a><a id="3699">)</a> <a id="3701">→</a> <a id="3703" href="#3611">Tree</a> <a id="3708" href="#3617">A</a> <a id="3710" href="#3630">i</a>

<a id="mapTree"></a><a id="3713" href="#3713">mapTree</a> <a id="3721">:</a> <a id="3723">(</a><a id="3724" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="3726">→</a> <a id="3728" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a><a id="3729">)</a> <a id="3731">→</a> <a id="3733" href="#3611">Tree</a> <a id="3738" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="3740" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a> <a id="3742">→</a> <a id="3744" href="#3611">Tree</a> <a id="3749" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a> <a id="3751" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a>
<a id="3753" href="#3713">mapTree</a> <a id="3761" href="#3761">f</a> <a id="3763">(</a><a id="3764" href="#3764">x</a> <a id="3766" href="#3657">&</a> <a id="3768" href="#3768">xs</a><a id="3770">)</a> <a id="3772">=</a> <a id="3774" href="#3761">f</a> <a id="3776" href="#3764">x</a> <a id="3778" href="#3657">&</a> <a id="3780" href="../code/terminating-tricky-traversals/Post.Prelude.html#678">map</a> <a id="3784">(</a><a id="3785" href="#3713">mapTree</a> <a id="3793" href="#3761">f</a><a id="3794">)</a> <a id="3796" href="#3768">xs</a>

So how do we use this stuff in our graph traversal? Well first we’ll need a coinductive Stream type:

<a id="3914">record</a> <a id="Stream"></a><a id="3921" href="#3921">Stream</a> <a id="3928">(</a><a id="3929" href="#3929">A</a> <a id="3931">:</a> <a id="3933" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="3938" href="../code/terminating-tricky-traversals/Post.Prelude.html#221">a</a><a id="3939">)</a> <a id="3941">(</a><a id="3942" href="#3942">i</a> <a id="3944">:</a> <a id="3946" href="../code/terminating-tricky-traversals/Agda.Builtin.Size.html#179">Size</a><a id="3950">)</a> <a id="3952">:</a> <a id="3954" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="3959" href="#3938">a</a> <a id="3961">where</a>
  <a id="3969">coinductive</a>
  <a id="3983">field</a>
    <a id="Stream.head"></a><a id="3993" href="#3993">head</a> <a id="3998">:</a> <a id="4000" href="#3929">A</a>
    <a id="Stream.tail"></a><a id="4006" href="#4006">tail</a> <a id="4011">:</a> <a id="4013">∀</a> <a id="4015">{</a><a id="4016" href="#4016">j</a> <a id="4018">:</a> <a id="4020" href="../code/terminating-tricky-traversals/Agda.Builtin.Size.html#211">Size<</a> <a id="4026" href="#3942">i</a><a id="4027">}</a> <a id="4029">→</a> <a id="4031" href="#3921">Stream</a> <a id="4038" href="#3929">A</a> <a id="4040" href="#4016">j</a>
<a id="4042">open</a> <a id="4047" href="#3921">Stream</a> <a id="4054">public</a>

<a id="smap"></a><a id="4062" href="#4062">smap</a> <a id="4067">:</a> <a id="4069">(</a><a id="4070" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="4072">→</a> <a id="4074" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a><a id="4075">)</a> <a id="4077">→</a> <a id="4079" href="#3921">Stream</a> <a id="4086" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="4088" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a> <a id="4090">→</a> <a id="4092" href="#3921">Stream</a> <a id="4099" href="../code/terminating-tricky-traversals/Post.Prelude.html#250">B</a> <a id="4101" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a>
<a id="4103" href="#4062">smap</a> <a id="4108" href="#4108">f</a> <a id="4110" href="#4110">xs</a> <a id="4113">.</a><a id="4114" href="#3993">head</a> <a id="4119">=</a> <a id="4121" href="#4108">f</a> <a id="4123">(</a><a id="4124" href="#4110">xs</a> <a id="4127">.</a><a id="4128" href="#3993">head</a><a id="4132">)</a>
<a id="4134" href="#4062">smap</a> <a id="4139" href="#4139">f</a> <a id="4141" href="#4141">xs</a> <a id="4144">.</a><a id="4145" href="#4006">tail</a> <a id="4150">=</a> <a id="4152" href="#4062">smap</a> <a id="4157" href="#4139">f</a> <a id="4159">(</a><a id="4160" href="#4141">xs</a> <a id="4163">.</a><a id="4164" href="#4006">tail</a><a id="4168">)</a>

And then we can use it to write our breadth-first traversal.

<a id="bfs"></a><a id="4245" href="#4245">bfs</a> <a id="4249">:</a> <a id="4251">⦃</a> <a id="4253" href="#4253">_</a> <a id="4255">:</a> <a id="4257" href="../code/terminating-tricky-traversals/Post.Prelude.html#2916">IsDiscrete</a> <a id="4268" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="4270">⦄</a> <a id="4272">→</a> <a id="4274">(</a><a id="4275" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="4277">→</a> <a id="4279" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="4284" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a><a id="4285">)</a> <a id="4287">→</a> <a id="4289" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="4291">→</a> <a id="4293" href="#3921">Stream</a> <a id="4300">(</a><a id="4301" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="4306" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a><a id="4307">)</a> <a id="4309" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a>
<a id="4311" href="#4245">bfs</a> <a id="4315" href="#4315">g</a> <a id="4317" href="#4317">r</a> <a id="4319">=</a> <a id="4321" href="#4062">smap</a> <a id="4326" href="../code/terminating-tricky-traversals/Agda.Builtin.Sigma.html#225">fst</a> <a id="4330">(</a><a id="4331" href="#2020">fix</a> <a id="4335">(</a><a id="4336" href="#3921">Stream</a> <a id="4343">_)</a> <a id="4346">(</a><a id="4347" href="#4490">f</a> <a id="4349" href="#4317">r</a> <a id="4351" href="../code/terminating-tricky-traversals/Post.Prelude.html#434">∘</a> <a id="4353" href="#4370">push</a><a id="4357">))</a>
  <a id="4362">where</a>
  <a id="4370" href="#4370">push</a> <a id="4375">:</a> <a id="4377" href="#1897">Thunk</a> <a id="4383">(</a><a id="4384" href="#3921">Stream</a> <a id="4391">_)</a> <a id="4394" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a> <a id="4396">→</a> <a id="4398" href="#3921">Stream</a> <a id="4405">_</a> <a id="4407" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a>
  <a id="4411" href="#4370">push</a> <a id="4416" href="#4416">xs</a> <a id="4419">.</a><a id="4420" href="#3993">head</a> <a id="4425">=</a> <a id="4427">(</a><a id="4428" href="../code/terminating-tricky-traversals/Post.Prelude.html#542">[]</a> <a id="4431" href="../code/terminating-tricky-traversals/Agda.Builtin.Sigma.html#209">,</a> <a id="4433" href="../code/terminating-tricky-traversals/Post.Prelude.html#542">[]</a><a id="4435">)</a>
  <a id="4439" href="#4370">push</a> <a id="4444" href="#4444">xs</a> <a id="4447">.</a><a id="4448" href="#4006">tail</a> <a id="4453">=</a> <a id="4455" href="#4062">smap</a> <a id="4460">(</a><a id="4461" href="../code/terminating-tricky-traversals/Agda.Builtin.Sigma.html#209">_,_</a> <a id="4465" href="../code/terminating-tricky-traversals/Post.Prelude.html#542">[]</a> <a id="4468" href="../code/terminating-tricky-traversals/Post.Prelude.html#434">∘</a> <a id="4470" href="../code/terminating-tricky-traversals/Agda.Builtin.Sigma.html#237">snd</a><a id="4473">)</a> <a id="4475">(</a><a id="4476" href="#4444">xs</a> <a id="4479">.</a><a id="4480" href="#1971">force</a><a id="4485">)</a>

  <a id="4490" href="#4490">f</a> <a id="4492">:</a> <a id="4494">_</a> <a id="4496">→</a> <a id="4498" href="#3921">Stream</a> <a id="4505">_</a> <a id="4507" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a> <a id="4509">→</a> <a id="4511" href="#3921">Stream</a> <a id="4518">_</a> <a id="4520" href="../code/terminating-tricky-traversals/Post.Prelude.html#276">i</a>
  <a id="4524" href="#4490">f</a> <a id="4526" href="#4526">x</a> <a id="4528" href="#4528">qs</a> <a id="4531">with</a> <a id="4536">(</a><a id="4537" href="#4526">x</a> <a id="4539" href="../code/terminating-tricky-traversals/Post.Prelude.html#3012">∈?</a> <a id="4542" href="#4528">qs</a> <a id="4545">.</a><a id="4546" href="#3993">head</a> <a id="4551">.</a><a id="4552" href="../code/terminating-tricky-traversals/Agda.Builtin.Sigma.html#237">snd</a><a id="4555">)</a> <a id="4557">.</a><a id="4558" href="../code/terminating-tricky-traversals/Post.Prelude.html#1059">does</a>
  <a id="4565">...</a> <a id="4569">|</a> <a id="4571" href="../code/terminating-tricky-traversals/Agda.Builtin.Bool.html#160">true</a> <a id="4576">=</a> <a id="4578">qs</a>
  <a id="4583">...</a> <a id="4587">|</a> <a id="4589" href="../code/terminating-tricky-traversals/Agda.Builtin.Bool.html#154">false</a> <a id="4595">=</a> <a id="4597">λ</a> <a id="4599">where</a> <a id="4605">.</a><a id="4606" href="#3993">head</a> <a id="4611">→</a> <a id="4613">(</a><a id="4614">x</a> <a id="4616" href="../code/terminating-tricky-traversals/Post.Prelude.html#556">∷</a> <a id="4618">qs</a> <a id="4621">.</a><a id="4622" href="#3993">head</a> <a id="4627">.</a><a id="4628" href="../code/terminating-tricky-traversals/Agda.Builtin.Sigma.html#225">fst</a> <a id="4632" href="../code/terminating-tricky-traversals/Agda.Builtin.Sigma.html#209">,</a> <a id="4634">x</a> <a id="4636" href="../code/terminating-tricky-traversals/Post.Prelude.html#556">∷</a> <a id="4638">qs</a> <a id="4641">.</a><a id="4642" href="#3993">head</a> <a id="4647">.</a><a id="4648" href="../code/terminating-tricky-traversals/Agda.Builtin.Sigma.html#237">snd</a><a id="4651">)</a>
                        <a id="4677">.</a><a id="4678" href="#4006">tail</a> <a id="4683">→</a> <a id="4685" href="../code/terminating-tricky-traversals/Post.Prelude.html#583">foldr</a> <a id="4691" href="#4490">f</a> <a id="4693">(</a><a id="4694">qs</a> <a id="4697">.</a><a id="4698" href="#4006">tail</a><a id="4702">)</a> <a id="4704">(</a><a id="4705" href="#4315">g</a> <a id="4707">x</a><a id="4708">)</a>

How do we convert this to a list of lists? Well, for this condition we would actually need to prove that there are only finitely many elements in the graph. We could actually use Noetherian finiteness for this: though I have a working implementation, I’m still figuring out how to clean this up, so I will leave it for another post.

Traversing a Braun Tree

A recent paper (Nipkow and Sewell) provided Coq proofs for some algorithms on Braun trees, which prompted me to take a look at them again. This time, I came up with an interesting linear-time toList function, which relies on the following peculiar type:

newtype Q2 a
  = Q2
  { unQ2 :: (Q2 a -> Q2 a) -> (Q2 a -> Q2 a) -> a
  }

Even after coming up with the type myself, I still can’t really make heads nor tails of it. If I squint, it starts to look like some bizarre church-encoded binary number (but I have to really squint). It certainly seems related to corecursive queues.

Anyway, we can use the type to write the following lovely toList function on a Braun tree.

toList :: Tree a -> [a]
toList t = unQ2 (f t b) id id
  where
    f (Node x l r) xs = Q2 (\ls rs -> x : unQ2 xs (ls . f l) (rs . f r))
    f Leaf         xs = Q2 (\_  _  -> [])

    b = Q2 (\ls rs -> unQ2 (ls (rs b)) id id)

So can we convert it to Agda?

Not really! As it turns out, this function is even more difficult to implement than one might expect. We can’t even write the Q2 type in Agda without getting in trouble.

<a id="6242">{-#</a> <a id="6246">NO_POSITIVITY_CHECK</a> <a id="6266">#-}</a>
<a id="6270">record</a> <a id="Q2"></a><a id="6277" href="#6277">Q2</a> <a id="6280">(</a><a id="6281" href="#6281">A</a> <a id="6283">:</a> <a id="6285" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="6290" href="../code/terminating-tricky-traversals/Post.Prelude.html#221">a</a><a id="6291">)</a> <a id="6293">:</a> <a id="6295" href="../code/terminating-tricky-traversals/Cubical.Core.Primitives.html#957">Type</a> <a id="6300" href="#6290">a</a> <a id="6302">where</a>
  <a id="6310">inductive</a>
  <a id="6322">field</a>
    <a id="Q2.q2"></a><a id="6332" href="#6332">q2</a> <a id="6335">:</a> <a id="6337">(</a><a id="6338" href="#6277">Q2</a> <a id="6341" href="#6281">A</a> <a id="6343">→</a> <a id="6345" href="#6277">Q2</a> <a id="6348" href="#6281">A</a><a id="6349">)</a> <a id="6351">→</a>
         <a id="6362">(</a><a id="6363" href="#6277">Q2</a> <a id="6366" href="#6281">A</a> <a id="6368">→</a> <a id="6370" href="#6277">Q2</a> <a id="6373" href="#6281">A</a><a id="6374">)</a> <a id="6376">→</a>
         <a id="6387" href="#6281">A</a>
<a id="6389">open</a> <a id="6394" href="#6277">Q2</a>

Q2 isn’t strictly positive, unfortunately.

<a id="6456">{-#</a> <a id="6460">TERMINATING</a> <a id="6472">#-}</a>
<a id="toList"></a><a id="6476" href="#6476">toList</a> <a id="6483">:</a> <a id="6485" href="../code/terminating-tricky-traversals/Post.Prelude.html#4077">Braun</a> <a id="6491" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="6493">→</a> <a id="6495" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="6500" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a>
<a id="6502" href="#6476">toList</a> <a id="6509" href="#6509">t</a> <a id="6511">=</a> <a id="6513" href="#6587">f</a> <a id="6515" href="#6509">t</a> <a id="6517" href="#6539">n</a> <a id="6519">.</a><a id="6520" href="#6332">q2</a> <a id="6523" href="../code/terminating-tricky-traversals/Post.Prelude.html#3105">id</a> <a id="6526" href="../code/terminating-tricky-traversals/Post.Prelude.html#3105">id</a>
  <a id="6531">where</a>
  <a id="6539" href="#6539">n</a> <a id="6541">:</a> <a id="6543" href="#6277">Q2</a> <a id="6546" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a>
  <a id="6550" href="#6539">n</a> <a id="6552">.</a><a id="6553" href="#6332">q2</a> <a id="6556" href="#6556">ls</a> <a id="6559" href="#6559">rs</a> <a id="6562">=</a> <a id="6564" href="#6556">ls</a> <a id="6567">(</a><a id="6568" href="#6559">rs</a> <a id="6571" href="#6539">n</a><a id="6572">)</a> <a id="6574">.</a><a id="6575" href="#6332">q2</a> <a id="6578" href="../code/terminating-tricky-traversals/Post.Prelude.html#3105">id</a> <a id="6581" href="../code/terminating-tricky-traversals/Post.Prelude.html#3105">id</a>

  <a id="6587" href="#6587">f</a> <a id="6589">:</a> <a id="6591" href="../code/terminating-tricky-traversals/Post.Prelude.html#4077">Braun</a> <a id="6597" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a> <a id="6599">→</a> <a id="6601" href="#6277">Q2</a> <a id="6604">(</a><a id="6605" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="6610" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a><a id="6611">)</a> <a id="6613">→</a> <a id="6615" href="#6277">Q2</a> <a id="6618">(</a><a id="6619" href="../code/terminating-tricky-traversals/Post.Prelude.html#507">List</a> <a id="6624" href="../code/terminating-tricky-traversals/Post.Prelude.html#237">A</a><a id="6625">)</a>
  <a id="6629" href="#6587">f</a> <a id="6631" href="../code/terminating-tricky-traversals/Post.Prelude.html#4113">leaf</a>         <a id="6644" href="#6644">xs</a> <a id="6647">.</a><a id="6648" href="#6332">q2</a> <a id="6651" href="#6651">ls</a> <a id="6654" href="#6654">rs</a> <a id="6657">=</a> <a id="6659" href="../code/terminating-tricky-traversals/Post.Prelude.html#542">[]</a>
  <a id="6664" href="#6587">f</a> <a id="6666">(</a><a id="6667" href="../code/terminating-tricky-traversals/Post.Prelude.html#4130">node</a> <a id="6672" href="#6672">x</a> <a id="6674" href="#6674">l</a> <a id="6676" href="#6676">r</a><a id="6677">)</a> <a id="6679" href="#6679">xs</a> <a id="6682">.</a><a id="6683" href="#6332">q2</a> <a id="6686" href="#6686">ls</a> <a id="6689" href="#6689">rs</a> <a id="6692">=</a> <a id="6694" href="#6672">x</a> <a id="6696" href="../code/terminating-tricky-traversals/Post.Prelude.html#556">∷</a> <a id="6698" href="#6679">xs</a> <a id="6701">.</a><a id="6702" href="#6332">q2</a> <a id="6705">(</a><a id="6706" href="#6686">ls</a> <a id="6709" href="../code/terminating-tricky-traversals/Post.Prelude.html#434">∘</a> <a id="6711" href="#6587">f</a> <a id="6713" href="#6674">l</a><a id="6714">)</a> <a id="6716">(</a><a id="6717" href="#6689">rs</a> <a id="6720" href="../code/terminating-tricky-traversals/Post.Prelude.html#434">∘</a> <a id="6722" href="#6587">f</a> <a id="6724" href="#6676">r</a><a id="6725">)</a>

Apparently this problem of strict positivity for breadth-first traversals has come up before: Berger, Matthes, and Setzer () ;.

References

Berger, Ulrich, Ralph Matthes, and Anton Setzer. 2019. “Martin Hofmann’s Case for Non-Strictly Positive Data Types.” In 24th international conference on types for proofs and programs (TYPES 2018) , ed by. Peter Dybjer, José Espírito Santo, and Luís Pinto, 130:22. Leibniz international proceedings in informatics (LIPIcs). Dagstuhl, Germany: Schloss DagstuhlLeibniz-Zentrum fuer Informatik. doi: 10.4230/LIPIcs.TYPES.2018.1 . http://drops.dagstuhl.de/opus/volltexte/2019/11405 .

Hofmann, Martin. 1993. “Non Strictly Positive Datatypes in System F.” https://www.seas.upenn.edu/~sweirich/types/archive/1993/msg00027.html .

Nipkow, Tobias, and Thomas Sewell. 2020. “Proof pearl: Braun trees.” In Certified programs and proofs, CPP 2020 , ed by. J. Blanchette and C. Hritcu, –. ACM. http://www21.in.tum.de/~nipkow/pubs/cpp20.html .

Okasaki, Chris. 1997. “Three Algorithms on Braun Trees.” Journal of Functional Programming 7 (6) (November): 661–666. doi: 10.1017/S0956796897002876 . https://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall/three-algorithms-on-braun-trees.pdf .

Smith, Leon P. 2009. “Lloyd Allison’s Corecursive Queues: Why Continuations Matter.” The Monad.Reader 14 (14) (July): 28. https://meldingmonads.files.wordpress.com/2009/06/corecqueues.pdf .