Search code examples
haskellinduction

Structual induction in Haskell

Can anyone give me an example of Structural induction in Haskell? I can't find nothing online about it, I have been given a hypothesis but having trouble formulating the base case.

The hypothesis is: For all lists xs of type [a] and all x of type a it is:

toLast (x:xs) = xs |++| [x]

With |++| being my own version of concatenating two lists and toLast being a function where the header of a list goes to the end of the list. I have tried to figure this out myself and got toLast [] = [] |++| [] but I am unsure if this is correct.

Solution

  • Can anyone give me an example of Structural induction in Haskell?

    Structural induction always requires two steps:

    1. Consider the base cases
    2. Consider the generic case by assuming that a function body exists for a list xs, and use that assumption to construct a definition for the next step (x:xs). This is the so called inductive step.

    Let's use the idea of structural induction to define your |++| function, which is a better example in my opinion.

    |++| takes in two lists and outputs a list that is the concatenation of the first with the second, the type signature is therefore:

    (|++|) :: [a] -> [a] -> [a]

    The second list input never changes, so we say that the first list is the parameter of recursion. The base case is therefore when the first list is empty:

    (|++|) [] ys = ys

    Now, lets consider the case when the first argument to |++| is not the empty list but is xs. The inductive step is to assume that our function (|++|) xs ys works (because it is shown to be valid in the base case) and use that assumption to define the general case when the first input to |++| is (x:xs). Putting these together, so far, we have:

    (|++|) []     ys = ys -- base case
(|++|) (x:xs) ys = let assumedAlreadyConcatenatedList = ((|++|) xs ys) in *something...* assumedAlreadyConcatenatedList -- half-done general case

    Having assumed that ((|++|) xs ys) works correctly, we just need to define what to do with x and then we are done. How do we concatenate x to a list of already concatenated items? We use cons:

    (|++|) []     ys = ys -- base case
(|++|) (x:xs) ys = let assumedAlreadyConcatenatedList = ((|++|) xs ys) in x : assumedAlreadyConcatenatedList -- completed general case.

    Hopefully it's clear that we would always need a base case to back our assumption in the inductive step.