14 Assignment 14: Pie

You might need to check the documentation of Pie occasionally.

Assignment

Introduction to types

1. Define intriguing-word so that intriguing-word is an Atom.

   (claim intriguing-word Atom)

2. Define lucky-num so that lucky-num is a Nat.

   (claim lucky-num Nat)

3. Define to-go-order so that pickup-order is a (Pair Nat Atom).

   (claim to-go-order (Pair Nat Atom))

4. Define MyFirstType so that MyFirstType is a type. NOTE: U is the type that describes all types (except itself) and is short for "the universe of types", so we have written as a claim that MyFirstType is a U (i.e. is a type).

   (claim MyFirstType U)

5. Define my-thing-and-atom so that my-thing-and-atom is a (Pair MyFirstType U).

   (claim my-thing-and-Atom (Pair MyFirstType U))

Nats

6. Define and test with-Nats, a function that takes two arguments: - a binary function over Nats, and - a pair of Nats.

   The result of with-Nats should be the result of applying the function (argument 1) to the two Nats in the pair of Nats (argument 2).

   (claim with-Nats

   (-> (-> Nat Nat

   Nat)

   (Pair Nat Nat)

   Nat))

   Test your definition with

   (check-same Nat (with-Nats (λ (n m) n) (cons 1 2)) 1)

   (check-same Nat (with-Nats (λ (n m) (add1 m)) (cons 1 2)) 3)

7. Define and test at-least-two?, it should take a Nat and return the Atom 't if its argument has at least two add1s at the top (i.e. if the Nat is >= 2), otherwise it should return the Atom 'nil. NOTE: the only Nat eliminator at-least-two? should use is which-Nat.

   (claim at-least-two?

   (-> Nat

   Atom))

   Test your definition with

   (check-same Atom (at-least-two? 0) 'nil)

   (check-same Atom (at-least-two? 1) 'nil)

   (check-same Atom (at-least-two? 41) 't)

8. Here are the definitions of addition and multiplication.

   (claim + (-> Nat Nat

   Nat))

   (define + (λ (n m) (rec-Nat n

   m

   (λ (k k+m) (add1 k+m)))))

   (claim * (-> Nat Nat

   Nat))

   (define * (λ (n m) (rec-Nat n

   0

   (λ (k k*m) (+ m k*m)))))

   Define expt to be exponentiation of natural numbers.

   (claim expt (-> Nat Nat Nat))

Lists

9. Define map.

   (claim map

   (Π ((A U)

   (B U))

   (→ (→ A B) (List A)

   (List B))))

10. Define nth which returns the nth element of a list, or if n is too big, returns the default

    (claim nth

    (Π ((A U))

    (→ (List A) A Nat

    A)))

Vecs

11. Define vec-second which takes a ‘proper‘ vector and returns its second element. Introduce your own claim for this one.

Brainteasers

12. Define and test max, a binary operator on natural numbers that returns the larger of the two numbers it is given.

13. Define Ackermann’s function.

    (ack n m) is:

    • (add1 m) if n = 0

    • (ack (sub1 n) 1) if n has add1 at the top and m = 0

    • (ack (sub1 n) (ack n (sub1 m))) if n and m have add1 at the top

Just Dessert

Using Nat and Either, we can define a new type Integer:

(claim Integer U)

(define Integer (Either Nat Nat))

Then we can use the left part to represent negative numbers, and right part to represent non-negative numbers:

(claim minus-one Integer)

(define minus-one (left 0))

(claim minus-two Integer)

(define minus-two (left 1))

(claim minus-four Integer)

(define minus-four (left 3))

(claim int-zero Integer)

(define int-zero (right 0))

(claim plus-two Integer)

(define plus-two (right 2))

(claim plus-three Integer)

(define plus-three (right 3))

Define a function int-+ that takes two Integers and returns their sum as another Integer. Here are some test cases:

(check-same Integer (int-+ minus-four plus-three) minus-one)

(check-same Integer (int-+ minus-two plus-two) int-zero)

(check-same Integer (int-+ minus-two minus-two) minus-four)

You may need to refer to this page for Either.