HOCA

HOCA is an abbreviation for Higher-Order Complexity Analysis, and is meant as a laboratory for the automated complexity analysis of higher-order functional programs. Currently, HOCA consists of one executable pcf2trs which translates a pure subset of OCaml to term rewrite systems, in a complexity reflecting manner.

$ cat examples/rev-dl.fp 

(* type 'a list = Nil | Cons of 'a * 'a list *)

let comp f g x = f (g x) ;;

let rev l =
  (* walk :: 'a list -> ('a list -> 'a list) *)
  let rec walk xs = 
    match xs with 
    | Nil -> (fun x -> x)
    | Cons(x,xs') -> comp (walk xs') (fun ys -> Cons(x,ys))
  in walk l Nil ;;  

$ pcf2trs examples/rev-dl.fp 

(STRATEGY INNERMOST)
(VAR x4 x3 x7 x9 x8 x12 x5)
(RULES
  walk#1(Nil()) -> walk_xs()
  walk#1(Cons(x4,x3)) -> comp_f_g(walk#1(x3),walk_xs_3(x4))
  comp_f_g#1(comp_f_g(x7,x9),walk_xs_3(x8),x12) -> 
     comp_f_g#1(x7,x9,Cons(x8,x12))
  comp_f_g#1(walk_xs(),walk_xs_3(x8),x12) -> Cons(x8,x12)
  main(Nil()) -> Nil()
  main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil()))

What is happening here?

• As a first step, HOCA desugars the given program to a variation of Plotkin's PCF with data-constructors;
• Via Reynold's defunctionalization, the PCF program is turned into an applicative term rewrite systems (ATRS for short); call-by-value reductions of the PCF program are simulated by the ATRS step-by-step;
• on the ATRS, various complexity reflecting transformations are performed: inlining, dead-code-elminiation, instantiation of higher-order variables through a call-flow-analysis and finally uncurrying. This results finally in a first-order rewrite system, whose runtime-complexity reflects the complexity of the initial program, asymptotically.

Download

You can download the latest stable release here. Compilation requires GHC, Version 7.10 or above and cabal.
The development version of HOCA is hosted on GitHub. The development version depends additionally on the term-rewriting-applicative library as well as the development version of the term-rewriting library.

Experiments

We conducted preliminary experiments on the examples collected sofar, using TcT and TTT2 on systems obtained from HOCA. The examples are contained in the source distribution..

Contact

e-mail: (λxy.martinyavanzinixuibkyacyat) @ .