Project report (2007-04-09(M))

Group Member:	Cherif Salama & Angela Zhu	Date:	2007-04-09

FFT using indexed types

Overview

Discrete Fourier Transformation (DFT) is widely used in digital signal processing applications, such as linear filtering, correlation analysis, and spectrum analysis. Its efficient computation is a topic that has been greatly studied in both academia and industry. The algorithm to perform DFT is called Fast Fourier Transform (FFT). Basically, computing the DFT can be seen as computing a sequence {X(k)} of N complex-valued numbers given another sequence of data {x(n)} of the same length N.

We are aiming at implement FFT algorithm, specifically the Cooley-Turkey's recursive algorithm (CT_FFT), using index types. The implementation in "A Methodology for Generating Verified Combinatorial Circuits" requires that the input to the algorithm must be a list whose length is power of 2. But this must be checked at run time.Our idea is that by encoding the length of FFT input and output, we can statically guarantee that the CT_FFT algorithm behaves well on its input.

---

++ Basic functions CT_FFT algorithm computes the DFT of a list of size N by first split the input list into two sub-lists, one has all odd index elements and another has all even index elements. It then computes the DFT of two sub-lists and uses the result to compute DFT the original list. If N = 2^n, this can be applied recursively and thus the basic functions in the implementation includes:

• Split function: take a list of size 2*n, output two list of size n

let rec  split l =
  match l with 
    [] -> ([], [])
  | x::y::xs -> let (a,b) = split xs in (x::a, y::b)

• Merge function: take two lists of size n, outputs a list of size 2*n.

let rec merge .|n:'(nat)| (dir: float) (l1: ('(n), 'a) slist) (l2: ('(n), 'a) slist): ('(n*2), 'a) slist =
   let len = fftlength .|'(n)| l1 in
    let rec mg .|m:'(nat)| (ll1: ('(m), 'a) slist) (ll2: ('(m), 'a) slist) j =
      match (ll1, ll2) in ('(n*2), 'a) slist with
      | Cons .|m1:'(nat)| (x, xs), Cons .|m2:'(nat)| (y, ys) ->
         let z1 = mult (w dir len j, y) in
         let zx = add (x, z1) in
         let zy = sub (x, z1) in
         let (a,b) = (mg .|'(m1)| xs ys (j+1)) in (Cons .|'(m1)| (zx, a), Cons .|'(m1)| (zy, b))
      | Nil, Nil -> Nil, Nil in 
   let (c, d) = mg .|'(n)| l1 l2 0 in 
      appends .|'(n), '(n)| c d

• FFT function: take a list of size 2^n, recursively call "split" and "merge", output a list of size 2^n.

let rec fft dir l =
  if (List.length l = 1) then 
    l
  else
    let (e,o) = split l in
    let y0 = fft dir e  in
    let y1 = fft dir o  in
    merge dir y0 y1

Lessons in implementation

Types of functions "split", "merge" and "FFT" (First Step):

We first tried to get the length of list recorded in the list and the three element functions:

type ('n  :'(nat), 'a) slist =
  | Nil : ('(0), 'a) slist
  | Cons of   l  et   'm:'(nat) in 'a * ('(m), 'a) slist: ('(S m), 'a) sl  ist

val split :
  (forall n:'(nat) .
      ('(n), 'a) slist -> ('(div2 n), 'a) slist * ('(div2 n), 'a) slist) =
  <forall>

val merge :
  (forall m:'(nat) .
      float ->
      ('(m), float * float) slist ->
      ('(m), float * float) slist -> ('(m + m), float * float) slist) =
  <forall>

val fft :
  (forall n:'(nat) .
      float -> ('(n), float * float) slist -> ('(n), float * float) slist) =
  <forall>

This is exactly what we want w.r.t. to the length of lists we manipulated. If the input to the "fft" function is exactly of length 2^n, we have no problem. However, if the input list has a length like "3, 6, 10,..." which are not a power of 2, the program will complain and report a mis-matching.

Types of functions "split", "merge" and "FFT" (Second Step):

Now the problem is clear: how to guarantee the index type .|n| is a power of 2? So that further in the split we know it will always get a list of even length.

To achieve this, in the index type of the input list, beside the length "n", we need a property or predicate to say that "n" is a power of 2. So we first define the property in Coq like follows:

Inductive isPower2: nat -> Prop :=
      | Power_0 : isPower2 1
      | Power_S : forall n, isPower2 n -> isPower2 (double n).

And now the fft function looks like this:

let rec fft .|n:'(nat), p:'(isPower2 n)| (dir: float) (l: ('(n), 'a) slist) : (('(n), 'a) slist) =
    if (fftlength .|'(n)| l = 1) then l
   else
      let (e,o) = split .|'(n)| l in
          let y0 = fft .|'(div2 n),'(isPower2 (div2 n))| dir e  in
          let y1 = fft .|'(div2 n),'(isPower2 (div2 n))| dir o  in
      aux .|'a, '(n)| (merge .|'(div2 n)| dir y0 y1);;

However, this will not work since we should not pass .|'(isPower2 (div2 n))|directly, as expected, we get the error:

Kind error while checking type application: 
    Type '(isPower2 (div2 n)) is expected to be  of kind '(isPower2 (div2 _UNBOUND_REL_2))     but got '(Prop)

To pass a correct property to say n/2 is also of power 2, we need the following Lemma:

   Lemma div_power2: forall n, gt n 1 -> isPower2 n -> isPower2 (div2 n).

In the next, we show the difficulties to proof and use this Lemma.

"gt n 1" and "gt n/2 1" ---- function "destr_gt"

One pre-condition of lemma "div_power2" is to guarantee that n>1, because n=1 is a power of 2, but 1/2=0 is not. Although in the fft function, if n=1 we return "l" directly, and the recursive call to fft only happens when n>1, but it is not easy to pass this information around.

Thanks to Emir for his help on this problem

*We define another natural number type where:

If n<=1, it is encoded as 'No0' and 'No1'; If n>1, it is encoded as 'Yes' and a proof of n>1:

type 'n:'(nat) gt_one =
  | No0: '(0) gt_one
  | No1: '(S 0) gt_one
  | Yes of let 'm:'(nat) 'p:'(gt m 1) in unit : '(m) gt_one

• We then define a "safelength" which instead of getting the length of the list, returns the lengh

of type '(n) gt_one.

let rec safelength .|n:'(nat)| (l: ('(n), 'a) slist) : '(n) gt_one =
  match l in '(n) gt_one with
  | Nil -> No0
  | Cons .|m1:'(nat)| (x, xs) ->
   (match xs in '(n) gt_one with
      | Nil -> No1
      | Cons .|m2:'(nat)| (y, ys) -> Yes .|'(n), '(ss_gt_1 m2)| ())

• Now we can pass the '(n) gt_one to fft function and it will get the proof of n>1 to prove n is a power of 2. But this is not trivial, we need an auxiliary function to behave like this:

Emir:" give me a return type r and a '(n) gt_one, and two functions (one for each case). If it is greater than the one, I'll invoke the first function and pass the prof to it. Otherwise, I'll invoke the other function and pass the proof to it. Both functions must return the result type 'r which you instantiate for every particular use. Note that this is just a function-based way of writing the case. BUT, it allows us to avoid nested matches etc.

......destr_gt which is an "elimination scheme" for the gt type which acts very much like the match statement, but can be used in place of the match statement. Its type is as follows: "

val destr_gt :
  (forall n:'(nat) , r:'(OCamlType) .
      '(n) gt_one ->
      (forall p:'(n > 1) . unit -> '(r)) ->
      (forall p:'(n <= 1) . unit -> '(r)) -> '(r))

and the "safefft" function now is implemented using the above auxiliary function:

let rec safefft .|n:'(nat),p:'(isPower2 n)| (dir:float) (l:('(n),'a) slist)  : ('(n),'a) slist =
   let case_less    .|p:'(n<=1)| () : ('(n),'a) slist = l in
   let case_greater .|q:'(n>1)| ()  : ('(n),'a) slist   = 
      let (e,o) = split .|'(n)| l in
      let y0 = safefft .|'(div2 n),'(div_power2 n q p)| dir e in
      let y1 = safefft .|'(div2 n),'(div_power2 n q p)| dir o in
      let rr = aux .|'a, '(n)| (merge .|'(div2 n)| dir y0 y1) in rr in
   let condition = destr_gt .|'(n), ('(n),float * float) slist| (safelength .|'(n)| l) in
      condition case_greater case_less

Proofs of Lemma in Coq

We use several Lemma in coq environment to guarantee the desired properties on the lenth of fft lists. Basically, we need the following definitions and lemmas:

Inductive isPower2: nat -> Prop :=
      | Power_0 : isPower2 1
      | Power_S : forall n, isPower2 n -> isPower2 (double n).

Lemma ss_gt_1: forall n, gt (S (S n)) 1.
Lemma div2_double : forall n:nat, div2 (2*n) = n.
Lemma div_power2: forall n, gt n 1 -> isPower2 n -> isPower2 (div2 n).
Lemma div2_plus_div2 : forall n:nat, gt n 1 -> isPower2 n -> div2 n + div2 n = n.
Lemma list_cast : forall e, forall m n:nat, (m=n) -> (OCaml_slist m e) = (OCaml_slist n e).

During this project, we learned how to write proofs for these lemma. Detailed proof please refer to the appendix.

A view on "safe cast"

Cast function is used in our implementation to convert the type of "merge" output, which is '(n/2 + n/2) slist, to the type '(n) slist, for "fft" function. Notice that this is only true when n is even. This is guaranteed if the input to "fft" function is a list of length 2^n. We achieve this by passing the proof around in the index type.

However cast function withOUT "Obj.magic" is a little different from what we've seen in the type checker. In "type_checker.ml" we do the cast by first construction a type called "eq_typ" which can help us to get an indexed type to another indexed type (computational cast). However, this is not applicable here since we only have original coq type.

Thanks to Emir for his help on this problem

Following is what worded for our implementation w.r.t. "cast" issue:

external castFun:'a -> 'b = "%identity";;

let cast .|a,b,p:'(a=b)| (x:'(a)) : '(b) = castFun x;;

let aux .|a, m:'(nat), p:'(gt m 1), q:'(isPower2 m)| (x: ('((div2 (m))+(div2 (m))), 'a) slist) =
    cast .|'(OCaml_slist ((div2 (m))+(div2 (m))) a),
           '(OCaml_slist (m) a),
           '(list_cast a ((div2 (m))+(div2 (m))) (m) (div2_plus_div2 m p q))| x

Concoqtion bug reporting

Before trying to proof the fft function will always get a list of length 2^n, we tried something on "split" function first to guarantee it will always get a input list of even length.

We failed because concoqtion's problem on nested matching, and reported in our email. Emir affirmed that this is a bug and the problem is specified as follows:

let rec split .|n:'(nat), p:'(even n)| (l: ('(n), 'a) slist): (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) =
   match l in (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) with
   | Nil -> Nil, Nil
   | Cons .|m1:'(nat)| (x, xt) ->   
      match xt in (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) with
      | Cons .|m2: '(nat)| (y, xs) ->       
         let (xxs,yys) = (split .|'(m2),'(even_minus_two m2 p)| xs) in Cons .|'(div2 m2)| (x, xxs), Cons .|'(div2 m2)| (y, yys) ;;
*************************************************************************
File "fft1.ml", line 113, characters 35-57:
Coq error in escaped type:
At location 19-20:
Error:
In environment
m2 : nat
m1 := S m2 : nat
n := S _UNBOUND_REL_0 : nat
p : even n
The term "p" has type "even n" while it is expected to have type
"even (S (S m2))"
*************************************************************************

Clearly, n = S m1 and m1 = S m2, but the pattern matching lost this information in the nested match statement.

Test and evaluation

The test cases we used is at the end of the attached source code in the "Appendix".

Appendix: Full implementation in concoqtion

(***********************************************
*     Angela Yun Zhu                           *
*     Cherif Salama                            *
*     RAP, CS Dept, Rice Univ.                 *
*     2007, April 8th                          *
*     Seminar 617 Homework                     *
*     Concoqtion implementation of FFT         *
************************************************)

(* Pi value *)
let pi = 4.0 *. atan(1.0)

(* W = exp(-2PI dir/N)^j. Note that dir=1.0 for the forward transform *)
let w dir n j = 
  let theta = dir *. ((float_of_int (-2 * j)) *. pi) /. (float_of_int n) in
  ((cos theta), (sin theta)) 

(* Complex number addition. Complex numbers are represented as float tuples *)
let add ((r1,i1), (r2, i2)) = ((r1 +. r2), (i1 +. i2))

(* Complex number addition. Complex numbers are represented as float tuples *)
let sub ((r1,i1), (r2, i2)) = ((r1 -. r2), (i1 -. i2))

(* Complex number addition. Complex numbers are represented as float tuples *)
let mult ((r1, i1), (r2, i2)) =
  let rp = (r1 *. r2) -. (i1 *. i2) in
  let ip = (r1 *. i2) +. (r2 *. i1) in
  (rp, ip)
  
(* Sized lists data type as defined before. Use to guarantee
   that the list returned from the fft function is of
   the correct size which is equal to the returned size *)
type ('n:'(nat), 'a) slist =
  | Nil : ('(0), 'a) slist
  | Cons of let 'm:'(nat) in 'a * ('(m), 'a) slist: ('(S m), 'a) slist
;;

(* Some coq definitions and lemmas *)
coq
   (* Required Libraries *)
   Require Import Div2.
   Require Import Arith.Gt.
   
   (* Inductive definition of isPower2, if n=1 than it is a
      power of 2 and if n=double n0 where n0 is a power of2 
      than n also is a power of 2 *)
   Inductive isPower2: nat -> Prop :=
      | Power_0 : isPower2 1
      | Power_S : forall n, isPower2 n -> isPower2 (double n).
   
   (* A successor of a successor is always greater than 1.
      Used for the safe length function *)
   Lemma ss_gt_1: forall n, gt (S (S n)) 1.
      auto with arith.
      Qed.
   
   (* Half double n equals n. Used in the proof of the following
      2 lemmas *)
   Lemma div2_double : forall n:nat, div2 (2*n) = n.
      induction n.
      simpl; auto.
      simpl.
      replace (n + S (n + 0)) with (S (2 * n)).
      rewrite IHn.
      auto.
      simpl.
      auto with arith.
      Qed.
   
   (* If n > 1 and n is a power of 2 than dividing n by 2 gives 
      a power of 2 also. Used in safefft to prove that after spliting 
      a sized list whose length is a power of 2 we get 2 sized lists
      whose lengths are also powers of 2 *)
   Lemma div_power2: forall n, gt n 1 -> isPower2 n -> isPower2 (div2 n).
      intros.
      inversion H0.
      subst.
      absurd (1 > 1).
      apply gt_irrefl.
      auto.
      replace (div2 (double n0)) with n0.
      auto.
      replace (double n0) with (2 * n0).
      rewrite div2_double.
      auto.
      replace (double n0) with (n0 + n0).
      simpl.
      auto.
      auto.
      Qed.

  (* If n > 1 and n is a power of 2 than dividing n by 2 and adding the
    result to itself gives n again. Used in safefft to prove that after 
    and merging we get a list of the same size as of the original list *)
  Lemma div2_plus_div2 : forall n:nat, gt n 1 -> isPower2 n -> div2 n + div2 n = n.
      intros.
      inversion H0.
      subst.
      absurd (1 > 1).
      apply gt_irrefl.
      auto.
      replace (div2 (double n0)) with n0.
      auto.
      replace (double n0) with (2 * n0).
      rewrite div2_double.
      auto.
      replace (double n0) with (n0 + n0).
      simpl.
      auto.
      auto.
      Qed.

 (* if m=n than a sized list of size m has a size equal to a sized list
    of size n. Used in aux function to help achieving a safe cast *)
 Lemma list_cast : forall e, forall m n:nat, (m=n) ->
           (OCaml_slist m e) = (OCaml_slist n e).
      intro; intro; intro.
      intro H.
      rewrite -> H.
      trivial.
        Qed.
end;;

(* external castFun : 'a -> 'b = "%identity" *)
external castFun:'a -> 'b = "%identity";;

(* val cast : (forall a , b , p:'(a = b) . '(a) -> '(b)) = <forall> *)
let cast .|a,b,p:'(a=b)| (x:'(a)) : '(b) = castFun x;;

let aux .|a, m:'(nat), p:'(gt m 1), q:'(isPower2 m)| (x: ('((div2 (m))+(div2 (m))), 'a) slist) =
    cast .|'(OCaml_slist ((div2 (m))+(div2 (m))) a),
           '(OCaml_slist (m) a),
           '(list_cast a ((div2 (m))+(div2 (m))) (m) (div2_plus_div2 m p q))| x

(* splits a lists into 2 lists of equal size, one containing the elements
   originally in odd positions and one containing the elements originally 
   in even positions *)
let rec split .|n:'(nat)| (l: ('(n), 'a) slist): (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist)=
   match l in (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) with
   | Nil -> Nil, Nil
   | Cons .|m1:'(nat)| (x, xs) -> 
      (match xs in (('(div2 n), 'a) slist) * (('(div2 n), 'a) slist) with 
       | Cons .|m2:'(nat)| (y, ys) -> 
         let (xxs, yys) = split .|'(m2)| ys in    
         Cons .|'(div2 m2)| (x, xxs), Cons .|'(div2 m2)| (y, yys))

(* The following 4 function are needed to implement the original merge function 
   as appeared in the paper *)

(* Function that takes a sized list and returns its length as an OCaml integer.
   Used in merge function *)
let rec fftlength .|n:'(nat)| (l: ('(n), 'a) slist) : int =
  match l in int with
  | Nil -> 0
  | Cons .|m1:'(nat)| (x, xs) -> 1 + fftlength .|'(m1)| xs;;

(* Function that takes 2 sized lists and append them. Used in merge function *)
let rec appends .|m:'(nat), n:'(nat)| (l1 : ('(m), 'a) slist) (l2 : ('(n), 'a) slist): ('(m+n), 'a) slist =
   (match l1 as ('i:'(nat),'t) slist in ('(i+n),'t) slist with
   | Nil -> l2
   | Cons .| m1:'(nat)| (x,xs) -> Cons .| '(m1+n) | (x, appends .|'(m1),'(n)| xs l2));;

(* Helper function for merge *)
let rec mg .|n:'(nat)| (l1: ('(n), 'a) slist) (l2: ('(n), 'a) slist) (dir: float) (n: int) (j: int): (('(n), 'a) slist) * (('(n), 'a) slist) =
    match (l1, l2) in (('(n), 'a) slist) * (('(n), 'a) slist) with
    | (Cons .|m1:'(nat)| (x, xs), Cons .|m2:'(nat)| (y, ys)) ->
   let z1 = mult (w dir n j, y) in
   let zx = add (x, z1) in
   let zy = sub (x, z1) in
   let (a,b) = (mg .|'(m1)| xs ys dir n (j+1)) in (Cons .|'(m1)| (zx,a), Cons .|'(m1)| (zy,b))
    | (Nil, Nil) -> (Nil, Nil);;

(* Merge function. Used in safefft *)
let merge .|m:'(nat)| (dir: float) (l1: ('(m), 'a) slist) (l2: ('(m), 'a) slist): (('(m+m), 'a) slist) =
  match l1 in (('(m+m), 'a) slist) with
  | Cons .|m1:'(nat)| (x, xs) -> 
      let n = 2 * fftlength .|'(S m1)| l1 in
      let (a,b) = mg .|'(S m1)| l1 l2 dir n 0 in appends .|'(S m1),'(S m1)| a b;;

(* The following type and 3 functions are needed to implement the original fft function
   as appeared in the paper *)
   
(* This type is required to be able to easily differentiate between numbers that are 
   greater than 1 and those that are not while storing their values. This can be 
   thought of a way of encoding natural numbers while keeping the fact of either
   they are greater than 1 or not explicit in the encoding itself *)   
type 'n:'(nat) gt_one =
  | No0: '(0) gt_one
  | No1: '(S 0) gt_one
  | Yes of let 'm:'(nat) 'p:'(gt m 1) in unit : '(m) gt_one
;;

(* This function is passed a sized list and returns a gt_one encoded number representing
   its length *)
let rec safelength .|n:'(nat)| (l: ('(n), 'a) slist) : '(n) gt_one =
  match l in '(n) gt_one with
  | Nil -> No0
  | Cons .|m1:'(nat)| (x, xs) ->
   (match xs in '(n) gt_one with
      | Nil -> No1
      | Cons .|m2:'(nat)| (y, ys) -> Yes .|'(n), '(ss_gt_1 m2)| ())

(* This function is passed a gt_one encoded number and returns a function that work as follows:
   If given a function that returns something of type r if this number is greater than 1
   and another function that returns something of type r if this number is not greater than r
   it returns something of type r *)
let rec destr_gt .|n:'(nat),r:'(OCamlType)| (cond:'(n) gt_one) : (forall p:'(n>1). unit -> '(r)) -> (forall p:'(n<=1). unit -> '(r)) ->  '(r) = 
   match cond as ('q:'(nat)) gt_one in (forall p:'(q>1). unit -> '(r)) -> (forall p:'(q<=1). unit -> '(r)) -> '(r) with 
   | Yes .|m:'(nat),p:'(m>1)| () -> fun  f g -> f .|'(p)| ()
   | No0 -> fun f g -> g .|'(le_S 0 0 (le_n 0))| ()
   | No1 -> fun f g -> g .| '(le_n 1)| ()  


(* Safe FFT function that takes a sized list of size n which is guaranteed to be a power of 2 
   and returns the FFT as a list of the same size *)
let rec safefft .|n:'(nat),p:'(isPower2 n)| (dir:float) (l:('(n),'a) slist)  : ('(n),'a) slist =
   let case_less    .|q1:'(n<=1)| () : ('(n),'a) slist = l in
   let case_greater .|q2:'(n>1)| ()  : ('(n),'a) slist   = 
      let (e,o) = split .|'(n)| l in
      let y0 = safefft .|'(div2 n),'(div_power2 n q2 p)| dir e in
      let y1 = safefft .|'(div2 n),'(div_power2 n q2 p)| dir o in
      let rr = aux .|'a, '(n), '(q2), '(p)| (merge .|'(div2 n)| dir y0 y1) in rr in
   let condition = destr_gt .|'(n), ('(n),float * float) slist| (safelength .|'(n)| l) in
      condition case_greater case_less
;;

(* The following function is the standard fft implementation from the paper *)
let pi0 = 4.0 *. atan(1.0);;

let w0 dir n j = 
  let theta = dir *. ((float_of_int (-2 * j)) *. pi0) /. (float_of_int n) in
  ((cos theta), (sin theta)) ;;

let add0 ((r1,i1), (r2, i2)) = ((r1 +. r2), (i1 +. i2));;

let sub0 ((r1,i1), (r2, i2)) = ((r1 -. r2), (i1 -. i2));;

let mult0 ((r1, i1), (r2, i2)) =
  let rp = (r1 *. r2) -. (i1 *. i2) in
  let ip = (r1 *. i2) +. (r2 *. i1) in
  (rp, ip);;

let rec split0 l =
  match l with 
  [] -> ([], [])
  | x::y::xs ->
  let (a,b) = split0 xs in (x::a, y::b);;

let merge0 dir l1 l2 =
  let n = 2 * List.length l1 in
  let rec mg0 l1 l2 j =
    match (l1, l2) with
      (x::xs, y::ys) ->
        let z1 = mult0 (w0 dir n j, y) in
        let zx = add0 (x, z1) in
        let zy = sub0 (x, z1) in
        let (a,b) = (mg0 xs ys (j+1)) in (zx::a, zy::b)
    | _ -> ([], []) in
  let (a,b) = mg0 l1 l2 0 in (a @ b);;

let rec fft0 dir l =
  if (List.length l = 1) then 
    l
  else
    let (e,o) = split0 l in
    let y0 = fft0 dir e  in
    let y1 = fft0 dir o  in
    merge0 dir y0 y1;;


(* Tests *)

(* Regular fft *)
let l10 = [(1.1,2.2);(3.3,4.4);(5.5,6.6);(7.7,8.8)];;
fft0 1.0 l10;;

(* Safe fft *)
let l1 = (Cons .|'(3)|((1.1,2.2),Cons .|'(2)|((3.3,4.4),Cons .|'(1)|((5.5,6.6),Cons .|'(0)|((7.7,8.8),Nil)))));;
safefft .|'(4),'(Power_S 2 (Power_S 1 Power_0))| 1.0 l1;;

(* Performance comparison *)
Trxtime.init_times ();;
Trxtime.timenew "Regular fft"  (fun _ -> fft0 1.0 l10);;
Trxtime.timenew "Safe fft"   (fun _ -> (safefft .|'(4),'(Power_S 2 (Power_S 1 Power_0))| 1.0 l1));;
Trxtime.print_times ();;

(* Results running the above code using concoqtion interpreter *)
(*
__ Regular fft _____________ 65536x avg= 1.793996E-02 msec
__ Safe fft ________________ 65536x avg= 1.936152E-02 msec
*)

(* Results running the above code using concoqtion compiler *)
(*
__ Regular fft _____________ 65536x avg= 2.199154E-02 msec
__ Safe fft ________________ 65536x avg= 2.548305E-02 msec
*)
(* In both cases Regular fft is about 10% faster than Safe fft *)

Project proposal (2007-03-26(M))

FFT using indexed types

Project Overview

• This is a two weeks project we will work on during Prof. Taha's absence. (3/23-4/9)
• Group member: Angela & Cherif
• Presentation dates: 3/30 (Cherif) & 4/2 (Angela)

Motivation

Discrete Fourier Transformation (DFT) is widely used in digital signal processing applications, such as linear filtering, correlation analysis, and spectrum analysis. Its efficient computation is a topic that has been greatly studied in both academia and industry. The algorithm to perform DFT is called Fast Fourier Transform (FFT). Basically, computing the DFT can be seen as computing a sequence {X(k)} of N complex-valued numbers given another sequence of data {x(n)} of the same length N.

We propose an index-typed implementation of FFT based on Cooley-Turkey's recursive algorithm. Using that index-type, we get the following benefits:

• Size of the input and output lists is guaranteed to be equal and this checking is done at the type level statically, therefore shouldn't increase the run time.
• Pattern matching is safer since we are now sure that input lists are of equal sizes.

We also want to check the following:

• How easy would it be to write an efficient FFT implementation using Concoqtion and explore more of Concoqtion features needed to achieve this.
• Performance of the Concoqtion implementation of FFT.

Project phases

• Gather information about FFT and its implementations
• Look at Prof. Taha's papers (A Methodology for Generating Verified Combinatorial Circuits, Relating FFTW and Split-Radix) and see how it's implemented there.
• Implement Cooley-Turkey's FFT algorithm with input list of size 2^n.
• Test it on different lists.
• Test it's performance and compare it to the non-indexed implementation.
• Analyze results and report them in class with discussion on difficulties we encountered.

Other project ideas

• Compile-time dimension checking for matrix operations.
• Implement functions simulating the functionality of certain hardware circuit families using indexed types. For example we could think of N-bit adders or N-bit multipliers where N is the type index.

617S07 Homeworks for Angela Zhu (2007-03-02(F))

Tagless Staged Interpreters

ML Implementation of Lambda Calculus (untyped terms)

As described in TAPL by Benjamin, with de Bruijn index representation of variable, untyped terms and its interpreter can be defined like the following. The output of OCaml compiler is also attached.

type term =
  | TmVar of int
  | TmAbs of term
  | TmApp of term * term
;;

let termShift d t =
    let rec walk c t = match t with
   | TmVar (n) -> if n>=c then TmVar(n+d) else TmVar(n)
   | TmAbs (t1) -> TmAbs (walk (c+1) t1)
   | TmApp (t1, t2) -> TmApp (walk c t1, walk c t2)
    in walk 0 t
;;

let termSubst j s t =
    let rec walk c t = match t with 
   | TmVar (n) -> if n=j+c then termShift c s else TmVar (n)
   | TmAbs (t1) -> TmAbs (walk (c+1) t1)
   | TmApp (t1, t2) -> TmApp (walk c t1, walk c t2)
    in walk 0 t
;;

let termSubstTop s t =
    termShift (-1) (termSubst 0 (termShift 1 s) t)
;;

let rec isval ctx t = match t with 
    | TmAbs (_) -> true
    | _ -> false
;;

exception NoRuleApplies

let rec eval1 ctx t = match t with
    | TmApp (TmAbs(t1), v2) when isval ctx v2 -> termSubstTop v2 t1
    | TmApp (v1, t2) when isval ctx v1 -> 
   let t2' = eval1 ctx t2 in TmApp(v1, t2')
    | TmApp (t1, t2) -> 
   let t1' = eval1 ctx t1 in TmApp(t1', t2)
    | _ -> raise NoRuleApplies
;;

let rec eval ctx t = 
    try let t' = eval1 ctx t in
   eval ctx t'
    with NoRuleApplies -> t
;; 

(***************************************************
val termShift : int -> term -> term = <fun>
val termSubst : int -> term -> term -> term = <fun>
val termSubstTop : term -> term -> term = <fun>
val isval : 'a -> term -> bool = <fun>
val eval1 : 'a -> term -> term = <fun>
val eval : 'a -> term -> term = <fun>
****************************************************)

Definition of well typed terms

We need to define an indexed type of terms in concoqtion. Since the index type need to be defined in Coq, we first write up the following coq definitions:

coq 
   Inductive ty: Set :=
   | Int: ty
   | Fun: ty -> ty -> ty.

   Inductive ev: Set :=
   | Empty: ev
   | Ext: ev -> ty -> ev.

   Fixpoint evalT (t:ty): OCamlType :=
     match t with
   | Int => OCaml_int
   | Fun dom cod => OCaml_Arr (evalT dom) (evalT cod)
     end.

   Notation "A -*- B" := 
     (OCaml_Tuple (OCaml_List_cons A (OCaml_List_cons B OCaml_List_nil))) (at level 31, left associativity).
end;;

coq
   Fixpoint evalEnv (e:ev) : OCamlType :=
     match e with
   | Empty => OCaml_unit
   | Ext env t => (evalEnv env) -*- (evalT t) end.
end;;

There are two things seems fishy here:

• You cannot combine this two coq snippet into one, otherwise it doesn't compile.
• You must write this (at level 31, left associativity), which I got from Emir, but cannot get the point.

Then we can define the index typed terms like this:

type ('e:'(ev), 't:'(ty)) tterm =
   | TInt of let 'e1:'(ev) in int: ('(e1), '(Int)) tterm
   | TVarZero of let 'e1:'(ev) 't1:'(ty) in unit: ('(Ext e1 t1), '(t1)) tterm
   | TVarPlus of let 'e1:'(ev) 't1:'(ty) 't2:'(ty) in ('(e1), '(t1)) tterm: ('(Ext e1 t2), '(t1)) tterm
   | TAbs of let 'e1:'(ev) 't1:'(ty) 't2:'(ty) in ('(Ext e1 t1), '(t2)) tterm: ('(e1), '(Fun t1 t2)) tterm
   | TApp of let 'e1:'(ev) 't1:'(ty) 't2:'(ty) in 
   ('(e1), '(Fun t1 t2)) tterm * ('(e1), '(t1)) tterm: ('(e1), '(t2)) tterm
;;

A tagless interpreter with index type

let rec t_eval .|e:'(ev), t:'(ty)| (exp:('(e), '(t)) tterm) (context:'(evalEnv e)): '(evalT t) = 
    match exp in '(evalT t) with
   | TInt .|e1:'(ev)| i -> i  
   | TVarZero .|e1:'(ev), t1:'(ty)| _ -> snd context  
   | TValPlus .|e1:'(ev), t1:'(ty), t2:'(ty)| v1 -> t_eval .|'(e1), '(t1)| v1 (fst context)  
   | TAbs .|e1:'(ev), t1:'(ty), t2:'(ty)| body -> (fun v -> t_eval .|'(Ext e1 t1), '(t2)| body (context, v))  
   | TApp .|e1:'(ev), t1:'(ty), t2:'(ty)| (rator, rand) -> (t_eval .|'(e1), '(Fun t1 t2)| rator context) (t_eval .|'(e1), '(t1)| rand context)
;;
(***************************************************
val t_eval :
  (forall e:'(ev) , t:'(ty) .
      ('(e), '(t)) tterm ->
      '((fix evalEnv (e0 : ev) : OCamlType :=
           match e0 with
           | Empty => OCaml_unit
           | Ext env t0 => evalEnv env -*- evalT t0
           end) e) ->
      '(evalT t)) =
  <forall>
***************************************************)

An interpreter with tags

Before wirte the tagless interpreter successfully with the help from Emir, I also tried to write a taged interpreter, which turns out to be more complicate to implement, because you need to manipulate the type in the index explicitly. Here is something I got:

type 't:'(ty) value = 
    | VInt of int: '(Int) value
    | VFun of let 't1:'(ty) 't2:'(ty) in '(t1) value * '(t2) value: '(Fun t1 t2) value
;;

coq
  Definition codom (t:ty) : ty :=
  match t with
    |  Int => Int
    |  Fun a b => b end.
  Definition dom (t:ty) : ty :=
  match t with
    |  Int => Int
    |  Fun a b => a end.
end

let apply .|arrow:'(ty)| (f:'(arrow) value) : ('(dom arrow) value) ->  '(codom arrow) value =
  match f as 't:'(ty) value in  '(dom t) value -> '(codom t) value with
    | VFun .|a:'(ty),b:'(ty)| f -> (fun x -> f x)
    | _ -> assert false


type 'e:'(ev) ctx =
    | NoBinding : '(Empty) ctx
    | Bindings of let 'e1:'(ev) 't1:'(ty) in '(t1) value * '(e1) ctx: '(Ext e1 t1) ctx

let rec t_eval .|e1:'(ev), t1:'(ty)| (exp:('(e1), '(t1)) tterm) (context:'(e1) ctx): '(t1) value = 
    match exp as ('e:'(ev), 't:'(ty)) tterm in '(t1) value with
   | TInt i -> 
   | TVarZero .|e1:'(ev), t1:'(ty)| _ ->
   | TVarPlus .|e2:'(ev), t1:'(ty), t2:'(ty)| v1 ->
   | TAbs .|e2:'(ev), t1:'(ty), t2:'(ty)| body ->
   | TApp .|e2:'(ev), t1:'(ty), t2:'(ty)| (rator, rand) -> 

Type checker (not accomplished yet)

type 't:'(ty) some_typ = 
 | INT: '(Int) some_typ
 | FUN of let 't1:'(ty) 't2:'(ty) in '(t1) some_typ * '(t2) some_typ: '(Fun t1 t2) some_typ

type 'e:'(ev) some_env = 
 | EMP: '(Empty) some_env
 | EXT of let 'e:'(ev) 't:'(ty) in '(e) some_env * '(t) some_typ: '(Ext e t) some_env

type 'e:'(ev) exist_type = ExTy of let 'e:'(ev)  't:'(ty) in '(t) some_typ * ('(e), '(t)) tterm;;

let rec type_checker .|e:'(ev)| (env0: '(e) some_env) exp0 : '(e) exist_type =
    match exp0 in '(e) exist_type with
   | UApp (e1, e2) -> 
    (match (type_checker .|'(e)| env0 e1, type_checker .|'(e)| env0 e2) in  '(e) exist_type with
      | ExTy .|env1: '(ev), typ1: '(ty)| (urator, trator), ExTy .|env2: '(ev), typ2: '(ty)| (urand, trand) ->
       (match e11 in  '(e) exist_type with
         | FUN .|rator_rator:'(ty), rator_rand:'(ty)| (rrator, rrand) -> 
            let new_rator = FUN .|urand:'(ty), rator_rand:'(ty)| (urand, rrand) in 
            let 
        )
    )

617S07 Homeworks for Angela Zhu (2007-02-26(M))

Homework assigned on 2/21:

• Some speed tests comparing use of existensial and universal quantifiers.
• Try to write zip without the context refinement.

Homework assigned on 2/23:

• Think about how to write lambda and application for next class.
• write three functions:
  • typecheck : untyped -> term option
  • untyped eval : uterm -> uenv -> uvalue option
  • eval : (\gamma, t) term -> (evalEnv \gamma) -> (evalType t)

un-refined zip

This is what I tried at first, but it doesn't work:

# let rec  zip_comp .|n:'(nat)| (xs:('(n), 'a) listl) (ys:('(n), 'b) listl) : ('a * 'b, '(n)) listl =
  (match xs,ys as ('i:'(nat), 'a) listl * ('j:'(nat), 'b) listl in forall p:'(i=j). unit -> ('(i), ('(a) * '(b))) listl with
        | Nil, Nil -> /\p:'(0=0). fun () -> Nil
        | Cons .|i1:'(nat)| (x,xs), Cons .|j1:'(nat)| (y,ys) ->  /\p:'((S i1) = (S j1)). fun () ->
                let ys' = cast .|'(j1),'(i1),'(pred_eq .|'(j1),'(i1)| '((S i1) = (S j1)))| ys in
                let r = zip .|'(i1)| xs ys' in
                Cons .|'(i1)| ((x,y), r)) .|'(refl_equal n)| ()
;;
(***************************************************              
EXCEPTION:
  At location 9-10:
  Syntax error: ',' or ')' expected after [constr:operconstr level 200] (in [constr:operconstr])
*************************************************)

After some effort, I succeded in making it work and the code is like this:

coq
    Require Export Arith.
        Require Omega.
        Lemma pred_eq : forall m n, (S m) = (S n) -> (m=n). intros; omega. Qed.
end

let cast .|m:'(nat),n:'(nat),p:'(m=n)| (x: ('(m), 'a) listl) : ('(n), 'a) listl =
  Obj.magic x
;;

let rec  zip_comp .|n:'(nat)| (xs:('(n), 'a) listl) (ys:('(n), 'b) listl) : ('(n), 'a * 'b) listl =
  (match xs,ys as ('i:'(nat), 'a) listl * ('j:'(nat), 'b) listl in forall p:'(i=j). unit -> ('(j), ('(a) * '(b))) listl with
        | Nil, Nil -> /\p:'(0=0). fun () -> Nil
        | Cons .|i1:'(nat)| (x,xs), Cons .|j1:'(nat)| (y,ys) ->  /\p:'(i1=j1). fun () ->
                let xs' = cast .|'(i1),'(j1),'(p)| xs in
                let r = zip_comp .|'(j1)| xs' ys in
                Cons .|'(j1)| ((x,y), r)) .|'(refl_equal n)| ()
;;

concoqtion encoding of typed term

type untyped =
  | UnVar of int
  | UnAbs of untyped
  | UnApp of untyped * untyped
;;

type (env, typ) term = 
  | TVarZero 
      let env':envType in
    : (env' * typ, typ) term
  | TVarPlus of
      let env':envType in
      let t':typeType in
         (env, typ) term
    : (env' * t', typ) term
  | TAbs of
      let env':envType in
      let t1:typeType t2:typeType in
         (env' * t1, t2) term
    : (env', t1 -> t2) term
  | TApp of
      let env':envType in
      let t1->t2:typeType t1:typeType in
         (env', t1->t2) term * (env', t1) term
    : (env', t2) term

;;

type exist_type = ETy of let env:envType, typ:typeType in (env, typ) term;;
type 'a option = 
   | Some of 'a
   | None
;;

typechecking and evaluation

(***************************************************
 typecheck : untyped -> term option
****************************************************)
let rec typecheck env:envType t:untyped: exist_type option =
    match t as untype in exist_type option with
   | UnVar (i) -> if (i=0) then Some (Ety .|env, typ| TVarZero)
            else (if i<length(env) 
               then let t1 = getTypeFromEnv env i in
                  Some (Ety .|env, typ| (TVarPlus .|t1| ))
               else None)
   | UnAbs (t) -> Some (Ety .|env, typ| (TAbs .|| ))
   | UnApp (t1, t2) -> let tt1 = typecheck env t1 in
             let tt2 = typecheck env t2 in
            match tt1 in exist_type option with Arrow (ta1, ta2) ->
               if ta1=tt2 then ta2 else None
;;


(***************************************************
 untyped_eval : untyped -> uenv -> uvalue option
****************************************************)
let rec untyped_eval env t = 
    match t with
   | UnApp (UnAbs(i, un), v) -> if (isVal v) then subst un v else 
               let v2 = untyped_eval env v in subst un v2
   | UnApp (t1, t2) -> let v1 = untyped_eval env t1 in
            (match v1 with | UnApp (UnAbs(i, un), v) -> if (isVal v) then subst un v else 
                   let v2 = untyped_eval env v in subst un v2
                      | _ -> None
;;


(***************************************************
 eval : (env, t) term -> (evalEnv env) -> (evalType t)
****************************************************)

617S07 Homeworks for Angela Zhu (2007-02-19(M))

Braun Trees

copy braun using Copy2 function (O(log n)) (using existential types)

type 'a exist_braun2 = EE of let 'n:'(nat) in (('(S n), 'a) braun_tree) * (('(n), 'a) braun_tree);;

let rec copy_two_braun (x:'a) (k: int): 'a exist_braun2 =
    if k=0 then EE .|'(0)| ((BBranch .|'(0)| (x, Leaf, Leaf)), Leaf) else 
    (let s= copy_two_braun x ((k-1)/2) in
    (match s as 'a exist_braun2 in 'a exist_braun2 with 
   | EE .|i:'(nat)| (s_tree, t_tree) ->
    if ((k/2)=(k-1)/2) then (* k is odd *) 
   EE .|'(S (i*2))| ((IBranch .|'(i)| (x, s_tree, t_tree)), (BBranch .|'(i)| (x, t_tree, t_tree)))
    else (* k is even *)
   EE .|'(S (S (i*2)))| ((BBranch .|'(S i)| (x, s_tree, s_tree)), (IBranch .|'(i)| (x, s_tree, t_tree)))
))
;;
(***************************************************
val copy_two_braun : 'a -> int -> 'a exist_braun2 = <fun>
*************************************************)

Here is the O(log n) time copy function using copy2:

type 'a exist_braun = EB of let 'n:'(nat) in (('(n), 'a) braun_tree);;


let rec copy_braun_logn (x:'a) (k: int) = 
    let braun2 = copy_two_braun x k in
    match braun2 as 'a exist_braun2 in 'a exist_braun with
   | EE .|m:'(nat)| (s_tree, t_tree) -> EB .|'(m)| t_tree
;;
(***************************************************
val copy_braun_logn : 'a -> int -> 'a exist_braun = <fun>
*************************************************)

copy braun using Copy2 function (O(log n)) (using odd_even natural encoding)

type ('m:'(nat)) odd_even = 
     | Z: '(0) odd_even
     | S_odd of let 'm:'(nat) in '(m) odd_even: '(S (m*2)) odd_even
     | S_even of let 'm:'(nat) in '(m) odd_even: '(S (S (m*2))) odd_even
;;

type exist_oe = EO of let 'n:'(nat) in ('(n) odd_even);;

let rec int2oe (k:int) : exist_oe =
    if k=0 then EO .|'(0)| Z else
       (if ((k/2)=(k-1)/2) then (* k is odd *) let x = int2oe (k/2) in 
   (match x in exist_oe with 
      | EO .|m:'(nat)| y -> EO .|'(S (m*2))| (S_odd .|'(m)| y)
   )
   else (* k is even *) let x = int2oe (k/2 -1) in
   (match x in exist_oe with 
      | EO .|m:'(nat)| y -> EO .|'(S (S (m*2)))| (S_even .|'(m)| y)
   ))
;;

let rec copy2 .|m:'(nat)| (x:'a) (k: '(m) odd_even): (('(S m), 'a) braun_tree) * ('(m), 'a) braun_tree =
    match k in (('(S m), 'a) braun_tree) * ('(m), 'a) braun_tree with
   | Z -> ((BBranch .|'(0)| (x, Leaf, Leaf)), Leaf)
   | S_odd .|n:'(nat)| y -> let st = copy2 .|'(n)| x y in
   (match st in (('(S (S (n * 2))), 'a) braun_tree) * ('(S (n * 2)), 'a) braun_tree with 
      | (s, t) -> (IBranch .|'(n)| (x, s, t), BBranch .|'(n)| (x, t, t)))
   | S_even .|n:'(nat)| y -> let st = copy2 .|'(n)| x y in
   (match st in (('(S (S n * 2)), 'a) braun_tree) * ('(S (S (n * 2))), 'a) braun_tree with 
      | (s, t) -> (BBranch .|'(S n)| (x, s, s), IBranch .|'(n)| (x, s, t)))
;;


let rec copy_braun_fast (x:'a) (k: int): 'a exist_braun = 
    let oe = int2oe k in
    match oe as exist_oe in 'a exist_braun with
   | EO .|m:'(nat)| kk -> (let st = copy2 .|'(m)| x kk in
   match st in 'a exist_braun with 
      | (s, t) -> EB .|'(m)| t)
;;
(***************************************************
val int2oe : int -> exist_oe = <fun>
val copy2 :
  (forall m:'(nat) .
      'a -> '(m) odd_even -> ('(S m), 'a) braun_tree * ('(m), 'a) braun_tree) =
  <forall>
val copy_braun_fast : 'a -> int -> 'a exist_braun = <fun>
*************************************************)

Remove a node from a tree

Remove function for a simple tree: 3 steps: (1) remove_last (2) get_last (3) remove_any: substitute a brand node with the last node in the tree

(***************************************************
Remove function
val remove_last : 'a tree -> 'a tree = <fun>
val get_last : 'a tree tree -> 'a tree = <fun>
val remove_tree : 'a tree -> 'a tree tree -> 'a tree tree = <fun>
*************************************************)

let rec remove_last t: 'a tree = 
    match t with 
   | Leaf_t -> Leaf_t
   | Branch_t (r, lchild, Leaf_t) -> remove_last lchild
   | Branch_t (r, lchild, rchild) -> Branch_t (r, lchild, (remove_last rchild))
;;

exception NULL;;

let rec get_last t: 'a tree = 
    match t with 
   | Leaf_t -> raise NULL
   | Branch_t (r, Leaf_t, Leaf_t) -> r
   | Branch_t (r, lchild, Leaf_t) -> get_last lchild
   | Branch_t (r, lchild, rchild) -> get_last rchild
;;



let rec remove_tree (x: 'a) (t: 'a tree) = 
    match t with 
   | Leaf_t -> raise NULL
   | Branch_t (x, lchild, Leaf_t) -> lchild
   | Branch_t (x, Leaf_t, rchild) -> rchild
   | Branch_t (x, lchild, rchild) -> let y = get_last t in Branch_t (y, lchild, (remove_last rchild))
;;

But I have problems to do it on braun_trees.

617S07 Homeworks for Angela Zhu (2007-02-09(F))

Braun Trees

Conceptions and Definitions

Braun trees are balanced trees which are most circumscribed. For any given node of a Braun tree, the left subtree is either exactly the same size as the right subtree, or one element larger. It has following properties:

• Braun trees always have minimum height.
• The shape of each braun tree is completely determined by its size.
• Most operations on braun tree which involves a single element (e.g. adding, removing, inspecting, updating) take O(log n) time.
• It has been used to implement both flexible arrays and priority queues.

Here is the definition of braun tree in concoqtion:

 type ('n:'(nat), 'a) braun_tree =
   | Leaf: ('(0), 'a) braun_tree
   | BBranch of let 'm: '(nat) in 'a * ('(m), 'a) braun_tree * ('(m), 'a) braun_tree:  ('(S (m*2)), 'a) braun_tree
   | IBranch of let 'm: '(nat) in 'a * ('(S m), 'a) braun_tree * ('(m), 'a) braun_tree:  ('(S (S (m*2))), 'a) braun_tree
   ;;  

(***************************************************
type ('a:'(nat), 'b:'(OCamlType)) braun_tree =
    Leaf:('(0), 'b) braun_tree
  | BBranch of  let 'm:'(nat)  in  'b * 
              ('(m), 'b) braun_tree * ('(m), 'b) braun_tree :
              ('(S (m * 2)), 'b) braun_tree
  | IBranch of  let 'm:'(nat)  in  'b * 
              ('(S m), 'b) braun_tree * 
              ('(m), 'b) braun_tree : ('(S (S (m * 2))), 'b) braun_tree
*************************************************)

"map" function on braun trees

let rec map_braun .|n:'(nat)| (f: 'a -> 'b) (btree: ('(n), 'a) braun_tree)
    : (('(n), 'b) braun_tree) =
    match btree as ('i: '(nat), 'a) braun_tree in ('(i), 'b) braun_tree with
   | Leaf -> Leaf
   | BBranch .|m:'(nat)| (root, lchild, rchild) -> BBranch .|'(m)| (f root, map_braun .|'(m)| f lchild, map_braun .|'(m)| f rchild)
   | IBranch .|m:'(nat)| (root, lchild, rchild) -> IBranch .|'(m)| (f root, map_braun .|'(S m)| f lchild, map_braun .|'(m)| f rchild)
;;

(***************************************************
val map_braun :
  (forall n:'(nat) .
      ('a -> 'b) -> ('(n), 'a) braun_tree -> ('(n), 'b) braun_tree) =
  <forall>
*************************************************)

"fold" function and "braun_to_list"

let rec fold_braun .|n:'(nat)| (res: 'r) (step: 'a -> 'r ->'r) (btree: ('(n), 'a) braun_tree): 'r = 
   match btree as ('i: '(nat), 'a) braun_tree in 'r with
   | Leaf -> res
   | BBranch .|m:'(nat)| (root, lchild, rchild) -> 
   (let r1 = step root res in 
    let r2 = fold_braun .|'(m)| r1 step lchild in
    fold_braun .|'(m)| r2 step rchild)
   | IBranch .|m:'(nat)| (root, lchild, rchild) -> 
   (let r1 = step root res in 
    let r2 = fold_braun .|'(S m)| r1 step lchild in
    fold_braun .|'(m)| r2 step rchild)
;;
(***************************************************
Warning: Unspecified return type for the extended match expression. 

(forall n:'(nat) . 'a -> ('b -> 'a -> 'a) -> ('(n), 'b) braun_tree -> 'a) =
  <forall>
*************************************************)

We then implement a function convert a braun tree to a list using the defined "fold" function:

let rec fold_braun_to_list .|n:'(nat)| (btree: ('(n), 'a) braun_tree): 'a list =
    let to_list node l = node::l in
    fold_braun .|'(n)| [] to_list btree
;;

(***************************************************
val braun_to_list : (forall n:'(nat) . ('(n), 'a) braun_tree -> 'a list) =
  <forall>
*************************************************)

Some implementations of "Three Algorithms on Braun Trees"

Calculating the size of a braun tree

It is trivial to calculate the size of a tree in O(n) time by counting every node individually.

size<>        = 0
size<x, s, t> = 1 + size s + size t

The concoqtion implementation of this algorithm as follows:

let rec size_braun_bad .|n:'(nat)| (btree: ('(n), 'a) braun_tree)
    : int =
    match btree as ('i: '(nat), 'a) braun_tree in int with
   | Leaf -> 0
   | BBranch .|m:'(nat)| (root, lchild, rchild) -> let m = size_braun_bad .|'(m)| rchild in (1+m+m)
   | IBranch .|m:'(nat)| (root, lchild, rchild) -> let m = size_braun_bad .|'(m)| rchild in (2+m+m)
;;

(***************************************************
val size_braun_bad : (forall n:'(nat) . ('(n), 'a) braun_tree -> int) =
  <forall>
*************************************************)

An algorithm of time O(log^2 n) to compute its size can be achieve by taking advantage of the fact that: Once we know the size of one subtree (right), there are only two possibility for the size of the other subtree (left) (= or +1).

The complete algorithm is as follows, detailed explaination please refer to the paper.

size <>        = 0
size <x, s, t> = let m = size t in 1 + 2*m + diff s m 

diff <> 0      = 0
diff <x, s, t> (2*k+1) = diff s k
diff <x, s, t> (2*k+2) = diff t k

Here is the concoqtion implementation of this algorithm:

let rec diff .|n:'(nat)| (btree: ('(n), 'a) braun_tree) (k:int): int =
    if (k=0) then (match btree as ('i: '(nat), 'a) braun_tree in int with
   | Leaf -> 0
     (*   | BBranch .|m:'(nat)| (x, Leaf, Leaf) -> 1  *) ) 
    else 
    (if ((k/2)=(k-1)/2) then (* k is odd , diff lchild (k/2) *)
   (match btree as ('i: '(nat), 'a) braun_tree in int with
   | BBranch .|m:'(nat)| (root, lchild, rchild) -> diff .|'(m)| lchild (k/2)
   | IBranch .|m:'(nat)| (root, lchild, rchild) -> diff .|'(S m)| lchild (k/2))
    else (* k is even , diff rchild (k/2-1) *)
   (match btree as ('i: '(nat), 'a) braun_tree in int with
   | BBranch .|m:'(nat)| (root, lchild, rchild) -> diff .|'(m)| rchild (k/2-1)
   | IBranch .|m:'(nat)| (root, lchild, rchild) -> diff .|'(m)| rchild (k/2-1)))
;;
(***************************************************
val diff : (forall n:'(nat) . ('(n), 'a) braun_tree -> int -> int) = <forall>
*************************************************)


let rec size_braun .|n:'(nat)| (btree: ('(n), 'a) braun_tree): int =
    match btree as ('i: '(nat), 'a) braun_tree in int with
   | Leaf -> 0
        | BBranch .|m:'(nat)| (root, lchild, rchild) -> let ss = size_braun .|'(m)| rchild in (1+2*ss + (diff .|'(m)| lchild ss))
   | IBranch .|m:'(nat)| (root, lchild, rchild) ->  let ss = size_braun .|'(m)| rchild in (1+2*ss + (diff .|'(S m)| lchild ss))
;;
(***************************************************
val size_braun : (forall n:'(nat) . ('(n), 'a) braun_tree -> int) = <forall>
*************************************************)

Creating a braun tree by copying

O(n) time version (1st of three)

Algorith:

copy x 0 = <>
copy x (2*m+1) = <x, copy x m, copy x m>
copy x (2*m+2) = <x, copy x m+1, copy x m>

Implemenation in concoqtion: Failed

let rec copy_braun_bad (x:'a) (k: int): 'a exist_braun =
    if k=0 then EB .|'(0)| Leaf else
    (if ((k/2)=(k-1)/2) then (* k is odd *) 
   (let child = (copy_braun_bad x (k/2)) in (match child as ('a exist_braun) in ('a exist_braun) with 
        | EB .|m:'(nat)| subtree -> EB .|'(S (m*2))| (BBranch .|'(m)| (x, subtree, subtree)))) 
     else (* k is even *)
   (let lchild = (copy_braun_bad x (k/2)) in let rchild = (copy_braun_bad x (k/2-1)) in 
   (match rchild as ('a exist_braun) in ('a exist_braun) with 
        | EB .|r:'(nat)| subr -> 
   (match lchild as ('a exist_braun) in ('a exist_braun) with 
        | EB .|l:'(nat)| subl -> EB .|'(S (S (r*2)))| (IBranch .|'(r)| (x, subl, subr))))))
;;

(*************************************************
This expression has type ('(_UNBOUND_REL_1), 'a) braun_tree
but is here used with type ('(S _UNBOUND_REL_3), 'b) braun_tree
*************************************************)

O(log^2 n) time version (2nd of three)

Algorithm:

copy x 0 = <>
copy x (2*m+1) = <x, t, t>
copy x (2*m+2) = <x, x+t, t>
      where t = copy x m
x+<>     = <x>
x+<y,s,t>= <x, y+t, s>
   is the standard algorithm for adding an element

Implemenation in concoqtion:

let rec insert_braun .|n:'(nat)| (x: 'a) (btree: ('(n), 'a) braun_tree): ('(S n), 'a) braun_tree =
    match btree as ('i: '(nat), 'a) braun_tree in ('(S i), 'a) braun_tree with
   | Leaf -> BBranch .|'(0)| (x, Leaf, Leaf)
        | BBranch .|m:'(nat)| (root, lchild, rchild) -> IBranch .|'(m)| (root, insert_braun .|'(m)| x lchild, rchild)
   | IBranch .|m:'(nat)| (root, lchild, rchild) -> BBranch .|'(S m)| (root, lchild, insert_braun .|'(m)| x rchild)
;;

(***************************************************
let rec insert_braun_ex .|n:'(nat)| (x: 'a) (btree: ('(n), 'a) braun_tree): ('(S n), 'a) braun_tree =
    match btree as ('i: '(nat), 'a) braun_tree in ('(S i), 'a) braun_tree with
   | Leaf -> BBranch .|'(0)| (x, Leaf, Leaf)
        | BBranch .|m:'(nat)| (root, lchild, rchild) -> IBranch .|'(m)| (root, insert_braun_ex .|'(m)| x rchild, lchild)
   | IBranch .|m:'(nat)| (root, lchild, rchild) -> BBranch .|'(S m)| (root, insert_braun_ex .|'(m)| x rchild, lchild)
;;
*************************************************)

type 'a exist_braun = EB of let 'n:'(nat) in (('(n), 'a) braun_tree);;

let rec copy_braun_bad (x:'a) (k: int): 'a exist_braun =
    if k=0 then EB .|'(0)| Leaf else
    (if ((k/2)=(k-1)/2) then (* k is odd *) 
   (let child = (copy_braun_bad x (k/2)) in (match child as ('a exist_braun) in ('a exist_braun) with 
        | EB .|m:'(nat)| subtree -> EB .|'(S (m*2))| (BBranch .|'(m)| (x, subtree, subtree)))) 
     else (* k is even *)
   (let rchild = (copy_braun_bad x (k/2-1)) in 
   (match rchild as ('a exist_braun) in ('a exist_braun) with 
        | EB .|m:'(nat)| subr -> EB .|'(S (S (m*2)))| (IBranch .|'(m)| (x, insert_braun .|'(m)| x subr, subr)))))
;;
(***************************************************
val copy_braun_bad : 'a -> int -> 'a exist_braun = <fun>
*************************************************)

O(log n) time version (3rd of three)

Algorithm:

copy x n       = snd (copy2 x n)

copy2 x 0 = (<x>,<>)
copy2 x (2*m+1) = (<x,s,t>, <x,t,t>)
copy2 x (2*m+2) = (<x,s,s>, <x,s,t>)
      where (s,t) = copy2 x m

Implemenation in concoqtion: Failed Here is the correct version.

let rec copy_two_braun (x:'a) (k: int): 'a exist_braun * 'a exist_braun =
    if k=0 then (EB .|'(1)| (BBranch .|'(0)| (x, Leaf, Leaf)), EB .|'(0)| Leaf) else 
    (let (s, t)= copy_two_braun x ((k-1)/2) in
    (match (s, t) as 'a exist_braun * 'a exist_braun in 'a exist_braun * 'a exist_braun with 
   | (EB .|i:'(nat)| s_tree, EB .|j:'(nat)| t_tree) ->
    if ((k/2)=(k-1)/2) then (* k is odd *) 
   (EB .|'(S (S (j*2)))| (IBranch .|'(j)| (x, s_tree, t_tree)), EB .|'(S (j*2))| (BBranch .|'(j)| (x, t_tree, t_tree))) 
    else (* k is even *)
   (EB .|'(S (i*2))| (BBranch .|'(i)| (x, s_tree, s_tree)), EB .|'(S (S (j*2)))| (IBranch .|'(j)| (x, s_tree, t_tree))) 
))
;;

(***************************************************
This expression has type ('(_UNBOUND_REL_2), 'a) braun_tree
but is here used with type ('(S _UNBOUND_REL_1), 'b) braun_tree
*************************************************)

617S07 Homeworks for Angela Zhu (2007-02-07(W))

Braun Trees

Descriptions and DML version (braun_tree)

Today we begin to try definition and functions on braun trees. A braun tree is a binary tree where for every branch node, the the size of its left son is the same as or one more than that of the right son. It can be readily proven that Braun trees are balanced trees. Here is its DML implementations:

datatype 'a brauntree with nat =
    L(0)
  | {m:nat, n:nat | n <= m <= n+1}
    B(m+n+1) of 'a * 'a brauntree(m) * 'a brauntree(n)

fun('a)
    diff (k, L) = 0
  | diff (k, B(_, l, r)) =
    if k = 0 then 1
    else if k % 2 = 1 then diff (k/2, l) else diff (k/2 - 1, r)
withtype {k:nat, n:nat | k <= n <= k+1} <n> => int(k) * 'a brauntree(n) -> int(n-k)

fun('a)
    size (L) = 0
  | size (B(_, l, r)) =
    let val n = size r in 1 + n + n + diff (n, l) end
withtype {n:nat} <n> => 'a brauntree(n) -> int(n)

Definition of braun tree in concoqtion

type 'a tree = 
   | Leaf_t
   | Branch_t of 'a * 'a tree * 'a tree
;;
(***************************************************
type 'a:'(OCamlType) tree =
    Leaf_t:'a tree
  | Branch_t of  'a * 'a tree * 'a tree : 'a tree
*************************************************)

 type ('n:'(nat), 'a) braun_tree =
   | Leaf: ('(0), 'a) braun_tree
   | BBranch of let 'm: '(nat) in 'a * ('(m), 'a) braun_tree * ('(m), 'a) braun_tree:  ('(1+m+m), 'a) braun_tree
   | IBranch of let 'm: '(nat) in 'a * ('(S m), 'a) braun_tree * ('(m), 'a) braun_tree:  ('(2+m+m), 'a) braun_tree
   ;;  
(***************************************************
type ('a:'(nat), 'b:'(OCamlType)) braun_tree =
    Leaf:('(0), 'b) braun_tree
  | BBranch of  let 'm:'(nat)  in  'b * ('(m), 'b) braun_tree *
             ('(m), 'b) braun_tree :
             ('(S
                  ((fix plus (n m0 : nat) {struct n} : nat :=
                      match n with
                      | O => m0
                      | S p => S (plus p m0)
                      end)
                     ((fix plus (n m0 : nat) {struct n} : nat :=
                         match n with
                         | O => m0
                         | S p => S (plus p m0)
                         end) 0 m) m)),
              'b)
             braun_tree
  | IBranch of  let 'm:'(nat)  in  'b * ('(S m), 'b) braun_tree *
             ('(m), 'b) braun_tree :
             ('(S
                  ((fix plus (n m0 : nat) {struct n} : nat :=
                      match n with
                      | O => m0
                      | S p => S (plus p m0)
                      end)
                     ((fix plus (n m0 : nat) {struct n} : nat :=
                         match n with
                         | O => m0
                         | S p => S (plus p m0)
                         end) 1 m) m)),
              'b)
             braun_tree
*************************************************)

"map" function on tree and braun_tree

let rec map_tree (f: 'a -> 'b) (t: 'a tree) =
    match t with
   | Leaf_t -> Leaf_t
   | Branch_t (r, lchild, rchild) -> Branch_t (f r, map_tree f lchild, map_tree f rchild)
;;
(***************************************************
val map_tree : ('a -> 'b) -> 'a tree -> 'b tree = <fun>
*************************************************)


let rec map_braun .|n:'(nat)| (f: 'a -> 'b) (btree: ('(n), 'a) braun_tree)
    : (('(n), 'b) braun_tree) =
    match btree as ('i: '(nat), 'a) braun_tree in ('(i), 'b) braun_tree with
   | Leaf -> Leaf
   | BBranch .|m:'(nat)| (root, lchild, rchild) -> BBranch .|'(m)| (f root, map_braun .|'(m)| f lchild, map_braun .|'(m)| f rchild)
   | IBranch .|m:'(nat)| (root, lchild, rchild) -> IBranch .|'(m)| (f root, map_braun .|'(S m)| f lchild, map_braun .|'(m)| f rchild)
;;
(***************************************************
val map_braun :
  (forall n:'(nat) .
      ('a -> 'b) -> ('(n), 'a) braun_tree -> ('(n), 'b) braun_tree) =
  <forall>
*************************************************)

617S07 Homeworks for Angela Zhu (2007-02-02)

Date:	2007-02-02(F)

Lists

Definition of Sized List

I tried two ways to define a "sized list". It seems that both ways are OK, but it turns out that "listm" will have some problems when we writing functions on it. "listl" works pretty well, and it is also good to change the "1+m" in its definition to "S m". I also printed the output of concoqtion compiler (conc). From these, it is clear what the difference between these two definitions.

(*unsized version: *)
type 'a list = Nil  |  'a * 'a list;;

#type ('n:'(nat), 'a) listm =
  | Nil : ('(0), 'a) listm
  | Cons of let 'm:'(nat) in 'a * ('(m), 'a) listm: ('(m+1), 'a) listm
  ;;


(***************************************************
type ('a:'(nat), 'b:'(OCamlType)) listm =
    Nil:('(0), 'b) listm
  | Cons of  let 'm:'(nat)  in  'b * ('(m), 'b) listm :
           ('((fix plus (n m0 : nat) {struct n} : nat :=
                 match n with
                 | O => m0
                 | S p => S (plus p m0)
                 end) m 1),
            'b)
           listm
*************************************************)


#type ('n:'(nat), 'a) listl =
  | Nil : ('(0), 'a) listl
  | Cons of let 'm:'(nat) in 'a * ('(m), 'a) listl: ('(1+m), 'a) listl
  ;;
(***************************************************
type ('a:'(nat), 'b:'(OCamlType)) listl =
    Nil:('(0), 'b) listl
  | Cons of  let 'm:'(nat)  in  'b * ('(m), 'b) listl :
           ('(S
                ((fix plus (n m0 : nat) {struct n} : nat :=
                    match n with
                    | O => m0
                    | S p => S (plus p m0)
                    end) 0 m)),
            'b)
           listl
*************************************************)

Walid: Very good points! And if you look carefully at the types that you got back, then you can see that the first way of writing things gets in the way of the application of the fix to the two arguments. And in fact, if you write S m directly in the type, then you also get a simpler type right away, and there is no need for any additional normalization when this type is used.

"mapl" function

The mapl function will take a sized list of type (a n listl) and a function of type (a -> b) as input, and give an output of type (b n listl). The operation is the same as in unsized list. The following code fragment works well:

(*unsized version: *)
let rec map_u f l =
    match l with 
   | [] -> []
    | x::xs -> (f x)::(map_u f xs)
;;

#let rec mapl .|n:'(nat)| (f: 'a -> 'b) (l: ('(n), 'a) listl)
    : (('(n), 'b) listl) =
    match l in ('(n), 'b) listl with
   | Nil -> Nil
   | Cons .|m:'(nat)| (x, xs) ->
     Cons .|'(m)| (f x, mapl .|'(m)| f xs) 
;;
(***************************************************
val mapl :
  (forall n:'(nat) . ('a -> 'b) -> ('(n), 'a) listl -> ('(n), 'b) listl) =
  <forall>
*************************************************)

"zipl" function

The zip function will take two sized lists of type (a n listl) and the same length as input, and outputs also a length "n" sized list, with its list elements are pairs of elements from each input list. This function appears in the tutorial and paper and also be discussed in class, thus there is no difficulty to write it correctly:

(*unsized version: *)
exception UNSIZED_EXN;;
let rec zip_u l1 l2 = match l1 with
   | [] -> (match l2 with | [] -> []
                | y::ys -> raise UNSIZED_EXN)
   | x::xs -> (match l2 with | [] -> raise UNSIZED_EXN
                | y::ys -> (x,y)::(zip_u xs ys))
;;

#let rec zipl .|n:'(nat)| (l1: ('(n), 'a) listl) (l2:('(n), 'b) listl)
    : (('(n), ('a * 'b)) listl) =
match l1 in ('(n), 'a * 'b) listl with 
    | Nil -> (match l2 in ('(n), 'a * 'b) listl with
                | Nil -> Nil)
    |  Cons .|i:'(nat)| (x, xs) -> (match l2 in ('(n), 'a * 'b) listl with
                | Cons .|j:'(nat)| (y, ys)  -> Cons .|'(j)| ((x,y), zipl .|'(i)| xs ys))
;;

(*the one defined in the paper "Indexed type now!"*)
let rec zipl .|n:'(nat)| (l1: ('(n), 'a) listl) (l2:('(n), 'b) listl)
    : (('(n), ('a * 'b)) listl) =
match (l1, l2) in ('(n), 'a * 'b) listl with 
    | Nil, Nil -> Nil
    | Cons .|i:'(nat)| (x, xs), Cons .|j:'(nat)| (y, ys) ->
      Cons .|'(j)| ((x,y), zipl .|'(i)| xs ys)
;;
(***************************************************
val zipl :
  (forall n:'(nat) .
      ('(n), 'a) listl -> ('(n), 'b) listl -> ('(n), 'a * 'b) listl) =
  <forall>
*************************************************)

"appl" function

(*unsized version: *)
let rec app_u l1 l2 =
    match l1 with 
   | [] -> l2
   | x::xs -> x::(app_u xs l2)
;;

let rec appl .|m:'(nat), n:'(nat)| (l1: ('(m), _) listl) (l2: ('(n), _) listl)
    : ('(m+n), _) listl =
   match l1 as ('i: '(nat), 'a: '(OCamlType)) listl 
     in ('(i+n), '(a)) listl with
   | Nil -> l2
   | Cons .|m2:'(nat)| (x, xs) ->
     Cons .|'(m2+n)| (x, appl .|'(m2), '(n)| xs l2)
;;
(***************************************************
val appl :
  (forall m:'(nat) , n:'(nat) .
      ('(m), 'a) listl -> ('(n), 'b) listl -> ('(m + n), 'a) listl) =
  <forall>
*************************************************)

"size_it" function

This function will take an unsized list and gives a sized list. Things become much more tricky because the type of this function should be:

size_it: 'a list -> exists n. ('a '(n)) listl

But so far we don't know how to write existential qualifiers in concoqtion. Here is a trick to encode an existential:

type 'a exist_size = EX of let 'n:'(nat) in (('(n), 'a) listl);;
(***************************************************
type 'a:'(OCamlType) exist_size =
    EX of  let 'n:'(nat)  in  ('(n), 'a) listl : 'a exist_size
*************************************************)

Now we can use this type definition of ('a exist_size) to construct our function "size_it". However, when I first time to try it, I failed. Here is the old code fragment and error message I got:

#let rec size_it (l: 'a list) : ('a exist_size) =
    match l as ('a list) in ('a exist_size) with
   | [] -> EX .|'(0)| (Nil)
   | x::xs -> let xsl = (size_it xs) in
      (match xsl with | EX .|m:'(nat)| y -> EX .|'(m)| (Cons .|'(m)| (x, y)));;
(***************************************************
Coq error in escaped type:
At location 1-2:
Error: The reference m was not found in the current environment
*************************************************)

Fortunatly, after another class on Friday, Prof. Taha clarified that, in concoqtion, when doing pattern matching, one must use "match ... in ..." , otherwise it will do the OCaml match. So I tried again the following code, and now it works:

#let rec size_it (l: 'a list) : ('a exist_size) =
    match l as ('a list) in ('a exist_size) with
   | [] -> EX .|'(0)| (Nil)
   | x::xs -> let xsl = (size_it xs) in
      (match xsl as 'a exist_size in 'a exist_size 
         with | EX .|m:'(nat)| y -> EX .|'(1+m)| (Cons .|'(m)| (x, y)));;
(***************************************************
 val size_it : 'a list -> 'a exist_size = <fun>
*************************************************)

"at_size" function

This function will take an unsized list and an integer n as input and returns a sized list with length n as an output. The n elements in the output should be the first n elements in the input list. If n greater than the length of the unsized list, what should we do? Here, we need a trick to model this exception. One thing we can use is "option" type, which has the following definition:

#type 'a option = 
      | None
      | Some of 'a ;;
(***************************************************
type 'a:'(OCamlType) option = None:'a option | Some of   'a : 'a option
*************************************************)

With this type I wrote the function like this, and it was compiled correctly.

(*unsized version: *)
let rec at_size_u l n = 
    match l with 
   | [] -> (if (n = 0) then [] else (raise UNSIZED_EXN))
   | x::xs -> x::(at_size_u xs n-1)
;;


#let rec at_size (l: 'a list) (n: int) : ('a exist_size) option =
    match (l, n) as ('a list * int) in ('a exist_size) option with
   | (_, 0) -> Some (EX .|'(0)| Nil)
   | ([], m) -> None
   | (x::xs, m) -> let ls = at_size xs (n-1) in
   (match ls as ('a exist_size) option in ('a exist_size) option with
   | None -> None
   | Some (EX .|k:'(nat)| y) -> Some (EX .|'(1+k)| (Cons .|'(k)| (x, y)))
   );;
(***************************************************
val at_size : 'a list -> int -> 'a exist_size option = <fun>
*************************************************)

"mk_snat"

Before doing "at_size" successfully, I also failed a couple of times. During the first attempt, I tried to write a "mk_snat" function first, and see if it will be useful in defining "at_size". The "mk_snat" function will take an integer and return a corresponding snat. I first difine ('(n) snat) as follows:

#type ('n: '(nat)) snat =
      | Zero : '(0) snat
      | Succ of let 'm:'(nat) in '(m) snat: '(1+m) snat;;
(***************************************************
type 'a:'(nat) snat =
    Zero:'(0) snat
  | Succ of  let 'm:'(nat)  in  '(m) snat :
           '(S
               ((fix plus (n m0 : nat) {struct n} : nat :=
                   match n with
                   | O => m0
                   | S p => S (plus p m0)
                   end) 0 m))
           snat
*************************************************)

Then I wrote up the "mk_snat" function with the same trick as I did in "size_it":

#type exist_snat = E of let 'n:'(nat) in '(n) snat;;

let rec mk_snat (n: int) : exist_snat = 
    match n in exist_snat with
   | 0 -> E .|'(0)| Zero 
   | _ -> let nx = mk_snat (n-1) in 
      (match nx in exist_snat with 
         | E .|m:'(nat)| y -> E .|'(1+m)| (Succ .|'(m)| y))
;;
(***************************************************
val mk_snat : int -> exist_snat = <fun>
*************************************************)

It works correctly, but it turns out I wrote the "at_size" without the help of this function. However, I'd like to keep it here.

Walid: Very good! It makes sense that one can "generate the existential" either when we create exists number or exists list(number), and that both are very similar.

Compare the running time of functions on "sized list" and "unsized list"

WALID:

The main comment that I have for everyone at this point is that you will want to post on your page both the code for timing and the actual results that you get back from your machine. In addition, it is always a good idea to print out information about your particular machine. For an example of the kind of information that is usefult to record, I suggest that you look at examples

My first guess on the efficiency of functions on sized_list and unsized_list is that: the sized list is too verbose thus might need more time to excute those functions. But it turned out I was wrong. I run a group of experiments as follows and the results show clearly that operation on sized lists are faster.

The reason it happens is because for sized list, all constraints are checked at compile time, while the unsized_list requires some run-time checking.

To measure the running time, their is a useful OCaml library we can use. Which is called "Trx" and can be used like this:

Trx.init_times ();;

Trx.timenew "Normal_add" (fun () -> 3+2);;
Trx.timenew "Sized_mult"  (fun () -> 3*2);;

Trx.print_times ();;

Experiment

Following are some function definitions for unsized list:

let l1 = [0;1;2;3;4;5;6;7;8;9];;
let ll1 = Cons .|'(9)| (0,  Cons .|'(8)| (1,  Cons .|'(7)| (2,  Cons .|'(6)| (3,  

Cons .|'(5)| (4,  Cons .|'(4)| (5,  Cons .|'(3)| (6,  

Cons .|'(2)| (7,  Cons .|'(1)| (8,  Cons .|'(0)| (9, Nil))))))))));;

let add x = x + x;;
let square x = x * x;;

let id l = l;;

10E-6sec	UnSized (10s)	Sized(10s)	UseLib(10s)	UnSized (100s)	Sized(100s)	UseLib(100s)	UnSized (1000s)	Sized(1000s)	UseLib(1000s)
id	0.7203	0.7003	-	3.7354	3.6606	-	33.240	33.308	-
map_add	6.1063	6.2078	6.9346	9.3380	9.0603	1.0143	38.941	38.975	40.058
map_square	6.1979	6.2173	6.9676	9.4013	9.2413	1.0287	38.914	39.012	40.141
zip	6.4581	6.4846	-	9.5383	9.2793	-	39.549	39.526	-
append	4.5822	4.5851	5.0980	7.5873	7.7518	8.0747	37.401	37.885	38.412
size_it	5.0542	-	-	8.0902	-	-	37.338	-	-
at_size	4.9039	4.4709	-	7.9354	7.4997	-	37.238	36.640	-

Conclusions on performance

• General Performance: Unsized > Sized > Use Lib;
• Exceptional ones: for function "zip" and "at_size", Sized list runs fast than unsized one.

Walid: Do these conclusions need to be revised based on our discussions?