1: \documentclass[a4paper]{article}

2: 

3: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

4: %                 LAYOUT PARAMETERS

5: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

6: \marginparwidth 2cm

7: \addtolength{\textwidth}{10mm}

8: \addtolength{\oddsidemargin}{-5mm}

9: \addtolength{\textheight}{15mm}

10: \addtolength{\topmargin}{-10mm}

11: 

12: \usepackage{amsmath}

13: \usepackage{amssymb} 

14: \usepackage{latexsym} 

15: \usepackage{picinpar}

16: \usepackage{curves}

17:  

18: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

19: %                 OUR COMMANDS 

20: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

21: 

22: \newcommand{\twocond}[2]{\genfrac{}{}{0pt}{}{#1}{#2}}

23: \newcommand{\reduces}[2]{\mathbin{\mathord{

24:   \stackrel{\scriptscriptstyle#1}{\longrightarrow}\hspace{-.2em}^{#2}}}}

25: \def\comment#1{\marginpar{\scriptsize #1}}

26: \def\onetom{\{1,\dots,m\}} 

27: \def\oneton{\{1,\dots,n\}} 

28: \def\onetol{\{1,\dots,l\}} 

29: \newcommand{\vars}{{ vars}} 

30: \newcommand{\pars}{{ pars}} 

31: \newcommand{\restr}[1]{\!\!\upharpoonright_{#1}} 

32: \newcommand{\vect}[1]{{\bar{#1}}}  

33: \newcommand{\dom}{{ dom}} 

34: \newcommand{\ran}{{ ran}} 

35: \def\ftau{f_{\tau_1 \dots \tau_n\rightarrow \tau}} 

36: \def\ptau{p_{\tau_1 \dots \tau_n}} 

37: \def\fdep{f_{\mathrm{rel}}}

38: \def\lar{\leftarrow}

39: \def\rar{\rightarrow}

40: \newcommand{\nt}[1]{\mbox{`}#1\mbox{'}}

41: \newcommand{\vt}{\Gamma}

42: \newcommand{\set}[1]{\{#1\}}

43: \newcommand{\bigset}[1]{\left\{#1\right\}}

44: \def\appl#1#2{#2 #1}

45: \def\subone{\triangleleft}

46: \def\subplus{\triangleleft^+}

47: \def\sub{\triangleleft^*} 

48: \def\rec{\bowtie}

49: \def\Rec{\mathop{\Join}}

50: \def\recjoker{\mathop{\Join}}

51: \def\nrs{\mathrel{\mathord{\triangleleft\hspace{-0.25em}\triangleleft}}}

52: \def\Nrs{\mathop{\mathord{\triangleleft\hspace{-0.25em}\triangleleft}}}

53: \def\notsub{\mathbin{\mathord{\not\!\sub}}}      

54: \newcommand{\AZ}{\mathcal{AZ}}

55: \newcommand{\palpha}{\aleph}

56: \newcommand{\ns}{\hspace{-0.4em}}

57: \def\varin{\in_{\scriptscriptstyle \approx}}

58: \newcommand{\describes}{\propto}

59: \newcommand{\sem}[1]{\mathord{[\hspace{-0.15em}[}#1\mathord{]\hspace{-0.15em}]}}

60: \newcommand{\renamed}[1]{\ll_{#1}}

61: \newcommand{\theory}{AC+}

62: \newcommand{\absleq}{\mathrel{\leq_\mathrm{\theory}}}

63: 

64: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

65: %                 OUR ENVIRONMENTS 

66: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

67:  

68: \def\newplaintheorem#1#2#3{%

69: \newtheorem{#1plain}[#3]{#2}%[section]

70: \newenvironment{#1}{\begin{#1plain}\rm}{\end{#1plain}}}

71: 

72: \newtheorem{theo}{Dummy}[section]

73: 

74: \newplaintheorem{ex}{Example}{theo}

75: \newplaintheorem{defi}{Definition}{theo}

76: \newplaintheorem{coro}{Corollary}{theo}

77: \newplaintheorem{rmtheorem}{Theorem}{theo}

78: \newplaintheorem{rmlemma}{Lemma}{theo}

79: \newplaintheorem{propo}{Proposition}{theo}

80: 

81: \newenvironment{pf}

82:  {{\normalfont \noindent {\scshape Proof.}}% 

83:    \setlength{\parindent}{0pt}%

84:    \setlength{\parskip}{1.5ex plus 0.5ex minus 1.0ex}% 

85: }

86:  {\hspace*{1em}\hfill$\Box$

87: \vspace{1ex}}

88: 

89: \pagestyle{plain} 

90:  

91: \begin{document} 

92: %\mainmatter 

93:  

94: \bibliographystyle{alpha} 

95:  

96: \title{Analysis of Polymorphically Typed 

97: Logic Programs Using ACI-Unification}

98: 

99:  

100: \author{Jan--Georg Smaus\thanks{

101: CWI, Amsterdam, The Netherlands,

102: \texttt{jan.smaus@cwi.nl}}}

103:  

104:  

105: \maketitle 

106: 

107: \begin{abstract} 

108: Analysis of (partial) groundness is an important application of

109: abstract interpretation. There are several proposals for improving the

110: precision of such an analysis by exploiting type information, icluding

111: our own work with Hill and King~\cite{SHK00}, where we had shown how

112: the information present in the type declarations of a program can be

113: used to characterise the degree of instantiation of a term in a

114: precise and yet inherently finite way. This approach worked for {\em

115: polymorphically} typed programs as in G\"odel or HAL. Here, we recast

116: this approach following Codish, Lagoon and

117: Stuckey~\cite{CL00,LS01}. To formalise which properties of

118: terms we want to characterise, we use {\em labelling functions}, which

119: are functions that extract subterms from a term along certain

120: paths. An {\em abstract term} collects the results of all labelling

121: functions of a term. For the analysis, programs are executed on 

122: abstract terms instead of the concrete ones, and usual 

123: unification is replaced by unification modulo an equality theory which

124: includes the well-known ACI-theory. Thus we

125: generalise~\cite{CL00,LS01} w.r.t.~the type systems considered and

126: relate those two works.

127: \end{abstract} 

128: 

129: \section{Introduction}\label{intro-sec}

130: 

131: Analysing logic programs for properties such as sharing and (partial)

132: groundness is important in compiler optimisations and

133: program development tools. Programs are usually analysed using

134: abstract interpretation~\cite{CC77}. In this paper, we consider in

135: particular the framework of {\em abstract compilation}~\cite{CD95}: 

136: a program is abstracted by replacing each unification with

137: an abstract counterpart, and then the abstract program is evaluated

138: just like a concrete program.

139: 

140: It has been recognised for some time that abstract interpretation can

141: be used for type analysis, and conversely, that type

142: information available a priori can improve the precision of other

143: analyses \cite{BM95,CD94,CL00,GdW94,JB92,HCC93}. For example, being

144: able to say that $\tt [1,X]$ is a list skeleton with possibly 

145: uninstantiated elements is more precise than only being able to

146: distinguish a ground from a possibly non-ground term. Underlying all

147: those works is a {\em descriptive} view of types: types are not part

148: of the programming language (in particular, no program is rejected

149: for not being ``well-typed''), but rather introduced to analyse an

150: arbitrary, say Prolog, program. In such approaches, it is natural that 

151: there is no sharp line between {\em type} analysis and {\em mode} 

152: (groundness, instantiation) analysis. For example, saying that a term 

153: is a list has two aspects: it is a list as opposed to, say, an

154: integer; it is a list, as opposed to an uninstantiated variable. 

155: 

156: Underlying this paper is a {\em prescriptive} view of types, i.e.,

157: types are a part of the programming language. We

158: analyse programs written in typed logic programming languages such as

159: G\"odel~\cite{goedel}, HAL~\cite{DGHMS99}, or

160: Mercury~\cite{mercury}. This implies that the types do not have to be

161: analysed since they are given beforehand by declarations or

162: inference. In particular, unlike e.g.~\cite{CL00}, we do not have to

163: deal with ``ill-typed'' terms such as $[1|2]$, since these can never

164: occur. 

165: 

166: We are aware of only two other works following

167: this view: our own~\cite{SHK00} and the recent work by Lagoon and

168: Stuckey~\cite{LS01}. This paper is a synthesis of those two works

169: and~\cite{CL00}, which, although designed for a

170: descriptive view of typing, can be adapted to prescriptive

171: typing.\footnote{The journal article~\cite{CL00} is based on an

172: earlier article~\cite{CL96}. However there are some interesting

173: differences, and therefore we will also sometimes refer to the earlier 

174: article.}

175: The generalisation w.r.t.~\cite{CL00,LS01} concerns {\em polymorphism},

176: which is disregarded in~\cite{LS01} and considered in~\cite{CL00} only

177: in a restricted form. We recast our own previous work using some 

178: aspects of their formalisms. In particular, the use

179: of the notions of {\em grammar} and {\em variables labelling

180: non-terminals}~\cite{LS01} should improve the understanding of what 

181: properties of terms our analysis captures, whereas the use of

182: ACI-unification~\cite{CL00} may provide the basis for an

183: implementation using well-studied algorithms. Also, we hope that our

184: work will prove to be applicable to analyses previously not envisaged by us, 

185: such as {\em sharing} analysis~\cite{LS01}.

186: 

187: In the intuitive explanations that follow, we refer to a set of

188: possible characterisations of the instantiation of a term as 

189: {\em abstract domain}.

190: 

191: The standard example to illustrate the benefits of an instantiation

192: analysis using types is the ubiquitous \texttt{APPEND} program. For

193: example, for the query 

194: $\tt append([A],[B],C)$, a typed analysis is able to infer that

195: any answer substitution will bind $\tt C$ to a list

196: skeleton. However, this example is unfit to explain the advance of

197: this paper over previous works. 

198: 

199: We therefore give another example.  A {\em table} is a data structure

200: containing an ordered collection of nodes, each of which has two

201: components, a key of type $\mathtt{string}$\footnote{

202: We abbreviate $\mathtt{string}$ by $\mathtt{str}$ and 

203: $\mathtt{integer}$ by $\mathtt{int}$.}, 

204: and a value,  of arbitrary type.

205: That is to say, the type constructor $\mathtt{table}$ is pa\-ra\-met\-rised by

206: the type of the values. For any type $\tau$, 

207: $\mathtt{table}(\tau)$ is the type of tables whose values have type 

208: $\tau$. Tables are implemented in G\"odel

209:   as an AVL-tree~\cite{vE81}:  a non-leaf node has a 

210: {\em key} argument, a {\em value} argument, arguments for the left and

211:   right subtrees, and an argument which represents balancing

212:   information. For a term of type $\mathtt{table}(\tau)$, our abstract 

213: domain characterises the instantiation of all key arguments, all value

214: arguments, and all the arguments representing the balancing

215: information. 

216: 

217: The characterisation of the instantiation of the value arguments

218: depends on $\tau$. Hence, our analysis supports parametric

219: polymorphism. In devising an analysis for polymorphically typed

220: programs, there are two main problems: the construction of an abstract 

221: domain for $\mathtt{table}(\tau)$ should be truly parametric in

222: $\tau$, and the abstract domains should be finite for a given program

223: and query. We only briefly illustrate what these points mean

224: here. Explaining why these requirements are non-trivial is

225: technically too involved for this introduction. 

226: 

227: The statement that the construction of an abstract domain for

228: $\mathtt{table}(\tau)$ is truly parametric in $\tau$, means,

229: for example, that the abstract domain for $\mathtt{table}(\mathtt{str})$

230: relates to $\mathtt{str}$ in exactly the same way as the abstract

231: domain for $\mathtt{table}(\mathtt{int})$ relates to 

232: %

233: \addtocounter{footnote}{-1}

234: %

235: $\mathtt{int}$\footnotemark. This implies that the abstraction of a

236: table can be defined in a generic way.

237: 

238: Lagoon and Stuckey formalise types as {\em regular tree

239: grammars}. Each type is identified with a non-terminal in

240: the grammar, and it is assumed that there are only finitely many

241: types. Finiteness is crucial for the termination of an analysis. When

242: we extend this approach to polymorphism, finiteness becomes a

243: problem, since there are infinitely many types, 

244: e.g.~$\tt list(int),\ list(list(int(int))), \dots$. Nevertheless,

245: under certain conditions, it can be ensured that for a given query and

246: program, there are only finitely many types. Note that this is in

247: contrast to~\cite{CL00} where it is proposed that termination of

248: analyses of polymorphic programs should be enforced by imposing an

249: ad-hoc bound on the depth of types.

250: 

251: %Although we follow the formalism of Lagoon and Stuckey in many ways,

252: %there are some differences that we want to note beforehand. They claim

253: %that their approach works for prescriptively typed programs, say

254: %G\"odel programs. But then in the formal part, the ``typedness'' of a

255: %program only means that each program variable is annotated with a

256: %grammar defining an expected type for this variable. We believe that

257: %prescriptive typing goes further than that. It must become clear that

258: %some annotations are legal and some are not, and for some programs no

259: %legal annotation exists. 

260: 

261: %This has a number of consequences. In particular, in the formalism

262: %of~\cite{LS01}, a unification constraint $\tt X = Y$ in a program

263: %means that the intersection of the two types corresponding to $\tt X$

264: %and $\tt Y$ must be computed. We believe that for prescriptively typed 

265: %programs, this should not be necessary, as the types of $\tt X$

266: %and $\tt Y$ must be identical anyway for the program to be

267: %well-typed. 

268: 

269: The rest of this paper is organised as follows.

270: The next section provides some preliminaries. 

271: In Sec.~\ref{structure-sec}, following~\cite{LS01}, 

272: we show how the type of a term gives rise to characterising 

273: its degree of instantiation in a structured way.

274: In Sec.~\ref{abstract-terms-sec}, following~\cite{CL00}, 

275: we define abstract terms based on the ACI1 equality theory.

276: In Sec.~\ref{alpha-label-relation-sec}, we formalise how abstract

277: terms capture the degree of instantiation of concrete terms, thereby

278: linking the two preceding sections, and also linking~\cite{LS01}

279: with~\cite{CL00}. 

280: Section~\ref{analysis-sec} lifts the abstraction of terms to an

281: abstraction of programs, and relates the semantics of a concrete

282: program and its abstraction in the sense of abstract interpretation. 

283: Section~\ref{implementation-sec} makes some comments on a possible

284: future implementation, and Sec.~\ref{discussion-sec} discusses our

285: results. 

286: 

287: 

288: \section{Preliminaries}\label{prelim-sec}

289: The reader is assumed to be familiar with the basics of logic

290: programming~\cite{L87}. We use 

291: a type system for logic programs with parametric

292: polymorphism~\cite{DGHMS99,goedel,mercury}. 

293: 

294: Let $\mathcal{K}$ be a finite set of (type) {\bf constructors},

295: each

296: $c\in\mathcal{K}$ with an arity $n\geq 0$ associated (by writing $c/n$),

297: and $\mathcal U$ be a denumerable set of {\bf parameters}.

298: The set of types is the term structure $\mathcal{T(K,U)}$. 

299: A {\bf type substitution} is an idempotent mapping

300: from parameters to types which is the identity almost everywhere.

301: We define the order $\prec$ on

302: types as the order induced by some (for example lexicographical) order on

303: constructor and parameter symbols, where parameter symbols come before

304: constructor symbols. 

305: 

306: The set of parameters in a syntactic object $o$ is denoted by $\pars(o)$.

307: Parameters are denoted by $u,v$, in concrete

308: examples by $\mathtt{U, V}$.

309: A tuple of {\em distinct} parameters ordered

310: with respect to~$\prec$ is denoted by $\bar{u}, \bar{v}$. 

311: 

312: Let $\mathcal V$ be a denumerable set of {\bf variables}.

313: The set of variables in a syntactic object $o$ is

314: denoted by $\vars(o)$.

315: Variables are denoted by $x, y$, in concrete

316: examples by $\mathtt{X, Y}$.

317: A tuple of {\em distinct} variables is denoted by 

318: $\vect{x}, \vect{y}$.  

319: 

320: A {\bf variable typing} is a mapping from a finite subset of 

321: $\mathcal V$ to $\mathcal{T(K,U)}$, written as

322: $\{x_1:\tau_1,\dots,x_n:\tau_n\}$. 

323: 

324: 

325: Let $\mathcal F$ (resp.~$\mathcal P$) 

326: be a finite set of {\bf function} (resp.~{\bf predicate}) symbols, each

327: with an arity and a {\bf declared type} associated with it, 

328: such that:

329: for each $f \in \mathcal F$, the declared type has the form

330: $(\tau_1,\dots,\tau_n,\tau)$, where $n$ is the arity of $f$,

331: $(\tau_1,\dots,\tau_n,\tau)\in \mathcal{T(K,U)}^{n+1}$,

332: and $\tau$ 

333: satisfies the {\em transparency condition} \cite{HT92}:\label{transparency}

334: $\pars(\tau_1,\dots,\tau_n) \subseteq \pars(\tau)$;

335: for each $p \in \mathcal P$, the declared type has the form

336: $(\tau_1,\dots,\tau_n)$, 

337: where $n$ is the arity of $p$ and

338: $(\tau_1,\dots,\tau_n)\in \mathcal{T(K,U)}^n$. 

339: We often indicate the declared types by writing 

340: $\ftau$ and $\ptau$.

341: %We assume that there is a special predicate symbol 

342: %$=_{u,u}$

343: %where $u\in \mathcal U$.

344: 

345: Throughout this paper, we assume $\mathcal K$, $\mathcal F$, and 

346: $\mathcal P$ arbitrary but fixed.

347: The {\bf typed language}, i.e.\ a language of terms, atoms etc.\ based

348: on $\mathcal K$, $\mathcal F$, and $\mathcal P$, is defined by the

349: rules in Table \ref{rules-tab}. All objects are defined relative to 

350: a variable typing $\vt$, and $\_\vdash\dots$ stands for ``there exists

351: $\vt$ such that $\vt\vdash\dots$''. 

352: Actually, we will rarely refer to the type system explicitly, but it

353: should be noted that any objects we will come across in the context of 

354: analysing a typed program will be correctly typed according to those

355: rules. This is guaranteed because typed programs have the 

356: {\em subject reduction} property~\cite{HT92}.

357: 

358: \begin{table}[t]

359: \caption{Rules defining a typed language ($\Theta$ is a type

360: substitution) \label{rules-tab}}

361: \begin{center}

362: %\small

363: \begin{tabular}{rl}

364: {\em (Var)} &

365: $\{x:\tau,\dots\}\vdash x:\tau$\\[2ex]

366: {\em (Func)} &

367: \Large

368: $\frac%

369:   {\vt\vdash t_1:\tau_1\Theta\ \cdots \ \vt\vdash t_n:\tau_n\Theta}%

370:   {\vt\vdash\ftau(t_1,\dots,t_n):\tau\Theta}$ 

371: %& $\Theta$ is a type substitution

372: \\[2ex]

373: {\em (Atom)} &

374: \Large

375: $\frac%

376:   {\vt\vdash t_1:\tau_1\Theta\ \cdots \ \vt\vdash t_n:\tau_n\Theta}%

377:   {\vt\vdash\ptau(t_1,\dots,t_n)\; \mathit{Atom}}$ 

378: %& $\Theta$ is a type substitution

379: \\[2ex]

380: {\em (Head)} &

381: \Large

382: $\frac%

383:   {\vt\vdash t_1:\tau_1\ \cdots \ \vt\vdash t_n:\tau_n}%

384:   {\vt\vdash\ptau(t_1,\dots,t_n)\; \mathit{Head}}$ 

385: %\\[2ex]

386: \end{tabular}

387: \begin{tabular}{rl}

388: {\em (Query)} &

389: \Large

390: $\frac%

391:   {\vt\vdash A_1\; \mathit{Atom}\ \cdots \  \vt\vdash A_n\; \mathit{Atom}}%

392:   {\vt\vdash A_1,\dots,A_n\; \mathit{Query}}$ \\[2ex]

393: {\em (Clause)} & 

394: \Large

395: $\frac%

396:   {\vt\vdash A\; \mathit{Head} \quad \vt\vdash Q\; Query}%

397:   {\vt\vdash A \leftarrow Q\; \mathit{Clause}}$ \\[2ex]

398: {\em (Program)} &

399: \Large

400: $\frac%

401:   {\_\vdash C_1\; \mathit{Clause} \ \cdots \ \_\vdash C_n\; \mathit{Clause}}%

402:   {\_\vdash \{C_1,\dots,C_n\}\; \mathit{Program}}$ 

403: %\\[2ex]

404: %{\em (Queryset)} &

405: %\Large

406: %$\frac%

407: %  {\_\vdash Q_1\; \mathit{Query}\ \cdots \  \_\vdash Q_n\; \mathit{Query}}%

408: %  {\_\vdash \{Q_1,\dots, Q_n\} \; \mathit{Queryset}}$ 

409: \end{tabular}

410: \end{center}

411: \end{table}

412: 

413: %\begin{defi}\label{substitution-def}

414: %If 

415: %$\vt\vdash x_1\!=\!t_1, \dots, x_n\! =\! t_n\ Query$

416: %where $x_1,\dots,x_n$ are distinct variables and for

417: %each $i\in \onetom$, $t_i$ is a term distinct from $x_i$, then 

418: %$(\{ x_1/t_1,\dots,x_n/t_n\}, \vt)$ is a 

419: %{\bf typed (term) substitution}. 

420: %\end{defi}

421: 

422: %The restriction of a 

423: %substitution $\theta$ to the variables in a syntactic object $o$ is

424: %denoted as $\theta \restr{o}$, and analogously for type 

425: %substitutions.

426: %The relation symbol of an atom $a$ is denoted by $Rel(a)$.

427: 

428: %Programs are assumed to be in {\em canonical form}: 

429: %a {\bf canonical literal}

430: %is a unification constraint (equation) of the

431: %    form $x = y$ or 

432: %$x = f(\bar{y})$, or an

433: %    atom $p(\bar{y})$.

434: %A {\bf canonical query} is a sequence of canonical literals. 

435: %A {\bf canonical clause} has the form 

436: %$p(\bar{y}) \lar Q$ where $Q$ is a canonical query.

437: %A program is {\bf canonical} if all of its clauses are. 

438: 

439: Concerning semantics, we entirely follow~\cite{CL00}.

440: The set of atoms is denoted by $\mathcal{B}$, and 

441: elements of $2^\mathcal{B}$ are called 

442: {\bf interpretations}. 

443: For a syntactic object $o$ and a set of objects $I$, we denote by

444: $\langle C_1,\dots,C_n\rangle\renamed{o} I$ that 

445: $C_1,\dots,C_n$ are elements of $I$ renamed apart from $o$ and from

446: each other.

447: So the analysis we shall propose is generic and independent of any particular

448: (say top-down or bottom-up) concrete semantics, but examples will be

449: given using the $s$-semantics, i.e.~the semantics based on the

450: non-ground $T_P$-operator, defined as follows:

451: \begin{align*}

452: T_P(I) = 

453: \set{H\theta \mid & 

454: C = H \lar B_1,\dots,B_n \in P,

455: \langle A_1,\dots,A_n \rangle \renamed{C} I,\\[-1ex]

456: &

457: \theta = 

458: MGU(\langle B_1,\dots,B_n\rangle,\langle A_1,\dots,A_n\rangle)}.

459: \end{align*}

460: We denote by $\sem{P}_s$ the least fixpoint of $T_P$.

461: 

462: We denote by $t_1\leq t_2$ that $t_1$ is an instance if $t_2$.

463: The domain of a substitution $\theta$ is denoted as $\dom(\theta)$.

464: 

465: \section{The Structure of Terms and Types}\label{structure-sec}

466: In this section, we show how the type of a term gives rise to a

467: certain way of characterising its structure, and in particular, how

468: its degree of instantiation can be characterised in a structured way. 

469: We alternate between recalling the

470: formalism of~\cite{LS01}, and adapting it to polymorphic types,

471: thereby linking to~\cite{SHK00}. 

472: 

473: \subsection{Regular Types~\cite{LS01}}\label{regular-subsec}

474: 

475: \begin{defi}\label{automaton-def}

476: A {\bf top-down deterministic finite tree automaton} (top-down DFTA)

477: is a tuple 

478: $\mathcal{A} = \langle q_0, Q, \Sigma, \Delta\rangle$, where $Q$ is a

479: set of states, $q_0 \in Q$ is an initial state and $\Delta$ is a set

480: of transition rules of the form

481: $q(f(x_1,\dots,x_n)) \rightarrow f(q_1(x_1),\dots,q_n(x_n))$, such

482: that no two rules have the same left-hand side.

483: \end{defi}

484: 

485: Top-down DFTA's accept the class of languages called {\em regular

486: types}. 

487: 

488: \begin{defi}\label{grammar-def}

489: A {\bf regular tree grammar} is a tuple 

490: $\mathcal{G} = \langle S, W, \Sigma, \Delta \rangle$, where

491: $W$ is a finite set of non-terminal symbols, 

492: $S\in W$ is a starting non-terminal, 

493: $\Delta$ is a set of productions in the form

494: $X \rightarrow f(Y_1,\dots,Y_n)$ s.t.~$X,Y_1,\dots,Y_n\in W$ and 

495: $f/n \in \Sigma$. 

496: %

497: A regular tree grammar is {\bf deterministic} if for any 

498: non-terminal $X$ and any two productions

499: $X \rightarrow f(Y_1,\dots,Y_n)$ and 

500: $X \rightarrow g(Z_1,\dots,Z_m)$, we have 

501: $f/n \neq g/m$.

502: \end{defi}

503: 

504: It has been pointed out that the two formalisms above define the same

505: class of languages. Transitions of the automaton can be converted to

506: grammar productions and vice versa by identifying each non-terminal

507: symbol with a corresponding state of the automaton. 

508: 

509: \begin{ex}\label{same-class-ex}

510: The DFTA 

511: $

512: \langle q_L, \set{q_L, q_E}, 

513: \set{\mathtt{nil}/0, \mathtt{cons}/2, \mathtt{a}/0, \mathtt{b}/0},

514: \Delta \rangle

515: $,

516: where 

517: \[

518: \Delta = \set{%

519: q_L(\mathtt{nil}) \rar\mathtt{nil},\;

520: q_L(\mathtt{cons}(x,y)) \rar\mathtt{cons}(q_E(x),q_L(y)),\;

521: q_E(\mathtt{a}) \rar\mathtt{a},\;\allowbreak

522: q_E(\mathtt{b}) \rar\mathtt{b}

523: },

524: \] 

525: accepts ground lists of $\mathtt{a}$'s and $\mathtt{b}$'s.

526: 

527: 

528: The grammar 

529: $L \rar\mathtt{nil} | \mathtt{cons}(E,L),\;

530: E \rar\mathtt{a} | \mathtt{b}$ 

531: defines the same language.

532: \end{ex}

533: 

534: The equivalence of the two formalisms allows us to represent derivations of

535: the grammar as transitions of a {\em deterministic} rewriting

536: system. These transitions have the form 

537: $N(f(t_1,\dots,t_n)) \rar f(N_1(t_1),\dots,N_n(t_n))$, where 

538: $N \rightarrow f(N_1,\dots,N_n)$ is a production of the grammar 

539: ($n \geq 0$). Using this notation, we say that the grammar

540: $\mathcal{G}= \langle S, W, \Sigma, \Delta \rangle$ 

541: {\bf accepts} a term $t$ if $S(t) \rar^* t$. Sometimes we are

542: interested in a particular segment of a single path in a derivation 

543: tree starting from root $S$ and reaching a non-terminal $N$ with a

544: subterm $t'$ of $t$, i.e., in derivations

545: $S(t) \rar^* s[N(t')]$, where the notation $s[N(t')]$ means that $s$

546: has $N(t')$ as a subterm. Abusing notation, we write

547: $S(t) \rar^* N(t')$ in this case. 

548: 

549: \begin{ex}\label{path-ex}

550: Given the grammar in Ex.~\ref{same-class-ex},

551: we have 

552: \[

553: L(\mathtt{cons}(\mathtt{a},\mathtt{nil})) \rar

554: \mathtt{cons}(E(\mathtt{a}), L(\mathtt{nil})) \rar

555: \mathtt{cons}(\mathtt{a}, L(\mathtt{nil})) \rar

556: \mathtt{cons}(\mathtt{a}, \mathtt{nil}).

557: \] 

558: We also write 

559: $L(\mathtt{cons}(\mathtt{a},\mathtt{nil})) \rar^* E(\mathtt{a})$ and

560: $L(\mathtt{cons}(\mathtt{a},\mathtt{nil})) \rar^* L(\mathtt{nil})$,

561: using the above notation.

562: 

563: 

564: This notation can also be applied to non-ground terms. For example, we 

565: have

566: $L(\mathtt{cons}(\mathtt{a},\mathtt{Y})) \rar^* E(\mathtt{a})$ and

567: $L(\mathtt{cons}(\mathtt{X},\mathtt{Y})) \rar^* L(\mathtt{Y})$. 

568: \end{ex}

569: 

570: \setlength{\unitlength}{3mm}

571: 

572: \begin{figwindow}[0,r,%

573: {\mbox{\hspace{1em}\begin{picture}(10,4)%

574: {\linethickness{0.2\unitlength}

575: \put(1,0){\framebox(2,3){$L$}}}%

576: \curve(3,2, 4,2.5, 4,4, 2.5,4, 2,3)%

577: \put(7,0){\framebox(2,3){$E$}}%

578: \put(3,1){\vector(1,0){4}}%

579: \put(2,3){\vector(0,-1){0}}%

580: \end{picture}}},%

581: {Type graph \label{one-type-graph-fig}}]

582: It is also convenient to depict a grammar graphically as a 

583: {\em type graph}, defined previously as a graph whose nodes are

584: labelled with types or functions~\cite{HCC93}. We simplify that

585: definition by leaving out the function nodes. Thus a type graph for 

586: $\mathcal{G} = \langle S, W, \Sigma, \Delta \rangle$ is

587: a directed graph whose nodes are labelled by non-terminals, and there

588: is an edge from $N$ to $N'$ if and only if there is a production 

589: $N \rar f(\dots,N',\dots)$ is $\mathcal{G}$. We call the node labelled

590: $S$ the {\bf starting node}. Figure~\ref{one-type-graph-fig} shows the type

591: graph for Ex.~\ref{same-class-ex}. 

592: \end{figwindow}

593: 

594: 

595: \subsection{Regular Types and Polymorphism}

596: \label{regular-polymorphic-subsec}

597: Converting the type declarations of a typed language such as Mercury

598: into grammar rules has been considered 

599: straightforward~\cite[footnote 1]{LS01}. This

600: seems justified, albeit only in the absence of polymorphism. Since

601: $\mathcal K$ is a {\em finite} set of type constants, we can identify

602: each type constant with a non-terminal, and each function 

603: $\ftau \in \mathcal{F}$ is translated into a production

604: $\tau \rar f(\tau_1,\dots,\tau_n)$.

605:  In that way, each type (constant)

606: corresponds to a grammar with that type as starting

607: non-terminal.\footnote{

608: Although one might be

609: confused by the fact that~\cite{LS01} also says that there is a

610: grammar for each {\em program variable}, but this is simply a matter

611: of renaming.}  

612: Table~\ref{formalisms-tab} summarises the correspondences between

613: the four formalisms we effectively identify in this paper.

614: 

615: \begin{table}[t]

616: \begin{center}

617: \begin{tabular}{llll}

618: Automata                                & Grammars     & 

619: Types                                   & Graphs \\\hline

620: state                                   & non-terminal\hspace{1em} & 

621: type                                    & node \\

622: transition rule\hspace{1em}             & production   & 

623: $\approx$ type declarations\hspace{1em} & edge

624: \end{tabular}

625: \end{center}

626: \caption{Correspondences between formalisms\label{formalisms-tab}}

627: \end{table}

628: 

629: Note that in Sec.~\ref{prelim-sec}, we have specified that each $f$

630: has {\em exactly} one declaration; in other words, there is no

631: overloading. This is a sufficient condition for the grammar to be

632: deterministic. One could allow some overloading, by specifying: if 

633: $\ftau\in \mathcal{F}$ and  

634: $f_{\sigma_1,\dots,\sigma_m\rar\sigma}\in \mathcal{F}$ and

635: $\ftau \neq f_{\sigma_1,\dots,\sigma_m\rar\sigma}$, then either 

636: $\tau\neq\sigma$, or $n\neq m$. This would strictly include the

637: overloading allowed in G\"odel. We prefer however to disallow

638: overloading to avoid unnecessary complication.  

639: 

640: We now give a pseudo-definition of a grammar corresponding to a

641: polymorphic type --- ``pseudo'' because the set of non-terminals may

642: be infinite. It is trivial to generalise the definition of a grammar

643: to infinite sets of non-terminals, but in the end, it is not

644: desirable, since it would undermine our goal of characterising

645: (approximating) properties of a term of arbitrary type in a finite

646: way. We will later impose a condition to ensure finiteness.

647: 

648: 

649: \begin{defi}\label{corresponding-grammar-def}

650: Consider a typed language given by $\mathcal{K, F}$

651:  and a type $\phi$. The 

652: {\bf grammar corresponding to $\phi$}, denoted 

653: $\mathcal{G}(\phi)$, 

654: is the grammar 

655: $\langle \nt{\phi}, W, \mathcal{F}, \Delta \rangle$, 

656: where $W$ is inductively defined as follows

657: \begin{itemize}

658: \item

659: $\nt{\phi} \in W$,

660: \item

661: $\ftau\in\mathcal{F}$ and

662: $\nt{\tau\Theta} \in W$ for some type substitution $\Theta$ implies\\

663: $\nt{\tau_1\Theta},\dots,\nt{\tau_n\Theta} \in W$,

664: \end{itemize}

665: and $\Delta = 

666: \set{\nt{\tau\Theta} \rar

667: \ftau(\nt{\tau_1\Theta},\dots,\nt{\tau_n\Theta})

668: \mid \tau\Theta \in W}$.

669: \end{defi}

670: 

671: We put types in quotation marks to indicate 

672: that when looking at the grammar, types are just non-terminal symbols. 

673: Type graphs are defined as before.

674: In Fig.~\ref{type-graphs-fig}, we give some type graphs to

675: which we will refer frequently.

676: 

677: 

678: 

679: \setlength{\unitlength}{2.3mm}

680: \begin{figure}[t]

681: \begin{picture}(8,12)

682: \put(0,0){\makebox(8,2){$\vdots$}}

683: \put(0,2){\framebox(8,2){$\mathtt{c(c(c(U)))}$}}

684: \put(4,6){\vector(0,-1){2}}

685: \put(0,6){\framebox(8,2){$\mathtt{c(c(U))}$}}

686: \put(4,10){\vector(0,-1){2}}

687: {\linethickness{0.2\unitlength}

688: \put(0,10){\framebox(8,2){$\mathtt{c(U)}$}}

689: }

690: \end{picture}

691: \hfill

692: \begin{picture}(4,6)

693: \put(0,0){\framebox(2,2){$\tt U$}}

694: \put(1,4){\vector(0,-1){2}}

695: {\linethickness{0.2\unitlength}

696: \put(0,4){\framebox(4,2){$\mathtt{k(U)}$}}

697: }

698: \end{picture}

699: \hfill

700: \begin{picture}(8,9)

701: \put(1,0){\framebox(7,2){$\mathtt{int}$}}

702: \put(0,3){\framebox(6,2){$\mathtt{str}$}}

703: \put(1,7){\vector(0,-1){2}}

704: \put(7,7){\vector(0,-1){5}}

705: {\linethickness{0.2\unitlength}

706: \put(0,7){\framebox(8,2){$\mathtt{k(str)}$}}

707: }

708: \end{picture}

709: \hfill

710: \begin{picture}(6,7)

711: \put(0,0){\framebox(2,2){$\tt U$}}

712: \put(1,4){\vector(0,-1){2}}

713: {\linethickness{0.2\unitlength}

714: \put(0,4){\framebox(6,2){$\mathtt{list(U)}$}}

715: }

716: \curve(1,6, 2,8, 4,8, 5,6)

717: \put(5,6){\vector(1,-4){0}}

718: \end{picture}

719: \hfill

720: \begin{picture}(11,11)

721: \put(0,0){\framebox(2,2){$\tt V$}}

722: \put(1,4){\vector(0,-1){2}}

723: {\linethickness{0.2\unitlength}

724: \put(0,4){\framebox(6,2){$\mathtt{nest(V)}$}}

725: }

726: \put(1,8){\vector(0,-1){2}}

727: \put(5,6){\vector(0,1){2}}

728: \put(0,8){\framebox(11,2){$\mathtt{list(nest(V))}$}}

729: \curve(1,10, 4,12, 7,12, 10,10)

730: \put(10,10){\vector(1,-1){0}}

731: \end{picture}

732: \hfill

733: \begin{picture}(8,13)

734: \put(1,0){\framebox(7,2){$\mathtt{bal}$}}

735: \put(0,3){\framebox(6,2){$\mathtt{str}$}}

736: \put(0,6){\framebox(2,2){$\tt U$}}

737: \put(1,10){\vector(0,-1){2}}

738: \put(4,10){\vector(0,-1){5}}

739: \put(7,10){\vector(0,-1){8}}

740: {\linethickness{0.2\unitlength}

741: \put(0,10){\framebox(8,2){$\mathtt{table(U)}$}}

742: }

743: \curve(1,12, 3,14, 5,14, 6.9,12.1)

744: \put(6.9,12.1){\vector(2,-3){0}}

745: \end{picture}

746: %\hfill

747: %\begin{picture}(6,10)

748: %{\linethickness{0.2\unitlength}

749: %\put(0,0){\framebox(6,2){$\mathtt{elist(U)}$}}}

750: %\put(0,4){\framebox(2,2){$\tt U$}}

751: %\put(5,2){\vector(0,1){6}}

752: %\put(3,8){\vector(0,-1){6}}

753: %\put(1,2){\vector(0,1){2}}

754: %\put(1,8){\vector(0,-1){2}}

755: %\put(0,8){\framebox(6,2){$\mathtt{olist(U)}$}}

756: %\end{picture}

757: 

758: \begin{picture}(8,2)

759: \put(0,0){\makebox(8,0){(a)}}

760: \end{picture}

761: \hfill

762: \begin{picture}(5,2)

763: \put(0,0){\makebox(5,0){(b)}}

764: \end{picture}

765: \hfill

766: \begin{picture}(8,2)

767: \put(0,0){\makebox(8,0){(c)}}

768: \end{picture}

769: \hfill

770: \begin{picture}(6,2)

771: \put(0,0){\makebox(6,0){\texttt{LISTS}}}

772: \end{picture}

773: \hfill

774: \begin{picture}(11,2)

775: \put(0,0){\makebox(11,0){\texttt{NESTS}}}

776: \end{picture}

777: \hfill

778: \begin{picture}(8,2)

779: \put(0,0){\makebox(8,0){\texttt{TABLES}}}

780: \end{picture}

781: \caption{Some type graphs, with starting node highlighted\label{type-graphs-fig}}

782: \end{figure} 

783: 

784: It is also useful to have names and a notation for the relations

785: holding between the types in a type graph.

786: 

787: \begin{defi} \label{subterm-type-def}

788: A type $\sigma$ is a 

789: {\bf direct subterm type of} $\phi$ (denoted as $\sigma \subone \phi$) if

790:  there is $\ftau \in \mathcal{F}$ and a type substitution $\Theta$ such

791:  that $\appl{\Theta}{\tau} = \phi$ and $\appl{\Theta}{\tau_i} = \sigma$ for some $i \in

792:  \oneton$.  The transitive, reflexive closure of $\subone$ is

793:  denoted as $\sub$. 

794: If $\sigma \sub  \phi$, then $\sigma$ is a 

795: {\bf subterm type of} $\phi$. 

796: \end{defi}

797: 

798: We now discuss two problems related to the generalisation to

799: polymorphism, including that of finiteness mentioned above. 

800: 

801: \begin{ex}\label{type-graphs-ex}

802: Whenever we give a particular typed language, $\mathcal K$ is given

803: implicitly as the set of all type constructors occurring in the type

804: subscripts in $\mathcal F$.

805: 

806: One would hope that even if a typed language contains an

807: infinite set of types, the type graph taking a fixed type as starting

808: node should be finite. However, consider 

809: $\mathcal{F} =

810: \set{\mathtt{f_{c(c(U)) \rar c(U)}}}$. The type graph of

811: $\mathtt{c(U)}$ is shown in

812: Fig.~\ref{type-graphs-fig} (a). As can be seen, it is infinite.

813: \end{ex}

814: 

815: We impose the following restriction on any typed language to ensure finiteness.

816: 

817:  \vspace{0.5em}   

818: 

819: \noindent {\bf Reflexive Condition:}  For all $c \in \mathcal{K}$ and 

820: types $\sigma = c(\bar{\sigma}), \tau = c(\bar{\tau})$, 

821: if $\sigma \sub\tau$, 

822: then $\sigma$ is a sub``term'' (in the syntactic sense) of $\tau$.

823: 

824: \vspace{0.5em}   

825: 

826: Clearly, this condition is violated by the example above, where 

827:  $\mathtt{c(c(U)) \subone c(U)}$. With this condition in place, it 

828: is easy to see that any type graph for a given starting node is

829: finite. 

830: 

831: In the introduction we mentioned another problem, namely that the construction

832: of abstract domains should be ``truly parametric''. 

833: 

834: \begin{ex}\label{truly-parametric-ex}

835: Consider

836: $\mathcal{F} = \set{

837: \mathtt{f_{U\rar k(U)}},

838: \mathtt{g_{int \rar k(str)}}

839: }$.

840: Figure~\ref{type-graphs-fig} (b) shows the type

841: graph for $\mathtt{k(U)}$. Essentially, the type graph for any

842: instance $\mathtt{k}(\tau)$ is obtained by replacing the node

843: $\mathtt{k(U)}$ with $\mathtt{k}(\tau)$ and the node 

844: $\tt U$ with the type graph for $\tau$. However, there is one

845: exception to this: if $\tau = \mathtt{str}$, then the type graph is

846: the one shown in Fig.~\ref{type-graphs-fig} (c). For this

847: example, it would clearly be wrong to say that 

848: ``$\mathtt{k(U)}$ relates to $\tt U$ in the same way as 

849: $\mathtt{k(str)}$ relates to $\mathtt{str}$''.

850: \end{ex}

851: 

852: Again, we rule out this anomaly. First we define:

853: 

854: \begin{defi}\label{flat-def}

855: A {\bf flat type} is a type of the form $c(\bar{u})$, where 

856: $c \in \mathcal{K}$.

857: \end{defi}

858: 

859: We now impose the following condition on any typed language.

860: 

861: \vspace{0.5em}

862: 

863: \noindent {\bf Flat Range Condition:} For all $\ftau \in \mathcal{F}$,

864: $\tau$ is a flat type.

865: 

866: \vspace{0.5em}   

867: 

868: In Mercury (and also in {\em functional} languages such as ML or

869: Haskell), this condition is enforced by the

870: syntax. In G\"odel, it is possible to violate the

871: condition, but this can be regarded as an artefact of that syntax. 

872: 

873: Thus we assume from now on that any typed language we consider meets

874: the two conditions above. 

875: 

876: 

877: \subsection{Labelling~\cite{LS01}}\label{labelling-subsec}

878: Labellings can be used to characterise the degree of

879: instantiation of a term taking its type into account, i.e.,

880: analyse a term on a {\em per-role} basis~\cite{LS01}. 

881: 

882: \begin{defi}\label{labelling-def}

883: A variable $x$ in a term $t$ labels a non-terminal $N$ of a grammar

884: $\mathcal{G}$ if $S(t) \rar^* N(x)$, where $S$ is the starting

885: non-terminal of $\mathcal{G}$. 

886: 

887: We denote by $\zeta(S,N,t)$ the function

888: which returns the set of

889: variables $x$ such that $S(t) \rar^* N(x)$ (one could also write

890: $\zeta(\mathcal{G},N,t)$~\cite{LS01}).

891: \end{defi}

892: 

893: \begin{ex}\label{labelling-ex}

894: The grammar

895: $LL \rar\mathtt{nil} | \mathtt{cons}(L,LL),\;

896: L \rar\mathtt{nil} |\mathtt{cons}(E,L),\;\allowbreak

897: E \rar\mathtt{a} | \mathtt{b}$ 

898: accepts ground lists of lists of 

899: $\mathtt{a}$'s and $\mathtt{b}$'s.

900: Note that the use of $\mathtt{cons}$ and 

901: $\mathtt{nil}$ could be regarded as overloading, but this is not

902: forbidden by~\cite{LS01} as it is not in contradiction to the grammar

903: being deterministic. 

904: 

905: \setlength{\unitlength}{3mm}

906: \begin{figwindow}[0,r,%

907: {\mbox{\begin{picture}(11,4.5)%

908: {\linethickness{0.2\unitlength}

909: \put(1,0){\framebox(2,3){$LL$}}}%

910: \curve(3,2, 4,2.5, 4,4, 2.5,4, 2,3)%

911: \put(2,3){\vector(0,-1){0}}%

912: \put(3,1){\vector(1,0){2}}%

913: \put(5,0){\framebox(2,3){$L$}}%

914: \curve(7,2, 8,2.5, 8,4, 6.5,4, 6,3)%

915: \put(6,3){\vector(0,-1){0}}%

916: \put(7,1){\vector(1,0){2}}%

917: \put(9,0){\framebox(2,3){$E$}}%

918: \end{picture}}},%

919: {List of lists \label{listlist-type-graph-fig}}]

920: We use the usual list notation for ease of reading.

921: The type graph of $LL$ is shown in

922: Fig.~\ref{listlist-type-graph-fig}. 

923: We are interested in the labelling of all non-terminals reachable from 

924: $LL$. 

925: Let $t = [[\mathtt{a}],[\mathtt{b}]]$. Then 

926: $\zeta(LL,E,t) = \zeta(LL,L,t) = \zeta(LL,LL,t) = \emptyset$. 

927: Now let $t = [[\mathtt{a}],[\mathtt{X}]]$. Then 

928: $\zeta(LL,E,t) = \set{\mathtt{X}}$ and

929: $\zeta(LL,L,t) = \zeta(LL,LL,t) = \emptyset$.

930: Now let $t = [[\mathtt{a}],\mathtt{X}]$. Then

931: $\zeta(LL,E,t) = \emptyset$, 

932: $\zeta(LL,L,t) = \set{\mathtt{X}}$ and

933: $\zeta(LL,LL,t) = \emptyset$.

934: 

935: \end{figwindow}

936: \end{ex}

937: 

938: \subsection{Labelling and Polymorphism}\label{labelling-polymorphic-subsec}

939: We now want to adapt the idea of labelling to the case when we have

940: polymorphism. With polymorphism, one can have infinitely many types,

941: and even though the type graph for a fixed type as starting node is

942: finite, it can become arbitrarily large, i.e., it can have an

943: arbitrary number of non-terminals reachable from the starting node. 

944: Also, it would clearly be desirable to describe the labellings for say

945: $\mathtt{list(int)}, \mathtt{list(list(int))},\dots$ in a

946: uniform way. This motivates defining a hierarchy in the type

947: graph. 

948: 

949: \begin{defi} \label{typerelations-def}

950: A type $\sigma$ is a {\bf recursive type of $\phi$} 

951: (denoted as $\sigma \rec \phi$) if 

952: $\sigma \sub \phi$ and $\phi \sub \sigma$.

953: %If $\{ \sigma_1,\dots,\sigma_m \} = 

954: %\{ \sigma \mid \sigma \rec \phi,\ \sigma\neq\phi \}$, 

955: %and 

956: %$\sigma_j \prec \sigma_{j+1}$ 

957: %for all $j \in \{1, \dots, m-1 \}$, 

958: %we write $\Rec(\phi)$ for the tuple

959: %$\langle  \sigma_1,\dots,\sigma_m \rangle$.

960: We write $\Rec(\phi)$ for the tuple of recursive types of $\phi$ 

961: other than $\phi$ itself, ordered by $\prec$ (see Sec.~\ref{prelim-sec}).

962: 

963: A type

964: $\sigma$ is a {\bf non-recursive subterm type (NRS) of $\phi$} 

965: (denoted as $\sigma \nrs \phi$)

966: if $\phi \notsub \sigma$ and there is

967: a type $\tau$ such that 

968: $\sigma \subone \tau$ and $\tau \rec \phi$. 

969: %If $\{ \sigma_1,\dots,\sigma_m \} = 

970: %\{ \sigma \mid \sigma \nrs \phi \}$, 

971: %and 

972: %$\sigma_j \prec \sigma_{j+1}$ 

973: %for all $j \in \{1, \dots, m-1 \}$, 

974: %we write $\Nrs(\phi)$ for the tuple

975: %$\langle  \sigma_1,\dots,\sigma_m \rangle$.

976: We write $\Nrs(\phi)$ for the tuple of non-recursive subterm types of

977: $\phi$, 

978: ordered by $\prec$.

979: \end{defi}

980: 

981: It follows immediately from the definition that, for any types $\phi,\sigma$, 

982: we have $\phi \rec \phi$ and,

983: if $\sigma \nrs \phi$, then $\sigma \not\rec \phi$.

984: Consider the type graph for $\phi$.

985: The recursive types of $\phi$ are all the types in the

986: strongly connected component (SCC) containing $\phi$.

987: The non-recursive

988: subterm types of $\phi$ are all the types $\sigma$ not in the SCC but

989: such that there is an edge from the SCC containing $\phi$ to $\sigma$.

990: 

991: \begin{ex}\label{typerelations-ex}

992: Consider Fig.~\ref{type-graphs-fig}.

993: Let

994: $\mathcal{F}_\mathtt{LISTS} = \set{\mathtt{nil_{\rar list(U)}, 

995:                             cons_{U,list(U) \rar list(U)}}}$.

996: We have

997: $\mathtt{list(U)} \rec \mathtt{list(U)}$ and

998: $\mathtt{U} \nrs \mathtt{list(U)}$. 

999: 

1000: Let

1001: $\mathcal{F}_\mathtt{NESTS} = \mathcal{F}_\mathtt{LISTS} \cup \set{\mathtt{

1002:                             e_{V \rar nest(V)},

1003:                             n_{list(nest(V)) \rar nest(V)}}}$. 

1004: The \texttt{NESTS} language implements {\em rose trees}~\cite{M88},

1005: i.e., trees where the number of children of each node is not fixed. 

1006: We have

1007: $\mathtt{list(nest(V))} \rec \mathtt{nest(V)}$ and

1008: $\mathtt{nest(V)} \rec \mathtt{nest(V)}$ and

1009: $\mathtt{V} \nrs \mathtt{nest(V)}$. 

1010: 

1011: Suppose $\mathcal{F}_\mathtt{STRINGS}$ contains all strings with 

1012: $\rar\mathtt{str}$ as type subscript.

1013: Let 

1014: $\mathcal{F}_\mathtt{TABLES} = \mathcal{F}_\mathtt{STRINGS} \cup$

1015: \[

1016: \{\mathtt{

1017: lh_{\rar bal}, rh_{\rar bal}, eq_{\rar bal}, null_{\rar table(U)}},

1018: \mathtt{node_{table(U),str,U,bal,table(U) \rar table(U)}}\},

1019: \] 

1020:  The type $\mathtt{bal}$ contains three constants

1021:  representing balancing information. We have 

1022: $\mathtt{table(U)} \rec \mathtt{table(U)}$ and

1023: $\Nrs(\mathtt{table(U)}) = 

1024: \langle \mathtt{U}, \mathtt{bal}, \mathtt{str} \rangle$.

1025: 

1026: An NRS of a flat type is often just a parameter of that type, as in 

1027: $\mathtt{U} \nrs \mathtt{list(U)}$. 

1028: However, this is not always the case, as witnessed by

1029: $\mathtt{str} \nrs \mathtt{table(U)}$.

1030: \end{ex}

1031: 

1032: Instead of looking at the labellings of \emph{all} non-terminals

1033: reachable from some starting node without distinction~\cite{LS01}, we classify

1034: them according to the recursive types and the NRSs of that node. This

1035: will be reflected in the construction of abstract domains.

1036: 

1037: Definition~\ref{typerelations-def} is obviously applicable in particular in the

1038: monomorphic case and thus to the grammars as in~\cite{LS01}.

1039: Figure~\ref{listlist-type-graph-fig} shows that the recursive types

1040: and NRSs may not be all types reachable from a starting node. In

1041: that example, we have $LL\rec LL$ and  $L\nrs LL$. 

1042: In the approach of~\cite{LS01}, we may also be

1043: interested in $\zeta(LL,E,t)$ for some term $t$, so in the labellings

1044: of $E$. In the approach proposed here, the domain construction for

1045: $LL$ depends on $E$ only indirectly, via the abstract domain for $L$. 

1046: Without such an inductive approach to domain construction, we would

1047: not know how to deal with polymorphism. 

1048: 

1049: The key to devising a ``parametric'' abstract domain construction is

1050: to focus on type constructors, or equivalently, on flat types

1051: $c(\vect{u})$. So for example, we should focus on $\mathtt{list(U)}$

1052: and not a particular instance such as $\mathtt{list(int)}$. This

1053: may not be surprising, but it has two consequences which may not be

1054: obvious.

1055: 

1056: First, note that the relation $\nrs$ is not stable under instantiation

1057: of types. This can be seen by comparing \texttt{LISTS} with

1058: \texttt{NESTS}. We have $\mathtt{U} \nrs \mathtt{list(U)}$, but

1059: $\mathtt{nest(V)} \rec \mathtt{list(nest(V))}$. The abstract

1060: domain for $\mathtt{list(nest(V))}$ however, being derived from 

1061: the abstract domain for $\mathtt{list(U)}$, must relate to

1062: $\mathtt{nest(V)}$ as if $\mathtt{nest(V)}$ was an NRS of 

1063: $\mathtt{list(nest(V))}$. In contrast, the abstract domain for

1064: $\mathtt{nest(V)}$ must reflect that 

1065: $\mathtt{list(nest(V))} \rec \mathtt{nest(V)}$. 

1066: One could paraphrase this by saying: 

1067: \texttt{LISTS} does not know about \texttt{NESTS}, but 

1068: \texttt{NESTS} does know about \texttt{LISTS}. 

1069: 

1070: The second consequence can be illustrated using \texttt{TABLES}. The type

1071: $\mathtt{table(U)}$ has three NRSs, and each of them will be dealt 

1072: with in the construction of the abstract domain. However, the instance 

1073: $\mathtt{table(string)}$ has only two NRSs, as $\mathtt{U}$

1074: becomes instantiated to $\mathtt{string}$. The

1075: domain for $\mathtt{table(\tau)}$ will be based on assuming 

1076: {\em three} NRSs, i.e., it will deal with the value and the key

1077: arguments separately, even if by coincidence $\tau$ is equal to

1078: $\mathtt{string}$.  

1079: 

1080: We now define a function $\mathcal{Z}$ in analogy to $\zeta$.  In the

1081: approach of~\cite{LS01}, we could safely identify a grammar with its

1082: starting non-terminal. In what follows, we will always assume a

1083: grammar $\mathcal{G}(\phi)$ where $\phi$ is flat 

1084: (Def.~\ref{corresponding-grammar-def}). However, it is also 

1085: useful to consider productions of that grammar starting from

1086: some other non-terminal than the ``official'' starting non-terminal.

1087: Therefore

1088: $\mathcal{Z}$ has {\em four} arguments, the additional first one

1089: specifying the grammar and the second the starting symbol. 

1090: 

1091: Unlike $\zeta$, the function $\mathcal{Z}$ also collects non-variable terms. 

1092: 

1093: \begin{defi}\label{my-labelling-def}

1094: Let $\phi$ be a flat type, $\tau$ be a type such that 

1095: $\tau\rec\phi$, and $\sigma$ a type such that either 

1096: $\sigma\rec\phi$ or $\sigma\nrs\phi$. 

1097: 

1098: We denote by $\mathcal{Z}(\phi,\tau,\sigma,t)$ the function

1099: which returns the set of all terms $s$ such that 

1100: $\nt{\tau}(t) \rar^* \nt{\sigma}(s)$ in the grammar $\mathcal{G}(\phi)$.

1101: \end{defi}

1102: 

1103: The function $\mathcal{Z}$ is lifted to sets (in the fourth argument) in the obvious way.

1104: 

1105: \begin{ex}\label{my-labelling-ex}

1106: Let 

1107: $\mathcal{F} = \mathcal{F}_\mathtt{LISTS} \cup 

1108: \set{\mathtt{a_{char}}, \mathtt{b_{char}}}$. 

1109: We have

1110: \begin{eqnarray*}

1111: \mathcal{Z}(\mathtt{list(U)}, \mathtt{list(U)}, \mathtt{list(U)}, [\mathtt{a},\mathtt{X}]) & = &

1112: \set{[\mathtt{a},\mathtt{X}], [\mathtt{X}], []}\\

1113: \mathcal{Z}(\mathtt{list(U)}, \mathtt{list(U)}, \mathtt{U},

1114: [\mathtt{a},\mathtt{X}]) & = & 

1115: \set{\mathtt{a, X}}\\[1ex]

1116: \mathcal{Z}(\mathtt{list(U)}, \mathtt{list(U)},\mathtt{list(U)}, [[\mathtt{a}],[\mathtt{X}]]) & = & 

1117: \set{[[\mathtt{a}], [\mathtt{X}]], [[\mathtt{X}]], []}\\ 

1118: \mathcal{Z}(\mathtt{list(U)}, \mathtt{list(U)},\mathtt{U},[[\mathtt{a}], [\mathtt{X}]]) & = & 

1119: \set{[\mathtt{a}], [\mathtt{X}]}\\[1ex]  

1120: \mathcal{Z}(\mathtt{list(U)}, \mathtt{list(U)}, \mathtt{list(U)},\mathtt{[[a]|X]}) & = & 

1121: \set{\mathtt{[[a]|X]}, \mathtt{X}}\\

1122: \mathcal{Z}(\mathtt{list(U)}, \mathtt{list(U)}, \mathtt{U},\mathtt{[[a]|X]}) & = & 

1123: \set{[\mathtt{a}]}.  

1124: \end{eqnarray*}

1125: Note that unlike $\zeta$ (Ex.~\ref{labelling-ex}), 

1126: $\mathcal{Z}$ cannot be used to 

1127: extract from the term $[[\mathtt{a}],[\mathtt{X}]]$ the subterm

1128: $\mathtt{X}$ directly.  

1129: 

1130: Now consider the \texttt{NESTS} example, assuming that

1131: $\mathcal{F}_\mathtt{NESTS}$ is augmented with the integers

1132: $1_\mathtt{int},\dots$. We have

1133: \begin{eqnarray}

1134: \mathcal{Z}(\mathtt{nest(V), nest(V), nest(V), n([e(7)])}) & = &

1135: \set{\mathtt{n([e(7)]), e(7)}}\nonumber\\

1136: \mathcal{Z}(\mathtt{nest(V), nest(V), list(nest(V)), n([e(7)])}) & = &

1137: \set{\mathtt{[e(7)], []}}\nonumber\\

1138: \mathcal{Z}(\mathtt{nest(V), nest(V), V, n([e(7)])}) & = &

1139: \set{\mathtt{7}}\nonumber\\[1ex]

1140: \mathcal{Z}(\mathtt{nest(V), list(nest(V)), nest(V), [n([e(7)])]}) & = &

1141: \set{\mathtt{n([e(7)]), e(7)}}\label{list-as-nest-1}\\

1142: \mathcal{Z}(\mathtt{nest(V), list(nest(V)), list(nest(V)), [n([e(7)])] }) & = &

1143: \set{\mathtt{[n([e(7)])], [e(7)], []}}\label{list-as-nest-2}\\

1144: \mathcal{Z}(\mathtt{nest(V), list(nest(V)), V, [n([e(7)])]}) & = &

1145: \set{\mathtt{7}}\label{list-as-nest-3}\\[1ex]

1146: \mathcal{Z}(\mathtt{list(U), list(U), list(U), [n([e(7)])]}) & = &

1147: \set{\mathtt{[n([e(7)])], []}}\label{list-as-list-1}\\

1148: \mathcal{Z}(\mathtt{list(U), list(U), U, [n([e(7)])]}) & = &

1149: \set{\mathtt{n([e(7)])}}\label{list-as-list-2}\\[1ex]

1150: \mathcal{Z}(\mathtt{nest(V), nest(V), V, e(7)}) & = &

1151: \set{\mathtt{7}}\label{nest-plain}

1152: \end{eqnarray}

1153: Note the difference between the labellings obtained for 

1154: $\mathtt{[e(7)]}$ depending on whether we use the grammar for 

1155: $\mathtt{nest(V)}$ (\ref{list-as-nest-1}, \ref{list-as-nest-2}, \ref{list-as-nest-3}), or

1156: the grammar for $\mathtt{list(U)}$ (\ref{list-as-list-1}, \ref{list-as-list-2}).

1157: \end{ex}

1158: 

1159: %PATCH 1

1160: 

1161: \begin{rmlemma}\label{subterm-label-lem}

1162: Let $\phi$ and $\tau$ be flat types such that 

1163: $\appl{\Theta}{\tau} \rec \phi$ for some  $\Theta$.

1164: Let $t = \ftau(t_1,\dots,t_n)$ be a term such that

1165: $\_\vdash t:\tau\Theta\Theta'$ for some $\Theta'$.

1166: Then

1167: \[

1168: \mathcal{Z}(\phi,\tau\Theta,\sigma,t) =

1169: \left\{

1170: \begin{array}{llll}

1171: & \set{t_i \mid \tau_i\Theta = \sigma} \cup & 

1172: \displaystyle

1173: \bigcup_{\tau_i\Theta\rec\phi} \mathcal{Z}(\phi,\tau_i\Theta,\sigma,t_i) \ &

1174: \mbox{if}\ \sigma\nrs\phi\\

1175:  & & 

1176: \displaystyle

1177: \bigcup_{\tau_i\Theta\rec\phi} \mathcal{Z}(\phi,\tau_i\Theta,\sigma,t_i) &

1178: \mbox{if}\ \sigma\rec\phi, \sigma\neq\phi\\

1179: \set{t} \cup & & 

1180: \displaystyle

1181: \bigcup_{\tau_i\Theta\rec\phi} \mathcal{Z}(\phi,\tau_i\Theta,\sigma,t_i) &

1182: \mbox{if}\ \sigma=\phi.

1183: \end{array}

1184: \right.

1185: \]

1186: \end{rmlemma}

1187: 

1188: \begin{pf}

1189: Follows from the fact that for each $i\in\oneton$, we have

1190: $\nt{\tau\Theta}(t) \rar \nt{\tau_i\Theta}(t_i)$ in 

1191: $\mathcal{G}(\phi)$. 

1192: \end{pf}

1193: 

1194: 

1195: \section{Abstract Terms}\label{abstract-terms-sec}

1196: In this section, we define an {\em abstraction} of terms using the

1197: notions of recursive type and non-recursive subterm type. This amounts

1198: to a generalisation of~\cite{CL00}.

1199: 

1200: 

1201: \subsection{Abstract Domains and Terms}\label{abstract-terms-subsec}

1202: We first introduce the formalism of {\em set logic programs} shown to be

1203: powerful for program analyses~\cite{LS01}. Consider a language

1204: based on a set of variables $\mathcal{V}$ and a set of functions

1205: $\mathcal{F}^\oplus = \set{\emptyset,\oplus}$, where

1206: $\emptyset/0$ represents the empty set and 

1207: $\oplus/2$ is a set constructor. {\em Set expressions} are elements of

1208: the

1209: term algebra $\mathcal{T}(\mathcal{F}^\oplus,\mathcal{V})$ modulo the

1210: ACI1 equality theory, consisting of:

1211: \begin{equation}

1212: \label{aci1-eq}

1213: \begin{array}{rcllrcll}

1214: (x\oplus y) \oplus z & \!=\! & x \oplus (y\oplus z) \!\! &

1215: \mbox{(associativity)} &

1216: x\oplus x & \!= \!& x &

1217: \mbox{(idempotence)} \\

1218: x \oplus y & \!=\! & y \oplus x &

1219: \mbox{(commutativity)}  &

1220: x \oplus \emptyset & \!=\! & x &

1221: \mbox{(unity)}

1222: \end{array}

1223: \end{equation}

1224: Lagoon and Stuckey~\cite{LS01} now proceed by regarding each

1225: non-terminal in the grammar corresponding to a variable $x$ as

1226: an {\em abstract variable}. The instantiation of that abstract

1227: variable obtained from the execution of the abstract program gives us

1228: information about the labels of the non-terminal after the concrete

1229: execution. 

1230: 

1231: %\comment{Maybe those three paragraphs can be shortened, noting that 

1232: %what we do very much follows~\cite{CL00}.}

1233: %Lagoon and Stuckey now proceed as follows. First, it must be noted that

1234: %each program variable $X$ is associated with a grammar

1235: %$\mathcal{G}_X$, whose non-terminals are uniquely marked as belonging

1236: %to $X$. In the abstraction, each non-terminal in $\mathcal{G}_X$ 

1237: %becomes an ``abstract variable''. For example, assuming that $X$ has

1238: %the grammar in Ex.~\ref{labelling-ex} associated with it, then if the

1239: %execution of the abstract program results in $LL = \emptyset$, this

1240: %means that $\zeta(LL,LL,X\theta) = \emptyset$, where $\theta$ is the

1241: %substitution obtained from the concrete execution.

1242: 

1243: %We prefer to define the abstraction in a slightly different

1244: %way. First, we do not introduce new variables; the variables of the

1245: %abstraction of a clause are the variables of the original clause.  

1246: %The essential reason for this is that in the presence of polymorphism, 

1247: %any polymorphic instance of a clause can be used in a program

1248: %execution, and the number of abstract variables we would have to 

1249: %introduce would somehow have to depend on that instance. 

1250: 

1251: We do not see how this approach could work in the presence of

1252: polymorphism. Instead, we follow~\cite{CL00}.

1253: We now introduce new function symbols, one $c^\mathcal{A}$ for

1254: each type constructor $c\in\mathcal{K}$, in addition to $\emptyset$

1255: and $\oplus$. These are used to collect the information corresponding

1256: to the different non-terminals in a structure, which we call 

1257: {\em abstract term}. The arity of $c^\mathcal{A}$ is given by the

1258: arity of $\Nrs(c(\bar{u}))$ plus the arity of $\Rec(c(\bar{u}))$.

1259: 

1260: 

1261: \begin{defi}\label{domain-def}\label{alpha-def}

1262: We define

1263: \[

1264: \mathcal{F}^\mathcal{A} := 

1265: \mathcal{F}^\oplus \cup

1266: \set{c^\mathcal{A}/m \mid c\in\mathcal{K},\ 

1267: m = \#(\Nrs(c(\bar{u}))) + \#(\Rec(c(\bar{u})))}.

1268: \]

1269: Now let $\tau = c(\bar{u})$, 

1270: $\Nrs(\tau) = \langle \rho_1,\dots,\rho_{m'} \rangle$, and

1271: $\Rec(\tau) = \langle \rho_{m'+1},\dots,\rho_m \rangle$.

1272: For a term 

1273: $t = \ftau(t_1,\dots,t_n)$, we define

1274: \[

1275: \alpha(t) = 

1276: c^\mathcal{A}

1277: \left(

1278: \bigoplus_{\tau_i=\rho_1} \alpha(t_i),

1279: \dots,

1280: \bigoplus_{\tau_i=\rho_m} \alpha(t_i)

1281: \right)

1282: \oplus

1283: \bigoplus_{\tau_i=\tau} \alpha(t_i).

1284: \]

1285: For a variable $x$ we define $\alpha(x) = x$.

1286: We call the image of $\alpha$ the {\bf domain of abstract terms}, or

1287: simply the {\bf abstract domain}.

1288: \end{defi}

1289: 

1290: In~\cite{CL96}, the abstraction function is denoted $\mathit{type}$,

1291: and it is essentially a special case of the above definition for 

1292: $\#(\Nrs(c(\bar{u})))  = 1$ and $\#(\Rec(c(\bar{u}))) = 0$.

1293: Using our terminology, they assume that there is a

1294: function, which they denote by $\alpha$, returning for each 

1295: $f_{\dots\rar c(u)}$ the type constructor $c$; moreover, there is a

1296: function $\pi$ returning the set of argument positions of $f$ that have

1297: declared type $c(u)$, and all other argument positions are assumed to

1298: have declared type $u$. However, since their typing is descriptive,

1299: $\alpha$ and $\pi$ have to be provided by the user.

1300: 

1301: \begin{ex}\label{alpha-ex}

1302: Consider again Ex.~\ref{my-labelling-ex}.

1303: \[

1304: \begin{array}{rclcl}

1305: \alpha(\mathtt{7}) & = &

1306: \mathtt{int}^\mathcal{A}\\

1307: \alpha(\mathtt{[7]}) & = &

1308: \mathtt{list^\mathcal{A}(\alpha(7)) \oplus \alpha(nil)} & = & 

1309: \mathtt{list^\mathcal{A}(int^\mathcal{A}) \oplus list^\mathcal{A}(\emptyset)}\\

1310: \alpha(\mathtt{e(7)}) & = &

1311: \mathtt{nest^\mathcal{A}(\alpha(7),\emptyset)} & = & 

1312: \mathtt{nest^\mathcal{A}(int^\mathcal{A},\emptyset)}\\

1313: \alpha(\mathtt{n([e(7)])}) & = &

1314: \mathtt{nest^\mathcal{A}(\emptyset,\alpha([e(7)]))} & = & 

1315: \mathtt{nest^\mathcal{A}(\emptyset,list^\mathcal{A}(nest^\mathcal{A}(int^\mathcal{A},\emptyset)))}.

1316: \end{array}

1317: \]

1318: \end{ex}

1319: 

1320: Note how it comes into play that the empty $\bigoplus$-sequence is

1321: naturally defined as  the neutral element $\emptyset$. There

1322: is a notable difference between~\cite{CL96} and~\cite{CL00} at this point.

1323: In the latter, there is no neutral element. This means

1324: in particular that $\mathtt{nil}$ cannot be abstracted as 

1325: $\mathtt{list(\emptyset)}$. Instead, it is abstracted as

1326: $\mathtt{nil}$, and as a consequence, the list $\mathtt{[7]}$ is abstracted as 

1327: $\mathtt{list(int) \oplus nil}$. While it is argued that such an

1328: abstraction simplifies the implementation of abstract unification, we believe that an

1329: object $\mathtt{list(int) \oplus nil}$ mixes types/abstract terms on

1330: the one hand and concrete terms on the other hand in a way which is 

1331: undesirable.

1332: 

1333: In fact, from the design of our abstract domains and the fact that we

1334: are analysing prescriptively typed programs, it follows that 

1335: whenever an expression

1336: $c^\mathcal{A}(\dots) \oplus {c'}^\mathcal{A}(\dots)$ occurs, then

1337: $c=c'$. This also explains why in the definition of $\alpha$, the

1338: abstraction of those $t_i$ such that $\tau_i\rec\tau$ but 

1339: $\tau_i\neq\tau$ is included in reserved argument positions of 

1340: $c^\mathcal{A}(\dots)$, whereas the abstraction of those $t_i$ 

1341: such that $\tau_i=\tau$ is directly conjoined (using $\oplus$) with

1342: the whole expression $c^\mathcal{A}(\dots)$.

1343: 

1344: Looking at Ex.~\ref{alpha-ex}, one might expect that 

1345: $\mathtt{list^\mathcal{A}(int^\mathcal{A}) \oplus list^\mathcal{A}(\emptyset)}$

1346: can be simplified to

1347: $\mathtt{list^\mathcal{A}(int^\mathcal{A})}$. Maybe less obvious, one

1348: might also expect that the abstract term

1349: $

1350: \mathtt{nest^\mathcal{A}(\emptyset,list^\mathcal{A}(nest^\mathcal{A}(int^\mathcal{A},\emptyset)))}

1351: $

1352: can be simplified to 

1353: $\mathtt{nest^\mathcal{A}(int^\mathcal{A},\emptyset)}$. We now extend

1354: ACI1 by further axioms for this purpose.

1355: 

1356: \begin{defi}\label{axioms-def}

1357: For each 

1358: $c^\mathcal{A}/m \in \mathcal{F}^\mathcal{A}$, the  

1359: {\bf distributivity axiom} is defined as follows:

1360: \begin{equation}

1361: \label{distr-eq}

1362: c^\mathcal{A} (x_1,\dots,x_m) \oplus

1363: c^\mathcal{A} (y_1,\dots,y_m) = 

1364: c^\mathcal{A} (x_1 \oplus y_1,\dots, x_m \oplus y_m) 

1365: \end{equation}

1366: Moreover, consider a flat type 

1367: $\phi=d(\vect{v})$ such that 

1368: $\Nrs(\phi) = \langle \sigma_1,\dots,\sigma_{l'}\rangle$,

1369: $\Rec(\phi) = \langle \sigma_{l'+1},\dots,\sigma_{l}\rangle$.

1370: For each $j\in\set{{l'}+1,\dots,l}$, we have

1371: $\sigma_j = \tau\Theta$ for some flat type 

1372: $\tau = c(\vect{u})$ and some $\Theta$.  Suppose

1373: $\Nrs(\tau) = \langle \rho_1,\dots,\rho_{m'}\rangle$,

1374: $\Rec(\tau) = \langle \rho_{m'+1},\dots,\rho_{m}\rangle$,

1375: We define the 

1376: {\bf extraction axiom} for $d^\mathcal{A}$ and $\sigma_j$ as follows:

1377: \[

1378: \label{extraction-eq}

1379: \begin{array}{l}

1380: d^\mathcal{A}(x_1,\dots,x_{j-1},

1381:               c^\mathcal{A}(y_1,\dots,y_m)\oplus x_j,

1382:               x_{j+1},\dots,x_l) = \\ 

1383: \displaystyle

1384: d^\mathcal{A}\!\left(\!

1385:               x_1\oplus\!\!\!\bigoplus_{\rho_k\Theta = \sigma_1}\!\!\! y_k,

1386:               \;\dots,\;

1387:               x_{j-1}\oplus\!\!\!\!\!\bigoplus_{\rho_k\Theta = \sigma_{j-1}}\!\!\!\!\! y_k,

1388:               \;x_j,\;

1389:               x_{j+1}\oplus\!\!\!\!\!\bigoplus_{\rho_k\Theta = \sigma_{j+1}}\!\!\!\!\! y_k,

1390:               \;\dots,\;

1391:               x_m\oplus\!\!\!\bigoplus_{\rho_k\Theta = \sigma_l}\!\!\! y_k

1392:               \! \right) \\

1393: \multicolumn{1}{r}{\displaystyle \oplus

1394:               \bigoplus_{\rho_k\Theta = \phi} y_k.}

1395: \end{array}

1396: \]

1397: Let {\bf ACI1DE} be the theory given by the axioms in~(\ref{aci1-eq}) and

1398: the distributivity and extraction axioms. We abbreviate ACI1DE by 

1399: {\bf \theory} and denote equality modulo \theory\ as $=_\mathrm{\theory}$.

1400: \end{defi}

1401: 

1402: Note that applying a distributivity or extraction axiom from left to

1403: right decreases the number of occurrences of function symbols by 1.

1404: 

1405: \begin{ex}\label{extractor-ex}

1406: Consider \texttt{LISTS}, \texttt{NESTS}, respectively. 

1407: The extraction axiom for $\mathtt{nest(V)}$ and $\mathtt{list(nest(V))}$

1408: is

1409: \[

1410: \mathtt{nest}^\mathcal{A}(x_1,\mathtt{list}^\mathcal{A}(y)\oplus x_2)

1411: = 

1412: \mathtt{nest}^\mathcal{A}(x_1, x_2) \oplus y.

1413: \]

1414: In \theory, we have

1415: \[

1416: \begin{array}{l}

1417: \mathtt{list^\mathcal{A}(int^\mathcal{A}) \oplus list^\mathcal{A}(\emptyset)}

1418: =_\mathrm{\theory} 

1419: \mathtt{list^\mathcal{A}(int^\mathcal{A}\oplus \emptyset)} 

1420: =_\mathrm{\theory} 

1421: \mathtt{list^\mathcal{A}(int^\mathcal{A})} \\ 

1422: \mathtt{nest^\mathcal{A}(\emptyset,list^\mathcal{A}(nest^\mathcal{A}(int^\mathcal{A},\emptyset)))} 

1423: =_\mathrm{\theory} 

1424: \mathtt{nest^\mathcal{A}(\emptyset,\emptyset)\oplus nest^\mathcal{A}(int^\mathcal{A},\emptyset)}

1425: =_\mathrm{\theory} \\ 

1426: \multicolumn{1}{r}{

1427: \mathtt{nest^\mathcal{A}(int^\mathcal{A},\emptyset)}.}

1428: \end{array}

1429: \]

1430: \end{ex}

1431: 

1432: In~\cite{CL00}, it is mentioned that one might have chosen to add a

1433: distributivity axiom but the authors argue the case for not doing

1434: so. The extraction axiom has no equivalent in~\cite{CL00}.

1435: 

1436: \subsection{Normal Abstract Terms}

1437: \label{normal-abstract-terms-subsec}

1438: Following~\cite{CL00}, we have defined the abstraction by structural

1439: induction on a term. This definition is a good basis for our analysis,

1440: but it is still unsatisfactory: as it is stated (i.e.~without

1441: applying any axioms), even for ground terms, the abstraction of a term

1442: is proportional in size to the term itself; consequently, the

1443: abstraction is not in a form that makes it convenient to read any

1444: properties of the concrete term from it.

1445: 

1446: We first show that using \theory, any abstract term can be converted in

1447: a normal form. To this end, it is useful to view abstract terms as

1448: typed terms according to the rules of Table~\ref{rules-tab}. 

1449: For each $\tau = c(\vect{u})$ with 

1450: $\Nrs(\tau) = \langle \rho_1,\dots,\rho_{m'} \rangle$ and

1451: $\Rec(\tau) = \langle \rho_{m'+1},\dots,\rho_m \rangle$, we 

1452: declare 

1453: $c^\mathcal{A}_{\rho_1,\dots,\rho_m \rar \tau}$. 

1454: Moreover, we declare $\emptyset_{\rar u}$ and

1455: $\oplus_{u,u\rar u}$.\footnote{These declarations violate the Simple

1456: Range Condition, and in any case would not be permissible in any

1457: existing typed programming language since a range type must not be a 

1458: parameter. However, this causes no problems for our theoretical 

1459: considerations.}

1460: Those declarations are designed exactly so that the following

1461: proposition holds.

1462: 

1463: \begin{propo}\label{abstract-nrs-rec-prop}

1464: The $\nrs$- and $\rec$-relations based on the declared types of 

1465: the ``abstract functions'' in $\mathcal{F^A}$ are the same as 

1466: the  $\nrs$- and $\rec$-relations based on $\mathcal{F}$.

1467: \end{propo}

1468: 

1469: To distinguish type judgements in the concrete

1470: and abstract language, we use $\vdash^\mathcal{A}$ for the latter.

1471: The following proposition says that the abstraction of a term

1472: has the same type as the concrete term itself. Its proof is

1473: straightforward by structural induction.

1474: 

1475: \begin{propo}\label{abstract-term-is-typed-prop}

1476: If $\Gamma\vdash t:\tau$ then $\Gamma\vdash^\mathcal{A} \alpha(t) : \tau$.

1477: \end{propo}

1478: 

1479: The next lemma says that application of the equality axioms

1480: preserves well-typing. The interesting axiom is the extraction axiom.

1481: 

1482: \begin{rmlemma}\label{axioms-preserve-well-typing-lem}

1483: If $\Gamma\vdash^\mathcal{A} a:\tilde{\tau}$ and $a =_\mathrm{\theory} b$ then

1484: $\Gamma\vdash^\mathcal{A} b:\tilde{\tau}$.

1485: \end{rmlemma}

1486: 

1487: \begin{pf}

1488: We only consider the extraction axiom. Assume the notations of

1489: Def.~\ref{axioms-def}, and consider an abstract term 

1490: \[

1491: a =  d^\mathcal{A}(b_1,\dots,b_{j-1},

1492:               c^\mathcal{A}(a_1,\dots,a_m)\oplus b_j,

1493:               b_{j+1},\dots,b_l)

1494: \] 

1495: where

1496: $ \_ \vdash^\mathcal{A} a :\phi\Theta'$

1497: for some $\Theta'$ (note that the typing rules are such that $a$

1498:  must have a type that is an instance of $\phi$, but not

1499: necessarily $\phi$ itself). 

1500: By the rules of Table~\ref{rules-tab}, we must have

1501: $\_ \vdash^\mathcal{A} b_{j'}: \sigma_{j'}\Theta'$ for all $j'\in\onetol$ and

1502: $\_ \vdash^\mathcal{A} a_k: \rho_k\Theta\Theta'$ for all $k\in\onetom$.

1503: Therefore it follows that for $j'\in\onetol\setminus\set{j}$, we have

1504: \[

1505: \_\vdash^\mathcal{A} 

1506: \left(

1507: b_{j'}\oplus\bigoplus_{\rho_k\Theta = \sigma_{j'}} a_k

1508: \right) : \sigma_{j'}\Theta',\ 

1509: \mbox{

1510: and we also have}\ 

1511: \_\vdash^\mathcal{A} 

1512: \left(

1513: \bigoplus_{\rho_k\Theta = \phi} a_k

1514: \right) : \phi\Theta'.

1515: \]

1516: This implies that if $b$ is obtained from $a$ by applying the

1517: extraction axiom in the $j$th position, then 

1518: $ \_ \vdash^\mathcal{A} b :\phi\Theta'$.

1519: \end{pf}

1520: 

1521: We now define normal forms for abstract terms. 

1522: To simplify the

1523: notation, we denote a variable sequence $x_1\oplus\dots\oplus x_n$ as 

1524: $x^\oplus$, and of course, this is $\emptyset$ if $n=0$.

1525: Note that the following definition is by structural induction: a

1526: normal abstract term for $\tau\Theta$ is defined based on a normal

1527: abstract term for some $\tau_i\Theta$. The well-foundedness of this

1528: induction is not obvious but has been stated in~\cite[Lemma 4.3]{SHK00}.

1529: 

1530: \begin{defi}\label{normal-form-def}

1531: For a parameter, the only {\bf normal abstract term} is $\emptyset$.

1532: 

1533: Now let $\tau=c(\vect{u})$ be a flat type such that 

1534: $\Nrs(\tau) = \langle\rho_{1},\dots,\rho_{m'}\rangle$ and

1535: $\Rec(\tau) = \langle \rho_{m'+1},\dots,\rho_m \rangle$, and $\Theta$ be

1536: any type substitution. A {\bf normal abstract term for $\tau\Theta$}

1537: is $\emptyset$ or of the form

1538: $c^\mathcal{A}(a_1 \oplus x^\oplus_1 ,\dots,

1539:                a_{m'} \oplus x^\oplus_{m'}, 

1540:                x^\oplus_{m'+1},\dots,x^\oplus_m) \oplus x^\oplus$, where

1541: for each $i\in\set{1,\dots,m'}$, $a_i$ is a normal abstract term for

1542: $\rho_i\Theta$. 

1543: \end{defi}

1544: 

1545: Note that in a normal abstract term, the ``second half'' of argument

1546: positions, i.e., those corresponding to recursive subterm types of

1547: $\tau$ other than $\tau$ itself, must only contain

1548: variables. Considering again Def.~\ref{alpha-def}, intuitively the

1549: abstractions of the recursive subterms of $t$ are stored in those

1550: positions only temporarily. The ultimate goal is to remove any

1551: non-variables there using the axioms, in particular the extraction

1552: axiom. 

1553: 

1554: Based on the propositions above, one can show:

1555: 

1556: \begin{rmtheorem}\label{normal-form-exists-thm}

1557: For any $t$ with $\_\vdash t:\phi$, $\alpha(t)$ has a representative 

1558: which is a normal abstract term for $\phi$.

1559: \end{rmtheorem}

1560: 

1561: \begin{pf}

1562: By Prop.~\ref{abstract-term-is-typed-prop}

1563: and Lemma~\ref{axioms-preserve-well-typing-lem} we have

1564: $\_\vdash a:\phi$ if $a=_\mathrm{\theory} \alpha(t)$.

1565: 

1566: Assume the notations of Def.~\ref{axioms-def}.

1567: The fact that an abstract term is typed according to the rules of

1568: Table~\ref{rules-tab} means in particular that if it

1569: has the form

1570: $d^\mathcal{A}(b_1,\dots,b_{j-1},

1571:               \dots\oplus {c'}^\mathcal{A}(\dots)\oplus\dots,

1572:               b_{j+1},\dots,b_l)$ where $j\in\set{l'+1,\dots,l}$,

1573: i.e., it is not in normal form, then $c' = c$ and an extraction 

1574: axiom is applicable, possibly after several applications of

1575: associativity and commutativity.

1576: 

1577: Likewise, if an abstract term has the form

1578: $\dots d^\mathcal{A}(\dots) \oplus\dots\oplus 

1579: {d'}^\mathcal{A}(\dots) \dots$, then $d = d'$ and the distributivity

1580: axiom is applicable.

1581: 

1582: Since the distributivity and extraction axioms can only be applied a

1583: finite number of times, it follows that successive application of them 

1584: yields an abstract term in normal form.

1585: \end{pf}

1586: 

1587: Example~\ref{extractor-ex} shows the conversion of two 

1588: abstract terms to their normal forms.

1589: 

1590: We can make some further observations. The first follows

1591: from the definition of $\alpha$.

1592: 

1593: \begin{propo}\label{alpha-variables-prop}

1594: For a term $t$, $\alpha(t)$ contains variables if and only if $t$

1595: contains variables.

1596: \end{propo}

1597: 

1598: The next proposition follows from the fact that by the transparency

1599: condition, no subterm type of a ground type $\phi$ can contain a

1600: parameter.

1601: 

1602: \begin{propo}\label{exactly-one-normal-prop}

1603: If $\phi$ is a ground type, then there is exactly one normal abstract

1604: term for $\phi$ not containing variables and not containing

1605: $\emptyset$.

1606: 

1607: Let $a$ be this abstract term. Then any other normal abstract term for $\phi$

1608: not containing variables is obtained by replacing some subterms in $a$

1609: with $\emptyset$.

1610: \end{propo}

1611: 

1612: The previous three statements tell us that the size of the abstraction

1613: of a ground term depends only on its type and not on the size of the

1614: term itself. However, it would be wrong to conclude that all ground

1615: terms of the same type have the same abstraction. The problem is due

1616: to polymorphism: one term can have several types. For example, it is

1617: correct to say that both $\mathtt{[]}$ and $\mathtt{[7]}$ are of 

1618: type $\mathtt{list(int)}$, but 

1619: $\alpha([]) = \mathtt{list^\mathcal{A}(\emptyset)}$ and 

1620: $\alpha(\mathtt{[7]}) = \mathtt{list^\mathcal{A}(int^\mathcal{A})}$.

1621: However, we can state:

1622: 

1623: \begin{rmlemma}\label{same-type-same-alpha-lem}

1624: If $\vdash s:\phi$ and $\vdash t:\phi$ and $s,t$ are ground, then

1625: both $\alpha(s)$ and $\alpha(t)$ are obtained from the unique normal

1626: abstract term as mentioned in Prop.~\ref{exactly-one-normal-prop} by

1627: replacing zero or more subterms with $\emptyset$.

1628: \end{rmlemma}

1629: 

1630: \section{Relating the Abstraction and the Labels}

1631: \label{alpha-label-relation-sec}

1632: Now that we know that each abstract term has a representative in a

1633: compact normal form, we state a theorem which relates the abstraction

1634: of a term to the labels as defined in Sec.~\ref{structure-sec}. 

1635: Actually, it would have been possible to have the following theorem as 

1636: {\em definition} of $\alpha$, and have our present definition as a

1637: lemma. This is effectively what we did in~\cite{SHK00}. 

1638: The theorem also links~\cite{CL00} with~\cite{LS01}.

1639: Note that $\alpha$ is lifted to sets as follows:

1640: $\alpha(S) := \bigoplus_{t\in S} \alpha(t)$. 

1641: 

1642: Before we can show the theorem, we extend the definition of

1643: $\mathcal{Z}$ to abstract terms, typed as shown in the previous

1644: section. We state the following lemma.

1645: 

1646: \begin{rmlemma}\label{abst-conc-labelling-lem}

1647: Let $\phi$ and $\tau$ be flat types such that 

1648: $\appl{\Theta}{\tau} \rec \phi$ for some  $\Theta$. Let $t$ be a term

1649: such that

1650: $\_\vdash t:\tau\Theta\Theta'$ for some $\Theta'$.

1651: Then for any $\sigma\nrs\phi$, or $\sigma\rec\phi$, we have

1652: $\alpha(\mathcal{Z}(\phi,\tau\Theta,\sigma,t)) =

1653: \mathcal{Z}(\phi,\tau\Theta,\sigma,\alpha(t))$.

1654: \end{rmlemma} 

1655: 

1656: \begin{pf}

1657: The proof is by induction on the depth of $t$. 

1658: First suppose that $t\in\mathcal{V}$. Then we have to distinguish

1659: whether $\sigma = \tau\Theta$ or $\sigma\neq\tau\Theta$. In the first case,

1660: $\alpha(\mathcal{Z}(\phi,\tau\Theta,\sigma,t)) = t =

1661: \mathcal{Z}(\phi,\tau\Theta,\sigma,\alpha(t))$. In the second case,

1662: $\alpha(\mathcal{Z}(\phi,\tau\Theta,\sigma,t)) = \emptyset =

1663: \mathcal{Z}(\phi,\tau\Theta,\sigma,\alpha(t))$.

1664: 

1665: Now suppose that $t$ is a constant. Again, we have to distinguish

1666: whether $\sigma = \tau\Theta$ or $\sigma\neq\tau\Theta$. In the first case,

1667: $\alpha(\mathcal{Z}(\phi,\tau\Theta,\sigma,t)) = 

1668: c^\mathcal{A}(\emptyset,\dots,\emptyset) =

1669: \mathcal{Z}(\phi,\tau\Theta,\sigma,\alpha(t))$. In the second case,

1670: $\alpha(\mathcal{Z}(\phi,\tau\Theta,\sigma,t)) = \emptyset =

1671: \mathcal{Z}(\phi,\tau\Theta,\sigma,\alpha(t))$.

1672: 

1673: Now consider a term $t = \ftau(t_1,\dots,t_n)$ and suppose the result

1674: has been proven for $t_1,\dots,t_n$. Suppose 

1675: $\Nrs(\tau) = \langle\rho_{1},\dots,\rho_{m'}\rangle$ and

1676: $\Rec(\tau) = \langle \rho_{m'+1},\dots,\rho_m \rangle$.

1677: Consider first $\sigma\nrs\phi$. In the following equation sequence,

1678: (*) marks steps that use simple rearrangements such as lifting a

1679: function to sets.

1680: \[

1681: \begin{array}{lr}

1682: \alpha(\mathcal{Z}(\phi,\tau\Theta,\sigma,t)) = & 

1683: \mbox{(Lem.~\ref{subterm-label-lem})}\\

1684: \displaystyle

1685: \alpha\left(

1686: \set{t_i \mid \tau_i\Theta = \sigma} \cup 

1687: \bigcup_{\tau_i\Theta\rec\phi}

1688: \mathcal{Z}(\phi,\tau_i\Theta,\sigma,t_i)\right) = &

1689: \mbox{(*)}\\

1690: \displaystyle

1691: \bigoplus_{\tau_i\Theta = \sigma} \alpha(t_i) \oplus

1692: \bigoplus_{\tau_i\Theta\rec\phi}

1693: \alpha(\mathcal{Z}(\phi,\tau_i\Theta,\sigma,t_i)) = &

1694: \mbox{(ind. hyp.)}\\ 

1695: \displaystyle

1696: \bigoplus_{\tau_i\Theta = \sigma} \alpha(t_i) \oplus

1697: \bigoplus_{\tau_i\Theta\rec\phi}

1698: \mathcal{Z}(\phi,\tau_i\Theta,\sigma,\alpha(t_i)) = &

1699: \mbox{(*)}\\ 

1700: \displaystyle

1701: \bigoplus_{\twocond{\rho_j\Theta = \sigma}{\tau_i = \rho_j}} \alpha(t_i) 

1702: \oplus

1703: \bigoplus_{\twocond{\rho_j\Theta\rec\phi}{\tau_i = \rho_j}}

1704: \mathcal{Z}(\phi,\rho_j\Theta,\sigma,\alpha(t_i)) 

1705: \oplus \\

1706: \multicolumn{1}{r}{\displaystyle

1707: \bigoplus_{\tau_i = \tau} 

1708: \mathcal{Z}(\phi,\tau_i\Theta,\sigma,\alpha(t_i)) =} &

1709: \mbox{(*)}\\

1710: \displaystyle

1711: \bigset{

1712: \bigoplus_{\tau_i = \rho_j} \alpha(t_i) \mid \rho_j\Theta = \sigma}

1713: \cup

1714: \bigcup_{\rho_j\Theta\rec\phi}

1715: \mathcal{Z}\left(\phi,\rho_j\Theta,\sigma,

1716: \bigoplus_{\tau_i = \rho_j} \alpha(t_i)\right)

1717: \oplus\\

1718: \multicolumn{1}{r}{\displaystyle

1719: \mathcal{Z}\left(

1720: \phi,\tau\Theta,\sigma,

1721: \bigoplus_{\tau_i=\tau} \alpha(t_i)\right)

1722: =} &

1723: \mbox{(Lem.~\ref{subterm-label-lem})}

1724: \end{array}

1725: \]

1726: 

1727: \[

1728: \begin{array}{lr}

1729: \displaystyle

1730: \mathcal{Z}\left(

1731: \phi,\tau\Theta,\sigma,

1732: c^\mathcal{A}

1733: \left(

1734: \bigoplus_{\tau_i=\rho_1} \alpha(t_i),

1735: \dots,

1736: \bigoplus_{\tau_i=\rho_m} \alpha(t_i)

1737: \right)\right)

1738: \oplus\\

1739: \multicolumn{1}{r}{\displaystyle

1740: \mathcal{Z}\left(

1741: \phi,\tau\Theta,\sigma,

1742: \bigoplus_{\tau_i=\tau} \alpha(t_i)

1743: \right)  =} & 

1744: \mbox{(*)}\\

1745: \displaystyle

1746: \mathcal{Z}\left(

1747: \phi,\tau\Theta,\sigma,

1748: c^\mathcal{A}

1749: \left(

1750: \bigoplus_{\tau_i=\rho_1} \alpha(t_i),

1751: \dots,

1752: \bigoplus_{\tau_i=\rho_m} \alpha(t_i)

1753: \right)

1754: \oplus

1755: \bigoplus_{\tau_i=\tau} \alpha(t_i)

1756: \right)  = & 

1757: \mbox{(Def.~\ref{alpha-def})}\\

1758: \mathcal{Z}(\phi,\tau\Theta,\sigma,\alpha(t)).

1759: \end{array}

1760: \]

1761: %PATCH 2

1762: The remaining cases, that either $\sigma\rec\phi$ and

1763: $\sigma\neq\phi$, or $\sigma = \phi$, are very similar and hence omitted.

1764: \end{pf}

1765: 

1766: We can now state the theorem.

1767: 

1768: \begin{rmtheorem}\label{alpha-thm}

1769: Let $\tau=c(\vect{u})$ be a flat type such that 

1770: $\Nrs(\tau) = \langle\rho_{1},\dots,\rho_{m'}\rangle$ and

1771: $\Rec(\tau) = \langle \rho_{m'+1},\dots,\rho_m \rangle$.

1772: For any term $t = \ftau(\dots)$, we have

1773: \begin{align*}

1774: \alpha(t)  =_\mathrm{\theory} 

1775:  c^\mathcal{A}\bigg(\! & 

1776: \alpha(\mathcal{Z}(\tau,\tau,\rho_1,t)),

1777: \dots,

1778: \alpha(\mathcal{Z}(\tau,\tau,\rho_{m'},t)),\\[-1ex]

1779: &

1780: \alpha(\mathcal{Z}(\tau,\tau,\rho_{m'+1},t))\cap\mathcal{V},

1781: \dots,

1782: \alpha(\mathcal{Z}(\tau,\tau,\rho_m,t))\cap\mathcal{V}

1783: \bigg)

1784: \oplus 

1785: (\mathcal{Z}(\tau,\tau,\tau,t)\cap\mathcal{V}).

1786: \end{align*}

1787: \end{rmtheorem}

1788: 

1789: \begin{pf}

1790: Suppose the normal form of $\alpha(t)$ is

1791: $c^\mathcal{A}(a_1,\dots,a_m)\oplus a$.

1792: 

1793: Consider some $j\in\set{1,\dots,m'}$. Since

1794:  $a$ as well as  $a_k$ for all $m' < k \leq m$, only consist of variables, it

1795: follows by Prop.~\ref{abstract-nrs-rec-prop} and Lemma~\ref{subterm-label-lem} that 

1796: \[

1797: \mathcal{Z}\left(\tau,\tau,\rho_j,c^\mathcal{A}(a_1,\dots,a_m)\oplus a\right)

1798: = a_j.

1799: \]

1800: At the same time, by Lemma~\ref{abst-conc-labelling-lem},

1801: \[

1802: \mathcal{Z}\left(\tau,\tau,\rho_j,\alpha(t)\right) = 

1803: \alpha(\mathcal{Z}\left(\tau,\tau,\rho_j,t)\right).

1804: \]

1805: 

1806: Now consider some $j\in\set{m'+1,\dots,m}$. Since

1807:  $a$ as well as  $a_k$ for all $m' < k \leq m$, only consist of variables, it

1808: follows by Prop.~\ref{abstract-nrs-rec-prop} and Lemma~\ref{subterm-label-lem} that 

1809: \[

1810: \mathcal{Z}\left(\tau,\tau,\rho_j,c^\mathcal{A}(a_1,\dots,a_m)\oplus a\right)

1811: \cap \mathcal{V}

1812: = a_j.

1813: \]

1814: At the same time, by Lemma~\ref{abst-conc-labelling-lem},

1815: \[

1816: \mathcal{Z}\left(\tau,\tau,\rho_j,\alpha(t)\right) = 

1817: \alpha(\mathcal{Z}\left(\tau,\tau,\rho_j,t)\right).

1818: \]

1819: 

1820: Finally consider $\tau$. Since

1821:  $a$ as well as  $a_k$ for all $m' < k \leq m$, only consist of variables, it

1822: follows by Prop.~\ref{abstract-nrs-rec-prop} and Lemma~\ref{subterm-label-lem} that 

1823: \[

1824: \mathcal{Z}\left(\tau,\tau,\tau,c^\mathcal{A}(a_1,\dots,a_m)\oplus a\right)

1825: \cap \mathcal{V}

1826: = a.

1827: \]

1828: At the same time, by Lemma~\ref{abst-conc-labelling-lem},

1829: \[

1830: \mathcal{Z}\left(\tau,\tau,\tau,\alpha(t)\right) = 

1831: \alpha(\mathcal{Z}\left(\tau,\tau,\tau,t)\right).

1832: \]

1833: Thus we have shown that the normal form of $\alpha(t)$ is as stated.

1834: \end{pf}

1835: 

1836: \begin{ex}\label{alpha-Z-ex}

1837: Consider \texttt{LISTS}. We have 

1838: \[

1839: \begin{array}{rlll}

1840: \alpha(\mathtt{[[X],[7]]}) & = &

1841: \mathtt{list^\mathcal{A}

1842: (\alpha(\mathcal{Z}(list(U),list(U),U,[[X],[7]])))}\\

1843: & & \oplus 

1844: \mathtt{\mathcal{Z}(list(U),list(U),list(U),[[X],[7]])\cap\mathcal{V})}\\

1845: & = &

1846: \mathtt{list^\mathcal{A}

1847: (\alpha(\set{[X],[7]}))

1848: \oplus

1849: (\set{[[X],[7]], [[7]], []}\cap\mathcal{V})}\\

1850: & = & 

1851: \mathtt{list^\mathcal{A}

1852: (list^\mathcal{A}(X\oplus int^\mathcal{A}))}

1853: \oplus\emptyset\\

1854: & =_\mathrm{\theory} & 

1855: \mathtt{list^\mathcal{A}

1856: (list^\mathcal{A}(X\oplus int^\mathcal{A}))}.

1857: \end{array}

1858: \]

1859: The theorem tells us how to read the abstract term. First, the absence

1860: of variable on the highest level (i.e.~$\alpha(\mathtt{[[X],[7]]})$ is

1861: not of the form $x\oplus\dots$) means that 

1862: $\mathtt{\mathcal{Z}(list(U),list(U),list(U),[[X],[7]])}$ contains no

1863: variables, or, to use the notation of~\cite{LS01} applied to the

1864: grammar in Ex.~\ref{labelling-ex}, $\zeta(LL,LL,\mathtt{[[X],[7]]})$

1865: is empty. Likewise, the theorem tells us that the argument of the

1866: outermost $\mathtt{list}^\mathcal{A}$ contains the abstraction of all

1867: subterms of $\mathtt{[[X],[7]]}$ returned by 

1868: $\mathtt{\mathcal{Z}(list(U),list(U),U,[[X],[7]])}$, and again in

1869: terms of~\cite{LS01}, the absence of variables at this level tells us

1870: that $\zeta(LL,L,\mathtt{[[X],[7]]})$ is empty.

1871: \end{ex}

1872: 

1873: \section{The Analysis}\label{analysis-sec}

1874: In this section, we show how an entire program is abstracted based on

1875: an abstraction of the fundamental operation, namely unification. The

1876: abstract program is then given a semantics. This semantics 

1877: {\em describes}, in a well-defined sense, the semantics of the

1878: concrete program. Moreover, under reasonable assumptions, it is

1879: finitely computable. 

1880: 

1881: \subsection{Abstract Interpretation}

1882: \label{abstract-interpretation-subsec}

1883: In this subsection, we link our formalism to the standard

1884: definitions of abstract interpretation.

1885: 

1886: Our abstract terms may contain variables, and hence it is only natural

1887: to define substitutions as for concrete terms, only that the range of

1888: those substitutions will contain abstract terms. The instantiation

1889: order $\absleq$ is defined as follows:

1890: $a\absleq b$ if $b\theta^\mathcal{A} =_\mathrm{\theory} a$ for some 

1891: $\theta^\mathcal{A}$. 

1892: It is lifted to substitutions:

1893: $\theta_1^\mathcal{A}\absleq\theta_2^\mathcal{A}$ if 

1894: $a\theta_1^\mathcal{A}\absleq a \theta_2^\mathcal{A}$ for all $a$.

1895: We write $a\approx b$ for $a\absleq b \; \wedge\; b\absleq a$. One should

1896: not confuse $\approx$ with $=_\mathrm{\theory}$! Our notation follows~\cite{CL00},

1897: not~\cite{LS01}. 

1898: An {\bf abstract atom} is an atom using 

1899: abstract terms. We denote the set of abstract atoms

1900: by $\mathcal{B}^\mathcal{A}$.

1901: 

1902: 

1903: 

1904: In order to define and relate semantics for concrete and abstract

1905: programs in the framework of abstract interpretation, we consider sets

1906: of (abstract) atoms with a suitable notion of ordering and

1907: equivalence. We consider the {\em lower power domain} or 

1908: {\em Hoare domain}~\cite{GS90}.

1909: For sets of abstract atoms $I^\mathcal{A}_1$ and

1910: $I^\mathcal{A}_2$, we define 

1911: \[

1912: I^\mathcal{A}_1 \absleq I^\mathcal{A}_2

1913: \; \Leftrightarrow \;

1914: \forall A_1^\mathcal{A} \in I^\mathcal{A}_1 \quad 

1915: \exists A_2^\mathcal{A} \in I^\mathcal{A}_2 \; . \;

1916: A_1^\mathcal{A} \absleq A_2^\mathcal{A}, 

1917: \]

1918: and 

1919: $I^\mathcal{A}_1 \approx I^\mathcal{A}_2$ if 

1920: $I^\mathcal{A}_1 \absleq I^\mathcal{A}_2$ and

1921: $I^\mathcal{A}_2 \absleq I^\mathcal{A}_1$. 

1922: The elements of 

1923: $[2^\mathcal{B^A}]_\approx$ are called {\bf abstract

1924: interpretations}. Abusing notation, we denote 

1925: $[2^\mathcal{B^A}]_\approx$ by $2^\mathcal{B^A}$.

1926: 

1927: We call a set of abstract atoms $I^\mathcal{A}$ {\bf downwards-closed} 

1928: if $A^\mathcal{A}\in I^\mathcal{A}$ implies 

1929: $\tilde{A}^\mathcal{A}\in I^\mathcal{A}$ for all 

1930: $\tilde{A}^\mathcal{A}\absleq A^\mathcal{A}$. The order relation $\approx$ is 

1931: defined in such a way that each 

1932: $I^\mathcal{A}\in 2^\mathcal{B^A}$ is equivalent to a downwards-closed set. This

1933: observation implies the following lemma.

1934: 

1935: 

1936: \begin{rmlemma}\cite[Lemma 3.1]{CL00}

1937: \label{is-lattice-lem}

1938: $(2^\mathcal{B^A},\absleq)$ is a complete lattice.

1939: \end{rmlemma}

1940: 

1941: \begin{defi}\label{galois-def}

1942: A {\bf Galois insertion} is a quadruple

1943: $\langle (A,\sqsubseteq_A),\alpha,(B,\sqsubseteq_B),\gamma\rangle$

1944: where

1945: \begin{enumerate}

1946: \item

1947: $(A,\sqsubseteq_A)$ and $(B,\sqsubseteq_B)$ are complete lattices of

1948: {\em concrete} and {\em abstract} domains, respectively;

1949: \item

1950: $\alpha: A \rar B$ and $\gamma: B \rar A$ are monotonic functions

1951: called {\em abstraction} and {\em concretisation}, respectively; and

1952: \item

1953: $a \sqsubseteq \gamma(\alpha(a))$ and $\alpha(\gamma(b)) = b$ for

1954: every

1955: $a\in A$ and $b\in B$.

1956: \end{enumerate}

1957: \end{defi}

1958: 

1959: In the above definition, the $\alpha$ is a priori not the $\alpha$ of

1960: Def.~\ref{alpha-def}, but of course, we have used the same letter

1961: because we link the two in the natural way.

1962: 

1963: \begin{rmtheorem}\cite[Theorem 3.3]{CL00}

1964: Define $\alpha$ and $\gamma$ as follows:

1965: \[

1966: \begin{array}{ll}

1967: \alpha: 2^\mathcal{B} \rar 2^\mathcal{B^A}, \quad &

1968: \alpha(I) = \set{\alpha(A) \mid A\in I},\\

1969: \gamma: 2^\mathcal{B^A} \rar 2^\mathcal{B}, &

1970: \gamma(I^\mathcal{A}) = \cup \set{I \mid \alpha(I) \absleq

1971: I^\mathcal{A}}.

1972: \end{array}

1973: \]

1974: Then

1975: $\langle 2^\mathcal{B}, \alpha, 2^\mathcal{B^A}, \gamma \rangle$

1976: is a Galois insertion.

1977: \end{rmtheorem}

1978: 

1979: 

1980: \begin{defi}\label{describes-def}

1981: An abstract term $a$ {\bf describes} a concrete term $t$, denoted 

1982: $a \describes t$, if $\alpha(t)\absleq a$ (and likewise for atoms).

1983: \end{defi}

1984: 

1985: 

1986: Note that for an atom $A$ and an abstract atom $A^\mathcal{A}$, we have

1987: $A^\mathcal{A} \describes A$ if and only if 

1988: $A\in\gamma(\set{A^\mathcal{A}})$. 

1989: For an interpretation $I$ and an abstract interpretation

1990: $I^\mathcal{A}$, we define 

1991: $I^\mathcal{A} \describes I$ if $I\subseteq\gamma(I^\mathcal{A})$, or

1992: equivalently, $\alpha(I) \absleq I^\mathcal{A}$. 

1993: 

1994: 

1995: 

1996: \subsection{Abstract Unification}

1997: \label{abstract-unification-subsec}

1998: In this subsection, we show how abstract unification describes

1999: concrete unification. First, we can relate abstraction and application

2000: of a substitution as follows.

2001: 

2002: \begin{rmlemma}\cite[Lemma 4.1]{CL00}\label{alpha-subst-lem}

2003: Let $t$ be a term an $\theta$ a substitution. Then

2004: $\alpha(t\theta) =_\mathrm{\theory} 

2005: \alpha(t) \set{x/\alpha(x\theta) \mid x\in\dom(\theta)}$.

2006: \end{rmlemma}

2007: 

2008: \begin{pf}

2009: By structural induction on the term. Let 

2010: $\theta^\mathcal{A} = \set{x/\alpha(x\theta) \mid

2011: x\in\dom(\theta)}$. 

2012: 

2013: If $t\in\mathcal{V}$ and $t\notin\dom(\theta)$, the result trivially

2014: holds. If $t\in\mathcal{V}$ and $t\in\dom(\theta)$, then

2015: $\alpha(t\theta) = t \set{t/\alpha(t\theta)} = \alpha(t) \theta^\mathcal{A}$.

2016: 

2017: Now consider $t = \ftau(t_1,\dots,t_n)$, where

2018: $\tau = c(\bar{u})$, 

2019: $\Nrs(\tau) = \langle \rho_1,\dots,\rho_{m'} \rangle$, and

2020: $\Rec(\tau) = \langle \rho_{m'+1},\dots,\rho_m \rangle$, 

2021:  and assume

2022: that the result holds for $t_1,\dots,t_n$. We have

2023: \[

2024: \begin{array}{rcl}

2025: \alpha(t\theta) & = & 

2026: \displaystyle

2027: c^\mathcal{A}

2028: \left(

2029: \bigoplus_{\tau_i=\rho_1} \alpha(t_i\theta),

2030: \dots,

2031: \bigoplus_{\tau_i=\rho_m} \alpha(t_i\theta)

2032: \right)

2033: \oplus

2034: \bigoplus_{\tau_i=\tau} \alpha(t_i\theta) \\

2035: & =  &

2036: \displaystyle

2037: c^\mathcal{A}

2038: \left(

2039: \bigoplus_{\tau_i=\rho_1} \alpha(t_i)\theta^\mathcal{A},

2040: \dots,

2041: \bigoplus_{\tau_i=\rho_m} \alpha(t_i)\theta^\mathcal{A}

2042: \right)

2043: \oplus

2044: \bigoplus_{\tau_i=\tau} \alpha(t_i)\theta^\mathcal{A} = 

2045: \alpha(t)\theta^\mathcal{A}.

2046: \end{array}

2047: \]

2048: \end{pf}

2049: 

2050: \begin{ex}\label{alpha-subst-ex}

2051: By Lemma~\ref{alpha-subst-lem}, 

2052: \[

2053: \begin{array}{l}

2054: \alpha(\mathtt{[X|Y]}\, \set{\mathtt{X/7, Y/nil}}) =\\ 

2055: \qquad

2056: \alpha(\mathtt{[7]})=\\ 

2057: \qquad

2058: \mathtt{list^\mathcal{A}(int^\mathcal{A})

2059: =_\mathrm{\theory}}\\

2060: \qquad 

2061: \mathtt{list^\mathcal{A}(int^\mathcal{A}) \oplus

2062: list^\mathcal{A}(\emptyset)} =\\

2063: \qquad 

2064: (\mathtt{list^\mathcal{A}(X) \oplus Y})\,

2065: \set{\mathtt{X/int^\mathcal{A}, Y/list^\mathcal{A}(\emptyset)}} =

2066: \qquad \\ 

2067: \multicolumn{1}{r}{

2068: \alpha(\mathtt{[X|Y]})\,

2069: \set{\mathtt{X/\alpha(7), Y/\alpha(nil)}}}.

2070: \end{array} 

2071: \]

2072: \end{ex}

2073: 

2074: The following theorem is a straightforward consequence.

2075: 

2076: \begin{rmtheorem}\cite[Thm.~4.2]{CL00}\label{alpha-order-thm}

2077: Let $t_1, t_2$ be terms. If $t_1\leq t_2$ then 

2078: $\alpha(t_1) \absleq \alpha(t_2)$ (and likewise for atoms).

2079: \end{rmtheorem}

2080: 

2081: 

2082: 

2083: \begin{defi}\label{unifier-def}

2084: We denote by 

2085: $cU_\mathrm{\theory}(o_1,o_2)$ a complete set of 

2086: \theory-unifiers of syntactic objects $o_1, o_2$, i.e., a set of

2087: abstract substitutions such that for each 

2088: $\theta^\mathcal{A}\in cU_\mathrm{\theory}(o_1,o_2)$, we have

2089: $o_1\theta^\mathcal{A} =_\mathrm{\theory} o_2\theta^\mathcal{A}$, and for 

2090: any $\tilde{\theta}^\mathcal{A}$ such that 

2091: $o_1\tilde{\theta}^\mathcal{A}=_\mathrm{\theory} o_2\tilde{\theta}^\mathcal{A}$, 

2092: we have $\tilde{\theta}^\mathcal{A}\absleq \theta^\mathcal{A}$ for some 

2093: $\theta^\mathcal{A}\in cU_\mathrm{\theory}(o_1,o_2)$.

2094: \end{defi}

2095: 

2096: The next theorem says that unification of abstract terms is a correct

2097: abstract unification. The second part of the statement says that an abstract

2098: substitution corresponding to a concrete substitution as stated

2099: correctly mimics that concrete substitution, for any atom.

2100: 

2101: \begin{rmtheorem}\cite[Thm.~4.4]{CL00}\label{abstract-unification-correct-thm}

2102: Let $A_1, A_2$ be atoms that are unifiable with MGU $\theta$,

2103: and $A_1^\mathcal{A},A_2^\mathcal{A}$ be abstract atoms such that   

2104: $A_1^\mathcal{A}\describes A_1$ and $A_2^\mathcal{A}\describes A_2$.

2105: Then there exists a unifier 

2106: $\theta^\mathcal{A}\in

2107: cU_\mathrm{\theory}(A_1^\mathcal{A},A_2^\mathcal{A})$ such that 

2108: $A_1^\mathcal{A}\theta^\mathcal{A} \describes A_1\theta$, and moreover

2109: for any atom $B$, we have 

2110: $\alpha(B)\theta^\mathcal{A} \describes B\theta$.

2111: \end{rmtheorem}

2112: 

2113: \begin{pf}

2114: Consider the pairs $\langle B,A_1\rangle$, $\langle B,A_2\rangle$

2115: where $B$ is an arbitrary atom. Since 

2116: $\langle B,A_i\rangle\theta\leq\langle B,A_i\rangle$, we have by

2117: Thm.~\ref{alpha-order-thm} and the definition of $\describes$

2118: \[

2119: \alpha(\langle B, A_i \rangle\theta)\absleq

2120: \alpha(\langle B, A_i \rangle)\absleq

2121: \langle \alpha(B),A_i^\mathcal{A}\rangle

2122: \quad (i = 1,2).

2123: \]

2124: Since $A_1\theta=A_2\theta$, it follows that

2125: $\alpha(\langle B, A_1 \rangle\theta) = 

2126:  \alpha(\langle B, A_2 \rangle\theta)$ and so 

2127: $\alpha(\langle B, A_1 \rangle\theta)$ is a common

2128: \theory-instance of   

2129: $\langle \alpha(B),A_1^\mathcal{A}\rangle$ and

2130: $\langle \alpha(B),A_2^\mathcal{A}\rangle$. Hence

2131: \[

2132: cU_\mathrm{\theory}(\langle \alpha(B), A_1^\mathcal{A}\rangle,

2133:                     \langle \alpha(B), A_2^\mathcal{A}\rangle)

2134: \]

2135: contains a $\theta^\mathcal{A}$ such that 

2136: $\alpha(\langle B, A_1 \rangle\theta) \absleq

2137: \langle \alpha(B), A_1^\mathcal{A}\rangle\theta^\mathcal{A}$ and so

2138: $\alpha(B\theta) \absleq \alpha(B)\theta^\mathcal{A}$ and

2139: $\alpha(A_1 \theta) \absleq A_1^\mathcal{A}\theta^\mathcal{A}$. 

2140: Now

2141: $cU_\mathrm{\theory}(\langle \alpha(B), A_1^\mathcal{A}\rangle,

2142:                     \langle \alpha(B), A_2^\mathcal{A}\rangle)$

2143: is also a complete set of unifiers of $A_1^\mathcal{A}$ and

2144: $A_2^\mathcal{A}$, and so the claim follows.

2145: \end{pf}

2146: 

2147: In addition, we also have that \theory-unification is optimal. To make

2148: this notion precise, consider two abstract atoms $A_1^\mathcal{A}$,

2149: $A_2^\mathcal{A}$, and let 

2150: $I_i = \gamma(\set{A_i^\mathcal{A}})$ ($i = 1,2$). For 

2151: two atoms $A_1\in I_1$, $A_2\in I_2$, any common instance is in

2152: $I_1\cap I_2$, since $I_1$, $I_2$ are downwards-closed. 

2153: Now let 

2154: $cI_\mathrm{\theory}(A_1^\mathcal{A},A_2^\mathcal{A}) = 

2155: \set{A_1^\mathcal{A} \theta^\mathcal{A} \mid 

2156: \theta^\mathcal{A} \in cU_\mathrm{\theory}(A_1^\mathcal{A},A_2^\mathcal{A})}$. 

2157: We might call $cI_\mathrm{\theory}(A_1^\mathcal{A},A_2^\mathcal{A})$ a

2158: {\em complete} set of common \theory-instances of 

2159: $A_1^\mathcal{A}$, $A_2^\mathcal{A}$. Optimality of abstract

2160: unification means that  

2161: $cI_\mathrm{\theory}(A_1^\mathcal{A},A_2^\mathcal{A})$ describes only

2162: the atoms in $I_1\cap I_2$.

2163: 

2164: \begin{rmtheorem}\cite[Thm.~4.6]{CL00}

2165: \label{abstract-unification-optimal-thm}

2166: For $i = 1,2$, let $A_i^\mathcal{A}$, be abstract atoms and 

2167: $I_i = \gamma(\set{A_i^\mathcal{A}})$.

2168: Then $cI_\mathrm{\theory}(A_1^\mathcal{A},A_2^\mathcal{A})$ describes only

2169: the atoms in $I_1\cap I_2$.

2170: \end{rmtheorem}

2171: 

2172: \begin{pf}

2173: To derive a contradiction, assume that $B$ is an atom such that for

2174: some

2175: $B^\mathcal{A}\in

2176: cI_\mathrm{\theory}(A_1^\mathcal{A},A_2^\mathcal{A})$, 

2177: we have $B^\mathcal{A}\describes B$ but $B\not\in I_1 \cap I_2$. This

2178: implies that $A_1^\mathcal{A}\not\describes B$ or

2179: $A_2^\mathcal{A}\not\describes B$. On the other hand, $B^\mathcal{A}$

2180: is a common instance of $A_1^\mathcal{A}$, $A_2^\mathcal{A}$, which

2181: implies $A_1^\mathcal{A}\describes B$ and

2182: $A_2^\mathcal{A}\describes B$. Contradiction.

2183: \end{pf}

2184: 

2185: \subsection{Abstraction of Programs}\label{program-abstraction-subsec}

2186: In~\cite{LS01,SHK00}, programs were assumed to be in normal, also

2187: called canonical, form. In~\cite{LS01}, the abstraction of a

2188: unification constraint $x = y$ involves computing the intersection of

2189: the two grammars corresponding to $x$ and $y$. In addition, the

2190: abstraction of a unification constraint $y = f(x_1,\dots,x_n)$ involves

2191: computing a grammar for $f(x_1,\dots,x_n)$ from the $n$ grammars for

2192: $x_1,\dots,x_n$. In~\cite{SHK00}, no such operations are performed,

2193: but still the abstraction of unification constraints is not obvious. 

2194: Each unification constraint $y = f(x_1,\dots,x_n)$ is abstracted

2195: as a call $\fdep(y,x_1,\dots,x_n)$, where $\fdep$ is a predicate that

2196: expresses the relationship between the abstraction of a term and its

2197: subterms. 

2198: 

2199: In the framework we have set up here following~\cite{CL00},

2200: abstracting a program is much simpler. We have designed the domains

2201: so that Thm.~\ref{abstract-unification-correct-thm} holds, and so we can

2202: abstract a program simply by replacing each term with its abstraction.

2203: Thus $\alpha$ is lifted in the obvious way to atoms, clauses, programs

2204: and queries. 

2205: 

2206: 

2207: The semantics of the abstract program will be defined using an 

2208: \theory-enhanced version of the $T_P$-operator. Formally

2209: \begin{align*}

2210: T^\mathcal{A}_P(I^\mathcal{A}) = 

2211: \set{\alpha(H)\theta^\mathcal{A} \mid & 

2212: C = H \lar B_1,\dots,B_n \in P,

2213: \langle A^\mathcal{A}_1,\dots,A^\mathcal{A}_n \rangle \renamed{C} I^\mathcal{A},\\

2214: &

2215: \theta^\mathcal{A}\in 

2216: cU_\mathrm{\theory} 

2217: (\langle \alpha(B_1),\dots,\alpha(B_n)\rangle,\langle A^\mathcal{A}_1,\dots,A^\mathcal{A}_n\rangle)}.

2218: \end{align*}

2219: 

2220: We denote by $\sem{P^\mathcal{A}}_\mathrm{\theory}$ the 

2221: least fixpoint of $T^\mathcal{A}_P$, which exists

2222: by~\cite[Cor.~5.2]{CL00}.  

2223: The following theorem says that this abstract semantics correctly

2224: describes the concrete semantics. 

2225: 

2226: \begin{rmtheorem}\cite[Thm.~5.4]{CL00}\label{correct-semantics-thm}

2227: Let $P$ be a program. Then 

2228: $\sem{\alpha(P)}_\mathrm{\theory}

2229: \describes

2230: \sem{P}_s

2231: $.

2232: \end{rmtheorem}

2233: 

2234: % PATCH 3

2235: 

2236: 

2237: 

2238: We could make further statements about the semantics, e.g.~call and

2239: answer patterns; for that purpose, we would use the magic set

2240: transformation. However, those results would be completely along the

2241: lines of~\cite{CL96,CL00}, as are the proofs of the results we gave in

2242: this subsection.

2243: 

2244: \subsection{Finiteness}\label{finiteness-subsec}

2245: In~\cite{CL00} we find a result that the abstract semantics of a

2246: program is finite provided that the type abstraction is

2247: monomorphic. 

2248: The result does not hold anymore for polymorphic type

2249: abstractions, and the authors give the program 

2250: \[

2251: P_1 :=

2252: \set{

2253: \mathtt{p([X]) \lar p(X).},\ 

2254: \mathtt{p(1).}}

2255: \] 

2256: as an example. As a solution, the authors propose a 

2257: {\em depth-$k$ abstraction}, i.e., some ad-hoc bound on the depth of

2258: types. 

2259: 

2260: It is understandable that a descriptive view of types leads to the

2261: conviction that infinity of the abstract semantics is inherent in a

2262: polymorphic type abstraction and cannot reasonably be

2263: avoided. 

2264: 

2265: Instead of $P_1$, consider the program

2266: \[

2267: P_2 := \set{

2268: \mathtt{p([X]) \lar p(X).},\ 

2269: \mathtt{p([]).}}

2270: \] 

2271: For the argument in~\cite{CL00}, $P_2$ is completely equivalent

2272: to $P_1$, i.e., the authors could just as well have chosen

2273: $P_2$. However, using $P_2$ allows us to make a stronger point than using

2274: $P_1$. The reason is that both programs are not typable

2275: by the rules of Table~\ref{rules-tab} (that is to say, in a

2276: prescriptive approach to typing), but for $P_2$, this is much less

2277: obvious.

2278: The program $P_2$ is forbidden due to the {\em head

2279: condition}~\cite{HT92}, i.e., the special typing rule $\mathit{Head}$

2280: which is different from rule $\mathit{Atom}$ (see

2281: Table~\ref{rules-tab}). 

2282: 

2283: \begin{propo}\label{head-propo}

2284: Assuming $\mathcal{F}_\mathtt{LISTS}$ (see

2285: Ex.~\ref{typerelations-ex}), there exists no variable typing

2286: $\Gamma$ such that 

2287: $\Gamma \vdash \mathtt{p([X]) \lar p(X)}\ \mathit{Clause}$,

2288: regardless of what the declared type of $\mathtt{p}$ is.

2289: \end{propo}

2290: 

2291: \begin{pf}

2292: To derive

2293: $\Gamma \vdash \mathtt{p([X]) \lar p(X)}\ \mathit{Clause}$, we need to 

2294: derive

2295: $\Gamma \vdash \mathtt{p([X])}\ \mathit{Head}$, and in turn,

2296: \begin{equation}

2297: \label{list-x-has-type-eq}

2298: \Gamma \vdash \mathtt{[X]}:\sigma

2299: \end {equation}

2300: for some type $\sigma$. 

2301: By rule $\mathit{Func}$ and the fact that the declared range type of

2302: $\mathtt{Cons}$ is $\mathtt{List(U)}$, it follows that 

2303: $\sigma = \mathtt{List(\tau)}$ for some $\tau$, and so for 

2304: $\Gamma \vdash \mathtt{p([X])}\ \mathit{Head}$ to be a valid type

2305: judgement, the declared type of $\mathtt{p}$ must be 

2306: $\mathtt{List(\tau)}$, so we write $\mathtt{p}_\mathtt{List(\tau)}$. 

2307: 

2308: To derive

2309: $\Gamma \vdash \mathtt{p([X]) \lar p(X)}\ \mathit{Clause}$, we 

2310: {\em also} need to derive

2311: $\Gamma\vdash \mathtt{p_{list(\tau)}(X)}: \mathit{Atom}$, and in turn,

2312: $\Gamma\vdash \mathtt{X}:\mathtt{list}(\tau)\Theta$ for some type

2313: substitution $\Theta$. This implies that 

2314: $\mathtt{X}:\mathtt{list}(\tau)\Theta \in \Gamma$ and hence

2315: $\Gamma\vdash \mathtt{[X]}:\mathtt{list(list(\tau))}\Theta$, and in

2316: particular,

2317: $\Gamma\not\vdash \mathtt{[X]}:\mathtt{list(\tau)}$. This is a

2318: contradiction to (\ref{list-x-has-type-eq}), showing that there exists 

2319: no $\Gamma$ such that 

2320: $\Gamma \vdash \mathtt{p([X]) \lar p(X)}\ \mathit{Clause}$.

2321: \end{pf}

2322: 

2323: We want to show that disregarding such programs, the abstract

2324: semantics is always finite. We first need the following lemma about

2325: concrete programs, stating that the arguments of any

2326: atom in $\sem{P}_s$ are of the declared type.

2327: 

2328: 

2329: \begin{rmlemma}\label{finitely-many-types-lem}

2330: Let $P$ be a typed program. For any atom

2331: $\ptau(t_1,\dots,t_n)\in\sem{P}_s$, we have

2332: $\_\vdash (t_1,\dots,t_n):(\tau_1,\dots,\tau_n)$.

2333: \end{rmlemma}

2334: 

2335: \begin{pf}

2336: Suppose $I$ is a set if atoms having the property stated for

2337: $\sem{P}_s$. We show that an application of the $T_P$-operator to 

2338: $I$ preserves the property. This immediately implies the result.

2339: 

2340: Consider some clause

2341: $C = \ptau(t_1,\dots,t_n) \lar B_1,\dots,B_m$ in $P$, and suppose that

2342: $\langle A_1,\dots,A_m \rangle \renamed{C} I$, such that 

2343: $\theta = 

2344: MGU(\langle B_1,\dots,B_m\rangle,\langle A_1,\dots,A_m\rangle)$.

2345:  By the rules in

2346: Table~\ref{rules-tab}, in particular $\mathit{Head}$, we have

2347: $\_\vdash (t_1,\dots,t_n):(\tau_1,\dots,\tau_n)$. 

2348: For each $B_l = q_{\sigma_1,\dots,\sigma_{n'}}(s_1,\dots,s_{n'})$, 

2349: by the rules in Table~\ref{rules-tab}, we have

2350: $\_\vdash (s_1,\dots,s_{n'}): (\sigma_1,\dots,\sigma_{n'})\Theta$ for

2351: some $\Theta$. Let $A_l = q(r_1,\dots,r_{n'})$. 

2352: By assumption about $I$, 

2353: we have 

2354: $\_\vdash (r_1,\dots,r_{n'}): (\sigma_1,\dots,\sigma_{n'})$ and hence, 

2355: by the typing rules, also 

2356: $\_\vdash (r_1,\dots,r_{n'}): (\sigma_1,\dots,\sigma_{n'})\Theta$.

2357: By standard results~\cite[Thm.~1.4.1, Lemma 1.4.2]{HT92}, it follows that  

2358: $\_\vdash (s_1,\dots,s_{n'})\theta:

2359: (\sigma_1,\dots,\sigma_{n'})\Theta$.

2360: Since the choice of $A_l$ was arbitrary, it follows that each atom in

2361: $C\theta$ can be typed using the same types as for the corresponding

2362: atom in $C$. This applies in particular for the clause head, and so

2363: $\_\vdash (t_1,\dots,t_n)\theta:(\tau_1,\dots,\tau_n)$.

2364: \end{pf}

2365: 

2366: 

2367: By Prop.~\ref{abstract-term-is-typed-prop}, the above lemma

2368: applies also to the abstraction of a program.

2369: 

2370: \begin{coro}\label{finitely-many-types-cor}

2371: Let $P$ be a typed program. For any atom

2372: $\ptau(a_1,\dots,a_n)\in\sem{\alpha(P)}_\mathrm{\theory}$, we have

2373: $\_\vdash^\mathcal{A} (a_1,\dots,a_n):(\tau_1,\dots,\tau_n)$.

2374: \end{coro}

2375: 

2376: 

2377: The following lemma states that for a given type $\phi$, 

2378: there are only finitely many different abstract terms for $\phi$.

2379: 

2380: \begin{rmlemma}\label{finitely-many-terms-lem}

2381: For any type $\phi$, the set of abstract terms

2382: $\set{ a \mid \_\vdash^\mathcal{A} a:\phi}$ is finite modulo $\approx$.

2383: \end{rmlemma}

2384: 

2385: \begin{pf}

2386: Since the claim is that the set is finite modulo $\approx$, it is

2387: clearly sufficient to restrict our attention to {\em normal} abstract

2388: terms. It is useful to recall the notations and definitions of

2389: Subsec.~\ref{normal-abstract-terms-subsec}. 

2390: 

2391: The proof is along the lines of the proof of~\cite[Thm.~3.2]{CL00},

2392: but matters are slightly more complicated since our abstract terms are 

2393: nested. 

2394: 

2395: We define by structural induction:

2396: \begin{itemize}

2397: \item

2398: for each abstract term $a\oplus x^\oplus$, $\epsilon$ is a {\em path},

2399: and any variable in $x^\oplus$ is a variable 

2400: {\em occurring in $a\oplus x^\oplus$ at $\epsilon$}; 

2401: \item

2402: for an abstract term $c^\mathcal{A}(a_1,\dots,a_m)\oplus\dots$, if 

2403: $\zeta$ is a path for $a_j$ and $x$ is a variable occurring in $a_j$

2404: at $\zeta$, then $j.\zeta$ is a 

2405: {\em path for $c^\mathcal{A}(a_1,\dots,a_m)\oplus\dots$}, 

2406: and $x$ is a variable

2407: {\em occurring in $c^\mathcal{A}(a_1,\dots,a_m)\oplus\dots$ at $j.\zeta$}.

2408: \end{itemize}

2409: By the well-definedness of normal abstract terms, it follows that that 

2410: there is a maximum number of paths that a normal abstract term for

2411: $\phi$ can have. Let $n$ be this number for our given $\phi$.

2412: 

2413: Suppose that a normal abstract term $a$ for $\phi$ 

2414: contains more that $2^n-1$ distinct variables. By a simple

2415: combinatorial argument, one sees that there must be at least two

2416: variables, say $x$ and $y$, occurring at exactly the same paths in

2417: $a$. Consider $a' = a \set{x/z, y/z}$. Trivially

2418: $a' \absleq a$. On the other hand, we have

2419: $a' \set{z/x\oplus y} =_\mathrm{\theory} a$, and thus

2420: $a \absleq a'$. So we have $a \approx a'$, and 

2421: $\#(\vars(a')) = \#(\vars(a)) - 1$. 

2422: 

2423: By iterating this argument, it follows that any normal abstract term

2424: for $\phi$ is $\approx$-equivalent to a term containing no more that

2425: $2^n-1$ variables, and thus the claim follows.

2426:  \end{pf}

2427: 

2428: 

2429: The following is a simple corollary.

2430: 

2431: \begin{coro}\label{finitely-many-atoms-cor}

2432: Let $\ptau$ be a predicate and $\Theta$ a type substitution.

2433: Modulo $\approx$, there are only finitely many abstract atoms

2434: $p(a_1,\dots,a_n)$ such that $(a_1,\dots,a_n)$ is a vector of 

2435: normal abstract terms for the type vector 

2436: $(\tau_1,\dots,\tau_n)\Theta$.

2437: \end{coro}

2438: 

2439: 

2440: \begin{rmtheorem}\label{finite-semantics-thm}

2441: Let $P$ be a typed program. Then 

2442: $\sem{\alpha(P)}_\mathrm{\theory}$ is finite.

2443: \end{rmtheorem}

2444: 

2445: \begin{pf}

2446: By Corollaries~\ref{finitely-many-types-cor}

2447: and~\ref{finitely-many-atoms-cor}. 

2448: \end{pf}

2449: 

2450: As it stands, the theorem depends critically on the fact that we

2451: assume a {\em bottom-up} semantics. To explain this, consider the

2452: program 

2453: \[

2454: P_3 = 

2455: \set{

2456: \mathtt{p(X) \lar p([X]).},\ 

2457: \mathtt{p([]).}},

2458: \] 

2459: which at first look is very similar to the program 

2460: $P_2$

2461: given at the beginning of this subsection. However, assuming that

2462: $\mathtt{p}$ has declared type $\mathtt{list(U)}$, the program $P_3$ is 

2463: typed according to the rules of Table~\ref{rules-tab}. Therefore, of

2464: course, Thm.~\ref{finite-semantics-thm} applies to this program. 

2465: 

2466: Note that $P_3$, when called with the query $\mathtt{p(Y)}$, gives rise 

2467: to infinitely many calls 

2468: $\mathtt{p(Y)}, 

2469: \mathtt{p([Y])}, 

2470: \mathtt{p([[Y]])},\dots$, with abstractions

2471: $\mathtt{p(Y)}, 

2472: \mathtt{p(list^\mathcal{A}(Y))},\allowbreak 

2473: \mathtt{p(list^\mathcal{A}(list^\mathcal{A}(Y)))},\allowbreak

2474: \dots$.

2475: So the set of calls cannot be described (in the technical sense,

2476: using $\describes$) finitely.  

2477: 

2478: We make two observations about $P_3$:

2479: \begin{itemize}

2480: \item

2481: The {\em magic set} version~\cite{CD95} of the program contains the

2482: clause 

2483: \[

2484: \mathtt{p^c([X]) \lar p^c(X).},

2485: \] which is to be read as ``in

2486: order for $\mathtt{p([X])}$ to be called, $\mathtt{p(X)}$ must be

2487: called. This clause is not typable according to the rules of

2488: Table~\ref{rules-tab} as the head condition is violated. Thus

2489: Thm.~\ref{finite-semantics-thm} is not applicable. This is not

2490: surprising given the fact that the very purpose of the magic set

2491: transformation is to characterise {\em calls}.

2492: \item

2493: In the literature on prescriptive typing, the

2494: behaviour exhibited by $P_3$ has been called 

2495: {\em polymorphic recursion}~\cite{H93}.

2496: It is by no means common. In fact, it 

2497: is very much on the borderline of what is allowed in prescriptively

2498: typed programming languages. In ML for example, it is forbidden, as it 

2499: breaks the capabilities of the type inference procedure.

2500: \end{itemize}

2501: It has previously been suspected that there is an interesting

2502: relationship between the head condition and polymorphic recursion, which 

2503: deserves some profound investigation~\cite{DS01}. The two observations 

2504: above add weight to this.

2505: 

2506: In this paper, we do not want to study the difference between top-down

2507: and bottom-up semantics in detail. Nevertheless, we now formulate what

2508: it means for a program not to use polymorphic recursion, in which case

2509: we say that it only uses monomorphic recursion. 

2510: 

2511: For simplicity, we assume that a program 

2512: only contains direct recursion, i.e., no recursion of the form

2513: $p \lar \dots q$,  $q \lar \dots p$. It is straightforward to

2514: generalise our considerations otherwise. In the following, we use

2515: $\vect{t}$ ($\vect{\tau}$) to denote vectors of terms (types).

2516: 

2517: \begin{defi}\label{monomorphic-recursion-def}

2518: A typed program {\bf uses only monomorphic recursion} if for any clause

2519: $p(\vect{t}) \lar \dots p(\vect{s}) \dots$, we have

2520: $\_\vdash \vect{t}:\vect{\tau},\ \vect{s}:\vect{\tau}$

2521: for some vector of types $\vect{\tau}$.

2522: \end{defi}

2523: 

2524: Thus monomorphic recursion means that in each clause, the type of any

2525: recursive call must be identical to the type of the head.

2526: Since the head condition is still in force, this implies that any

2527: recursive call must have a type which is identical to the declared

2528: type of its predicate.

2529: 

2530: For programs using only monomorphic recursion, it should be possible

2531: to devise a variant of the magic set transformation such that the

2532: transformed program is typed according to the rules in

2533: Table~\ref{rules-tab}, and therefore has a finite abstract semantics.

2534: 

2535: \section{Towards an Implementation}

2536: \label{implementation-sec}

2537: So far, we have not implemented the analysis proposed in this

2538: paper. As far as computing the semantics of the abstract program is

2539: concerned, the only difference with the implementations mentioned

2540: in~\cite{CL96,CL00} is that instead of ACI or ACI1 we have the

2541: equality theory \theory. The former theories are finitary~\cite{BS98},

2542: and the corresponding unification 

2543: problems are NP-complete. Obviously, \theory\ cannot behave any

2544: better. Studying \theory\ is a topic for future work, but we would

2545: certainly expect it to be finitary as well. 

2546: 

2547: There is an implementation of the analysis we proposed

2548: in~\cite{SHK00}, which essentially aims at the same degree of

2549: precision we have here, but the framework is different. In fact, this

2550: paper relates to~\cite{SHK00} in the same way as~\cite{CL96,CL00} relates

2551: to~\cite{CD94}. This is interesting because the authors mention that

2552: an implementation using ACI-unification turned out to be much 

2553: faster than the implementation in~\cite{CD94}.

2554: 

2555: Note that to compute the abstraction of a program,

2556: in~\cite{CD94,CL00}, it is the user who has to provide information

2557: about the particular type language used in a program (see paragraph

2558: after Def.~\ref{alpha-def}), whereas in our analysis, this information

2559: is extracted from the declared types. We had previously shown~\cite{SHK00} that

2560: analysing the type declarations (computing the NRSs and recursive

2561: types) is viable even for some contrived, complex type declarations,

2562: which one would never expect in practice, since {\em good programs

2563: have small types}~\cite{H93}\footnote{However, this should not be

2564: understood as a contradiction to our \texttt{NESTS} or \texttt{TABLES}

2565: examples. Henglein comes from a functional programming background, 

2566: and in that community, those type declarations would by all means

2567: still qualify as ``small''.}.

2568:  

2569: In~\cite{CL96}, there is some speculation as to why abstract

2570: unification is not as bad as it seems by the theoretical result that

2571: it is NP-complete. It is said that usually unifications involve

2572: ``few'' variables. Here we want to substantiate that claim somewhat,

2573: but it remains speculation all the same. 

2574: \begin{itemize}

2575: \item

2576: The first argument is that abstract terms (in normal form) are likely

2577: to be linear. Recall that the abstract terms are designed in such a

2578: way that different positions correspond to different subterm

2579: types. Since we use prescriptive types, one is tempted to conclude

2580: that abstract terms {\em must} be linear, since the same variable

2581: cannot have different types. That however would be a fallacy, since

2582: via instantiation of types, different subterm types can become

2583: equal. For example, the term

2584: $\mathtt{node(null,X,X,eq,null)}$ of type 

2585: $\mathtt{table(string)}$ has the abstraction

2586: $\mathtt{table^\mathcal{A}(X,bal^\mathcal{A},X)}$ which is not linear.

2587: Nevertheless, this should be an exception.

2588: \item

2589: On the whole, logic programs are based on a very simple notion of

2590: modes. Of course, it is the very exceptions to this rule that justify

2591: developing a complex instantiation analysis like the one of this paper

2592: or~\cite{CL00,LS01}, but still, often one deals with simple

2593: assignments rather than full unification in concrete programs, and

2594: this carries through to abstract programs. 

2595: \end{itemize}

2596: 

2597: To give at least one example of the advance of our analysis

2598: over~\cite{CL00}, we use $\mathtt{table(int)}$. Suppose there is a

2599: predicate $\mathtt{insert}/4$ whose arguments represent:  a table $t$, 

2600: a key $k$, a value $v$, and a table

2601: obtained from $t$ by inserting the node whose key is $k$ 

2602: and whose value is $v$.

2603: From the abstract semantics of the program, it is possible 

2604: to read that a query whose abstraction is 

2605: \[

2606: \mathtt{insert(

2607: table^\mathcal{A}(int^\mathcal{A},bal^\mathcal{A},str^\mathcal{A}),

2608: str^\mathcal{A},V2,T)},

2609: \] 

2610: i.e., a query to insert 

2611: an {\em uninstantiated} value into a ground table, yields an answer

2612: whose abstraction is 

2613: \[

2614: \mathtt{insert(

2615: table^\mathcal{A}(int^\mathcal{A},bal^\mathcal{A},str^\mathcal{A}),

2616: str^\mathcal{A},V2,

2617: table^\mathcal{A}(int^\mathcal{A}\oplus V2,bal^\mathcal{A},str^\mathcal{A}))},

2618: \] 

2619: i.e., the result is a table whose values may be uninstantiated. 

2620: 

2621: %\section{Groundness Analysis}\label{groundness-sec}

2622: 

2623: %\section{Sharing Analysis}\label{sharing-sec}

2624: 

2625: \section{Discussion}\label{discussion-sec}

2626: In this paper, we have proposed a formalism for deriving abstract

2627: domains from the type declarations of a typed program. Effectively, we

2628: have recast our previous work~\cite{SHK00} using

2629: important parts of the formalisms of~\cite{CL00,LS01}.

2630: We now compare this paper with those two works under several aspects.

2631: 

2632: 

2633: 

2634: \paragraph{The type system.}

2635: Using the terminology introduced in this paper, one can say

2636: that~\cite{CL00} uses a polymorphic type system with the following

2637: assumptions: types are either monomorphic or unary, and

2638: the only subterm types of a unary type $c(u)$ are $c(u)$ itself 

2639: (and $c(u) \rec c(u)$) and $u$ (and $u \nrs c(u)$). This is the 

2640: simplest thinkable scenario of proper polymorphism; in fact, 

2641: only lists and trees are covered. Our \texttt{TABLES} or let alone the 

2642: \texttt{NESTS} example are not covered. In contrast,~\cite{LS01}

2643: assumes regular types without polymorphism. Thus there are only

2644: finitely many types the analysis has to deal with. However, those may

2645: be very complex; e.g., one can easily construct a grammar that

2646: corresponds to the type $\mathtt{table(int)}$. So the type systems

2647: of~\cite{CL00,LS01} are not formally comparable, but the type system

2648: we assume in this paper is a strict generalisation of both.

2649: 

2650: \paragraph{Descriptive vs.~prescriptive types.}

2651: According to the authors' claims,~\cite{CL00} takes a

2652: descriptive view of typing, whereas~\cite{LS01} takes a prescriptive

2653: view. However, we find that the formalism of~\cite{CL00} can very well

2654: be adapted to prescriptive typing. On the other hand, we find that

2655: some aspects of~\cite{LS01} belong rather to a descriptive view of

2656: typing. 

2657: 

2658: First, the fact that the typing approach of~\cite{CL00} is descriptive

2659: rightly accounts for the fact that they must consider ``ill-typed''

2660: terms such as $\mathtt[1|2]$. In this paper, all terms are

2661: ``well-typed'', and so are the abstract terms. 

2662: 

2663: In~\cite{LS01} it is assumed that a unique type (or equivalently, grammar) is associated

2664: with each program variable. A unification constraint in a program

2665: gives rise to operations such as computing the intersection of two

2666: types and computing the type of a term from the types of its

2667: subterms. Such operations can improve the precision of an analysis,

2668: e.g.~if $\mathtt{X}$ has the declared type 

2669: ``list with an even number of elements'' and 

2670: $\mathtt{Y}$ has the declared type 

2671: ``list with a number of elements divisible by $3$'', then a unification 

2672: $\mathtt{X} = \mathtt{Y}$ implies that both variables have the type 

2673: ``list with a number of elements divisible by $6$''. 

2674: In our opinion, the presence of such operations introduces an aspect

2675: of type {\em inference} into their formalism which is somewhat in

2676: contradiction  to a {\em prescriptive} 

2677: approach to typing. While such type inference may be useful, the

2678: authors do not give a convincing example for it being so.

2679: 

2680: 

2681: \paragraph{Labellings.}

2682: Labellings are useful to formalise which aspects of the structure of a

2683: concrete term we want to capture by our analysis, and so it is natural

2684: that we used them mainly in Sec.~\ref{structure-sec}. In~\cite{CL00},

2685: they are absent, although they may have been useful (see

2686: Sec.~\ref{alpha-label-relation-sec}). In~\cite{SHK00}, there

2687: were similar functions called {\em extractors} and {\em termination functions}.

2688: 

2689: First note that $\zeta$ only collects variables, whereas $\mathcal{Z}$ 

2690: also collects non-variable terms. This generalisation allows us to

2691: describe the relation between a term and its abstraction as we did in

2692: Sec.~\ref{alpha-label-relation-sec}. 

2693: 

2694: The labelling function $\zeta$ in~\cite{LS01} has three arguments: a

2695: grammar (which however can be identified with its starting

2696: non-terminal), a non-terminal to be labelled, and a labelling

2697: term. Our labelling function $\mathcal{Z}$ has {\em four} arguments. 

2698: We found it useful to have as first argument a {\em flat} type

2699: (e.g.~$\mathtt{nest(V)}$) which

2700: gives us a certain grammar, but also allow for productions of that

2701: grammar starting from some other non-terminal 

2702: (e.g.~$\mathtt{list(nest(V))}$). Actually, it may well be the 

2703: case that the first argument is redundant, i.e.~that the grammar can 

2704: be derived from the starting non-terminal (e.g.~$\mathtt{nest(V)}$

2705: from $\mathtt{list(nest(V))}$). We prefer however to keep this useful

2706: intuitive explanation: one argument to indicate the grammar, one to 

2707: indicate the starting non-terminal.

2708: The difference between our labelling function and that of~\cite{LS01}

2709: is due to polymorphism.

2710: 

2711: \paragraph{Abstract terms.}

2712:  In~\cite{LS01}, the abstraction of terms

2713: is not actually made explicit, but effectively, given a program

2714: variable $x$, its abstraction is the (somehow ordered) tuple of 

2715: non-terminals of the grammar of $x$. Non-terminals are thought of as

2716: {\em abstract variables} (see the paragraph after Equation

2717: (\ref{aci1-eq})). 

2718: Our abstraction of terms, denoted $\alpha$, is designed in such a way

2719: that the abstraction $\mathit{type}$ in~\cite{CL00} is essentially a

2720: special case of it. We do not introduce abstract variables but rather 

2721: collect the labellings for a term in a structure called 

2722: {\em abstract term}. The reason for this decision is that it

2723: allows us to deal with arbitrarily large grammars/type graphs.

2724: 

2725: \paragraph{Type hierarchies.}

2726: Given a function $f_{\dots\rar c(u)}$, 

2727: the abstraction $\mathit{type}$ in~\cite{CL00} distinguishes between 

2728: the argument positions of declared type $u$ and the ``recursive''

2729: argument positions. Via type instantiation, this already gives rise to

2730: a certain hierarchy of arbitrary depth, as reflected for example in 

2731: the abstract term 

2732: $\mathtt{list^\mathcal{A}(list^\mathcal{A}(int^\mathcal{A}))}$.

2733: Our concepts of {\em non-recursive subterm type} and 

2734: {\em recursive type} generalise this idea. An NRS of a flat type is

2735: not necessarily a parameter, and $\tau$ can have other recursive types

2736: than $\tau$ itself. This hierarchy allows us to deal with the fact 

2737: that through instantiation of types, a polymorphic language gives rise 

2738: to arbitrarily big type graphs (grammars).

2739: 

2740: In contrast, in~\cite{LS01}, all non-terminals (types) reachable from

2741: the starting node of a grammar are treated in the same way. This

2742: approach is viable since the size of the grammars is fixed beforehand.

2743: 

2744: \paragraph{Equality theory.}

2745: The equality theory for evaluating abstract terms in~\cite{LS01} is

2746: ACI1. Distributivity is not applicable.  In~\cite{CL00}, the equality

2747: theory is ACI, so there is no neutral element. The authors mention

2748: distributivity but decide against it. This is in contrast

2749: to~\cite{CL96} where the equality theory is ACI1 plus distributivity.

2750: Our extraction axioms are only

2751: relevant for a language where some type has a recursive type other

2752: than itself, and so it is not applicable to~\cite{CL96,CL00}.

2753: We believe that at least conceptually, both a neutral element and the

2754: distributivity axioms are very natural, even if at the level of an

2755: implementation, it might be preferable not to have them.

2756: 

2757: \paragraph{Types = abstract terms?}

2758: In~\cite{CL00}, there is no distinction between a type constructor $c$

2759: and the function $c^\mathcal{A}$ to build abstract terms. Also, the

2760: equivalent of our function $\alpha$ is

2761: called {\em type abstraction} and denoted by $\mathit{type}$, which

2762: highlights the fact that in descriptive approaches to typing, 

2763: {\em type} analysis and {\em mode} analysis are blurred almost to the

2764: extent of being considered to be the same thing. However, such an

2765: identification only works because the assumptions about the type

2766: system are so restrictive. \\

2767: 

2768: \noindent

2769: Thus we have generalised~\cite{CL00,LS01} by considering a type system

2770: which almost (see below) corresponds to the type system of existing typed

2771: programming languages.  We have given several examples in

2772: Sec.~\ref{structure-sec} hoping to convince the reader that such a

2773: generalisation is non-trivial. In particular, there are two natural

2774: requirements: the construction of an abstract domain for a polymorphic

2775: type should be truly parametric, and the abstract domains should be

2776: finite for a given program and query. We had to impose two conditions

2777: on the type declarations to ensure these requirements.

2778: On a technical level, the fact that the SCCs of a type graph are not

2779: stable under instantiation makes it difficult to meet those

2780: requirements.

2781: 

2782: We now very briefly recall some other related work. We refer to the

2783: discussions in~\cite{CL00,LS01,SHK00} for more details.

2784: 

2785: Both this paper and~\cite{CL00,LS01} build on ideas presented

2786: originally in~\cite{CD94}. 

2787: 

2788: {\em Recursive modes}~\cite{TL97} characterise that

2789: the left spine, right spine, or both, of a term are instantiated.

2790: This seems ad-hoc but often coincides with characterising that

2791: all recursive subterms of a term are instantiated.

2792: 

2793: A system for type analysis of Prolog is presented in~\cite{HCC93}. It

2794: takes a descriptive approach to typing, and the abstract domains are,

2795: in general, infinite. Therefore, widenings must be used. 

2796: Similarly, in~\cite{JB92},  the finiteness of

2797: abstract domains and terms is ensured by imposing an ad-hoc

2798: bound on the number of symbols.

2799: 

2800: It would probably be possible to express the abstraction of terms

2801: proposed here as application of a particular 

2802: {\em pre-interpretation}~\cite{GBS95}. 

2803: 

2804: A classical instantiation analysis is not interesting for

2805: Mercury~\cite{mercury} as the language is strongly moded. However,

2806: our work might also have applications for Mercury.

2807: 

2808: \subsection*{Acknowledgements}

2809: The author was supported by the ERCIM fellowship programme.

2810: 

2811: \bibliography{modes_types,thesis}

2812: 

2813: \appendix

2814: %\section{Proofs}\label{proofs-sec}

2815: %We first show the following simple statement:

2816: %$\alpha(t) = \alpha(\mathcal{Z}(\tau,\tau,\tau,t))$. The proof is by

2817: %structural induction. The base case 

2818: %$\mathcal{Z}(\tau,\tau,\tau,t) = t$ is trivial. In the inductive case,

2819: %we have

2820: %\[

2821: %\begin{array}{rcl}

2822: %\alpha(t) & = &  

2823: % c^\mathcal{A}

2824: %\left(

2825: %\bigoplus_{\tau_i=\rho_1} \alpha(t_i),

2826: %\dots,

2827: %\bigoplus_{\tau_i=\rho_m} \alpha(t_i)

2828: %\right)

2829: %\oplus

2830: %\bigoplus_{\tau_i=\tau} \alpha(t_i) \\

2831: %& = &  

2832: % c^\mathcal{A}

2833: %\left(

2834: %\bigoplus_{\tau_i=\rho_1} \alpha(t_i),

2835: %\dots,

2836: %\bigoplus_{\tau_i=\rho_m} \alpha(t_i)

2837: %\right)

2838: %\oplus

2839: %\bigoplus_{\tau_i=\tau} \alpha(t_i)

2840: %\oplus

2841: %\bigoplus_{\tau_i=\tau} \alpha(t_i) \\

2842: %& = &  

2843: %\alpha(t)

2844: %\oplus

2845: %\bigoplus_{\tau_i=\tau} \alpha(\mathcal{Z}(\tau,\tau,\tau,t_i)) \\

2846: %& = &  

2847: %\alpha(\mathcal{Z}(\tau,\tau,\tau,t)).

2848: %\end{array}

2849: %\]

2850: 

2851: \end{document}

2852: 

2853: