List concatenation copies the spine of its first operand and shares the second:
(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
For finite first-operand length , fully producing the copied spine costs , independently of the second-operand length. With lazy evaluation, requesting only the first few result constructors can cost less; the bound concerns the complete concatenation spine, without forcing its element values or traversing the already existing second operand.
For input length , the successive list concatenations copy prefixes of lengths . Thus and . The direct implementation takes time for a fully produced nonempty reversal. The repeated copying, rather than the number of recursive calls alone, causes the quadratic cost.
Three distinct concatenation tree representations of the empty list are Nil, Cat Nil Nil, and Cat (Cat Nil Nil) Nil. For the singleton [x], use One x, Cat Nil (One x), and Cat (One x) Nil.
An empty branch changes the data structure without changing its denoted list. Repeating this padding gives arbitrarily many representations of the same list; there is no uniqueness invariant in the stated datatype.
One simple right-associated representation is
rep :: [a] -> CatList a
rep []     = Nil
rep (x:xs) = Cat (One x) (rep xs)
It constructs two data constructors per input element and one final Nil, so full construction takes time and produces constructors. Structural induction shows that its denotation is the original list.
Carry the eventual output tail as an accumulator, thereby avoiding repeated list concatenation:
abs :: CatList a -> [a]
abs t = flatten t []
  where
    flatten Nil       zs = zs
    flatten (One x)   zs = x : zs
    flatten (Cat l r) zs = flatten l (flatten r zs)
The invariant is flatten t zs = denotation t ++ zs. It is immediate for Nil and One; at Cat, applying the two induction hypotheses and associativity of list concatenation proves it. In particular, the empty accumulator gives the required abstraction.
Each concatenation tree constructor is processed once, and each One emits one result cons. Consequently full production takes time, where is the input constructor count, on every tree shape. This is a difference list calculation written with an explicit tail, an instance of linear flattening of a binary tree. The call stack can have depth for a badly skewed input; a linear time bound does not imply logarithmic stack space.
A concatenation tree may contain arbitrarily many Cat and Nil nodes while denoting an empty or singleton list. For example, repeatedly wrap One x as Cat Nil previous. The output length stays one while the input size grows without bound. An arbitrary leaf could hide another One, so a correct general conversion cannot disregard unexamined branches. Output length alone therefore cannot bound the work; input size must be included.
Reverse the children and recursively reverse each child:
rev :: CatList a -> CatList a
rev Nil       = Nil
rev (One x)   = One x
rev (Cat l r) = Cat (rev r) (rev l)
The proof uses and structural induction. The complete representation is processed and reconstructed in time. This is worst-case optimal for fully processing arbitrary explicit input representations with constructors; the datatype allows output information to be hidden at any leaf. Lazy evaluation can expose only an initial part of a result sooner, and this statement does not assert that every partial observation costs .
Compose the three functions:
reverse :: [a] -> [a]
reverse = abs . rev . rep
The representation built by rep has constructors. rev preserves that count, and abs traverses it once. Their three linear bounds add to total time, improving the direct quadratic reversal. The correctness equations for representation, reversal and abstraction compose to the required reversed list.

Articles by others on the same topic (0)

There are currently no matching articles.