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?
• 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.

e-mail: `(λxy.`martin`y`avanzini`x`uibk`y`ac`y`at`)` @ .