Folie 118:

Comprehension unnesting is equivalence-preserving:


 fold programs for comprehensions:
 (1)

    [ G | G <- [ e | X1 <- R ]bag ]sum
 =
    fold (z^sum, (x), [ e | X1 <- R ]bag)
    with
        (x) (c,G) = c (+)^sum [ G | ]sum
 =
    fold (0, (x), [ e | X1 <- R ]bag)
    with
        (x) (c,G) = c + G
 =
    fold (0, (x), fold (z^bag, (.), R))
    with
        (x) (c,G)  = c + G
        (.) (c,X1) = c (+)^bag [ e | ]bag
 =
    fold (0, (x), fold ({}, (.), R))
    with
        (x) (c,G)  = c + G
        (.) (c,X1) = c |_|+ { e }


    R = { r_1, r_2, r_3, ..., r_n }

      = { r_1 } |_|+ { r_2 } |_|+ { r_3 } |_|+ ... |_|+ { r_n } |_|+ {}

  fold ({}, (.), R) =

        {  e  } |_|+ {  e  } |_|+ {  e  } |_|+ ... |_|+ {  e  } |_|+ {}

  fold(0, (x), fold ({}, (.), R)) =

           e     +      e     +      e     +   ...    +     e     +   0



 (2)

    [ e | X1 <- R ]sum
 =
    fold (z^sum, (x), R)
    with
        (x) (c,X1) = c (+)^sum [ e | ]sum
 =
    fold (0, (x), R)
    with
        (x) (c,X1) = c + e


    R = { r_1, r_2, r_3, ..., r_n }

      = { r_1 } |_|+ { r_2 } |_|+ { r_3 } |_|+ ... |_|+ { r_n } |_|+ {}

  fold (0, (x), R) =

           e     +      e     +      e     +   ...    +     e     +   0