liquidhaskell-0.8.10.7: docs/slides/plpv14/lhs/10_Termination.lhs.markdown
Termination {#termination}
==========================
<div class="hidden">
<pre><span class=hs-linenum> 7: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>Termination</span> <span class='hs-keyword'>where</span>
<span class=hs-linenum> 8: </span>
<span class=hs-linenum> 9: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Prelude</span> <span class='hs-varid'>hiding</span> <span class='hs-layout'>(</span><span class='hs-varid'>gcd</span><span class='hs-layout'>,</span> <span class='hs-varid'>mod</span><span class='hs-layout'>,</span> <span class='hs-varid'>map</span><span class='hs-layout'>)</span>
<span class=hs-linenum>10: </span><span class='hs-definition'>fib</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span>
<span class=hs-linenum>11: </span><span class='hs-definition'>gcd</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span>
<span class=hs-linenum>12: </span><span class='hs-keyword'>infixr</span> <span class='hs-varop'>`C`</span>
<span class=hs-linenum>13: </span>
<span class=hs-linenum>14: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>C</span> <span class='hs-varid'>a</span> <span class='hs-layout'>(</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span>
<span class=hs-linenum>15: </span>
<span class=hs-linenum>16: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>invariant</span> <span class='hs-keyword'>{v:</span> <span class='hs-layout'>(</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-keyword'>| 0 <= (llen v)}</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>17: </span>
<span class=hs-linenum>18: </span><span class='hs-definition'>mod</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span>
<span class=hs-linenum>19: </span><a class=annot href="#"><span class=annottext>x1:{VV : (Int) | (VV >= 0)}
-> x2:{VV : (Int) | (VV >= 0) && (0 < VV) && (VV < x1)}
-> {VV : (Int) | (VV >= 0) && (VV < x2)}</span><span class='hs-definition'>mod</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (0 < VV) && (VV < a)}</span><span class='hs-varid'>b</span></a> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == a) && (x3 >= 0)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a> <a class=annot href="#"><span class=annottext>x1:{x10 : (Int) | (x10 > 0) && (0 < x10) && (x10 < a)}
-> x2:{x10 : (Int) | (x10 > 0) && (0 < x10) && (x10 < a)}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 > x2))}</span><span class='hs-varop'>></span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{VV : (Int) | (VV >= 0)}
-> x2:{VV : (Int) | (VV >= 0) && (0 < VV) && (VV < x1)}
-> {VV : (Int) | (VV >= 0) && (VV < x2)}</span><span class='hs-varid'>mod</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == a) && (x3 >= 0)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a>
<span class=hs-linenum>20: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == a) && (x3 >= 0)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a> <a class=annot href="#"><span class=annottext>x1:{x12 : (Int) | (x12 > 0) && (0 < x12) && (x12 < a) && (x12 <= b)}
-> x2:{x12 : (Int) | (x12 > 0) && (0 < x12) && (x12 < a) && (x12 <= b)}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == a) && (x3 >= 0)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a>
<span class=hs-linenum>21: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == a) && (x3 >= 0)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a> <a class=annot href="#"><span class=annottext>x1:{x12 : (Int) | (x12 == b) && (x12 > 0) && (0 < x12) && (x12 < a)}
-> x2:{x12 : (Int) | (x12 == b) && (x12 > 0) && (0 < x12) && (x12 < a)}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 == x2))}</span><span class='hs-varop'>==</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == b) && (x5 >= 0) && (0 < x5) && (x5 < a)}</span><span class='hs-varid'>b</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:(Int#) -> {x2 : (Int) | (x2 == (x1 : int))}</span><span class='hs-num'>0</span></a>
<span class=hs-linenum>22: </span>
<span class=hs-linenum>23: </span><span class='hs-definition'>merge</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Ord</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=></span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span>
</pre>
</div>
Dependent != Refinement
-----------------------
<div class="fragment">**Dependent Types**</div>
+ <div class="fragment">*Arbitrary terms* appear inside types</div>
+ <div class="fragment">Termination ensures well-defined</div>
<br>
<div class="fragment">**Refinement Types**</div>
+ <div class="fragment">*Restricted refinements* appear in types</div>
+ <div class="fragment">Termination *not* required ...</div>
+ <div class="fragment">... except, alas, with *lazy* evaluation!</div>
Refinements & Termination
----------------------------
<div class="fragment">
Fortunately, we can ensure termination *using refinements*
</div>
Main Idea
---------
Recursive calls must be on *smaller* inputs
<br>
+ [Turing](http://classes.soe.ucsc.edu/cmps210/Winter11/Papers/turing-1936.pdf)
+ [Sized Types](http://dl.acm.org/citation.cfm?id=240882)
Recur On *Smaller* `Nat`
------------------------
<div class="fragment">
**To ensure termination of**
<div/>
<pre><span class=hs-linenum>69: </span><span class='hs-definition'>foo</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>T</span>
<span class=hs-linenum>70: </span><span class='hs-definition'>foo</span> <span class='hs-varid'>x</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>body</span>
</pre>
</div>
<br>
<div class="fragment">
**Check `body` Under Assumption**
`foo :: {v:Nat | v < x} -> T`
<br>
*i.e.* require recursive calls have inputs *smaller* than `x`
</div>
Ex: Recur On *Smaller* `Nat`
----------------------------
<pre><span class=hs-linenum>93: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>fib</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>94: </span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0)}</span><span class='hs-definition'>fib</span></a> <span class='hs-num'>0</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:(Int#) -> {x2 : (Int) | (x2 == (x1 : int))}</span><span class='hs-num'>1</span></a>
<span class=hs-linenum>95: </span><span class='hs-definition'>fib</span> <span class='hs-num'>1</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:(Int#) -> {x2 : (Int) | (x2 == (x1 : int))}</span><span class='hs-num'>1</span></a>
<span class=hs-linenum>96: </span><span class='hs-definition'>fib</span> <span class='hs-varid'>n</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>fib</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 >= 0)}</span><span class='hs-varid'>n</span></a><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>fib</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 >= 0)}</span><span class='hs-varid'>n</span></a><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2 : int))}</span><span class='hs-num'>2</span></a><span class='hs-layout'>)</span>
</pre>
<br>
<div class="fragment">
Terminates, as both `n-1` and `n-2` are `< n`
</div>
<br>
<div class="fragment">
<a href="http://goto.ucsd.edu:8090/index.html#?demo=GCD.hs" target="_blank">Demo:</a>What if we drop the `fib 1` case?
</div>
Refinements Are Essential!
--------------------------
<pre><span class=hs-linenum>115: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>gcd</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{b:</span><span class='hs-conid'>Nat</span> <span class='hs-keyword'>| b < a}</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>116: </span><a class=annot href="#"><span class=annottext>x1:{VV : (Int) | (VV >= 0)}
-> {VV : (Int) | (VV >= 0) && (VV < x1)} -> (Int)</span><span class='hs-definition'>gcd</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>a</span></a> <span class='hs-num'>0</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == a) && (x3 >= 0)}</span><span class='hs-varid'>a</span></a>
<span class=hs-linenum>117: </span><span class='hs-definition'>gcd</span> <span class='hs-varid'>a</span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{VV : (Int) | (VV >= 0)}
-> {VV : (Int) | (VV >= 0) && (VV < x1)} -> (Int)</span><span class='hs-varid'>gcd</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 >= 0) && (x3 < a)}</span><span class='hs-varid'>b</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == a) && (x3 >= 0)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:{x9 : (Int) | (x9 >= 0)}
-> x2:{x7 : (Int) | (x7 >= 0) && (0 < x7) && (x7 < x1)}
-> {x3 : (Int) | (x3 >= 0) && (x3 < x2)}</span><span class='hs-varop'>`mod`</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 >= 0) && (x3 < a)}</span><span class='hs-varid'>b</span></a><span class='hs-layout'>)</span>
</pre>
<br>
<div class="fragment">
Need refinements to prove `(a mod b) < b` at *recursive* call!
</div>
<br>
<div class="fragment">
<pre><span class=hs-linenum>130: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>mod</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span>
<span class=hs-linenum>131: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-conop'>:</span><span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>|(0 < v && v < a)}</span>
<span class=hs-linenum>132: </span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>| v < b}</span> <span class='hs-keyword'>@-}</span>
</pre>
</div>
Recur On *Smaller* Inputs
-------------------------
What of input types other than `Nat` ?
<div/>
<pre><span class=hs-linenum>142: </span><span class='hs-definition'>foo</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>S</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>T</span>
<span class=hs-linenum>143: </span><span class='hs-definition'>foo</span> <span class='hs-varid'>x</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>body</span>
</pre>
<br>
<div class="fragment">
**Reduce** to `Nat` case...
</div>
<br>
Recur On *Smaller* Inputs
-------------------------
What of input types other than `Nat` ?
<div/>
<pre><span class=hs-linenum>160: </span><span class='hs-definition'>foo</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>S</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>T</span>
<span class=hs-linenum>161: </span><span class='hs-definition'>foo</span> <span class='hs-varid'>x</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>body</span>
</pre>
<br>
Specify a **default measure** `mS :: S -> Int`
<br>
<div class="fragment">
**Check `body` Under Assumption**
`foo :: {v:s | 0 <= (mS v) < (mS x)} -> T`
</div>
Ex: Recur on *smaller* `List`
-----------------------------
<pre><span class=hs-linenum>181: </span><a class=annot href="#"><span class=annottext>forall a b. (a -> b) -> (L a) -> (L b)</span><span class='hs-definition'>map</span></a> <a class=annot href="#"><span class=annottext>a -> b</span><span class='hs-varid'>f</span></a> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a. {x2 : (L a) | ((llen x2) == 0)}</span><span class='hs-conid'>N</span></a>
<span class=hs-linenum>182: </span><span class='hs-definition'>map</span> <span class='hs-varid'>f</span> <span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>a -> b</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}</span><span class='hs-varop'>`C`</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>forall a b. (a -> b) -> (L a) -> (L b)</span><span class='hs-varid'>map</span></a> <a class=annot href="#"><span class=annottext>a -> b</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>{x3 : (L a) | (x3 == xs) && (0 <= (llen x3))}</span><span class='hs-varid'>xs</span></a><span class='hs-layout'>)</span>
</pre>
<br>
Terminates using **default** measure `llen`
<div class="fragment">
<pre><span class=hs-linenum>191: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>data</span> <span class='hs-conid'>L</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>llen</span><span class='hs-keyglyph'>]</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>N</span>
<span class=hs-linenum>192: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>C</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span><span class='hs-keyglyph'>::</span><span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>xs</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>193: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>measure</span> <span class='hs-varid'>llen</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span>
<span class=hs-linenum>194: </span> <span class='hs-varid'>llen</span> <span class='hs-layout'>(</span><span class='hs-conid'>N</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span>
<span class=hs-linenum>195: </span> <span class='hs-varid'>llen</span> <span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>1</span> <span class='hs-varop'>+</span> <span class='hs-layout'>(</span><span class='hs-varid'>llen</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span>
</pre>
</div>
Recur On *Smaller* Inputs
-------------------------
What of *smallness* spread across inputs?
<br>
<pre><span class=hs-linenum>208: </span><a class=annot href="#"><span class=annottext>forall a. (Ord a) => (L a) -> (L a) -> (L a)</span><span class='hs-definition'>merge</span></a> <a class=annot href="#"><span class=annottext>(L a)</span><span class='hs-varid'>xs</span></a><span class='hs-keyglyph'>@</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>xs'</span><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>(L a)</span><span class='hs-varid'>ys</span></a><span class='hs-keyglyph'>@</span><span class='hs-layout'>(</span><span class='hs-varid'>y</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>ys'</span><span class='hs-layout'>)</span>
<span class=hs-linenum>209: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>x1:a -> x2:a -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>forall a. (Ord a) => (L a) -> (L a) -> (L a)</span><span class='hs-varid'>merge</span></a> <a class=annot href="#"><span class=annottext>{x3 : (L a) | (x3 == xs') && (0 <= (llen x3))}</span><span class='hs-varid'>xs'</span></a> <a class=annot href="#"><span class=annottext>{x5 : (L a) | (x5 == ys) && (x5 == (Termination.C y ys')) && ((llen x5) == (1 + (llen ys'))) && (0 <= (llen x5))}</span><span class='hs-varid'>ys</span></a>
<span class=hs-linenum>210: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a> <a class=annot href="#"><span class=annottext>a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>forall a. (Ord a) => (L a) -> (L a) -> (L a)</span><span class='hs-varid'>merge</span></a> <a class=annot href="#"><span class=annottext>{x5 : (L a) | (x5 == xs) && (x5 == (Termination.C x xs')) && ((llen x5) == (1 + (llen xs'))) && (0 <= (llen x5))}</span><span class='hs-varid'>xs</span></a> <a class=annot href="#"><span class=annottext>{x3 : (L a) | (x3 == ys') && (0 <= (llen x3))}</span><span class='hs-varid'>ys'</span></a>
</pre>
<br>
<div class="fragment">
Neither input decreases, but their *sum* does.
</div>
Recur On *Smaller* Inputs
-------------------------
Neither input decreases, but their *sum* does.
<br>
<pre><span class=hs-linenum>227: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>merge</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Ord</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=></span> <span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>ys</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>_</span>
<span class=hs-linenum>228: </span> <span class='hs-varop'>/</span> <span class='hs-keyglyph'>[</span><span class='hs-layout'>(</span><span class='hs-varid'>llen</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-varop'>+</span> <span class='hs-layout'>(</span><span class='hs-varid'>llen</span> <span class='hs-varid'>ys</span><span class='hs-layout'>)</span><span class='hs-keyglyph'>]</span> <span class='hs-keyword'>@-}</span>
</pre>
<br>
<div class="fragment">
Synthesize *ghost* parameter equal to `[...]`
</div>
<br>
<div class="fragment">
Reduces to single-parameter-decrease case.
</div>
Important Extensions
--------------------
- <div class="fragment">Mutual recursion</div>
- <div class="fragment">Lexicographic ordering...</div>
Recap
-----
Main idea: Recursive calls on *smaller inputs*
<br>
- <div class="fragment">Use refinements to *check* smaller</div>
- <div class="fragment">Use refinements to *establish* smaller</div>
A Curious Circularity
---------------------
<div class="fragment">Refinements require termination ...</div>
<br>
<div class="fragment">... Termination requires refinements!</div>
<br>
<div class="fragment"> (Meta-theory is tricky, but all ends well.)</div>
Recap
-----
1. **Refinements:** Types + Predicates
2. **Subtyping:** SMT Implication
3. **Measures:** Strengthened Constructors
4. **Abstract Refinements:* Decouple Invariants
5. **Lazy Evaluation:** Requires Termination
6. **Termination:** Via Refinements!
7. <div class="fragment">**Evaluation** </div>