Homework 3: ML and the simply-typed λ-calculus

• Due: 10/14 at 11:59pm
• Points: 30

Please prepare your solutions for problems 1–2 as .ml files and your answer to problem 3 as a PDF file (scanned handwriting is okay, but no .doc or .docx, please). Submit both files in Canvas.

1. Avoid kerning fails

Don’t let this happen to you! Write an ML function find_split : (string → string → bool) → string → (string * string) option that looks for a way to split a string in two such that a given predicate is true. That is, find_split f w should do the following:

• If w can be split into two (possibly empty) strings u and v such that f u v is true, then it returns Some (u, v).

• Otherwise, it returns None.

Then the following code should print don ate:

let input_lines chan =
  let rec loop acc =
    match input_line chan with
    | line → loop (line::acc)
    | exception End_of_file → List.rev acc
  in loop []

let words = input_lines (open_in "/usr/share/dict/words")

let s = "donate"

let () = match find_split (fun x y → List.mem x words && List.mem y words) s with
  | None → print_string "no\n"
  | Some (u, v) → print_string (u ^ " " ^ v ^ "\n")

Hint: Look in the String module for helpful functions, especially String.length, String.get, and String.sub.

2. Regular expression matching

1. Define an ML type regexp for regular expressions:

   • EmptySet is a regexp (which matches nothing)
   • Epsilon is a regexp (which matches only the empty string)
   • Symbol a is a regexp if a is a char
   • Union (a, b) is a regexp if a and b are
   • Concat (a, b) is a regexp if a and b are
   • Star a is a regexp if a is

   For example, the regular expression (a|bc)* would be represented by

   Star (Union (Symbol 'a', Concat (Symbol 'b', Symbol 'c')))

2. Write an ML function match_regexp : regexp → string → bool such that match_regexp a w returns true iff w matches regular expression a. Hints:

   • Use your solution to question 1.

   • String w matches Concat(a, b) iff w can be split into two (possibly empty) strings u and v such that u matches a and v matches b.

   • String w matches Star a iff

     • w is empty, or

     • w can be split into two strings u (which is non-empty) and v (which could be empty) such that u matches a and v matches Star a.

   • Check the test case match_regexp (Star Epsilon) "a" = false.

3. Unpairing

1. Consider the following term:

   t = λx:___. if x.1 then x.2 else succ x.2

   What type should go into the ___ to make t well-typed? Write out the typing derivation for t.

   In Python, we can write things like (a, b) = p, which is equivalent to a = p[0]; b = p[1] if p is a pair. Let’s add a similar construct to our extended λ-calculus:

   t ::= ...
         letpair {x1, x2} = t3 in t4

   Furthermore, suppose that we want to get rid of .1 and .2 and make letpair the only way to unpair pairs.

2. Write .1 and .2 as syntactic sugar in terms of letpair (fill in the ___):

   t.1 ≡ ___
   t.2 ≡ ___

3. Write evaluation and typing rules for letpair.