DP: Insertion Sort

foldr ins [] xs
where
ins x [] = [x]
ins x (z:zs) = min x z : ins (max x z) zs

toterm [] = []
toterm (x:xs) = I x p n f : toterm xs

sem [] = []
sem (I x p n f : ts) = ins x (sem ts)
sem (C x p n f : ts) = x : sem ts

I x p n f
=> C x p' n' f' if n = Nil
=> I x p' n' f' if n = I _ _ _ _
=> C (min x y) p' n' f' if n = C y _ _ _

C x p n f
=> C x p' n' f' if p = Nil
=> I (max x y) p' n' f' if p = I y _ _ _
=> C x p' n' f' if p = C _ _ _ _

foldr ins [] xs = sem $ (map (=>) ) ^ n $ toterm $ xs

foldr ins [] [10,1,5,2]
= ins 10 (ins 1 (ins 5 (ins 2 [])))
= ins 10 (ins 1 (ins 5 (cons 2 [])))
= ins 10 (ins 1 (cons 2 (ins 5 [])))
= ins 10 (cons 1 (ins 2 (cons 5 [])))
= cons 1 (ins 10 (cons 2 (ins 5 [])))
= cons 1 (cons 2 (ins 10 (cons 5 [])))
= cons 1 (cons 2 (cons 5 (ins 10 [])))
= cons 1 (cons 2 (cons 5 (cons 10 [])))

* 방향
- 병렬성이나 Lazy Evaluation이 연관된 증명이 매우 어려워 보임.
- 우선 Equational Equality를 보이는데 중점.
- 병렬성은 map 함수로 설명
- pure functional context는 lazy evaluation으로 설명