Problem 1: Boolean Blasters

Consider the following top-level Racket definitions over booleans that give implementations of the standard boolean operations not, and, and or:

(define my-not
  (lambda (b)
    (if b #f #t)))

(define my-and
  (lambda (b1 b2)
    (if b1 b2 #f)))

(define my-or
  (lambda (b1 b2)
    (if b1 #t b2)))

Prove the following claims of program equivalence about these definitions:

For any derivations that you write, you may evaluate a function call directly to the branch of the selected conditional in its body.

Problem 2: The Corporate World

The CEO of a company has asked their in-house programming team to build a new payment system. Obviously, this payment system is written in Racket. The code for the system is given below.

#lang racket

(require racket/match)

;;; An employee in this payment system is a list of four elements:
;;; + The employee's position, a string,
;;; + The employee's name, a string
;;; + The employee's time at the company in years, a nonnegative integer, and
;;; + Whether the employee wears shoes in the office, a boolean.

;;; (senior? employee) returns #t iff the employee is senior.
(define senior?
  (lambda (employee)
    (match employee
      [(list "Accountant" _ yrs _) (>= yrs 5)]
      [(list "Programmer" _ yrs _) (>= yrs 5)]
      [(list "Manager" _ yrs _)    (>= yrs 8)]
      [(list "CEO" _ yrs _)        (>= yrs 1)])))

(define acct-base 2)
(define prog-base 5)

;;; (pay employee) returns the pay of the given employee
;;; in tens of thousands of dollars, an integer.
(define pay
  (lambda (employee)
    (match employee
      [(list "Accountant" _ _ _)
       (if (senior? employee) (+ 2 acct-base) acct-base)]
      [(list "Programmer" _ _ shoes?)
       (if shoes? (* prog-base 8) (* prog-base 4))]
      [(list "Manager" name yrs shoes?)
       (cond [(equal? name "Tony")     -1]
             [(< yrs 2)                prog-base]
             [(not (senior? employee)) (* prog-base 2)]
             [else                     (* prog-base 10)])]
      [(list "CEO" _ _ _) 1])))

• The CEO has announced as part of his new budget plans that he will be receiving the lowest paycheck at the company. Write down a formal proposition exemplifies this property in terms of the code above. In your definition, appeal to the “formal” definition of an employee as a list of four elements as described above.

• Does the property that you described above hold of the code? If so, prove it. If not, provide a counterexample and show that the counterexample violates the property.

• The CEO also announced a new policy to try to encourage junior (non-senior) programmers to stay as programmers and not become managers. The following formal proposition captures this idea:

  Claim: (pay '("Programmer" n t s)) ≥ (pay '("Manager" n t s))) for any employee with name n, time spent t, and shoe status s whenever (not (senior? '("Programmer" n t s))) and (not (senior? '("Manager" n t s)).

  Prove that this property holds of the code above.

• While the property above holds, it is still undesirable for junior programmers to stay as programmers! In sentence or two, describe why this is the case.

Problem 3: Zero Is The Hero

1. Implement a Racket function dropzeroes that takes a list l of numbers as input and returns l but with all 0s. For example (dropzeroes '(1 3 0 1 0 2)) --> '(1 3 1 2). Make sure to test your code in Dr. Racket and add your code to this write-up using a code block.

2. Prove the following property of dropzeroes:

   Claim (Idempotency of dropzeroes): (dropzeroes (dropzeroes l)) ≡ (dropzeroes l).

   You may take the shortcut of evaluating a recursive function call directly to the branch that it selects in a single step.

   (Hint: be precise with your program derivations and every step you make! In particular, make sure that every step is justified and you consider all possibilities of evaluation.)