Computation with Bounded Resources
Research Group

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?

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) @ .