Coding Induce statements and expressions in Haskell (and gofer)
================================================================

Prependix 0: The definitions of the data types and induce functions
-------------------------------------------------------------------

> infixr 0 &>
> infixr 0 &

> type Nat = Int

> nat_induce :: Nat -> ((Nat -> a) -> (a, (Nat -> a))) -> a
>
> nat_induce 0 bdy = fst (bdy btm)
>	where btm = error "Illegal application in base of nat_induce"
> nat_induce (n+1) bdy = (snd (bdy foo)) n
>	where foo x = if x > n
>		      then error "Illegal application in step of nat_induce"
>		      else nat_induce x bdy

Theorem:  If f is defined by
	f 0 = x
	f (n+1) = y
with x containing no call of f and y containing only calls of the
form f n , then (for fresh identifier g):
	f n = nat_induce n (\g-> (x, (\n-> y)))
Proof
	???
End Proof

> nat_induce' :: Nat -> b -> ((Nat -> b -> a) -> b -> (a, (Nat -> a))) -> a
>
> nat_induce' 0 b bdy = fst (bdy btm b)
>	where btm = error "Illegal application in base of nat_induce'"
> nat_induce' (n+1) b bdy = (snd (bdy foo b)) n
>	where foo x y = if x > n
>		        then error "Illegal application in step of nat_induce'"
>		        else nat_induce' x y bdy

> data Tree2 a = Empty2 | Node2 a (Tree2 a) (Tree2 a)

> tree2_induce :: Tree2 a -> 
>                 ((Tree2 a -> b) -> (b, ((a,Tree2 a,Tree2 a) -> b))) ->
>		  b
>
> tree2_induce Empty2 bdy = fst (bdy btm)
>       where btm = error "Illegal application in base of tree2_induce"
> tree2_induce (Node2 a left right) bdy = (snd (bdy foo)) (a, left, right)
>       where foo x = tree2_induce x bdy

> tree2_induce' :: Tree2 a ->
>		   c ->
>                  ((Tree2 a -> c -> b) ->
>		    c ->
>		    (b, ((a,Tree2 a,Tree2 a) -> b))) ->
>                  b
>
> tree2_induce' Empty2 c bdy = fst (bdy btm c)
>       where btm = error "Illegal application in base of tree2_induce'"
> tree2_induce' (Node2 a left right) c bdy = (snd (bdy foo c)) (a, left, right)
>       where foo x c = tree2_induce' x c bdy

> list_induce :: [a] -> (([a] -> b) -> (b, ((a, [a]) -> b))) -> b
> list_induce [] bdy = fst (bdy btm)
>	where btm = error "Illegal application in base of list_induce"
> list_induce (hd:tl) bdy = (snd (bdy foo)) (hd, tl)
>       where foo x = list_induce x bdy

> list_induce' :: [a] ->
>                  c ->
>                  (([a] -> c -> b) -> c -> (b, ((a,[a]) -> b))) ->
>                  b
>
> list_induce' [] c bdy = fst (bdy btm c)
>       where btm = error "Illegal application in base of list_induce'"
> list_induce' (hd:tl) c bdy = (snd (bdy foo c)) (hd, tl)
>       where foo x c = list_induce' x c bdy

> data Tree a = Empty | Node a [Tree a]
>
> tree_induce :: Tree a -> ((Tree a -> b) -> (b, ((a, [Tree a]) -> b))) -> b
> tree_induce Empty bdy = fst (bdy btm)
>       where btm = error "Illegal application in base of tree_induce"
> tree_induce (Node l ts) bdy = (snd (bdy foo)) (l, ts)
>       where foo x = tree_induce x bdy

> tree_induce' :: Tree a ->
>                  c ->
>                  ((Tree a -> c -> b) -> c -> (b, ((a,[Tree a]) -> b))) ->
>                  b
>
> tree_induce' Empty c bdy = fst (bdy btm c)
>       where btm = error "Illegal application in base of tree_induce'"
> tree_induce' (Node l ts) c bdy = (snd (bdy foo c)) (l, ts)
>       where foo x c = tree_induce' x c bdy


Prependix 1: The state transformer monad
----------------------------------------

State transformers

> type StateTransformer state result = state -> (state, result)

> skip :: StateTransformer s ()
> skip s = (s, ())


> (&>) :: (StateTransformer s r) -> (r -> (StateTransformer s r')) -> (StateTransformer s r')
>
> (t &> f) s  = let (s', r) = t s in f r s'

> (&) :: (StateTransformer s r) -> (StateTransformer s r') -> (StateTransformer s r')
>
> (t & u) s = let (s', _) = t s in u s'

> getState :: StateTransformer s s
> getState s = (s,s)

> run :: s -> StateTransformer s r -> r
> run s t = snd (t s)

Examples from Induce-Statements and Induce-Expression: Constructs for
---------------------------------------------------------------------
Inductive Programming, Theo Norvell, FST&TCS '93, LNCS 761.
-----------------------------------------------------------

Example: list reversal

induce reverse(l, acc := nil)
when nil : acc
when head.tail : reverse( tail, acc )
end reverse

Using list_induce' we can write

> rev l = list_induce' l [] (\reverse-> \acc->
>		(acc,
>		 \(head, tail)-> reverse tail (head:acc)))

Try
	? rev [1,2,3,4]

Example from figure 0(c).

induce f(n)
when 0 : sum := 0
when i' f(i)
	sum := A(i) + sum
	A(i) := sum

This is an imperative program, but using a state monad we can
mimic the imperative style with functions.
We use the state tranformer monad (See Prependix) which defines
	t &> k			Sequential composition with a value
	t & u			Vanila sequential composisiton
	run i t			Execute t from initial state i and
			        return the output.

The state consists of  n, A, sum  with the constraint that n is the
length of A.  A is represented by a list, since gofer doesn't have arrays.


> type ArraySum = (Int, [Int], Int)

> getSum (n, a, sum) = ((n, a, sum), sum)
> putSum sum (n, a, _) = ((n, a, sum), ())
> getN (n, a, sum) = ((n, a, sum), n)
> getA (n, a, sum) = ((n, a, sum), a)
> getAi i (n, a, sum) = ((n, a, sum), head(drop i a))
> putAi i z (n, a, sum) = ((n, take i a ++ [z] ++ drop (i+1) a, sum), ())

The program is represented as a function that takes a list argument
that represents the initial value of A and returns a list value representing
the final value of A.

> fig0c l = run (length l, l, -13) bar
> 	where bar = getN &> (\n->
>		    nat_induce n (\f->
> 			   (putSum 0,
> 			    (\i -> (f i &
> 				    getSum &> \sum->
> 				    getAi i &> \ai->
> 				    putSum (ai+sum) &
> 				    getSum &> \sum->
> 				    putAi i sum)))) &
> 		    getA )

Try
	? fig0c [1,2,3,4,5,6,7,8,9]

Example from Figure 2a

Towers of hanoi is similar.  This time the state is just the
collected output.

> put :: String -> StateTransformer String ()
> put message s = (s ++ message, ())

> hanoi n = nat_induce' n ("a", "b", "c") (\h-> \(source, target, other)->
>		( skip,
>		  (\i -> h i (source, other, target) &
>			 put "Move from " & put source &
>			 put " to " & put target & put "\n" &
>			 h i (other, target, source)) ) ) &
>	    getState

Try
	run "" (hanoi 7)


Example from figure 1(a)

Traversing a tree imperatively.  The function inOrder takes
a procedural argument and a tree and returns a procedure
that runs the procedure at every node of the tree.

> inOrder :: (a -> StateTransformer s ()) -> Tree2 a -> (StateTransformer s ())
> inOrder visit t =
>	tree2_induce t (\iot ->
>		(skip,
>                (\(label, left, right)->
>		   iot left &
>		   visit label &
>		   iot right)))

In this particular example the state has one (list valued) variable
and the procedure to be run at each node adds the label of the node
to the end of the list.

> flattener :: a -> StateTransformer [a] ()
> flattener label state = (state ++ [label], ())

> tree1 = Node2 1 Empty2 Empty2
> tree2 = Node2 2 tree1 tree1
> atree =  Node2 17 (Node2 9 (Node2 5 (Node2 3 tree2 tree1) tree2)
>			     (Node2 4 tree2 tree2))
>		    (Node2 8 (Node2 4 tree2 tree2) (Node2 4 tree2 tree2))

Try
	? run [] ((inOrder flattener atree) & getState)


Example from figure 2(b).

As in the previous example, we write a higher-order-procedure
that takes a procedure to be executed upon visitation and a tree
and returns a procedure that executes the first parameter at
each node of the second.

> preOrder :: (a -> StateTransformer s ()) -> Tree a -> StateTransformer s ()
> preOrder visit t =
>	tree_induce t (\traverse_tree->
>		(skip,
>		 \(label, children)->
>		   visit label &
>		   list_induce children (\traverse_tree_list->
>			(skip,
>			 \(child, siblings)->
>			   traverse_tree child &
>			   traverse_tree_list siblings) ) ) )

The state is one integer variable and the procedural parameter
adds the current label to the variable.

> summer :: Int -> StateTransformer Int ()
> summer i s = (i+s, ())

> exampleTree = Node 1 [Node 2 [], Node 3 [Node 4 [], Node 5 []]]

Try
	? run 0 ((preOrder summer exampleTree) & getState)

Example:  Ackermann/Peter function

> p 0 n = n+1
> p (m+1) 0 = p m 1
> p (m+1) (n+1) = p m (p (m+1) n)

Try
	p 3 3

Using nat_induce and nat_induce'

> ip' m n = nat_induce' m n (\p-> \n->
>               ( n+1,
>                 (\m-> nat_induce n (\q ->
>                           (p m 1,
>                            (\n-> p m (q n))
>                           ) ) )
>               ) )

Try
	? ip' 3 3

Ackermann/Peter using nat_induce alone.

> ip m n = foo n
>       where foo = nat_induce m (\p->
>                       ( (+1),
>                        (\m -> (\n -> nat_induce n (\q ->
>                                       ( p m 1,
>                                         (\n -> p m (q n))
>                                       ) ) ) )
>                       ) )

Try
	ip 3 3