Hello everyone I want to ask if the following a definition of structural induction or not

init xs = take ( length xs - 1) xs

0 init :: [ a ] -> [ a ]

1  init ( x :[]) = []

2  init ( x : z : xs ) = x : init ( z : xs ) 

also Can someone give me an example of structural induction in Haskell?

CodePudding user response：

First, you need to define what init does, so you have something to compare the implementation take (length xs - 1) xs against. Such a specification might be

 init [x] = []
 init (x:xs) = x : init xs

(The fact that this is basically a valid Haskell definition itself is one of the strengths of Haskell.)

To prove that init xs = take (length xs - 1) xs is correct, you need to prove that the definition satisfies the specification, using equational reasoning.

The base cases (every singleton list) is simple:

init [x] == take (length [x] - 1) [x]  -- definition of init
         == take (1 - 1) [x]  -- definition of length
         == take 0 [x]  -- arithmetic
         == []  -- using the definition of take

Having proven that init is correct for lists of length 1, the inductive hypothesis is that init xs is correct for any list xs of length k > 1. The inductive step is to prove that init is correct for a list (x:xs) of length k 1 (i.e., any list created by adding one more element to a list of length k).

init (x:xs) == take (length (x:xs) - 1) (x:xs)  -- definition of init
            == take (1   length xs - 1) (x:xs)  -- definition of length
            == take (length xs) (x:xs)  -- arithmetic
            == x : take (length xs - 1) xs -- definition of take
            == x : init xs -- definition of init