HOCAHOCA 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
pcf2trswhich translates a pure subset of OCaml to term rewrite systems, in a complexity reflecting manner.
What is happening here?
$ 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()))
- 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.
DownloadYou 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.
ExperimentsWe 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..