1: \documentclass[acmtocl]{acmtrans2m}
2:
3: \acmVolume{?}
4: \acmNumber{?}
5: \acmYear{??}
6: \acmMonth{?}
7:
8: \newtheorem{theorem}{Theorem}[section]
9: \newtheorem{corollary}[theorem]{Corollary}
10: \newtheorem{lemma}[theorem]{Lemma}
11: \newdef{definition}[theorem]{Definition}
12: \newdef{remark}[theorem]{Remark}
13: \newdef{example}[theorem]{Example}
14:
15: \usepackage{latexsym}
16: \usepackage{amsfonts}
17:
18: % Deductions
19:
20: \newbox\tempa
21: \newbox\tempb
22: \newdimen\tempc
23: \newbox\tempd
24:
25: \def\mud#1{\hfil $\displaystyle{#1}$\hfil}
26: \def\rig#1{\hfil $\displaystyle{#1}$}
27:
28: \def\inruleanhelp#1#2#3{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}%
29: \setbox\tempd=\hbox{$\; #3$}%
30: \setbox\tempb=\vbox{\halign{##\cr
31: \mud{#1}\cr
32: \noalign{\vskip\the\lineskip}%
33: \noalign{\hrule height 0pt}%
34: \rig{\vbox to 0pt{\vss\hbox to 0pt{\copy\tempd \hss}\vss}}\cr
35: \noalign{\hrule}%
36: \noalign{\vskip\the\lineskip}%
37: \mud{\copy\tempa}\cr}}%
38: \tempc=\wd\tempb
39: \advance\tempc by \wd\tempa
40: \divide\tempc by 2 }
41:
42: \def\inrulean#1#2#3{{\inruleanhelp{#1}{#2}{#3}%
43: \hbox to \wd\tempa{\hss \box\tempb \hss}}}
44: \def\inrulebn#1#2#3#4{\inrulean{#1\quad\qquad #2}{#3}{#4}}
45:
46: \def\ian#1#2#3{{\lineskip 4pt\inrulean{#1}{#2}{#3}}}
47: \def\ibn#1#2#3#4{{\lineskip 4pt\inrulebn{#1}{#2}{#3}{#4}}}
48:
49: \def\lowerhalf#1{\hbox{\raise -0.8\baselineskip\hbox{#1}}}
50:
51: \def\ianc#1#2#3{{\lineskip 4pt\lowerhalf{\inruleanhelp{#1}{#2}{#3}%
52: \box\tempb\hskip\wd\tempd}}}
53: \def\ibnc#1#2#3#4{{\lineskip 4pt\ianc{#1\quad\qquad #2}{#3}{#4}}}
54:
55: \newcommand{\arv}[2]{\begin{array}{c} #1\\#2\end{array}}
56:
57: % Informal logical symbols
58: \newcommand{\Imp}{\supset}
59: \newcommand{\Or}{\vee}
60: \newcommand{\And}{\wedge}
61: \newcommand{\BImp}{\Leftrightarrow}
62:
63: % Example constants
64: \newcommand{\itlam}{{\it lam}}
65: \newcommand{\itapp}{{\it app}}
66: \newcommand{\itexp}{{\it exp}}
67:
68: % Connectives and misc definitions
69: \newcommand{\lamb}[2]{\lambda {#1}\oftp{#2}\ldot}
70: \newcommand{\lxua}{\lam x^u\oftp A\ldot} % ^u added: A.M.
71: \newcommand{\lxka}{\lam x^k\oftp A\ldot}
72: \newcommand{\ldot}{.\;}
73:
74: \newcommand{\bnfas}{\mathrel{::=}}
75: \newcommand{\bnfalt}{\mid}
76: \newcommand{\arrow}{\rightarrow}
77: \newcommand{\lam}{\lambda}
78: \newcommand{\oftp}{\mathord{:}}
79: \newcommand{\hastype}{\mathrel{:}}
80: \newcommand{\rep}[1]{\ulcorner #1\urcorner} % amsfonts.sty
81: \newcommand{\vd}{\vdash}
82: \newcommand{\nvd}{\null\mathrel{\not\vdash}}
83:
84: \newcommand{\one}{\mathbf{1}}
85: \newcommand{\zero}{\mathbf{0}}
86:
87: % Letters
88: \newcommand{\GG}{\Gamma}
89: \newcommand{\DD}{\Delta}
90: \newcommand{\OO}{\Omega}
91: \newcommand{\god}{\Gamma; \Omega; \Delta}
92: \newcommand{\godc}{(\GG,\OO,\DD)}
93:
94: \newcommand{\cD}{{\cal D}}
95: \newcommand{\cE}{{\cal E}}
96: \newcommand{\cM}{{\cal M}}
97: \newcommand{\cN}{{\cal N}}
98: \newcommand{\cP}{{\cal P}}
99:
100: % Arrows
101: \newcommand{\da}{\downarrow}
102: \newcommand{\bua}{\Uparrow}
103: \newcommand{\buda}{\Uparrow\!\downarrow}
104: \newcommand{\blip}{\Rightarrow}
105:
106: \newcommand{\whr}{\stackrel{\mbox{\tiny whr}}{\longrightarrow}}
107: \newcommand{\betared}{\stackrel{\beta}{\longrightarrow}}
108:
109: \newcommand{\etaexp}{\stackrel{\bar\eta}{\longrightarrow}}
110:
111:
112: \newcommand{\GImp}[1]{\stackrel{\mbox{\tiny ${#1}$}}{\arrow}}
113: \newcommand{\TImp}{\GImp{u}}
114: \newcommand{\RImp}{\GImp{1}}
115: \newcommand{\ZImp}{\GImp{0}}
116:
117: \newcommand{\lop}{\mathbin{-\!\circ}}
118:
119: % Names
120: \newcommand{\dom}{\mbox{\textrm{dom}}}
121: \newcommand{\mnot}{{\rm Not}}
122: \newcommand{\Pat}{\mathrm{Pat}_A(\Psi)}
123:
124: % Delimiters
125: \newcommand{\lsemantics}{\mathopen{\lbrack\mkern-3mu\lbrack}}
126: \newcommand{\rsemantics}{\mathclose{\rbrack\mkern-3mu\rbrack}}
127: \newcommand{\den}[1]{\lsemantics#1\rsemantics}
128:
129: % Markups
130: \newcommand{\ednote}[1]{\message{ednote!}\footnote{\it #1}}
131: \newcommand{\elide}[2]{\message{elide!}\footnote{\it elide: #1}}
132:
133: \markboth{A. Momigliano and F. Pfenning}{Higher-Order Pattern Complement}
134:
135: \title{Higher-Order Pattern Complement and the Strict $\lambda$-Calculus}
136:
137: \author{ALBERTO MOMIGLIANO\\University of Leicester\and
138: FRANK PFENNING\\Carnegie Mellon University}
139:
140: \begin{abstract}
141: We address the problem of complementing higher-order patterns without
142: repetitions of existential variables. Differently from the first-order case,
143: the complement of a pattern cannot, in general, be described by a
144: pattern, or even by a finite set of patterns. We therefore generalize
145: the simply-typed $\lambda$-calculus to include an internal notion of
146: \emph{strict function} so that we can directly express that a term must
147: depend on a given variable. We show that, in this more expressive
148: calculus, finite sets of patterns without repeated variables are closed
149: under complement and intersection. Our principal application is the
150: transformational approach to negation in higher-order logic programs.
151: \end{abstract}
152:
153: \category{D.3.3}{Programming Languages}{Language Constructs and Features}
154: \category{D.1.6}{Programming Techniques}{Logic Programming}
155: \category{F.4.1}{Mathematical Logic and Formal Language}{Mathematical Logic}[Lambda calculus and related systems]
156: \terms{Languages, Theory}
157: \keywords{Complement, higher-order patterns, strict $\lambda$-calculus}
158:
159: \begin{document}
160: \begin{bottomstuff}
161: Author's addresses: \newline
162: A.~Momigliano, Department of Mathematics and Computer Science,
163: University of Leicester, Leicester, LE1 HR2, U.K.,
164: \texttt{am133@mcs.le.ac.uk}\newline
165: F.~Pfenning, Department of Computer Science,
166: Carnegie Mellon University, Pittsburgh, PA 15213, U.S.A.,
167: \texttt{fp@cs.cmu.edu} \newline
168: This work has been support by the National Science Foundation
169: under grant CCR-9988281.
170: \end{bottomstuff}
171:
172: \maketitle
173:
174: % \input{intro} % intro and pleminaries
175:
176: \section{Introduction}
177: \label{sec:intro}
178:
179: In most functional and logic programming languages the notion of a
180: pattern, together with the requisite algorithms for matching or
181: unification, play an important role in the operational semantics.
182: Besides unification, other problems such as generalization or complement
183: also arise frequently. In this paper we are concerned with the problem
184: of pattern complement in a setting where patterns may contain binding
185: operators, so-called \emph{higher-order
186: patterns}~\cite{Miller91jlc,Nipkow91lics}. Higher-order patterns have
187: found applications in logic programming~\cite{Miller91jlc,Pfenning91lf},
188: logical frameworks~\cite{Despeyroux97}, term
189: rewriting~\cite{Nipkow93tlca}, and functional logic
190: programming~\cite{Hanus96RTA}. Higher-order patterns inherit many
191: pleasant properties from the first-order case. In particular, most
192: general unifiers~\cite{Miller91jlc} and least general
193: generalizations~\cite{Pfenning91lics} exist, even for complex type
194: theories.
195:
196: Unfortunately, the complement operation does not generalize as smoothly.
197: Lugiez \citeyear{Lug95} has studied the more general problem of
198: higher-order disunification and had to go outside the language of
199: patterns and terms to describe complex constraints on sets of solutions.
200: We can isolate one basic difficulty: a pattern such as $\lambda x\ldot
201: E\ x$ for an existential variable $E$ matches any term of appropriate
202: type, while $\lambda x\ldot E$ matches precisely those terms $\lambda
203: x\ldot M$ where $M$ does not depend on $x$. The complement then
204: consists of all terms $\lambda x\ldot M$ such that $M$ \emph{does}
205: depend on $x$. However, this set cannot be described by a pattern, or
206: even a finite set of patterns.
207:
208: This formulation of the problem suggests that we should consider a
209: $\lambda$-calculus with an internal notion of \emph{strictness} so
210: that we can directly express that a term must depend on a given
211: variable. For reasons of symmetry and elegance we also add the dual
212: concept of \emph{invariance} expressing that a given term does
213: \emph{not} depend on a given variable. As in the first-order case, it
214: is useful to single out the case of \emph{linear patterns}, namely
215: those where no existential variable occurs more than
216: once.\footnote{This notion of linearity should not be confused with
217: the eponymous concept in linear logic and $\lambda$-calculus.} We
218: further limit attention to \emph{simple} patterns, that is, those where
219: constructors must be strict in their arguments---a condition naturally
220: satisfied in our intended application domains of functional and logic
221: programming. Simple linear patterns in our $\lambda$-calculus of
222: strict and invariant function spaces then have the following
223: properties:
224: \begin{enumerate}
225: \item The complement of a pattern is a finite set of patterns.
226: \item Unification of two patterns is decidable and finitary.
227: \end{enumerate}
228: Consequently, finite sets of simple linear patterns in the strict
229: $\lambda$-calculus are closed under complement and unification. If we
230: think of finite sets of linear patterns as representing the set of all
231: their ground instances, then they form a boolean algebra under
232: set-theoretic union union, intersection (implemented via unification)
233: and the complement operation.
234:
235: The paper is organized as follows: Section~\ref{sec:facomp} briefly
236: reviews related work and introduces some preliminary definitions. In
237: Section~\ref{sec:strict} we introduce a strict $\lam$-calculus and
238: prove some basic properties culminating in the proof of the existence
239: of canonical forms in Section~\ref{sec:canonthm}.
240: Section~\ref{sec:strictcomp} introduces simple terms, followed by the
241: algorithm for complementation in Section~\ref{sec:compl}. In
242: Section~\ref{sec:sunif} we give a corresponding unification algorithm.
243: Section~\ref{sec:algebra} observes how the set of those patterns can
244: be arranged in a boolean algebra. We conclude in
245: Section~\ref{sec:concl} with some applications and speculations on
246: future research.
247:
248: \section{Preliminaries and Related Work}
249: \label{sec:facomp}
250:
251: A pattern $t$ with free variables can be seen as a representation of the
252: set of its ground instances, denoted by $\| t \|$. According to this
253: interpretation, the \emph{complement} of $t$ is the set of ground terms
254: that are \emph{not} instances of $t$, i.e., the terms are in the set-theoretic
255: complement of $\| t \|$. It is natural to generalize this to
256: finite sets of terms, where $\|t_1,\ldots,t_n\| = \|t_1\| \cup
257: \cdots \cup \|t_n\|$. If we take this one step further we obtain the
258: important problem of \emph{relative complement}; this corresponds to
259: computing a suitable representation of all the ground instances of a
260: given (finite) set of terms which are not instances of another given
261: one, written as \( \| t_1, \ldots, t_n \| - \| u_1, \ldots, u_m \|. \)
262:
263: Complement problems have a number of applications in theoretical
264: computer science (see \citeN{Comon91} for a list of references). For
265: example, they are used in functional programming to produce unambiguous
266: function definitions by patterns and to improve their compilation. In
267: rewriting systems they are used to check whether an algebraic
268: specification is sufficiently complete. They can also be employed to
269: analyze communicating processes expressed by infinite transition
270: systems. Other applications lie in the areas of machine learning and
271: inductive theorem proving. In logic programming, Kunen
272: \citeyear{Kunen87} used term complement to represent infinite sets of
273: answers to negative queries. Our main motivation has been the explicit
274: synthesis of the negation of higher-order logic programs~[Momigliano
275: \citeyearNP{Momigliano00phd}; \citeyearNP{Momigliano00csl}], as discussed
276: briefly in Section~\ref{sec:concl}.
277:
278: \citeN{Lassez87} proposed the seminal \emph{uncover}
279: algorithm for computing \emph{first-order} relative complements and
280: introduced the now familiar restriction to linear terms. We quote the
281: definition of the ``$\mnot$'' algorithm for the (singleton)
282: complement problem given in \cite{Bar90} which we generalize in
283: Definition~\ref{def:compl}. Given a finite signature $\Sigma$ and a
284: linear term $t$ they define:
285: \[ \begin{array}{lcl}
286: \mnot_\Sigma(x) & = & \emptyset \\
287: \mnot_\Sigma(f(t_1,\ldots,t_n)) & = &
288: \{g(x_1,\ldots,x_m) \mid \mbox{$g \in \Sigma$ and $g \not= f$} \} \\
289: & \cup & \{f(z_1, \ldots, z_{i-1},s,z_{i+1}, \ldots,z_n) \mid
290: s\in\mnot_\Sigma(t_{i}), 1\leq i \leq n \}
291: \end{array} \]
292: The relative complement problem is then solved by composing the above
293: complement operation with term intersection implemented via first-order
294: unification.
295:
296: An alternative solution to the relative complement problem is
297: \emph{disunification} (see \cite{Comon91} for a survey and \cite{Lug95}
298: for an extension to the simply-typed $\lam$-calculus). Here, operations on
299: sets of terms are translated into conjunctions or disjunctions of
300: equations and dis-equations under explicit quantification.
301: Non-deterministic application of a few dozen rules eventually turns a
302: given problem into a solved form. Though a reduction to a significant
303: subset of the disunification rules is likely to be attainable for
304: complement problems, control is a major problem. We argue that using
305: disunification for this purpose is unnecessarily general. Moreover, the
306: higher-order case results in additional complications, such as restrictions on
307: the occurrences of bound variables, which fall outside an otherwise
308: clean framework. As we show in this paper, this must not necessarily be
309: the case. We believe that our techniques can also be applied to analyze
310: disunification, although we have not investigated this possibility at
311: present.
312:
313: We now introduce some preliminary definitions and examples which guide
314: our development. We begin with the simply-typed $\lambda$-calculus. We
315: write $a$ for atomic types, $c$ for term-level constants, and $x$ for
316: term-level variables. Note that variables $x$ should be seen as
317: parameters and not subject to instantiation.
318:
319: \[ \begin{array}{rrcl}
320: \mbox{\textit{Simple Types}} & A & \bnfas & a \bnfalt A_1 \arrow A_2 \\
321: \mbox{\textit{Terms}} & M & \bnfas & c \bnfalt x \bnfalt \lam
322: x\oftp A\ldot M \bnfalt M_1\ M_2 \\
323: \mbox{\textit{Signatures}} & \Sigma & \bnfas & \cdot \bnfalt
324: \Sigma, a \oftp \mbox{type} \bnfalt \Sigma, c\oftp A \\
325: \mbox{\textit{Contexts}} & \GG & \bnfas & \cdot \bnfalt \GG, x\oftp A
326: \end{array} \]
327:
328: We require that signatures and contexts declare each constant or variable at
329: most once. Furthermore, we identify contexts that differ only in their
330: order and promote `,' to denote disjoint set union. As usual we identify
331: terms which differ only in the names of their bound variables. We restrict
332: attention to well-typed terms, omitting the standard typing rules.
333: We write the main typing judgment as $\Gamma \vd M \hastype A$, assuming
334: a fixed signature $\Sigma$.
335:
336: In applications such as logic programming or logical frameworks,
337: $\lambda$-abstraction is used to represent binding operators in some
338: object language. In such a situation the most appropriate notion of
339: normal form is the long $\beta\eta$-normal form (which we call
340: \emph{canonical form}), since canonical forms are almost always the
341: terms in bijective correspondence with the objects we are trying to
342: represent. Every well-typed term in the simply-typed $\lambda$-calculus
343: has a unique canonical form---a property which persists in the strict
344: $\lambda$-calculus introduced in Section~\ref{sec:strict}.
345:
346: We denote existential variables of type $A$ (also called logical variables,
347: meta-variables, or pattern variables) by $E_A$, although we mostly omit the
348: type $A$ when it is clear from the context. We think of existential variables
349: as syntactically distinct from bound variables or free variables declared in a
350: context. A term possibly containing some existential variables is called a
351: \emph{pattern} if each occurrence of an existential variable appears in a
352: subterm of the form $E\ x_1\ldots x_n$, where the arguments $x_i$ are distinct
353: occurrences of free or bound variables (but not existential variables). We
354: call a term \emph{ground} if it contains no existential variables. Note that
355: it may still contain parameters.
356:
357: Semantically, an existential variable $E_A$ stands for all canonical
358: terms $M$ of type $A$ in the empty context with respect to a given
359: signature. We extend this to arbitrary well-typed patterns in the usual
360: way, and write $\GG \vd M\in\| N\| \hastype A$ when a term $M$ is a instance
361: of a pattern $N$ at type $A$ containing only the parameters in $\GG$
362: and no existential variables. In this setting, unification of two
363: patterns without shared existential variables corresponds to an
364: intersection of the set of terms they
365: denote~\cite{Miller91jlc,Pfenning91lics}. This set is always either
366: empty, or can be expressed again as the set of instances of a single
367: pattern. That is, patterns admit most general unifiers.
368:
369: The class of higher-order patterns inherits many properties from
370: first-order terms. However, as we will see, it is \emph{not} closed
371: under complement, but a special subclass is. We call a canonical
372: pattern $\GG \vd M \hastype A$ \emph{fully applied} if each
373: occurrence of an existential variable $E$ under binders $y_1,\ldots,y_m$
374: is applied to some permutation of the variables in $\GG$ and
375: $y_1,\ldots,y_m$. Fully applied patterns play an important role in
376: functional logic programming and rewriting~\cite{Hanus96RTA}, because any
377: fully applied existential variable $\GG \vd E\ x_1\ldots x_n \hastype
378: a$ denotes all canonical terms of type $a$ with parameters from
379: $\GG$. It is this property which makes complementation particularly
380: simple.
381:
382: \begin{example}
383: \label{ex:lam}
384: Consider the untyped $\lam$-calculus:\footnote{We
385: use $\Lambda$ and $@$ to avoid confusion with $\lam$ and application in
386: the language of patterns.}
387: \begin{eqnarray*}
388: e & \bnfas & x \mid \Lambda x\ldot e \mid e_1\ @\ e_2
389: \end{eqnarray*}
390: We encode these expressions using the usual technique of higher-order abstract
391: syntax as canonical forms over the following signature.
392: \begin{eqnarray*}
393: \Sigma & = & \itexp\hastype \mbox{\textrm{type}}, \itlam\hastype (\itexp\arrow
394: \itexp)\arrow \itexp, \itapp \hastype \itexp \arrow \itexp\arrow \itexp
395: \end{eqnarray*}
396: The representation function $\rep{\_}$ is defined as follows:
397: \begin{eqnarray*}
398: \rep{x} & = & x\hastype \itexp\\
399: \rep{\Lambda x\ldot e} & = & \itlam\ (\lamb{x}{\itexp} \rep{e})\\
400: \rep{e_1\ @ \ e_2} & = & \itapp\ \rep{e_1}\ \rep{e_2}
401: \end{eqnarray*}
402: The representation of an object-language $\beta$-redex then has the
403: form
404: \begin{eqnarray*}
405: \rep{(\Lambda x\ldot e)\ @\ f} & = & \itapp\ (\itlam\ (\lamb{x}{\itexp} \rep{e}))\ \rep{f},
406: \end{eqnarray*}
407: where $\rep{e}$ may have free occurrences of $x$. When written as a
408: pattern with existential variables $E_{\itexp \arrow \itexp}$ and $F_{\itexp}$
409: this is expressed as
410: \[ \itapp\ (\itlam\ (\lamb{x}{\itexp} E\ x)\ F). \]
411: Note that in the empty context this pattern is fully applied. Its
412: complement with respect to the empty context contains every top-level
413: abstraction plus every application where the first argument is not an
414: abstraction.
415: \[ \mnot(\itapp\ (\itlam\ (\lamb{x}{\itexp} E\ x)\ F)) =
416: \{\itlam\ (\lamb{x}{\itexp} H\ x), \itapp\ (\itapp\ H_{1}\ H_{2})\ H_{3}\}
417: \]
418: Here $H$, $H_1$, $H_2$, $H_3$ are fresh existential variables of appropriate
419: type, namely $H \hastype \itexp \arrow \itexp$ and $H_i \hastype \itexp$.
420: \end{example}
421:
422: For patterns that are not fully applied, the complement cannot
423: be expressed as a finite set of patterns, as the following example
424: illustrates.
425:
426: \begin{example}
427: \label{ex:etardx}
428: The encoding of an $\eta$-redex takes the form:
429: \begin{eqnarray*}
430: \rep{\Lambda x.\, (e\ @\ x)} & = & \itlam\ (\lamb{x}{\itexp} \itapp\ \rep{e}\ x)
431: \end{eqnarray*}
432: where $\rep{e}$ may contain no free occurrence of $x$. The side
433: condition is expressed in a pattern by introducing an existential
434: variable $E_{\itexp}$ which {\em does not\/} depend on $x$, that is
435: \[ \itlam\ (\lamb{x}{\itexp} \itapp\ E\ x). \]
436: Hence, its complement with respect to the empty context should
437: contain, among others, also all terms
438: \[ \itlam\ (\lamb{x}{\itexp} \itapp\ (F\ x)\ (H\ x)) \] where
439: $F\hastype \itexp \arrow \itexp$ {\em must\/} depend on its argument $x$
440: while $H\hastype \itexp \arrow \itexp$ may or may not depend on $x$.
441: \end{example}
442:
443: As the example above shows, the complement of patterns that are not fully
444: applied cannot be represented as a finite set of patterns. Indeed, there is
445: no finite set of patterns which has as its ground instances exactly those
446: terms $M$ which depend on a given variable $x$. This failure of closure under
447: complementation cannot be avoided similarly to the way in which
448: left-linearization bypasses the limitation to linear patterns and it needs to
449: be addressed directly.
450:
451: One approach is taken by \citeN{Lug95}: he modifies the language of
452: terms to permit occurrence constraints. For example $\lam xyz.\ M\{1,3\}$
453: would denote a function which depends on its first and third argument. The
454: technical handling of those objects then becomes awkward as they require
455: specialized rules which are foreign to the issues of complementation.
456:
457: Since our underlying $\lambda$-calculus is typed, we use typing to
458: express that a function \emph{must} depend on a variable $x$. Following
459: standard terminology, we call such terms \emph{strict in $x$} and the
460: corresponding function $\lamb{x}{A} M$ a \emph{strict function}. In the
461: next section we develop such a $\lambda$-calculus and then generalize the
462: complement algorithm to work on such terms.
463:
464: % \input{calculus} % the calculus
465:
466:
467: \section{Strict Types}
468: \label{sec:strict}
469:
470: As we have seen in the preceding section, the complement of a partially
471: applied pattern in the simply-typed $\lambda$-calculus cannot be
472: expressed in a finitary manner within the same calculus. We thus
473: generalize our language to include \emph{strict} functions of type $A
474: \RImp B$ (which are guaranteed to depend on their argument) and
475: \emph{invariant} functions of type $A \ZImp B$ (which are guaranteed
476: \emph{not} to depend on their argument). Of course, any concretely
477: given function either will or will not depend on its argument, but in
478: the presence of higher-order functions and existential variables we
479: still need the ability to remain uncommitted. Therefore our calculus
480: also contains the full function space $A \TImp B$. We first concentrate
481: on a version without existential variables. A similar calculus has been
482: independently investigated by \citeN{Wright92} and \citeN{Baker94}; for
483: a comparison see the end of Section~\ref{sec:canonthm}.
484:
485:
486: \[ \begin{array}{rrcl}
487: \mbox{\textit{Labels}} & k & \bnfas & 1 \bnfalt 0 \bnfalt u \\
488: \mbox{\textit{Types}} & A & \bnfas & a \bnfalt A_1 \GImp{k} A_2 \\
489: \mbox{\textit{Terms}} & M & \bnfas & c \bnfalt x \bnfalt \lam
490: x^k\oftp A\ldot M \bnfalt M_1\ M_2^k
491: \end{array} \]
492:
493: Note that there are three different forms of abstractions and
494: applications, where the latter are distinguished by different labels on
495: the argument. It is not really necessary to distinguish three forms of
496: application syntactically, since the type of a function determines the
497: status of its argument, but it is convenient for our purposes. A label
498: $u$ is called \emph{undetermined}, otherwise it is \emph{determined} and
499: denoted by $d$.
500:
501: We use a formulation of the typing judgment
502: \[ \GG; \OO; \DD \vd M \hastype A \]
503: with three zones: $\GG$ containing \emph{unrestricted} hypotheses,
504: $\OO$ containing the \emph{irrelevant} hypotheses, and $\DD$ containing
505: the \emph{strict} hypotheses. We implicitly assume a fixed signature
506: $\Sigma$ which would otherwise clutter the presentation. Recall that
507: $\GG_1,\GG_2$ is the union of two contexts that do not declare any
508: common variables. Recall also that we consider contexts as sets, that
509: is, exchange is left implicit. The typing rules are given in
510: Figure~\ref{fig:typrules}.
511:
512: \begin{figure}
513:
514: \[ \begin{array}{c}
515: \ianc{c\oftp A \in \Sigma}{\GG; \OO; \cdot \vd c \hastype
516: A}{\mathtt{Con}} \\[1em]
517:
518: \ianc{}{(\GG, x\oftp A); \OO; \cdot \vd x \hastype A}{\mathtt{Id}^u}
519: \hspace{2em} \mbox{\textit{no $\mathtt{Id}^0$ rule}} \hspace{2em}
520: \ianc{}{\GG; \OO; x\oftp A \vd x \hastype A}{\mathtt{Id}^1} \\[1em]
521:
522: \ianc{(\GG, x\oftp A); \OO; \DD \vd M \hastype B}{\GG;
523: \OO; \DD \vd \lam x^u \oftp A\ldot M \hastype A \GImp{u}
524: B}{\GImp{u}I} \\[1em]
525:
526: \ianc{\GG; (\OO, x\oftp A); \DD \vd M \hastype B}{\GG;
527: \OO; \DD \vd \lam x^0 \oftp A\ldot M \hastype A \GImp{0}
528: B}{\GImp{0}I} \\[1em]
529:
530: \ianc{\GG; \OO; (\DD, x\oftp A)\vd M \hastype B}{\GG;
531: \OO; \DD \vd \lam x^1 \oftp A\ldot M \hastype A \GImp{1}
532: B}{\GImp{1}I} \\[1em]
533:
534: \ibnc{\GG; \OO; \DD \vd M \hastype A \TImp B}{(\GG,
535: \DD); \OO; \cdot \vd N \hastype A}{\GG; \OO; \DD \vd M\
536: N^u \hastype B}{\GImp{u}E} \\[1em]
537:
538: \ibnc{\GG; \OO; \DD \vd M \hastype A \ZImp B}{(\GG,
539: \OO,\DD); \cdot; \cdot \vd N \hastype A}{\GG; \OO; \DD
540: \vd M\ N^0 \hastype B}{\GImp{0}E} \\[1em]
541:
542: \ibnc{(\GG, \DD_N); \OO; \DD_M \vd M \hastype A \RImp
543: B}{(\GG, \DD_M); \OO; \DD_N \vd N \hastype A}{\GG;
544: \OO; (\DD_M, \DD_N) \vd M\ N^1 \hastype B}{\GImp{1}E}
545:
546: \end{array} \]
547: \caption{Typing rules for $\god\vd M\hastype A$}
548: \label{fig:typrules}
549: \end{figure}
550:
551: Our system is biased towards a bottom-up reading of the rules in that
552: variables never disappear, i.e., they are always propagated from the
553: conclusion to the premises, although their status might be changed.
554:
555: Let us go through the typing rules in detail. The requirement for the
556: strict context $\DD$ to be empty in the $\mathtt{Id}^u$ and
557: $\mathtt{Id}^1$ rules expresses that strict variables must be used,
558: while undetermined variables in $\GG$ or irrelevant variables in
559: $\OO$ can be ignored. Note that there is no rule for irrelevant
560: variables, which expresses that they cannot be used. The introduction
561: rules for undetermined, invariant, and strict functions simply add a
562: variable to the appropriate context and check the body of the function.
563: The difficult rules are the three elimination rules. First, the
564: unrestricted context $\GG$ is always propagated to both premises.
565: This reflects that we place no restriction on the use of these
566: variables.
567:
568: Next we consider the strict context $\DD$: recall that this contains
569: the variables which should occur strictly in a term. An undetermined
570: function $M\hastype A \GImp{u} B$ may or may not use its argument. An
571: occurrence of a variable in the argument to such a function can
572: therefore not be guaranteed to be used. Hence we must require in the
573: rule $\GImp{u}E$ for an application $M\ N^u$ that all variables in
574: $\DD$ occur strictly in $M$. This ensures at least one strict
575: occurrence in $M$ and no further restrictions on occurrences of strict
576: variables in the argument are necessary. This is reflected in the rule
577: by adding $\DD$ to the unrestricted context while checking the
578: argument $N$. The treatment of the strict variables in the vacuous
579: application $M\ N^0$ is similar.
580:
581: In the case of a strict application $M\ N^1$ each strict variable
582: should occur strictly in either $M$ or $N$. We therefore split the
583: context into $\DD_M$ and $\DD_N$ guaranteeing that each variable
584: has at least one strict occurrence in $M$ or $N$, respectively.
585: However, strict variables can occur more than once, so variables from
586: $\DD_N$ can be used freely in $M$, and variables from $\DD_M$
587: can occur freely in $N$. As before, we reflect this by adding these
588: variables to the unrestricted context.
589:
590: Finally we consider the irrelevant context $\OO$. Variables
591: declared in $\OO$ cannot be used \emph{except} in the argument to
592: an invariant function (which is guaranteed to ignore its argument).
593: We therefore add the irrelevant context $\OO$ to the unrestricted
594: context when checking the argument of a vacuous application $M\ N^0$.
595:
596: We now illustrate how the strict application rule
597: non-deterministically splits contexts. Consider the typing problem
598: $\cdot;\cdot; (x \oftp A \RImp A\RImp B ,y\oftp A)\vd (x\ y^1) \
599: y^1\hastype B$, related to the contraction principle. There are four
600: ways to split the strict context for the outer application.
601:
602: \[\begin{array}{ll}
603: \DD_{M} = x \oftp A \RImp A\RImp B ,y\oftp A & \DD_{N}=\cdot\\ \DD_{M} =
604: x \oftp A \RImp A\RImp B & \DD_{N} = y\oftp A\\ \DD_{M} = y\oftp A &
605: \DD_{N}= x \oftp A \RImp A\RImp B\\ \DD_{M} =\cdot & \DD_{N}=x \oftp A
606: \RImp A\RImp B ,y\oftp A
607: \end{array}\]
608: Only the first two yield a valid derivation as depicted in
609: Figures~\ref{fig:strictex} and~\ref{fig:strictex2}. Here we
610: have dropped the types in the context.
611:
612: \begin{figure}
613: \newcommand{\aaa}{y; \cdot; x \vd x \hastype A\RImp A\RImp B}
614: \newcommand{\bbb}{x;\cdot ; y \vd y\hastype A }
615: \newcommand{\ccc}{\cdot;\cdot ;( x , y )\vd x\ y^1 \hastype A\RImp B}
616: \newcommand{\ddd}{(x, y ); \cdot ;\cdot\vd y\hastype A}
617: \newcommand{\eee}{\cdot;\cdot; (x \oftp A \RImp A\RImp B, y\oftp
618: A)\vd (x\ y^1) \ y^1 \hastype B}
619: \[ \ianc{\ian{\ian{}{\aaa}{\mathtt{Id}^1} \hspace{2em}
620: \ian{}{\bbb}{\mathtt{Id}^1}}
621: {\ccc}{{\RImp}E} \hspace{7em}
622: \ian{}{\ddd}{\mathtt{Id}^u}}
623: {\eee}{{\RImp}E}
624: \]
625: \caption{First derivation of $\cdot;\cdot; (x \oftp A \RImp A\RImp B
626: ,y\oftp A) \vd (x\ y^1)\ y^1\hastype B$}
627: \label{fig:strictex}
628: \end{figure}
629:
630: \begin{figure}
631: \newcommand{\aaa}{y ; \cdot; x \vd x \hastype A \RImp A\RImp B}
632: \newcommand{\bbb}{(x , y );\cdot;\cdot\vd y\hastype A }
633: \newcommand{\ccc}{y ;\cdot ; x \vd x\ y^1 \hastype A\RImp B}
634: \newcommand{\ddd}{ x ;\cdot; y \vd y\hastype A}
635: \newcommand{\eee}{
636: \cdot;\cdot; (x \oftp A \RImp A\RImp B ,y\oftp A)\vd (x\ y^1) \ y^1
637: \hastype B}
638: \[ \ianc{\ian{\ian{}{\aaa}{\mathtt{Id}^1} \hspace{2em}
639: \ian{}{\bbb}{\mathtt{Id}^u}}
640: {\ccc}{{\RImp}E} \hspace{9em}
641: \ian{}{\ddd}{\mathtt{Id}^1}}
642: {\eee}{{\RImp}E}
643: \]
644: \caption{Second derivation of $\cdot;\cdot; (x \oftp A \RImp A\RImp
645: B ,y\oftp A)\vd (x \ y^1)\ y^1\hastype B$}
646: \label{fig:strictex2}
647: \end{figure}
648:
649: Our strict $\lambda$-calculus satisfies the expected properties,
650: culminating in the existence of canonical forms which is critical for
651: the intended applications. First we remark that types are unique,
652: although typing derivations may not.
653:
654: \begin{theorem}[Uniqueness of Typing] \mbox{}
655: \label{thm:uniqueT}
656: Assume $(\GG,\OO,\DD) = (\GG',\OO',\DD')$. \newline
657: If $\GG;\OO;\DD \vd M\hastype A$ and $\GG';\OO';\DD'\vd M\hastype A'$,
658: then $A = A'$.
659: \end{theorem}
660: \begin{proof}
661: By induction on the structure of the given derivation, exploiting
662: uniqueness for declarations of variables and constants.
663: \end{proof}
664:
665: We start addressing the structural properties of the contexts. Exchange
666: is directly built into the formulation and will not be repeated. Note
667: that our calculus is formulated entirely without structural rules, which
668: now have to be shown to be admissible.
669:
670: \begin{lemma}[Weakening] \mbox{}
671: \label{thm:weak}
672: \begin{enumerate}
673: \item (Weakening$^{u}$) If $\GG; \OO; \DD\vd M \hastype A$,
674: then $(\GG, x\oftp C); \OO; \DD\vd M \hastype A$.
675: \item (Weakening$^{0}$) If $\GG; \OO; \DD\vd M \hastype A$,
676: then $\GG ; (\OO, x\oftp C); \DD\vd M \hastype A$.
677: \end{enumerate}
678: \end{lemma}
679:
680: \begin{proof}
681: By induction on the structure of the given derivations.
682: \end{proof}
683:
684:
685: The following properties allow us to lose track of strict and vacuous
686: occurrences, if we are so inclined.
687:
688:
689: \begin{lemma}[Loosening]
690: \label{thm:loosex}
691: \mbox{}
692: \begin{enumerate}
693: \item (Loosening$^{0}$)
694: If $\GG; (\OO, x\oftp C); \DD \vd M \hastype A$, then $(\GG,x\oftp
695: C);\OO;\DD \vd M \hastype A$.
696: \item (Loosening$^{1}$)
697: If $\GG; \OO; (\DD,x\oftp C)\vd M \hastype A$, then $(\GG, x\oftp C);
698: \OO; \DD \vd M \hastype A$.
699: \end{enumerate}
700: \end{lemma}
701: \begin{proof}
702: By induction on the structure of the given derivations.
703: \end{proof}
704:
705: Next we come to the critical substitution properties. They verify the
706: intended meaning of the hypothetical judgments and directly entail
707: subject reduction (Theorem~\ref{thm:subred}). To be consistent with the
708: design of our typing rules, we formulate the substitution properties so
709: that each of the given derivation depends on the same variables,
710: although their status might be different (unrestricted, irrelevant, or
711: strict). Note that this is possible only because we have included
712: irrelevant hypotheses in our judgment.
713:
714: \begin{lemma}[Substitution] \mbox{}
715: \label{thm:substitution}
716: \begin{enumerate}
717: \item \label{part:subu}
718: (Substitution$^u$) If $(\GG, x\oftp A);\OO;\DD\vd M
719: \hastype C$ and $(\GG,\DD); \OO;\cdot \vd N \hastype A$, then
720: $\GG;\OO;\DD \vd [N/x]M \hastype C$.
721: \item (Substitution$^0$) If $\GG;(\OO,x\oftp A);\DD \vd M
722: \hastype C$ and $(\GG, \DD,\OO) ;\cdot;\cdot \vd N \hastype
723: A$, then $\GG;\OO;\DD \vd [N/x]M \hastype C$.
724: \item \label{part:sub1}
725: (Substitution$^1$) If $(\GG,\DD_N);\OO; (\DD_M,
726: x\oftp A )\vd M \hastype C$ and $(\GG,\DD_M);\OO;\DD_N
727: \vd N\hastype A$, then
728: $\GG; \OO;( \DD_M, \DD_N) \vd [N/x]M \hastype C$.
729: \end{enumerate}
730: \end{lemma}
731:
732: \begin{proof}
733: We proceed by mutual induction on the structure of the derivation $\cD$ of
734: $M\hastype C$, using weakening and loosening as needed to match the form of
735: the induction hypothesis. Each case is otherwise entirely straightforward.
736: We show only one case in the proof of strict substitution
737: (part~\ref{part:sub1}). Here and in subsequent proofs we sometimes write $\cD
738: :: J$ if $\cD$ is a derivation of judgment $J$ instead of the two-dimensional
739: notation $\arv{\cD}{J}$.
740:
741: \begin{description}
742: \item[Case] $\cD$ ends in ${\RImp}E$. There are two sub-cases, depending
743: on whether the declaration $x\oftp A$ is strict in the left premise or
744: right premise. We show the former.
745: \[ \ianc{\arv {\cD_1}{(\GG,\DD_{N},\DD_{Q}); \OO;
746: (\DD_{P}, x\oftp A) \vd P \hastype B \RImp C} \hspace{1em} \arv{\cD_2}{
747: (\GG,\DD_{N},\DD_{P}, x\oftp A);\OO;\DD_{Q} \vd Q \hastype B} }
748: {(\GG,\DD_N); \OO; (\DD_{P}, x\oftp A,\DD_{Q})\vd P\ Q^1 \hastype
749: C}{\GImp{1}E} \]
750:
751: \begin{tabbing}
752: $\cD_1::(\GG,\DD_{N},\DD_{Q}); \OO; (\DD_{P}, x\oftp A) \vd P
753: \hastype B \RImp C$ \` Subderivation\\
754: $\cE::(\GG,\DD_P, \DD_{Q});\OO;\DD_{N}\vd N\hastype A$ \` Assumption \\
755: $(\GG,\DD_{Q}); \OO; (\DD_{P}, \DD_N) \vd [N/x] P \hastype B \RImp
756: C$ \` By i.h. (\ref{part:sub1}) on $\cD_{1}, \cE$\\
757: $(\GG,\DD_{Q},\DD_N); \OO; \DD_{P} \vd [N/x] P \hastype B
758: \RImp C$ \` By Loosening$^1$ $\DD_N$\\
759: $\cD_2::(\GG,\DD_{N}, \DD_{P}, x\oftp A);\OO;\DD_{Q} \vd Q \hastype B$ \`
760: Subderivation\\
761: $\cE'::(\GG,\DD_P,\DD_Q,\DD_N);\OO;\cdot\vd N\hastype A$ \`By
762: Loosening$^{1}$ $\DD_N$ in $\cE$\\
763: $(\GG,\DD_{N},\DD_{P}); \OO; \DD_{Q} \vd [N/x] Q \hastype B$ \` By
764: i.h. (\ref{part:subu}) on $\cD_{2}, \cE'$\\
765: $\GG;\OO;(\DD_{P},\DD_{Q},\DD_{N})\vd[N/x] (P\ Q^{1})\hastype C$\` By rule
766: ${\RImp}E$
767: \end{tabbing}
768: \end{description}
769: \end{proof}
770:
771: Weakening, loosening, and substitution directly imply the contraction
772: property for all three kinds of hypotheses. Since we do not use
773: contraction in this paper, we elide the formal statement and proof
774: of this property.
775:
776: The notions of reduction and expansion derive directly from the ordinary
777: $\beta$ and $\eta$ rules.
778:
779: \[ \begin{array}{rcl}
780: (\lam x^k\oftp A\ldot M)\, N^k & \betared & [N/x]M \\[1ex]
781: (M \hastype A \GImp{k} B) & \etaexp & \lam x^k\oftp A\ldot M\ x^k
782: \end{array} \]
783:
784: An application of $\eta$-expansion rules requires the term $M$ to have
785: the indicated type. The subject reduction and expansion theorems are an
786: immediate consequence of the structural and substitution properties.
787:
788: \begin{theorem}[Subject Reduction] \mbox{} \newline
789: \label{thm:subred}
790: If $\GG;\OO; \DD \vd M \hastype A$ and $M \betared M'$ then
791: $\GG;\OO; \DD \vd M' \hastype A$.
792: \end{theorem}
793: \begin{proof} We proceed by cases and inversion followed
794: by an appeal to the substitution property. We show only one case.
795: Let $M = (\lamb{x^{1}}{B} P)\ Q^{1}\hastype A$ and $M' = [Q/x]P$.
796: \begin{tabbing}
797: $\GG;\OO;\DD\vd (\lamb{x^{1}}{B} P)\ Q^{1}\hastype A$ \` Assumption \\
798: $\DD=(\DD_{P},\DD_{Q})$, $\cE::(\GG,\DD_{P});\OO;\DD_{Q}\vd Q\hastype B$, and \\
799: $(\GG,\DD_{Q});\OO;\DD_{P}\vd \lamb{x^{1}}{B} P\hastype B\RImp A$ \` By inversion \\
800: $\cD::(\GG,\DD_{Q});\OO;(\DD_{P},x\oftp B)\vd P\hastype A$
801: \` By further inversion \\
802: $\GG;\OO;(\DD_{P},\DD_{Q})\vd[Q/x]P\hastype A$
803: \`By substitution$^{1}$ on $\cD,\cE$
804: \end{tabbing}
805: \end{proof}
806:
807: Subject reduction continues to hold if we allow the reduction of an arbitrary
808: subterm occurrence. We omit the obvious statement and formal proof of
809: this fact.
810:
811: \begin{theorem}[Subject Expansion] \mbox{} \newline
812: \label{thm:subexp}
813: If $\GG;\OO; \DD \vd (M \hastype A) \GImp{k} B$ and $(M \hastype
814: A\GImp{k} B) \etaexp M'$ then $\GG;\OO; \DD \vd M' \hastype A
815: \GImp{k} B$.
816: \end{theorem}
817: \begin{proof} Direct. We consider only the strict case ($k = 1$).
818: \begin{tabbing}
819: $\GG;\OO;\DD\vd M\hastype A\RImp B$ \` Assumption \\
820: $(\GG,x\oftp A);\OO; \DD\vd M \hastype A\RImp B$\` By
821: weakening$^{u}$ \\
822: $(\GG,\DD);\OO;x\oftp A\vd x\hastype A$ \` By rule $\mathtt{Id}^{1}$ \\
823: $\GG;\OO; (\DD,x\oftp A) \vd M\ x^{1} \hastype B$
824: \` By rule ${\RImp}E$ \\
825: $\GG;\OO; \DD\vd \lamb{x^{1}}{A} M\ x^{1} \hastype A\RImp B$
826: \` By rule $\RImp I$
827: \end{tabbing}
828: \end{proof}
829:
830: The following lemma establishes a sort of consistency property of the
831: type system, showing that a term $M$ cannot be both strict and vacuous
832: in a given variable. This will be central in the proof of disjointness
833: of pattern complementation (Lemma~\ref{le:part1}).
834:
835: \begin{lemma}[Exclusivity] \mbox{}
836: \label{le:disj}
837: It is not the case that both $\GG_1;\OO_1;(\DD_1,x\oftp C)\vd M\hastype
838: A$ and $\GG_2;(\OO_2,x\oftp C);\DD_2\vd M\hastype A$.
839: \end{lemma}
840: \begin{proof}
841: By induction on the structure of the derivation of
842: $\GG_1;\OO_1;(\DD_1,x\oftp C)\vd M\hastype A$, applying inversion on the
843: derivation of $\GG_2;(\OO_2,x\oftp C);\DD_2\vd M\hastype A$ in each
844: case.
845: \end{proof}
846:
847: % \input{canonical} % the canonical form theorem
848:
849: \section{The Canonical Form Theorem}
850: \label{sec:canonthm}
851:
852: In this section we establish the existence of canonical forms for the
853: strict $\lambda$-calculus, i.e., $\beta$-normal $\eta$-long forms, which
854: is crucial for our intended application. We prove this by Tait's
855: method of \emph{logical relations}; we essentially follow the account
856: in \cite{Pfenning01book}, with a surprisingly little amount of
857: generalization from simple to strict types, thanks to a
858: simplified account of substitutions.
859:
860: We start by presenting the inductive definition of \emph{canonical}
861: forms. It is realized by the two mutually recursive
862: judgments depicted in Figure~\ref{fig:canon}:
863: \[ \begin{tabular}{ll}
864: $\GG;\OO;\DD\vd M \da A$ & $M$ is atomic of type $A$. \\
865: $\GG;\OO;\DD\vd M \bua A$ & $M$ is canonical of type $A$.
866: \end{tabular} \]
867:
868: \begin{figure}
869: \[
870: \begin{array}{c}
871: \ianc{c\oftp A\in\Sigma}{\GG; \OO;\cdot \vd c\da A}{\mathtt{cIdc}}\\[2ex]
872: \ianc{}{(\GG,x\oftp A);\OO; \cdot \vd x\da A}{\mathtt{cId}^{u}}
873: \qquad \mbox{\textrm{no $\mathtt{cId}^0$ rule}}
874: \qquad
875: \ianc{}{\GG;\OO; x\oftp A \vd x\da A} {\mathtt{cId}^{1}}
876: \\[2ex]
877: %\ianc{}{\GG;\OO;\DD\vd E\ \ol{x_{n}^{l}}\da P}{cPat}
878: %\qquad
879: \ianc{\GG;\OO;\DD \vd M\da a}{\GG;\OO;\DD \vd M\bua a}
880: {\mathtt{cAt}}\\[2ex]
881: \ianc{(\GG,x\oftp A) ; \OO;\DD \vd M\bua B}{\GG;\OO;\DD\vd(\lamb{x^u}{A} M) \bua
882: A\TImp B} {\mathtt{c}\TImp I}
883: \\[2ex]
884: \ianc{\GG ; \OO; (\DD,x\oftp A) \vd M\bua B}{\GG;\OO;\DD\vd(\lamb{x^1}{A} M) \bua
885: A\RImp B}{\mathtt{c}\RImp I}
886: \\[2ex]
887: \ianc{\GG ;(\OO, x\oftp A) ;\DD \vd M\bua B}{\GG;\OO;\DD\vd(\lamb{x^0}{A} M) \bua
888: A\ZImp B}{\mathtt{c}\ZImp I}
889: \\[2ex]
890: \ibnc{\GG; \OO; \DD \vd M \da A \TImp B}{(\GG, \DD);
891: \OO; \cdot \vd N \bua A}{\GG; \OO; \DD
892: \vd M\ N^u \da B}{\mathtt{c}\GImp{u}E}
893: \\[2ex]
894: \ianc{\GG;\OO;\DD\vd M \da A \ZImp B \quad (\GG,\OO,\DD);\cdot;\cdot \vd N \bua A
895: } {\GG;\OO;\DD \vd M \ N^0 \da B}{\mathtt{c}{\ZImp}E}\\[2ex]
896: \ibnc{(\GG, \DD_N); \OO; \DD_M \vd M \da A \RImp
897: B}{(\GG, \DD_M); \OO; \DD_N \vd N \bua A}{\GG; \OO;
898: (\DD_M, \DD_N) \vd M\ N^1 \da B}{\mathtt{c}{\RImp}E}
899: \end{array}
900: \]
901: \caption{Canonical forms: $\god\vd M\buda A$}
902: \label{fig:canon}
903: \end{figure}
904:
905:
906: \begin{figure}
907: \[
908: \begin{array}{c}
909: \ianc{c\oftp A\in\Sigma}{\Psi \vd c\da c\hastype A}{\mathtt{tcIdc}}\qquad
910: %\ianc{}{\Psi\vd x\da x\hastype A}{tcId^{u}}
911: %\qquad \mbox{\textrm{no rule for }}tcId^{0}
912: \qquad
913: \ianc{x\oftp A\in\Psi}{\Psi \vd x\da x\hastype A} {\mathtt{tcIdvar}}
914: \\[2ex]
915: \ibnc{M\whr M'}{\Psi\vd M'\bua M''\hastype a}{\Psi\vd M\bua M''\hastype a}{\mathtt{tc}
916: \whr}
917: \qquad
918: \ianc{\Psi \vd M\da N\hastype a}{\Psi\vd
919: M\bua N\hastype a}{\mathtt{tcAtm}}
920: \\[2ex]
921: \ianc{\Psi,x\oftp A \vd M\ x^k\bua N\hastype B}
922: {\Psi\vd M\bua (\lamb{x^x}{A} N) \hastype A\GImp{k} B}
923: {\mathtt{tc}\GImp{k} I}
924: \qquad
925: % \ianc{\GG ;(\OO, x\oftp A) ;\DD \vd M\ x^0\bua N\hastype B}
926: % {\GG;\OO;\DD\vd M\bua (\lamb{x^0}{A} N) \hastype A\ZImp B}{\mathtt{tc}\ZImp I}
927: % \\[2ex]
928: % \ianc{\GG ; \OO; (\DD,x\oftp A) \vd M\ x^1\bua N\hastype B}
929: % {\GG;\DD\vd M\bua(\lamb{x^1}{A} N) \hastype A\RImp B}{\mathtt{tc}\RImp I}
930: % \\[2ex]
931: \ibnc{\Psi\vd M \da P\hastype A \GImp{k} B}{\Psi \vd N \bua Q
932: \hastype A}{\Psi \vd M\ N^k \da P\ Q^k\hastype B}{\mathtt{tc}\GImp{k}E}
933: % \\[2ex]
934: % \ibnc{\GG;\OO;\DD\vd M \da P\hastype A \ZImp B}{ (\GG,\OO,\DD);
935: % \cdot;\cdot \vd N \bua Q\hastype A}
936: % {\GG;\OO;\DD \vd M \ N^0 \da P\ Q^0\hastype B}{\mathtt{tc}{\ZImp}E}\\[2ex]
937: % \ibnc{(\GG, \DD_N); \OO; \DD_M \vd M \da P\hastype A \RImp
938: % B}{(\GG, \DD_M); \OO; \DD_N \vd N \bua Q\hastype
939: % A}{\GG; \OO; (\DD_M, \DD_N) \vd M\ N^1 \da P\ Q^1\hastype
940: % B}{\mathtt{tc}{\RImp}E}
941: \end{array}
942: \]
943: \caption{Conversion to canonical form: $\Psi\vd M \buda N\hastype A$}
944: \label{fig:tocanon}
945: \end{figure}
946:
947: Informally, $M$ is atomic (written $M \da A$ for some $A$) if $M$
948: consists of a variable applied to a sequence of arguments, where each of
949: the arguments is canonical at appropriate type. A term $M$ is canonical
950: if $M$ consists of a sequence of $\lambda$-abstractions followed by an
951: atomic term of atomic type. We shall abbreviate judgments involving
952: $\bua$ and $\da$ as $\buda$.
953:
954: \begin{lemma}[Soundness of Canonical Terms] \mbox{} \newline
955: \label{le:conversound}
956: If $\god\vd M\buda A$, then $\god\vd M\hastype A$.
957: \end{lemma}
958: \begin{proof}
959: By induction on the structure of the derivation of $\god\vd
960: M\buda A$.
961: \end{proof}
962:
963: We describe an algorithm for conversion to canonical form in
964: Figure~\ref{fig:tocanon}. This algorithm is presented as a deductive
965: system that can be used to construct a canonical form from an arbitrary
966: well-typed term. Note that the algorithm does not need to keep track of
967: occurrence constraints---they will be satisfied by construction (see
968: Theorem~\ref{thm:convercf}). We write $\Psi$ for a single context of
969: distinct variable declarations whose status should be considered
970: ambiguous since it is unnecessary to know whether they are unrestricted,
971: irrelevant, or strict.
972:
973: \[ \begin{tabular}{ll}
974: $\Psi\vd M \da N\hastype A$ & $M$ has atomic form $N$ of type $A$. \\
975: $\Psi\vd M \bua N\hastype A$ & $M$ has canonical form $N$ at type $A$.
976: \end{tabular} \]
977: These utilize weak head reduction, which
978: includes local reduction ($\beta$) and partial congruence ($\nu$):
979: \begin{eqnarray*}
980: \ianc{}{(\lamb{x^k}{A} M)\ N^k \whr [N/x]M}{\beta^k}\qquad
981: \ianc{M\whr Q}{M\ N^k \whr Q\ N^k}{\nu^k}
982: \end{eqnarray*}
983: Operationally, we assume that $M$ is given and we construct
984: an $N$ such that $M \whr N$ or fail. The judgments for conversion
985: to canonical form can be interpreted as an algorithm in the following
986: manner:
987: \[ \begin{tabular}{ll}
988: $\Psi \vd M \da N \hastype A$ & Given $\Psi$ and $M$ construct $N$ and $A$ \\
989: $\Psi \vd M \bua N \hastype A$ & Given $\Psi$, $M$, and $A$ construct $N$ \\
990: \end{tabular} \]
991: The main theorem of this section states that if $\GG; \OO; \DD \vd
992: M \hastype A$ and $\Psi = (\GG,\OO,\DD)$ then the two judgments
993: above will always succeed to construct an $N$ and $A$, or $N$, respectively.
994:
995: \begin{theorem}[Conversion Yields Canonical Terms]\mbox{} \newline
996: \label{thm:convercf}
997: If $(\GG,\OO,\DD) \vd M\buda N\hastype A$ and $\GG; \OO;
998: \DD \vd M\hastype A$, then $\god\vd N\buda A$.
999: \end{theorem}
1000: \begin{proof}
1001: By induction on the structure of the derivation of
1002: $(\GG,\OO,\DD) \vd M\buda N\hastype A$ and inversion on the
1003: given typing derivation in each case.
1004: \end{proof}
1005:
1006: In the construction of logical relations we will need a notion of
1007: context extension, $\Psi' \geq \Psi$ ($\Psi'$ extends $\Psi$ with zero
1008: or more declarations). It is clear that conversion to canonical form is
1009: not affected by weakening. We omit the formal statement of this
1010: property.
1011:
1012: We can now introduce a unary \emph{Kripke-logical relation}, in complete
1013: analogy with the usual definition for the simply-typed $\lam$-calculus.
1014: At base type we postulate the property we are trying to show, namely
1015: existence of canonical forms. At higher type we reduce the property to
1016: lower types by quantifying over all possible elimination forms.
1017:
1018: \begin{definition}[Valid Terms]
1019: \mbox{}
1020: \begin{enumerate}
1021: \item $\Psi\vd M\in\den{a}$ iff $\Psi\vd M\bua N\hastype a$, for some $N$.
1022: \item
1023: $\Psi\vd M\in\den{A\GImp{k} B}$ iff for every $\Psi'\geq \Psi$ and every
1024: $N$, if $ \Psi'\vd N\in\den{A}$, then $\Psi'\vd M\ N^k\in\den{B}$.
1025: \end{enumerate}
1026: We say a term $M$ is \emph{valid} if $\Psi \vd M \in\den{A}$ for
1027: appropriate $\Psi$ and $A$.
1028: \end{definition}
1029:
1030: First we show that all valid terms have canonical forms. We prove at
1031: the same time that atomic terms are valid, both by induction on the
1032: structure of their types.
1033:
1034: \begin{lemma}[Valid Terms have Canonical Forms] \mbox{}
1035: \label{le:lr2canon}
1036: \begin{enumerate}
1037: \item If $\Psi\vd M\in\den{A}$, then $\Psi\vd M\bua N\hastype A$.
1038: \item If $\Psi\vd M\da N\hastype A$, then $\Psi\vd M\in\den{A}$.
1039: \end{enumerate}
1040: \end{lemma}
1041: \begin{proof}
1042: By induction on $A$.
1043: \begin{description}
1044: \item[Case] $A=a$. Immediate from the definition of $\den{a}$.
1045: \item[Case] $A=A_1\GImp{k} A_2$.
1046: \begin{enumerate}
1047: \item %1
1048: \begin{tabbing}
1049: $\Psi\vd M\in\den{A_1\GImp{k} A_2}$ \` Assumption \\
1050: $\Psi,x\oftp A_1\geq \Psi$ \` By definition of $\geq$\\
1051: $\Psi,x\oftp A_1\vd x\da x\hastype A_1$ \` By rule $\mathtt{tcIdvar}$\\
1052: $\Psi,x\oftp A_1\vd x\in\den{A_1}$ \` By i.h.\ (2)\\
1053: $\Psi,x\oftp A_1\vd M\ x^k\in\den{ A_2}$ \` By definition of $\den{\cdot}$\\
1054: $\Psi,x\oftp A_1\vd M\ x^k\bua N\hastype A_2$ \` By i.h.\ (1)\\
1055: $\Psi\vd M\bua\lamb{x^k}{A_1}N\hastype A_1\GImp{k} A_2$
1056: \` By rule $\mathtt{tc} \GImp{k} I$
1057: \end{tabbing}
1058: \item %2
1059: \begin{tabbing}
1060: $\Psi\vd M\da M'\hastype A_1\GImp{k} A_2$ \` Assumption \\
1061: $\Psi'\geq\Psi$ and $\Psi'\vd N\in\den{A_1}$ for arbitrary $\Psi'$ and $N$
1062: \` New assumption \\
1063: $\Psi'\vd N\bua N' \hastype {A_1}$ \` By i.h.\ (1) \\
1064: $\Psi'\vd M\da M'\hastype A_1\GImp{k} A_2$ \` By weakening \\
1065: $\Psi'\vd M\ N^k\da M'\ {N'}^k\hastype A_2$ \` By rule $\mathtt{tc}{\GImp{k}}E$\\
1066: $\Psi'\vd M\ N^k\in\den{ A_2}$ \` By i.h.\ (2)\\
1067: $\Psi\vd M\in\den{A_1\GImp{k} A_2}$ \` By definition of $\den{\cdot}$
1068: \end{tabbing}
1069: \end{enumerate}
1070: \end{description}
1071: \end{proof}
1072:
1073: The second major part states that every well-typed term is valid. For
1074: this we need closure of validity under head expansion.
1075:
1076: \begin{lemma}[Closure under Head Expansion]
1077: \label{le:clohead}
1078: \mbox{} \newline
1079: If $\Psi\vd M'\in\den{A}$ and $M\whr M'$, then $\Psi \vd M\in\den{A}$.
1080: \end{lemma}
1081: \begin{proof} By induction on $A$:
1082: \begin{description}
1083: \item[Case] $A=a$. immediate by definition and rule $\texttt{tc}\whr$.
1084: \item[Case] $A=A_1\GImp{k} A_2$.
1085: \begin{tabbing}
1086: $\Psi\vd M'\in\den{A_1\GImp{k} A_2}$ \` Assumption \\
1087: $\Psi'\vd N\in\den{A_1}$ for arbitrary $\Psi'\geq \Psi$ and $N$
1088: \` New assumption \\
1089: $\Psi'\vd M'\ N^k\in\den{A_2}$ \` By definition of $ \den{\cdot}$ \\
1090: $M\ N^k\whr M'\ N^k$ \` By rule $\nu$ \\
1091: $\Psi'\vd M\ N^k\in\den{A_2}$ \` By i.h.\ on $A_2$ \\
1092: $\Psi\vd M\in\den{A_1\GImp{k} A_2}$ \` By definition of $ \den{\cdot}$
1093: \end{tabbing}
1094: \end{description}
1095: \end{proof}
1096:
1097: Due to the need to $\beta$-reduce during conversion to canonical form,
1098: we need to introduce \emph{substitutions}. We will not require
1099: substitutions to be well-typed, but they have to be valid in the sense
1100: that all substitution terms should be valid.
1101:
1102: \[ \begin{array}{rrcl}
1103: \mbox{\textit{Substitutions}}& \theta & \bnfas \epsilon\bnfalt \theta,M/x
1104: \end{array} \]
1105:
1106: For $\theta=\theta',M/x$, we say that $x$ is \emph{defined} in $\theta$
1107: and we write $\theta(x)=M$. We require all variables defined in a
1108: substitution to be distinct: we use $\dom(\theta)$ for the set of
1109: variables defined in $\theta$. Furthermore, the co-domain of $\theta$
1110: are the variables occurring in the substituting terms.
1111:
1112: Next, we define the \emph{application} of a substitution $\theta$ to a
1113: term $M$, denoted $[\theta]M$. We limit application of substitutions to
1114: objects whose free variables are in the domain of $\theta$.
1115: \begin{eqnarray*}
1116: [\theta] c & = & c \\ \relax
1117: [\theta] x & = & \theta(x)\\ \relax
1118: [\theta](M\ N^k) & = & ([\theta]M) \ ([\theta] N)^k\\ \relax
1119: [\theta](\lamb{x^k}{A}M) & = & \lamb{x^k}{A}[\theta,x/x]M
1120: \end{eqnarray*}
1121: In the last case we assume that $x$ does not already occur in the
1122: domain or co-domain of $\theta$. This can always be achieved by
1123: renaming of the bound variable.
1124:
1125: We will also need to mediate between single substitutions
1126: stemming from $\beta$-reduction and simultaneous substitutions. We
1127: define how to \emph{compose} a single substitution from a
1128: $\beta$-reduction with simultaneous substitutions, written
1129: as $[N/x]\theta$.
1130: \begin{eqnarray*}
1131: [N/x](\epsilon) & = & \epsilon \\ \relax
1132: [N/x](\theta,M/y) & = & [N/x](\theta), ([N/x]M)/y
1133: \end{eqnarray*}
1134:
1135: Note that $[N/x]([\theta,x/x]M) = [\theta,N/x]M$ if $x$ does not occur
1136: in the co-domain of $\theta$. For a context $\Psi=x_1\oftp A_1,\ldots,
1137: x_n\oftp A_n$, we introduce the \emph{identity} substitution on $\Psi$
1138: as ${\rm id}_{\Psi}=x_1/x_1,\ldots, x_n/x_n$. Clearly, ${\rm id}_{\Psi}M
1139: = M$ if the free variables of $M$ are contained in $\Psi$.
1140:
1141: We extend the notion of validity to substitutions as already indicated
1142: above: a substitution $\theta$ is valid for context $\Psi$ if for
1143: every binding $M/x$ such that $x\oftp A$ is in $\Psi$ we have $M$ is in
1144: $\den{A}$.
1145:
1146: \begin{definition}[Valid Substitutions]
1147: \mbox{}
1148: \begin{enumerate}
1149: \item $\Phi\vd \theta\in\den{\cdot}$ iff $\theta=\epsilon$.
1150: \item $\Phi\vd\theta\in\den{\Psi',x\oftp A}$
1151: iff $\theta=\theta',M/x$ such that $\Phi\vd M\in\den{A}$ and
1152: $\Phi\vd\theta'\in\den{\Psi'}$.
1153: \end{enumerate}
1154: \end{definition}
1155:
1156: We remark that contexts are not ordered, hence, for
1157: $\Psi=(\GG,\OO,\DD)$ we will identify, for example,
1158: $\den{\Psi,x\oftp A}$ with $\den{(\GG,x\oftp A,\OO,\DD)}$. Clearly, this
1159: view is legitimate in terms of the above definition, since validity
1160: of a substitution simply reduces to validity of the terms in
1161: it. It is easy to see that validity, both
1162: for terms and for substitutions, satisfies weakening. We omit
1163: the formal statement and proof of this property.
1164:
1165: The next lemma is critical. It generalizes the statement that
1166: well-typed terms are valid by allowing for a valid substitution
1167: to be applied. This is necessary in order to proceed with the
1168: proof in the case of any of the three $\lambda$-abstractions.
1169:
1170: \begin{lemma}[Well-Typed Terms are Valid]
1171: \label{le:lrmain} \mbox{} \newline
1172: If $\god\vd M\hastype A$, then for every $\Psi$ such that
1173: $\Psi\vd\theta\in\den{\godc}$ we have $\Psi\vd [\theta]M\in\den{A}$.
1174: \end{lemma}
1175: \begin{proof}
1176: By induction on the typing derivation $\cD$ of $\god\vd M\hastype A$.
1177: \begin{description}
1178: \item[Case]
1179: \[ \cD= \ianc{}{(\GG, x\oftp A); \OO; \cdot \vd x \hastype A}{\mathtt{Id}^u} \]
1180: \begin{tabbing}
1181: $\Psi\vd\theta\in\den{(\GG,x\oftp A,\OO)}$ \` Assumption \\
1182: $\Psi\vd\theta(x)\in\den{A}$ \` By definition of $\den{\cdot}$\\
1183: $\Psi\vd[\theta]x\in\den{A}$ \` By definition of substitution
1184: \end{tabbing}
1185: \item[Case] $\cD$ ends in $\mathtt{Id}^1$. As in the previous case.
1186: \item[Case] $\cD$ ends in $\mathtt{Con}$. Immediate by
1187: Lemma~\ref{le:lr2canon}(2) and definition of substitution.
1188: \item[Case] % TImp
1189: \[ \cD=\ianc{(\GG, x\oftp A); \OO; \DD \vd M \hastype B}{\GG;
1190: \OO; \DD \vd \lam x^u \oftp A\ldot M \hastype A \GImp{u}
1191: B}{\GImp{u}I} \]
1192: \begin{tabbing}
1193: $(\GG, x\oftp A); \OO; \DD \vd M \hastype B$ \` Subderivation \\
1194: $\Psi\vd\theta\in\den{\godc}$ \` Assumption \\
1195: $\Psi'\vd N\in\den{A}$ for arbitrary $\Psi' \geq \Psi$ and $N$
1196: \` New assumption \\
1197: $\Psi'\vd(\theta,N/x)\in\den{(\GG,x\oftp A,\OO,\DD)}$
1198: \` By definition of $\den{\cdot}$
1199: and weakening\\
1200: $\Psi'\vd [\theta,N/x]M\in\den{B}$ \` By i.h. \\
1201: $\Psi'\vd [N/x]([\theta,x/x] M)\in\den{B}$ \` By property of substitution \\
1202: $\Psi'\vd(\lamb{x^u}{A}[\theta,x/x]M) N^u\in\den{B}$ \` By Lemma~\ref{le:clohead} \\
1203: $\Psi'\vd ([\theta](\lamb{x^u}{A}M)) N^u\in\den{B}$
1204: \` By definition of substitution \\
1205: $\Psi\vd [\theta](\lamb{x^u}{A}M)\in\den{A\TImp B}$
1206: \` By definition of $\den{A\TImp B}$
1207: \end{tabbing}
1208: \item[Cases] $\cD$ ends in ${\GImp{0}I}$ or ${\GImp{1}I}$. Analogous
1209: to previous case.
1210: \item[Case]
1211: \[ \cD = \ibnc{\GG; \OO; \DD \vd M \hastype A \TImp B}{(\GG,
1212: \DD); \OO; \cdot \vd N \hastype A}{\GG; \OO; \DD \vd M\
1213: N^u \hastype B}{\GImp{u}E} \]
1214: \begin{tabbing}
1215: $\Psi\vd\theta\in\den{\godc}$ \` Assumption \\
1216: $\GG; \OO; \DD \vd M \hastype A \TImp B$ \` Subderivation \\
1217: $\Psi\vd[\theta]M\in\den{A\TImp B}$ \` By i.h. \\
1218: $(\GG,\DD); \OO; \cdot \vd N \hastype A$ \` Subderivation \\
1219: $\Psi \vd [\theta]N \in\den{ A}$ \` By i.h. \\
1220: $\Psi\geq\Psi$ \` By definition of $\geq$\\
1221: $\Psi\vd ([\theta]M)([\theta] N)^u\in\den{B}$ \` By definition
1222: of $\den{\cdot}$ \\
1223: $\Psi\vd [\theta](M\ N)^u\in\den{B}$ \` By definition of substitution
1224: \end{tabbing}
1225: \item[Cases] $\cD$ ends in ${\GImp{0}E}$ or ${\GImp{1}E}$. Analogous
1226: to the previous case.
1227: \end{description}
1228: \end{proof}
1229:
1230: From this central lemma, the canonical form theorem follows by
1231: noting that the identity substitution is valid.
1232:
1233: \begin{lemma}[Validity of Identity]
1234: \label{le:lrid}
1235: $\Psi\vd id_{\Psi}\in\den{\Psi}$.
1236: \end{lemma}
1237: \begin{proof}
1238: By a straightforward induction on $\Psi$ using
1239: Lemma~\ref{le:lr2canon}(2).
1240: \end{proof}
1241:
1242: \begin{theorem}[Canonical Forms]
1243: \label{thm:canonical} \mbox{} \newline
1244: If $\god\vd M\hastype A$, then there exists an $N$ such that $\godc\vd
1245: M\bua N\hastype A$ and $\god\vd N\bua A$.
1246: \end{theorem}
1247: \begin{proof} Direct from prior lemmas.
1248: \begin{tabbing}
1249: $\god\vd M\hastype A$ \` Assumption \\
1250: $\godc\vd id_{\godc}\in\den{\godc}$ \` By Lemma~\ref{le:lrid} \\
1251: $\godc\vd [id_{\godc}]M\in\den{A}$ \` By Lemma~\ref{le:lrmain} \\
1252: $\godc\vd M\in\den{A}$ \` By identity substitution \\
1253: $\godc\vd M\bua N\hastype A$ for some $N$ \` By Lemma~\ref{le:lr2canon}(1) \\
1254: $\god\vd N\bua A$ \` By Theorem~\ref{thm:convercf}
1255: \end{tabbing}
1256: \end{proof}
1257:
1258:
1259: We close this section with some remarks on related work on strictness.
1260: Church original definition of the set $\Lambda_{I}$ of (untyped)
1261: $\lam$-terms \cite{Church41} has this clause for abstraction:
1262: \begin{center}
1263: If $M\in\Lambda_{I}$ and $x\in FV(M)$, then $\lam x\ldot M\in\Lambda_{I}$.
1264: \end{center}
1265: Therefore, in this language there cannot be any vacuous abstractions.
1266: The combinatorial counterpart of this calculus excludes $\mathbf{K}$ and
1267: consists of $\mathbf{I,W,B,C}$. Those are the axioms of what Church
1268: called \emph{weak implicational logic}~\cite{Church51}, i.e., identity,
1269: contraction, prefixing and permutation. This establishes the link with
1270: an enterprise born from a very different origin, namely the relevance
1271: logic project~\cite{Anderson75}, which emerged in fact in the early
1272: sixties out of Anderson and Belnap's dissatisfaction with the so-called
1273: ``\emph{paradoxes of implication}'', let it be material, intuitionistic,
1274: or strict (in the modal sense of Lewis and Langford).
1275:
1276: Following Girard's and Belnap's suggestion \cite{Belnap93}, we will
1277: \emph{not} refer to our calculus as \emph{relevant}, but as
1278: \emph{strict} logic, as the former may also satisfy other principles
1279: such as distributivity of implication over conjunction.
1280:
1281: On an unrelated front, starting with Mycroft's seminal paper
1282: \cite{Mycroft80}, compile-time analysis of functional programs
1283: concentrated on strictness analysis in order to get the best out of
1284: call-by-value and call-by-need evaluation; first in terms of abstract
1285: interpretation, later by using non-standard types to represent these
1286: ``intensional'' properties of functions (see \cite{Jensen91} for a
1287: comparison of these two techniques). However, earlier work such as
1288: \cite{Kuo89} used non-standard primitive type to distinguish strict or
1289: non-strict terms, closed only under unrestricted function space.
1290: In the setting of functional programming, various different notions
1291: of strictness emerged. However, the absence of recursion and
1292: effects in our setting admits fewer distinctions.
1293:
1294: \citeN{Wright92} seems to be the first to have extended the
1295: Curry-Howard isomorphism to the implicational fragment of relevance
1296: logic and explicitly connected the two areas, although both
1297: \cite{Belnap74} and \cite{Helman77} had previously recognized the link
1298: between strictness and relevance.
1299:
1300: \citeN{Baker94} presents a type assignment system that
1301: makes available strict, invariant and intuitionistic types. It is
1302: biased towards enforcing strictness information, which ultimately leads
1303: to a different expressive power from our calculus. There is only one
1304: context, where variables carry their occurrence status as a label.
1305: There is one identity rule, the strict one, so that e.g.\ $\lam x\ldot x
1306: \hastype A\TImp A$ is not derivable, as it can be given the more stringent type
1307: $A\RImp A$. Let us consider the elimination rules for strict and
1308: irrelevant functions.
1309: \[ \begin{array}{c}
1310: \ibnc{\GG\vd M\hastype A\RImp B}{\GG'\vd N\hastype A'}{\GG,\GG'\vd
1311: M\ N\hastype B}{app\RImp}\\[1ex]
1312: \ibnc{\GG\vd M\hastype A\ZImp
1313: B}{\GG'\vd N\hastype A'}{\GG,\GG'[1:=0]\vd M\ N\hastype
1314: B}{app\ZImp}
1315: \end{array} \]
1316: A side condition $A'\leq A$ enforces the information ordering, so that
1317: for example $A'\ZImp B\leq A\TImp B'$, provided that $A\leq A', B\leq
1318: B'$. This allows us to infer by strict application $\GG,\GG'\vd M\
1319: N\hastype C$ from $\GG\vd M\hastype (A\TImp B)\RImp C$ and $\GG'\vd N
1320: \hastype A\ZImp B$. The latter is instead forbidden in our system by the
1321: labeled reduction rules. The rationale on the relabeling operation in
1322: the rule $app\ZImp$ is that $A$ is not relevant to $B$, so all
1323: hypothesis should be deleted. Instead, in order to preserve every
1324: variable declaration, their strict label is changed into irrelevant.
1325: This would amount to moving the strict variables in the irrelevant
1326: context in our system. Note the difference with our rule, where the
1327: latter variables are moved in the unrestricted context. Moreover,
1328: having only one context, the author needs a strategy to deal with
1329: the same variable with different annotations; the solution is that while
1330: propagating premises top-down a binding $x^1\oftp A$ supersedes
1331: $x^u\oftp A$ which in turn supersedes $x^0\oftp A$.
1332:
1333: \citeN{Wright96} introduces \emph{Annotation Logic} as a
1334: general framework for resource-conscious logics. Its formulae have the
1335: form $A\bnfas X^k\bnfalt A\GImp{k} B$ for any annotation $k$ and there
1336: are specific structural as well as annotation rules. The latter
1337: implement rules such as promotion or dereliction. By instantiation with
1338: different algebras of annotation, we get systems such as linear and
1339: strict logic as well as various other usage logics. An abstract
1340: normalization procedure is sketched, which however requires commutative
1341: conversions already in the purely implicational fragment.
1342:
1343: In summary, none of the systems of strict function in the literature
1344: served our purpose, nor did any of the authors prove the existence
1345: of canonical forms that are critical for our application.
1346:
1347:
1348: \section{Simple Terms}
1349: \label{sec:strictcomp}
1350:
1351: Now that we have developed a calculus which is potentially strong enough
1352: to represent the complement of linear patterns, two questions naturally
1353: arise: how do we embed the original $\lambda$-calculus, and is the
1354: calculus now closed under complement? We require that our complement
1355: operator ought to satisfy the usual boolean rules for negation:
1356: \begin{enumerate}
1357: \item (Exclusivity) It is not the case that some $M$ is both a ground
1358: instance of $N$ and of $\mnot(N)$.
1359: \item (Exhaustivity) Every $M$ is a ground instance of $N$ or of $\mnot(N)$.
1360: \end{enumerate}
1361: Remember that when we refer to \emph{ground instances} we mean instances
1362: without any existential variables. Parameters, on the other hand, can
1363: certainly occur.
1364:
1365: Unfortunately, while the first property follows quite easily for a
1366: suitable algorithm, it turns out the second cannot be achieved for the
1367: full strict $\lambda$-calculus calculus as presented in the previous
1368: sections. The following counterexample is a pattern whose complement
1369: cannot be expressed within the language.
1370:
1371: \begin{example}
1372: Consider the signature $a\oftp\mbox{type}, b\oftp a, c\oftp a \TImp a$.
1373: Then in the context $x\oftp a; \cdot; \cdot$ we have
1374: \[ \begin{array}{rcl}
1375: \| E\ x^0 \| & = & \{ b, c\ b^u, c\ (c\ b^u)^u, \ldots \} \\
1376: \mnot(\| E\ x^0 \|) & = & \{ x, c\ x^u, c\ (c\ x^u)^u, \ldots \} \\
1377: % \| F\ x^1 \| & = & \{ x \} \\
1378: % \mnot(\| F\ x^1 \|) & = & \{ c\ x^u, c\ (c\ x^u)^u, \ldots, b, c\ b^u, \ldots \}
1379: \end{array} \]
1380: It is easy to see that $\mnot(\| E\ x^0\|)$ cannot be described by a
1381: finite set of patterns. The underlying problem is the undetermined
1382: status of the argument to $c \oftp a \TImp a$ which means it can
1383: contain neither strict nor irrelevant variables while being allowed to
1384: contain unrestricted variables.
1385: \end{example}
1386:
1387: However, the main result of this section is that the complement
1388: algorithm presented in Definition~\ref{def:compl} is sound and complete
1389: for the fragment which results from the natural embedding of the
1390: original simply-typed $\lambda$-calculus; this is sufficient for our
1391: intended applications. We will proceed in two phases. First we
1392: restrict ourselves to a class of terms (that we call \emph{simple}) for
1393: which the crucial property of \emph{tightening} (Lemma~\ref{le:exh}) can
1394: be established. Second we transform the complement problem so that each
1395: existential variable is applied to \emph{all} parameters and bound
1396: variables in whose scope it appears. This improvement is mainly
1397: cosmetic and makes it easier to state and prove correctness for our
1398: algorithms.
1399:
1400: Recall that we have introduced strictness to capture occurrence
1401: conditions on variables in canonical forms. This means that first-order
1402: constants (and by extension bound variables) should be considered
1403: \emph{strict} functions of their argument, since these arguments will
1404: indeed occur in the canonical form. On the other hand, if we have a
1405: second order constant, we cannot restrict the argument function to be
1406: either strict or vacuous, since this would render our representation
1407: language too weak.
1408:
1409:
1410: \begin{example}
1411: \label{ex:excont}
1412: Continuing Example~\ref{ex:lam}, consider the representation of the
1413: \textbf{K} combinator:
1414: \begin{eqnarray*}
1415: \rep{\Lambda x\ldot \Lambda y\ldot x}& = & \itlam\ (\lamb{x}{\itexp} \itlam\ (\lamb{y}{\itexp} x))
1416: \end{eqnarray*}
1417: Notice that the argument to the first occurrence of `$\itlam$' is a
1418: strict function, while the argument to the second occurrence is an
1419: invariant function. If we can give only one type to `$\itlam$' it must
1420: therefore be $(\itexp \GImp{u} \itexp) \GImp{1} \itexp$.
1421: \end{example}
1422:
1423: Generalizing this observation means that positive occurrence of
1424: function types are translated to strict functions, while the negative
1425: ones to undetermined functions. We can formalize this as an
1426: embedding of the simply-typed $\lam$-calculus into a fragment of the
1427: strict calculus via two (overloaded) mutually recursive translations
1428: $()^{-}$ and $()^{+}$. First, the definition on types:
1429: \begin{eqnarray*}
1430: (A\arrow B)^{+} & = & A^{-} \RImp B^{+}\\
1431: (A\arrow B)^{-} & = & A^{+} \TImp B^{-}\\
1432: a^{-} = a^{+} & = & a
1433: \end{eqnarray*}
1434: We extend it to atomic and canonical terms (including existential
1435: variables), signatures, and contexts; we therefore need the usual
1436: inductive definition of atomic and canonical terms in the simply-typed
1437: $\lam$-calculus (see for example~\cite{Pfenning01book}), which can be
1438: obtained by dropping labels from the definition of canonical form in
1439: Figure~\ref{fig:canon}. In addition, we allow well-typed applications
1440: $E_A\ x_1^{k_1}\ldots x_n^{k_n}$ of base type as canonical terms.
1441: Recall that $x_1, \ldots, x_n$ must be distinct bound variables or
1442: parameters. Note that the embedding $()^{-}$ is applied only to
1443: canonical terms, while $()^{+}$ is applied only to atomic terms.
1444:
1445: \begin{eqnarray*}
1446: (\lam x\oftp A\ldot M)^{-} & = & \lamb{x^{u}}{A^{+}} M^{-} \\
1447: (E_A\ x_1\ldots x_n)^{-} & = & F_{A^{-}} \ x_1^u\ldots x^u_n \\
1448: M^{-} & = & M^{+} \qquad\qquad \mbox{for $M$ of base type} \\
1449: x^{+} & = & x\\
1450: c^{+} & = & c\\
1451: (M\ N)^{+} & = & M^{+}\ (N^{-})^{1} \\[1em]
1452: (\cdot)^{+} & = & \cdot \\
1453: (\GG,x\oftp A)^{+} & = & \GG^{+}, x\oftp A^{+}\\
1454: (\Sigma,a\oftp type)^{+} & = & \Sigma^{+}, a\oftp type\\
1455: (\Sigma,c\oftp A)^{+} & = & \Sigma^{+}, c\oftp A^{+} \end{eqnarray*}
1456:
1457: \begin{example} Returning to Example~\ref{ex:excont}:
1458: \begin{eqnarray*}
1459: (\itlam\ (\lamb{x}{\itexp} \itlam\ (\lamb{y}{\itexp} x)))^+& = &
1460: \itlam\ (\lamb{x^u}{\itexp} \itlam\ (\lamb{y^u}{\itexp} x)^1)^1
1461: \end{eqnarray*}
1462: \end{example}
1463:
1464: The image of the embedding of the canonical forms of the simply-typed
1465: $\lambda$-calculus gives rise to the following fragment, where we
1466: allow existential variables to have arguments with arbitrary
1467: labels.
1468: \[ \begin{array}{rrcl}
1469: \mbox{\textit{Simple Terms}} & M & \bnfas & \lam x^{u}\oftp
1470: A^{+}\ldot M \bnfalt h\ M_1^{1} \ldots M_n^{1} \bnfalt
1471: E_{A}\ x_{1}^{k_1}\ldots x_{n}^{k_n}
1472: \end{array} \]
1473: It is possible to generalize this language further to allow
1474: arbitrary abstractions as well, but this is beyond the scope
1475: of the present paper (see the comment in the Section~\ref{sec:concl}).
1476:
1477: \begin{theorem}[Correctness of $()^{\pm}$]
1478: \label{thm:embed}
1479: \mbox{}
1480: \begin{enumerate}
1481: \item If $\GG\vd M\bua A$, then $\GG^{+};\cdot;\cdot \vd M^{-}\bua A^{-}$.
1482: \item If $\GG\vd M\da A$, then $\GG^{+};\cdot;\cdot \vd M^{+}\da A^{+}$.
1483: \end{enumerate}
1484: \end{theorem}
1485:
1486: \begin{proof}
1487: By mutual induction on the structure of the derivations of $\GG\vd
1488: M\bua A$ and $\GG\vd M\da A$.
1489: \end{proof}
1490:
1491: From now on we may hide the $()^1$ decoration from strict application of
1492: constants in examples. Moreover, we will shorten judgment $\cal J$ on
1493: simple terms of the form $\Psi; \cdot; \cdot \vd {\cal J}$ to $\Psi \vd
1494: {\cal J}$.
1495:
1496: We can now prove the crucial tightening lemma. It expresses the
1497: property that every simple term with no existential variable is either
1498: strict or vacuous in a given undetermined variable.
1499:
1500: \begin{lemma}[Tightening]
1501: \label{le:exh}
1502: Let $M$ be a simple term of type $A$ with no existential variables.
1503: \begin{enumerate}
1504: \item If $(\GG, x\oftp C); \OO; \DD \vd M\da A$ then \newline
1505: either $\GG; \OO; (\DD, x\oftp C) \vd M\da A$ or $\GG; (\OO, x\oftp
1506: C); \DD \vd M\da A$.
1507: \item If $(\GG, x\oftp C); \OO; \DD \vd M\bua A$ then \newline
1508: either $\GG\; \OO; (\DD, x\oftp C) \vd M\bua A$ or $\GG; (\OO, x\oftp
1509: C); \DD \vd M\bua A$.
1510: \end{enumerate}
1511: \end{lemma}
1512: \begin{proof}
1513: By mutual induction on $\cD_{1}::(\GG, x\oftp C); \OO; \DD \vd M\da A$ and
1514: $\cD_{2}::(\GG, x\oftp C); \OO; \DD \vd M\bua A$. We show only one case.
1515: \begin{description}
1516: \item[Case]
1517: \[ \cD_1 = \ianc{(\GG,x\oftp C,\DD_N);\OO;\DD_M \vd M \da A \RImp B
1518: \hspace{1em} (\GG,x\oftp C,\DD_M);\OO;\DD_N \vd N \bua A}{(\GG,x\oftp
1519: C);\OO; (\DD_{M},\DD_{N}) \vd M\ N^1 \da B}{\mathtt{c}{\RImp}E} \]
1520: There are four sub-cases, stemming from the two possibilities
1521: each for the two subderivations.
1522: \begin{enumerate}
1523: \item
1524: \begin{tabbing}
1525: $(\GG,\DD_N);\OO;(\DD_M,x\oftp C)\vd M\da A\RImp B$ \` Subcase of i.h. \\
1526: $(\GG,\DD_{M});\OO;(\DD_N,x\oftp C)\vd N\bua A$ \` Subcase of i.h. \\
1527: $(\GG,\DD_M,x\oftp C);\OO;\DD_N\vd N\bua A$ \` By Loosening$^{1}$ $x$\\
1528: $\GG;\OO;(\DD_M,x\oftp C,\DD_N)\vd M\ N^{1}\da B$ \` By rule $\texttt{c}{\RImp}E$
1529: \end{tabbing}
1530: \item
1531: \begin{tabbing}
1532: $(\GG,\DD_N);(\OO,x\oftp C);\DD_M\vd M\da A\RImp B$ \` Subcase of i.h. \\
1533: $(\GG,\DD_M);(\OO,x\oftp C);\DD_N\vd N\bua A$ \` Subcase of i.h. \\
1534: $\GG;(\OO,x\oftp C);(\DD_{M},\DD_{N})\vd M\ N^{1}\da B$ \` By rule $\texttt{c}{\RImp}E$
1535: \end{tabbing}
1536: \item
1537: \begin{tabbing}
1538: $(\GG,\DD_N);\OO;(\DD_M,x\oftp C)\vd M\da A\RImp B$ \` Subcase of i.h. \\
1539: $(\GG,\DD_M);(\OO,x\oftp C);\DD_N\vd N\bua A$ \` Subcase of i.h. \\
1540: $(\GG,\DD_M,x\oftp C);\OO;\DD_N\vd N\bua A$ \` By Loosening$^{0}$ $x$ \\
1541: $\GG;\OO;(\DD_M,x\oftp C,\DD_N)\vd M\ N^{1}\da B$ \` By rule $\texttt{c}{\RImp}E$
1542: \end{tabbing}
1543: \item Symmetrical to (3).
1544: \end{enumerate}
1545: \end{description}
1546: \end{proof}
1547:
1548: We remark that tightening fails to hold once we allow unrestricted function
1549: types in a negative position. For example, $(y\oftp A\TImp B,x\oftp
1550: A);\cdot;\cdot \vd y\ x^u\hastype B$ but both $y\oftp A\TImp B;\cdot;x\oftp
1551: A\nvd y\ x^u\hastype B$ and $y\oftp A\TImp B;x\oftp A;\cdot\nvd y\ x^u\hastype
1552: B$.
1553:
1554: We also have the following related property.
1555:
1556: \begin{lemma}[Irrelevance]
1557: \label{le:fat}
1558: Let $M$ be a simple term without existential variables.
1559: \begin{enumerate}
1560: \item If $\GG; (\OO, x\oftp C); \DD \vd M\bua A$,
1561: then $\GG; \OO; \DD \vd M\bua A$.
1562: \item If $\GG; (\OO, x\oftp C); \DD \vd M\da A$,
1563: then $\GG; \OO; \DD \vd M\da A$.
1564: \end{enumerate}
1565: \end{lemma}
1566:
1567: \begin{proof}
1568: By mutual induction on the given derivations.
1569: \end{proof}
1570:
1571: Note that irrelevance holds for any strict canonical term, but it is
1572: false for terms containing redices. For example, for
1573: $c\oftp B$ we have $\cdot;x\oftp A;\cdot\vd
1574: (\lamb{y^0}{A} c)\ x^0\hastype B$, but $\cdot;\cdot;\cdot\nvd
1575: (\lamb{y^0}{A} c)\ x^0\hastype B$.
1576:
1577: For simple terms it is often more convenient to replace explicit reference
1578: to atomic forms by an $n$-ary version of $\mathtt{c}{\RImp}E$. This can
1579: easily be seen to cover all atomic forms for simple terms where
1580: the head $h$ can be a variable $x$ or constant $c$.
1581: \[ \ianc{\Psi\vd h\hastype A_1\RImp\cdots\RImp A_n\RImp a \quad
1582: \Psi \vd N_1\bua A_1 \quad \cdots \quad \Psi \vd N_n \bua A_n}
1583: {\Psi \vd h\ N_1^1\ldots N_{n}^1\bua a}{\texttt{c}{\RImp}E} \]
1584:
1585: We can simplify the presentation of the algorithms for complement and
1586: later unification if we require any existential variable to be applied
1587: to every bound variable in its declaration context. This is possible
1588: for any simple linear pattern without changing the set of its
1589: ground instances. We just insert vacuous applications, which
1590: guarantee that the extra variables are not used.
1591:
1592: In a slight abuse of notation we call the resulting patterns \emph{fully
1593: applied}. This transformation is entirely straightforward and its
1594: correctness is easily established using Irrelevance
1595: (Lemma~\ref{le:fat}). We omit the formal details here, showing only an
1596: example.
1597:
1598: \begin{example}
1599: Recall the simple pattern that encodes an object-level $\eta$-redex
1600: from Example~\ref{ex:etardx},
1601: \[ \itlam\ (\lamb{x^u}{\itexp} \itapp\ E\ x). \]
1602: It is not fully applied, since $E$ is not applied to $x$. This is crucial,
1603: since $E$ is not allowed to depend on the bound variable $x$.
1604: In its fully applied form
1605: \[ \itlam\ (\lamb{x^u}{\itexp} \itapp\ (E'\ x^0)\ x), \]
1606: this occurrence condition is encoded by an irrelevant application of a
1607: fresh existential variable $E'$ of type $\itexp \GImp{0} \itexp$ to $x$.
1608: According to Lemma~\ref{le:fat}, this means that $x$ cannot occur in the
1609: canonical form of $E'\; x^0$ for any instance of $E'$.
1610: \end{example}
1611:
1612: In the remainder of this paper we will assume that all existential variables
1613: are fully applied as defined above. We refer to a pattern $E\, x_1^{k_1}\ldots
1614: x_n^{k_n}$ as a \emph{generalized variable}. Furthermore, we always sort the
1615: variables $x_1\ldots x_n$ so that they come in some standard order; this
1616: simplifies the description of some of the algorithms on fully applied
1617: patterns. Following standard terminology we call atomic terms whose head is
1618: a bound variable or a parameter \emph{rigid}, while terms whose head is an
1619: existential variable is called \emph{flexible}.
1620:
1621: Under these assumptions we can more formally specify the interpretation
1622: of terms with existential variables. We use $\Phi$ for sequences of
1623: distinct, labelled bound variables; if $x^k\in\Phi$, we set $\Phi(x)=
1624: k$. We say that $\god\vd\Phi\ ok$ if the following holds:
1625: \begin{eqnarray*}
1626: \Phi(x) = u & \BImp & x\in\dom(\GG)\\
1627: \Phi(x) = 0 & \BImp & x\in\dom(\OO)\\
1628: \Phi(x) = 1 & \BImp & x\in\dom(\DD)
1629: \end{eqnarray*}
1630: Note that $\Phi$ determines $\GG; \OO; \DD$ and vice versa whenever
1631: $\god\vd \Phi\ ok$.
1632:
1633: \begin{figure}
1634: \[
1635: \begin{array}{c}
1636: \ianc{\GG; \OO; \DD \vd \Phi\; ok \qquad
1637: \GG; \OO; \DD \vd M \hastype a}
1638: {\Psi \vd M \in\| E_A\ \Phi\|\hastype a}
1639: {\mbox{\tt grFlx}}
1640: \\[2ex]
1641: \ianc{(\Psi,x\oftp A)\vd M \in\| N\|\hastype B}
1642: {\Psi \vd \lam x^u\oftp A\ldot M \in\|\lam x^u\oftp A\ldot N \|:A\TImp B}{\mbox{\tt grLam}}
1643: \\[2ex]
1644: \ianc{\Psi \vd h \hastype A_1\RImp\cdots\RImp A_n\RImp a \qquad
1645: \Psi \vd M_1 \in\| N_{1}\|\hastype A_1\;\cdots\;
1646: \Psi\vd M_n\in\|N_n\| \hastype A_n}
1647: {\Psi \vd h\ M_1^1\ldots M_n^1 \in\|h\ N_1^1\ldots N_n^1 \|\hastype a}
1648: {\mbox{\tt grApp}}
1649: \end{array}
1650: \]
1651: \caption{Ground instance: $\Psi \vd M\in \|N\| \hastype A$}
1652: \label{fig:grinst}
1653: \end{figure}
1654:
1655: Recall that every pattern can be seen as the intensional
1656: representation of the set of its instances with respected to a fixed
1657: signature $\Sigma$ and a set of parameters declared in a context
1658: $\Psi$. The judgment in Figure~\ref{fig:grinst}, $\Psi \vd M\in\|
1659: N\|\hastype A $, formalizes the conditions for $M$ canonical of type
1660: $A$ to be a ground instance of a simple \emph{linear} pattern $N$ at
1661: type $A$.
1662:
1663: \begin{remark}
1664: \label{rmrk:gr}
1665: Note that $\Psi \vd M \in \|E_A\ \Phi\| \hastype a$ means that $M$ is
1666: indeed a ground instance of $E_A\ \Phi$. Conversely, if $\Phi =
1667: x_1^{k_1} \ldots x_n^{k_n}$ and $A = A_1 \GImp{k^1} \cdots
1668: A_n \GImp{k^n} a$ then we set $E_A = \lam x_1^{k_1}\oftp A_1\ldots \lam
1669: x_n^{k_n}\oftp A_n\ldot M$
1670: \end{remark}
1671:
1672: \section{The Complement Algorithm}
1673: \label{sec:compl}
1674:
1675: The idea of complementation for atomic terms and abstractions is quite
1676: simple and similar to the first-order case. For generalized variables
1677: we consider each argument in turn. If an argument variable is
1678: undetermined it does not contribute to the negation. If an argument
1679: variable is strict, then any term where this variable does not occur
1680: contributes to the negation. We therefore complement the
1681: corresponding label from $0$ to $1$ while all other arguments are
1682: undetermined. For vacuous argument variables we proceed dually.
1683:
1684: In preparation for the rules, we observe that the complement operation
1685: on patterns behaves on labels like negation does on truth-values in
1686: Kleene's three-valued logic, in the sense of the following table:.
1687: \[ \begin{array}{c}
1688: \mnot(1) = 0 \qquad
1689: \mnot(0) = 1 \qquad
1690: \mnot(u) = u
1691: \end{array} \]
1692:
1693: We extend this definition to sequences of variables as they are used to
1694: codify occurrence constraints for existential variables.
1695: \begin{eqnarray*}
1696: \mnot_i(x_{1}^{k_{1}}\ldots
1697: x_{i-1}^{k_{i-1}} \ x_{i}^{d}\ x_{i+1}^{k_{i+1}}\ldots x_n^{k_{n}})
1698: & = &
1699: x_{1}^u\ldots x_{i-1}^u \
1700: x_{i}^{\mnot(d)}\ x_{i+1}^u\ldots x_n^u
1701: \end{eqnarray*}
1702: Note that we require $x_i$ to be determined ($d \in \{0,1\}$) for
1703: $\mnot_i$ to be defined, and that variables $x_j$ for $j \not= i$ are
1704: all unrestricted on the right-hand side even though their status on
1705: the left-hand side varies.
1706:
1707: \begin{figure}
1708: \[
1709: \begin{array}{c}
1710: \ianc{\mbox{$\mnot_i(\Phi)$ defined}}
1711: {\Psi\vd \mnot(E \ \Phi) \blip Z\ \mnot_i(\Phi) \hastype a}
1712: {\mathtt{NotFlx}^i}
1713: \\[2ex]
1714: \ianc{\Psi,x\oftp A\vd \mnot(M) \blip N\hastype B}
1715: {\Psi\vd \mnot(\lam x^u\oftp A\ldot M) \blip \lam x^u\oftp A\ldot N\hastype A\TImp B}{\mathtt{NotLam}}
1716: \\[2ex]
1717: \ianc{g\in\mathrm{dom}(\Sigma\cup\Psi), g \hastype A_{1}\RImp\ldots\RImp
1718: A_{m}\RImp a, h \not= g}
1719: {\Psi\vd \mnot (h\ M_1^1\ldots M_n^1) \blip
1720: g\ (Z_{1} \ \Psi^{u})^{1}\ldots (Z_{m}\ \Psi^{u})^{1}\hastype a}
1721: {\mathtt{NotApp}_{1}}
1722: \\[2ex]
1723: \ianc{\Psi\vd \mnot( M_i) \blip N\hastype A_i}
1724: {\Psi\vd \mnot (h\ M_1^1\ldots M_n^1) \blip
1725: h\ (Z_{1}\ \Psi^{u})^{1}\ldots (Z_{i-1}\ \Psi^{u})^{1} \ N^{1}\
1726: (Z_{i+1}\ \Psi^{u})^{1}\ldots (Z_{n}\ \Psi^{u})^{1}\hastype a}
1727: {\mathtt{NotApp}_{2}^i}
1728: \end{array}
1729: \]
1730: \caption{Complement algorithm: $\Psi\vd \mnot(M) \blip N\hastype A$}
1731: \label{fig:compl}
1732: \end{figure}
1733:
1734: \begin{definition}[Higher-Order Pattern Complement]
1735: \label{def:compl}
1736: For a linear simple pattern $M$ such that $\Psi \vd M \Uparrow A$, define $\Psi
1737: \vd \mnot(M) \blip N\hastype A$ by the rules in Figure~\ref{fig:compl}, where
1738: the $Z$'s are fresh logic variables of appropriate type,
1739: $h\in\mathrm{dom}(\Sigma\cup\Psi)$ and $\Psi\vd h\hastype A_{1}\RImp\ldots\RImp
1740: A_{n}\RImp a$. We write $Z\ \Psi^u$ as an abbreviation for $Z\ \Phi$ where
1741: $\Psi; \cdot; \cdot \vd \Phi\ ok$.
1742:
1743: Note that a given $M$ may be related to several patterns $N$ all of which
1744: belong to the complement of $M$. We therefore define $\Psi\vd\mnot(M)=
1745: \cN\hastype A$ if $\cN=\{N\mid\Psi\vd \mnot(M)\blip N\hastype A\}$.
1746: \end{definition}
1747:
1748: We may drop the type information from the above judgment in examples
1749: and proofs; we will write $\Psi\vd M \in \| \mnot(N) \|\hastype A$, when
1750: $\Psi\vd\mnot(N)=\cN$ and $\Psi\vd M \in \| \cN \|\hastype A$.
1751:
1752: \begin{example} Consider the following complement problems.
1753: \begin{eqnarray}
1754: x\oftp a, y\oftp a \vd \mnot (E\ x^{u}\ y^{1}) & = & \{ F\ x^{u}\ y^{0} \}\nonumber \\
1755: x\oftp a, y\oftp a \vd \mnot(E\ x^{0}\ y^{1}) & = & \{ F\ x^{1}\ y^{u}, G\ x^{u}\ y^{0} \}
1756: \label{eq:l}
1757: \end{eqnarray}
1758: \end{example}
1759:
1760: It is worthwhile to observe that the members of a complement set are not
1761: mutually disjoint, due to the indeterminacy of $u$. We can achieve
1762: exclusive patterns if we resolve this indeterminacy by considering for
1763: every $x^{u}$ the two possibilities $x^{1},x^{0}$. Thus, for example,
1764: the right-hand side of equation (\ref{eq:l}) can be rewritten as
1765: \[ \{F \ x^{1} y^{1}, G \ x^{1} y^{0}, H \ x^{0} y^{0}\}. \]
1766: It is clear that in the worst case scenario the number of patterns in a
1767: complement set is bounded by $2^{n}$; hence the usefulness of this
1768: further step needs to be pragmatically determined.
1769:
1770: We can now revisit the example of an $\eta$-redex in the untyped
1771: $\lambda$-calculus. To avoid too many indices on existential variables,
1772: we adopt a convention that the scope of existential variables is limited
1773: to each member of a complement set.
1774:
1775: \begin{example}
1776: Reconsider Example~\ref{ex:etardx}. Then we calculate:
1777: \[ \begin{array}{rcl}
1778: \cdot & \vd & \mnot(\itlam(\lamb{x^{u}}{\itexp} \itapp\ (E\ x^{0})\ x))\\
1779: & & = \{
1780: \begin{array}[t]{@{}l}
1781: \itlam(\lamb{x^u}{\itexp} \itapp\ (Z\ x^1)\ (Z'\ x^u)),\\
1782: \itlam(\lamb{x^u}{\itexp} \itapp\ (Z\ x^u)\ (\itapp\ (Z'\ x^u) \ (Z''\ x^u)), \\
1783: \itlam(\lamb{x^u}{\itexp} \itapp\ (Z\ x^u)\ ( \itlam(\lamb{y^u}{\itexp} Z'\ x^u\ y^u)),\\
1784: \itlam(\lamb{x^u}{\itexp} \itlam(\lamb{y^u}{\itexp} Z\ x^u\ y^u) ),\\
1785: \itlam(\lamb{x^u}{\itexp}x),\\
1786: \itapp\ Z\ Z'\}
1787: \end{array}
1788: \end{array} \]
1789: \end{example}
1790:
1791: We now address the correctness of the complement algorithm with respect to the
1792: set-theoretic semantics. The proof obligation consists in proving that the
1793: former does behave as a complement operation on sets of patterns, that is, it
1794: satisfies disjointness and exhaustivity. Disjointness is the property that a
1795: set and its complement share no element; exhaustivity states that every
1796: element is in the set or its complement. Termination is obvious as the
1797: algorithm is syntax-directed and only finitely branching. We start with
1798: disjointness between a pattern and its complement.
1799:
1800: \begin{lemma}[Disjointness of Complementation]
1801: \label{le:part1}
1802: \mbox{} \newline
1803: Let $\Psi\vd N\bua A$ be a simple linear pattern. Then for every $Q$
1804: such that $\Psi\vd \mnot(N)\blip Q\hastype A$, it is not the case that
1805: both $\Psi\vd M \in \| N\|\hastype A$ and $\Psi\vd M \in \| Q\|\hastype
1806: A$.
1807: \end{lemma}
1808: \begin{proof}
1809: By induction on the structure of $\cD::\Psi\vd \mnot(N)\blip Q\hastype A$.
1810: \begin{description}
1811: \item[Case]
1812: $\cD$ ends in $\mnot\mbox{\tt Flx}^i$.
1813: \begin{tabbing}
1814: $\Psi \vd M \in \|E\ \Phi\|\hastype a$ \` Assumption \\
1815: $\Psi \vd M \in \|Z\ \mnot_i(\Phi)\|\hastype a$ \` Assumption \\[0.5ex]
1816: $\Phi(x_i) = 1$ or $\Phi(x_i) = 0$ \` Since $\mnot_i(\Phi)$ defined
1817: % $\Phi(x_i) = 1$ \` Subcase \\
1818: \end{tabbing}
1819: \begin{description}
1820: \item[Subcase] $\Phi(x_i) = 1$
1821: \begin{tabbing}
1822: $\GG; \OO; (\DD, x_i\oftp A) \vd M \hastype a$ \` By
1823: inversion on $M \in \|E\ \Phi\|$ \\
1824: $(\GG, \OO, \DD); x_i\oftp A; \cdot \vd M \hastype a$
1825: \` By inversion on $M \in \|Z\ \mnot_i(\Phi)\|$ \\
1826: $\perp$ \` By exclusivity (Lemma~\ref{le:disj})
1827: \end{tabbing}
1828: %\begin{description}
1829: \item[Subcase] $\Phi(x_i) = 0$ is symmetrical.
1830: % \begin{tabbing}
1831: % $\Phi(x_i) = 0$ \` Subcase \\
1832: % $\perp$ \` Symmetrical
1833: % \end{tabbing}
1834: \end{description}
1835: % \end{tabbing}
1836:
1837: \item[Case] $\cD$ ends in $\mathtt{NotApp}_{1}$.
1838: \begin{tabbing}
1839: $\Psi \vd M \in \|h\ N_1^1\ldots N_n^1\|\hastype a$ \` Assumption \\
1840: $\Psi \vd M \in \|g\ (Z_1\ \Psi^u)^1\ldots (Z_m\ \Psi^u)^1\|\hastype a$ for $g\not= h$
1841: \` Assumption \\
1842: $M = h \cdots$ \` By inversion on \texttt{grApp} \\
1843: $M = g \cdots$ \` By inversion on \texttt{grApp} \\
1844: $\perp$ \` Since $g\neq h$
1845: \end{tabbing}
1846:
1847: \item[Case] $\cD$ ends in $\mathtt{NotApp}_{2}^i$.
1848: \begin{tabbing}
1849: $\Psi \vd M \in \|h\ N_1^1\ldots N_n^1\|\hastype a$ \` Assumption \\
1850: $\Psi \vd M \in \|h\ (Z_1\ \Psi^u)^1\ldots (Z_{i-1}\ \Psi^u)^1 \ Q^{1}\
1851: (Z_{i+1}\ \Psi^u)^1\ldots (Z_n\ \Psi^u)^1\| \hastype a$ and \\
1852: $\Psi \vd \mnot(N_i) \blip Q \hastype A_i$ \` Assumption \\
1853: $M = h\ M_1\ldots M_n$ and \\
1854: $\Psi \vd M_i \in \|N_i\| \hastype A_i$ \` By inversion \\
1855: $\Psi \vd M_i \in \|Q\| \hastype A_i$ \` By inversion \\
1856: $\perp$ \` By i.h.
1857: \end{tabbing}
1858:
1859: \item[Case] $\cD$ ends in $\mathtt{NotLam}$.
1860: \begin{tabbing}
1861: $\Psi\vd \mnot(\lxua N) \blip \lxua Q\hastype A\TImp B$ \` This case \\
1862: $\Psi,x\oftp A\vd \mnot( N) \blip Q\hastype B$ \` Subderivation \\
1863: $\Psi \vd \lxua M\in \| \lxua N\|\hastype A\TImp B$ \` Assumption \\
1864: $\Psi \vd \lxua M\in \| \lxua Q\|\hastype A\TImp B$ \` Assumption \\
1865: $\Psi,x\oftp A \vd M\in \| N\|\hastype B$\` By inversion \\
1866: $\Psi,x\oftp A \vd M\in \| Q\|\hastype B$\` By inversion \\
1867: $\perp$\` By i.h.
1868: \end{tabbing}
1869: \end{description}
1870: \end{proof}
1871:
1872: Note that disjointness is based on exclusivity (Lemma~\ref{le:disj}), which
1873: holds for \emph{any} strict term---it does not require simple terms.
1874: Next, we turn to the other direction. First a lemma concerning
1875: the special case of generalized variables.
1876:
1877: \begin{lemma}[Exhaustivity for Flexible Patterns]
1878: \label{le:exhflex}
1879: \mbox{} \newline
1880: For every closed $M$ such that $\Psi \vd M \bua a$,
1881: either $\Psi \vd M\in \| E_A\ \Phi \| \hastype a$ or
1882: $\Psi \vd M\in \| Z\ \mnot_i(\Phi)\| \hastype a$ for some $i$.
1883: \end{lemma}
1884: \begin{proof}
1885: Assume $\Psi \vd M\bua a$. Then by iterated applications of
1886: Lemma~\ref{le:exh} there exist $\OO$ and $\DD$ such that
1887: $\Psi=\OO,\DD$ and $\cdot;\OO;\DD\vd M\bua a$.
1888: \begin{description}
1889: \item[Case]
1890: For every $x\in\dom(\OO)$ we have $\Phi(x)\in\{0,u\}$
1891: and for every $x \in \dom(\DD)$ we have $\Phi(x)\in\{1,u\}$.
1892: Then $\Psi\vd M\in\| E\ \Phi\|$.
1893: \item[Case]
1894: For some $x_i\in\dom(\OO)$ we have $\Phi(x_i) = 1$. \newline
1895: Then $\Psi \vd M\in\|Z\ x_{1}^{u}\ldots x_{i-1}^{u}\
1896: x_{i}^{1}\ x_{i+1}^{u}\ldots x_n^{u} \|$ and therefore $\Psi\vd
1897: M\in\|Z\ \mnot_i(\Phi)\|$.
1898: \item[Case] For some $x_i \in\dom(\DD)$ we have $\Phi(x_i) = 0$. \newline
1899: Then $\Psi \vd M\in\|Z\ x_{1}^{u}\ldots x_{i-1}^{u}\
1900: x_{i}^{0}\ x_{i+1}^{u}\ldots x_n^{u} \|$ and therefore $\Psi\vd
1901: M\in\|Z\ \mnot_i(\Phi)\|$.
1902: \end{description}
1903: \end{proof}
1904:
1905: We are now ready to prove exhaustivity of complementation.
1906:
1907: \begin{lemma}[Exhaustivity of Complementation] \mbox{} \newline
1908: \label{le:part2}
1909: Assume $\Psi\vd N\bua A$ is a simple linear pattern. Then for every
1910: closed $M$ such that $\Psi \vd M \bua A$, either $\Psi \vd M\in \| N \|
1911: \hastype A$ or there is a $Q$ such that $\Psi\vd \mnot(N)\blip Q\hastype
1912: A$ and $ \Psi \vd M\in \| Q\| \hastype A$.
1913: \end{lemma}
1914: \begin{proof}
1915: By induction on the structure of $\cD::\Psi \vd N\bua A$.
1916: \begin{description}
1917: \item[Case] $\cD$ ends in \texttt{cPat}. Then the claim
1918: follows immediately by Lemma~\ref{le:exhflex}.
1919:
1920: \item[Case] $\cD$ ends in $\mathtt{c}\TImp I$. The i.h.\ yields the
1921: two sub-cases.
1922: \begin{description}
1923: \item[Subcase] $\Psi,x\oftp A \vd M\in \| N\| \hastype B$.
1924: \begin{tabbing}
1925: $\Psi\vd\lxua M\in\|\lxua N\|\hastype A\TImp B$\` By rule \texttt{grLam}
1926: \end{tabbing}
1927: \item[Subcase] $\Psi,x\oftp A\vd\mnot(N)\blip Q\hastype B$ and
1928: $\Psi,x\oftp A \vd M\in \| Q\| \hastype B$ for some $Q$.
1929: \begin{tabbing}
1930: $\Psi\vd\mnot(\lxua N)\blip\lxua Q \hastype A\TImp B$
1931: \` By rule $\mathtt{NotLam}$ \\
1932: $\Psi\vd\lxua M\in\|\lxua Q\|\hastype A\TImp B$ \` By rule \texttt{grLam}
1933: \end{tabbing}
1934: \end{description}
1935:
1936: \item[Case]
1937: \[ \cD=\ianc{\Psi \vd h\hastype A_1\RImp\cdots\RImp A_n\RImp a \quad
1938: \Psi \vd N_1\bua A_1 \quad \cdots \quad \Psi \vd N_n \bua A_n}
1939: {\Psi \vd h\ N_1^1\ldots N_{n}^1 \bua a}
1940: {\mathtt{c}{\RImp}E} \]
1941: First, assume $M = g\ M_1^1\ldots M_m^1$, for
1942: $g\in\mathrm{dom}(\Sigma\cup\Psi)$, $h \not= g $. Then
1943: \begin{tabbing}
1944: $\Psi\vd \mnot (h\ N_1^1\ldots N_n^1) \blip
1945: g\ (Z_{1} \ \Psi^{u})^{1}\ldots (Z_{m}\ \Psi^{u})^{1}\hastype a$
1946: \` By rule $\mathtt{NotApp}_1$ \\
1947: $\Psi\vd M_{i}\in\|Z_{i}\ \Psi^{u}\|\hastype A_i$ for all
1948: $1\leq i\leq m$
1949: \` By rule \texttt{grFlx} \\
1950: $\Psi\vd g\ M_1^1\ldots M_m^1 \in \|g\ (Z_{1}\ \Psi^{u})^{1}\ldots
1951: (Z_{n}\ \Psi^{u})^{1}\|\hastype a$
1952: \` By rule \texttt{grApp}
1953: \end{tabbing}
1954: Otherwise, assume $M = h\ M_1^1\ldots M_n^1$. Again, the i.h.\ yields
1955: two sub-cases.
1956: \begin{description}
1957: \item[Subcase] $\Psi\vd M_i\in\|N_i\| \hastype A_i$, for all $1\leq i\leq n$.
1958: \begin{tabbing}
1959: $\Psi \vd h\ M_1^1\ldots M_n^1\in\|h\ N_1^1\ldots N_n^1\|\hastype
1960: a$
1961: \` By rule \texttt{grApp}
1962: \end{tabbing}
1963: \item[Subcase]
1964: $\Psi\vd\mnot(N_{i}) \blip Q\hastype A_i$ and
1965: $\Psi \vd M_{i}\in \| Q\| \hastype A_i$, for some $Q$.
1966: \begin{tabbing}
1967: $\Psi\vd M_{j}\in\|Z_{j}\ \Psi^{u}
1968: \|\hastype A_j$ for all $j\not= i$, $1\leq j\leq n$
1969: \` By rule \texttt{grFlx} \\
1970: $\Psi\vd \mnot (h\ M_1^1\ldots M_n^1)$ \\
1971: $\qquad \blip
1972: h\ (Z_{1}\ \Psi^{u})^{1}\ldots (Z_{i-1}\ \Psi^{u} )^{1} \ Q^{1}\
1973: (Z_{i+1}\ \Psi^{u} )^{1}\ldots (Z_{n}\ \Psi^{u})^{1}\hastype a$ % \\
1974: \` By rule $\mathtt{NotApp}_2^i$ \\
1975: $\Psi \vd h\ M_1^1\ldots M_n^1\in \| h\ (Z_{1}\ \Psi^{u} )^{1}\ldots (Z_{i-1}\
1976: \Psi^{u})^{1}\ Q^{1}\ (Z_{i+1}\ \Psi^{u} )^{1}\ldots (Z_{m}\ \Psi^{u}
1977: )^{1} \| \hastype a$ \\
1978: \` By rule \texttt{grApp}.
1979: \end{tabbing}
1980: \end{description}
1981: \end{description}
1982: \end{proof}
1983:
1984: The correctness of the algorithm for pattern complement follows
1985: directly from the preceding two lemmas.
1986:
1987: \begin{theorem}[Correctness of Pattern Complement]
1988: \label{thm:compl}
1989: \mbox{} \newline Assume $N$ is a simple linear pattern such that $\Psi
1990: \vd N \hastype A$. Then for every closed $M$ with $\Psi \vd M \bua A$,
1991: $\Psi \vd M \in \|\mnot(N)\| \hastype A$ iff $\Psi \not\vd M \in
1992: \|N\|$.
1993: \end{theorem}
1994:
1995: It is easy to see that simple linear patterns are closed under complementation.
1996:
1997: \begin{theorem}[Closure under Complementation]
1998: Assume $M$ is a simple linear pattern with $\Psi \vd M \Uparrow A$.
1999: Then $\Psi\vd\mnot(M)\blip N\hastype A$ implies $N$ is a simple
2000: linear pattern and $\Psi \vd N \Uparrow A$.
2001: \end{theorem}
2002: \begin{proof}
2003: By induction on the structure of the derivation of
2004: $\Psi\vd\mnot(M)\blip N\hastype A$.
2005: \end{proof}
2006:
2007: % \input{unif}
2008:
2009: \section{Unification of Simple Patterns}
2010: \label{sec:sunif}
2011:
2012: As we observed earlier, we can solve a relative complement problem by
2013: pairing complementation with intersection. We therefore address the
2014: task of giving an algorithm for unification of linear simple patterns.
2015: We start by determining when two labels are compatible:
2016: \begin{eqnarray*}
2017: 1 \cap 1 = u \cap 1 = 1\cap u = 1\\
2018: 0 \cap 0 = u \cap 0 = 0\cap u = 0\\
2019: u\cap u = u
2020: \end{eqnarray*}
2021:
2022: Recall that $\Phi$ is a list of labelled bound variables. We call
2023: $\Phi_1$ and $\Phi_2$ \emph{compatible} if they contain the same
2024: variables in the same order, but with possibly different labels. We can
2025: extend the intersection operations to compatible lists.
2026: \begin{eqnarray*}
2027: \cdot\cap \cdot & = & \cdot\\
2028: ( \Phi, x^k)\cap ( \Phi', x^{k'}) & = & (\Phi\cap \Phi', x^{k\cap
2029: k'}) \quad\mbox{\textrm{if $k\cap k'$ is defined.}}
2030: \end{eqnarray*}
2031:
2032: For contexts $\GG_1$ and $\GG_2$ that may have variable declarations
2033: in common, we write $\GG_1 \cap \GG_2$ and $\GG_1 \cup \GG_2$ for
2034: set-theoretic union and intersection. In both cases we assume
2035: that a variable $x$ declared in both $\GG_1$ and $\GG_2$ must be
2036: assigned the same type in both contexts.
2037:
2038:
2039: \begin{remark}
2040: \label{rmk:compa}
2041: Assume $\Phi_1$ and $\Phi_2$ are compatible and $\Phi_1 \cap \Phi_2$
2042: is defined. Then $\GG_1;\OO_1;\DD_1\vd\Phi_1\
2043: ok$ and $\GG_2;\OO_2;\DD_2\vd\Phi_2\ ok$ implies
2044: that $\DD_1 \cap \OO_2 = \DD_2 \cap \OO_1 = \emptyset$.
2045: Moreover,
2046: $(\GG_1\cap\GG_2);(\OO_1\cup\OO_2);(\DD_1\cup\DD_2)\vd (\Phi_1\cap\Phi_2) \ ok$.
2047: From that it follows that $\Psi\vd M\in
2048: \|E_{A}\ (\Phi_{1}\cap\Phi_{2})\| \hastype a$ iff
2049: $(\GG_1\cap\GG_2);(\OO_1\cup \OO_2);(\DD_1 \cup \DD_2)\vd M\hastype a$.
2050: \end{remark}
2051:
2052: \begin{figure}
2053: \[
2054: \begin{array}{c}
2055: \ianc{}
2056: {\Psi\vd (E_1 \ \Phi_1)\cap (E_2\ \Phi_2)\blip H\ (\Phi_{1}\cap \Phi_{2}) \hastype a}
2057: {\cap \mathtt{FF}}
2058: \\[2ex]
2059: \mbox{\textrm{no rule for flex/flex same}}
2060: \\[2ex]
2061: \ianc{c\in\mathrm{dom}(\Sigma)\quad \Psi\vd (H_1 \ \Phi_{1}) \cap
2062: M_{1}\blip N_{1}\hastype A_{1}\cdots \Psi\vd (H_n \ \Phi_{n})\cap
2063: M_{n}\blip N_{n}\hastype A_{n} }
2064: { \Psi\vd (E \ \Phi) \cap (c\ M_1^1\ldots M_n^1)\blip c\ N_1^1\ldots N_n^1\hastype a} {\cap
2065: \mathtt{FR}^c }
2066: \\[2ex]
2067: \ianc{y\in\mathrm{dom}(\Psi)\quad \quad \Psi\vd (H_1 \ \Phi_{1})\cap
2068: M_{1}\blip N_{1}\hastype A_{1}\cdots \Psi\vd (H_n \ \Phi_{n})\cap
2069: M_{n}\blip N_{n}\hastype A_{n} }
2070: {\Psi\vd (E\ \Phi) \cap (y\ M_1^1\ldots M_n^1)\blip y\ N_1^1\ldots N_n^1 \hastype a} {\cap \mathtt{FR}^y }
2071: \\[2ex]
2072: \ianc{ h\in\mathrm{dom}(\Psi\cup\Sigma)\quad \Psi\vd M_1 \cap N_{1} \blip
2073: Q_1\hastype A_1 \cdots \Psi\vd M_n \cap N_{n}\blip Q_n \hastype A_n}
2074: {\Psi\vd (h\ M_1^1\ldots M_n^1)\cap (h\ N_1^1\ldots N_n^1) \blip h\
2075: Q_1^1\ldots Q_n^n \hastype a}
2076: {\cap \mathtt{RR}}
2077: \\[2ex]
2078: \ianc{\Psi,x\oftp A\vd M \cap N \blip Q\hastype B}
2079: {\Psi\vd ( \lxua M ) \cap (\lxua) N \blip \lxua Q \hastype A\TImp B}{\cap \mathtt{L}}
2080: \end{array}
2081: \]
2082: \caption{Unification algorithm: $\Psi\vd M \cap N \blip Q \hastype A$}
2083: \label{fig:unif}
2084: \end{figure}
2085:
2086: \begin{definition}[Higher-Order Pattern Intersection]
2087: Assume $M$ and $N$ are linear simple patterns without shared existential
2088: variables such that $\Psi \vd M \Uparrow A$ and $\Psi \vd N\Uparrow A$. We
2089: define $\Psi\vd M \cap N \blip Q \hastype A$ by the rules in
2090: Figure~\ref{fig:unif}, where the $H$'s are fresh variables of appropriate
2091: type. We omit two rules, $\cap \mathtt{RF}^c$ and $\cap \mathtt{RF}^y$, that
2092: are symmetric to $\cap \mathtt{FR}^c$ and $\cap \mathtt{FR}^y$.
2093:
2094: The rules $\cap \mathtt{FR}^c$ and $\cap\mathtt{RF}^c$ have the
2095: following proviso: for all $1 \leq i \leq n$, $\dom(\Phi_i) =
2096: \dom(\Phi)$ and
2097: \begin{eqnarray*}
2098: \forall x. \Phi(x) = 0 \Imp \forall i\ldot \Phi_{i}(x) = 0\\
2099: \forall x. \Phi(x) = u \Imp \forall i\ldot \Phi_{i}(x) = u\\
2100: \forall x. \Phi(x) = 1 \Imp \exists i\ldot \Phi_{i}(x) = 1
2101: \And \forall j\ldot j\not = i \Imp \Phi_{j}(x) = u
2102: \end{eqnarray*}
2103: The rules $\cap \mathtt{FR}^y$ and $\cap RF^y$ are subject to the
2104: proviso:
2105: \begin{eqnarray*}
2106: \forall x. \Phi(x) = 0 \Imp \forall i\ldot \Phi_{i}(x) = 0\\
2107: \forall x. \Phi(x) = u \Imp \forall i\ldot \Phi_{i}(x) = u\\
2108: \forall x. x \not= y \And \Phi(x) = 1 \Imp \exists i\ldot \Phi_{i}(x) = 1
2109: \And \forall j\ldot j\not = i \Imp \Phi_{j}(x) = u \\
2110: \Phi(y)=1 \Imp \forall i. \Phi_{i}(y) = u
2111: \end{eqnarray*}
2112: Finally define $\Psi \vd M \cap N = {\cal Q} \hastype A$ if ${\cal Q}=
2113: \{Q\mid\Psi\vd M\cap N \blip Q \hastype A\}$.
2114: \end{definition}
2115:
2116: Some remarks are in order:
2117: \begin{itemize}
2118: \item In rule $\cap \mathtt{FF}$ we can assume $\Phi_1$ and $\Phi_2$
2119: are compatible lists of variables, since generalized variables
2120: are fully applied and their arguments are in a standard order.
2121: \item Since patterns are linear and $M$ and $N$ share no pattern
2122: variables, the flex/flex case arises only with distinct variables. This
2123: also means we do not have to apply substitutions or perform the
2124: customary occurs-check.
2125: \item In the flex/rigid and rigid/flex rules, the proviso enforces the
2126: typing discipline since each strict variable $x$ must be strict in some
2127: premise. If instead $y$ is the projected variable, the modified
2128: condition on $y$ takes into account that the head of an application
2129: constitutes a strict occurrence; moreover, since $y$ did occur, it is
2130: set to $u$ in the rest of the computation, as there are no more
2131: requirements on that variable.
2132: \item The symmetric rules take the place of an explicit exchange rule
2133: that is problematic with respect to termination.
2134: \end{itemize}
2135:
2136: The following example illustrates how the flex/rigid rules, in this
2137: case $\cap \mathtt{FR}^c$, make unification on simple patterns finitary.
2138: We describe a \emph{unification problem} by omitting
2139: the eventually computed solution as $\Psi \vd M \cap N \hastype A$.
2140:
2141: \begin{example}
2142: Consider the unification problem
2143: \[ x\oftp a\vd E\ x^{1} \cap c\ (F\ x^{u})^{1} \ (F'\ x^{u})^{1}\hastype a \]
2144: Since $x$ is strict in the left-hand side, there are two ways to
2145: apply the $\cap \mathtt{FR}^c$ rule, leading to the following subproblems:
2146: \[
2147: \begin{array}{rlrr}
2148: 1. &x\oftp a\vd E' \ x^{1}\cap\ F\ x^{u} \hastype a
2149: & & x\oftp a\vd E''\ x^{u}\cap\ F'\ x^{u} \hastype a
2150: \\
2151: 2. & x\oftp a\vd E' \ x^{u}\cap\ F\ x^{u} \hastype a
2152: & & x\oftp a\vd E''\ x^{1}\cap\ F'\ x^{u} \hastype a
2153: \end{array}
2154: \]
2155: Hence the result:
2156: \begin{eqnarray*}
2157: %\label{eq:int}
2158: x\oftp A\vd E\ x^{1} \cap c\ (F\ x^{u})^{1} \ (F'\
2159: x^{u})^{1}= \{c\ (H\ x^{1})^{1} \ (H'\ x^{u})^1,c\ (H\ x^{u})^1 \ (H'\
2160: x^{1})^1\}
2161: \end{eqnarray*}
2162: \end{example}
2163:
2164: Note that, similarly to complementation, intersection returns
2165: a set of patterns with common terms; again it is possible, in a
2166: post-processing phase to make the result exclusive.
2167:
2168: The following example illustrates the additional proviso on
2169: $\cap \mathtt{FR}^{y}$
2170: \begin{example}
2171: The unification problem
2172: \[ y\oftp a \RImp a \RImp a \vd E\ y^{0} \cap y\ (F\
2173: y^{1})^1 \ (F'\ y^{u})^1 \hastype a \]
2174: has no solution, whereas
2175: \[ y\oftp a \RImp a \RImp a
2176: \vd E\ y^1 \cap y\ (F\ y^1)^1 \ (F'\ y^{0})^1 = \{y \ (H\ y^1)^1 \
2177: (H'\ y^{0})^1\} \hastype a \]
2178: \end{example}
2179:
2180: This first lemma will be needed to handle the case for unification
2181: of generalized variables.
2182:
2183: \begin{lemma}
2184: \label{le:flexunif}
2185: Assume $\Phi_1$ and $\Phi_2$ are compatible and $\Phi_1 \cap \Phi_2$
2186: is defined. Assume furthermore that $\GG_1;\OO_1;\DD_1\vd\Phi_1\
2187: ok$ and $\GG_2;\OO_2;\DD_2\vd\Phi_2\ ok$.
2188: Then $\GG_1; \OO_1; \DD_1 \vd M\hastype A$ and $\GG_2; \OO_2; \DD_2 \vd M\hastype A$ iff $(\GG_{1}\cap\GG_{2});(\OO_{1}\cup\OO_{2});(\DD_{1}\cup\DD_{2}) \vd
2189: M\hastype A$.
2190: \end{lemma}
2191: \begin{proof}
2192: From left to right by induction on the size of $(\GG_1\cup\GG_2)\setminus
2193: (\GG_1\cap\GG_2)$, using tightening (Lemma~\ref{le:exh}). From right to
2194: left by appropriate appeals to loosening (Lemma~\ref{thm:loosex}).
2195: \end{proof}
2196:
2197: We introduce two $n$-ary strict application rules which, for the
2198: special case of simple terms, capture the notion of atomic forms more
2199: compactly than the previous definition. The rules differ only in
2200: whether the head $h$ of the atomic term is a strict variable or
2201: unrestricted. These will be needed in the proof of Lemma~\ref{le:unif2}
2202: and Lemma~\ref{le:unif1}.
2203:
2204: \begin{eqnarray*}
2205: \ianc{(\GG,\DD^{u}_{i});\OO;\DD_i^1 \vd M_{i}\hastype A_{i} \quad
2206: 1\leq i\leq n}
2207: {\GG;\OO;\DD \vd h\ M_1^1\ldots M_{n}^1\hastype B}
2208: {{\RImp}E^{u}}
2209: \end{eqnarray*}
2210: where $h\ \hastype A_1\RImp\ldots\RImp A_{n}\RImp b$ in $\dom(\GG\cup\Sigma)$
2211: and
2212: \begin{enumerate}
2213: \item $\forall x\in\dom(\DD)\ldot \exists\mbox{!} i:1\leq i\leq n \ldot
2214: x\in\dom(\DD_{i}^1)$.
2215: \item $\forall i:1\leq i\leq n\ldot (\DD_{i}^{u},\DD_{i}^1)=\DD$.
2216: \end{enumerate}
2217:
2218: %proj rule
2219: \begin{eqnarray*}
2220: \ianc{(\GG,\DD^{u}_{i});\OO;\DD_i^1 \vd M_{i}\hastype A_{i}\quad
2221: 1\leq i\leq n}{\GG;\OO; \DD\vd y\ M_1^1\ldots M_{n}^1\hastype
2222: B}{{\RImp}E^{1}}
2223: \end{eqnarray*}
2224: where $y \hastype A_1\RImp\ldots\RImp A_{n}\RImp b \in \dom(\DD)$
2225: and
2226: \begin{enumerate}
2227: \item $\forall x\in\dom(\DD), x\not= y\ldot\exists\mbox{!} i:1\leq i\leq n
2228: \ldot x\in\dom(\DD_{i}^1)$.
2229: \item $\forall i:1\leq i\leq n \ldot(\DD_{i}^{u},\DD_{i}^1)=\DD$.
2230: \item $\forall i:1\leq i\leq n \ldot y\in\dom(\DD_i^u)$.
2231: \end{enumerate}
2232:
2233: It is straightforward, but tedious to show that these rules can replace
2234: the rules for atomic terms. The curious reader is invited to
2235: consult~\cite{Momigliano00phd} for details.
2236:
2237: We are now ready to address correctness of unification.
2238: First we show that our algorithm only computes unifiers, then that
2239: the set of unifiers we compute is most general.
2240:
2241: \begin{lemma}[Intersection Computes Unifiers]
2242: \label{le:unif2}
2243: \mbox \newline
2244: For any simple linear pattern $N_1$ and $N_2$ without shared variables
2245: such that $\Psi \vd N_1 \Uparrow A$ and $\Psi \vd N_2 \Uparrow A$, for
2246: every $N$ such that $\Psi\vd N_1\cap N_{2}\blip N$ if $\Psi\vd
2247: M\in\|N\|\hastype A$, then $ \Psi\vd M\in\|N_1\|\hastype A$ and
2248: $\Psi\vd M\in\|N_{2}\|\hastype A$.
2249: \end{lemma}
2250: \begin{proof}
2251: By induction on the structure of $\cD::\Psi\vd N_1\cap N_{2}\blip N$
2252: and inversion on $\cD'::\Psi\vd M\in\|N\|\hastype A$. We show only
2253: some of the cases; the others are analogous.
2254: \begin{description}
2255: \item[Case] $\cD$ ends in $\cap \mathtt{FF}$:
2256: \begin{tabbing}
2257: ${\Psi\vd (E_1 \ \Phi_1)\cap (E_2\ \Phi_2)\blip H\ (\Phi_{1}\cap
2258: \Phi_{2}) \hastype a} $ \` Assumption \\
2259: $\Psi\vd M\in \| H\ (\Phi_{1}\cap \Phi_{2})\| \hastype a$
2260: \` Assumption \\
2261: $\GG_i;\OO_i;\DD_i\vd\Phi_i\ ok$ for $i=1,2$ for some $\GG_i$, $\OO_i$,
2262: $\DD_i$
2263: \` Determined from $\Phi_i$ \\
2264: $(\GG_{1}\cap\GG_{2});(\OO_{1}\cup\OO_{2});(\DD_{1}\cup\DD_{2})
2265: \vd\Phi_1\cap\Phi_2\ ok$\` By Remark~\ref{rmk:compa} \\
2266: $\GG_i;\OO_i;\DD_i\vd M \hastype a$
2267: \` By Lemma~\ref{le:flexunif} ($\leftarrow$)\\
2268: $\Psi\vd M\in\|N_i\|\hastype a$ \` By rule \texttt{grFlx}
2269: \end{tabbing}
2270: \item[Case] $\cD$ ends in $\cap \mathtt{FR}^c $.
2271: \begin{tabbing}
2272: $\cD::\Psi\vd (E\ \Phi)\cap (c\ Q_1^1\ldots Q_{n}^1)
2273: \blip c\ N_1^1\ldots N_n^1\hastype a$
2274: \` Assumption \\
2275: $\cD_i::\Psi\vd (E\ \Phi_i)\cap Q_i \blip N_i\hastype A_i,$ for all $ 1\leq i\leq n$
2276: \` Subderivations \\
2277: $\Psi\vd c\ M_1^1\ldots M_n^1\in\|c\ N_1^1\ldots N_n^1\|\hastype a$ \` Assumption \\
2278: $\Psi\vd M_i\in\|N_i\|\hastype A_i$ \` By inversion \\
2279: $\Psi\vd M_{i}\in\|Q_{i}\|\hastype A_i$ and $\Psi\vd M_{i}\in\|E_{i}\
2280: \Phi_{i}\|\hastype A_i$
2281: \` By i.h.\ on $\cD_i$ \\
2282: $(\GG_{i},\DD^u_i);\OO;\DD^1_i\vd \Phi_i\ ok$ and $(\GG_{i},\DD^u_i);\OO;\DD^1_i\vd M_{i}\hastype A_{i}$
2283: \` By rule \texttt{grFlx} \\
2284: $\god\vd c\ M_1^1\ldots M_n^1\hastype a$ \` By rule ${\RImp}E^{u}$ \\
2285: $\Psi\vd c\ M_1^1\ldots M_n^1\in\|E\ \Phi\|\hastype a$
2286: \` By rule \texttt{grFlx} \\
2287: $\Psi\vd c\ M_1^1\ldots M_n^1\in\|c\ Q_1^1\ldots Q_n^1\| \hastype a$
2288: \` By rule \texttt{grApp}
2289: \end{tabbing}
2290: \end{description}
2291: \end{proof}
2292:
2293: The second part consists of showing that any unifier of two patterns
2294: is an instance of an element from the computed set of unifiers.
2295:
2296: \begin{lemma}[Intersections are Most General]
2297: \label{le:unif1}
2298: For any simple linear patterns $N_1$ and $N_2$ without shared variables such
2299: that $\Psi \vd N_1 \bua A$ and $\Psi \vd N_2 \bua A$, if $\Psi\vd
2300: M\in\|N_1\|\hastype A$ and $\Psi\vd M\in\|N_{2}\|\hastype A$, then there is
2301: $N$ such that $\Psi\vd N_1\cap N_{2}\blip N\hastype A$ and $\Psi\vd
2302: M\in\|N\|\hastype A$.
2303: \end{lemma}
2304: \begin{proof}
2305: By simultaneous induction on the structure
2306: of $\cD_1::\Psi \vd M\in\|N_1\| \hastype A$ and $\cD_2::\Psi \vd
2307: M\in\| N_2\| \hastype A$.
2308: \begin{description}
2309: \item[Case] $\cD_1,\cD_2$ end in \texttt{grFlx}:
2310: \begin{tabbing}
2311: $\GG_i;\OO_i;\DD_i\vd\Phi_i\ ok$ and $\GG_i;\OO_i;\DD_i\vd M \hastype a$
2312: for $i=1,2$ \` Subderivations \\
2313: $\Phi_1 \cap \Phi_2$ is defined \` By exclusivity (Lemma~\ref{le:disj}) \\
2314: $\Psi\vd (E_1 \ \Phi_1)\cap (E_2\ \Phi_2)\blip H\ (\Phi_{1}\cap
2315: \Phi_{2}) \hastype a$ \` By rule $\cap\mathtt{FF}$ \\
2316: $(\GG_{1}\cap\GG_{2});(\OO_{1}\cup\OO_{2});(\DD_{1}\cup\DD_{2})\vd M\hastype a$\` By Lemma~\ref{le:flexunif}($\arrow$)\\
2317: $(\GG_{1}\cap\GG_{2});(\OO_{1}\cup\OO_{2});(\DD_{1}\cup\DD_{2})\vd\Phi_1\cap\Phi_2\ ok$\` By Remark~\ref{rmk:compa} \\
2318: % $\Psi\vd M\in\|E_i\ \Phi_i\|\hastype a$ for $1\leq i\leq 2$\bh
2319: $\Psi\vd M\in \| H\ (\Phi_{1}\cap \Phi_{2})\| \hastype a$
2320: \` By rule \texttt{grFlx}
2321: \end{tabbing}
2322: \item[Case]
2323: $\cD_1$ ends in \texttt{grFlx} and $\cD_2$ ends in \texttt{grApp}: there are
2324: two cases depending on whether the head of $N_2$ is a constant or a parameter.
2325: \begin{description}
2326: \item[Subcase] The head of $N_2$ is a constant $c$.
2327: \begin{tabbing}
2328: $\Psi\vd M \in \|c\ Q_1^1\ldots Q_n^1\| \hastype a$ \` Assumption \\
2329: $M = c\ M_1^1\ldots M_n^1$ and $\cD^2_i::\Psi\vd M_{i}\in\|Q_{i}\|\hastype A_i$ for
2330: all $1\leq i\leq n$ \` Subderivation \\
2331: $\Psi\vd c\ M_1^1\ldots M_n^1\in\|E\ \Phi\|\hastype a$ \` Assumption \\
2332: $\god\vd c\ M_1^1\ldots M_n^1 \hastype a$ and $\god\vd\Phi\ ok$
2333: \` By inversion on rule \texttt{grFlx}\\
2334: $(\GG,\DD^u_i);\OO;\DD^1_i\vd M_{i}\hastype A_{i}$ for some
2335: $\DD^u_i,\DD^u_i$ satisfying $(1)$ and $(2)$ \\
2336: \` By inversion on rule ${\RImp}E^u$ \\
2337: $\cD^1_i::\Psi\vd M_{i}\in\|E_{i}\ \Phi_{i}\|\hastype A_i$
2338: for $\Phi_i$ such that $(\GG,\DD^u_i);\OO;\DD^1_i\vd\Phi_i \ ok$\\
2339: \` By rule \texttt{grFlx} \\
2340: $\cD_i::\Psi\vd (E_{i}\ \Phi_i)\cap Q_i \blip N_i\hastype A_i$ and
2341: $\Psi\vd M_{i}\in\|N_{i}\|\hastype A_i$
2342: \` By i.h.\ on $\cD_i^1,\cD_i^2$ \\
2343: $\cD::\Psi\vd (E\ \Phi)\cap (c\ Q_1^1\ldots Q_n^1) \blip c\
2344: N_1^1\ldots N_n^1 \hastype a$
2345: \` By rule $\cap \mathtt{FR}^c$\\
2346: $\Psi\vd c\ M_1^1\ldots M_n^1\in\|c\ N_1^1\ldots N_n^n\|\hastype a$
2347: \` By rule \texttt{grApp}
2348: \end{tabbing}
2349: \item[Subcase] Proceed as above, but using inversion
2350: on rule ${\RImp}E^{1}$ % \ie Corollary~\ref{co:derivey}.
2351: \end{description}
2352: \item[Case] $\cD_2$ ends in \texttt{grFlx} and $\cD_1$ ends in \texttt{grApp}:
2353: symmetrical to the above.
2354: \item[Case] $\cD_1,\cD_2$ end in \texttt{grLam}: straightforward
2355: by induction hypothesis.
2356: \item[Case] $\cD_1,\cD_2$ end in \texttt{grApp}: a straightforward appeal to
2357: the induction hypothesis as in the above case.
2358: \end{description}
2359: \end{proof}
2360:
2361: The correctness of the algorithm for pattern intersection follows
2362: directly from the preceding two lemmas.
2363:
2364: \begin{theorem}[Correctness of Pattern Intersection]
2365: \label{thm:unif} \mbox{} \newline
2366: Assume $N_1$ and $N_2$ are simple linear patterns without shared variables
2367: such that $\Psi \vd N_1 \Uparrow A$ and $\Psi \vd N_2 \Uparrow A$. Then $\Psi\vd
2368: M\in\|N_1\|\hastype A$ and $\Psi\vd M\in\|N_{2}\|\hastype A$ iff $\Psi\vd
2369: M\in\|N_1 \cap N_2\|\hastype A$.
2370: \end{theorem}
2371:
2372: Also note that the intersection of linear simple patterns is again
2373: a simple linear pattern.
2374:
2375: \begin{theorem}[Closure under Intersection]
2376: Assume $M$ and $N$ are simple linear patterns with $\Psi \vd
2377: M \Uparrow A$ and $\Psi \vd N \Uparrow A$. Then $\Psi \vd M \cap N \blip
2378: Q \hastype A$ implies that $Q$ is a simple linear pattern
2379: and $\Psi \vd Q \Uparrow A$.
2380: \end{theorem}
2381: \begin{proof}
2382: By induction on the structure of the derivation of $\Psi \vd M \cap N
2383: \blip Q \hastype A$.
2384: \end{proof}
2385:
2386: \section{The Algebra of Linear Simple Patterns}
2387: \label{sec:algebra}
2388:
2389: An interesting and natural question is whether complementation is
2390: involutive. The answer is of course positive, since the latter is a
2391: boolean property and the complement operation has been shown to satisfy
2392: ``tertium non datur'' and the principle of non-contradiction. However,
2393: the reader should keep in mind that the \emph{representation} of the set
2394: $\mnot(\mnot(N))$ may be different from $\{N\}$, even though the two
2395: sets are guaranteed to have the same set of ground instances. Since on
2396: finite set of patterns we also have intersection and set-theoretic
2397: union, we obtain a boolean algebra. For the sake of readability, we
2398: introduce the following notation: $\Pat$ denotes the finite set of
2399: linear simple patterns $M$ with $\Psi \vd M \hastype A$. In the
2400: following, we also drop the type information and overload the singleton
2401: pattern notation.
2402:
2403: \begin{definition}
2404: \label{def:setop} For
2405: $\cM,\cN \in \Pat$, define:
2406: \begin{eqnarray*}
2407: \cM \cap \cN & = & \bigcup_{M\in\cM,N\in\cN} M \cap N \\[2ex]
2408: \mnot (\cM) & = & \bigcap_{M\in\cM} \mnot(M)
2409: \end{eqnarray*}
2410: \end{definition}
2411:
2412: Those operations on sets of patterns satisfy the same properties that
2413: singleton intersection and complementation do.
2414:
2415: \begin{corollary}[Correctness of Set Intersection] \mbox{} \newline
2416: \label{co:setunif}
2417: For $\cN_1,\cN_{2}\in \Pat$, $\Psi\vd M\in\|\cN_1\|\hastype A$ and $\Psi\vd
2418: M\in\|\cN_{2}\|\hastype A$ iff $\Psi\vd M\in\|\cN_1\cap
2419: \cN_{2}\|\hastype A$.
2420: \end{corollary}
2421: % \begin{proof}
2422: % $\GG\vd M\in\|\cN_1\|\hastype A$ and $\GG\vd
2423: % M\in\|\cN_{2}\|\hastype A$ iff there is $N_1\in\cN_1$ and
2424: % $N_{2}\in\cN_{2}$ such that $\GG\vd M\in\|N_1\|\hastype A$ and
2425: % $\GG\vd M\in\|N_{2}\|\hastype A$ iff, by Corollary \ref{co:unif},
2426: % $\GG\vd M\in\|N_1\cap N_{2}\|\hastype A$ iff, by definition,
2427: % $\GG\vd M\in\|\cN_1\cap \cN_{2}\|\hastype A$.
2428: % \end{proof}
2429:
2430: \begin{corollary}[Correctness of Set Complement] \mbox{} \newline
2431: \label{co:setpart}
2432: For $\cN \in \Pat$, $\Psi \vd M \in \|\mnot(\cN)\| \hastype A$ iff
2433: $\Psi \not\vd M \in \|\cN\| \hastype A$
2434: \end{corollary}
2435:
2436: As we have remarked earlier, we can define the relative complement
2437: operation by using complement and intersection. Its correctness
2438: follows immediately from the correctness of pattern set intersection
2439: and complement.
2440:
2441: \begin{definition}[Relative Complement]\mbox{}\\
2442: \label{def:relcompl}
2443: Given $\cM,\cN\in\Pat$, we define \mbox{$\cM - \cN = \cM\cap \mnot (\cN)$}.
2444: \end{definition}
2445:
2446: The properties above mean that we can organize, for a given signature
2447: $\Sigma$, context $\Psi$, and a type $A$, finite sets of simple linear
2448: patters into a Boolean algebra by taking equality as extensional
2449: identity on sets of terms without existential variables. In symbols, for
2450: $\cN_1,\cN_{2}\in \Pat$:
2451: \begin{eqnarray*}
2452: \cN_1\simeq \cN_2 & \mbox{iff} & \|\cN_1\| = \|\cN_2\|
2453: \end{eqnarray*}
2454:
2455: Under this interpretation, the $\zero$ element is the empty set and the
2456: $\one$ element the singleton set containing the $\eta$-expansion of a
2457: generalized existential variable of the appropriate type that may
2458: depend on all variables in the context $\Psi$.
2459: \begin{eqnarray*}
2460: \zero & = & \emptyset \\
2461: \one & = & \{\lam x_1^u\oftp A_1\ldots \lam x_n^u\oftp A_n\ldot E\ \Psi^u\
2462: x_1^u\ldots x_n^u\}
2463: \end{eqnarray*}
2464: where $A = A_1\TImp \cdots A_n \TImp a$.
2465:
2466: \begin{theorem}
2467: \label{thm:algebra}
2468: Consider the algebra $\langle \Pat,\cup,\cap,\mnot, \one,
2469: \zero\rangle$. Then the following holds:
2470: \begin{enumerate}
2471: \item $\cM\cap\cM \simeq \cM$.
2472: \item $\cM\cap\cN \simeq \cN\cap\cM$.
2473: \item\label{it:DM} $\cM\cap(\cN\cup\cP)\simeq
2474: (\cM\cap\cN)\cup(\cM\cap\cP)$.
2475: \item $\cM\cap(\cN\cap\cP) \simeq (\cM\cap\cN)\cap\cP$.
2476: \item $\mnot(\mnot (\cM))\simeq\cM$.
2477: \item $\mnot(\one)\simeq \zero$.
2478: \item $\mnot(\zero)\simeq \one$.
2479: \end{enumerate}
2480: \end{theorem}
2481: \begin{proof}
2482: From Corollaries~\ref{co:setunif} and~\ref{co:setpart} and the fact that
2483: $\cup$ is set-theoretic.
2484: \end{proof}
2485:
2486: \begin{corollary}
2487: \label{co:boolean}
2488: The algebra of finite sets of simple linear patterns is boolean.
2489: \end{corollary}
2490:
2491: It is notable that the $\cup$ operator must be set-theoretic union
2492: rather than anti-unification or generalization, as traditional in
2493: lattice-theoretic investigations of the algebra of terms
2494: \cite{Lassez88}. The problem is the intrinsically classical
2495: nature of complementation which is not compatible with the very
2496: irregular structure of the lattice of terms where the smallest upper
2497: bound is interpreted as anti-unification.
2498:
2499: We end this section showing how pattern complement can be used as a
2500: building block of our main application, that is a clause complement
2501: algorithm~\cite{Bar90}. In (higher-order) logic programming, in fact,
2502: pattern complement is a necessary component in any algorithm to
2503: synthesize the negation of a given program. This synthesis includes two
2504: basic operations: negation to compute the complements of heads of
2505: clauses in the definition of a predicate, and intersection to combine
2506: results of negating individual clause heads. In this paper we have
2507: provided algorithms to compute both. A full development for the
2508: higher-order case can be found in~\cite{Momigliano00phd}.
2509:
2510: \begin{example}
2511: \label{ex:combi}
2512: We can combine Example~\ref{ex:lam} and~\ref{ex:etardx} and consider
2513: the following trivial program, which encodes when an object-level
2514: lambda term is a $\beta\eta$-redex:
2515: \[
2516: \begin{array}{lll}
2517: {\it betardx} & : & {\it isredx}\ (\itapp\ (\itlam\ (\lamb{x^u}{\itexp} E\ x^u))\ F).\\
2518: {\it etardx} & : & {\it isredx}\ (\itlam\ (\lamb{x^u}{\itexp} \itapp\ (E\ x^0) \ x)).
2519: \end{array}\]
2520: We can compute the complement of both heads, as follows:
2521: \[
2522: \begin{array}{ll}
2523: \multicolumn{2}{l}{\mnot\{\itapp\ (\itlam\ (\lamb{x^u}{\itexp} E\ x^u)) \
2524: F, \itlam(\lamb{x^u}{\itexp} \itapp\ (E\ x^0) \ x)\}} \\
2525: = & \mnot(\itapp\ (\itlam\ (\lamb{x^u}{\itexp} E\ x^u))\ F)
2526: \cap\mnot(\itlam(\lamb{x^{u}}{\itexp} \itapp\ (E\ x^{0})\ x )) \\
2527: = & \{ \itlam\ (\lamb{x^u}{\itexp} H\ x^u), \itapp\ (\itapp\ H\ H') \ H''\} \\
2528: & \null \cap \{
2529: \begin{array}[t]{@{}l}
2530: \itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\ x^1)\ (H'\ x^u)),\\
2531: \itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\ x^u)\ (\itapp\ (H'\ x^u) \ (H'' x^u))), \\
2532: \itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\ x^u)\ (\itlam\ (\lamb{y^u}{\itexp} H'\ x^u\ y^u))),\\
2533: \itlam\ (\lamb{x^u}{\itexp} \itlam\ (\lamb{y^u}{\itexp} H\ x^u\ y^u) ),\\
2534: \itlam\ (\lamb{x^u}{\itexp} x),\\
2535: \itapp\ H\ H' \}
2536: \end{array} \\
2537: = & \{
2538: \begin{array}[t]{@{}l}
2539: \itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\ x^1)\ (H'\ x^{u})), \\
2540: \itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\ x^u)\ (\itapp\ (H'\ x^{u}) \ ( H''\ x^{u}))),\\
2541: \itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\ x^u)\ (\itlam\ (\lamb{y^u}{\itexp} H'\ x^u\ y^u)))\\
2542: \itlam\ (\lamb{x^u}{\itexp} \itlam\ (\lamb{y^u}{\itexp} H'\ x^u\ y^u)),\\
2543: \itlam\ (\lamb{x^u}{\itexp}x),\\
2544: \itapp\ (\itapp\ H\ H')\ H''\}
2545: \end{array}
2546: \end{array}
2547: \]
2548:
2549: This yields the negation of that program, that is the complementary clauses:
2550: \[
2551: \begin{array}{lll}
2552: {\it nb}_1 & : & {\it non\_isredx}\ (\itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\
2553: x^1)\ (H'\ x^{u}))).\\
2554: {\it nb}_2 & : & {\it non\_isredx}\ (\itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\
2555: x^u)\
2556: (\itapp\ (H'\ x^{u}) \ ( H''\ x^{u})))).\\
2557: {\it nb}_3 & : & {\it non\_isredx}\ (\itlam\ (\lamb{x^u}{\itexp} \itapp\ (H\
2558: x^u)\ (\itlam\ (\lamb{y^u}{\itexp} H'\ x^u\ y^u)))).\\
2559: {\it nb}_4 & : & {\it non\_isredx}\ (\itlam\ (\lamb{x^u}{\itexp}
2560: \itlam\ (\lamb{y^u}{\itexp} H\ x^u\ y^u) )).\\
2561: {\it nb}_5 & : & {\it non\_isredx}\ (\itlam\ (\lamb{x^u}{\itexp}x)).\\
2562: {\it nb}_6 & : & {\it non\_isredx}\ (\itapp\ (\itapp\ H\ H')\ H'').
2563: \end{array}\]
2564: \end{example}
2565:
2566: \section{Conclusions}
2567: \label{sec:concl}
2568: In this paper we have been concerned with the relative complement
2569: problem for higher-order patterns. As we have seen, the complement
2570: operation does not generalize easily from the first-order case.
2571: Indeed, the complement of a partially applied higher-order pattern
2572: cannot be described by a pattern, or even a by finite set of patterns.
2573: The formulation of the problem suggests that we should consider a
2574: $\lambda$-calculus with an internal notion of \emph{strictness} so that
2575: we can directly express that a term must depend on a given variable. We
2576: have developed such a calculus and we have shown that via a suitable
2577: embedding in our calculus the complement of a linear pattern is a finite
2578: set of linear patterns and unification of two patterns is decidable and
2579: leads to a finite set of most general unifiers. Moreover, they form a
2580: boolean algebra under set-theoretic union, intersection (implemented via
2581: unification) and the complement operation.
2582:
2583:
2584: The latter item brings up the question if we can actually decide
2585: extensional equality between, and membership of terms in, finite sets of
2586: simple terms. For membership, one can see that $\Psi\vd M\in \|
2587: N_1,\ldots,N_n\|$ iff $M$ unifies with some $N_i$. As far as equality
2588: is concerned between say $\| M_1,\ldots,M_m\|$ and $\| N_1,\ldots,N_n\|$
2589: calculate the two relative complements $\{ M_1,\ldots,M_m\} - \{
2590: N_1,\ldots,N_n\}$ and $ \{ N_1,\ldots,N_n\} - \{ M_1,\ldots,M_m\}$ and
2591: then check if they are both empty. An emptiness check would rely on the
2592: decidability of inhabitation in the underlying calculus. We conjecture
2593: this question to be decidable for the strict $\lambda$-calculus and we plan to
2594: address this question in future work.
2595: % possibly via a translation in an equivalent
2596: % contraction-free sequent calculus, following Dyckhoff's
2597: % approach~\cite{Dyckhoff92}.
2598:
2599: Our main application is the transformational approach to negation in
2600: higher-order logic programming \cite{Bar90}, where pattern complement
2601: and unification is a necessary component. We plan to extend the
2602: results to dependent types to endow intentionally weak frameworks such
2603: as Twelf \cite{Schurmann98cade} with a logically meaningful notion of
2604: negation along these lines.
2605:
2606: It may be argued that the restriction to simple terms is somewhat ad
2607: hoc. Ideally, one would have a complement algorithm for the full strict
2608: lambda-calculus (including vacuous types). Yet, this seems to be
2609: ill-defined, because ``occurrence'' no longer has the desired meaning
2610: once we lift the principle that constructors should be strict in their
2611: argument. As we have remarked earlier, it is possible to describe
2612: complement and unification algorithms for a larger fragment than treated
2613: here by allowing arbitrary abstractions, if we adhere to the above
2614: strictness assumption for constructors. The technical development is
2615: not difficult but entails a proliferation of rules to cover the new
2616: abstraction cases, as well as the duplication of all rules concerning
2617: strict application in versions similar to the ${\RImp}E^u$ and
2618: ${\RImp}E^1$ typing rules.
2619:
2620: Finally, it is our contention that the strict $\lam$-calculus that we
2621: have introduced has independent interest in the investigation of
2622: sub-structural logics. Our type system is simple and uniform and
2623: arguably more elegant than those ones presented in the literature (see
2624: the earlier discussion of related work at the end of
2625: Section~\ref{sec:canonthm}). Moreover, the explicit introduction of the
2626: notion of \emph{vacuous} or \emph{irrelevant} variables can be useful in
2627: a variety of contexts. In fact, the second author has suggested some
2628: unexpected usage of those variables in type theory for uses in reasoning
2629: about staged computation~\cite{Pfenning00saig} and proof compression in
2630: logical frameworks~\cite{Pfenning01lics}. Furthermore, extending a
2631: linear $\lam$-calculus with vacuous variables permits more programs
2632: under type assignment; for example a term such as $\lam x\ldot \lam
2633: y\ldot x\otimes (\lam w\ldot y)\ x$, which is traditionally considered
2634: \emph{not} linear, can be given the linear type $A \lop B \lop (A
2635: \otimes B)$. This carries over to the study of \emph{explicit
2636: substitutions} in resource-conscious $\lam$-calculi~\cite{Ghani98} where
2637: it might clarify the logical status of the \emph{extension operator}.
2638:
2639: \begin{acknowledgments}
2640: We would like to thank Roberto Virga, who discovered an error in an
2641: earlier version of this paper, and Iliano Cervesato and Carsten
2642: Sch\"urmann for several discussions and comments on a draft of this
2643: paper.
2644: \end{acknowledgments}
2645:
2646: \bibliographystyle{acmtrans}
2647: % \bibliography{not,framework,strict}
2648: \bibliography{tocl}
2649:
2650: \begin{received}
2651: Submitted September 2001
2652: % November 1993;
2653: % accepted January 1996
2654: \end{received}
2655:
2656: \end{document}
2657: