Updated slides, Coq demo, and OCaml exercise.

README.md

@@ -69,7 +69,8 @@ We also show the limits of dependently-typed functional programming.
   Syntax and operational semantics, on paper and on a machine
   ([slides 01a](slides/fpottier-01a.pdf))
   ([slides 01b](slides/fpottier-01b.pdf))
-  ([Coq demo](coq/DemoSyntaxReduction.v)).
+  ([Coq demo](coq/DemoSyntaxReduction.v))
+  ([OCaml solution to Newton-Raphson exercise](ocaml/NewtonRaphson.ml)).
 * (29/09/2017)
   From a small-step semantics down to an efficient interpreter,
   in several stages.

coq/DemoSyntaxReduction.v

@@ -137,7 +137,28 @@ Hint Extern 1 (_ = _) => autosubst : autosubst.
 
 (* -------------------------------------------------------------------------- *)
 
-(* Let us now prove that the semantics is stable under arbitrary substitutions. *)
+(* Demo: a term that reduces to itself. *)
+
+Definition Delta :=
+  Lam (App (Var 0) (Var 0)).
+
+Definition Omega :=
+  App Delta Delta.
+
+Goal
+  red Omega Omega.
+Proof.
+  (* Apply the beta-reduction rule.
+     (This forces Coq to unfold the left-hand [Omega].) *)
+  eapply RedBeta.
+  (* Check this equality. *)
+  asimpl. (* optional *)
+  reflexivity.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* Let us prove that the semantics is stable under arbitrary substitutions. *)
 
 Lemma red_subst:
   forall t1 t2,
@@ -223,3 +244,7 @@ Qed.
 (* As another EXERCISE, extend the operational semantics with a rule that
    allows strong reduction, that is, reduction under a lambda-abstraction.
    This exercise is more difficult; do not hesitate to ask for help or hints. *)
+
+(* Another suggested EXERCISE: define call-by-value reduction, [cbv]. Prove
+   that [cbv] is a subset of [red]. Prove that values do not reduce. Prove
+   that [cbv] is deterministic. *)

ocaml/NewtonRaphson.ml

@@ -0,0 +1,151 @@
+(* A couple abbreviations. *)
+
+type 'a thunk = 'a Lazy.t
+let force = Lazy.force
+
+(* The definition of (finite or infinite) lazy lists. *)
+
+type 'a stream =
+  'a head thunk
+
+and 'a head =
+  | Nil
+  | Cons of 'a * 'a stream
+
+(* Calling [tail xs] demands the head of the stream, that is, forces
+   the computation of the first element of the stream (if there is one). *)
+
+let tail xs =
+  match force xs with
+  | Nil -> assert false
+  | Cons (_, xs) -> xs
+
+(* Newton-Raphson approximation, following Hughes,
+   "Why functional programming matters", 1990. *)
+
+let next n x =
+  (x +. n /. x) /. 2.
+
+(* An infinite stream obtained by iterating [f]. *)
+
+(* The following definition, copied almost literally from Hughes'
+   paper, is correct but somewhat unsatisfactory; can you see why? Can
+   you fix it? Think about it before reading the solution below. *)
+
+let rec repeat (f : 'a -> 'a) (a : 'a) : 'a stream =
+  lazy (Cons (a, repeat f (f a)))
+
+(*
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *)
+
+(* In the above definition of [repeat], the function call [f a] takes
+   place when the *first* element of the list is demanded by the consumer.
+   That's too early -- ideally, this function call should take place only
+   when the *second* element is demanded, since the result of [f a] is the
+   second element in the infinite stream [a], [f a], [f (f a)], ... *)
+
+(* This code exhibits the problem: *)
+
+let () =
+  let x = ref 0 in
+  let f () = incr x; () in
+  let xs = repeat f () in
+  let xs = tail xs in
+  (* This assertion fails because [x] has been incremented once: *)
+  assert (!x = 0);
+  ignore xs
+
+(* This can be fixed in several ways. One solution is to let [repeat] take an
+   argument of type ['a thunk] instead of ['a]. This approach is in fact the
+   standard encoding of call-by-need into call-by-value, applied to Hughes'
+   code. *)
+
+let rec repeat (f : 'a -> 'a) (a : 'a thunk) : 'a stream =
+  lazy (
+    Cons (
+      force a,
+      repeat f (lazy (f (force a)))
+    )
+  )
+
+(* It can also be written as follows. *)
+
+let rec repeat (f : 'a -> 'a) (a : 'a thunk) : 'a stream =
+  lazy (
+    let a = force a in
+    Cons (
+      a,
+      repeat f (lazy (f a))
+    )
+  )
+
+
+(* We define a wrapper so [repeat] has the desired type again: *)
+
+let repeat (f : 'a -> 'a) (a : 'a) : 'a stream =
+  repeat f (lazy a)
+
+(* The problematic code now behaves as desired: *)
+
+let () =
+  let x = ref 0 in
+  let f () = incr x; () in
+  let xs = repeat f () in
+  (* These assertions succeed: *)
+  let xs = tail xs in
+  assert (!x = 0);
+  let xs = tail xs in
+  assert (!x = 1);
+  let xs = tail xs in
+  assert (!x = 2);
+  ignore xs
+
+(* Back to Newton-Rapshon. *)
+
+let rec within (eps : float) (xs : float stream) : float =
+  match force xs with
+  | Nil -> assert false
+  | Cons (a, xs) ->
+      match force xs with
+      | Nil -> assert false
+      | Cons (b, _) ->
+          if abs_float (a /. b -. 1.) <= eps then b
+          else within eps xs
+
+let sqrt (n : float) : float =
+  within 0.0001 (repeat (next n) n)
+
+let sqrt2 =
+  sqrt 2.