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 executablepcf2trs
which 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.
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.
martiny
avanzinix
uibky
acy
at)
@ .