liquidhaskell-0.7.0.0: docs/slides/BOS14/lhs/06_Inductive.lhs
Abstract Refinements {#induction}
=================================
Decoupling Invariants & Code
----------------------------
<br>
Abstract refinements decouple invariants from code
<br>
<div class="fragment">
**Next:** Precise Specifications for HOFs
<div class="hidden">
\begin{code}
module Loop where
import Prelude hiding ((!!), foldr, length, (++))
import Data.Set hiding (insert, foldr,size,filter, append)
-- import Measures
import Language.Haskell.Liquid.Prelude
{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--short-names" @-}
{-@ measure size :: (L a) -> Int
size (N) = 0
size (C x xs) = 1 + (size xs) @-}
{-@ measure elems :: L a -> (Set a)
elems (N) = (Set_empty 0)
elems (C x xs) = (Set_cup (Set_sng x) (elems xs))
@-}
{-@ type UnElems Xs Ys = {v:_ | elems v = Set_cup (elems Xs) (elems Ys)} @-}
size :: L a -> Int
add :: Int -> Int -> Int
loop :: Int -> Int -> α -> (Int -> α -> α) -> α
ifoldr :: (L a -> a -> b -> b) -> b -> L a -> b
\end{code}
</div>
<!-- BEGIN CUT
Induction
=========
Example: A Higher Order `loop`
-------------------------------
<br>
<br>
\begin{code}
loop lo hi base f = go lo base
where
go i acc
| i < hi = go (i+1) (f i acc)
| otherwise = acc
\end{code}
Iteration Dependence
--------------------
We can use `loop` to write
<br>
\begin{spec}
{-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
add n m = loop' 0 m n (\_ i -> i + 1)
\end{spec}
<br>
<div class="fragment">
**Problem** But cannot prove `add n m :: {v:_ | v = n + m}`
- As property only holds after *last* loop iteration...
- ... cannot instantiate `α` with `{v:Int | v = n + m}`
</div>
Iteration Dependence
--------------------
We used `loop` to write
<br>
\begin{spec}
{-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
add n m = loop 0 m n (\_ i -> i + 1)
\end{spec}
<br>
**Problem**
Need invariant relating *iteration* `i` with *accumulator* `acc`
Iteration Dependence
--------------------
We used `loop` to write
\begin{spec} <br>
{-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
add n m = loop 0 m n (\_ i -> i + 1)
\end{spec}
<br>
**Solution**
- Abstract Refinement `p :: Int -> a -> Prop`
- `(p i acc)` relates *iteration* `i` with *accumulator* `acc`
Induction in `loop` (by hand)
-----------------------------
\begin{code}
loop lo hi base f = go lo base
where
go i acc
| i < hi = go (i+1) (f i acc)
| otherwise = acc
\end{code}
<br>
<div class="fragment">
<div align="center">
------------ --- ----------------------------
**Assume** : `out = loop lo hi base f`
**Prove** : `(p hi out)`
------------ --- ----------------------------
</div>
</div>
Induction in `loop` (by hand)
-----------------------------
\begin{spec} <br>
loop lo hi base f = go lo base
where
go i acc
| i < hi = go (i+1) (f i acc)
| otherwise = acc
\end{spec}
<br>
**Base Case:** Initial accumulator `base` satisfies invariant
`(p lo base)`
Induction in `loop` (by hand)
-----------------------------
\begin{spec} <br>
loop lo hi base f = go lo base
where
go i acc
| i < hi = go (i+1) (f i acc)
| otherwise = acc
\end{spec}
<br>
**Inductive Step:** `f` *preserves* invariant at `i`
`(p i acc) => (p (i+1) (f i acc))`
Induction in `loop` (by hand)
-----------------------------
\begin{spec} <br>
loop lo hi base f = go lo base
where
go i acc
| i < hi = go (i+1) (f i acc)
| otherwise = acc
\end{spec}
<br>
**"By Induction"** `out` satisfies invariant at `hi`
`(p hi out)`
Induction in `loop` (by type)
-----------------------------
Induction is an **abstract refinement type** for `loop`
<br>
\begin{code}
{-@ loop :: forall a <p :: Int -> a -> Prop>.
lo:Int
-> hi:{Int | lo <= hi}
-> base:a<p lo>
-> f:(i:Int -> a<p i> -> a<p (i+1)>)
-> a<p hi> @-}
\end{code}
<br>
Induction in `loop` (by type)
-----------------------------
`p` is the *index dependent* invariant!
\begin{spec}<br>
p :: Int -> a -> Prop -- invt
base :: a<p lo> -- base
f :: i:Int -> a<p i> -> a<p(i+1)> -- step
out :: a<p hi> -- goal
\end{spec}
Using Induction
---------------
\begin{code}
{-@ add :: n:Nat -> m:Nat -> {v:Nat| v=m+n} @-}
add n m = loop 0 m n (\_ z -> z + 1)
\end{code}
<br>
**Verified** by *instantiating* the abstract refinement of `loop`
`p := \i acc -> acc = i + n`
Generalizes To Structures
-------------------------
Same idea applies for induction over *structures* ...
<br>
<br>
[DEMO 02_AbstractRefinements.hs #2](../hs/02_AbstractRefinements.hs)
END CUT -->
Structural Induction
====================
Example: Lists
--------------
<br>
\begin{code}
data L a = N
| C a (L a)
\end{code}
<br>
<div class="fragment">
Lets write a generic loop over lists ...
</div>
Example: `foldr`
----------------
<br>
<br>
\begin{code}
foldr :: (α -> β -> β) -> β -> L α -> β
foldr f acc N = acc
foldr f acc (C x xs) = f x (foldr f acc xs)
\end{code}
Problem
-------
Recall our *failed attempt* to write `append` with `foldr`
<br>
\begin{spec}
{-@ app :: xs:_ -> ys:_ -> UnElems xs ys @-}
app xs ys = foldr C ys xs
\end{spec}
<br>
<div class="fragment">
- Property holds after *last* iteration
- Cannot instantiate `α` with `UnElems xs ys`
</div>
Problem
-------
Recall our *failed attempt* to write `append` with `foldr`
<br>
\begin{spec}
{-@ app :: xs:_ -> ys:_ -> UnElems xs ys @-}
app xs ys = foldr C ys xs
\end{spec}
<br>
Need to **relate** each *iteration* with *accumulator* `acc`
Solution: Inductive `foldr`
---------------------------
<br>
<br>
<div class="fragment">
Lets brace ourselves for the type...
</div>
Solution: Inductive `foldr`
---------------------------
\begin{code}
{-@ ifoldr ::
forall a b <p :: L a -> b -> Prop>.
(xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>)
-> b<p N>
-> ys:L a
-> b<p ys> @-}
ifoldr f b N = b
ifoldr f b (C x xs) = f xs x (ifoldr f b xs)
\end{code}
<br>
<div class="fragment">
Lets step through the type...
</div>
`ifoldr`: Abstract Refinement
-----------------------------
\begin{spec} <div/>
p :: L a -> b -> Prop
step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>
base :: b<p N>
ys :: L a
out :: b<p ys>
\end{spec}
<br>
`(p xs b)` relates `b` with **folded** `xs`
`p :: L a -> b -> Prop`
`ifoldr`: Base Case
-------------------
\begin{spec} <div/>
p :: L a -> b -> Prop
step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>
base :: b<p N>
ys :: L a
out :: b<p ys>
\end{spec}
<br>
`base` is related to **empty** list `N`
`base :: b<p N>`
`ifoldr`: Ind. Step
-------------------
\begin{spec} <div/>
p :: L a -> b -> Prop
step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>
base :: b<p N>
ys :: L a
out :: b<p ys>
\end{spec}
<br>
`step` **extends** relation from `xs` to `C x xs`
`step :: xs:_ -> x:_ -> b<p xs> -> b<p (C x xs)>`
`ifoldr`: Output
----------------
\begin{spec} <div/>
p :: L a -> b -> Prop
step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>
base :: b<p N>
ys :: L a
out :: b<p ys>
\end{spec}
<br>
Hence, relation holds between `out` and **entire input** list `ys`
`out :: b<p ys>`
Using `ifoldr`: Size
-------------------
We can now verify
<br>
\begin{code}
{-@ size :: xs:_ -> {v:Int| v = size xs} @-}
size = ifoldr (\_ _ n -> n + 1) 0
\end{code}
<br>
<div class="fragment">
by *automatically instantiating* `p` with
`\xs acc -> acc = size xs`
</div>
Using `foldr`: Append
---------------------
We can now verify
<br>
\begin{code}
{-@ (++) :: xs:_ -> ys:_ -> UnElems xs ys @-}
xs ++ ys = ifoldr (\_ -> C) ys xs
\end{code}
<br>
<br>
<div class="fragment">
By *automatically* instantiating `p` with
`\xs acc -> elems acc = Set_cup (elems xs) (elems ys)`
</div>
More Examples
-------------
Induction over *structures* from `GHC.List`
<br>
+ `length`
+ `append`
+ `filter`
+ ...
<br>
[DEMO 02_AbstractRefinements.hs #2](../hs/02_AbstractRefinements.hs)
Recap
-----
<br>
Abstract refinements *decouple* **invariant** from **iteration**
<br>
<div class="fragment">**Precise** specs for higher-order functions.</div>
<br>
<div class="fragment">**Automatic** checking and instantiation by SMT.</div>
Recap
-----
1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Strengthened Constructors
4. Abstract: Refinements over Type Signatures
+ <div class="fragment">**Functions**</div>
+ <div class="fragment">**Recursive Data** <a href="08_Recursive.lhs.slides.html" target="_blank">[continue]</a></div>
5. <div class="fragment">[Evaluation](11_Evaluation.lhs.slides.html)</div>