ass5: tweaks

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/assignment5.mdwn b/assignment5.mdwn
index fab21e4..d73dc0e 100644 (file)
--- a/assignment5.mdwn
+++ b/assignment5.mdwn
@@ -165,7 +165,7 @@ times. In the polymorphic encoding above, the result of that iteration can be
 any type 'a, as long as you have a base element z : 'a and a function s : 'a → 'a.
 
 **Excercise**: get booleans and Church numbers working in OCaml,
 any type 'a, as long as you have a base element z : 'a and a function s : 'a → 'a.
 
 **Excercise**: get booleans and Church numbers working in OCaml,

-including OCaml versions of bool, true, false, zero, succ, add.
+including OCaml versions of bool, true, false, zero, iszero, succ, and **pred**.

 
 Consider the following list type:
 
 
 Consider the following list type:
 


@@ -174,8 +174,8 @@ Consider the following list type:
 We can encode τ lists, lists of elements of type τ as follows:
 
        τ list := ∀'a. 'a → (τ → 'a → 'a) → 'a
 We can encode τ lists, lists of elements of type τ as follows:
 
        τ list := ∀'a. 'a → (τ → 'a → 'a) → 'a

-       nilτ := Λ'a. λn:'a. λc:τ → 'a → 'a. n
-       makeListτ := λh:τ. λt:τ list. Λ'a. λn:'a. λc:τ → 'a → 'a. c h (t ['a] n c)
+       nil τ := Λ'a. λn:'a. λc:τ → 'a → 'a. n
+       make_list τ := λh:τ. λt:τ list. Λ'a. λn:'a. λc:τ → 'a → 'a. c h (t ['a] n c)

 
 As with nats, recursion is built into the datatype.
 
 
 As with nats, recursion is built into the datatype.
 


@@ -185,17 +185,18 @@ We can write functions like map:
                = λf :σ → τ. λl:σ list. l [τ list] nilτ (λx:σ. λy:τ list. consτ (f x) y
 
 **Excercise** convert this function to OCaml.  Also write an `append` function.
                = λf :σ → τ. λl:σ list. l [τ list] nilτ (λx:σ. λy:τ list. consτ (f x) y
 
 **Excercise** convert this function to OCaml.  Also write an `append` function.

-Test with simple lists.
+Also write a **head** function. Test with simple lists.
+

 
 Consider the following simple binary tree type:
 
        type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
 
 **Excercise**
 
 Consider the following simple binary tree type:
 
        type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
 
 **Excercise**

-Write a function `sumLeaves` that computes the sum of all the
+Write a function `sum_leaves` that computes the sum of all the

 leaves in an int tree.
 
 leaves in an int tree.
 

-Write a function `inOrder` : τ tree → τ list that computes the in-order traversal of a binary tree. You
+Write a function `in_order` : τ tree → τ list that computes the in-order traversal of a binary tree. You

 may assume the above encoding of lists; define any auxiliary functions you need.
 
 Baby monads
 may assume the above encoding of lists; define any auxiliary functions you need.
 
 Baby monads