1: %This file is the corr version of flops 2001 and RR 4082.
2: %RR 4082 contains a mistake corrected here.
3:
4: \documentclass{article}
5:
6: \usepackage[french,english]{babel}
7: \selectlanguage{english}
8: \def\english{\selectlanguage{english}}
9: \def\french{\selectlanguage{french}}
10: \usepackage{RR}
11: \usepackage{myNotation}
12: \usepackage{amssymb}
13: \usepackage{latexsym}
14:
15: \RRNo{4082}
16: \RRdate{December 2000} % date de publication du rapport
17: %%
18: \RRauthor{Pierre Deransart\thanks{\texttt{pierre.deransart@inria.fr}}
19: \and
20: Jan--Georg Smaus\thanks{ \texttt{jan.smaus@cwi.nl},
21: CWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands.}}
22:
23: %%
24: \authorhead{Deransart \& Smaus} % Ceci apparait sur chaque page paire.
25:
26: %%
27: \RRetitle{Well-Typed Logic Programs Are not Wrong}
28: %%
29: \RRtitle{Les programmes logiques bien typ\'es ont tout bon}
30:
31: %%
32: \titlehead{Well-Typed Logic Programs Are not Wrong} %titre court, sur toutes les pages.
33: %%
34: \RRnote{This report is the complete version of a paper presented at
35: FLOPS 2001~\cite{DS01}. It contains all proofs omitted there for space
36: reasons. Copies of this report obtained from INRIA contain a mistake
37: (the converse of Theorem~\ref{type-tree-theorem} is claimed to hold)
38: which is corrected in the present version.}
39:
40: \RRresume{On \'etudie ici les syt\`emes de typage prescriptif (\`a la G\"odel ou
41: Mercury) pour la programmation en logique. Dans de tels syst\`emes, le
42: typage est {\em statique}, mais il garantit une propri\'et\'e
43: op\'erationnelle: si un programme est ``bien typ\'e'', alors tous les
44: buts obtenus par d\'erivation d'un but ``bien typ\'e'' sont eux-m\^eme
45: ``bien typ\'es''. Le syst\`eme est alors dit {\em stable par
46: r\'eduction} (``subject reduction''). Nous montrons dans ce papier que
47: cette propri\'et\'e de stabilit\'e est en fait aussi {\em
48: d\'eclarative}. Cette vue d\'eclarative nous conduit \`a
49: reconsid\'erer une condition habituellement admise et n\'ec\'essaire
50: pour la stabilit\'e par r\'eduction, dite {\em condition de t\^ete}
51: (``head condition''). Cette condition stipule que le type des t\^etes
52: des clauses d'un programme ``bien typ\'e'' doit \^etre une variante
53: (et non une instance quelconque) du type d\'eclar\'e de son
54: pr\'edicat. Il est alors possible de formuler des conditions plus
55: g\'en\'erales qui r\'etablissent une certaine sym\'etrie entre les
56: t\^etes et les atomes du corps, et qui garantissent en fait que dans
57: toutes d\'erivations les types des termes unifiables sont eux aussi
58: unifiables. On discute enfin les implications possibles d'un tel
59: r\'esultat, en particulier la relation entre la condition de t\^ete et
60: la {\em recursion polymorphique}, un concept connu dans la
61: programmation fonctionnelle.
62: }
63:
64: \RRabstract{We consider prescriptive type systems for logic programs (as in
65: G\"odel or Mercury). In such systems, the typing is {\em static}, but
66: it guarantees an operational property: if a program is ``well-typed'',
67: then all derivations starting in a ``well-typed'' query are again
68: ``well-typed''. This property has been called {\em subject
69: reduction}. We show that this property can also be phrased as a
70: property of the {\em proof-theoretic} semantics of logic programs,
71: thus abstracting from the usual operational (top-down) semantics.
72: This proof-theoretic view leads us to questioning a condition
73: which is usually considered necessary for subject reduction, namely
74: the {\em head condition}. It states that the head of each clause must
75: have a type which is a variant (and not a proper instance) of the
76: declared type. We provide a more general condition, thus
77: reestablishing a certain symmetry between heads and body atoms. The
78: condition ensures that in a derivation, the types of two unified terms
79: are themselves unifiable. We discuss possible implications of this result.
80: We also discuss the relationship between the head condition and
81: {\em polymorphic recursion}, a concept known in functional programming.}
82: %%
83: \RRmotcle{programmation en logique, syst\`eme de type (prescriptif),
84: ``subject reduction'', polymorphisme, condition de t\^ete,
85: arbre de d\'erivation, recursion polymorphique}
86: \RRkeyword{Logic programming, (prescriptive) type system, subject
87: reduction, polymorphism, head condition, derivation tree,
88: polymorphic recursion}
89: \RRprojet{Contraintes}
90: %%
91: %\RRprojets{Contraintes} % cas de 2 projets.
92: %%
93: %% \RRtheme{4} % cas d'un seul theme
94: \RRtheme{2} % cas de 2 themes
95: %%
96: %% \URLorraine % pour ceux qui sont ^^e0 l'est
97: %% \URRennes % pour ceux qui sont ^^e0 l'ouest
98: %% \URRhoneAlpes % pour ceux qui sont dans les montagnes
99: \URRocq % pour ceux qui sont au centre de la France
100: %%\URSophia % pour ceux qui sont au Sud.
101: %%
102:
103: \newcommand{\hgen}{HG}
104: \newcommand{\bgen}{BG}
105: \newcommand{\gen}{Gen}
106: \newcommand{\nongen}{\overline{Gen}}
107:
108: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
109: % OUR ENVIRONMENTS
110: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
111:
112: \newtheorem{theorem}{Theorem}{\bfseries}{\rm}
113: \newtheorem{rmtheorem}[theorem]{Theorem}{\bfseries}{\rm}
114: \newtheorem{rmlemma}[theorem]{Lemma}{\bfseries}{\rm}
115: \newtheorem{coro}[theorem]{Corollary}{\bfseries}{\rm}
116: \newtheorem{propo}[theorem]{Proposition}{\bfseries}{\rm}
117: \newtheorem{definition}{Definition}{\bfseries}{\rm}
118: \newtheorem{defi}[definition]{Definition}{\bfseries}{\rm}
119: \newtheorem{example}{Example}{\bfseries}{\rm}
120: \newtheorem{ex}[example]{Example}{\bfseries}{\rm}
121:
122: \newenvironment{proof}{\bfseries Proof:\rm} {\hfill$\square$\vspace{4mm}}
123:
124: %original one uses index n. Here we want m
125: \renewcommand\ftau{f_{\tau_1 \dots \tau_m\rightarrow\tau}}
126: \renewcommand\ptau{p_{\tau_1 \dots \tau_m}}
127:
128:
129: %\setlength{\topmargin}{1cm}
130: %\setlength{\headheight}{0cm}
131: %\setlength{\headsep}{0cm}
132: %\setlength{\oddsidemargin}{0cm}
133: %\setlength{\textwidth}{16cm}
134: %\setlength{\textwidth}{14cm}
135: %\setlength{\textheight}{23.5cm}
136: %\setlength{\hoffset}{0cm}
137: %\setlength{\voffset}{0cm}
138: %\setlength{\footskip}{0.5cm}
139:
140: %\pagestyle{plain}
141:
142: \bibliographystyle{plain}
143:
144: \begin{document}
145:
146:
147:
148:
149: %%
150: \makeRR % cas d'un rapport de recherche
151: %% \makeRT % cas d'un rapport technique.
152: %% a partir d'ici, chacun fait comme il le souhaite
153:
154:
155: \author{Pierre Deransart\inst{1} \and Jan-Georg Smaus\inst{2}}
156:
157:
158: \section{Introduction}
159: Prescriptive types are used in logic programming
160: (and other paradigms)
161: to restrict the
162: underlying syntax so that only ``meaningful'' expressions are
163: allowed. This allows for many programming errors to be detected by the
164: compiler. Moreover, it ensures that once a program
165: has passed the compiler, the types of arguments of predicates can be
166: ignored at runtime, since it is guaranteed that they will be of
167: correct type. This has been turned into the famous slogan~\cite{M78,MO84}
168: %
169: \begin{quote}
170: Well-typed programs cannot go wrong.
171: \end{quote}
172: %
173: Adopting the terminology from the theory of the
174: $\lambda$-calculus~\cite{Tho91}, this property of a typed program is
175: called {\em subject reduction}. For the simply typed
176: $\lambda$-calculus, subject reduction states that the type of a
177: $\lambda$-term is invariant under reduction. Translated to logic
178: programming, this means that resolving a ``well-typed'' query with a
179: ``well-typed'' clause will always result in a ``well-typed'' query,
180: and so the successive queries obtained during a derivation are all
181: ``well-typed''.
182:
183: From this observation, it is clear that subject reduction is
184: a property of the {\em operational} semantics of a
185: logic program, i.e., SLD resolution~\cite{L87}.
186: In this paper, we show that it is also a property of
187: the proof-theoretic semantics based on {\em derivation
188: trees}. This is obtained by showing that using ``well-typed'' clauses,
189: only ``well-typed'' derivation trees can be constructed, giving rise
190: to the new slogan:
191: %
192: \begin{quote}
193: Well-typed programs {\em are} not wrong.
194: \end{quote}
195: The {\em head condition}, which is a condition on the program
196: (clauses)~\cite{HT92-new}, is usually considered to be crucial for
197: subject reduction. The second objective of this paper is to analyse
198: the head condition in this new light and open the field for
199: generalisations, of which we introduce one.
200:
201: The head condition, also called
202: {\em definitional genericity}~\cite{LR91}, states that the types of the arguments of a clause
203: head must be a variant\footnote{A variant is obtained by renaming the
204: type parameters in a type.} (and not a proper instance) of the
205: declared type of the head predicate. This
206: condition
207: %has an operational flavour as it
208: imposes a distinction between ``definitional'' occurrences (clause
209: heads) and ``applied'' occurrences (body atoms) of a predicate. In
210: contrast, the proof-theoretic view of subject reduction we propose
211: reestablishes a certain symmetry between the different occurrences. By
212: this generalisation, the class of programs for which subject reduction
213: is guaranteed is enlarged.
214:
215: This paper is organised as follows. Section \ref{prelim-sec} contains some
216: preliminaries. Section~\ref{trees-sec} introduces our proof-theoretic
217: notion of subject reduction.
218: Section~\ref{conditions-sec} gives conditions for subject reduction,
219: and in particular, a generalisation of the head condition.
220: In Section~\ref{is-restrictive-sec}, we discuss, in the light of these
221: results, the usefulness of the head condition and its generalisation.
222: We also exhibit an interesting relationship between
223: the head condition and {\em polymorphic recursion}~\cite{KFU93-short}.
224: Section~\ref{conclusion-sec} concludes by mentioning possible
225: applications of these results.
226:
227: \section{Preliminaries}\label{prelim-sec}
228:
229: We assume familiarity with the standard concepts of logic
230: programming~\cite{L87}.
231: To simplify the notation, a vector such as $o_1,\dots,o_m$
232: is often denoted by $\bar{o}$. The restriction of a
233: substitution $\theta$ to the variables in a syntactic object $o$ is
234: denoted as $\theta \restr{o}$, and analogously for type
235: substitutions (see Subsec.~\ref{typed-prog-subsec}).
236: The relation symbol of an atom $a$ is denoted by $Rel(a)$.
237:
238: When we refer to a {\em clause in a program}, we usually mean a copy
239: of this clause whose variables are renamed apart from variables
240: occurring in other objects in the context. A query is a sequence of
241: atoms. A
242: query $Q'$ is {\bf derived from} a query $Q$, denoted $Q \leadsto Q'$,
243: if
244: $Q= a_1,\dots,a_m$,
245: $Q'=(a_1,\dots,a_{k-1},B,a_{k+1},\dots,a_m)\theta$,
246: and $h\leftarrow B$ is a clause (in a program usually clear from
247: the context) such that $h$ and $a_k$ are unifiable with MGU $\theta$.
248: A {\bf derivation} $Q \leadsto^* Q'$ is defined in the usual way.
249: Given a program $P$, the {\bf immediate consequence operator}
250: $T_P$ is defined by
251: $
252: T_P(M) =
253: \{h\theta \mid
254: h\leftarrow a_1,\dots,a_m \in P,\;
255: a_1\theta,\dots,a_m\theta \in M\}$.
256:
257:
258:
259: \subsection{Derivation Trees}
260: A key element of this work is the proof-theoretic semantics of
261: logic programs based on derivation trees~\cite{DM93}.
262: We recall some important notions and basic
263: results.
264:
265: \begin{defi}
266: %defterm[instance name]
267: \label{instance-name-def}
268: An {\bf instance name} of a clause $C$ is a pair of the form
269: $\langle C, \theta \rangle$, where $\theta$ is a substitution.
270: \end{defi}
271:
272: \begin{defi}
273: %defterm[derivation tree]
274: \label{der-tree-def}
275: Let $P$ be a program. A {\bf derivation tree} for $P$ is a labelled
276: ordered tree~\cite{DM93} such that:
277: \begin{enumerate}
278: \item
279: Each leaf node is labelled by $\bot$ or an instance name
280: $\langle C,\theta \rangle$ of a clause\footnote{
281: Recall that $C$ is renamed apart from any other clause in the
282: same tree.} in $P$;
283: %\item
284: each non-leaf node is labelled by an instance name
285: $\langle C,\theta \rangle$ of a clause in $P$.
286: \item
287: If a node is labelled by
288: $\langle h\leftarrow a_1,\dots,a_m,\theta \rangle$, where $m \geq 0$,
289: then this node has $m$ children, and for $i \in \onetom$, the $i$th
290: child is labelled either $\bot$, or
291: $\langle h'\leftarrow B,\theta' \rangle$ where $h'\theta'=a_i\theta$.
292: \end{enumerate}
293: %
294: Nodes labelled $\bot$ are {\bf incomplete}, all other nodes are
295: {\bf complete}.
296: A derivation tree containing only complete nodes is a
297: {\bf proof tree}.
298: \end{defi}
299:
300:
301: To define the semantics of logic programs, it is useful to associate
302: an atom with each node in a derivation tree in the following way.
303:
304: \begin{defi}
305: %defterm[node atom]
306: \label{node-atom-def}
307: Let $T$ be a derivation tree. For each node $n$ in $T$, the
308: {\bf node atom} of $n$, denoted $atom(n)$, is defined as follows:
309: If $n$ is labelled
310: $\langle h\leftarrow B,\theta \rangle$, then
311: $h \theta$ is the node atom of $n$; if $n$ is labelled
312: $\bot$, and $n$ is the
313: $i$th child of its parent labelled
314: $\langle h\leftarrow a_1,\dots,a_m,\theta \rangle$, then
315: $a_i\theta$ is the node atom of $n$.
316: If $n$ is the root of $T$ then $atom(n)$ is the {\bf head of $T$},
317: denoted $head(T)$.
318: \end{defi}
319:
320:
321: Derivation trees are obtained by grafting instances of clauses of a
322: program. To describe this construction in a general way, we
323: define the following concept.
324:
325: \begin{defi}
326: %defterm[skeleton (tree)]
327: \label{skel-def}
328: Let $P$ be a program. A {\bf skeleton (tree)} for $P$ is a labelled
329: ordered tree such that:
330: \begin{enumerate}
331: \item
332: Each leaf node is labelled by $\bot$ or a clause
333: in $P$, and
334: %\item
335: each non-leaf node is labelled by a clause in $P$.
336: \item
337: If a node is labelled by
338: $h\leftarrow a_1,\dots,a_m$, where $m \geq 0$, then
339: this node has $m$ children, and for $i \in \onetom$, the $i$th child is
340: labelled either $\bot$, or
341: $h'\leftarrow B$ where $Rel(h') = Rel(a_i)$.
342: \end{enumerate}
343: \end{defi}
344:
345:
346: The {\bf skeleton of a tree} $T$, denoted $Sk(T)$, is the skeleton
347: obtained from $T$ by replacing each label
348: $\langle C, \theta \rangle$ with $C$. Conversely, we
349: say that $T$ is a {\bf derivation tree based on} $Sk(T)$.
350:
351: \begin{defi}
352: %defterm[$\mathit{Eq}(S)$]
353: \label{eqs-def}
354: Let $S$ be a skeleton. We define
355: \[
356: \begin{array}{ll}
357: \mathit{Eq}(S) =
358: \{
359: a_i=h'
360: \mid &
361: \mbox{there exist complete nodes $n$, $n'$ in $S$
362: such that}\\
363: &
364: \mbox{$\bullet$ $n'$ is the $i$th child of $n$,}\\
365: &
366: \mbox{$\bullet$ $n$ is labelled $h\leftarrow a_1,\dots,a_m$,}\\
367: &
368: \mbox{$\bullet$ $n'$ is labelled $h'\leftarrow B$}
369: \}
370: \end{array}
371: \]
372: Abusing notation, we frequently identify the set of equations with the
373: conjunction or sequence of all equations contained in it.
374: If $\mathit{Eq}(S)$ has a unifier then we call $S$ a {\bf proper} skeleton.
375: \end{defi}
376:
377: \begin{propo}\cite[Prop.~2.1]{DM93}\label{der-tree-exists-prop}
378: Let $S$ be a skeleton. A derivation tree based on $S$ exists if and
379: only if $S$ is proper.
380: \end{propo}
381:
382: \begin{rmtheorem}\cite[Thm.~2.1]{DM93}
383: Let $S$ be a skeleton and $\theta$ an MGU of $\mathit{Eq}(S)$. Let $D(S)$ be
384: the tree obtained from $S$ by replacing each node label $C$ with the
385: pair $\langle C, \theta\restr{C} \rangle$. Then $D(S)$ is a most
386: general derivation tree based on $S$ (i.e., any other derivation
387: tree based on $S$ is an instance of $D(S)$).
388: \end{rmtheorem}
389:
390: \begin{example}\label{proof-tree-ex}
391: Figure~\ref{no-pure-BC-fig} shows a program, one of
392: its derivation trees, and the skeleton of the derivation tree.
393: \end{example}
394:
395: \setlength{\unitlength}{0.46cm}
396: \begin{figure}[t]
397: \begin{picture}(6,5)
398: \put(0,3.3){
399: \begin{minipage}{6cm}
400: {%\small
401: $\tt h(X) \leftarrow q(X), p(X).$\\
402: $\tt q([]).$\\
403: $\tt p(X) \leftarrow r(X).$
404: }
405: \end{minipage}}
406: \end{picture}
407: \hfill
408: \begin{picture}(12,5)
409: \put(4,0){\makebox(8,1){$\bot$}}
410: \put(8,1){\line(0,1){1}}
411: \put(0,2){\makebox(4,1){
412: $\langle \tt q([]),\emptyset \rangle$}}
413: \put(4,2){\makebox(8,1){
414: $\langle \tt p(X') \leftarrow r(X'),\;
415: \{x'/[]\}\rangle$}}
416: \put(2,3){\line(1,1){1}}
417: \put(8,3){\line(-1,1){1}}
418: \put(1,4){\makebox(10,1){
419: $\langle \tt h(X) \leftarrow q(X) \und p(X),\;
420: \{x/[]\}\rangle$}}
421: \end{picture}
422: \hfill
423: \begin{picture}(8,5)
424: \put(2,0){\makebox(6,1){$\bot$}}
425: \put(5,1){\line(0,1){1}}
426: \put(0,2){\makebox(2,1){
427: $\tt q([])$}}
428: \put(2,2){\makebox(6,1){
429: $\tt p(X') \leftarrow r(X')$}}
430: \put(1,3){\line(1,1){1}}
431: \put(5,3){\line(-1,1){1}}
432: \put(0,4){\makebox(8,1){
433: $\tt h(X) \leftarrow q(X), p(X)$}}
434: \end{picture}
435: \caption{A program, a derivation tree and its skeleton
436: \label{no-pure-BC-fig}\label{trees-fig}}
437: \end{figure}
438:
439:
440: To model derivations for a program $P$ and a query
441: $Q$, we assume that $P$ contains an
442: additional clause ${\tt go} \leftarrow Q$,
443: where $\tt go$ is a new predicate symbol.
444:
445: We recall the following straightforward
446: correspondences between derivations, the $T_P$-semantics and
447: derivation trees.
448:
449: \begin{propo}\label{semant-equiv-propo}
450: Let $P$ be a program. Then
451: \begin{enumerate}
452: \item \label{tree=TP}
453: $a \in \mathit{lfp}(T_P)$ if and only if $a=head(T)$ for some proof tree
454: $T$ for $P$,
455: \item \label{tree=operational}
456: $Q \leadsto^* Q'$ if and only if $Q'$ is the
457: sequence of node atoms of incomplete nodes
458: of a most general derivation tree for
459: $P \cup \{{\tt go} \leftarrow Q\}$ with head $\tt go$, visited
460: left to right.
461: \end{enumerate}
462: \end{propo}
463:
464:
465: \subsection{Typed Logic Programming}\label{typed-prog-subsec}
466: We assume a type system for logic programs with parametric
467: polymorphism but without subtyping,
468: as realised in the languages G\"odel~\cite{goedel} or
469: Mercury~\cite{mercury}.
470:
471: The set of types $\mathcal T$ is given by the term structure based on
472: a finite set of {\bf constructors} $\mathcal K$, where with each
473: $K\in\mathcal{K}$ an arity
474: $m\geq 0$ is associated (by writing $K/m$),
475: and a denumerable set $\mathcal U$ of
476: {\bf parameters}.
477: A {\bf type substitution} is an idempotent mapping
478: from parameters to types which is the identity almost everywhere.
479: The set of parameters in a syntactic object $o$ is denoted by $\pars(o)$.
480:
481: We assume a denumerable set $\mathcal V$ of {\bf variables}.
482: The set of variables in a syntactic object $o$ is
483: denoted by $\vars(o)$.
484: A {\bf variable typing} is a mapping from a finite subset of
485: $\mathcal V$ to $\mathcal T$, written as
486: $\{x_1:\tau_1,\dots,x_m:\tau_m\}$.
487:
488: We assume a finite set $\mathcal F$ (resp.~$\mathcal P$)
489: of {\bf function} (resp.~{\bf predicate}) symbols, each
490: with an arity and a {\bf declared type} associated with it,
491: such that:
492: for each $f \in \mathcal F$, the declared type has the form
493: $(\tau_1,\dots,\tau_m,\tau)$,
494: where $m$ is the arity of $f$,
495: $(\tau_1,\dots,\tau_m)\in {\mathcal T}^m$,
496: and $\tau$
497: satisfies the {\em transparency condition} \cite{HT92-new}:\label{transparency}
498: $\pars(\tau_1,\dots,\tau_m) \subseteq \pars(\tau)$;
499: for each $p \in \mathcal P$, the declared type has the form
500: $(\tau_1,\dots,\tau_m)$,
501: where $m$ is the arity of $p$ and
502: $(\tau_1,\dots,\tau_m)\in {\mathcal T}^m$.
503: We often indicate the declared types by writing
504: $\ftau$ and $\ptau$, however we assume that the parameters in
505: $\tau_1,\dots,\tau_m,\tau$ are fresh for each occurrence of $f$ or $p$.
506: We assume that there is a special predicate symbol
507: $=_{u,u}$
508: where $u\in \mathcal U$.
509:
510: Throughout this paper, we assume $\mathcal K$, $\mathcal F$, and
511: $\mathcal P$ arbitrary but fixed.
512: %In examples, we loosely follow G\"odel syntax~\cite{goedel}.
513: The {\bf typed language}, i.e.\ a language of terms, atoms etc.\ based
514: on $\mathcal K$, $\mathcal F$, and $\mathcal P$, is defined by the
515: rules
516: in Table \ref{rules-tab}. All objects are defined relative to
517: a variable typing $U$, and $\_\vdash\dots$ stands for ``there exists
518: $U$ such that $U\vdash\dots$''. The expressions below the line are called
519: {\bf type judgements}.
520:
521: \begin{table}[t]
522: \caption{Rules defining a typed language\label{rules-tab}}
523: \begin{center}
524: \begin{tabular}{lll}
525: {\em (Var)} &
526: $\{x:\tau,\dots\}\vdash x:\tau$\\[2ex]
527: {\em (Func)} &
528: \Large
529: $\frac%
530: {U\vdash t_1:\tau_1\Theta\ \cdots \ U\vdash t_m:\tau_m\Theta}%
531: {U\vdash\ftau(t_1,\dots,t_m):\tau\Theta}$ &
532: $\Theta$ is a type substitution\\[2ex]
533: {\em (Atom)} &
534: \Large
535: $\frac%
536: {U\vdash t_1:\tau_1\Theta\ \cdots \ U\vdash t_m:\tau_m\Theta}%
537: {U\vdash\ptau(t_1,\dots,t_m)\; \mathit{Atom}}$ &
538: $\Theta$ is a type substitution\\[2ex]
539: {\em (Query)} &
540: \Large
541: $\frac%
542: {U\vdash A_1\; \mathit{Atom}\ \cdots \ U\vdash A_m\; \mathit{Atom}}%
543: {U\vdash A_1,\dots,A_m\; \mathit{Query}}$ \\[2ex]
544: {\em (Clause)} &
545: \Large
546: $\frac%
547: {U\vdash A\; \mathit{Atom} \quad U\vdash Q\; Query}%
548: {U \vdash A \leftarrow Q\; \mathit{Clause}}$ \\[2ex]
549: {\em (Program)} &
550: \Large
551: $\frac%
552: {\_\vdash C_1\; \mathit{Clause} \ \cdots \ \_\vdash C_m\; \mathit{Clause}}%
553: {\_\vdash \{C_1,\dots,C_m\}\; \mathit{Program}}$ \\[2ex]
554: {\em (Queryset)} &
555: \Large
556: $\frac%
557: {\_\vdash Q_1\; \mathit{Query}\ \cdots \ \_\vdash Q_m\; \mathit{Query}}%
558: {\_\vdash \{Q_1,\dots, Q_m\} \; \mathit{Queryset}}$
559: \end{tabular}
560: \end{center}
561: \end{table}
562:
563: Formally, a proof of a type judgement is a tree where the nodes are
564: labelled with judgements and the edges are labelled with rules (e.g.\
565: see Fig.\ \ref{judgment-fig})~\cite{Tho91}.
566: From the form of the rules, it is clear that in order to prove
567: any type judgement, we must, for each occurrence of a term $t$ in the
568: judgement, prove a judgement $\dots \vdash t:\tau$ for some $\tau$.
569: We now define the most general such $\tau$. It exists and can be
570: computed by {\em type inferencing algorithms}~\cite{B95}.
571:
572: \begin{figure}[t]
573: \begin{center}
574: $
575: \begin{array}{ccccc}
576: & \hspace{0.5em} & \vdots & & \vdots
577: \\
578: \raisebox{0pt}[0pt]{\vdots} & &
579: U\vdash \bar{t}_1:\bar{\tau}_1 &
580: \raisebox{-1.3ex}{\dots} &
581: U\vdash \bar{t}_m:\bar{\tau}_m
582: \\
583: \cline{3-3}\cline{5-5}
584: U\vdash \bar{t}:\bar{\tau} & &
585: U\vdash p_1(\bar{t}_1)\ \mathit{Atom} & &
586: U\vdash p_m(\bar{t}_m)\ \mathit{Atom}
587: \\
588: \cline{1-1}\cline{3-5}
589: U\vdash p(\bar{t})\ \mathit{Atom} & &
590: \multicolumn{3}{c}{U\vdash p_1(\bar{t}_1),\dots,p_m(\bar{t}_m)\ \mathit{Query}}
591: \\\hline
592: \multicolumn{5}{c}{U\vdash p(\bar{t})\leftarrow p_1(\bar{t}_1),\dots,p_m(\bar{t}_m)\ \mathit{Clause}}
593: \end{array}
594: $
595: \end{center}
596: \caption{Proving a type judgement\label{judgment-fig}}
597: \end{figure}
598:
599: \begin{defi}\label{most-general-def}
600: Consider a judgement
601: $U\vdash p(\bar{t})\leftarrow p_1(\bar{t}_1),\dots,p_m(\bar{t}_m)\
602: \mathit{Clause}$,
603: and a proof of this judgement containing judgements
604: $U\vdash \bar{t}:\bar{\tau}$,
605: $U\vdash \bar{t}_1:\bar{\tau}_1$, \dots,
606: $U\vdash \bar{t}_m:\bar{\tau}_m$ (see Fig.\ \ref{judgment-fig})
607: such that
608: $(\bar{\tau},\bar{\tau}_1,\dots,\bar{\tau}_m)$ is
609: most general (wrt.\ all such proofs).
610: We call $(\bar{\tau},\bar{\tau}_1,\dots,\bar{\tau}_m)$ the
611: {\bf most general type}
612: of $p(\bar{t})\leftarrow p_1(\bar{t}_1),\dots,p_m(\bar{t}_m)$
613: {\bf wrt.\ $U$}.
614:
615: Moreover, consider the variable typing $U'$ and the proof of the judgement
616: $U'\vdash p(\bar{t})\leftarrow p_1(\bar{t}_1),\dots,p_m(\bar{t}_m)\
617: \mathit{Clause}$\hspace{0.5em} containing judgments
618: $U'\vdash \bar{t}:\bar{\tau}$,
619: $U'\vdash \bar{t}_1:\bar{\tau}_1$, \dots,
620: $U'\vdash \bar{t}_m:\bar{\tau}_m$ such that
621: $(\bar{\tau},\bar{\tau}_1,\dots,\bar{\tau}_m)$ is
622: most general (wrt.\ all such proofs and all possible $U'$).
623: We call $(\bar{\tau},\bar{\tau}_1,\dots,\bar{\tau}_m)$ the
624: {\bf most general type}
625: of $p(\bar{t})\leftarrow p_1(\bar{t}_1),\dots,p_m(\bar{t}_m)$.
626: \end{defi}
627:
628: The following example explains the difference between the most general
629: type wrt.\ a fixed variable typing, and the most general type as such.
630:
631: \begin{example}\label{most-general-example}
632: Consider function
633: $\tt nil_{\rightarrow list(U)}$ and clause
634: $C = \tt p \leftarrow X\! =\! nil,$
635: $\tt nil\! =\! nil$.
636: Fixing $U= \{\tt X:list(int)\}$, the judgement
637: $U\vdash C\ \mathit{Clause}$ can be proven using
638: the judgements
639: $U\vdash \tt X: list(int)$ and then
640: $U\vdash \tt nil: list(int)$ for {\em each} occurrence
641: of $\tt nil$. It can also be proven
642: using the judgements
643: $U\vdash \tt X: list(int)$ and then
644: $U\vdash \tt nil: list(int)$ (for the first occurrence of
645: $\tt nil$) and then
646: $U\vdash \tt nil: list(V)$ (for the other two occurrences of
647: $\tt nil$). In the latter case, we obtain
648: $(\tt list(int), list(int), list(V), list(V))$, the most general
649: type of $C$ wrt.\ $U$.
650: Moreover,
651: $(\tt list(V'), list(V'), list(V), list(V))$ is the most general type
652: of $C$ (choose $U' = \{\tt X:list(V')\}$).
653: \end{example}
654:
655: \begin{defi}\label{substitution-def}
656: If
657: $U\vdash x_1\!=\!t_1, \dots, x_m\! =\! t_m\ Query$
658: where $x_1,\dots,x_m$ are distinct variables and for
659: each $i\in \onetom$, $t_i$ is a term distinct from $x_i$, then
660: $(\{ x_1/t_1,\dots,x_m/t_m\}, U)$ is a
661: {\bf typed (term) substitution}.
662: %The application of a substitution is
663: %defined in the usual way.
664: \end{defi}
665:
666:
667: We shall need three fundamental lemmas introduced
668: in~\cite{HT92-new}.\footnote{
669: Note that some results in~\cite{HT92-new}
670: have been shown to be faulty (Lemmas 1.1.7, 1.1.10 and 1.2.7),
671: although we believe that these mistakes only affect type systems
672: which include subtyping.}
673:
674: \begin{rmlemma}~\cite[Lemma~1.2.8]{HT92-new}\label{variable-typing-lemma}
675: Let $U$ be a variable typing and $\Theta$ a type
676: substitution.
677: If $U\vdash t:\sigma$, then
678: $U\Theta\vdash t:\sigma\Theta$.
679: Moreover, if
680: $U\vdash A\ \mathit{Atom}$ then $U\Theta\vdash A\ \mathit{Atom}$, and
681: likewise for queries and clauses.
682: \end{rmlemma}
683: \begin{proof}
684: The proof is by structural induction. For the base case, suppose
685: $U\vdash x:\sigma$ where $x\in \mathcal V$. Then
686: $x: \sigma \in U$ and hence $x:\sigma\Theta \in U\Theta$. Thus
687: $U\Theta\vdash x:\sigma\Theta$.
688:
689: Now consider
690: $U\vdash \ftau(t_1,\dots,t_m):\sigma$
691: where the inductive hypothesis holds for $t_1,\dots,t_m$.
692: By Rule {\em (Func)}, there exists a type
693: substitution $\Theta'$ such that $\sigma=\tau\Theta'$
694: and $U\vdash t_i:\tau_i\Theta'$
695: for each $i \in \onetom$.
696: By the inductive hypothesis,
697: $U\Theta \vdash t_i:\tau_i\Theta'\Theta$ for each
698: $i\in\onetom$, and hence by
699: Rule {\em (Func)},
700: $U\Theta\vdash \ftau(t_1,\dots,t_m): \tau\Theta'\Theta$.
701:
702: The rest of the proof is now trivial.
703: \end{proof}
704:
705: \begin{rmlemma}~\cite[Lemma~1.4.2]{HT92-new}\label{apply-substitution-lemma}
706: Let $(\theta,U)$ be a typed substitution.
707: If $U\vdash t:\sigma$ then $U\vdash t\theta :\sigma$. Moreover, if
708: $U\vdash A\ \mathit{Atom}$ then $U\vdash A\theta\ \mathit{Atom}$,
709: and likewise for queries and clauses.
710: \end{rmlemma}
711: \begin{proof}
712: The proof is by structural induction. For the base case, suppose
713: $U\vdash x:\sigma$ where $x\in \mathcal V$. If
714: $x\theta=x$, there is nothing to show. If $x/t \in \theta$, then by
715: definition of a typed substitution,
716: $U\vdash t: \sigma$.
717:
718: Now consider
719: $U\vdash \ftau(t_1,\dots,t_m) :\sigma$
720: where the inductive hypothesis holds for $t_1,\dots,t_m$.
721: By Rule {\em (Func)}, there exists a type
722: substitution $\Theta'$ such that $\sigma=\tau\Theta'$,
723: and $U\vdash t_i:\tau_i\Theta'$ for each $i \in \onetom$.
724: By the inductive hypothesis,
725: $U\vdash t_i\theta:\tau_i\Theta'$ for each $i\in\onetom$, and hence by
726: Rule {\em (Func)},
727: $U\vdash \ftau(t_1,\dots,t_m)\theta : \tau\Theta'$.
728:
729: The rest of the proof is now trivial.
730: \end{proof}
731:
732:
733: \begin{rmlemma}~\cite[Thm.\ 1.4.1]{HT92-new}\label{is-substitution-lemma}
734: Let $E$ be a set (conjunction) of equations such that for some
735: variable typing $U$, we have $U\vdash E\ \mathit{Query}$. Suppose
736: $\theta$ is an MGU of $E$. Then $(\theta,U)$ is a typed substitution.
737: \end{rmlemma}
738: \begin{proof}
739: We show that the result is true when $\theta$ is computed using the
740: well-known Martelli-Montanari algorithm~\cite{MM82} which works by
741: transforming a set of equations $E=E_0$ into a set of the form required
742: in the definition of a typed substitution. Only the following two
743: transformations are considered here. The others are trivial.
744: \begin{enumerate}
745: \item\label{replacement}
746: If $x=t\in E_k$ and $x$ does not occur in $t$,
747: then replace all occurrences of $x$ in all other equations in $E$ with
748: $t$, to obtain $E_{k+1}$.
749: \item\label{decomposition}
750: If $f(t_1,\dots,t_m)=f(s_1,\dots,s_m)\in E_k$, then replace this
751: equation with $t_1=s_1,\dots,t_m=s_m$, to obtain $E_{k+1}$.
752: \end{enumerate}
753: We show that if $U\vdash E_k\ \mathit{Query}$ and
754: $E_{k+1}$ is obtained by either of the above transformations,
755: then $U\vdash E_{k+1}\ \mathit{Query}$.
756: For (\ref{replacement}), this follows from
757: Lemma~\ref{apply-substitution-lemma}.
758:
759: For (\ref{decomposition}), suppose $U\vdash E_k\ \mathit{Query}$ and
760: $f(t_1,\dots,t_m)=f(s_1,\dots,s_m)\in E_k$ where $f=\ftau$.
761: By Rule {\em (Query)}, we must have
762: $U\vdash f(t_1,\dots,t_m)=_{u, u}f(s_1,\dots,s_m)\ \mathit{Atom}$,
763: and hence by Rule {\em (Atom)},
764: $U\vdash f(t_1,\dots,t_m): u\Theta$ and
765: $U\vdash f(s_1,\dots,s_m): u\Theta$ for some type substitution
766: $\Theta$. On the other hand, by Rule {\em (Func)},
767: $u\Theta= \tau\Theta_t$ and
768: $u\Theta= \tau\Theta_s$ for some type substitutions $\Theta_s$ and
769: $\Theta_t$, and moreover for each $i\in\onetom$, we have
770: $U\vdash t_i: \tau_i\Theta_t$ and
771: $U\vdash s_i: \tau_i\Theta_s$.
772: Since
773: $\pars(\tau_i) \subseteq \pars(\tau)$, it follows that
774: $\tau_i\Theta_t = \tau_i\Theta_s$.\footnote{
775: Note how the transparency condition is essential to ensure that
776: subarguments in corresponding positions have identical types. This
777: condition was ignored in~\cite{MO84}.}
778: Therefore $U\vdash t_i=s_i\ \mathit{Atom}$, and so
779: $U\vdash E_{k+1}\ \mathit{Query}$.
780: \end{proof}
781:
782: \section{Subject Reduction for Derivation Trees}
783: \label{trees-sec}
784:
785: We first define subject reduction as
786: a property of derivation trees and show that
787: it is equivalent to the usual operational notion.
788: We then show that a sufficient condition for
789: subject reduction is that the types of all
790: unified terms are themselves unifiable.
791: %illustrate that it is crucial for
792: %subject reduction that unified terms have unifiable types.
793: %Finally, we illustrate how the head condition~\cite{HT92-new}
794: %ensures type unifiability.
795:
796:
797: \subsection{Proof-Theoretic and Operational Subject Reduction}
798: Subject reduction is a well-understood concept, yet it has to be
799: defined formally for each system. We now provide two fundamental
800: definitions.
801:
802: \begin{defi}
803: %defterm[subject reduction wrt $\mathcal Q$]
804: \label{subj-red-def}\label{subj-red-oper-def}
805: Let $\_\vdash P \ \mathit{Program}$ and
806: $\_\vdash\mathcal Q\ \mathit{Queryset}$.
807: We say $P$ has
808: {\bf (proof-theoretic) subject reduction wrt.~$\mathcal Q$} if
809: for every $ Q \in \mathcal Q$, for every
810: most general derivation tree $T$ for
811: $P\cup \{{\tt go} \leftarrow Q\}$ with head $\tt go$,
812: there exists a variable typing $U'$ such that for each
813: node atom $a$ of $T$,
814: $U'\vdash a\ \mathit{Atom}$.
815:
816: $P$ has {\bf operational subject reduction wrt.~$\mathcal Q$}
817: if for every $ Q \in \mathcal Q$, for every
818: derivation $Q \leadsto^* Q'$ of $P$, we have
819: $\_\vdash Q'\ \mathit{Query}$.
820: \end{defi}
821:
822: The reference to $\mathcal Q$ is omitted if
823: $\mathcal Q=\{ Q\mid \_\vdash Q\ \mathit{Query}\}$.
824: The following theorem states a certain equivalence between the two
825: notions.
826:
827: \begin{rmtheorem}\label{decl-oper-theo}
828: Let $\_\vdash P \ \mathit{Program}$ and $\_\vdash\mathcal Q\ \mathit{Queryset}$.
829: If $P$ has subject reduction wrt.~$\mathcal Q$, then
830: $P$ has operational subject reduction wrt.~$\mathcal Q$.
831: If $P$ has operational subject reduction, then
832: $P$ has subject reduction.
833: \end{rmtheorem}
834: \begin{proof}
835: The first statement is a straightforward consequence of
836: Prop.~\ref{semant-equiv-propo} (\ref{tree=operational}).
837:
838: For the second statement, assume $U\vdash Q\ \mathit{Query}$, let
839: $\xi = Q \leadsto^* Q'$, and $T$ be the derivation tree
840: for $P \cup \{{\tt go} \leftarrow Q\}$ corresponding to $\xi$ (by
841: Prop.~\ref{semant-equiv-propo} (\ref{tree=operational})).
842:
843: By hypothesis, there exists a variable typing $U'$ such that for each
844: {\em incomplete} node $n$ of $T$, we have
845: $U'\vdash atom(n)\ \mathit{Atom}$. To show that this also holds for {\em complete}
846: nodes, we transform $\xi$ into a derivation which ``records the
847: entire tree $T$''. This is done as follows: Let $\tilde{P}$ be the program
848: obtained from $P$ by replacing each clause $h \leftarrow B$ with
849: $h \leftarrow B, B$. Let us call the atoms in the second occurrence of
850: $B$ {\em unresolvable}. Clearly
851: $\_\vdash h \leftarrow B, B\ \mathit{Clause}$ for each such clause.
852:
853: By induction on the length of derivations, one can show that $\tilde{P}$
854: has operational subject reduction. For a single derivation step, this
855: follows from the operational subject reduction of $P$.
856:
857: Now let $\tilde{\xi}= {\tt go} \leadsto \tilde{Q}'$ be the
858: derivation for
859: $\tilde{P} \cup \{{\tt go} \leftarrow Q, Q\}$ using in each
860: step the clause corresponding to the clause used in $\xi$ for that
861: step, and resolving only the resolvable atoms. First note that
862: since $\tilde{P}$ has operational subject reduction, there exists a
863: variable typing $U'$ such that $U'\vdash \tilde{Q}' \ \mathit{Query}$.
864: Moreover, since the unresolvable atoms are not
865: resolved in $\tilde{\xi}$, it follows that $\tilde{Q}'$ contains
866: exactly the non-root node atoms of $T$. This however shows
867: that for each node atom $a$ of $T$, we have
868: $U'\vdash a\ \mathit{Atom}$. Since the choice of $Q$ was arbitrary,
869: $P$ has subject reduction.
870: \end{proof}
871:
872:
873: The following example shows that in the second statement of the above
874: theorem, it is crucial that $P$ has operational subject reduction
875: wrt.~{\em all} queries.
876:
877: \begin{example}\label{oper-SR-only-ex}
878: Let
879: $\mathcal{K} = \{\mathtt{list}/1, \mathtt{int}/0\}$,
880: $\mathcal{F} = \{
881: \mathtt{nil_{\rightarrow list(U)}},$
882: $\mathtt{cons_{U,list(U)\rightarrow list(U)}},$
883: $\mathtt{-1_{\rightarrow int}}, $
884: $\mathtt{0_{\rightarrow int}},\dots\}$,
885: $\mathcal{P} = \{
886: \mathtt{p_{list(int)}},$
887: $\mathtt{r_{list(U)}}\}$, and $P$ be
888:
889: {%\small
890: \begin{verbatim}
891: p(X) <- r(X). r([X]) <- r(X).
892: \end{verbatim}
893: }
894:
895: \noindent
896: For each derivation
897: ${\tt p(X)} \leadsto^* Q'_0$, we have
898: $Q'_0= \tt p(Y)$ or $Q'_0= \tt r(Y)$ for some
899: ${\tt Y}\in\mathcal{V}$, and so
900: $\{\tt Y : list(int)\}\vdash {\tt p(Y)}\ \mathit{Query}$ or
901: $\{\tt Y : list(U)\}\vdash {\tt r(Y)}\ \mathit{Query}$.
902: Therefore $P$ has operational subject reduction
903: wrt.~$\{\tt p(X)\}$. Yet the derivation trees for $P$ have heads
904: $\tt p(Y)$, $\tt p([Y])$, $\tt p([[Y]])$ etc., and
905: $\_\not\vdash {\tt p([[Y]])}\ \mathit{Query}$.
906: \end{example}
907:
908:
909:
910: \subsection{Unifiability of Types and Subject Reduction}
911: We now lift the notion of skeleton to the type level.
912:
913: \begin{defi}
914: %defterm[type skeleton]
915: \label{type-skel-def}
916: Let $\_\vdash P \ \mathit{Program}$ and
917: $S$ be a skeleton for $P$.
918: The {\bf type skeleton corresponding to} $S$
919: is a tree obtained from $S$ by replacing each
920: node label
921: $C_n = p(\bar{t})\leftarrow p_1(\bar{t}_1),\dots,p_m(\bar{t}_m)$
922: with
923: $p(\bar{\tau})\leftarrow p_1(\bar{\tau}_1),\dots,p_m(\bar{\tau}_m)$,
924: where $(\bar{\tau},\bar{\tau}_1,\dots,\bar{\tau}_m)$ is the most
925: general type of $C_n$.\footnote{
926: Recall that the variables in $C_n$ and the parameters in
927: $\bar{\tau},\bar{\tau}_1,\dots,\bar{\tau}_m$
928: are renamed apart from other node labels in the same (type) skeleton.}
929: %
930: For a type skeleton $\mathit{TS}$, the {\bf type equation set}
931: $\mathit{Eq}(\mathit{TS})$ and a {\bf proper} type skeleton are defined as
932: in Def.~\ref{eqs-def}.
933: \end{defi}
934:
935:
936:
937: The following theorem states that subject reduction is ensured if
938: terms are unified only if their types are also unifiable.
939:
940: \begin{rmtheorem}\label{type-tree-theorem}
941: Let $\_\vdash P \ \mathit{Program}$ and $\_\vdash \mathcal{Q} \ \mathit{Queryset}$.
942: $P$ has subject reduction wrt.~$\mathcal Q$ if for each proper
943: skeleton $S$ of $P\cup\{{\tt go} \leftarrow Q\}$ with head $\tt go$,
944: where $Q\in\mathcal{Q}$,
945: the {\em type} skeleton corresponding to $S$ is proper.
946: \end{rmtheorem}
947: \begin{proof}
948: Let $S$ be an arbitrary proper
949: skeleton for
950: $P\cup\{{\tt go}\leftarrow Q\}$ with head $\tt go$, where
951: $Q\in \mathcal Q$. Let $\theta=MGU(Eq(S))$ and
952: $\Theta=MGU(Eq(TS))$.
953: For each node $n$ in $S$, labelled
954: $p(\bar{t})\leftarrow p_1(\bar{t}_1),\dots,p_m(\bar{t}_m)$ in
955: $S$ and
956: $p(\bar{\tau})\leftarrow p_1(\bar{\tau}_1),\dots,p_m(\bar{\tau}_m)$ in
957: $TS$, let $U_n$ be the variable typing such that
958: $U_n\vdash
959: (\bar{t},\bar{t}_1,\dots,\bar{t}_m):
960: (\bar{\tau},\bar{\tau}_1,\dots,\bar{\tau}_m)$.
961: Let
962: \[
963: U =
964: \bigcup_{n \in S}
965: U_n\Theta.
966: \]
967: Consider a pair of nodes $n$, $n'$ in $S$ such that
968: $n'$ is a child of $n$, and the equation
969: $p(\bar{s})=p(\bar{s}') \in Eq(S)$ corresponding to this pair (see
970: Def.~\ref{eqs-def}). Consider also the equation
971: $p(\bar{\sigma}) = p(\bar{\sigma}') \in Eq(TS)$ corresponding to the pair
972: $n$, $n'$ in $TS$. Note that
973: $U_n \vdash \bar{s}: \bar{\sigma}$ and
974: $U_{n'}\vdash \bar{s}':\bar{\sigma}'$.
975: By Lemma~\ref{variable-typing-lemma},
976: $U\vdash\bar{s} :\bar{\sigma} \Theta$ and
977: $U\vdash\bar{s}':\bar{\sigma}'\Theta$.
978: Moreover, since $\Theta=MGU(Eq(TS))$, we have
979: $\bar{\sigma}\Theta=\bar{\sigma}'\Theta$.
980: Therefore
981: $U\vdash p(\bar{s}) = p(\bar{s}')\ \mathit{Atom}$.
982: Since the same reasoning applies for any equation in
983: $Eq(S)$, by Lemma~\ref{is-substitution-lemma}, $(\theta,U)$ is a typed
984: substitution.
985:
986: Consider a node $n''$ in $S$ with node atom $a$.
987: Since $U_{n''}\vdash a\ \mathit{Atom}$,
988: by Lemma~\ref{variable-typing-lemma},
989: $U\vdash a\ \mathit{Atom}$. and
990: by Lemma~\ref{apply-substitution-lemma},
991: $U\vdash a\theta\ \mathit{Atom}$.
992: Therefore $P$ has subject
993: reduction wrt.~$\mathcal Q$.
994: \end{proof}
995:
996:
997: \setlength{\unitlength}{0.42cm}
998: \begin{figure}[t]
999: \begin{picture}(12,7)
1000: \put(0,0){\makebox(12,1){$\tt r([X''']) \leftarrow r(X''')$}}
1001: \put(6,1){\line(0,1){1}}
1002: \put(0,2){\makebox(12,1){$\tt r([X'']) \leftarrow r(X'')$}}
1003: \put(6,3){\line(0,1){1}}
1004: \put(0,4){\makebox(12,1){$\tt p(X') \leftarrow r(X')$}}
1005: \put(6,5){\line(0,1){1}}
1006: \put(0,6){\makebox(12,1){$\tt go \leftarrow p(X)$}}
1007: \end{picture}
1008: \hfill
1009: \begin{picture}(12,7)
1010: \put(0,0){\makebox(12,1){$\tt r(list(U''')) \leftarrow r(U''')$}}
1011: \put(6,1){\line(0,1){1}}
1012: \put(0,2){\makebox(12,1){$\tt r(list(U'')) \leftarrow r(U'')$}}
1013: \put(6,3){\line(0,1){1}}
1014: \put(0,4){\makebox(12,1){$\tt p(list(int)) \leftarrow r(list(int))$}}
1015: \put(6,5){\line(0,1){1}}
1016: \put(0,6){\makebox(12,1){$\tt go \leftarrow p(list(int))$}}
1017: \end{picture}
1018: \caption{A skeleton and the corresponding
1019: {\em non-proper} type skeleton\label{proper-nonproper-fig}
1020: for Ex.~\ref{oper-SR-only-ex}}
1021: \end{figure}
1022:
1023: \begin{example}\label{append-ex}
1024: Figure \ref{proper-nonproper-fig} shows a proper skeleton and the
1025: corresponding {\em non-proper} type skeleton for the program in
1026: Ex.~\ref{oper-SR-only-ex}.
1027:
1028: In contrast,
1029: let $\mathcal K$ and $\mathcal F$ be as in
1030: Ex.~\ref{oper-SR-only-ex}, and
1031: $\mathcal P =
1032: \{ \tt app_{list(U),list(U),list(U)},$
1033: $\tt r_{list(int)} \}$. Let $P$ be the program shown in Fig.\
1034: \ref{append-prog-fig}.
1035: The most general type of each clause is indicated as comment.
1036: Figure~\ref{append-fig} shows a skeleton $S$ and the corresponding
1037: type skeleton $\mathit{TS}$ for $P$. A solution of
1038: $\mathit{Eq}(\mathit{TS})$ is obtained
1039: %The type derivation tree is obtained
1040: by instantiating all parameters with $\tt int$.
1041: \end{example}
1042:
1043:
1044:
1045: \begin{figure}[t]
1046: %\small
1047: \begin{verbatim}
1048: app([],Ys,Ys). %app(list(U),list(U),list(U))
1049: app([X|Xs],Ys,[X|Zs]) <- %app(list(U),list(U),list(U))
1050: app(Xs,Ys,Zs). %app(list(U),list(U),list(U))
1051:
1052: r([1]). %r(list(int))
1053:
1054: go <-
1055: app(Xs,[],Zs), %app(list(int),list(int),list(int))
1056: r(Xs). %r(list(int))
1057: \end{verbatim}
1058: \caption{A program used to illustrate type skeletons\label{append-prog-fig}}
1059: \end{figure}
1060:
1061: \setlength{\unitlength}{0.46cm}
1062: \begin{figure}[t]
1063: \begin{picture}(13,6)
1064: \put(0,0){\makebox(10,1){$\tt app([],Ys'',Ys'')$}}
1065: \put(5,1){\line(0,1){1}}
1066: \put(0,2){\makebox(10,2){$
1067: \begin{array}{l}
1068: \tt app([X'|Xs'],Ys',[X'|Zs']) \leftarrow\\
1069: \quad \quad \quad \tt app(Xs',Ys',Zs')
1070: \end{array}$}}
1071: \put(10,2){\makebox(3,2){$\tt r([1])$}}
1072: \put(5,4){\line(1,1){1}}
1073: \put(11.5,4){\line(-1,1){1}}
1074: \put(0,5){\makebox(13,1){$\tt
1075: go \leftarrow app(Xs,[],Zs)\; \und \; r(Xs)$}}
1076: \end{picture}
1077: \hfill
1078: \begin{picture}(13,6)
1079: \put(0,0){\makebox(8,1){$\tt app(list(U'')^3)$}}
1080: \put(4,1){\line(0,1){1}}
1081: \put(0,2){\makebox(8,2){$
1082: \begin{array}{l}
1083: \tt app(list(U')^3) \leftarrow\\
1084: \quad \quad \quad \tt app(list(U')^3)
1085: \end{array}$}}
1086: \put(8,2){\makebox(5,2){$\tt r(list(int))$}}
1087: \put(4,4){\line(1,1){1}}
1088: \put(10.5,4){\line(-1,1){1}}
1089: \put(0,5){\makebox(13,1){$\tt
1090: go \leftarrow app(list(int)^3)\; \und \; r(list(int))$}}
1091: \end{picture}
1092: \caption{A skeleton and the corresponding type skeleton
1093: % and the type derivation tree
1094: for Ex.~\ref{append-ex} \label{append-fig}}
1095: \end{figure}
1096:
1097: \section{Conditions for Subject Reduction}
1098: \label{conditions-sec}
1099: By Thm.~\ref{type-tree-theorem}, a program has subject reduction
1100: if for each proper skeleton, the corresponding type skeleton is
1101: also proper. A more general sufficient condition consists in ensuring
1102: that {\em any} type skeleton is proper. We call this property
1103: {\bf type unifiability}. Arguably, type unifiability is in the spirit
1104: of prescriptive typing, since subject reduction should be independent
1105: of the unifiability of terms, i.e., success or failure of the computation.
1106: However this view has been challenged in the context of higher-order
1107: logic programming~\cite{NP92}.
1108:
1109: We conjecture that both subject reduction and type unifiability are
1110: undecidable. Proving this is a topic for future work.
1111: %In the next subsection, we show the undecidability results.
1112: %We then give a sufficient condition for unifiability of a set of
1113: %equations, show that the head condition implies this condition, and
1114: %present a generalisation.
1115:
1116: \subsection{The Head Condition}
1117:
1118: %The head condition is the standard way~\cite{HT92-new} of ensuring that
1119: %type derivation trees based on type skeletons always exist.
1120: The head condition is the standard way~\cite{HT92-new} of ensuring type unifiability.
1121:
1122: \begin{defi}
1123: %defterm[head condition]
1124: \label{HC-def}
1125: A clause
1126: $C =
1127: p_{\bar{\tau}}(\bar{t}) \leftarrow
1128: B$
1129: fulfills the {\bf head condition} if its most general type has the form
1130: $(\bar{\tau},\dots)$.
1131: \end{defi}
1132:
1133: Note that by the typing rules in Table~\ref{rules-tab}, clearly the
1134: most general type of $C$ must be $(\bar{\tau},\dots)\Theta$ for some
1135: type substitution $\Theta$. Now the head condition states that
1136: the type of the head arguments must be the declared type of the
1137: predicate, or in other words, $\Theta\restr{\bar{\tau}}=\emptyset$.
1138: It has been shown previously that typed programs
1139: fulfilling the head condition have operational subject
1140: reduction~\cite[Theorem 1.4.7]{HT92-new}.
1141: By Thm.~\ref{decl-oper-theo}, this means that they have subject
1142: reduction.
1143:
1144: \subsection{Generalising the Head Condition}
1145: To reason about the existence of a solution for the equation set of a
1146: type skeleton, we give a sufficient condition for unifiability of a finite set
1147: of term equations.
1148:
1149: \begin{propo}\label{eq-unif}
1150: Let
1151: $E = \{l_1=r_1,\dots,l_m=r_m\}$ be a set of oriented equations, and
1152: assume an order relation on the equations such that
1153: $l_1=r_1\rightarrow l_2=r_2$ if $r_1$ and
1154: $l_2$ share a variable. $E$ is unifiable if
1155: \begin{enumerate}
1156: \item \label{equ-c0} for all $1\leq i < j \leq m$, $r_i$ and $r_j$
1157: have no variable in common, and
1158: \item \label{equ-c1} the graph of $\rightarrow$ is a partial order, and
1159: \item \label{equ-c2} for all $i\in\onetom$, $l_i$ is an instance of $r_i$.
1160: \end{enumerate}
1161: \end{propo}
1162:
1163: In fact, the head condition ensures that $\mathit{Eq}(\mathit{TS})$
1164: meets the above conditions for any type skeleton $\mathit{TS}$. The
1165: equations in $\mathit{Eq}(\mathit{TS})$ have the form
1166: $p(\bar{\tau}_a) = p(\bar{\tau}_h)$, where $\bar{\tau}_a$
1167: is the type of an atom and $\bar{\tau}_h$ is the type of a
1168: head. Taking into account that the ``type clauses'' used for
1169: constructing the equations are renamed apart, all the head types
1170: (r.h.s.) have no parameter in common, the graph of $\rightarrow$ is a
1171: tree isomorphic to $\mathit{TS}$, and, by the head
1172: condition, $\bar{\tau}_a$ is an instance of $\bar{\tau}_h$.
1173: In the next subsection, we show that by decomposing each equation
1174: $p(\bar{\tau}_a) = p(\bar{\tau}_h)$, one can refine this condition.
1175:
1176: \subsection{Semi-generic Programs}\label{semi-generic-subsec}
1177: In the head condition, all arguments of a predicate in clause head
1178: position are ``generic'' (i.e.~their type is the declared type). One
1179: might say that all arguments are ``head-generic''. It is thus possible to
1180: generalise the head condition by partitioning the arguments of each
1181: predicate into those which stay head-generic
1182: and those which one requires to be generic for body atoms.
1183: The latter ones will be called {\em
1184: body-generic}.
1185: If we place the head-generic arguments of a
1186: clause head and the body-generic arguments of a clause body on
1187: the right hand sides of the equations associated with a type
1188: skeleton, then Condition~\ref{equ-c2} in Prop.\ \ref{eq-unif} is met.
1189:
1190: The other two conditions can be obtained in various ways, more or less
1191: complex to verify (an analysis of the analogous problem of
1192: not being subject to occur check (NSTO) can be found in~\cite{DM93}).
1193: Taking into account the renaming of
1194: ``type clauses'', a relation between two equations amounts to a
1195: shared parameter between a generic argument (r.h.s.) and a non-generic
1196: argument (l.h.s.) of a clause.
1197: We propose here a condition on the clauses which implies that
1198: the equations of any skeleton can be ordered.
1199:
1200: In the following, an atom written as $p(\bar{s},\bar{t})$
1201: means: $\bar{s}$ and $\bar{t}$ are the vectors of terms
1202: filling the head-generic and body-generic positions of $p$,
1203: respectively. The notation $p(\bar{\sigma},\bar{\tau})$, where $\sigma$
1204: and $\tau$ are types, is defined analogously.
1205:
1206: \begin{defi}
1207: %defterm[semi-generic]
1208: \label{semi-generic-def}
1209: Let $\_\vdash P\ \mathit{Program}$ and
1210: $\_\vdash C\ \mathit{Clause}$ where
1211: \[
1212: C =
1213: p_{\bar{\tau}_0,\bar{\sigma}_{m+1}}(\bar{t}_0,\bar{s}_{m+1}) \leftarrow
1214: p^1_{\bar{\sigma}_1,\bar{\tau}_1}(\bar{s}_1,\bar{t}_1),\dots,
1215: p^m_{\bar{\sigma}_m,\bar{\tau}_m}(\bar{s}_m,\bar{t}_m),
1216: \]
1217: and
1218: $\Theta$ the type substitution such that
1219: $(\bar{\tau}_0,\bar{\sigma}_{m+1},
1220: \bar{\sigma}_1,\bar{\tau}_1,\dots,
1221: \bar{\sigma}_m,\bar{\tau}_m)\Theta$ is the most general type of $C$.
1222: We call $C$ {\bf semi-generic} if
1223: \begin{enumerate}
1224: \item\label{is-linear}
1225: for all $i,j \in \zerotom$, $i \neq j$,
1226: $\pars(\tau_i\Theta) \cap \pars(\tau_j\Theta) = \emptyset$,
1227: \item\label{is-disjoint}
1228: for all $i \in \onetom$,
1229: $\pars(\bar{\sigma}_i) \cap
1230: \bigcup_{i \leq j \leq m} \pars(\bar{\tau}_j)
1231: = \emptyset$,
1232: \item\label{is-generic}
1233: for all $i \in \zerotom$, $\tau_i \Theta=\tau_i$.
1234: \end{enumerate}
1235:
1236: A query $Q$ is {\bf semi-generic} if the
1237: clause ${\tt go} \leftarrow Q$ is semi-generic.
1238: A program is {\bf semi-generic} if each of its clauses is
1239: semi-generic.
1240: \end{defi}
1241:
1242: Note that semi-genericity has a strong resemblance with
1243: {\em nicely-modedness}, where head-generic corresponds to input, and
1244: body-generic corresponds to output. Nicely-modedness has been used,
1245: among other things, to show that programs are free from
1246: unification~\cite{AE93}. Semi-genericity serves a very similar purpose
1247: here. Note also that a typed program which fulfills the head
1248: condition is semi-generic, where all argument positions are
1249: head-generic.
1250:
1251: The following theorem states subject reduction for semi-generic
1252: programs.
1253:
1254: \begin{rmtheorem}\label{condgen-thm}
1255: Every semi-generic program $P$ has
1256: subject reduction wrt.\ the set of semi-generic queries.
1257: \end{rmtheorem}
1258: \begin{proof}
1259: Let $Q$ be a semi-generic query and $TS$ a type skeleton corresponding
1260: to a skeleton for
1261: $P\cup \{{\tt go} \leftarrow Q\}$ with head $\tt go$.
1262: Each equation in $Eq(TS)$ originates from a pair of nodes
1263: $(n,n_i)$ where $n$ is labelled
1264: $C = p(\bar{\tau}_0,\bar{\sigma}_{m+1}) \leftarrow
1265: p_1(\bar{\sigma}_1,\bar{\tau}_1),\dots,
1266: p_m(\bar{\sigma}_m,\bar{\tau}_m)$ and $n_i$ is labelled
1267: $C_i = p_i(\bar{\tau}'_i,\bar{\sigma}'_i)\leftarrow\dots$, and the equation
1268: is
1269: $p_i(\bar{\tau}'_i,\bar{\sigma}'_i) =
1270: p_i(\bar{\sigma}_i,\bar{\tau}_i)$.
1271: Let
1272: $Eq'$ be obtained from $Eq(TS)$ by replacing each such equation with
1273: the two equations
1274: $\bar{\sigma}_i = \bar{\tau}'_i$,
1275: $\bar{\sigma}'_i = \bar{\tau}_i$.
1276: Clearly $Eq'$ and $Eq(TS)$ are equivalent. Because of the renaming of
1277: parameters for each node and since $TS$ is a tree, it is possible to
1278: define an order $\dashrightarrow$ on the equations in $Eq'$ such that
1279: for {\em each} label $C$ defined as above,
1280: $\bar{\sigma}_1 = \bar{\tau}'_1 \dashrightarrow
1281: E_1 \dashrightarrow
1282: \bar{\sigma}'_1 = \bar{\tau}_1 \dashrightarrow
1283: \dots \dashrightarrow
1284: \bar{\sigma}_m = \bar{\tau}'_m \dashrightarrow
1285: E_m \dashrightarrow
1286: \bar{\sigma}'_m = \bar{\tau}_m$,
1287: where for each $i\in\onetom$,
1288: $E_i$ denotes a sequence containing all equations
1289: $e$ with $\pars (e) \cap \pars(C_i) \neq \emptyset$.
1290:
1291: We show that $Eq'$ fulfills the conditions of Prop.\ \ref{eq-unif}.
1292: By Def.~\ref{semi-generic-def} (\ref{is-linear}), $Eq'$ fulfills
1293: condition~\ref{equ-c0}.
1294: By Def.~\ref{semi-generic-def} (\ref{is-disjoint}), it follows that
1295: $\rightarrow$ is a subrelation of $\dashrightarrow$, and hence
1296: $Eq'$ fulfills condition~\ref{equ-c1}.
1297: By Def.~\ref{semi-generic-def} (\ref{is-generic}), $Eq'$ fulfills
1298: condition~\ref{equ-c2}.
1299:
1300: Thus $Eq(TS)$ has a solution, so $TS$ is proper, and so by Thm.\
1301: \ref{type-tree-theorem}, $P$ has subject reduction wrt.\ the set of
1302: semi-generic queries.
1303: \end{proof}
1304:
1305: The following example shows that our condition
1306: extends the class of programs that have subject reduction.
1307:
1308: \begin{example}\label{semi-generic-ex}
1309: Suppose $\mathcal{K}$ and $\mathcal{F}$ define lists as usual (see
1310: Ex.\ \ref{oper-SR-only-ex}). Let
1311: $\mathcal{P} =
1312: \{\tt p_{U,V}, q_{U,V}\}$ and assume that for
1313: $\tt p, q$, the first argument is head-generic and the
1314: second argument is body-generic.
1315: Consider the following program.
1316:
1317: \begin{verbatim}
1318: p(X,[Y]) <- %p(U,list(V)) <-
1319: q([X],Z), q([Z],Y). % q(list(U),W), q(list(W),V).
1320: q(X,[X]). %q(U,list(U)).
1321: \end{verbatim}
1322:
1323: This program is semi-generic. E.g.\ in the first type clause the terms
1324: in generic positions are $\tt U,W, V$; all generic arguments have the
1325: declared type (condition~\ref{is-generic}); they do not share a
1326: parameter (condition~\ref{is-linear}); no generic argument in the body
1327: shares a parameter with a non-generic position to the left of it
1328: (condition~\ref{is-disjoint}). A type skeleton is shown in
1329: Fig.~\ref{semi-generic-fig}.
1330:
1331: \setlength{\unitlength}{0.52cm}
1332: \begin{figure}[t]
1333: %\begin{picture}(4,3) %%
1334: %\put(0,0){\makebox(4,1){ %%
1335: % $\tt q(X,[X])$}} %%
1336: %\end{picture} %%
1337: \begin{center}
1338: \begin{picture}(13,3)
1339: \put(0,0){\makebox(5,1){$\tt q(U',list(U'))$}}
1340: \put(8,0){\makebox(5,1){$\tt q(U'',list(U''))$}}
1341: \put(2.5,1){\line(1,1){1}}
1342: \put(10.5,1){\line(-1,1){1}}
1343: \put(0,2){\makebox(13,1){$
1344: \tt p(U,list(V)) \leftarrow q(list(U),W), q(list(W),V)$}}
1345: \end{picture}
1346: \end{center}
1347: \caption{A type skeleton
1348: for a semi-generic program\label{semi-generic-fig}}
1349: \end{figure}
1350:
1351: As another example, suppose now that
1352: $\mathcal{K}$ and $\mathcal{F}$ define list and integers,
1353: and consider the predicate ${\tt r}/2$ specified as
1354: $\tt r(1,[]), r(2,[[]]), r(3,[[[]]])\dots$. Its obvious definition
1355: would be
1356:
1357: {%\small
1358: \begin{verbatim}
1359: r(1,[]).
1360: r(J,[X]) <- r(J-1,X).
1361: \end{verbatim}
1362: }
1363: One can see that this program must violate the head condition no
1364: matter what the declared type of $\tt r$ is. However, assuming
1365: declared type $\tt (int,list(U))$ and letting the second argument be
1366: body-generic, the program is semi-generic.
1367: \end{example}
1368:
1369: One can argue that in the second example, there is an intermingling of
1370: the typing and the computation, which contradicts the spirit of
1371: prescriptive typing. However, as we discuss in the next section,
1372: the situation is not always so clearcut.
1373:
1374: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1375: % end cut pierre.tex
1376: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1377:
1378:
1379: \section{What is the Use of the Head Condition?}
1380: \label{is-restrictive-sec}
1381: The above results shed new light on the head condition. They allow us
1382: to view it as just one particularly simple condition guaranteeing
1383: type unifiability and consequently subject reduction and
1384: ``well-typing'' of the result, and hence a certain correctness of the
1385: program. This raises the question whether by generalising the
1386: condition, we have significantly enlarged the class of ``well-typed''
1387: programs.
1388:
1389: However, the head condition is also sometimes viewed as a condition
1390: inherent in the type system, or more specifically, an essential
1391: characteristic of {\em generic} polymorphism, as opposed to
1392: {\em ad-hoc} polymorphism. Generic polymorphism means that
1393: predicates are defined on an infinite number of types and that the
1394: definition is independent of a particular instance of the
1395: parameters. Ad-hoc polymorphism, often called
1396: {\em overloading}~\cite{M78}, means, e.g., to use the same
1397: symbol $+$ for integer addition, matrix addition and list
1398: concatenation. Ad-hoc polymorphism is in fact forbidden by the head
1399: condition.
1400:
1401: One way of reconciling ad-hoc polymorphism with the head condition is
1402: to enrich the type system so that types can be passed as parameters,
1403: and the definition of a predicate depends on these
1404: parameters~\cite{LR96}.
1405: %This view makes the traditional, general meaning of ``parameter''
1406: %(input argument) coincide with the technical meaning (type variable)
1407: %it has in this paper.
1408: Under such conditions, the head condition is regarded as natural.
1409:
1410: So as a second, more general question,
1411: we discuss the legitimacy of the head condition
1412: briefly, since the answer justifies the interest
1413: in our first question.
1414:
1415: In favour of the head condition, one could argue (1) that a program typed
1416: in this way does not compute types, but only propagates them; (2) that it
1417: allows for separate compilation since an imported predicate can be
1418: compiled without consulting its definition; and (3) that it disallows
1419: certain ``unclean'' programs~\cite{craft}.
1420:
1421: In reality, these points are not, strictly speaking, fundamental
1422: arguments in favour of the head condition. Our generalisation does not
1423: necessarily imply a confusion between computation and typing (even if
1424: the result type does not depend on the result of a computation, it may
1425: be an instance of the declared type). Moreover, if the type
1426: declarations of the predicates are accompanied by declarations of the
1427: head- and body-generic arguments, separate compilation remains
1428: possible. Finally, Hanus~\cite{Han92} does not consider the head
1429: condition to be particularly natural, arguing that it is an
1430: important feature of logic programming that it allows for
1431: {\em lemma generation}.
1432:
1433: We thus believe that the first question is, after all, relevant. So
1434: far, we have not been able to identify a ``useful'', non-contrived,
1435: example which clearly shows the interest in the class of
1436: semi-generically typed programs. The following example demonstrates
1437: the need for a generalisation, but also the insufficiency of the class
1438: defined in Def.~\ref{semi-generic-def}.
1439:
1440:
1441: \begin{example}\label{fg-ex}
1442: Let
1443: $\mathcal{K} =$
1444: $\{\mathtt{t}/1, \mathtt{int}/0\}$ and
1445: \[
1446: \mathcal{F} =
1447: \{\mathtt{-1_{\rightarrow int}},
1448: \mathtt{0_{\rightarrow int}},\dots,
1449: \mathtt{c}_\mathtt{\rightarrow t(U)},
1450: \mathtt{g}_\mathtt{U \rightarrow t(U)},
1451: \mathtt{f}_\mathtt{t(t(U)) \rightarrow t(U)}\}.
1452: \]
1453: For all
1454: $i \geq 0$, we have
1455: $\_\vdash \mathtt{g}^i({\tt c}) : {\tt t}^{i+1}({\tt U})$ and
1456: $\_\vdash \mathtt{f}^i(\mathtt{g}^i({\tt c})) : {\tt t}({\tt U})$.
1457: This means that the set
1458: $
1459: \{\sigma \mid \exists s,t.\ \mbox{$s$ is subterm of $t$},
1460: \ \mbox{$\_\vdash s:\sigma$},
1461: \ \mbox{$\_\vdash t:{\tt t(U)}$} \}
1462: $
1463: is infinite, or in words, there are infinitely many types that a
1464: subterm of a term of type $\tt t(U)$ can have.
1465: This property of the type $\tt t(U)$
1466: is very unusual. In~\cite{SHK00}, a condition is considered (the
1467: {\em Reflexive Condition}) which rules out this situation.
1468:
1469: Now consider the predicate ${\tt fgs}/2$ specified as
1470: ${\tt fgs}(i,\mathtt{f}^i(\mathtt{g}^i({\tt c})))$ ($i \in \nat$).
1471: Figure~\ref{fg-fig}
1472: presents three potential definitions of this
1473: predicate. The declared types of the predicates are given by
1474: $\mathcal{P} = $
1475: $\{\tt fgs1_{int, t(U)}, $
1476: $\tt gs1_{int, t(U)},$
1477: $\tt fgs2_{int, t(U)},$
1478: $\tt fgs3_{int, t(U)},$
1479: $\tt fs1_{int, t(U), int},$
1480: $\tt fs2_{int, t(U), int},$\linebreak
1481: $\tt gs2_{int, t(U), t(V)},$
1482: $\tt fgs3\_aux_{int, t(U), t(U)}\}$.
1483: The first solution is the most straightforward one, but its
1484: last clause does not fulfill the head condition. For the second
1485: solution, the fact clause \verb@gs2(0,x,x).@ does not
1486: fulfill the head condition. The third program fulfills the head
1487: condition but is the least obvious solution.
1488:
1489: \begin{figure}[t]
1490: \begin{minipage}{2.95cm}
1491: \small
1492: \begin{verbatim}
1493: fgs1(I,Y) <-
1494: fs1(I,Y,I).
1495:
1496: fs1(I,f(X),J) <-
1497: fs1(I-1,X,J).
1498: fs1(0,X,J) <-
1499: gs1(J,X).
1500:
1501: gs1(J,g(X)) <-
1502: gs1(J-1,X).
1503: gs1(0,c).
1504: \end{verbatim}
1505: \end{minipage}
1506: \hfill
1507: \vline
1508: \hfill
1509: \begin{minipage}{3.35cm}
1510: \small
1511: \begin{verbatim}
1512: fgs2(I,Y) <-
1513: fs2(I,Y,I).
1514:
1515: fs2(I,f(X),J) <-
1516: fs2(I-1,X,J).
1517: fs2(0,X,J) <-
1518: gs2(J,X,c).
1519:
1520: gs2(J,X,Y) <-
1521: gs2(J-1,X,g(Y)).
1522: gs2(0,X,X).
1523: \end{verbatim}
1524: \end{minipage}
1525: \hfill
1526: \vline
1527: \hfill
1528: \begin{minipage}{4.3cm}
1529: \small
1530: \begin{verbatim}
1531: fgs3(I,X) <-
1532: fgs3_aux(I,c,X).
1533:
1534: fgs3_aux(I,X,f(Y)) <-
1535: fgs3_aux(I-1,g(X),Y).
1536: fgs3_aux(0,X,X).
1537:
1538:
1539:
1540:
1541:
1542: \end{verbatim}
1543: \end{minipage}
1544: \caption{Three potential solutions for Ex.~\ref{fg-ex}\label{fg-fig}}
1545: \end{figure}
1546: \end{example}
1547:
1548: For the above example, the head condition is a real restriction.
1549: It prevents a solution using
1550: the most obvious algorithm, which is certainly a drawback of any type
1551: system. We suspected initially that it would be impossible
1552: to write a program fulfilling the specification of $\tt fgs$ without
1553: violating the head condition.
1554:
1555: Now it would of course be interesting to see if the first two
1556: programs, which violate the head condition, are
1557: semi-generic. Unfortunately, they are not. We explain this for the
1558: first program. The second position of
1559: \verb@gs1@ must be body-generic because of the second clause for
1560: \verb@gs1@. This implies that the second position of
1561: \verb@fs1@ must also be body-generic because of the second clause
1562: for \verb@fs1@
1563: (otherwise there would be two generic positions with a common
1564: parameter). That however is unacceptable for the first clause of
1565: \verb@fs1@ ($\tt X$ has type $\tt t(t(U))$, instance of
1566: $\tt t(U)$).
1567:
1568: It can however be observed that both programs have subject
1569: reduction wrt.\ the queries
1570: %${\tt \{ x:int, y:t(U)\}:\leftarrow\
1571: %fgsi(X,Y)}$ for ${\tt i = 1,2}$.
1572: ${\tt fgs}j(i,{\tt Y})$ for $i \in \nat$ and $j = 1,2$.
1573: In fact for these queries all type
1574: skeletons are proper, but it can be seen that the
1575: equations associated with the type skeletons cannot be ordered.
1576: This shows that the condition of semi-genericity is still too
1577: restrictive.
1578:
1579: There is a perfect analogy between \verb@gs1@ and $\tt r$ in Ex.\
1580: \ref{semi-generic-ex}.
1581:
1582: To conclude this section, note that our solution to the problem in
1583: Ex.\ \ref{fg-ex} uses {\em polymorphic recursion}, a concept
1584: previously discussed for functional programming~\cite{KFU93-short}:
1585: In the recursive clause for {\tt fgs3\_aux}, the arguments of the
1586: recursive call have type
1587: $\tt (int,t(t(U)),t(t(U)))$,
1588: while the arguments of the clause head have type
1589: $\tt (int,t(U),t(U))$.
1590: If we wrote a function corresponding to \verb@fgs3_aux@ in
1591: Miranda~\cite{Tho95} or ML, the type checker
1592: could not infer its type, since it assumes that recursion is
1593: monomorphic, i.e., the type of a recursive call is identical to the
1594: type of the ``head''. In Miranda, this problem can be overcome by
1595: providing a type declaration, while in ML, the function will
1596: definitely be rejected. This limitation of the ML type system, or
1597: alternatively, the ML type checker, has been studied by Kahrs~\cite{K96}.
1598:
1599: There is a certain duality between the head condition and monomorphic
1600: recursion. When trying to find a solution to our problem, we found
1601: that we either had to violate the head condition or use polymorphic
1602: recursion.
1603: For example, in the recursive clause for {\tt gs1},
1604: the arguments of the recursive call have type
1605: $\tt (int,t(U))$,
1606: while the arguments of the clause head have type
1607: $\tt (int,t(t(U)))$, which is in a way the reverse of the situation
1608: for \verb@fgs3_aux@. Note that this implies a violation of the
1609: head condition for {\em any} declared type of {\tt gs1}. It would be
1610: interesting to investigate this duality further.
1611:
1612:
1613: \section{Conclusion}\label{conclusion-sec}
1614:
1615: In this paper we redefined the notion of {\em subject
1616: reduction} by using derivation trees, leading to a
1617: proof-theoretic view of typing in logic programming.
1618: We showed that this new notion is equivalent to the operational
1619: one (Thm.\ \ref{decl-oper-theo}).
1620:
1621: We introduced {\em type skeletons}, obtained from skeletons by
1622: replacing terms with their types. We showed that a program has subject
1623: reduction if for each proper skeleton, the type skeleton
1624: is also proper. Apart from clarifying the motivations of the
1625: head condition, it has several potential applications:
1626:
1627: \begin{itemize}
1628: \item
1629: It facilitates studying the
1630: semantics of typed programs by simplifying its formulation in
1631: comparison to other works (e.g.\ \cite{LR91}). Lifting the notions of
1632: derivation tree and skeleton on the level of types can
1633: help formulate proof-theoretic and operational semantics,
1634: just as this has
1635: been done for untyped logic programming with the classical trees
1636: \cite{BGLM91,DM93,FLMP89}.
1637: \item
1638: The approach may enhance program analysis based on abstract
1639: interpretation.
1640: Proper type skeletons could also be modelled
1641: by fixpoint operators \cite{CominiLMV96,CC77,GDL95}.
1642: Abstract interpretation for prescriptively typed programs has been
1643: studied by~\cite{RBM99,SHK00}, and it has been pointed out that the
1644: head condition is essential for ensuring that the abstract semantics
1645: of a program is finite, which is crucial for the termination of an
1646: analysis. It would be interesting to investigate the impact of more
1647: general conditions.
1648: \item
1649: This ``proof-theoretic'' approach to typing could also be applied for
1650: synthesis of typed programs. In~\cite{TBD97}, the authors propose
1651: the automatic generation of lemmas, using synthesis techniques based
1652: on resolution. It is interesting to observe that the generated lemmas
1653: meet the head condition, which our approach seems to be able to
1654: justify and even generalise.
1655: \item
1656: The approach may help in combining {\em prescriptive} and
1657: {\em descriptive} approaches to typing. The latter are usually based
1658: on partial correctness properties. Descriptive type systems satisfy
1659: certain criteria of type-correctness \cite{DM98}, but subject
1660: reduction is difficult to consider in such systems. Our approach is a
1661: step towards potential combinations of different approaches.
1662: \end{itemize}
1663:
1664: We have presented a condition for type unifiability which is a
1665: refinement of the head condition (Thm.~\ref{condgen-thm}). Several
1666: observations arise from this:
1667: \begin{itemize}
1668: \item
1669: Definition~\ref{semi-generic-def} is decidable. If the partitioning of
1670: the arguments is given, it can be verified in polynomial
1671: time. Otherwise, finding a partitioning is exponential in the number
1672: of argument positions.
1673:
1674: \item
1675: The refinement has a cost: subject reduction does not hold for
1676: arbitrary (typed) queries. The head condition, by its name, only
1677: restricts the clause heads, whereas our generalisation also restricts
1678: the queries, and hence the ways in which a program can be used.
1679:
1680: \item As we have seen, the proposed refinement may not be
1681: sufficient. Several approaches can be used to introduce further
1682: refinements based on abstract interpretation or on properties of sets
1683: of equations. Since any sufficient condition for type unifiability
1684: contains at least an NSTO condition, one could also benefit from
1685: the refinements proposed for the NSTO check \cite{DM93}.
1686: Such further refined conditions should, in particular, be fulfilled by
1687: all solutions of Ex.~\ref{fg-ex}.
1688: \end{itemize}
1689:
1690: We have also studied {\em operational} subject reduction for type
1691: systems with subtyping~\cite{SFD00}. As future work, we want to
1692: integrate that work with the {\em proof-theoretic} view of subject
1693: reduction of this paper. Also, we want to prove the undecidability of
1694: subject reduction and type unifiability, and design more refined tests
1695: for type unifiability.
1696:
1697: \subsection*{Acknowledgements}
1698: We thank Fran\c{c}ois Fages for interesting discussions. Jan-Georg
1699: Smaus was supported by an ERCIM fellowship.
1700:
1701: {\small
1702: \bibliography{thesis,modes_types}
1703: }
1704:
1705: \tableofcontents
1706: \end{document}
1707:
1708: