assignments/assignment2/assignment2.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Before you turn this problem in, make sure everything runs as expected. First, **restart the kernel** (in the menubar, select Kernel$\\rightarrow$Restart) and then **run all cells** (in the menubar, select Cell$\\rightarrow$Run All).\n",
    "\n",
    "Make sure you fill in any place that says `YOUR CODE HERE` or \"YOUR ANSWER HERE\", as well as your name below:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "let name = \"\"\n",
    "let rollno = \"\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Important notes about grading:\n",
    "\n",
    "1. **Compiler errors:** All code you submit must compile. Programs that do not compile will probably receive an automatic zero. If you are having trouble getting your assignment to compile, please visit consulting hours. If you run out of time, it is better to comment out the parts that do not compile, than hand in a more complete file that does not compile.\n",
    "2. **Late assignments:** Please carefully review the course website's policy on late assignments, as all assignments handed in after the deadline will be considered late. Verify on moodle that you have submitted the correct version, before the deadline. Submitting the incorrect version before the deadline and realizing that you have done so after the deadline will be counted as a late submission."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "770eb84e794eb6ca02df6a1da06583f5",
     "grade": false,
     "grade_id": "cell-7c7cac7907d9700a",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "# Lambda Calculus Interpreter\n",
    "\n",
    "In this assignment, you will implement lambda calculus interpreters that use different reduction strategies. The abstract syntax tree (AST) for lambda expressions is the one that we have seen in class:\n",
    "\n",
    "\n",
    "```ocaml\n",
    "type expr = \n",
    "  | Var of string\n",
    "  | Lam of string * expr\n",
    "  | App of expr * expr\n",
    "```\n",
    "\n",
    "\n",
    "You are provided a parser function `parse_string` that converts a string to this AST and a printer function `string_of_expr` that converts the AST to string. For example, "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "52ec513522bbeea55ff57211ad27443f",
     "grade": false,
     "grade_id": "cell-23e1b5549d80c9d4",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "#use \"init.ml\"\n",
    "open Syntax\n",
    "let parse_string = Lambda_parse.parse_string\n",
    "let string_of_expr = string_of_expr\n",
    "\n",
    "let _ = parse_string \"(\\\\x.x) (\\\\y.y)\"\n",
    "let _ = string_of_expr (App (Var \"x\",Lam(\"y\",App(Var \"y\", Var \"x\"))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "ea998f1dd614d8045a3c365e5142a6fd",
     "grade": false,
     "grade_id": "cell-194c2c247afe7d06",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "You will need some helper functions to operate over sets. Since we have not studied set data structure in OCaml. We will use lists instead and implement set functionality on top of lists. You can use the functions from the OCaml list standard library for this assignment. The documentation for OCaml list module is available in the [OCaml manual](https://caml.inria.fr/pub/docs/manual-ocaml/libref/List.html). "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "bf1003bf6e6578d15846a3309d6d4b36",
     "grade": false,
     "grade_id": "cell-32cbd4bef27f6b23",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 1\n",
    "\n",
    "Implement a function\n",
    "\n",
    "```ocaml\n",
    "mem : 'a -> 'a list -> bool\n",
    "```\n",
    "\n",
    "`mem e l` returns `true` if the element `e` is present in the list. Otherwise, it returns false. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "982c4de66be8386f73ebda833847e8fb",
     "grade": false,
     "grade_id": "cell-206225a8fc096ef3",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let mem e l = \n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "307673c2297acfaf755d2ded13b6d7ca",
     "grade": true,
     "grade_id": "cell-625148cc24b57f40",
     "locked": true,
     "points": 5,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 5 points *)\n",
    "assert (mem \"b\" [\"a\";\"b\";\"c\"] = true);\n",
    "assert (mem \"x\" [\"a\";\"b\";\"c\"] = false)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "3430c0ab7718078909e38a05b8632a28",
     "grade": false,
     "grade_id": "cell-1ec7266a6b861156",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 2\n",
    "\n",
    "Implement a function\n",
    "\n",
    "```ocaml\n",
    "remove : 'a -> 'a list -> 'a list\n",
    "```\n",
    "\n",
    "`remove e l` returns a list `l'` with all the element in `l` except `e`. `remove` also preserves the order of the elements not removed. If `e` is not present in `l`, then return `l`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "93a5dd227c8fc445f1f778ab16119320",
     "grade": false,
     "grade_id": "cell-3d615242df1b1ad1",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let remove e l = \n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "d00a2840e31a3a14ff835a882f211d7d",
     "grade": true,
     "grade_id": "cell-815b5c339ce6eec3",
     "locked": true,
     "points": 5,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 5 points *)\n",
    "assert (remove \"b\" [\"a\";\"b\";\"c\"] = [\"a\";\"c\"]);\n",
    "assert (remove \"x\" [\"a\";\"b\";\"c\"] = [\"a\";\"b\";\"c\"])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "2cc6e63bb83f6c5d644a0983f3993201",
     "grade": false,
     "grade_id": "cell-c33b1d8b7804ea79",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 3\n",
    "\n",
    "Implement a function\n",
    "\n",
    "```ocaml\n",
    "union : string list -> string list -> string list\n",
    "```\n",
    "\n",
    "`union l1 l2` performs set union of elements in `l1` and `l2`. The elements in the result list `l` must be lexicographically sorted. Hint: You may want to use the functions `List.sort` and `remove_stutter` from assignment 1 to implement union. Here is an example of using `List.sort`. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "7ffc0220b4463a829ac120e15090ee3a",
     "grade": false,
     "grade_id": "cell-873b9c400e58dce1",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "assert (List.sort String.compare [\"x\";\"a\";\"b\";\"m\"] = [\"a\";\"b\";\"m\";\"x\"])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "b6072019c1e4df6000334a0cb9820e2d",
     "grade": false,
     "grade_id": "cell-e498f15f8517e45a",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let union l1 l2 = \n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "6eaac4259a556eabcdab59969373408d",
     "grade": true,
     "grade_id": "cell-42c81525ae442418",
     "locked": true,
     "points": 5,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 5 points *)\n",
    "assert (union [\"a\"; \"c\"; \"b\"] [\"d\"; \"b\"; \"x\"; \"a\"] = [\"a\"; \"b\"; \"c\"; \"d\"; \"x\"])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "610b8144a0c8533db3c7eb8664901eda",
     "grade": false,
     "grade_id": "cell-34fcea53b9616cb9",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 4\n",
    "\n",
    "Implement a function\n",
    "\n",
    "```ocaml\n",
    "add : 'a -> 'a list -> 'a list\n",
    "```\n",
    "\n",
    "`add e l` does a set addition of element `e` to list `l` and returns a list. The resultant list is sorted. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "ecb21b80f375738ebc034a837bdc79a2",
     "grade": false,
     "grade_id": "cell-de42368283c8797d",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let add e l = \n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "0da970ee7310621c448e8e05ad6f7384",
     "grade": true,
     "grade_id": "cell-635dea866c593bca",
     "locked": true,
     "points": 5,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 5 points *)\n",
    "assert (add \"b\" [\"a\";\"c\"] = [\"a\";\"b\";\"c\"]);\n",
    "assert (add \"a\" [\"c\"; \"a\"] = [\"a\";\"c\"])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "874843b413803eb8a2ace0de6417806b",
     "grade": false,
     "grade_id": "cell-f1dd9619dc756101",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Substitution\n",
    "\n",
    "At the heart of reducing lambda expressions is substitution. Recall from the lecture that substitution requires us to generate fresh variable names that is different from every other name used in the current context. We will use the following helper function to generate fresh names."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "9c31a25af601396b5f2822c275dd936e",
     "grade": false,
     "grade_id": "cell-3b59cbec9a54505f",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "let r = ref 0                                                                       \n",
    "                                                                                    \n",
    "let fresh s =                                                                       \n",
    "  let v = !r in                                                                     \n",
    "  r := !r + 1;                                                                      \n",
    "  s ^ (string_of_int v)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "f2a0457a468910ece58905ff5117eee0",
     "grade": false,
     "grade_id": "cell-74338145db045aa3",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "It uses mutability features of OCaml which we will study in later lectures. You can use the `fresh` function as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "d2d2e6ab5efd126ac6bba0b20306615d",
     "grade": false,
     "grade_id": "cell-5b0d0f27bb9cce3e",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "let a = fresh \"a\"\n",
    "let b = fresh \"b\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "5f8908994bdeb653bf6e80302ae264ee",
     "grade": false,
     "grade_id": "cell-f675a808f6af1a01",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 5\n",
    "\n",
    "Implement a function \n",
    "\n",
    "```ocaml\n",
    "free_variables: expr -> string list\n",
    "```\n",
    "\n",
    "that returns the free variables in the given lambda term."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "661276b4380182a3d81dfea20c8cf4c7",
     "grade": false,
     "grade_id": "cell-8ad0bb22f3fca6ed",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let rec free_variables e = \n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "db5902f2bff40fd177cc46d403cde339",
     "grade": true,
     "grade_id": "cell-67d38d859ec6173a",
     "locked": true,
     "points": 20,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 20 points *)\n",
    "assert (free_variables (parse_string \"\\\\x.x\") = []);\n",
    "assert (free_variables (parse_string \"\\\\x.y\") = [\"y\"])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "732ac64fa5642a78b67989abd8d19f95",
     "grade": false,
     "grade_id": "cell-1c48542a53d45ed8",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 6\n",
    "\n",
    "Implement the function\n",
    "\n",
    "```ocaml\n",
    "substitute : expr -> string -> expr -> expr\n",
    "```\n",
    "\n",
    "where `substitute e x v` does `e[v/x]`. For renaming `x` in `Lam(x,y)` with a fresh name, use `Lam (fresh x, ...)`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "d1d5e6ca2267f51586b5cc185097dba1",
     "grade": false,
     "grade_id": "cell-c659e5c57a377290",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let rec substitute expr a b =\n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "4c1cd7b27543b71c37c05d084c898a20",
     "grade": true,
     "grade_id": "cell-d15558191ca8be99",
     "locked": true,
     "points": 20,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 20 points *)\n",
    "assert (alpha_equiv \n",
    "          (substitute (parse_string \"\\\\y.x\") \"x\" (parse_string \"\\\\z.z w\")) \n",
    "          (parse_string \"λy.λz.z w\"));\n",
    "assert (alpha_equiv \n",
    "          (substitute (parse_string \"\\\\x.x\") \"x\" (parse_string \"y\"))\n",
    "          (parse_string \"λx.x\"));\n",
    "assert (alpha_equiv \n",
    "          (substitute (parse_string \"\\\\x.y\") \"y\" (parse_string \"x\"))\n",
    "          (parse_string \"λx0.x\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "5fe2030c1b5cc5da324dfea794f8e106",
     "grade": false,
     "grade_id": "cell-3b42c7f4e25aa1eb",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 7\n",
    "\n",
    "Implement a single step of the call-by-value reduction. Implement the function\n",
    "\n",
    "```ocaml\n",
    "reduce_cbv : expr -> expr option\n",
    "```\n",
    "\n",
    "which does a single step of the call-by-value reduction. Recall that call-by-value reduction is determinisitic. Hence, if reduction is possible, then a single rule applies. `reduce e` returns `Some e'` if reduction is possible and `e'` is the new expression. `reduce e` returns `None` if reduction is not possible."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "f050928143d3324cb8c06263125962f3",
     "grade": false,
     "grade_id": "cell-f0a4289c56a6e0c2",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let rec reduce_cbv e =\n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "55edb677c38d13f45cfd9a15d97aebe1",
     "grade": true,
     "grade_id": "cell-653a749cafdc8a78",
     "locked": true,
     "points": 20,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 20 points *)\n",
    "begin match reduce_cbv (parse_string \"(\\\\x.x) ((\\\\x.x) (\\\\z.(\\\\x.x) z))\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"(λx.x) (λz.(λx.x) z)\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "        \n",
    "begin match reduce_cbv (parse_string \"(λx.x) (λz.(λx.x) z)\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"λz.(λx.x) z\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "        \n",
    "assert (reduce_cbv (parse_string \"λz.(λx.x) z\") = None);\n",
    "        \n",
    "begin match reduce_cbv (parse_string \"(λx.y) ((λx.x x) (λx.x x))\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"(λx.y) ((λx.x x) (λx.x x))\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "\n",
    "assert (reduce_cbv (parse_string \"x y z\") = None)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "cc9a4606c477ad0a4de30757b618f920",
     "grade": false,
     "grade_id": "cell-1cdb7ff49469bd21",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 8\n",
    "\n",
    "Implement a single step of the call-by-name reduction. Implement the function\n",
    "\n",
    "```ocaml\n",
    "reduce_cbn : expr -> expr option\n",
    "```\n",
    "\n",
    "The rest of the instructions are same as `reduce_cbv`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "8e2e4a65202933305105c1432b426a19",
     "grade": false,
     "grade_id": "cell-97e3a2c41734215b",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let rec reduce_cbn e =\n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "c1c1cc0ba8b367ae43b1da6f73c039d4",
     "grade": true,
     "grade_id": "cell-e988e3a110046165",
     "locked": true,
     "points": 20,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 20 points *)\n",
    "begin match reduce_cbn (parse_string \"(\\\\x.x) ((\\\\x.x) (\\\\z.(\\\\x.x) z))\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"(λx.x) (λz.(λx.x) z)\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "        \n",
    "begin match reduce_cbn (parse_string \"(λx.x) (λz.(λx.x) z)\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"λz.(λx.x) z\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "        \n",
    "assert (reduce_cbn (parse_string \"λz.(λx.x) z\") = None);\n",
    "        \n",
    "begin match reduce_cbn (parse_string \"(λx.y) ((λx.x x) (λx.x x))\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"y\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "\n",
    "begin match reduce_cbn (parse_string \"(\\\\x.x x) ((\\\\z.z) y)\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"(λz.z) y ((λz.z) y)\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "\n",
    "assert (reduce_cbn (parse_string \"x y z\") = None)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "53b0b7f92c3d86f76a2c5d677358e7a1",
     "grade": false,
     "grade_id": "cell-db04235908ea8a26",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "source": [
    "## Problem 9\n",
    "\n",
    "Implement a single step of the normal order reduction. Implement the function\n",
    "\n",
    "```ocaml\n",
    "reduce_normal : expr -> expr option\n",
    "```\n",
    "\n",
    "The rest of the instructions are same as `reduce_cbv`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "07d40a515d4a6cc49e2b59fe7896c59f",
     "grade": false,
     "grade_id": "cell-ba11da6e2b5e2acc",
     "locked": false,
     "schema_version": 3,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "let rec reduce_normal e =\n",
    "  (* YOUR CODE HERE *)\n",
    "  raise (Failure \"Not implemented\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "315ac4d140254a82bfdf1d10c1b4c503",
     "grade": true,
     "grade_id": "cell-ded05a8d3813e1e9",
     "locked": true,
     "points": 20,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 20 points *)\n",
    "begin match reduce_normal (parse_string \"(\\\\x.x) ((\\\\x.x) (\\\\z.(\\\\x.x) z))\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"(λx.x) (λz.(λx.x) z)\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "        \n",
    "begin match reduce_normal (parse_string \"(λx.x) (λz.(λx.x) z)\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"λz.(λx.x) z\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "        \n",
    "begin match reduce_normal (parse_string \"λz.(λx.x) z\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"λz. z\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "        \n",
    "begin match reduce_normal (parse_string \"(λx.y) ((λx.x x) (λx.x x))\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"y\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "\n",
    "begin match reduce_normal (parse_string \"(\\\\x.x x) ((\\\\z.z) y)\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"(λz.z) y ((λz.z) y)\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "        \n",
    "begin match reduce_normal (parse_string \"f (\\\\x.x x) ((\\\\z.z) y)\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"f (λx.x x) y\"))\n",
    "| None -> assert false\n",
    "end;\n",
    "\n",
    "begin match reduce_normal (parse_string \"(\\\\x.(\\\\z.z) y) (\\\\x.x x)\") with\n",
    "| Some expr -> assert (alpha_equiv expr (parse_string \"(λz.z) y\"))\n",
    "| None -> assert false\n",
    "end\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "996dc205735dd3cf36e17b376a22f2e2",
     "grade": false,
     "grade_id": "cell-4e0b420ebe296901",
     "locked": true,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "let rec eval log depth reduce expr =                     \n",
    "  if depth = 0 then failwith \"non-termination?\"                                  \n",
    "  else                                                                     \n",
    "    begin match reduce expr with\n",
    "    | None -> expr\n",
    "    | Some expr' ->\n",
    "      if log then print_endline (\"= \" ^ (string_of_expr expr'));                 \n",
    "      eval log (depth-1) reduce expr'                                    \n",
    "    end\n",
    "  \n",
    "let eval_cbv = eval true 1000 reduce_cbv\n",
    "let eval_cbn = eval true 1000 reduce_cbn\n",
    "let eval_normal = eval true 1000 reduce_normal"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "61382ad7e15a0254ff45ef14998f0a92",
     "grade": true,
     "grade_id": "cell-8d1c02b4a1ab2c2f",
     "locked": true,
     "points": 10,
     "schema_version": 3,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "(* 10 points *)\n",
    "let zero = parse_string \"\\\\f.\\\\x. x\" in\n",
    "let one = parse_string \"\\\\f.\\\\x. f x\" in\n",
    "let two = parse_string \"\\\\f.\\\\x. f (f x)\" in\n",
    "let three = parse_string \"\\\\f.\\\\x. f (f (f x))\" in\n",
    "\n",
    "let plus = parse_string \"λm. λn. λs. λz. m s (n s z)\" in\n",
    "let mult = parse_string \"λm. λn. λs. λz. m (n s) z\" in\n",
    "\n",
    "assert (alpha_equiv (eval_normal (App (App (plus, one), two))) three);\n",
    "print_endline \"\";\n",
    "assert (alpha_equiv (eval_normal (App (App (mult, one), three))) three);\n",
    "print_endline \"\";\n",
    "assert (alpha_equiv (eval_normal (App (App (mult, zero), three))) zero)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "OCaml 4.10",
   "language": "OCaml",
   "name": "ocaml-jupyter"
  },
  "language_info": {
   "codemirror_mode": "text/x-ocaml",
   "file_extension": ".ml",
   "mimetype": "text/x-ocaml",
   "name": "OCaml",
   "nbconverter_exporter": null,
   "pygments_lexer": "OCaml",
   "version": "4.10.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}