Module 11 Using List Abstractions (Module 7)

List abstractions

See Figure 95:

; [X] N [N -> X] -> [List-of X]
; constructs a list by applying f to 0, 1, ..., (sub1 n)
; (build-list n f) == (list (f 0) ... (f (- n 1)))
(define (build-list n f) ...)

; [X] [X -> Boolean] [List-of X] -> [List-of X]
; produces a list from those items on lx for which p holds
(define (filter p lx) ...)

; [X] [List-of X] [X X -> Boolean] -> [List-of X]
; produces a version of lx that is sorted according to cmp
(define (sort lx cmp) ...)

; [X Y] [X -> Y] [List-of X] -> [List-of Y]
; constructs a list by applying f to each item on lx
; (map f (list x-1 ... x-n)) == (list (f x-1) ... (f x-n))
(define (map f lx) ...)

; [X] [X -> Boolean] [List-of X] -> Boolean
; determines whether p holds for every item on lx
; (andmap p (list x-1 ... x-n)) == (and (p x-1) ... (p x-n))
(define (andmap p lx) ...)

; [X] [X -> Boolean] [List-of X] -> Boolean
; determines whether p holds for at least one item on lx
; (ormap p (list x-1 ... x-n)) == (or (p x-1) ... (p x-n))
(define (ormap p lx) ...)

Foldr and Foldl

Folds a list of values into one value from the left or right:

> (foldr string-append "" (list "a" "b" "c"))
"abcd"
> (foldl string-append "" (list "a" "b" "c"))
"dcba"

Foldr does it with the first element first, so

(cons "a"
  (cons "b"
    (cons "c"
      (cons "d" '()))))

becomes

(string-append "a"
  (string-append "b"
    (string-append "c"
      (string-append "d" ""))))
"abcd"

And Foldl does the last element first, sop

(cons "a"
  (cons "b"
    (cons "c"
      (cons "d" '()))))

becomes

(string-append "d"
  (string-append "c"
    (string-append "b"
      (string-append "a" ""))))
"dcba"

where "" is the base case in both cases.

Build list

Perfect squares example:

; perfect-squares : Nat -> [List-of Nat]
; produce a list of the first k perfect squares

(check-expect (perfect-squares 0)
              '())

(check-expect (perfect-squares 1)
              (list 1))

(check-expect (perfect-squares 5)
              (list 1 4 9 16 25))

(define (perfect-squares k)
  (build-list k make-perfect-square))


;; make-perfect-square : Nat -> Nat
;; produce the square of 1 plus the input

(check-expect (make-perfect-square 0) 1)

(check-expect (make-perfect-square 1) 4)


(define (make-perfect-square n)
  (sqr (add1 n)))

Andmap and Ormap

ISL List Abstraction: andmap/ormap

  • andmap: does the predicate return true for all the elements of the list?
    • If you cannot come up with a counter-example, the answer is yes
  • ormap: does the predicate return true for any the elements of the list?