properties.rkt

;; Die ersten drei Zeilen dieser Datei wurden von DrRacket eingefügt. Sie enthalten Metadaten
;; über die Sprachebene dieser Datei in einer Form, die DrRacket verarbeiten kann.
#reader(lib "DMdA-vanilla-reader.ss" "deinprogramm")((modname properties) (read-case-sensitive #f) (teachpacks ()) (deinprogramm-settings #(#f write repeating-decimal #f #t none explicit #f ())))
; Kapitel "Eigenschaften von Prozeduren"

; 3 Checks schlagen fehl.

; Kommutativität von +
(check-property
 (for-all ((a number)
           (b number))
    (= (+ a b)
       (+ b a))))

; Kommutativität von -
(check-property
 (for-all ((a number)
           (b number))
   (= (- a b)
      (- b a))))

(check-property
 (for-all ((a number)
           (b number)
           (c number))
    (= (+ a (+ b c))
       (+ (+ a b) c))))

(+ 2.6666666666666665 (+ 6.857142857142857 -6.857142857142857))
(+ (+ 2.6666666666666665 6.857142857142857) -6.857142857142857)

; Assoziativität von +
(check-property
 (for-all ((a rational)
           (b rational)
           (c rational))
    (= (+ a (+ b c))
       (+ (+ a b) c))))

(check-property
 (for-all ((a number)
           (b number)
           (c number))
    (expect-within (+ a (+ b c))
                   (+ (+ a b) c)
                   0.1)))

; Distributivität von + und *
(check-property
 (for-all ((a rational)
           (b rational)
           (c rational))
   (= (* a (+ b c))
      (+ (* a b) (* a c)))))

; neutrales Element
(check-property
  (for-all ((a rational))
    (= (+ a 0) a)))

; inverses Element
(check-property
 (for-all ((a rational))
   (= (+ a (- a)) 0)))

(check-property
 (for-all ((a rational))
   (= (+ (- a) a) 0)))

; Kommutativität von *
(check-property
 (for-all ((a rational)
           (b rational))
   (= (* a b)
      (* b a))))

; Kommutativität als abstrakte Eigenschaft, 1. Versuch
#|
(: commutativity ((rational rational -> rational) -> property))

(check-property (commutativity *))
(check-property (commutativity +))

(define commutativity
  (lambda (op)
    (for-all ((a rational)
              (b rational))
      (= (op a b)
         (op b a)))))
|#

; Kommutativität von and
(check-property
 (for-all ((a boolean)
           (b boolean))
    (boolean=? (and a b)
               (and b a))))

; Kommutativität als abstrakte Eigenschaft, 2. Versuch
(: commutativity ((%a %a -> %b) signature (%b %b -> boolean) -> property))

(check-property (commutativity * (signature rational) =))
(check-property (commutativity + (signature rational) =))

(check-property (commutativity (lambda (a b) (and a b))
                               (signature boolean) boolean=?))
(check-property (commutativity (lambda (a b) (or a b))
                               (signature boolean)
                               boolean=?))

(define commutativity
  (lambda (op sig =?)
    (for-all ((a sig)
              (b sig))
      (=? (op a b)
          (op b a)))))


; Assoziativität als abstrakte Eigenschaft
(: associativity ((%a %a -> %a) signature (%a %a -> boolean) -> property))

(check-property (associativity + (signature rational) =))
(check-property (associativity * (signature rational) =))
(check-property (associativity (lambda (a b) (and a b))
                               (signature boolean)
                               boolean=?))
(check-property (associativity (lambda (a b) (or a b))
                               (signature boolean)
                               boolean=?))

(define associativity
  (lambda (op sig =?)
    (for-all ((a sig)
              (b sig)
              (c sig))
      (=? (op a (op b c))
          (op (op a b) c)))))

; Assoziativität von and
(check-property
 (for-all ((a boolean)
           (b boolean)
           (c boolean))
    (boolean=? (and a (and b c))
               (and (and a b) c))))

; Distributivität von and und or: ÜBUNGSAUFGABE

(check-property
 (for-all ((a boolean)
           (b boolean)
           (c boolean))
   (boolean=? (and a (or b c))
              (or (and a b) (and a c)))))

(check-property
 (for-all ((a boolean)
           (b boolean)
           (c boolean))
   (boolean=? (or a (and b c))
              (and (or a b) (or a c)))))

; DeMorgan von and
(check-property
 (for-all ((a boolean)
           (b boolean))
   (boolean=? (not (and a b))
              (or (not a) (not b)))))

; DeMorgan von or
(check-property
 (for-all ((a boolean)
           (b boolean))
          (expect (not (or a b))
                  (and (not a) (not b)))))

; Reflexivität von =
(check-property
 (for-all ((a number))
   (= a a)))

; Symmetrie von =
(check-property
 (for-all ((a number)
           (b number))
   (==> (= a b)
        (= b a))))

; Transitivität von =
(check-property
 (for-all ((a number)
           (b number)
           (c number))
   (==> (and (= a b) (= b c))
        (= a c))))

(: concatenate ((list-of %a) (list-of %a) -> (list-of %a)))
(check-expect (concatenate (list 1 2 3) (list 4 5 6)) (list 1 2 3 4 5 6))
(check-expect (concatenate (list 1 2 3) empty) (list 1 2 3))
(check-expect (concatenate empty (list 1 2 3)) (list 1 2 3))
(check-expect (concatenate empty empty) empty)
(check-expect (concatenate (list 1 2 3) (list "vier" "fünf" "sechs")) (list 1 2 3 "vier" "fünf" "sechs"))

(check-property
 (associativity concatenate (signature (list-of number)) number-list=?))

(check-property
 (for-all ((lis (list-of number)))
   (number-list=? lis (concatenate empty lis))))

(check-property
 (for-all ((lis (list-of number)))
   (number-list=? lis (concatenate lis empty))))

(check-property
 (commutativity concatenate (signature (list-of number)) number-list=?))

(define concatenate
  (lambda (lis-1 lis-2)
    (cond
      ((empty? lis-1) lis-2)
      ((pair? lis-1) 
       (make-pair (first lis-1)
                  (concatenate (rest lis-1) lis-2))))))

; Zwei Listen aus Zahlen vergleichen
(: number-list=? ((list-of number) (list-of number) -> boolean))

(check-expect (number-list=? empty empty) #t)
(check-expect (number-list=? (list 1.0 2.0 3.0) (list 1.0 2.0 3.0)) #t)
(check-expect (number-list=? (list 1.0 2.0 3.0) (list 1.0 2.0)) #f)
(check-expect (number-list=? (list 1.0 2.0) (list 1.0 2.0 3.0)) #f)
(check-expect (number-list=? (list 1.0 2.0 3.0) (list 1.0 2.1 3.0)) #f)

; Reflexivität
(check-property
 (for-all ((lis (list-of number)))
   (number-list=? lis lis)))

; Symmetrie
(check-property
  (for-all ((lis-1 (list-of number))
            (lis-2 (list-of number)))
    (==> (number-list=? lis-1 lis-2)
         (number-list=? lis-2 lis-1))))

; Transitivität
(check-property
 (for-all ((lis-1 (list-of number))
           (lis-2 (list-of number))
           (lis-3 (list-of number)))
   (==> (and (number-list=? lis-1 lis-2)
             (number-list=? lis-2 lis-3))
        (number-list=? lis-1 lis-3))))

#;(define number-list=?
  (lambda (lis-1 lis-2)
    (cond
      ((empty? lis-1)
       ...)
      ((empty? lis-2)
       ... (number-list=? (rest lis-1) ...) ...))))

(define number-list=?
  (lambda (lis-1 lis-2)
    (cond
      ((empty? lis-1)
       (cond
         ((empty? lis-2) #t)
         ((pair? lis-2) #f)))
      ((pair? lis-1)
       (cond
         ((empty? lis-2) #f)
         ((pair? lis-2)
          (and (= (first lis-1) (first lis-2))
               (number-list=? (rest lis-1) (rest lis-2)))))))))


; Elemente einer Liste summieren
(: list-sum ((list-of number) -> number))
(check-expect (list-sum (make-pair 1 (make-pair 7 (make-pair 3 empty)))) 11)
(check-expect (list-sum empty) 0)

(check-property
 (for-all ((lis-1 (list-of number))
           (lis-2 (list-of number)))
   (expect-within (+ (list-sum lis-1) (list-sum lis-2))
                  (list-sum (concatenate lis-1 lis-2))
                  0.1)))
          
(check-property
 (for-all ((lis-1 (list-of rational))
           (lis-2 (list-of rational)))
   (expect (+ (list-sum lis-1) (list-sum lis-2))
           (list-sum (concatenate lis-1 lis-2)))))

(check-property
 (for-all ((lis-1 (list-of rational))
           (lis-2 (list-of rational)))
   (expect (list-sum (concatenate lis-1 lis-2))
           (list-sum (concatenate lis-2 lis-1)))))

(define list-sum
  (lambda (lis)
    (cond
      ((empty? lis) 0)
      ((pair? lis) 
       (+ (first lis)
          (list-sum (rest lis)))))))

; Liste umdrehen
(: invert ((list-of %a) -> (list-of %a)))

(check-property
 (for-all ((lis (list-of number)))
   (number-list=? lis (invert (invert lis)))))

(check-property
 (for-all ((lis (list-of string)))
   (expect lis (invert (invert lis)))))

(check-property
 (for-all ((lis-1 (list-of rational))
           (lis-2 (list-of rational)))
   (expect (invert (concatenate lis-1 lis-2))
           (concatenate (invert lis-2) (invert lis-1)))))

(define invert
  (lambda (lis)
    (invert-helper lis empty)))

(: invert-helper ((list-of %a) (list-of %a) -> (list-of %a)))
(define invert-helper
  (lambda (lis acc)
    (cond
      ((empty? lis) acc)
      ((pair? lis)
       (invert-helper (rest lis)
                      (make-pair (first lis) acc))))))

; Prozedur mit zwei Parametern staffeln
(: curry ((%a %b -> %c) -> (%a -> (%b -> %c))))

(check-expect (((curry +) 1) 2) 3)

(define curry
  (lambda (proc)
    (lambda (a)
      (lambda (b)
        (proc a b)))))


; Prozedur zu einer Prozedur mit zwei Parametern entstaffeln
(: uncurry ((%a -> (%b -> %c)) -> (%a %b -> %c)))

(check-expect ((uncurry (curry +)) 1 2) 3)

; funktioniert nicht:
;(check-property
; (for-all ((proc (string string -> string)))
;   (expect (curry (uncurry proc))
;           proc)))

(check-property
 (for-all ((a string)
           (b string)
           (proc (string string -> string)))
    (expect ((uncurry (curry proc)) a b)
            (proc a b))))

(define uncurry 
  (lambda (proc)
    (lambda (a b)
      ((proc a) b))))


(: f (natural -> rational))

(check-property
 (for-all ((k natural))
   (= (f k) (/ k (+ k 1)))))

(define f
  (lambda (n)
    (if (= n 0)
        0
        (+ (f (- n 1))
           (/ 1 (* n (+ n 1)))))))

; Fakultät berechnen

(: ! (natural -> natural))

(check-expect (! 0) 1)
(check-expect (! 3) 6)
(check-expect (! 5) 120)

(define !
  (lambda (n)
    (!-helper n 1)))

(define !-helper
  (lambda (n acc)
    (if (= n 0)
        acc
        (!-helper (- n 1) (* acc n)))))