A Transformational Approach to Resource Analysis with Typed-norms Inference

TL;DR

This paper introduces a transformational, data-flow analysis-based method for automatically inferring typed-norms to estimate program resource consumption across various programming paradigms, demonstrating efficiency and accuracy on benchmarks.

Contribution

It presents a novel transformational approach to resource analysis using inferred typed-norms via data-flow analysis, applicable to multiple programming paradigms.

Findings

Efficient and accurate analysis on standard benchmarks.

Applicable across functional, logic, and imperative paradigms.

Formalized on a simple rule-based representation.

Abstract

In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program's execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice. Under consideration in Theory and Practice of Logic Programming (TPLP).

Equations

$$\begin{array}[]{lll}P&::=&[\overline{\mathit{Dd}}]~{}\overline{\mathit{Proc}}\\ \mathit{Proc}&::=&p::T_{1}\times\cdots\times T_{k}~{}\overline{r}\\ r&::=&p(\bar{x},\bar{y})\leftarrow g,b_{1},\ldots,b_{n}\\ b&::=&{x}{:}{=}{t}\mid\ p(\bar{x},\bar{y})\\ g&::=&{\it true}\mid g\wedge g\mid e>e\mid e=e\mid e\geq e\mid{\it match}(x,p)\mid{\it nonmatch}(x,p)\\ p&::=&\mathit{Co}(\bar{x})\\ t&::=&{\it e}\mid\mathit{Co}(\bar{t})\\ {\it e}&::=&x\mid n\mid{\it e}{+}{\it e}\mid{\it e}{-}{\it e}\\ \end{array}$$

$$\begin{array}[]{l@{}l}\it C_{0}\equiv&\langle\mbox{main},\underline{\mbox{l${}_{0}$:=Cons(2, Nil)}}\cdot\mbox{factSum($\langle$l${}_{0}$$

\rangle$,$\langle$r^{\prime }${}_{0}

$$\rangle$)},\epsilon\rangle\leadsto^{(1)\cdot\epsilon}\\ \it C_{1}\equiv&\langle\mbox{main},\underline{\mbox{factSum($\langle$l${}_{0}$$

\rangle$,$\langle$r^{\prime }${}_{0}

$$\rangle$)}},[\mbox{l${}_{0}$}\mapsto\mbox{Cons(2, Nil)}]\rangle\leadsto^{(2)\cdot 4}\\ \it C_{2}\equiv&\langle\mbox{factSum},\underline{\mbox{sum${}_{2}$:=0}}\cdot\mbox{while\_1($\langle$l${}_{2}$, sum${}_{2}$$

\rangle$,$\langle$su{m}^{\prime }${}_{2}

$$\rangle$)},[\mbox{l${}_{2}$}\mapsto\mbox{Cons(2, Nil)}]\rangle\cdot\\ &\langle\mbox{main}[\mbox{sum'${}_{2}$}\sim\mbox{r'${}_{0}$}],\epsilon,[\mbox{l${}_{0}$}\mapsto\mbox{Cons(2, Nil)}]\rangle\leadsto^{(1)\cdot\epsilon}\\ \it C_{3}\equiv&\langle\mbox{factSum},\underline{\mbox{while\_1($\langle$l${}_{2}$, sum${}_{2}$$

\rangle$,$\langle$su{m}^{\prime }${}_{2}

$$\rangle$)}},[\mbox{l${}_{2}$}\mapsto\mbox{Cons(2, Nil)},\mbox{sum${}_{2}$}\mapsto 0]\rangle\cdot\\ &\langle\mbox{main}[\mbox{sum'${}_{2}$}\sim\mbox{r'${}_{0}$}],\epsilon,[\mbox{l${}_{0}$}\mapsto\mbox{Cons(2, Nil)}]\rangle\leadsto^{(2)\cdot 6}\\ \it C_{4}\equiv&\langle\mbox{while\_1},\underline{\mbox{fact($\langle$e${}_{4}$$

\rangle$,$\langle$prod${}_{4}

$$\rangle$)}}\cdots\mbox{while\_1($\langle$l1${}_{4}$,sum${}_{4}$$

\rangle$,$\langle$su{m}^{\prime }${}_{4}

$$\rangle$)},[\mbox{l${}_{4}$}\mapsto\mbox{Cons(2, Nil)},\\ &~{}~{}~{}\mbox{sum${}_{4}$}\mapsto 0,\mbox{e${}_{4}$}\mapsto 2,\mbox{l1${}_{4}$}\mapsto\mbox{Nil}]\rangle\cdot\\ &\langle\mbox{factSum}[\mbox{sum'${}_{4}$}\sim\mbox{sum'${}_{2}$}],\epsilon,[\mbox{l${}_{2}$}\mapsto\mbox{Cons(2, Nil)},\mbox{sum${}_{2}$}\mapsto 0]\rangle\cdot\\ &\langle\mbox{main}[\mbox{sum'${}_{2}$}\sim\mbox{r'${}_{0}$}],\epsilon,[\mbox{l${}_{0}$}\mapsto\mbox{Cons(2, Nil)}]\rangle\leadsto^{*}\\ \it C_{5}\equiv&\langle\mbox{while\_1},\underline{\epsilon},[\mbox{l${}_{4}$}\mapsto\mbox{Cons(2, Nil)},\mbox{sum${}_{4}$}\mapsto 0,\mbox{e${}_{4}$}\mapsto 2,\mbox{l1${}_{4}$}\mapsto\mbox{Nil},\mbox{sum'${}_{4}$}\mapsto 2]\rangle\cdot\\ &\langle\mbox{factSum}[\mbox{sum'${}_{4}$}\sim\mbox{sum'${}_{2}$}],\epsilon,[\mbox{l${}_{2}$}\mapsto\mbox{Cons(2, Nil)},\mbox{sum${}_{2}$}\mapsto 0]\rangle\cdot\\ &\langle\mbox{main}[\mbox{sum'${}_{2}$}\sim\mbox{r'${}_{0}$}],\epsilon,[\mbox{l${}_{0}$}\mapsto\mbox{Cons(2, Nil)}]\rangle\leadsto^{(3)\cdot\epsilon}\\ \it C_{6}\equiv&\langle\mbox{factSum},\underline{\epsilon},[\mbox{l${}_{2}$}\mapsto\mbox{Cons(2, Nil)},\mbox{sum${}_{2}$}\mapsto 0,\mbox{sum'${}_{2}$}\mapsto 2]\rangle\cdot\\ &\langle\mbox{main}[\mbox{sum'${}_{2}$}\sim\mbox{r'${}_{0}$}],\epsilon,[\mbox{l${}_{0}$}\mapsto\mbox{Cons(2, Nil)}]\rangle\leadsto^{(3)\cdot\epsilon}\\ \it C_{7}\equiv&\langle\mbox{main},\epsilon,[\mbox{l${}_{0}$}\mapsto\mbox{Cons(2, Nil)},\mbox{r'${}_{0}$}\mapsto 2]\rangle\\ \end{array}$$

$$\parallel t{\parallel }_T^{+}=\{\begin{array}{ll}t& \text{mbox}ifT={\mathtt{Int}}^{+}\text{mbox}andtype(t)={\mathtt{Int}}^{+}\\ 0& \text{mbox}ifT\ne {\mathtt{Int}}^{+}\text{mbox}andtype(t)={\mathtt{Int}}^{+}\\ 1+{\sum }_{i=1}^n\parallel t_i{\parallel }_T^{+}& \text{mbox}ift=Co(t_1,\dots ,t_n)\text{mbox}andtype(t)=T\\ {\sum }_{i=1}^n\parallel t_i{\parallel }_T^{+}& \text{mbox}ift=Co(t_1,\dots ,t_n)\text{mbox}andtype(t)\ne T\end{array}$$

$$\parallel t{\parallel }_T=\{\begin{array}{ll}t& \text{mbox}ifT=\mathtt{Int}\text{mbox}andtype(t)=\mathtt{Int}\\ 0& \text{mbox}ifT\ne \mathtt{Int}\text{mbox}andtype(t)=\mathtt{Int}\\ 1+{\sum }_{i=1}^n\parallel t_i{\parallel }_T& \text{mbox}ift=Co(t_1,\dots ,t_n)\text{mbox}andtype(t)=T\\ {max}_{i=1}^n\parallel t_i{\parallel }_T& \text{mbox}ift=Co(t_1,\dots ,t_n)\text{mbox}andtype(t)\ne T\end{array}$$

$$\parallel t{\parallel }_T=\{\begin{array}{ll}{X}_T& \text{mbox}ift\equiv x\text{mbox}andT\in Constituents(type(x))\\ -\infty & \text{mbox}ift\equiv x,T=\text{mbox}Int\text{mbox}and\text{mbox}Int\notin Constituents(type(x))\\ n& \text{mbox}ift\equiv n\text{mbox}andT=\mathtt{Int}\\ \parallel e_1{\parallel }_T\pm \parallel e_2{\parallel }_T& \text{mbox}ift\equiv e_1\pm e_2\text{mbox}andT=\mathtt{Int}\\ 1+{\sum }_{i=1}^n\parallel t_i{\parallel }_T& \text{mbox}ift=Co(t_1,\dots ,t_n)\text{mbox}andtype(t)=T\\ {max}_{i=1}^n\parallel t_i{\parallel }_T& \text{mbox}ift=Co(t_1,\dots ,t_n)\text{mbox}andtype(t)\ne T\\ 0& \text{mbox}inothercase\end{array}$$

$$non\_neg(S)=\bigwedge \{X_T\ge 0|x\in S,T\in rtypes(x),T\ne \mathtt{Int}\}$$

$$\begin{array}[]{l@{}l}\mathit{AC}_{0}\equiv&\langle\underline{L^{0}_{\mathtt{Int}}=2\wedge L^{0}_{\mathtt{IntList}}=2}\cdot\mbox{factSum}(\langle L^{0}_{\mathtt{Int}},L^{0}_{\mathtt{IntList}}\rangle,\langle R^{\prime 0}_{\mathtt{Int}}\rangle)\rangle~{}|~{}L^{0}_{\mathtt{IntList}}\geq 0\leadsto_{\alpha}^{(1)\cdot\epsilon}\\ \mathit{AC}_{1}\equiv&\langle\underline{\mbox{factSum}(\langle L^{0}_{\mathtt{Int}},L^{0}_{\mathtt{IntList}}\rangle,\langle R^{\prime 0}_{\mathtt{Int}}\rangle)}\rangle~{}|~{}L^{0}_{\mathtt{IntList}}\geq 0\land L^{0}_{\mathtt{Int}}=2\wedge L^{0}_{\mathtt{IntList}}=2\leadsto_{\alpha}^{(2)\cdot 4}\\ \mathit{AC}_{2}\equiv&\langle\underline{\mathit{Sum}^{2}_{\mathtt{Int}}=0}\cdot\mbox{while}\_1(\langle L^{2}_{\mathtt{Int}},L^{2}_{\mathtt{IntList}},\mathit{Sum}^{2}_{\mathtt{Int}}\rangle,\langle\mathit{Sum}^{\prime 2}_{\mathtt{Int}}\rangle)\rangle^{R^{\prime 0}_{\mathtt{Int}}=\mathit{Sum}^{\prime 2}_{\mathtt{Int}}}~{}\cdot\\ &\langle\epsilon\rangle~{}|~{}\psi_{1}\land L^{0}_{\mathtt{Int}}=L^{2}_{\mathtt{Int}}\wedge L^{0}_{\mathtt{IntList}}=L^{2}_{\mathtt{IntList}}\wedge L^{2}_{\mathtt{IntList}}\geq 0\cbstart\leadsto_{\alpha}^{(1)\cdot\epsilon}\cbend\\ \mathit{AC}_{3}\equiv&\langle\underline{\mbox{while}\_1(\langle L^{2}_{\mathtt{Int}},L^{2}_{\mathtt{IntList}},\mathit{Sum}^{2}_{\mathtt{Int}}\rangle,\langle\mathit{Sum}^{\prime 2}_{\mathtt{Int}}\rangle)}\rangle^{R^{\prime 0}_{\mathtt{Int}}=\mathit{Sum}^{\prime 2}_{\mathtt{Int}}}~{}\cdot\\ &\langle\epsilon\rangle~{}|~{}\psi_{2}\land\mathit{Sum}^{2}_{\mathtt{Int}}=0\leadsto_{\alpha}^{(2)\cdot 6}\\ \mathit{AC}_{4}\equiv&\langle\underline{\mbox{fact}(\langle E^{4}_{\mathtt{Int}}\rangle,\langle Prod^{4}_{\mathtt{Int}}\rangle)}\cdots\rangle^{\mathit{Sum}^{\prime 2}_{\mathtt{Int}}=\mathit{Sum}^{\prime 4}_{\mathtt{Int}}}~{}\cdot\\ &\langle\epsilon\rangle^{R^{\prime 0}_{\mathtt{Int}}=\mathit{Sum}^{\prime 2}_{\mathtt{Int}}}~{}\cdot\\ &\langle\epsilon\rangle~{}|~{}\psi_{3}\land L^{2}_{\mathtt{Int}}=L^{4}_{\mathtt{Int}}\wedge L^{2}_{\mathtt{IntList}}=L^{4}_{\mathtt{IntList}}\wedge\mathit{Sum}^{2}_{\mathtt{Int}}=\mathit{Sum}^{4}_{\mathtt{Int}}\wedge\\ &L^{4}_{\mathtt{Int}}=\max(E^{4}_{\mathtt{Int}},L1^{4}_{\mathtt{Int}})\wedge L^{4}_{\mathtt{IntList}}=1+L1^{4}_{\mathtt{IntList}}\wedge\\ &L^{4}_{\mathtt{IntList}}\geq 0\wedge L1^{4}_{\mathtt{IntList}}\geq 0\leadsto_{\alpha}^{*}\\ \mathit{AC}_{5}\equiv&\langle\underline{\epsilon}\rangle^{\mathit{Sum}^{\prime 2}_{\mathtt{Int}}=\mathit{Sum}^{\prime 4}_{\mathtt{Int}}}\cdot\\ &\langle\epsilon\rangle^{R^{\prime 0}_{\mathtt{Int}}=\mathit{Sum}^{\prime 2}_{\mathtt{Int}}}~{}\cdot\\ &\langle\epsilon\rangle~{}|~{}\psi_{5}\leadsto_{\alpha}^{(3)\cdot\epsilon}\\ \mathit{AC}_{6}\equiv&\langle\underline{\epsilon}\rangle^{R^{\prime 0}_{\mathtt{Int}}=\mathit{Sum}^{\prime 2}_{\mathtt{Int}}}~{}\cdot\\ &\langle\epsilon\rangle~{}|~{}\psi_{5}\land\mathit{Sum}^{\prime 2}_{\mathtt{Int}}=\mathit{Sum}^{\prime 4}_{\mathtt{Int}}\leadsto_{\alpha}^{(3)\cdot\epsilon}\\ \mathit{AC}_{7}\equiv&\langle\epsilon\rangle~{}|~{}\psi_{6}\land R^{\prime 0}_{\mathtt{Int}}=\mathit{Sum}^{\prime 2}_{\mathtt{Int}}\\ \end{array}$$

$$(\mu\oplus\mu^{\prime})(x)=\left\{\begin{array}[]{rl}\mu(x)\cup\mu^{\prime}(x)&\text{if }x\in\mathit{dom}(\mu)\cap\mathit{dom}(\mu^{\prime})\\ \mu(x)&\text{if }x\in\mathit{dom}(\mu)\smallsetminus\mathit{dom}(\mu^{\prime})\\ \mu^{\prime}(x)&\text{if }x\in\mathit{dom}(\mu^{\prime})\smallsetminus\mathit{dom}(\mu)\\ \text{undefined}&i.o.c.\end{array}\right.$$

$$⟨{\mu }_1,\dots ,{\mu }_n⟩\oplus ⟨{\mu }_1^{\prime },\dots ,{\mu }_n^{\prime }⟩=⟨{\mu }_1\oplus {\mu }_1^{\prime },\dots ,{\mu }_n\oplus {\mu }_n^{\prime }⟩$$

$$({\mu}|_{C})(x)=\left\{\begin{array}[]{rl}\mu(x)&\text{if }x\in C\\ \text{undefined}&i.o.c.\end{array}\right.$$

$$({\mu}_{{\bar{x}}\sim{\bar{y}}})(z)=\left\{\begin{array}[]{rl}\mu(x_{i})&\text{if }z=y_{i}\\ \mu(z)&\text{if }z\in\mathit{dom}(\mu)\smallsetminus\{\bar{x}\}\\ \text{undefined}&i.o.c.\end{array}\right.$$

$$\begin{array}[]{rcl}\mu_{1}&=&[x\mapsto\{\mbox{Int}\},y\mapsto\{\mbox{Int},\mbox{IntList}\}]\\ \mu_{2}&=&[y\mapsto\{\mbox{IntList}\}]\\ \mu_{3}&=&[y\mapsto\{\mbox{Int}\}]\end{array}$$

$$\begin{array}[]{rrl}\mathit{gen}^{P{}}&:&\Sigma^{P{}}\mapsto\Sigma^{P{}}\\ \mathit{gen}^{P{}}(\sigma)&=&\sigma\oplus\bigoplus_{i=1}^{n}\mathit{gen}^{P{}}_{i}(\sigma)\\ \end{array}$$

$$\begin{array}[]{rrl}\mathit{gen}^{P{}}_{i}&:&\Sigma^{P{}}\mapsto\Sigma^{P{}}\\ \mathit{gen}^{P{}}_{i}(\sigma)&=&\langle{\mathit{genG}^{P{}}_{i}(g,\sigma)}\rangle^{n}_{i}\oplus\mathit{genS}^{P{}}_{i}(\{\bar{b}\},\sigma)\oplus\langle{\mu_{i}}\rangle^{n}_{i},\text{ where }\\ &&~{}~{}{P{}}^{i}=p(\bar{x},\bar{y})\leftarrow g,\bar{b},~{}~{}~{}\mu_{i}=\bigoplus_{\mu\in S_{i}}\mu\text{~{}and}\\ &&~{}~{}S_{i}=\{{({\sigma(j)}|_{\bar{w}\bar{z}})}_{{\bar{w}\bar{z}}\sim{\bar{x}\bar{y}}}\mid j\in[1..n],{P{}}^{j}=p(\bar{w},\bar{z})\leftarrow g^{\prime},\bar{b^{\prime}}\}\end{array}$$

$$\begin{array}[]{rrl}\mathit{genG}^{P{}}_{i}&:&\text{Guard}\times\Sigma^{P{}}\mapsto M\\ \mathit{genG}^{P{}}_{i}({\it true},\sigma)&=&\epsilon\\ \mathit{genG}^{P{}}_{i}(g_{1}\wedge g_{2},\sigma)&=&\mathit{genG}^{P{}}_{i}(g_{1},\sigma)\oplus\mathit{genG}^{P{}}_{i}(g_{2},\sigma)\\ \mathit{genG}^{P{}}_{i}(e_{1}~{}op~{}e_{2},\sigma)&=&[x\mapsto\{\mathtt{Int}\}\mid x\in\mathit{vars}(e_{1})\cup\mathit{vars}(e_{2})]\\ \mathit{genG}^{P{}}_{i}({\it match}(x,p),\sigma)&=&[x\mapsto\{T\}\mid T=\mathit{type}_{i}(x),T\text{ is recursive}]~{}\oplus\\ &&[x\mapsto\{T\mid y\in\mathit{vars}(p),~{}T\in\sigma(i)(y)\}]\\ \mathit{genG}^{P{}}_{i}({\it nonmatch}(x,p),\sigma)&=&[x\mapsto\{T\mid y\in\mathit{vars}(p),~{}T\in\sigma(i)(y)\}]\\ \end{array}$$

$$\begin{array}[]{rrl}\mathit{genS}^{P{}}_{i}&:&P(\text{Statement})\times\Sigma^{P{}}\mapsto\Sigma^{P{}}\\ \mathit{genS}^{P{}}_{i}(\{\bar{b}\},\sigma)&=&\bigoplus_{b\in\{\bar{b}\}}\mathit{genS}^{P{}}_{i}(b,\sigma)\\ \end{array}$$

$$\begin{array}[]{rrl}\mathit{genS}^{P{}}_{i}&:&\text{Statement}\times\Sigma^{P{}}\mapsto\Sigma^{P{}}\\ \mathit{genS}^{P{}}_{i}({x}{:}{=}{t},\sigma)&=&\langle{[y\mapsto T_{x,y,i}\mid y\in\mathit{vars}(t)]}\rangle^{n}_{i},\text{ where }\\ &&\cbstart~{}~{}T_{x,y,i}=\{T\mid T\in\sigma(i)(x)\cap\mathit{Constituents}({\mathit{type}_{i}(y)})\}\cbend\\ \mathit{genS}^{P{}}_{i}(p(\bar{x},\bar{y}),\sigma)&=&\bigoplus_{\sigma\in A\cup B}\sigma,\text{ where }\\ &&~{}~{}A=\{\langle{{({\sigma(j)}|_{\bar{w}})}_{{\bar{w}}\sim{\bar{x}}}}\rangle^{n}_{i}\mid j\in[1..n],{P{}}^{j}=p(\bar{w},\bar{z})\leftarrow g,\bar{b}\}\\ &&~{}~{}B=\{\langle{{({\sigma(i)}|_{\bar{y}})}_{{\bar{y}}\sim{\bar{z}}}}\rangle^{n}_{j}\mid j\in[1..n],{P{}}^{j}=p(\bar{w},\bar{z})\leftarrow g,\bar{b}\}\end{array}$$

$$\begin{array}[]{lll}\mathit{Proc}&::=&p\langle\Gamma\rangle::T(\Gamma)\times\cdots\times T(\Gamma)~{}\overline{r}\\ \end{array}$$

$$\parallel t{\parallel }_{(T,A)}^{\Lambda }=\{\begin{array}{ll}{X}_{(T,A)}& \text{mbox}ift\equiv x\text{mbox}and(T,A)\in Constituents(type(x))\\ -\infty & \text{mbox}ift\equiv x,T=\text{mbox}Int\text{mbox}and(\text{mbox}Int,A)\notin Constituents(type(x))\\ n& \text{mbox}ift\equiv n\text{mbox}andT=\mathtt{Int}\\ \parallel e_1{\parallel }_{(T,A)}^{\Lambda }\pm \parallel e_2{\parallel }_{(T,A)}^{\Lambda }& \text{mbox}ift\equiv e_1\pm e_2\text{mbox}andT=\mathtt{Int}\\ 1+{\sum }_{i=1}^n\parallel t_i{\parallel }_{(T,A)}^{\Lambda }& \text{mbox}ift=Co(t_1,\dots ,t_n)\text{mbox}andtype(t)=T\\ {max}_{i=1}^n\parallel t_i{\parallel }_{(T,A)}^{\Lambda }& \text{mbox}ift=Co(t_1,\dots ,t_n)\text{mbox}andtype(t)\ne T\\ 0& \text{mbox}inothercase\end{array}$$

$$\parallel t{\parallel }_{(T,A)}^{(Co,i)\cdot rest}=\{\begin{array}{ll}\parallel t_i{\parallel }_{(T,A)}^{rest}& \text{mbox}ift=Co(t_1,\dots ,t_n)\\ -\infty & \text{mbox}ift\ne Co(t_1,\dots ,t_n)\text{mbox}andT=\text{mbox}Int\\ 0& \text{mbox}inothercase\end{array}$$

$$eva{l}_t(t,lv)=\{\begin{array}{ll}lv(x)& ift\equiv x,x\in dom(lv)\\ n& ift\equiv n\\ eva{l}_t(e_1,lv)+eva{l}_t(e_2,lv)& ift\equiv e_1+e_2\\ eva{l}_t(e_1,lv)-eva{l}_t(e_2,lv)& ift\equiv e_1-e_2\\ Co(\overline{eva{l}_t(t_n,lv)})& ift\equiv Co(\overline{t_n})\\ undefined& i.o.c\end{array}$$

$$eva{l}_g(g,lv)=\{\begin{array}{ll}ϵ& ifg\equiv true\\ l{v}_1\uplus l{v}_2& ifg\equiv g_1\wedge g_2,eva{l}_g(g_1,lv)=l{v}_1,\\ & eva{l}_g(g_2,lv\uplus l{v}_1)=l{v}_2\\ ϵ& ifg\equiv e_1\mathtt{op}{e}_2,\mathtt{op}\in \{>,=,\ge \},\\ & eva{l}_t(e_1,lv)=n_1,eva{l}_t(e_2,lv)=n_2,n_1\mathtt{op}{n}_2\\ l{v}^{\prime }& ift\equiv match(x,p),\exists l{v}^{\prime }\in \mathcal{L}\mathcal{V}s.t.l{v}^{\prime }(p)=lv(x),\\ & dom(l{v}^{\prime })=vars(p)\\ ϵ& ift\equiv nonmatch(x,p),\nexists l{v}^{\prime }\in \mathcal{L}\mathcal{V}s.t.l{v}^{\prime }(p)=lv(x),\\ & dom(l{v}^{\prime })=vars(p)\\ undefined& i.o.c\end{array}$$

$$(1)~{}\begin{array}[]{c}\varphi_{1}{\wedge}\psi_{n-1}\not\models{\mathord{\mathit{false}}}\\ \hline\cr\langle\varphi_{1}\cdot bs^{\alpha}\rangle\cdot ar^{\alpha}|\psi_{n-1}\leadsto_{\alpha}^{(1)\cdot\epsilon}\langle bs^{\alpha}\rangle\cdot ar^{\alpha}|\varphi_{1}{\wedge}\psi_{n-1}\\ \end{array}$$

$$(2)~{}\begin{array}[]{c}b\equiv m(\bar{x},\bar{y})~{}~{}m(\bar{x^{\prime}},\bar{y^{\prime}})\leftarrow g,b_{1}\cdot\cdot\cdot b_{k}\in\it P\mathit{~{}fresh}\\ \it lv_{1}\equiv[\overline{x^{\prime}\mapsto\it lv(x)}]~{}~{}eval_{g}(g,\it lv_{1})=\it lv_{2}\par\\ \hline\cr\it C_{n-1}\equiv\langle p,b{\cdot}{\it bs},\it lv\rangle{\cdot}\it C\leadsto^{(2)\cdot\mathit{rn}}\langle m,b_{1}\cdot\cdot\cdot b_{k},\it lv_{1}\uplus\it lv_{2}\rangle{\cdot}\langle p[\overline{y^{\prime}\sim y}],{\it bs},\it lv\rangle{\cdot}\it C\equiv\it C_{n}\end{array}$$

$$(2)~{}\begin{array}[]{c}m(\bar{X^{\prime}},\bar{Y^{\prime}})\leftarrow g^{\alpha}~{}|~{}b^{\alpha}_{1},\ldots,b^{\alpha}_{k}\in\it P^{\alpha}\mathit{~{}fresh}~{}~{}~{}~{}~{}~{}\overline{X=X^{\prime}}\wedge\psi_{n-1}{\wedge}g^{\alpha}\not\models{\it false}\\ \hline\cr\langle m(\bar{X},\bar{Y})\cdot bs^{\alpha}\rangle\cdot ar^{\alpha}|\psi_{n-1}\leadsto_{\alpha}^{(2)\cdot\mathit{rn}}\\ \langle b^{\alpha}_{1}\cdots b^{\alpha}_{k}\rangle^{\overline{Y=Y^{\prime}}}\cdot\langle bs^{\alpha}\rangle\cdot ar^{\alpha}|\overline{X=X^{\prime}}\wedge\psi_{n-1}\wedge g^{\alpha}\end{array}$$

$$\begin{array}[]{ll}&(\overline{X=X^{\prime}}\wedge\psi_{n-1}\wedge\widetilde{\psi_{n-1}})\wedge g^{\alpha}\wedge\it lv^{\alpha}_{1}\wedge\it lv^{\alpha}_{2}\not\models{\mathord{\mathit{false}}}\\ =&(\overline{X=X^{\prime}}\wedge g^{\alpha}\wedge\psi_{n-1})\wedge(\it lv^{\alpha}_{1}\wedge\it lv^{\alpha}_{2}\wedge\widetilde{\psi_{n-1}})\not\models{\mathord{\mathit{false}}}\\ =&\psi_{n}\wedge\widetilde{\psi_{n}}\not\models{\mathord{\mathit{false}}}\\ \end{array}$$

$$(3)~{}\begin{array}[]{c}\\ \hline\cr\it C_{n-1}\equiv\langle m,\epsilon,\it lv_{0}\rangle{\cdot}\langle p[\overline{y^{\prime}\sim y}],{\it bs},\it lv\rangle{\cdot}\it C\leadsto^{(3)\cdot\epsilon}\langle p,{\it bs},\it lv[\overline{y\mapsto\it lv_{0}(y^{\prime})}]\rangle{\cdot}\it C\equiv\it C_{n}\end{array}$$

$$(3)\begin{array}[]{c}\psi_{n-1}{\wedge}\overline{Y=Y^{\prime}}\not\models{\it false}\\ \hline\cr\langle\epsilon\rangle^{\overline{Y=Y^{\prime}}}\cdot\langle bs^{\alpha}\rangle\cdot ar^{\alpha}|\psi_{n-1}\leadsto_{\alpha}^{(3)\cdot\epsilon}\langle bs^{\alpha}\rangle\cdot ar^{\alpha}|\psi_{n-1}{\wedge}\overline{Y=Y^{\prime}}\end{array}$$

$$\mathit{dep^{T}({D,g})}=\left\{\begin{array}[]{lll}\mathit{dep^{T}({\mathit{dep^{T}({D,g_{1}})},g_{2}})}&&\mbox{ if }g=g_{1}\land g_{2}\\ D\cup\{{x}\Rightarrow_{T}{y}\mid y\in\mathit{vars}(p),~{}T\preceq\mathit{type}(y)\}\cup&&\mbox{ if }g={\it match}(x,p)\\ ~{}~{}\{{z}\Rightarrow_{T}{y}\mid{z}\Rightarrow_{T}{x}\in D,~{}y\in\mathit{vars}(p),~{}T\preceq\mathit{type}(y)\}\\ D&{}{}{}&\mbox{ otherwise }\\ \end{array}\right.\enspace$$

$$\begin{array}[]{lc}(1)&\begin{array}[]{c}b\equiv{x}{:}{=}{t}~{}~{}eval_{t}(t,\it lv)=v\\ \hline\cr\langle p^{i},b{\cdot}{\it bs},\it lv\rangle{\cdot}\it C\leadsto\langle p^{i},{\it bs},\it lv[x\mapsto v]\rangle{\cdot}\it C\end{array}\end{array}$$

Full text

Under consideration in Theory and Practice of Logic Programming (TPLP).

1 Introduction

Automated resource analysis [Wegbreit (1975)] needs to infer how the sizes of data are modified along program’s execution. Size is measured using so-called norms [Bossi et al. (1991)] which define how the size of a term is computed. Examples of norms are list-length which counts the number of elements of a list, tree-depth which counts the depth of a tree, term-size which counts the number of constructors, etc. Basically, in order to infer the resource consumption of executing a loop that traverses a data-structure, the analyzer tries to infer how the size of such data-structure decreases at each iteration w.r.t. the chosen norm. Given a tree t, using a term-size norm, we infer that a loop like “while (t!=leaf) t=t.right;” performs at most nodes(t) iterations, where function nodes returns the number of nodes in the tree. This is because size analysis infers that at each iteration the instruction t=t.right decreases nodes(t). However, by using the tree-depth norm, we will infer that depth(t) is an upper bound on the number of iterations. The latter is obviously more precise than the former bound as depth(t)$\leq$nodes(t).

The last two decades have witnessed a wealth of research on using norms in termination analysis, especially in the context of logic programming [Bossi et al. (1991), Bruynooghe et al. (2007), Genaim et al. (2002)]. Early work pointed out that the choice of norm affects the precision such that the analyzer may only succeed to prove termination if a certain norm is used, while it cannot prove it with others. Later on, there has been further investigation on applying multiple norms, i.e., using two or more norms by applying them simultaneously [Bossi et al. (1991)]. This means that the same data in the original program is replaced by two or more abstract data each one specifying its size information w.r.t. the corresponding norm. Even a further step has been taken on using typed-norms which allow defining norms based on type information (namely on recursive types) [Bruynooghe et al. (2007)]. Inferring norms from type information makes sense as recursive types represent recursive data-structures and thus, in termination analysis, they identify some potential sources of infinite recursion and, in resource analysis, they might influence the number of iterations that the loops perform. Besides, typed-norms allow that the same term can be measured differently depending on its type. As pointed out in [Genaim et al. (2002)], this is particularly useful when the same function symbol may occur in different type contexts.

In the context of resource analysis, we found early work that already pointed out that the combination of norms affects the precision of lower-bound time analysis [King et al. (1997)]. Sized-types provide a way to consider more than one norm for each type. They have been used in the context of functional [Pedro Vasconcelos (2008), Vasconcelos and Hammond (2003)] and recently in logic programming [Serrano et al. (2013), Serrano et al. (2014)]. In the former case, they are inferred by a type analysis and in the latter via abstract interpretation. In contrast, we propose a transformational approach which provides a simple and accurate way to use multiple typed-norms in resource analysis as follows: (1) we first transform the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms valid for its type, (2) such intermediate program is then transformed into upper and lower resource bounds automatically. As regards the first phase, we formalize the transformation assuming that the input programs are given in a simple rule-based representation. The rule-based representation contains program rules, pattern matching and assignment using a compact syntax. Programs written in \cbstartfirst-order \cbendfunctional or imperative programming languages can be represented by means of this representation in a straightforward way (since this representation can model control-flow graphs with procedure calls). Logic programs can be represented as well by replacing matching (and assignment) by unification, without any further change in our analysis. As regards the second phase, \cbstartnote that we are interested in relying on existing techniques and using them as a black-box without modifying them. This is important since they receive abstract programs that come from different sources, and we do not want to make any change that is particular to our transformation that might break the functionality of other parts. \cbendThus, formalizing our framework focuses only on the first step.

While allowing multiple norms might lead to more accurate bounds than adopting one norm, the efficiency of the analysis can be degraded considerably. This is because the process of finding resource bounds from abstractions that have more arguments (due to the use of multiple norms) is more costly. Thus, an essential aspect for the practical applicability of our method is to obtain the smallest sets for the relevant typed-norms, i.e., eliminate those abstractions that will not lead to further precision. For this purpose, we present a new algorithm for the inference of typed-norms which, by inspecting the program, can detect which norms are useful to later infer the resource consumption, and discard norms that are useless for this purpose. Our inference is formalized as a data-flow analysis which is applied as a pre-process, such that once the relevant norms are inferred, the transformation into the abstract program is carried out w.r.t. the inferred norms.

1.1 Summary of Contributions

The main contributions of this article can be summarized as follows:

We introduce a transformation from the rule-based representation to an abstract representation in which each variable is abstracted with respect to all considered norms valid for its type, and prove soundness of the process. 2. 2.

We present to the best of our knowledge the first algorithm for the inference of typed-norms that are relevant to infer the resource consumption, and prove soundness of the type inference step. 3. 3.

We extend our approach to handle polymorphic types and context-sensitive norms. 4. 4.

We perform an experimental evaluation and compare the results with those obtained using other systems [Hoffmann et al. (2012), Serrano et al. (2014)].

This article is an extended and revised version of a conference paper that was published in the proceedings of LOPSTR 2013 [Albert et al. (2014)]. The main extensions w.r.t. the conference paper affect all points above. As regards (1), we now provide a semantics for the rule-based representation and for the abstract representation and prove soundness of the transformation process, while [Albert et al. (2014)] did not have soundness results. \cbstart(2) The formalization of the algorithm for the inference of typed-norms and its soundness are new contributions of this article. In [Albert et al. (2014)] the inference algorithm was informally presented without any theoretical result, but in this extended revised version we present a completely formalized data-flow algorithm for inferring typed-norms, prove its termination and also prove that the detected typed-norms cover those that may affect the program executions, i.e., the inference algorithm is correct. \cbend(3) Also, in [Albert et al. (2014)], we had considered only monomorphic types. (4) The experiments of [Albert et al. (2014)] have also been improved to deal with the same benchmarks as in related work [Hoffmann et al. (2012), Serrano et al. (2014)] and a comparison with these systems has been included. We also have analyzed an industrial case study to show the performance of our approach when handling larger programs.

1.2 Organization of the Article

The article is organized as follows. In Section 2 we describe the syntax and the semantics of the rule-based representation. Section 3 presents our transformational approach to resource analysis with typed-norms. We start by reviewing the concept of typed-norm in Section 3.1. It is then extended to symbolic typed-norm and used to define the program abstraction in Section 3.2. Soundness of the transformation is proven in Section 3.3. Section 4 presents a typed-norms inference algorithm that is essential for the scalability of our approach. It infers the smallest sets for the typed-norms that are relevant for the inference of upper bounds. Section 4.1 formalizes the inference process and Section 4.2 proves its soundness. In Section 5.1 we describe the extension of our approach to handle polymorphic types. Section 6 contains our experimental evaluation, Section 7 compares our approach to related work, and Section 8 concludes. \cbstartFinally, A contains the proofs of the theoretical results. \cbend

2 A Rule-based Language

To simplify the presentation, we formalize our approach on a compact program syntax called rule-based representation (RBR) that contains program rules, pattern matching, and assignment. It already incorporates static single assignment [Cytron et al. (1991)] (each variable is assigned exactly once). Recursion is the only iterative mechanism and rule guards are the only conditional constructions in the RBR. Although simple, the RBR syntax can represent programs from different programming languages by means of an intermediate translation. For example, the RBR can be obtained from Java programs [Albert et al. (2012)], from the functional part of Abstract Behavioral Specification [Johnsen et al. (2012)] (ABS) programs [Albert et al. (2015)], and from the imperative part of ABS [Albert et al. (2015)]. This RBR can handle core-Prolog programs as well simply by interpreting the pattern matching as unification. Interestingly this does not require any further change in our size abstraction since our abstract programs are actually constraint logic programs. However, we note that analyzing abstract programs that originate from logic programs for cost should be done by an analyzer that takes failure into account [Serrano et al. (2014)].

2.1 Syntax of the rule-based language

In order to present typed-norms and its impact on termination and resource analyses in a clear way, for now we will consider only monomorphic types, although in Section 5.1 we will present the extension to polymorphic types.

Definition 1** (Monomorphic types)**

A monomorphic type $T$ can be a built-in data type as Int or an algebraic data type $\mathit{D}$ defined as:

\begin{array}[]{l@{~~~~~}lll}\hfil~{}~{}~{}~{}~{}&\mathit{Dd}&::=&\mathit{data}~{}\mathit{D}=\mathit{Alt}~{}[\overline{\mid\mathit{Alt}{}}]\\ \hfil~{}~{}~{}~{}~{}&\mathit{Alt}&::=&\mathit{Co}[(\overline{T})]\\ \end{array}**

where $\mathit{Co}$ represents a data constructor and the notation $[\overline{X}]$ represents an optional sequence of elements $X$. For simplicity, we assume that recursive types are in direct recursive form, otherwise, we could consider mutually recursive types to be the same type.

Example 1** (List of integer numbers)**

Using the syntax presented in Def. 1 we can define the data type of integer lists (IntList) as follows:

data IntList = Nil | Cons(Int, IntList)**

In this case, the type of the nullary data constructor Nil is IntList, and the type of the binary data constructor Cons is Int $\times$ IntList $\to$ IntList.

We define programs in rule-based representation (RBR programs in the sequel) as a set of data declarations followed by typed procedures:

Definition 2** (RBR syntax)**

[TABLE]

RBR programs P are formed by an optional set of data declarations ($\mathit{Dd}$) followed by a set of typed procedures ($\mathit{Proc}{}$). A typed procedure begins with a type declaration $p::T_{1}\times\cdots\times T_{n}\times T_{n+1}\times\cdots\times T_{n+m}$ stating the types $T_{1},\ldots,T_{n}$ of its $n$ input arguments $\bar{x}$ ($n\geq 0$) and the types $T_{n+1},\ldots T_{n+m}$ of its $m$ output arguments $\bar{y}$ ($m\geq 0$). After the type declarations there is a set of guarded rules ($r$), where $p(\bar{x},\bar{y})$ is the head of the rule, the guard $g$ specifies the conditions for the rule to be applicable and $b_{1},\dots,b_{n}$ are the statements in the rule’s body. For clarity, we sometimes enclose input and output arguments with angles “$\langle$” and “$\rangle$”, i.e., $p::\langle T_{1}\times\cdots\times T_{n}\rangle\times\langle T_{n+1}\times\cdots\times T_{n+m}\rangle$ and $p(\langle\bar{x}\rangle,\langle\bar{y}\rangle)$. If a program P has $n$ rules, we say that $|{P{}}|=n$ and ${P{}}^{i}$ represents the i-th rule of $P{}$. Guards ${\it match}(x,p)$ and ${\it nonmatch}(x,p)$, where $x\not\in{\it vars}(p)$ and $x$ and $p$ are of the same type, check if the value stored in variable $x$ matches with pattern $p$. Patterns ($p$) are data constructors $\mathit{Co}$ applied to variables. Terms ($t$) can be expressions (variables, integer numbers or arithmetic operations over expressions) or data constructors $\mathit{Co}$ applied to properly typed terms (e.g., Cons$(6,y)$, where $6$ has type Int and $y$ has type IntList). Terms not containing variables are called closed terms (a.k.a. ground terms). \cbstartWe assume that RBR programs are well-typed, i.e., every term and subterm in the program (including variables) have a type assigned that is coherent with procedure type declarations and data constructor types, considering a standard monomorphic type system [Pierce (2002)]\cbend.

Example 2** (RBR program)**

Figure 1 contains the RBR of a program with three principal procedures: fact computes the factorial of an integer number, factSum traverses a list of integer numbers and adds the factorial value for each element, and main is the entry point of the program that invokes factSum with the unitary list Cons(2,Nil). Both fact and factSum have only one rule each, which establishes the value of the accumulator and invokes while_n. Each loop is a procedure with two rules: one for finishing the loop and other for computing one iteration. For example, the first rule of while_0 has the guard 0 >= n (Line 9) to check that the loop has finished, therefore returning the input accumulator as output value. On the other hand, the second rule of while_0 (lines 11–14) contains the guard 0 < n that checks that the loop has not finished yet. In that case, updated values of prod and n are stored in prod1 and n1 (recall the use of static single assignment) and those values are used in the recursive call. Finally, main is a procedure with one rule that simply invokes factSum.

2.2 Semantics of the rule-based language

The rule-based language is evaluated using an operational semantics based on variable mappings and configurations, which are defined as:

Definition 3** (Variable mappings)**

A variable mapping $\it lv\in\mathcal{LV}$ is a mapping $[\overline{x\mapsto v}]$ that associates values $\overline{v}$ (namely integer numbers or ground constructed terms) to variables $\overline{x}$. We use the symbol $\epsilon{}$ for empty mappings and $\it lv_{1}\uplus\it lv_{2}$ for the union of variable mappings with disjoint domain. The notation $\it lv[\overline{x\mapsto v}]$ represents the extension of $\it lv$ with the new mappings $[\overline{x\mapsto v}]$ (this operation redefines the previous mappings for variables $\overline{x}$ if they appear in the domain of $\it lv$). The application $\it lv(x)$ returns the value $v$ associated to variable $x$, and $\it lv(t)$ returns the term resulting of replacing every variable in $t$ by its value in $\it lv$ (similarly for patterns $p$).

Example 3** (Variable mappings)**

Consider two variable mappings $\it lv_{1}\equiv[x\mapsto 3,y\mapsto\mbox{Nil}]$ and $\it lv_{2}\equiv[z\mapsto\mbox{Cons}(3,\mbox{Nil})]$. Since $\it lv_{1}$ and $\it lv_{2}$ have disjoint domains its union $\it lv_{1}\uplus\it lv_{2}$ is defined, with result $[x\mapsto 3,y\mapsto\mbox{Nil},z\mapsto\mbox{Cons}(3,\mbox{Nil})]$. On the other hand, $\it lv_{1}[x\mapsto\mbox{Nil},z\mapsto 0]=[y\mapsto\mbox{Nil},x\mapsto\mbox{Nil},z\mapsto 0]$ because the mapping $x\mapsto 3$ has been redefined in the extension of $\it lv_{1}$.

Definition 4** (Configurations)**

A configuration \cbstart(or call stack\cbend), denoted as $\it C$, is a sequence of activation records. An activation record is a triple of the form $\langle p,b{\cdot}{\it bs},\it lv\rangle$ where $p$ is a procedure name,111While procedure names are not really needed in the operational semantics, they increase clarity and simplify the proofs in A. $b$ is the next statement to execute, ${\it bs}$ is the sequence of statements after $b$, and $\it lv$ is the variable mapping that stores the values of the procedure parameters and local variables. Elements in sequences are separated by dots, where the last element of the sequence can represent the rest of the sequence (for example $b_{1}\cdot b_{2}\cdot{\it bs}$ or $\langle p,b{\cdot}{\it bs},\it lv\rangle\cdot\it C$), and we overload the symbol $\epsilon$ to denote empty sequences.

Figure 2 shows the rules of the operational semantics ($\leadsto$) that evaluates RBR programs. We consider a function $eval_{t}(t,\it lv)$ that evaluates a term $t$ under a variable mapping $\it lv$, returning a value $v$, and a function $eval_{g}(g,\it lv)$ that checks if a guard $g$ is satisfied under a variable mapping $\it lv$, returning a new (possibly empty) mapping that performs pattern matching.222The straightforward definition of these functions can be found in A. Figure 2 contains 3 rules. Rule $(1)$ evaluates activation records where the next statement is an assignment. In that case the value obtained from the right-hand side is introduced in the variable mapping of the activation record. Rule $(2)$ evaluates an activation record where the next statement is a procedure call $m(\bar{x},\bar{y})$. The first step is to obtain a fresh version of a rule of $m$ with all its variables renamed to avoid any collision. Then a variable mapping $\it lv_{1}$ is created for parameter passing and this mapping is used to evaluate the rule guard $g$. If the guard is evaluated to $\mathit{true}$, a new activation record with the rule body and the variable mapping333Static single assignment guarantees that $x$ does not appears in $\it lv_{1}$, so we could use mapping union instead of extension. $\it lv_{1}\uplus\it lv_{2}$ (where $\it lv_{2}$ is generated during the evaluation of the guard) is inserted in front of the configuration. Note that the activation record of the caller stores the relation $\overline{y^{\prime}\sim y}$ between the output values of the rule and the output parameters of the call. Finally, rule $(3)$ handles empty activation records, which are removed after the output values of the callee are stored in the variable mapping of the caller.

When needed, we decorate steps with two values $\leadsto^{a\cdot b}$: the semantic rule $a$ applied—(1), (2) or (3)—and the program rule number $b$ used, considering the whole program. If the step is not a procedure call i.e., it uses semantic rules (1) or (3), the program rule number is set to $\epsilon$. Examples of these decorations can be seen in the next example:

Example 4** (Evaluation of an RBR program)**

The evaluation of the main procedure in Figure 1 proceeds as shown below. For simplicity, when obtaining fresh names for variables—rule (2) in Figure 2—we simply use subscripts (n) with the same number as the current configuration $\it C_{n}$, we have underlined the statement that controls each step, and we write $\leadsto^{*}$ for several $\leadsto$-steps. Note that the program rule of factSum is the $4^{th}$ rule in the program, and the second rule of while_1 is the $6^{th}$ rule in the program.

[TABLE]

Definition 5** (Traces and sequences of steps)**

A trace $\mathcal{T}=\it C_{0}\leadsto^{r_{1}}\it C_{1}\leadsto^{r_{2}}\ldots\leadsto^{r_{n}}\it C_{n}$ is a sequence of $\leadsto$-steps from an initial configuration $\it C_{0}$. Given a trace $\mathcal{T}$, its steps are defined as $\mathit{steps}({\mathcal{T}})=\langle r_{1},r_{2},\ldots,r_{n}\rangle$, i.e., the sequence of step decorations of the $\leadsto$-steps in $\mathcal{T}$. Finally, the set of trace steps combines the steps of all the possible traces starting from a given configuration. Formally, $\mathit{Tr}(\it C_{0})=\{\mathit{steps}({\it C_{0}\leadsto^{r_{1}}\it C_{1}\leadsto^{r_{2}}\ldots\leadsto^{r_{n}}\it C_{n}})\mid n\in\mathbb{N}\}$. \cbstartThese notions will play an important role when defining the soundness of the abstraction (Section 3.3) and the soundness of the typed-norms inference in Section 4.2. \cbend

\cbstart

Let us informally discuss how the operational semantics is typically instrumented to account for cost of traces. We first assume that our language includes a special instruction tick($n$), where $n$ is a number, which is used to simulate a consumption of $n$ resources. Note that $n$ can be negative to simulate release of resources as well. In practice, we also allow the use any arithmetic expression instead of $n$, but for simplicity we assume it is a constant. Next, we instrument activation records with a global resource consumption counter called cost, and add a corresponding semantic rule for tick($n$) that simply sets cost to $\texttt{cost}-n$. A trace $\mathcal{T}$ is said to be valid if cost never takes negative values, i.e., cost is initialized with an amount of resources that is enough to carry out this particular execution. The cost of a trace is the minimal initial value for cost that makes it valid. Finally, a function $f$ that maps initial configurations to nonnegative values is called an upper bound on the worst-case cost if, for any initial configuration $\it C_{0}$, setting the initial value of cost to $f(\it C_{0})$ guarantees generating valid traces only. It is called a lower bound on the best-case cost if, for any initial configuration $\it C_{0}$, setting the initial value of cost to a value smaller than $f(\it C_{0})$ generates an invalid trace. \cbend

3 Size Abstraction Using Typed-Norms

The resource analysis framework we rely on [Albert et al. (2007), Albert et al. (2015)] performs two phases: (1) the program is transformed into an abstract representation where data are replaced by their sizes, and (2) such intermediate program is then analyzed to obtain upper/lower bounds on the resource consumption. In this section we will present how to abstract the size of program data using typed-norms and we will show that this abstraction is sound wrt. the original semantics of RBR programs. The second phase, performed by cost relation solvers like PUBS [Albert et al. (2013)], CoFloCo [Flores-Montoya and Hähnle (2014), Flores-Montoya (2016)] or the solver in CiaoPP [Serrano et al. (2014)], is independent of the technique applied to abstract data sizes and therefore will not be covered in this paper.

3.1 Preliminaries on Typed-Norms

In order to obtain the abstract representation of a program, we first replace data with numbers representing their sizes and then transform each instruction to linear constraints that reflect how these sizes change. The mapping from data structures to sizes is done by means of size functions (usually called norms). The most well-known norm used in the literature is term-size [Bossi et al. (1991), Bruynooghe et al. (2007)], which counts the number of constructors in a given data structure:

Definition 6** (Term-size norm)**

*The size of a term $t$ using the term-size norm is defined as: ${\parallel}{\mathit{Co}(t_{1},\ldots,t_{n})}{\parallel_{\mathit{ts}}}=1+\sum_{i=1}^{n}{\parallel}{t_{i}}{\parallel_{\mathit{ts}}}$. *

Notice that term-size is defined for terms containing only data constructors and cannot handle integer numbers.

Example 5** (Term-size norm)**

Consider the following program that uses binary trees (BT), list of binary trees (BTL), and lists of lists of binary trees (BTLL).

The trees function counts the number of binary trees in a list of type BTL, and sumtrees counts the number of binary trees in all the lists inside a list of type BTLL. Using the term-size norm, an empty list N or NL has size $1$ (one data constructor), whereas the list C(E,C(E,N)) has size $5$ (three list constructors plus two empty binary tree constructors). The function sumtrees traverses every element of the list for computing its number of trees. Using the term-size norm, a static analysis obtains a complexity of $O(n^{2})$ \cbstartfor the function sumtrees\cbend, where $n$ is the total size of the original list (i.e., the number of list, list of lists, and binary tree constructors). The size of each inner BTL list is bounded by $n$, so each call to trees will contribute $O(n)$ to the overall complexity. This is an example where term-size is not very precise, as it does not keep separate the information about the length of the BTLL list ($l$), the length of the inner BTL lists ($s$), and the size of the binary trees ($b$) to obtain a more accurate complexity of $O(l\times s)$. Note that the size of the binary trees does not play any role in the actual complexity of sumtrees because the binary trees are not traversed.

In order to overcome the mentioned imprecision we use typed-norms, which distinguish data constructors according to their types. Using this kind of norms we can measure the length of a list and the size of its elements separately, similarly to what has been done in the context of termination analysis of logic programs [Bruynooghe et al. (2007)]. Before introducing typed-norms, we present some notation about types that will be used throughout the paper:

Definition 7

Given two types $T_{1}$ and $T_{2}$, we say that $T_{2}$ depends on $T_{1}$, written $T_{1}\preceq T_{2}$, if the definition of type $T_{2}$ uses (either directly or transitively) type $T_{1}$. Relying on this notion, we define the set of constituent types of T as $\mathit{Constituents}({T})=\{T^{\prime}\mid T^{\prime}\preceq T\}\cup\{T\}$, i.e., all the types involved in the definition of $T$ including $T$ itself. If $T\preceq T$ we say that $T$ is a recursive type. \cbstartWe use $\mathit{type}_{i}(t)$ to refer to the type of a term $t$ in the i-th rule of the program, or simply $\mathit{type}(t)$ if the rule is clear from the context (note that the same variable can have different types in different rules). As the program is well-typed then every term $t$ has a monomorphic type assigned, so $\mathit{type}_{i}(t)$ simply returns that type.\cbend

By definition of $\mathtt{IntList}$—Line 1) in Figure 1—we have that $\mathtt{Int}\preceq\mathtt{IntList}$ and $\mathtt{IntList}\preceq\mathtt{IntList}$, therefore $\mathtt{IntList}$ is a recursive type and $\mathit{Constituents}({\mathtt{IntList}})=\{\mathtt{Int},\mathtt{IntList}\}$.

Definition 8** (Typed-norms for closed terms)**

We consider two typed-norms for computing the size of a closed term $t$ regarding a type $T$: ${\parallel}{t}{\parallel^{+}_{T}}$ and ${\parallel}{t}{\parallel_{T}}$. We will not contemplate integer values for the first norm but non-negative integer numbers (denoted as $\mathtt{Int}^{+}$) as we explain later.

[TABLE]

[TABLE]

Note that, in the last case of the definition of ${\parallel}{t}{\parallel_{T}}$, the $\mathit{max}$ of an empty set is $-\infty$ if $T$ is $\mathtt{Int}$, and [math] otherwise. In principle, this depends on the domain of the elements whose $\mathit{max}$ we are taking. The intuition behind these typed-norms is to count the number of data constructors of type $T$ that appear in term $t$. For integer numbers they simply return their value, whereas for constructed terms they check whether the term has type $T$ or not in order to count the constructor in the head. The difference is how to handle those nested subterms of type $T$ that occur in a bigger term of type different from $T$: ${\parallel}{t}{\parallel^{+}_{T}}$ sums the sizes of those subterms, whereas ${\parallel}{t}{\parallel_{T}}$ just keeps the size of the maximal subterm. The reason to constrain ${\parallel}{t}{\parallel^{+}_{T}}$ to $\mathtt{Int}^{+}$ instead of $\mathtt{Int}$ is that adding the integers inside a data structure provides a size that is not sound when negative values are involved. For example, ${\parallel}{\mbox{Cons(3, Cons(-3, Nil))}}{\parallel^{+}_{\mathtt{Int}}}$ would be [math]. On the other hand, ${\parallel}{\mbox{Cons(3, Cons(-3, Nil))}}{\parallel_{\mathtt{Int}}}=3$, so we know that any integer inside the list is smaller than or equal to $3$. We claim that ${\parallel}{t}{\parallel_{T}}$ suits better in the static analysis framework we consider, as we explain in Example 6.

In our rule-based language we only consider the basic type of integer numbers, so the rest of values are constructed using data constructors $\mathit{Co}$. However, typed-norms could be easily extended to support more basic types by providing a suitable case in the definition of ${\parallel}{\cdot}{\parallel^{+}_{T}}$ and ${\parallel}{\cdot}{\parallel_{T}}$. For example, if $\mathtt{String}$ were a basic type, we could define the size of strings as their length: ${\parallel}{\cdot}{\parallel^{+}_{T}}=\mathit{length}(t)\mbox{ if }T=\mathtt{String}\mbox{ and }\mathit{type}(t)=\mathtt{String}$ (similarly for ${\parallel}{\cdot}{\parallel_{T}}$).

Example 6** (Typed-norms for closed terms)**

\cbstart

Consider the program involving lists of binary trees shown in Example 5. The program does not contain integer values but only constructed data, so in this case both typed-norms ${\parallel}{\cdot}{\parallel_{T}}$ and ${\parallel}{\cdot}{\parallel^{+}_{T}}$ are sound. \cbendRegarding the list types BTL and BTLL, both typed-norms obtain the same values: ${\parallel}{\mathtt{N}}{\parallel^{+}_{\mathtt{BTL}}}={\parallel}{\mathtt{N}}{\parallel_{\mathtt{BTL}}}=1$ and ${\parallel}{\mathtt{NL}}{\parallel^{+}_{\mathtt{BTLL}}}={\parallel}{\mathtt{NL}}{\parallel_{\mathtt{BTLL}}}=1$ because they contain exactly one list constructor. They also coincide in the list of type BTLL with two elements $t\equiv$ CL( C(E,C(E,N)), CL(N,NL) ) regarding the type BTLL—${\parallel}{t}{\parallel^{+}_{\mathtt{BTLL}}}={\parallel}{t}{\parallel_{\mathtt{BTLL}}}=3$—as both count the number of list constructors: two constructors CL and one NL. However, the two norms differ wrt. type BTL: ${\parallel}{t}{\parallel^{+}_{\mbox{BTL}}}=4$ because it is the sum of all the BTL constructors in the list, 3 in the first element and one in the second element, but ${\parallel}{\cdot}{\parallel_{\mbox{BTL}}}=3$ as it is the maximum number of BTL constructors that appear in some element of the list. This difference has an impact on the concrete upper bounds obtained by static analysis. For example, the function sumtrees defined in Example 5 has an asymptotic complexity of $O(l\times s)$ in both cases, where $l$ is the size of the list of lists BTLL and $s$ is the size of its inner lists BTL. The size of any list $l$ is the same using both typed-norms (${\parallel}{l}{\parallel^{+}_{\mathtt{BTLL}}}={\parallel}{l}{\parallel_{\mathtt{BTLL}}}$), however, the size of its elements of type BTL will differ (${\parallel}{l}{\parallel^{+}_{\mathtt{BTL}}}$ $\geq$ ${\parallel}{l}{\parallel_{\mathtt{BTL}}}$). Since the static analysis framework we are considering is compositional and assumes worst-case scenarios for each iteration, the upper bound obtained using ${\parallel}{\cdot}{\parallel_{T}}$ \cbstartwill in general be tighter.\cbend

As a final comment, note that we could also define a typed-norm analogous to ${\parallel}{\cdot}{\parallel_{T}}$ that estimates the minimum value, by replacing “$\max$” with “$\min$”. This would be useful in situations where the upper bounds depend on the minimum value that an inner element of type $T$ can take, for example in recursive definitions where the value increments in every invocation. Similarly, if we replace the sum in the definition of ${\parallel}{\cdot}{\parallel_{T}}$ by “$\max$”, then we estimate the depth of terms instead of the number of their constructs. This is useful in cases like the example in Section 1. Note that all these norms can be used at the same time, so the size of some elements could be measured using minimum, maximum, depth, etc., if these values are relevant for the cost.

3.2 Our Transformational Approach

Next we describe how to use typed-norms to translate RBR programs to abstract programs that only contain procedure calls and constraints between sizes. From this information the resource analysis framework can produce cost relations [Albert et al. (2011)] to obtain the desired bounds. The main feature of our approach is that we allow the use of several abstractions for the same variable at the same time, as in [Bruynooghe et al. (2007)]. Thus, we can estimate the size of a term using different measures, and even relations between sizes of different measures which might be crucial for precision as claimed in [Bruynooghe et al. (2007)].

This is important since two different parts of the program might traverse two different parts of the same data structure, so having both measures allows us to provide tighter bounds. Since rules will usually contain variables, we need symbolic versions of typed-norms. These versions extend the typed-norms presented in Definition 8 with new cases for handling variables. In the following definition we only show the symbolic typed-norm ${\parallel}{\cdot}{\parallel_{T}}$, but it is analogous for ${\parallel}{\cdot}{\parallel^{+}_{T}}$. Notice that we use the same notation to represent typed-norms for closed terms and their symbolic counterparts because the version used is clear from the context.

Definition 9** (Symbolic typed-norms)**

The symbolic typed-norm to compute the size of a term $t$ (possibly with variables) regarding a type $T$ is defined as:

[TABLE]

Note that, as in the closed case, the max of an empty set is $-\infty$ if $T=\mathtt{Int}$, and [math] otherwise. When a variable $x$ is abstracted using a type $T\in\mathit{Constituents}({\mathit{type}(x)})$, it generates a variable $X_{T}$. On the other hand, abstracting variables not related to $\mathtt{Int}$ using the type $T=\mathtt{Int}{}$ generates the size $-\infty$. This special case is useful to obtain precise sizes in terms containing integer numbers and variables like pairs $(\mathtt{Int},\mbox{Seq})$. For example, we get ${\parallel}{\mbox{Pair}(-5,x)}{\parallel_{\mathtt{Int}}}=max({\parallel}{-5}{\parallel_{\mathtt{Int}}},{\parallel}{x}{\parallel_{\mathtt{Int}}})=max(-5,-\infty)=-5$ because $\mbox{Int}\notin\mathit{Constituents}({\mathit{type}(x)})=\{\mbox{Seq}\}$, which is more precise than a size of [math] obtained if ${\parallel}{x}{\parallel_{\mathtt{Int}}}=0$. Integer numbers are abstracted to themselves if $T$ is $\mathtt{Int}$, and in integer expressions with $T=\mathtt{Int}$ both subexpressions are abstracted recursively. The cases for data constructors are similar to Definition 8. Finally, if the type $T\neq\mathtt{Int}$ is not valid wrt. the type of $t$, i.e., $t$ cannot include any subterm of type $T$, then the symbolic typed-norm simply returns [math]. Notice that the symbolic version is equivalent to the typed-norm defined in Definition 8 for closed terms.

As an example, consider the term $3+x$ where both $3$ and $x$ have type $\mathtt{Int}$. The abstractions wrt. $\mathtt{Int}$ and $\mathtt{IntList}$ are ${\parallel}{3+x}{\parallel_{\mathtt{Int}}}=3+X_{\mathtt{Int}}$ and ${\parallel}{3+x}{\parallel_{\mathtt{IntList}}}=0$. If we consider a more complex term like $t\equiv$ \cbstartCons(z,Cons(5,Nil)) \cbendwe have that ${\parallel}{t}{\parallel_{\mathtt{Int}}}=\max(Z_{\mathtt{Int}},max(5,0))$ and ${\parallel}{t}{\parallel_{\mathtt{IntList}}}=1+1+1=3$.

In some cases it is inevitable to measure the size of a variable $x$ wrt. all its dependent types—$\mathit{Constituents}({\mathit{type}(x)})$—to bound the resource consumption of a program. However, \cbstartoften many types \cbenddo not play any role for termination or resource consumption and therefore can be safely ignored. In order to consider only those important types we use the notion of relevant types. For every variable $x$ and rule $i$ in the program, we write $\mathit{rtypes}_{i}(x)$ to refer to the set of types wrt. which we want to measure the size of that variable. In Section 4 we explain how to automatically infer these types. If the rule is clear from the context, we usually omit the subscript. Note that the set $\mathit{rtypes}(x)$ must be a subset of all dependent types of a variable $x$ in a program rule, i.e., $\mathit{rtypes}_{i}(x)\subseteq\mathit{Constituents}({\mathit{type}_{i}(x)})$.

Using the above symbolic typed-norms and the notion of relevant type-norms we can define our transformation of RBR programs. Figure 3 contains the definition of the function $\cdot^{\alpha}$ that abstracts guards, statements, rules, and procedures into \cbstartprocedure calls and conjunctions of arithmetic constraints between sizes444Relations ($=,>,\geq$) between linear expressions containing integer variables representing sizes. . \cbendIn all these cases we assume that given a type $T\in\mathit{rtypes}(x)$ the variable $X_{T}$ is an integer valued variable representing the size of (the value of) $x$ w.r.t. the typed-norm ${\parallel}{.}{\parallel_{T}}$. If $T\neq\mathtt{Int}$, then we implicitly assume $X_{T}\geq 0$, as constructed terms cannot have negative size. For a sequence of variables $\bar{x}$, we consider $\bar{X}$ is a sequence that results from replacing each variable $x_{i}$ by $X_{T_{1}}^{i},\ldots,X_{T_{n}}^{i}$, where $\mathit{rtypes}(x_{i})=\{T_{1},\ldots,T_{n}\}$.

As shown in Figure 3, the trivial guard true is transformed into the truth value $\top$, the identity element of conjunction. Conjunction of guards ($g_{1}\wedge g_{2}$) is abstracted into the conjunction of their size abstractions. Arithmetic guards are abstracted by replacing their variables $y$ with $Y_{\mathtt{Int}}$. For example, the expression $5$ is directly abstracted as $5$, whereas $x+y+8$ is abstracted as $X_{\mathtt{Int}}+Y_{\mathtt{Int}}+8$. Match guards—${\it match}(x,t)$—generate a conjunction with as many elements as types in $\mathit{rtypes}(x)$. Each element in the conjunction will be an equality between the variable $X_{T}$ (the size of $x$ wrt. $T$) and ${\parallel}{t}{\parallel_{T}}$ (the size of the term $t$ wrt. $T$, computed using the symbolic typed-norm). For example, if $\mathit{rtypes}(z)=\{\mathtt{Int},\mathtt{IntList}\}$, the abstraction of ${\it match}(z,\mathit{Cons(6,Nil)})$ will be the conjunction $Z_{\mathtt{Int}}=max(6,0)\wedge Z_{\mathtt{IntList}}=2$. On the other hand, the ${\it nonmatch}(x,t)$ guard is abstracted to the truth value $\top$, as it does not provide any information relating the sizes of $x$ and $t$. Regarding statements, the abstraction of a procedure call $p(\bar{x},\bar{y})$ simply replaces each variable with variables related to its different sizes555When needed, we use angles “$\langle$” and “$\rangle$” to enclose input and output variables, as we do in Section 2. (for example, $p(x,y)$ is abstracted to $p(X_{\mathtt{Int}},X_{\mathtt{IntList}},Y_{\mathtt{Int}})$ considering $\mathit{rtypes}(x)=\{\mathtt{Int},\mathtt{IntList}\}$ and $\mathit{rtypes}(y)=\{\mathtt{Int}\}$). Likewise, an assignment $x:=t$ is abstracted by generating a conjunction of equalities between the different variables $X_{T}$ and their sizes. The abstraction of a rule $p(\bar{x},\bar{y})\leftarrow g,b_{1},\ldots,b_{n}$ proceeds compositionally by abstracting its head, the guard and all the statements. As mentioned before, non-integer variables in a rule are assumed to be non-negative. The abstraction inserts these constraints explicitly using function $non\_neg({S})$, where $S$ is the set of variables occurring in the rule. The definition of $non\_neg({S})$ is the following:

[TABLE]

Finally, the abstraction of a procedure is the abstraction of all its rules.

Definition 10** (Program abstraction)**

Given a program $P\equiv[\overline{\mathit{Dd}}]~{}\overline{\mathit{Proc}}$, its size abstraction $P^{\alpha}$ is obtained by abstracting each procedure, i.e., $P^{\alpha}\equiv\overline{\mathit{Proc}^{\alpha}}$.

Figure 4 shows the abstraction for a fragment of the running example \cbstartgiven in Figure 1\cbend. When using the typed-norm ${\parallel}{\cdot}{\parallel_{T}}$ in Definition 9, $P^{\alpha}$ might include constraints of the form $X_{T}=E$ where $E$ is an arithmetic expression that involves “$\max$”. If the second phase of the resource analysis framework does not support this kind of constraints, they can be approximated using linear constraints as follows: (1) replace the sub-expression $\max(B_{1},\ldots,B_{n})$ by a new auxiliary variable $A$, (2) add the constraints $A\geq B_{1}\wedge\cdots\wedge A\geq B_{n}$; and (3) if $B_{i}\geq 0$ for all $1\leq i\leq n$, then add the constraint $B_{1}+\ldots+B_{n}\geq A$ as well. This process might be applied repeatedly in case of nested or multiple occurrences of $\max$. In the case of nested “$\max$” expression, we try to flatten them first. Notice that this approximation is not the only approach to handle $\max$ constraints, as they could also be approximated as in [Alonso-Blas et al. (2011)]. Moreover, in practice, the constant $-\infty$ (that we used in the definition of norms) can safely be replaced by any other constant — replacing it by the minimum value that syntactically appears in the program (or by [math]) works well in practice.

Example 7** (Program abstraction)**

Figure 4 shows the abstraction using the typed-norm ${\parallel}{\cdot}{\parallel_{T}}$ of the procedures factSum, while_1 and main from Figure 1. Each line contains a comment indicating if it involves non-negativity constraints or is the abstraction of a particular line of the original RBR program. We assume that list variables ($x\in\{$ l, l1$\}$) have $\mathit{rtypes}(x)=\{\mathtt{Int},\mathtt{IntList}\}$, whereas integer variables ($x\in\{$ sum, sum”, e, prod, sum1, r”$\}$) have $\mathit{rtypes}(x)=\{\mathtt{Int}\}$. The abstraction proceeds rule by rule, abstracting rule heads, guards, and statements; \cbstartso rule numbers (gray circles in the left margin) does not change from the concrete program. \cbendNotice that the constraints from the guard are combined with the non-negativity of all the non-integer variables of each rule. The most interesting part is the abstraction of the guard match(l, Cons(e,l1)) in the second rule of while_1. For the type $\mathtt{Int}$, the guard generates LInt = max(EInt, L1Int)—which could be approximated by linear constraints—and for the type $\mathtt{IntList}$ the guard generates the constraint $L_{\mathtt{IntList}}=1+L1_{\mathtt{IntList}}$, stating that the new list l1 is one constructor smaller than l.

\cbstart

Note that deterministic programs can be abstracted to non-deterministic programs if different terms of the same type have the same size. For example, consider the simple data type data Dir = Up | Down, and the following price :: $\langle\mathsf{Dir}\rangle\times\langle\mbox{Int}\rangle$ procedure:

Since $\mathit{rtypes}(x)=\mathsf{Dir}$ and $\mathit{rtypes}(y)=\mathsf{Int}$ in both rules, and ${\parallel}{\mathsf{Up}}{\parallel_{\mathsf{Dir}}}={\parallel}{\mathsf{Down}}{\parallel_{\mathsf{Dir}}}=1$, the program abstraction results in the nondeterministic version:

However, the possible nondeterminism introduced by the abstraction is not a problem from the point of view of soundness, as any trace in the deterministic program can be performed in the nondeterministic abstraction. This result is presented in the next section. \cbend

3.3 Soundness

The abstraction presented in the previous section transforms RBR programs into abstract programs, which the resource analysis framework can take as input for computing bounds. Therefore, we ensure that the size of variables that are observed in $\leadsto$ traces of RBR programs can be observed in traces of their abstractions. In order to prove this soundness result, we need an abstract operational semantics for abstract programs, which is an adaptation of the operational semantics for RBR programs in Figure 2. This abstract operational semantics evaluates abstract configurations step by step:

Definition 11** (Abstract configurations)**

An abstract configuration, denoted as $\mathit{AC}\equiv ar^{\alpha}|\psi$, is a sequence $ar^{\alpha}$ of abstract activation records followed by a conjunction $\psi$ of constraints. Similarly, an abstract activation record, denoted as $\langle bs^{\alpha}\rangle$, is a sequence of constraint conjunctions and abstract procedure calls $p(\bar{X},\bar{Y})$. We use Greek letters ($\psi$, $\varphi$, …) to denote constraint conjunctions, $b^{\alpha}$ to denote one constraint conjunction or one abstract procedure call, and $bs^{\alpha}$ to denote a sequence $b^{\alpha}_{1}\cdots b^{\alpha}_{n}$.

Figure 5 contains the operational semantics $\leadsto_{\alpha}$ that evaluates abstract configurations regarding an abstract program $P^{\alpha}$. Rule $(1)$ handles abstracted assignments, which are translated into conjunctive constraints $\varphi$. If $\varphi$ is consistent wrt. the global set of constraints ($\psi\wedge\varphi\not\models{\it false}$) then it is added to the global constraints and the evaluation continues with the next element of the abstract activation record. Rule $(2)$ handles procedure invocation. First, we obtain a fresh rule \cbstartfrom the abstract program $P^{\alpha}$\cbend. Then, if the parameter passing, the guard and the global constraints are consistent \cbstart($\overline{X=X^{\prime}}\wedge\varphi{\wedge}\psi\not\models{\it false}$),666We use the notation $\overline{X=X^{\prime}}$ to denote the conjunction of constraints $\bigwedge\overline{X=X^{\prime}}$. \cbenda new abstract activation record containing the body of the procedure is inserted in the abstract configuration.

Similarly to the $\leadsto$ semantics, the relation $\overline{Y=Y^{\prime}}$ between the output variables and the parameters is stored as a mark. Finally, rule $(3)$ removes an empty abstract activation record if the output variables are consistent with the global constraints. Notice that global constraints accumulate variables from all the abstract activation records, even those whose execution has finished and therefore have been removed. \cbstartSimilarly to $\leadsto$, we use the notion of abstract trace $\mathcal{T}^{\alpha}=\mathit{AC}_{0}\leadsto_{\alpha}^{r_{1}}\mathit{AC}_{1}\leadsto_{\alpha}^{r_{2}}\ldots\leadsto_{\alpha}^{r_{n}}\mathit{AC}_{n}$ where its steps are defined as $\mathit{steps}({\mathcal{T}^{\alpha}})=\langle r_{1},r_{2},\ldots,r_{n}\rangle$, and the set of abstract trace steps as the combination of the steps of all the possible abstract traces starting from a given configuration ($\mathit{Tr}(\mathit{AC}_{0})=\{\mathit{steps}({\mathit{AC}_{0}\leadsto^{r_{1}}\mathit{AC}_{1}\leadsto^{r_{2}}\ldots\leadsto^{r_{n}}\mathit{AC}_{n}})\mid n\in\mathbb{N}\}$. \cbend

Example 8** (Evaluation of an abstract program)**

The abstract evaluation of the main procedure in Figure 1 proceeds similarly to Example 4. When obtaining fresh names for variables—rule ($2$) in Figure 5—we use superscripts with the same number as the current abstract configuration $\mathit{AC}_{n}$. For simplicity, the statement or constraint that controls each step is underlined, the constraints in each abstract configuration $\mathit{AC}_{i}$ are denoted as $\psi_{i}$ and $\top$ is omitted. \cbstartEach step $\leadsto_{\alpha}^{a\cdot b}$ is decorated with the semantic rule $a$ and abstract program rule $b$ used, \cbendand $\leadsto_{\alpha}^{*}$ refers to many $\leadsto_{\alpha}$-steps.

[TABLE]

In $\mathit{AC}_{3}$ the first program rule of while_1 (Line 6 in Figure 4) cannot be used to evaluate the call because the guard is not compatible with the global set of constraints, namely: $L^{2}_{\mathtt{IntList}}=L^{4}_{\mathtt{IntList}}\wedge L^{4}_{\mathtt{IntList}}=1\land L^{0}_{\mathtt{IntList}}=L^{2}_{\mathtt{IntList}}\land L^{0}_{\mathtt{IntList}}=2\models\mathit{false}$. Therefore, the evaluation can only proceed with the second rule of while_1 (Rule 6, Line 11 in Figure 4).

The soundness result relates $\leadsto$-traces starting from a configuration $\it C$ with abstract $\leadsto_{\alpha}$-traces starting from the abstraction of $\it C$. The following definitions present the abstraction of configurations, which is based on ${\parallel}{\cdot}{\parallel_{T}}$ and the abstraction of statements defined in Figure 3.

Definition 12** (Variable mapping abstraction)**

The abstraction of a variable mapping $\it lv$ is defined as $\it lv^{\alpha}=\bigwedge\{X_{T}={\parallel}{\it lv(x)}{\parallel_{T}}~{}|~{}x\in\mathit{dom}(\it lv),T\in\mathit{rtypes}(x)\}$. Notice that $\it lv^{\alpha}$ is a conjunction of equalities between distinct $X_{T}$ variables and integer values, since $\it lv(x)$ are concrete values and therefore ${\parallel}{\it lv(x)}{\parallel_{T}}$ generates integer numbers.

Definition 13** (Configuration abstraction)**

Let $\it C=\langle p_{1},{\it bs}_{1},\it lv_{1}\rangle{\cdot}{\cdot}{\cdot}\langle p_{n},{\it bs}_{n},\it lv_{n}\rangle$ be a configuration. Its abstraction is defined as: $\it C^{\alpha}=\langle\it bs^{\alpha}_{1}\rangle{\cdot}{\cdot}{\cdot}\langle\it bs^{\alpha}_{n}\rangle|\psi$ where $\psi=\it lv^{\alpha}_{1}\wedge\ldots\wedge\it lv^{\alpha}_{n}$. Notice that $\psi$ is a conjunction of equalities between distinct $X_{T}$ variables and integer values, since every activation record uses fresh variables and $\psi$ is the conjunction of abstracted variable mappings.

The following \cbstarttheorem establishes the soundness of our translation using typed-norms: for any trace $\it C_{0}\leadsto^{*}\it C_{n}$ it is possible to create an abstract trace $\it C_{0}^{\alpha}\leadsto_{\alpha}^{*}ar^{\alpha}|\psi$ with the same steps.\cbend

\cbstart

Theorem 1** (Soundness)**

If $\mathcal{T}\equiv\it C_{0}\leadsto^{*}\it C_{n}$ then there is an abstract trace $\mathcal{T}^{\alpha}\equiv\it C_{0}^{\alpha}\leadsto_{\alpha}^{*}ar^{\alpha}|\psi$ such that $\mathit{steps}({\mathcal{T}})=\mathit{steps}({\mathcal{T}^{\alpha}})$, $\it C_{n}^{\alpha}=ar^{\alpha}|\widetilde{\psi}$ and $\psi\wedge\widetilde{\psi}\not\models{\mathord{\mathit{false}}}$.

\cbend

Intuitively, the above theorem states that the sizes of the variables of the concrete configuration $\it C_{n}$, w.r.t. the corresponding norm, define a model of the abstract state configuration.

\cbstart

Let us now informally explain how abstract programs preserve cost. The idea is to simulate the same process that we have described at the end of Section 2. First, during the abstraction phase the instruction tick($n$) is kept in the abstract program. Next, we instrument abstract activation records with a cost counter $\mathtt{cost}^{\alpha}$, and add a corresponding abstract semantic rule for tick($n$) that simply sets $\mathtt{cost}^{\alpha}$ to $\mathtt{cost}^{\alpha}-n$. An abstract trace $\mathcal{T}^{\alpha}$ is said to be valid if $\texttt{cost}^{\alpha}$ never takes negative values, i.e., cost is initialized with an amount of resources that is enough to carry out this particular abstract execution. Finally, a function $f^{\alpha}$ that maps initial abstract configurations to nonnegative values is called an upper bound on the (abstract) worst-case cost if, for and $\mathit{AC}_{0}$, setting the initial value of $\mathit{cost}^{\alpha}$ to $f^{\alpha}(\mathit{AC}_{0})$ guarantees generating valid abstract traces only. It is called a lower bound on the best-case cost if, for any $\mathit{AC}_{0}$, setting the initial value of $\texttt{cost}^{\alpha}$ to a value smaller than $f^{\alpha}(\mathit{AC}_{0})$ generates an invalid abstract trace. The function $f^{\alpha}$ is typically given in terms of the input abstract variables, i.e., in terms of the sizes of the corresponding data. The black-box component that infer the cost of the abstract program, infers such functions.

Given the statement of Theorem 1, it is easy to see that if $f^{\alpha}$ is is an upper (resp. lower) bound on the abstract worst-case (resp. best-case) cost, then it is also an upper (resp. lower) bound on the concrete cost (up to rewriting it in terms of typed-norms instead of corresponding abstract variables).

As a final remark, let us mention that although the paper and the experiments focus on upper bounds inference, our transformation is valid also to infer lower bounds as it ensures that the cost of every trace is preserved by the transformed program. \cbend

4 Inference of Relevant Types

As explained in the previous section, in order to abstract the size of a variable $x$ in the rule number $i$ we consider a set $\mathit{rtypes}_{i}(x)$ containing its relevant types. It is safe to assume that $\mathit{rtypes}_{i}(x)$ contains all the constituent types of $x$. However, the \cbstartcomplexity \cbendof the solving phase that obtains bounds grows exponentially with the number of variables involved, so it is very important to obtain the smallest sets for the relevant typed-norms. In this section we will present the inference algorithm for relevant types as well as its soundness result.

As it was observed in [Albert et al. (2008)], variables that do not affect the cost can be removed from the abstract program and the bounds obtained do not change. In our setting, the cost of a program depends primarily on the number of recursive calls performed, which is affected by the guards in the rules. Therefore, any variable that does not affect directly or indirectly the value of a guard can be ignored. We push this idea further \cbstartand detect, from each variable, those types that do not affect \cbenda guard evaluation directly or indirectly. These types are useless from the point of view of resource analysis, so they should be discarded from the set of relevant types of the variable.

The main intuition behind the algorithm for inferring relevant types is detecting those constituent types of a guard variable that are involved in the guard evaluation. For example, in match(l,Cons(x,xs)) we say that the type IntList of variable l is involved in the guard evaluation because the pattern matched is of type IntList. On the other hand, the type Int of the same variable is not involved in the guard evaluation because it can succeed or fail regardless of the possible Int values stored in l. Once we have this information from the guards, we propagate it backwards to include those relevant types in the rest of variables that can affect the value of the guard variable. \cbstartRelevant types will be propagated to the rules formal parameters, where they will be combined \cbendwith the relevant types from the rest of rules of the same procedure. Similarly, when invoking a procedure, the relevant types of the formal parameters will be included in the variables of the actual arguments.

Example 9** (Intuition of relevant types inference)**

Consider the RBR program in Figure 1. From Line 9 (Rule
2 ) we discover that Int is involved in the arithmetic guard 0 >= n for procedure while_0, so $\mbox{Int}\in\mathit{rtypes}_{2}($n$)$. The procedure while_0 is invoked in Line 6 of Rule
1 , so that this relevant type is propagated to the fact rule, i.e., $\mbox{Int}\in\mathit{rtypes}_{1}($n$)$. Similarly, fact is invoked in Line 27 of the Rule
6 corresponding to the while_1 predicate, so Int will be a relevant type for variable e. That rule contains a guard match(l, Cons(e,l1)) in Line 26, so Int will be propagated from variable e to l, i.e., $\mbox{Int}\in\mathit{rtypes}_{6}($l$)$. After another step of propagation in Rule
4 (procedure factSum) we will obtain that $\mbox{Int}\in\mathit{rtypes}_{4}(\mathsf{l})$. In summary, the relevant type Int detected in Rule
2 has been propagated to Rule
4 following the path
2 $\to$
1 $\to$
6 $\to$
4 . A similar but shorter process would produce that $\mbox{IntList}\in\mathit{rtypes}_{4}($l$)$ by propagating it in the path
5 $\to$
4 . In this case all the constituent types of IntList are relevant types for the parameter l in factSum (Rule
4 ), as the resource usage depends both in the length of the list and its stored numbers.

4.1 Formalization of relevant type inference

We formalize the relevant types inference algorithms as a data-flow analysis that constructs a mapping for the complete program. This mapping relates a set of relevant types to every variable in the program, and is defined as follows:

Definition 14** (Rule and program mappings)**

A rule mapping $M\ni\mu=[\overline{x\mapsto P({\textit{Types}})}]$ maps variables $\bar{x}$ in a rule to sets of types. The domain of $\mu$ is denoted as $\mathit{dom}(\mu)=\{\bar{x}\}$, and $\mu(x)$ returns the set of relevant types related to variable $x$. We use $\epsilon$ to denote an empty rule mapping.

A program mapping $\Sigma^{P{}}\ni\sigma=\langle\mu_{1},\mu_{2},\ldots,\mu_{n}\rangle$ aggregates the mappings of all the rules of a program $P{}$, considering that $P$ has $n$ rules. We use the notation $\sigma(i)=\mu_{i}$ to refer to the ith rule mapping in $\sigma$, and $\sigma(i)(x)$ to refer to the set of relevant types of variable $x$ in the $i^{th}$ rule.

Rule and program mappings support the following set of standard operations (extension, ordering, combination, restriction and renaming) that we use in the formalization of the inference algorithm.

Definition 15** (Operations on rule and program mappings)**

A rule mapping can be extended to a program mapping by assigning it to the $i^{th}$ rule and considering the empty mapping for the rest of rules. The extension of a rule mapping is denoted as $\langle{\mu}\rangle^{n}_{i}=\langle\epsilon_{1},\ldots,\epsilon_{i-1},\mu,\epsilon_{i+1},\ldots,\epsilon_{n}\rangle$.

We consider the natural order of rule mappings based on subset inclusion. We say that $\mu\sqsubseteq\mu^{\prime}$ iff. $\forall x\in\mathit{dom}(\mu).~{}\mu(x)\subseteq\mu^{\prime}(x)$. This order is extended to program mappings as follows: $\sigma\sqsubseteq\sigma^{\prime}$ iff. $\sigma(i)\sqsubseteq\sigma^{\prime}(i)$ for all rule $i$.

Rule mappings can be combined using the commutative and associative operator $\oplus$, defined as:

[TABLE]

If a variable $x$ appears in both rule mappings, its typed-norms are combined, otherwise it takes the typed-norms from the mapping where \cbstartit appears. \cbendNotice that variables not appearing in $\mathit{dom}(\mu_{1})$ \cbstartnor \cbend$\mathit{dom}(\mu_{2})$ are undefined in $\mu_{1}\oplus\mu_{2}$. We also consider the combination of program mappings of the same length by proceeding element-wise. We overload the symbol $\oplus$:

[TABLE]

When combining sequences of mappings we use the notation $\bigoplus_{i=1}^{n}\mu_{i}=\mu_{1}\oplus\ldots\oplus\mu_{n}$, and $\bigoplus_{\sigma\in C}\sigma=\sigma_{1}\oplus\ldots\oplus\sigma_{n}$ for combining sets $C=\{\sigma_{1},\ldots,\sigma_{n}\}$ of program mappings.

Rule mappings can be restricted to a set of variables $C$, formally:

[TABLE]

Finally, we use ${\mu}_{{\bar{x}}\sim{\bar{y}}}$ to denote the renaming of a rule mapping $\mu$, where the variables $\bar{x}=x_{1},\ldots,x_{n}$ are renamed to $\bar{y}=y_{1},\ldots,y_{n}$ (we consider that $\{\bar{x}\}\subseteq\mathit{dom}(\mu)$ and $\{\bar{y}\}\cap\mathit{dom}(\mu)=\emptyset$):

[TABLE]

Example 10** (Operations on rule and program mappings)**

Consider the following rule mappings:

[TABLE]

We have that $\mu_{2}\sqsubseteq\mu_{1}$ ($\{\mbox{IntList}\}\subseteq\{\mbox{Int},\mbox{IntList}\}$ for variable $y$) and $\mu_{3}\sqsubseteq\mu_{1}$ ($\{\mbox{Int}\}\subseteq\{\mbox{Int},\mbox{IntList}\}$ for variable $y$) but $\mu_{1}\not\sqsubseteq\mu_{2}$ ($x\notin\mathit{dom}(\mu_{2})$) and $\mu_{2}\not\sqsubseteq\mu_{3}$ ($\{\mbox{IntList}\}\not\subseteq\{\mbox{Int}\}$ for variable $y$). Regarding combination, we have that $\mu_{2}\oplus\mu_{3}=[y\mapsto\{\mbox{Int},\mbox{IntList}\}]$ and $\mu_{1}\oplus\mu_{2}=\mu_{1}\oplus\mu_{3}=\mu_{1}$. The restriction of rule mappings simply reduces the domain, so ${\mu_{1}}|_{\{x\}}=[x\mapsto\{\mbox{Int}\}]$ and \cbstart${\mu_{1}}|_{\{y\}}=[y\mapsto\{\mbox{Int},\mbox{IntList}\}]$. \cbendFinally, the renaming changes the variables in the domain, for example ${\mu_{1}}_{{x,y}\sim{a,b}}=[a\mapsto\{\mbox{Int}\},b\mapsto\{\mbox{Int},\mbox{IntList}\}]$ because $x$ is renamed by $a$ and $y$ is renamed by $b$.

Next we explain the inference algorithm, which is based on the definition of $\mathit{gen}^{P{}}$ that is given in Figure 6. Let $P{}$ be a program with $n$ rules ($|{P{}}|=n$). Then the relevant types inferred for the program is the least fixed point of the function $\mathit{gen}^{P{}}$, i.e., $\mathit{lfp}(\mathit{gen}^{P{}})\in\Sigma^{P}$. \cbstartNote that $\mathit{gen}^{P{}}$ is a monotone function and $\Sigma^{P}$ is a finite complete lattice, so the least fixed point can be computed exactly. \cbendConsidering this fixed point, the notation $\mathit{rtypes}_{i}(x)$ is defined as $\mathit{lfp}(\mathit{gen}^{P{}})(i)(x)$. The function $\mathit{gen}^{P{}}$ takes a program mapping $\sigma$ and extends it with the new information from the different rules of the program. For each program rule, it computes $\mathit{gen}^{P{}}_{i}(\sigma)$ and combines them with the current program mapping.

The function $\mathit{gen}^{P{}}_{i}$ takes the current program mapping and extends it using the information in rule number $i$. This function processes a rule $p(\bar{x},\bar{y})\leftarrow g,\bar{b}$ by combining the information from the guard ($\mathit{genG}^{P{}}_{i}$), the body ($\mathit{genS}^{P{}}_{i}$) and also collecting the relevant types from the parameters of all the rules of the same procedure (mapping $\mu_{i}$). This last step, which requires a renaming of the parameters $\bar{w}\bar{z}$ to $\bar{x}\bar{y}$, forces rules of the same predicate to have the same relevant types and therefore be abstracted to rules with the same name and number of abstracted parameters.

The function \cbstart$\mathit{genG}^{P{}}_{i}$ \cbendtakes a guard $g$ and a program mapping $\sigma$ and generates new relevant types in a rule mapping. This function proceeds by combining the new relevant types obtained in every fragment of the guard. A true guard always succeeds, so it does not impose any relevant type. Arithmetic guards $e_{1}~{}op~{}e_{2}$ requires Int as a relevant type for any variable in the expression. If there is a ${\it match}(x,p)$ guard and $x$ has a recursive type $T$ then this type is included as a relevant type for $x$. Non-recursive types are ignored because they cannot directly affect the number of recursions. However, if it contains an inner recursive type it will be detected and propagated when computing the fixed point. Finally, in ${\it match}(x,p)$ and ${\it nonmatch}(x,p)$ guards all relevant types already detected in the variables of the pattern $p$ are propagated to the matching variable $x$. \cbstartNote that in ${\it match}(x,p)$ guards, the recursive type $T$ of $x$ will be only relevant if the procedure is recursive, otherwise it will not affect the execution. Therefore, in practice we can infer relevant types for recursive procedures and then transfer that information to non-recursive ones. \cbend

The function $\mathit{genS}^{P{}}_{i}$ is overloaded. When it takes a set of statements $\{\bar{b}\}$ and a program mapping $\sigma$ then it traverses all the statements, invoking $\mathit{genS}^{P{}}_{i}$ for each one and combining the results. When $\mathit{genS}^{P{}}_{i}$ is invoked with only one statement $b$ then it propagates the information from $\sigma$ according to the statement processed. If $b\equiv{x}{:}{=}{t}$ then all the relevant types detected for $x$ that are constituents of the type of some variable $y$ of the right-hand side $t$ (set $T_{x,y,i}$) are propagated to that variable $y$. Finally, if the statement is a procedure call $p(\bar{x},\bar{y})$ then the function propagates the relevant types of the parameters. The set $A$ propagates all the relevant types for the input parameters $\bar{w}$ of the rules $j$ for the same procedure to the input parameters $\bar{x}$ of the current rule $i$. Similarly, the set $B$ propagates the relevant types of the output parameters $\bar{y}$ of the current rule $i$ to the output parameters $\bar{z}$ of the rules $j$ of the same predicate. Sets $A$ and $B$ contain program mappings that are combined.

The result of the relevant types inference always exists, and it can be effectively computed by iterating $\mathit{gen}^{P{}}$ starting from the empty program typed-norms mapping, as we state below.

Theorem 2

Consider a program $P{}$ such that $|{P{}}|=n$. Then $\mathit{lfp}(\mathit{gen}^{P{}})$ exists and is the supremum of the ascending Kleene chain starting from $\langle\epsilon_{1},\ldots,\epsilon_{n}\rangle$.

Example 11** (Relevant types inference)**

Here we explain how the functions in Figure 6 produce the result intuitively explained in Example 9. We consider $P$ as the RBR program in Figure 1. The process starts with an empty program mapping $\sigma_{0}=\langle\epsilon,\epsilon,\epsilon,\epsilon,\epsilon,\epsilon,\epsilon\rangle$. In the first iteration $\sigma_{1}=\mathit{gen}^{P{}}(\sigma_{0})$, when processing Rule
2 we obtain that $\mbox{Int}\in\sigma_{1}(2)(n)$ because of the call $\mathit{genG}^{P{}}_{2}($0 >= n$,\sigma_{0})$. In the next iteration, $\sigma_{2}=\mathit{gen}^{P{}}(\sigma_{1})$, so that information is propagated to Rule
1 , i.e., $\mbox{Int}\in\sigma_{2}(1)(n)$, thanks to the invocation \cbstart$\mathit{genS}^{P{}}_{1}($while_0($\langle$n, prod$\rangle$, $\langle$prod’$\rangle$)’$,\sigma_{1})$. \cbendThis information is collected in the set $A$ from Rule
2 . Similarly, that information is propagated to \cbstart$\mbox{Int}\in\sigma_{3}(6)(e)$ from the procedure call fact($\langle$e$\rangle$, $\langle$prod$\rangle$) \cbendin Line 27 by invoking $\mathit{genS}^{P{}}_{6}($fact($\langle$e$\rangle$, $\langle$prod$\rangle$)$,\sigma_{2})$. In the next step, the relevant type of \cbstarte \cbendis propagated to l—$\mbox{Int}\in\sigma_{4}(6)(l)$—when processing the guard with $\mathit{genG}^{P{}}_{6}($match(l, Cons(e,l1))$,\sigma_{3})$. Finally, the relevant type in the input parameter \cbstartl \cbendof Rule
6 is propagated to Rule
4 when processing the procedure call with \cbstart$\mathit{genS}^{P{}}_{4}($while_1($\langle$l, sum$\rangle$, $\langle$sum’$\rangle$)’$,\sigma_{4})$, \cbendso $\mbox{Int}\in\sigma_{5}(4)(l)$. As the function $\mathit{gen}^{P{}}$ is monotone, all this information will be kept in the least fixed point.

4.2 Soundness of relevant types inference

The inference of relevant types previously presented obtains a set of interesting types for every variable in every rule in the program. In order to state that those inferred types are enough to guide the traces, we need to introduce a new notion: value variation.

Definition 16** (Value variation)**

We say that $v^{\prime}$ is a variation of $v$ wrt. a type $T$ (written ${v}\triangleright^{T}{v^{\prime}}$) if $v^{\prime}$ results from replacing some components of $v$ with type $T$ for other components of the same type. For example, ${\mathtt{Cons(1,Nil)}}\triangleright^{\mathtt{Int}}{\mathtt{Cons(4,Nil)}}$—replacing $1$ by $4$—and ${\mathtt{Cons(0,Cons(1,Nil))}}\triangleright^{\mathtt{IntList}}{\mathtt{Cons(1,Nil)}}$—replacing the list completely.

Using the notion of variation, we can define when a type is useful for a variable: $T$ will be useful for a variable $x$ in the i-th rule of a program if changing the value of that variable changes the set of trace steps starting from a configuration of rule $i$. Formally:

Definition 17** (Useful type)**

We say that a type $T$ is useful for variable $x$ in the i-th rule of a program $P{}$—written $\mathit{useful}_{i}^{T}(x)$—if there are configurations $\it C_{0}$ and $\it C^{\prime}_{0}$ such that:

$\it C_{0}=\langle p,b{\cdot}{\it bs},\it lv\rangle\cdot\it C_{1}$, where $b{\cdot}{\it bs}$ are statements from the i-th rule of $P{}$ 2. 2.

$x\in\mathit{dom}(\it lv)$** 3. 3.

$\it C^{\prime}_{0}=\langle p,b{\cdot}{\it bs},\it lv^{\prime}\rangle\cdot\it C_{1}$* with $\it lv^{\prime}=\it lv[x\mapsto v]$ and ${\it lv(x)}\triangleright^{T}{v}$* 4. 4.

$\mathit{Tr}(\it C_{0})\neq\mathit{Tr}(\it C^{\prime}_{0})$**

Finally, we can state the soundness result of the inference of relevant types: if changing some components of type $T$ of a variable $x$ in rule $i$ affects the possible trace steps—i.e. $\mathit{useful}_{i}^{T}(x)$—then that type $T$ will be inferred by our process—i.e. $T\in\mathit{rtypes}_{i}(x)$.

Theorem 3** (Soundness)**

If $\mathit{useful}_{i}^{T}(x)$ then $T\in\mathit{rtypes}_{i}(x)$.

5 Extensions

The purpose of this section is to propose two extensions, which are very useful in practice, to the previous analysis. This, moreover, demonstrates that extending our framework is very easy.

5.1 Extension to Polymorphic Types

Let us now describe the extension of our approach to handle polymorphic types. First, we extend the data type definition in Section 2 by adding polymorphic types.

Definition 18** (Polymorphic types)**

Given a countable set of type variables $V_{T}$, a polymorphic type $T(V_{T})$ can be either a monomorphic type $T$, a type variable $\alpha\in V_{T}$, or an algebraic data type $\mathit{D}\langle\Gamma\rangle$ defined as:

\begin{array}[]{lll}\mathit{pDd}&::=&\mathit{data}~{}\mathit{D}\langle\Gamma\rangle=p\mathit{Alt}~{}[\overline{\mid p\mathit{Alt}{}}]\\ p\mathit{Alt}&::=&\mathit{Co}[(\overline{T(\Gamma)})]\\ \end{array}**

where $\Gamma\subseteq V_{T}$ is a finite subset of variables and any type variable in the right-hand side of a data type definition must be in the finite subset of variables in the left-hand side.

Example 12** (Polymorphic list)**

Using the syntax presented in Definition 18 we can define the data type of a polymorphic list (List$\langle$A$\rangle$) as follows:

data List$\langle$A$\rangle$ = Nil | Cons(A, List$\langle$A$\rangle$)**

The type IntList in Definition 1 can be represented by the type List$\langle$Int$\rangle$, where the parametric type A is instantiated to Int.

The RBR program syntax in Definition 2 can also be extended by adding polymorphic typed procedures in the following way:

[TABLE]

In this context, properly typed terms must be understood as the natural extension to polymorphic types. Figure 7 contains a RBR program with polymorphic types. In order to avoid confusion with the angles used to represent polymorphic types, in the examples of this section we use ${\tiny<}$ and ${\tiny>}$ to separate input and output arguments.

Analyzing RBR programs with polymorphic types can be done by transforming them into equivalent programs with monomorphic types only. This basically creates monomorphic versions of procedures (and types) for every use of the polymorphic types. Note that all possible uses (or instantiations) of the polymorphic types can be inferred using standard type inference algorithms. The following list of steps describes how such a transformation can be carried out:

• •

For every polymorphic type definition $\mathit{D}\langle\Gamma\rangle$ and every needed instantiation of the polymorphic type, we replace the polymorphic type definition by new copies using fresh monomorphic types and constructors.

• •

For every polymorphic procedure $p\langle\Gamma\rangle$ and every needed instantiation of its polymorphic type declarations, we replace the polymorphic procedure by new copies using fresh monomorphic types. Calls to procedures are also replaced by their properly typed monomorphic translations.

Note that, in addition, in some situations the user might be interested in analyzing a polymorphic procedure without providing any calling context, i.e., the polymorphic type cannot be instantiated to a monomorphic one in such cases. To handle these cases, for every type variable A in the program, we create a corresponding fresh monomorphic type A together with a fresh constant a, and then use those types to instantiate the corresponding procedures.

Example 13

Consider the RBR program in Figure 7. We can analyze the program and extract that head and tail are called in the body of while_1 with the type A instantiated to $\mathtt{Int}$. Therefore, we obtain the transformed program presented in Figure 8 and its abstraction in Figure 9. Note also that we have instantiated procedures head and tail with respect to the auxiliary monomorphic type A. This allows analyzing these procedures directly without considering the calling context of while_1.

\cbstart

Notice that, in this example, the number of arguments of head and tail procedures in the different instantiated versions of Figure 9 are the same, but they can differ depending on the instantiations of the type variables. In this way, we can keep the size relations between input and output instantiated abstractions (this is not possible if we have only one version of head and tail and a fixed number of arguments). \cbend

It is easy to check that any evaluation step given in the original RBR program is translated into an evaluation step in the transformed RBR program. The rest of the analysis follows from previous sections.

Another possibility for handling polymorphism could be to analyze every method once and instantiate that information in every particular method invocation. However, this is not an straightforward approach because different uses of the same polymorphic method can involve a different number of norms whose sizes must be related. Our approach is not completely modular and cannot be applied in every scenario (for example, polymorphic recursion cannot be handled), but provides a simple and effective way of supporting standard parametric polymorphism in our setting.

5.2 Context-Sensitive Norms

\cbstart

In this section, we propose a way to improve the precision of typed-norms using annotations. When we define a data type, we can use the same type in different positions and for different purposes. \cbstart\cbendIn such cases, if the type is not part of the recursive data structure, we can distinguish the different uses of the same type. The corresponding upper bounds are typically more precise and provide insights on the complexity of processing each part of the data. Technically, to achieve this, we \cbstart\cbendneed to annotate non-recursive types with their positions in the data type structures.

Definition 19** (Annotated Monomorphic types)**

An annotated monomorphic type $T$ can be a built-in data type as Int or an algebraic data type $\mathit{D}$ defined as:

\begin{array}[]{l@{~~~~~}lll}\hfil~{}~{}~{}~{}~{}&\mathit{Dd}&::=&\mathit{data}~{}\mathit{D}=\mathit{Alt}_{D}~{}[\overline{\mid\mathit{Alt}_{D}}]\\ \hfil~{}~{}~{}~{}~{}&\mathit{Alt}_{D}&::=&\mathit{Co}[(T_{D,\mathit{Co},1},\ldots,T_{D,\mathit{Co},n})]\\ \hfil~{}~{}~{}~{}~{}&T_{D,\mathit{Co},1}&::=&\mbox{\begin{cases}T&\mbox{ if $T$ is recursive in $D$}\ T_{\mathit{Co},i}&\mbox{ if $T$ is non-recursive in $D$}\end{cases}}\end{array}**

By unrolling annotated type definitions as trees we can extend $\mathit{Constituents}({T})$ to consider the annotations in the path from the root to the types. Figure 10 shows the type definition IntListPair = Pair(IntList, IntList) as a tree. From these annotations we obtain $\mathit{Constituents}({\mathtt{IntListPair}})=\{(\mathtt{IntListPair},\Lambda),(\mathtt{IntList},(\mathtt{Pair},1)),(\mathtt{Int},(\mathtt{Pair},1)\cdot(\mathtt{Cons},1)),(\mathtt{IntList},(\mathtt{Pair},2)),\allowbreak(\mathtt{Int},(\mathtt{Pair},2)\cdot(\mathtt{Cons},1))\}$, where each element of the set is formed by a pair (type, chain of positions) that represents its annotations in the tree, and the empty chain is represented by $\Lambda$. Notice that, if we do not have duplicated non-recursive types, we obtain the same number of norms (but annotated).

Symbolic typed norms are extended to deal with annotated types. The intuition in ${\parallel}{t}{\parallel_{(T,A)}}$ is that we traverse the annotated data structure using $A$ and when the annotation is empty ($\Lambda$), we have reached the type-norm we want to compute and we can use a definition similar to Definition 9.

Definition 20** (Symbolic annotated typed-norms)**

The symbolic typed-norm to compute the size of a term $t$ (possibly with variables) regarding a type $T$ is defined as ${\parallel}{t}{\parallel_{(T,A)}}={\parallel}{t}{\parallel^{A}_{(T,A)}}$ where:

[TABLE]

[TABLE]

By using ${\parallel}{t}{\parallel_{(T,A)}}$, we obtain a sound abstraction in the sense of Theorem 1, and the relevant type inference presented in Section 4 could be easily adapted to consider annotated type-norms. In the following, we present an example that shows how this technique is applied in practice.

Example 14

Consider the program in Figure 11 (left) where the rule lengthP takes a non-recursive IntListPair structure and computes the length of the second list if the first list is empty; otherwise, returns the length of the first list. Since both lists are of the same type (IntList), we are interested in considering their norms separately to obtain a better upper bound. Figure 11 \cbstart(right) \cbendshows this abstraction777For simplicity, we use $\mbox{IntList}_{1}$ and $\mbox{IntList}_{2}$ instead of $\mbox{IntList}_{(\mbox{Pair},1)}$ and $\mbox{IntList}_{(\mbox{Pair},2)}$, and $\mbox{Int}_{1}$ and $\mbox{Int}_{2}$ instead of $\mbox{Int}_{(\mbox{Pair},1)\cdot(\mbox{Cons},1)}$ and $\mbox{Int}_{(\mbox{Pair},2)\cdot(\mbox{Cons},1)}$.. It basically distinguishes the uses of IntList by their position in the definition of IntListPair—note the use of $\mbox{IntList}_{1}$ and $\mbox{IntList}_{2}$. Using this improvement, we can obtain the upper bound $1+max(6+6*\mbox{P}_{\mbox{IntList}_{1}},5+6*\mbox{P}_{\mbox{IntList}_{2}})$ for the function $\mbox{lengthP}({\tiny<}\mbox{P}_{\mathtt{IntListPair}},\mbox{P}_{\mathtt{IntList}_{1}},\mbox{P}_{\mathtt{IntList}_{2}},\mbox{P}_{\mathtt{Int}_{1}},\mbox{P}_{\mathtt{Int}_{2}}{\tiny>},{\tiny<}\mbox{Res}_{\mathtt{Int}}{\tiny>})$ instead of $7+6*\mbox{P}_{\mathtt{IntList}}$ $\mbox{lengthP}({\tiny<}\mbox{P}_{\mathtt{IntListPair}},\mbox{P}_{\mathtt{IntList}},\mbox{P}_{\mathtt{Int}}{\tiny>},$ ${\tiny<}\mbox{Res}_{\mathtt{Int}}{\tiny>})$. Note that in this case $\mbox{P}_{\mathtt{IntList}}=\mbox{P}_{\mathtt{IntList}_{1}}+\mbox{P}_{\mathtt{IntList}_{2}}$.

\cbend

The proposed approach using annotated types to handle context-sensitive norms generates abstract programs without any type information where every parameter represents an integer value. Therefore, these abstract programs can be solved automatically to upper and lower resource bounds using the existing techniques with no additional adaptations.

6 Experiments