90 \pagestyle{empty} |
94 \pagestyle{empty} |
91 \begin{titlepage} |
95 \begin{titlepage} |
92 \maketitle |
96 \maketitle |
93 \begin{abstract} |
97 \begin{abstract} |
94 This paper presents a fixedpoint approach to inductive definitions. |
98 This paper presents a fixedpoint approach to inductive definitions. |
95 Instead of using a syntactic test such as `strictly positive,' the |
99 Instead of using a syntactic test such as ``strictly positive,'' the |
96 approach lets definitions involve any operators that have been proved |
100 approach lets definitions involve any operators that have been proved |
97 monotone. It is conceptually simple, which has allowed the easy |
101 monotone. It is conceptually simple, which has allowed the easy |
98 implementation of mutual recursion and other conveniences. It also |
102 implementation of mutual recursion and other conveniences. It also |
99 handles coinductive definitions: simply replace the least fixedpoint by a |
103 handles coinductive definitions: simply replace the least fixedpoint by a |
100 greatest fixedpoint. This represents the first automated support for |
104 greatest fixedpoint. This represents the first automated support for |
101 coinductive definitions. |
105 coinductive definitions. |
102 |
106 |
103 The method has been implemented in two of Isabelle's logics, ZF set theory |
107 The method has been implemented in two of Isabelle's logics, \textsc{zf} set |
104 and higher-order logic. It should be applicable to any logic in which |
108 theory and higher-order logic. It should be applicable to any logic in |
105 the Knaster-Tarski Theorem can be proved. Examples include lists of $n$ |
109 which the Knaster-Tarski theorem can be proved. Examples include lists of |
106 elements, the accessible part of a relation and the set of primitive |
110 $n$ elements, the accessible part of a relation and the set of primitive |
107 recursive functions. One example of a coinductive definition is |
111 recursive functions. One example of a coinductive definition is |
108 bisimulations for lazy lists. \ifCADE\else Recursive datatypes are |
112 bisimulations for lazy lists. Recursive datatypes are examined in detail, |
109 examined in detail, as well as one example of a {\bf codatatype}: lazy |
113 as well as one example of a \defn{codatatype}: lazy lists. |
110 lists. The appendices are simple user's manuals for this Isabelle |
114 |
111 package.\fi |
115 The Isabelle package has been applied in several large case studies, |
|
116 including two proofs of the Church-Rosser theorem and a coinductive proof of |
|
117 semantic consistency. |
112 \end{abstract} |
118 \end{abstract} |
113 % |
119 % |
114 \bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson} |
120 \bigskip |
|
121 \centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson} |
115 \thispagestyle{empty} |
122 \thispagestyle{empty} |
116 \end{titlepage} |
123 \end{titlepage} |
117 \tableofcontents\cleardoublepage\pagestyle{plain} |
124 \tableofcontents\cleardoublepage\pagestyle{plain} |
118 |
125 |
|
126 \setcounter{page}{1} |
|
127 |
119 \section{Introduction} |
128 \section{Introduction} |
120 Several theorem provers provide commands for formalizing recursive data |
129 Several theorem provers provide commands for formalizing recursive data |
121 structures, like lists and trees. Examples include Boyer and Moore's shell |
130 structures, like lists and trees. Robin Milner implemented one of the first |
122 principle~\cite{bm79} and Melham's recursive type package for the Cambridge HOL |
131 of these, for Edinburgh \textsc{lcf}~\cite{milner-ind}. Given a description |
123 system~\cite{melham89}. Such data structures are called {\bf datatypes} |
132 of the desired data structure, Milner's package formulated appropriate |
124 below, by analogy with {\tt datatype} definitions in Standard~ML\@. |
133 definitions and proved the characteristic theorems. Similar is Melham's |
125 |
134 recursive type package for the Cambridge \textsc{hol} system~\cite{melham89}. |
126 A datatype is but one example of an {\bf inductive definition}. This |
135 Such data structures are called \defn{datatypes} |
|
136 below, by analogy with datatype declarations in Standard~\textsc{ml}\@. |
|
137 Some logics take datatypes as primitive; consider Boyer and Moore's shell |
|
138 principle~\cite{bm79} and the Coq type theory~\cite{paulin92}. |
|
139 |
|
140 A datatype is but one example of an \defn{inductive definition}. This |
127 specifies the least set closed under given rules~\cite{aczel77}. The |
141 specifies the least set closed under given rules~\cite{aczel77}. The |
128 collection of theorems in a logic is inductively defined. A structural |
142 collection of theorems in a logic is inductively defined. A structural |
129 operational semantics~\cite{hennessy90} is an inductive definition of a |
143 operational semantics~\cite{hennessy90} is an inductive definition of a |
130 reduction or evaluation relation on programs. A few theorem provers |
144 reduction or evaluation relation on programs. A few theorem provers |
131 provide commands for formalizing inductive definitions; these include |
145 provide commands for formalizing inductive definitions; these include |
132 Coq~\cite{paulin92} and again the HOL system~\cite{camilleri92}. |
146 Coq~\cite{paulin92} and again the \textsc{hol} system~\cite{camilleri92}. |
133 |
147 |
134 The dual notion is that of a {\bf coinductive definition}. This specifies |
148 The dual notion is that of a \defn{coinductive definition}. This specifies |
135 the greatest set closed under given rules. Important examples include |
149 the greatest set closed under given rules. Important examples include |
136 using bisimulation relations to formalize equivalence of |
150 using bisimulation relations to formalize equivalence of |
137 processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}. |
151 processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}. |
138 Other examples include lazy lists and other infinite data structures; these |
152 Other examples include lazy lists and other infinite data structures; these |
139 are called {\bf codatatypes} below. |
153 are called \defn{codatatypes} below. |
140 |
154 |
141 Not all inductive definitions are meaningful. {\bf Monotone} inductive |
155 Not all inductive definitions are meaningful. \defn{Monotone} inductive |
142 definitions are a large, well-behaved class. Monotonicity can be enforced |
156 definitions are a large, well-behaved class. Monotonicity can be enforced |
143 by syntactic conditions such as `strictly positive,' but this could lead to |
157 by syntactic conditions such as ``strictly positive,'' but this could lead to |
144 monotone definitions being rejected on the grounds of their syntactic form. |
158 monotone definitions being rejected on the grounds of their syntactic form. |
145 More flexible is to formalize monotonicity within the logic and allow users |
159 More flexible is to formalize monotonicity within the logic and allow users |
146 to prove it. |
160 to prove it. |
147 |
161 |
148 This paper describes a package based on a fixedpoint approach. Least |
162 This paper describes a package based on a fixedpoint approach. Least |
149 fixedpoints yield inductive definitions; greatest fixedpoints yield |
163 fixedpoints yield inductive definitions; greatest fixedpoints yield |
150 coinductive definitions. The package has several advantages: |
164 coinductive definitions. Most of the discussion below applies equally to |
151 \begin{itemize} |
165 inductive and coinductive definitions, and most of the code is shared. To my |
152 \item It allows reference to any operators that have been proved monotone. |
166 knowledge, this is the only package supporting coinductive definitions. |
153 Thus it accepts all provably monotone inductive definitions, including |
167 |
154 iterated definitions. |
168 The package supports mutual recursion and infinitely-branching datatypes and |
155 \item It accepts a wide class of datatype definitions, including those with |
169 codatatypes. It allows use of any operators that have been proved monotone, |
156 infinite branching. |
170 thus accepting all provably monotone inductive definitions, including |
157 \item It handles coinductive and codatatype definitions. Most of |
171 iterated definitions. |
158 the discussion below applies equally to inductive and coinductive |
172 |
159 definitions, and most of the code is shared. To my knowledge, this is |
173 The package has been implemented in Isabelle~\cite{isabelle-intro} using |
160 the only package supporting coinductive definitions. |
174 \textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has |
161 \item Definitions may be mutually recursive. |
175 since been ported to Isabelle/\textsc{hol} (higher-order logic). The |
162 \end{itemize} |
176 recursion equations are specified as introduction rules for the mutually |
163 The package has been implemented in Isabelle~\cite{isabelle-intro} using ZF |
177 recursive sets. The package transforms these rules into a mapping over sets, |
164 set theory \cite{paulson-set-I,paulson-set-II}; part of it has since been |
178 and attempts to prove that the mapping is monotonic and well-typed. If |
165 ported to Isabelle's higher-order logic. However, the fixedpoint approach is |
179 successful, the package makes fixedpoint definitions and proves the |
166 independent of Isabelle. The recursion equations are specified as |
180 introduction, elimination and (co)induction rules. Users invoke the package |
167 introduction rules for the mutually recursive sets. The package transforms |
181 by making simple declarations in Isabelle theory files. |
168 these rules into a mapping over sets, and attempts to prove that the |
|
169 mapping is monotonic and well-typed. If successful, the package makes |
|
170 fixedpoint definitions and proves the introduction, elimination and |
|
171 (co)induction rules. The package consists of several Standard ML |
|
172 functors~\cite{paulson91}; it accepts its argument and returns its result |
|
173 as ML structures.\footnote{This use of ML modules is not essential; the |
|
174 package could also be implemented as a function on records.} |
|
175 |
182 |
176 Most datatype packages equip the new datatype with some means of expressing |
183 Most datatype packages equip the new datatype with some means of expressing |
177 recursive functions. This is the main omission from my package. Its |
184 recursive functions. This is the main omission from my package. Its |
178 fixedpoint operators define only recursive sets. To define recursive |
185 fixedpoint operators define only recursive sets. The Isabelle/\textsc{zf} |
179 functions, the Isabelle/ZF theory provides well-founded recursion and other |
186 theory provides well-founded recursion~\cite{paulson-set-II}, which is harder |
180 logical tools~\cite{paulson-set-II}. |
187 to use than structural recursion but considerably more general. |
181 |
188 Slind~\cite{slind-tfl} has written a package to automate the definition of |
182 {\bf Outline.} Section~2 introduces the least and greatest fixedpoint |
189 well-founded recursive functions in Isabelle/\textsc{hol}. |
|
190 |
|
191 \paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint |
183 operators. Section~3 discusses the form of introduction rules, mutual |
192 operators. Section~3 discusses the form of introduction rules, mutual |
184 recursion and other points common to inductive and coinductive definitions. |
193 recursion and other points common to inductive and coinductive definitions. |
185 Section~4 discusses induction and coinduction rules separately. Section~5 |
194 Section~4 discusses induction and coinduction rules separately. Section~5 |
186 presents several examples, including a coinductive definition. Section~6 |
195 presents several examples, including a coinductive definition. Section~6 |
187 describes datatype definitions. Section~7 presents related work. |
196 describes datatype definitions. Section~7 presents related work. |
188 Section~8 draws brief conclusions. \ifCADE\else The appendices are simple |
197 Section~8 draws brief conclusions. \ifshort\else The appendices are simple |
189 user's manuals for this Isabelle package.\fi |
198 user's manuals for this Isabelle package.\fi |
190 |
199 |
191 Most of the definitions and theorems shown below have been generated by the |
200 Most of the definitions and theorems shown below have been generated by the |
192 package. I have renamed some variables to improve readability. |
201 package. I have renamed some variables to improve readability. |
193 |
202 |
196 follows: |
205 follows: |
197 \begin{eqnarray*} |
206 \begin{eqnarray*} |
198 \lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\ |
207 \lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\ |
199 \gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\} |
208 \gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\} |
200 \end{eqnarray*} |
209 \end{eqnarray*} |
201 Let $D$ be a set. Say that $h$ is {\bf bounded by}~$D$ if $h(D)\sbs D$, and |
210 Let $D$ be a set. Say that $h$ is \defn{bounded by}~$D$ if $h(D)\sbs D$, and |
202 {\bf monotone below~$D$} if |
211 \defn{monotone below~$D$} if |
203 $h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is |
212 $h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is |
204 bounded by~$D$ and monotone then both operators yield fixedpoints: |
213 bounded by~$D$ and monotone then both operators yield fixedpoints: |
205 \begin{eqnarray*} |
214 \begin{eqnarray*} |
206 \lfp(D,h) & = & h(\lfp(D,h)) \\ |
215 \lfp(D,h) & = & h(\lfp(D,h)) \\ |
207 \gfp(D,h) & = & h(\gfp(D,h)) |
216 \gfp(D,h) & = & h(\gfp(D,h)) |
208 \end{eqnarray*} |
217 \end{eqnarray*} |
209 These equations are instances of the Knaster-Tarski Theorem, which states |
218 These equations are instances of the Knaster-Tarski theorem, which states |
210 that every monotonic function over a complete lattice has a |
219 that every monotonic function over a complete lattice has a |
211 fixedpoint~\cite{davey&priestley}. It is obvious from their definitions |
220 fixedpoint~\cite{davey&priestley}. It is obvious from their definitions |
212 that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. |
221 that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. |
213 |
222 |
214 This fixedpoint theory is simple. The Knaster-Tarski Theorem is easy to |
223 This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to |
215 prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must |
224 prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must |
216 also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as |
225 also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as when |
217 when a set of `theorems' is (co)inductively defined over some previously |
226 a set of theorems is (co)inductively defined over some previously existing set |
218 existing set of `formulae.' Isabelle/ZF provides a suitable bounding set |
227 of formul{\ae}. Isabelle/\textsc{zf} provides suitable bounding sets for infinitely |
219 for finitely branching (co)datatype definitions; see~\S\ref{univ-sec} |
228 branching (co)datatype definitions; see~\S\ref{univ-sec}. Bounding sets are |
220 below. Bounding sets are also called {\bf domains}. |
229 also called \defn{domains}. |
221 |
230 |
222 The powerset operator is monotone, but by Cantor's Theorem there is no |
231 The powerset operator is monotone, but by Cantor's theorem there is no |
223 set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because |
232 set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because |
224 there is no suitable domain~$D$. But \S\ref{acc-sec} demonstrates |
233 there is no suitable domain~$D$. But \S\ref{acc-sec} demonstrates |
225 that~$\pow$ is still useful in inductive definitions. |
234 that~$\pow$ is still useful in inductive definitions. |
226 |
235 |
227 \section{Elements of an inductive or coinductive definition}\label{basic-sec} |
236 \section{Elements of an inductive or coinductive definition}\label{basic-sec} |
240 $n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$ |
249 $n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$ |
241 varies. Section~\ref{listn-sec} describes how to express this set using the |
250 varies. Section~\ref{listn-sec} describes how to express this set using the |
242 inductive definition package. |
251 inductive definition package. |
243 |
252 |
244 To avoid clutter below, the recursive sets are shown as simply $R_i$ |
253 To avoid clutter below, the recursive sets are shown as simply $R_i$ |
245 instead of $R_i(\vec{p})$. |
254 instead of~$R_i(\vec{p})$. |
246 |
255 |
247 \subsection{The form of the introduction rules}\label{intro-sec} |
256 \subsection{The form of the introduction rules}\label{intro-sec} |
248 The body of the definition consists of the desired introduction rules, |
257 The body of the definition consists of the desired introduction rules. The |
249 specified as strings. The conclusion of each rule must have the form $t\in |
258 conclusion of each rule must have the form $t\in R_i$, where $t$ is any term. |
250 R_i$, where $t$ is any term. Premises typically have the same form, but |
259 Premises typically have the same form, but they can have the more general form |
251 they can have the more general form $t\in M(R_i)$ or express arbitrary |
260 $t\in M(R_i)$ or express arbitrary side-conditions. |
252 side-conditions. |
|
253 |
261 |
254 The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on |
262 The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on |
255 sets, satisfying the rule |
263 sets, satisfying the rule |
256 \[ \infer{M(A)\sbs M(B)}{A\sbs B} \] |
264 \[ \infer{M(A)\sbs M(B)}{A\sbs B} \] |
257 The user must supply the package with monotonicity rules for all such premises. |
265 The user must supply the package with monotonicity rules for all such premises. |
258 |
266 |
259 The ability to introduce new monotone operators makes the approach |
267 The ability to introduce new monotone operators makes the approach |
260 flexible. A suitable choice of~$M$ and~$t$ can express a lot. The |
268 flexible. A suitable choice of~$M$ and~$t$ can express a lot. The |
261 powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$ |
269 powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$ |
262 expresses $t\sbs R$; see \S\ref{acc-sec} for an example. The `list of' |
270 expresses $t\sbs R$; see \S\ref{acc-sec} for an example. The \emph{list of} |
263 operator is monotone, as is easily proved by induction. The premise |
271 operator is monotone, as is easily proved by induction. The premise |
264 $t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual |
272 $t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual |
265 recursion; see \S\ref{primrec-sec} and also my earlier |
273 recursion; see \S\ref{primrec-sec} and also my earlier |
266 paper~\cite[\S4.4]{paulson-set-II}. |
274 paper~\cite[\S4.4]{paulson-set-II}. |
267 |
275 |
268 Introduction rules may also contain {\bf side-conditions}. These are |
276 Introduction rules may also contain \defn{side-conditions}. These are |
269 premises consisting of arbitrary formulae not mentioning the recursive |
277 premises consisting of arbitrary formul{\ae} not mentioning the recursive |
270 sets. Side-conditions typically involve type-checking. One example is the |
278 sets. Side-conditions typically involve type-checking. One example is the |
271 premise $a\in A$ in the following rule from the definition of lists: |
279 premise $a\in A$ in the following rule from the definition of lists: |
272 \[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \] |
280 \[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \] |
273 |
281 |
274 \subsection{The fixedpoint definitions} |
282 \subsection{The fixedpoint definitions} |
302 monotonicity proof requires some unusual rules. These state that the |
309 monotonicity proof requires some unusual rules. These state that the |
303 connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect |
310 connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect |
304 to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and |
311 to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and |
305 only if $\forall x.P(x)\imp Q(x)$.} |
312 only if $\forall x.P(x)\imp Q(x)$.} |
306 |
313 |
307 The package returns its result as an ML structure, which consists of named |
314 The package returns its result as an \textsc{ml} structure, which consists of named |
308 components; we may regard it as a record. The result structure contains |
315 components; we may regard it as a record. The result structure contains |
309 the definitions of the recursive sets as a theorem list called {\tt defs}. |
316 the definitions of the recursive sets as a theorem list called {\tt defs}. |
310 It also contains some theorems; {\tt dom\_subset} is an inclusion such as |
317 It also contains some theorems; {\tt dom\_subset} is an inclusion such as |
311 $\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint |
318 $\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint |
312 definition is monotonic. |
319 definition is monotonic. |
313 |
320 |
314 Internally the package uses the theorem {\tt unfold}, a fixedpoint equation |
321 Internally the package uses the theorem {\tt unfold}, a fixedpoint equation |
315 such as |
322 such as |
316 \begin{eqnarray*} |
323 \[ |
317 \Fin(A) & = & |
|
318 \begin{array}[t]{r@{\,}l} |
324 \begin{array}[t]{r@{\,}l} |
319 \{z\in\pow(A). & z=\emptyset \disj{} \\ |
325 \Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\ |
320 &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\} |
326 &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\} |
321 \end{array} |
327 \end{array} |
322 \end{eqnarray*} |
328 \] |
323 In order to save space, this theorem is not exported. |
329 In order to save space, this theorem is not exported. |
324 |
330 |
325 |
331 |
326 \subsection{Mutual recursion} \label{mutual-sec} |
332 \subsection{Mutual recursion} \label{mutual-sec} |
327 In a mutually recursive definition, the domain of the fixedpoint construction |
333 In a mutually recursive definition, the domain of the fixedpoint construction |
328 is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$, |
334 is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$, |
329 \ldots,~$n$. The package uses the injections of the |
335 \ldots,~$n$. The package uses the injections of the |
330 binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections |
336 binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections |
331 $h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$. |
337 $h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$. |
332 |
338 |
333 As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/ZF defines the |
339 As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/\textsc{zf} defines the |
334 operator $\Part$ to support mutual recursion. The set $\Part(A,h)$ |
340 operator $\Part$ to support mutual recursion. The set $\Part(A,h)$ |
335 contains those elements of~$A$ having the form~$h(z)$: |
341 contains those elements of~$A$ having the form~$h(z)$: |
336 \begin{eqnarray*} |
342 \[ \Part(A,h) \equiv \{x\in A. \exists z. x=h(z)\}. \] |
337 \Part(A,h) & \equiv & \{x\in A. \exists z. x=h(z)\}. |
|
338 \end{eqnarray*} |
|
339 For mutually recursive sets $R_1$, \ldots,~$R_n$ with |
343 For mutually recursive sets $R_1$, \ldots,~$R_n$ with |
340 $n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using |
344 $n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using |
341 a fixedpoint operator. The remaining $n$ definitions have the form |
345 a fixedpoint operator. The remaining $n$ definitions have the form |
342 \begin{eqnarray*} |
346 \[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n. \] |
343 R_i & \equiv & \Part(R,h_{in}), \qquad i=1,\ldots, n. |
|
344 \end{eqnarray*} |
|
345 It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint. |
347 It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint. |
346 |
348 |
347 |
349 |
348 \subsection{Proving the introduction rules} |
350 \subsection{Proving the introduction rules} |
349 The user supplies the package with the desired form of the introduction |
351 The user supplies the package with the desired form of the introduction |
359 in the rules, the package must prove |
361 in the rules, the package must prove |
360 \[ \emptyset\in\pow(A) \qquad |
362 \[ \emptyset\in\pow(A) \qquad |
361 \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} |
363 \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} |
362 \] |
364 \] |
363 Such proofs can be regarded as type-checking the definition.\footnote{The |
365 Such proofs can be regarded as type-checking the definition.\footnote{The |
364 Isabelle/HOL version does not require these proofs, as HOL has implicit |
366 Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol} |
365 type-checking.} The user supplies the package with type-checking rules to |
367 has implicit type-checking.} The user supplies the package with |
366 apply. Usually these are general purpose rules from the ZF theory. They |
368 type-checking rules to apply. Usually these are general purpose rules from |
367 could however be rules specifically proved for a particular inductive |
369 the \textsc{zf} theory. They could however be rules specifically proved for a |
368 definition; sometimes this is the easiest way to get the definition |
370 particular inductive definition; sometimes this is the easiest way to get the |
369 through! |
371 definition through! |
370 |
372 |
371 The result structure contains the introduction rules as the theorem list {\tt |
373 The result structure contains the introduction rules as the theorem list {\tt |
372 intrs}. |
374 intrs}. |
373 |
375 |
374 \subsection{The case analysis rule} |
376 \subsection{The case analysis rule} |
375 The elimination rule, called {\tt elim}, performs case analysis. There is one |
377 The elimination rule, called {\tt elim}, performs case analysis. It is a |
376 case for each introduction rule. The elimination rule |
378 simple consequence of {\tt unfold}. There is one case for each introduction |
377 for $\Fin(A)$ is |
379 rule. If $x\in\Fin(A)$ then either $x=\emptyset$ or else $x=\{a\}\un b$ for |
|
380 some $a\in A$ and $b\in\Fin(A)$. Formally, the elimination rule for $\Fin(A)$ |
|
381 is written |
378 \[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]} |
382 \[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]} |
379 & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} } |
383 & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} } |
380 \] |
384 \] |
381 The subscripted variables $a$ and~$b$ above the third premise are |
385 The subscripted variables $a$ and~$b$ above the third premise are |
382 eigenvariables, subject to the usual `not free in \ldots' proviso. |
386 eigenvariables, subject to the usual ``not free in \ldots'' proviso. |
383 The rule states that if $x\in\Fin(A)$ then either $x=\emptyset$ or else |
|
384 $x=\{a\}\un b$ for some $a\in A$ and $b\in\Fin(A)$; it is a simple consequence |
|
385 of {\tt unfold}. |
|
386 |
|
387 The package also returns a function for generating simplified instances of |
|
388 the case analysis rule. It works for datatypes and for inductive |
|
389 definitions involving datatypes, such as an inductively defined relation |
|
390 between lists. It instantiates {\tt elim} with a user-supplied term then |
|
391 simplifies the cases using freeness of the underlying datatype. The |
|
392 simplified rules perform `rule inversion' on the inductive definition. |
|
393 Section~\S\ref{mkcases} presents an example. |
|
394 |
387 |
395 |
388 |
396 \section{Induction and coinduction rules} |
389 \section{Induction and coinduction rules} |
397 Here we must consider inductive and coinductive definitions separately. |
390 Here we must consider inductive and coinductive definitions separately. |
398 For an inductive definition, the package returns an induction rule derived |
391 For an inductive definition, the package returns an induction rule derived |
471 greatest fixedpoint satisfying the rules |
464 greatest fixedpoint satisfying the rules |
472 \[ \LNil\in\llist(A) \qquad |
465 \[ \LNil\in\llist(A) \qquad |
473 \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)} |
466 \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)} |
474 \] |
467 \] |
475 The $(-)$ tag stresses that this is a coinductive definition. A suitable |
468 The $(-)$ tag stresses that this is a coinductive definition. A suitable |
476 domain for $\llist(A)$ is $\quniv(A)$, a set closed under variant forms of |
469 domain for $\llist(A)$ is $\quniv(A)$; this set is closed under the variant |
477 sum and product for representing infinite data structures |
470 forms of sum and product that are used to represent non-well-founded data |
478 (see~\S\ref{univ-sec}). Coinductive definitions use these variant sums and |
471 structures (see~\S\ref{univ-sec}). |
479 products. |
|
480 |
472 |
481 The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. |
473 The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. |
482 Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$ |
474 Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$ |
483 is the greatest solution to this equation contained in $\quniv(A)$: |
475 is the greatest solution to this equation contained in $\quniv(A)$: |
484 \[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) & |
476 \[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) & |
485 \infer*{z=\LNil\disj \bigl(\exists a\,l.\, |
477 \infer*{ |
486 z=\LCons(a,l) \conj a\in A \conj l\in X\un\llist(A) \bigr)} |
478 \begin{array}[b]{r@{}l} |
487 {[z\in X]_z}} |
479 z=\LNil\disj |
488 % \begin{array}[t]{@{}l} |
480 \bigl(\exists a\,l.\, & z=\LCons(a,l) \conj a\in A \conj{}\\ |
489 % z=\LCons(a,l) \conj a\in A \conj{}\\ |
481 & l\in X\un\llist(A) \bigr) |
490 % l\in X\un\llist(A) \bigr) |
482 \end{array} }{[z\in X]_z}} |
491 % \end{array} }{[z\in X]_z}} |
|
492 \] |
483 \] |
493 This rule complements the introduction rules; it provides a means of showing |
484 This rule complements the introduction rules; it provides a means of showing |
494 $x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then |
485 $x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then |
495 applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$ |
486 applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$ |
496 is the set of natural numbers.) |
487 is the set of natural numbers.) |
497 |
488 |
498 Having $X\un\llist(A)$ instead of simply $X$ in the third premise above |
489 Having $X\un\llist(A)$ instead of simply $X$ in the third premise above |
499 represents a slight strengthening of the greatest fixedpoint property. I |
490 represents a slight strengthening of the greatest fixedpoint property. I |
500 discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}. |
491 discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}. |
501 |
492 |
|
493 The clumsy form of the third premise makes the rule hard to use, especially in |
|
494 large definitions. Probably a constant should be declared to abbreviate the |
|
495 large disjunction, and rules derived to allow proving the separate disjuncts. |
|
496 |
502 |
497 |
503 \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec} |
498 \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec} |
504 This section presents several examples: the finite powerset operator, |
499 This section presents several examples from the literature: the finite |
505 lists of $n$ elements, bisimulations on lazy lists, the well-founded part |
500 powerset operator, lists of $n$ elements, bisimulations on lazy lists, the |
506 of a relation, and the primitive recursive functions. |
501 well-founded part of a relation, and the primitive recursive functions. |
507 |
502 |
508 \subsection{The finite powerset operator} |
503 \subsection{The finite powerset operator} |
509 This operator has been discussed extensively above. Here is the |
504 This operator has been discussed extensively above. Here is the |
510 corresponding invocation in an Isabelle theory file. Note that |
505 corresponding invocation in an Isabelle theory file. Note that |
511 $\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/ZF. |
506 $\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}. |
512 \begin{ttbox} |
507 \begin{ttbox} |
513 Finite = Arith + |
508 Finite = Arith + |
514 consts Fin :: i=>i |
509 consts Fin :: i=>i |
515 inductive |
510 inductive |
516 domains "Fin(A)" <= "Pow(A)" |
511 domains "Fin(A)" <= "Pow(A)" |
572 ListN = List + |
567 ListN = List + |
573 consts listn :: i=>i |
568 consts listn :: i=>i |
574 inductive |
569 inductive |
575 domains "listn(A)" <= "nat*list(A)" |
570 domains "listn(A)" <= "nat*list(A)" |
576 intrs |
571 intrs |
577 NilI "<0,Nil> : listn(A)" |
572 NilI "<0,Nil>: listn(A)" |
578 ConsI "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)" |
573 ConsI "[| a: A; <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)" |
579 type_intrs "nat_typechecks @ list.intrs" |
574 type_intrs "nat_typechecks @ list.intrs" |
580 end |
575 end |
581 \end{ttbox} |
576 \end{ttbox} |
582 The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$. |
577 The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$. |
583 Because $\listn(A)$ is a set of pairs, type-checking requires the |
578 Because $\listn(A)$ is a set of pairs, type-checking requires the |
584 equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$; the |
579 equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. The |
585 package always includes the necessary rules. |
580 package always includes the rules for ordered pairs. |
586 |
581 |
587 The package returns introduction, elimination and induction rules for |
582 The package returns introduction, elimination and induction rules for |
588 $\listn$. The basic induction rule, {\tt ListN.induct}, is |
583 $\listn$. The basic induction rule, {\tt listn.induct}, is |
589 \[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) & |
584 \[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) & |
590 \infer*{P(\pair{\succ(n),\Cons(a,l)})} |
585 \infer*{P(\pair{\succ(n),\Cons(a,l)})} |
591 {[a\in A & \pair{n,l}\in\listn(A) & P(\pair{n,l})]_{a,l,n}}} |
586 {[a\in A & \pair{n,l}\in\listn(A) & P(\pair{n,l})]_{a,l,n}}} |
592 \] |
587 \] |
593 This rule requires the induction formula to be a |
588 This rule requires the induction formula to be a |
594 unary property of pairs,~$P(\pair{n,l})$. The alternative rule, {\tt |
589 unary property of pairs,~$P(\pair{n,l})$. The alternative rule, {\tt |
595 ListN.mutual\_induct}, uses a binary property instead: |
590 listn.mutual\_induct}, uses a binary property instead: |
596 \[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)} |
591 \[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)} |
597 {P(0,\Nil) & |
592 {P(0,\Nil) & |
598 \infer*{P(\succ(n),\Cons(a,l))} |
593 \infer*{P(\succ(n),\Cons(a,l))} |
599 {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}} |
594 {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}} |
600 \] |
595 \] |
603 \[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \] |
598 \[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \] |
604 This latter result --- here $r``X$ denotes the image of $X$ under $r$ |
599 This latter result --- here $r``X$ denotes the image of $X$ under $r$ |
605 --- asserts that the inductive definition agrees with the obvious notion of |
600 --- asserts that the inductive definition agrees with the obvious notion of |
606 $n$-element list. |
601 $n$-element list. |
607 |
602 |
608 Unlike in Coq, the definition does not declare a new datatype. A `list of |
603 Unlike in Coq, the definition does not declare a new datatype. A ``list of |
609 $n$ elements' really is a list and is subject to list operators such |
604 $n$ elements'' really is a list and is subject to list operators such |
610 as append (concatenation). For example, a trivial induction on |
605 as append (concatenation). For example, a trivial induction on |
611 $\pair{m,l}\in\listn(A)$ yields |
606 $\pair{m,l}\in\listn(A)$ yields |
612 \[ \infer{\pair{m\mathbin{+} m,\, l@l'}\in\listn(A)} |
607 \[ \infer{\pair{m\mathbin{+} m,\, l@l'}\in\listn(A)} |
613 {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} |
608 {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} |
614 \] |
609 \] |
615 where $+$ here denotes addition on the natural numbers and @ denotes append. |
610 where $+$ here denotes addition on the natural numbers and @ denotes append. |
616 |
611 |
617 \subsection{A demonstration of rule inversion}\label{mkcases} |
612 \subsection{Rule inversion: the function {\tt mk\_cases}} |
618 The elimination rule, {\tt ListN.elim}, is cumbersome: |
613 The elimination rule, {\tt listn.elim}, is cumbersome: |
619 \[ \infer{Q}{x\in\listn(A) & |
614 \[ \infer{Q}{x\in\listn(A) & |
620 \infer*{Q}{[x = \pair{0,\Nil}]} & |
615 \infer*{Q}{[x = \pair{0,\Nil}]} & |
621 \infer*{Q} |
616 \infer*{Q} |
622 {\left[\begin{array}{l} |
617 {\left[\begin{array}{l} |
623 x = \pair{\succ(n),\Cons(a,l)} \\ |
618 x = \pair{\succ(n),\Cons(a,l)} \\ |
624 a\in A \\ |
619 a\in A \\ |
625 \pair{n,l}\in\listn(A) |
620 \pair{n,l}\in\listn(A) |
626 \end{array} \right]_{a,l,n}}} |
621 \end{array} \right]_{a,l,n}}} |
627 \] |
622 \] |
628 The ML function {\tt ListN.mk\_cases} generates simplified instances of |
623 The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of |
629 this rule. It works by freeness reasoning on the list constructors: |
624 this rule. It works by freeness reasoning on the list constructors: |
630 $\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If |
625 $\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If |
631 $x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases} |
626 $x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt listn.mk\_cases} |
632 deduces the corresponding form of~$i$; this is called rule inversion. For |
627 deduces the corresponding form of~$i$; this is called rule inversion. |
633 example, |
628 Here is a sample session: |
634 \begin{ttbox} |
629 \begin{ttbox} |
635 ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)" |
630 listn.mk_cases list.con_defs "<i,Nil> : listn(A)"; |
|
631 {\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm} |
|
632 listn.mk_cases list.con_defs "<i,Cons(a,l)> : listn(A)"; |
|
633 {\out "[| <?i, Cons(?a, ?l)> : listn(?A);} |
|
634 {\out !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q } |
|
635 {\out |] ==> ?Q" : thm} |
636 \end{ttbox} |
636 \end{ttbox} |
637 yields a rule with only two premises: |
637 Each of these rules has only two premises. In conventional notation, the |
|
638 second rule is |
638 \[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & |
639 \[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & |
639 \infer*{Q} |
640 \infer*{Q} |
640 {\left[\begin{array}{l} |
641 {\left[\begin{array}{l} |
641 i = \succ(n) \\ a\in A \\ \pair{n,l}\in\listn(A) |
642 a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n) |
642 \end{array} \right]_{n}}} |
643 \end{array} \right]_{n}}} |
643 \] |
644 \] |
644 The package also has built-in rules for freeness reasoning about $0$ |
645 The package also has built-in rules for freeness reasoning about $0$ |
645 and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt |
646 and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt |
646 ListN.mk\_cases} can similarly deduce the corresponding form of~$l$. |
647 listn.mk\_cases} can deduce the corresponding form of~$l$. |
647 |
648 |
648 The function {\tt mk\_cases} is also useful with datatype definitions. The |
649 The function {\tt mk\_cases} is also useful with datatype definitions. The |
649 instance from the definition of lists, namely {\tt List.mk\_cases}, can |
650 instance from the definition of lists, namely {\tt list.mk\_cases}, can |
650 prove the rule |
651 prove that $\Cons(a,l)\in\lst(A)$ implies $a\in A $ and $l\in\lst(A)$: |
651 \[ \infer{Q}{\Cons(a,l)\in\lst(A) & |
652 \[ \infer{Q}{\Cons(a,l)\in\lst(A) & |
652 & \infer*{Q}{[a\in A &l\in\lst(A)]} } |
653 & \infer*{Q}{[a\in A &l\in\lst(A)]} } |
653 \] |
654 \] |
654 A typical use of {\tt mk\_cases} concerns inductive definitions of |
655 A typical use of {\tt mk\_cases} concerns inductive definitions of evaluation |
655 evaluation relations. Then rule inversion yields case analysis on possible |
656 relations. Then rule inversion yields case analysis on possible evaluations. |
656 evaluations. For example, the Isabelle/ZF theory includes a short proof |
657 For example, Isabelle/\textsc{zf} includes a short proof of the |
657 of the diamond property for parallel contraction on combinators. |
658 diamond property for parallel contraction on combinators. Ole Rasmussen used |
|
659 {\tt mk\_cases} extensively in his development of the theory of |
|
660 residuals~\cite{rasmussen95}. |
|
661 |
658 |
662 |
659 \subsection{A coinductive definition: bisimulations on lazy lists} |
663 \subsection{A coinductive definition: bisimulations on lazy lists} |
660 This example anticipates the definition of the codatatype $\llist(A)$, which |
664 This example anticipates the definition of the codatatype $\llist(A)$, which |
661 consists of finite and infinite lists over~$A$. Its constructors are $\LNil$ |
665 consists of finite and infinite lists over~$A$. Its constructors are $\LNil$ |
662 and |
666 and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}. |
663 $\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}. |
|
664 Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant |
667 Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant |
665 pairing and injection operators, it contains non-well-founded elements such as |
668 pairing and injection operators, it contains non-well-founded elements such as |
666 solutions to $\LCons(a,l)=l$. |
669 solutions to $\LCons(a,l)=l$. |
667 |
670 |
668 The next step in the development of lazy lists is to define a coinduction |
671 The next step in the development of lazy lists is to define a coinduction |
692 \begin{ttbox} |
695 \begin{ttbox} |
693 consts lleq :: i=>i |
696 consts lleq :: i=>i |
694 coinductive |
697 coinductive |
695 domains "lleq(A)" <= "llist(A) * llist(A)" |
698 domains "lleq(A)" <= "llist(A) * llist(A)" |
696 intrs |
699 intrs |
697 LNil "<LNil, LNil> : lleq(A)" |
700 LNil "<LNil,LNil> : lleq(A)" |
698 LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)" |
701 LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)" |
699 type_intrs "llist.intrs" |
702 type_intrs "llist.intrs" |
700 \end{ttbox} |
703 \end{ttbox} |
701 Again, {\tt addconsts} declares a constant for $\lleq$ in the parent theory. |
|
702 The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking |
704 The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking |
703 rules include the introduction rules for $\llist(A)$, whose |
705 rules include the introduction rules for $\llist(A)$, whose |
704 declaration is discussed below (\S\ref{lists-sec}). |
706 declaration is discussed below (\S\ref{lists-sec}). |
705 |
707 |
706 The package returns the introduction rules and the elimination rule, as |
708 The package returns the introduction rules and the elimination rule, as |
707 usual. But instead of induction rules, it returns a coinduction rule. |
709 usual. But instead of induction rules, it returns a coinduction rule. |
708 The rule is too big to display in the usual notation; its conclusion is |
710 The rule is too big to display in the usual notation; its conclusion is |
709 $x\in\lleq(A)$ and its premises are $x\in X$, |
711 $x\in\lleq(A)$ and its premises are $x\in X$, |
710 ${X\sbs\llist(A)\times\llist(A)}$ and |
712 ${X\sbs\llist(A)\times\llist(A)}$ and |
711 \[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\, |
713 \[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\, |
712 z=\pair{\LCons(a,l),\LCons(a,l')} \conj |
714 \begin{array}[t]{@{}l} |
713 a\in A \conj\pair{l,l'}\in X\un\lleq(A) \bigr) |
715 z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\ |
714 % \begin{array}[t]{@{}l} |
716 \pair{l,l'}\in X\un\lleq(A) \bigr) |
715 % z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\ |
717 \end{array} |
716 % \pair{l,l'}\in X\un\lleq(A) \bigr) |
|
717 % \end{array} |
|
718 }{[z\in X]_z} |
718 }{[z\in X]_z} |
719 \] |
719 \] |
720 Thus if $x\in X$, where $X$ is a bisimulation contained in the |
720 Thus if $x\in X$, where $X$ is a bisimulation contained in the |
721 domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that |
721 domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that |
722 $\lleq(A)$ is reflexive: the equality relation is a bisimulation. And |
722 $\lleq(A)$ is reflexive: the equality relation is a bisimulation. And |
723 $\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that |
723 $\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that |
724 $\lleq(A)$ coincides with the equality relation takes some work. |
724 $\lleq(A)$ coincides with the equality relation takes some work. |
725 |
725 |
726 \subsection{The accessible part of a relation}\label{acc-sec} |
726 \subsection{The accessible part of a relation}\label{acc-sec} |
727 Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$. |
727 Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$. |
728 The {\bf accessible} or {\bf well-founded} part of~$\prec$, written |
728 The \defn{accessible} or \defn{well-founded} part of~$\prec$, written |
729 $\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits |
729 $\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits |
730 no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is |
730 no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is |
731 inductively defined to be the least set that contains $a$ if it contains |
731 inductively defined to be the least set that contains $a$ if it contains |
732 all $\prec$-predecessors of~$a$, for $a\in D$. Thus we need an |
732 all $\prec$-predecessors of~$a$, for $a\in D$. Thus we need an |
733 introduction rule of the form |
733 introduction rule of the form |
734 \[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \] |
734 \[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \] |
735 Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes |
735 Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes |
736 difficulties for other systems. Its premise is not acceptable to the |
736 difficulties for other systems. Its premise is not acceptable to the |
737 inductive definition package of the Cambridge HOL |
737 inductive definition package of the Cambridge \textsc{hol} |
738 system~\cite{camilleri92}. It is also unacceptable to Isabelle package |
738 system~\cite{camilleri92}. It is also unacceptable to Isabelle package |
739 (recall \S\ref{intro-sec}), but fortunately can be transformed into the |
739 (recall \S\ref{intro-sec}), but fortunately can be transformed into the |
740 acceptable form $t\in M(R)$. |
740 acceptable form $t\in M(R)$. |
741 |
741 |
742 The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to |
742 The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to |
743 $t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To |
743 $t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To |
744 express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a |
744 express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a |
745 term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is |
745 term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is |
746 the inverse image of~$\{a\}$ under~$\prec$. |
746 the inverse image of~$\{a\}$ under~$\prec$. |
747 |
747 |
748 The theory file below follows this approach. Here $r$ is~$\prec$ and |
748 The definition below follows this approach. Here $r$ is~$\prec$ and |
749 $\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a |
749 $\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a |
750 relation is the union of its domain and range.) Finally $r^{-}``\{a\}$ |
750 relation is the union of its domain and range.) Finally $r^{-}``\{a\}$ |
751 denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt |
751 denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt |
752 Pow\_mono}, which asserts that $\pow$ is monotonic. |
752 Pow\_mono}, which asserts that $\pow$ is monotonic. |
753 \begin{ttbox} |
753 \begin{ttbox} |
754 Acc = WF + |
|
755 consts acc :: i=>i |
754 consts acc :: i=>i |
756 inductive |
755 inductive |
757 domains "acc(r)" <= "field(r)" |
756 domains "acc(r)" <= "field(r)" |
758 intrs |
757 intrs |
759 vimage "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)" |
758 vimage "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)" |
760 monos "[Pow_mono]" |
759 monos "[Pow_mono]" |
761 end |
|
762 \end{ttbox} |
760 \end{ttbox} |
763 The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For |
761 The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For |
764 instance, $\prec$ is well-founded if and only if its field is contained in |
762 instance, $\prec$ is well-founded if and only if its field is contained in |
765 $\acc(\prec)$. |
763 $\acc(\prec)$. |
766 |
764 |
767 As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$ |
765 As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$ |
768 gives rise to an unusual induction hypothesis. Let us examine the |
766 gives rise to an unusual induction hypothesis. Let us examine the |
769 induction rule, {\tt Acc.induct}: |
767 induction rule, {\tt acc.induct}: |
770 \[ \infer{P(x)}{x\in\acc(r) & |
768 \[ \infer{P(x)}{x\in\acc(r) & |
771 \infer*{P(a)}{[r^{-}``\{a\}\in\pow(\{z\in\acc(r).P(z)\}) & |
769 \infer*{P(a)}{\left[ |
772 a\in\field(r)]_a}} |
770 \begin{array}{r@{}l} |
|
771 r^{-}``\{a\} &\, \in\pow(\{z\in\acc(r).P(z)\}) \\ |
|
772 a &\, \in\field(r) |
|
773 \end{array} |
|
774 \right]_a}} |
773 \] |
775 \] |
774 The strange induction hypothesis is equivalent to |
776 The strange induction hypothesis is equivalent to |
775 $\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$. |
777 $\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$. |
776 Therefore the rule expresses well-founded induction on the accessible part |
778 Therefore the rule expresses well-founded induction on the accessible part |
777 of~$\prec$. |
779 of~$\prec$. |
792 circumvented by regarding them as functions on lists. Another difficulty, |
794 circumvented by regarding them as functions on lists. Another difficulty, |
793 the notion of composition, is less easily circumvented. |
795 the notion of composition, is less easily circumvented. |
794 |
796 |
795 Here is a more precise definition. Letting $\vec{x}$ abbreviate |
797 Here is a more precise definition. Letting $\vec{x}$ abbreviate |
796 $x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$, |
798 $x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$, |
797 $[y+1,\vec{x}]$, etc. A function is {\bf primitive recursive} if it |
799 $[y+1,\vec{x}]$, etc. A function is \defn{primitive recursive} if it |
798 belongs to the least set of functions in $\lst(\nat)\to\nat$ containing |
800 belongs to the least set of functions in $\lst(\nat)\to\nat$ containing |
799 \begin{itemize} |
801 \begin{itemize} |
800 \item The {\bf successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$. |
802 \item The \defn{successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$. |
801 \item All {\bf constant} functions $\CONST(k)$, such that |
803 \item All \defn{constant} functions $\CONST(k)$, such that |
802 $\CONST(k)[\vec{x}]=k$. |
804 $\CONST(k)[\vec{x}]=k$. |
803 \item All {\bf projection} functions $\PROJ(i)$, such that |
805 \item All \defn{projection} functions $\PROJ(i)$, such that |
804 $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. |
806 $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. |
805 \item All {\bf compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, |
807 \item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, |
806 where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive, |
808 where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive, |
807 such that |
809 such that |
808 \begin{eqnarray*} |
810 \[ \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] = |
809 \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] & = & |
811 g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. \] |
810 g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. |
812 |
811 \end{eqnarray*} |
813 \item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive |
812 |
|
813 \item All {\bf recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive |
|
814 recursive, such that |
814 recursive, such that |
815 \begin{eqnarray*} |
815 \begin{eqnarray*} |
816 \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\ |
816 \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\ |
817 \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}]. |
817 \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}]. |
818 \end{eqnarray*} |
818 \end{eqnarray*} |
842 PROJ "i: nat ==> PROJ(i) : primrec" |
842 PROJ "i: nat ==> PROJ(i) : primrec" |
843 COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec" |
843 COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec" |
844 PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec" |
844 PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec" |
845 monos "[list_mono]" |
845 monos "[list_mono]" |
846 con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]" |
846 con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]" |
847 type_intrs "nat_typechecks @ list.intrs @ \ttback |
847 type_intrs "nat_typechecks @ list.intrs @ |
848 \ttback [lam_type, list_case_type, drop_type, map_type, \ttback |
848 [lam_type, list_case_type, drop_type, map_type, |
849 \ttback apply_type, rec_type]" |
849 apply_type, rec_type]" |
850 end |
850 end |
851 \end{ttbox} |
851 \end{ttbox} |
852 \hrule |
852 \hrule |
853 \caption{Inductive definition of the primitive recursive functions} |
853 \caption{Inductive definition of the primitive recursive functions} |
854 \label{primrec-fig} |
854 \label{primrec-fig} |
855 \end{figure} |
855 \end{figure} |
856 \def\fs{{\it fs}} |
856 \def\fs{{\it fs}} |
857 Szasz was using ALF, but Coq and HOL would also have problems accepting |
857 |
858 this definition. Isabelle's package accepts it easily since |
858 Szasz was using \textsc{alf}, but Coq and \textsc{hol} would also have |
859 $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and |
859 problems accepting this definition. Isabelle's package accepts it easily |
860 $\lst$ is monotonic. There are five introduction rules, one for each of |
860 since $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and |
861 the five forms of primitive recursive function. Let us examine the one for |
861 $\lst$ is monotonic. There are five introduction rules, one for each of the |
862 $\COMP$: |
862 five forms of primitive recursive function. Let us examine the one for |
|
863 $\COMP$: |
863 \[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \] |
864 \[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \] |
864 The induction rule for $\primrec$ has one case for each introduction rule. |
865 The induction rule for $\primrec$ has one case for each introduction rule. |
865 Due to the use of $\lst$ as a monotone operator, the composition case has |
866 Due to the use of $\lst$ as a monotone operator, the composition case has |
866 an unusual induction hypothesis: |
867 an unusual induction hypothesis: |
867 \[ \infer*{P(\COMP(g,\fs))} |
868 \[ \infer*{P(\COMP(g,\fs))} |
874 |
875 |
875 Figure~\ref{primrec-fig} presents the theory file. Theory {\tt Primrec} |
876 Figure~\ref{primrec-fig} presents the theory file. Theory {\tt Primrec} |
876 defines the constants $\SC$, $\CONST$, etc. These are not constructors of |
877 defines the constants $\SC$, $\CONST$, etc. These are not constructors of |
877 a new datatype, but functions over lists of numbers. Their definitions, |
878 a new datatype, but functions over lists of numbers. Their definitions, |
878 most of which are omitted, consist of routine list programming. In |
879 most of which are omitted, consist of routine list programming. In |
879 Isabelle/ZF, the primitive recursive functions are defined as a subset of |
880 Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of |
880 the function set $\lst(\nat)\to\nat$. |
881 the function set $\lst(\nat)\to\nat$. |
881 |
882 |
882 The Isabelle theory goes on to formalize Ackermann's function and prove |
883 The Isabelle theory goes on to formalize Ackermann's function and prove |
883 that it is not primitive recursive, using the induction rule {\tt |
884 that it is not primitive recursive, using the induction rule {\tt |
884 Primrec.induct}. The proof follows Szasz's excellent account. |
885 primrec.induct}. The proof follows Szasz's excellent account. |
885 |
886 |
886 |
887 |
887 \section{Datatypes and codatatypes}\label{data-sec} |
888 \section{Datatypes and codatatypes}\label{data-sec} |
888 A (co)datatype definition is a (co)inductive definition with automatically |
889 A (co)datatype definition is a (co)inductive definition with automatically |
889 defined constructors and a case analysis operator. The package proves that |
890 defined constructors and a case analysis operator. The package proves that |
890 the case operator inverts the constructors and can prove freeness theorems |
891 the case operator inverts the constructors and can prove freeness theorems |
891 involving any pair of constructors. |
892 involving any pair of constructors. |
892 |
893 |
893 |
894 |
894 \subsection{Constructors and their domain}\label{univ-sec} |
895 \subsection{Constructors and their domain}\label{univ-sec} |
895 Conceptually, our two forms of definition are distinct. A (co)inductive |
896 A (co)inductive definition selects a subset of an existing set; a (co)datatype |
896 definition selects a subset of an existing set; a (co)datatype definition |
897 definition creates a new set. The package reduces the latter to the |
897 creates a new set. But the package reduces the latter to the former. A |
898 former. Isabelle/\textsc{zf} supplies sets having strong closure properties to serve |
898 set having strong closure properties must serve as the domain of the |
899 as domains for (co)inductive definitions. |
899 (co)inductive definition. Constructing this set requires some theoretical |
900 |
900 effort, which must be done anyway to show that (co)datatypes exist. It is |
901 Isabelle/\textsc{zf} defines the Cartesian product $A\times |
901 not obvious that standard set theory is suitable for defining codatatypes. |
902 B$, containing ordered pairs $\pair{a,b}$; it also defines the |
902 |
903 disjoint sum $A+B$, containing injections $\Inl(a)\equiv\pair{0,a}$ and |
903 Isabelle/ZF defines the standard notion of Cartesian product $A\times B$, |
904 $\Inr(b)\equiv\pair{1,b}$. For use below, define the $m$-tuple |
904 containing ordered pairs $\pair{a,b}$. Now the $m$-tuple |
905 $\pair{x_1,\ldots,x_m}$ to be the empty set~$\emptyset$ if $m=0$, simply $x_1$ |
905 $\pair{x_1,\ldots,x_m}$ is the empty set~$\emptyset$ if $m=0$, simply |
906 if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$. |
906 $x_1$ if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$. |
907 |
907 Isabelle/ZF also defines the disjoint sum $A+B$, containing injections |
|
908 $\Inl(a)\equiv\pair{0,a}$ and $\Inr(b)\equiv\pair{1,b}$. |
|
909 |
908 |
910 A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be |
909 A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be |
911 $h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$. |
910 $h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$. |
912 In a mutually recursive definition, all constructors for the set~$R_i$ have |
911 In a mutually recursive definition, all constructors for the set~$R_i$ have |
913 the outer form~$h_{in}$, where $h_{in}$ is the injection described |
912 the outer form~$h_{in}$, where $h_{in}$ is the injection described |
914 in~\S\ref{mutual-sec}. Further nested injections ensure that the |
913 in~\S\ref{mutual-sec}. Further nested injections ensure that the |
915 constructors for~$R_i$ are pairwise distinct. |
914 constructors for~$R_i$ are pairwise distinct. |
916 |
915 |
917 Isabelle/ZF defines the set $\univ(A)$, which contains~$A$ and |
916 Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and |
918 furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$, |
917 furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$, |
919 $b\in\univ(A)$. In a typical datatype definition with set parameters |
918 $b\in\univ(A)$. In a typical datatype definition with set parameters |
920 $A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is |
919 $A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is |
921 $\univ(A_1\un\cdots\un A_k)$. This solves the problem for |
920 $\univ(A_1\un\cdots\un A_k)$. This solves the problem for |
922 datatypes~\cite[\S4.2]{paulson-set-II}. |
921 datatypes~\cite[\S4.2]{paulson-set-II}. |
924 The standard pairs and injections can only yield well-founded |
923 The standard pairs and injections can only yield well-founded |
925 constructions. This eases the (manual!) definition of recursive functions |
924 constructions. This eases the (manual!) definition of recursive functions |
926 over datatypes. But they are unsuitable for codatatypes, which typically |
925 over datatypes. But they are unsuitable for codatatypes, which typically |
927 contain non-well-founded objects. |
926 contain non-well-founded objects. |
928 |
927 |
929 To support codatatypes, Isabelle/ZF defines a variant notion of ordered |
928 To support codatatypes, Isabelle/\textsc{zf} defines a variant notion of |
930 pair, written~$\pair{a;b}$. It also defines the corresponding variant |
929 ordered pair, written~$\pair{a;b}$. It also defines the corresponding variant |
931 notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$ |
930 notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$ |
932 and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines |
931 and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines the |
933 the set $\quniv(A)$, which contains~$A$ and furthermore contains |
932 set $\quniv(A)$, which contains~$A$ and furthermore contains $\pair{a;b}$, |
934 $\pair{a;b}$, $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a |
933 $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a typical codatatype |
935 typical codatatype definition with set parameters $A_1$, \ldots, $A_k$, a |
934 definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is |
936 suitable domain is $\quniv(A_1\un\cdots\un A_k)$. This approach using |
935 $\quniv(A_1\un\cdots\un A_k)$. |
937 standard ZF set theory~\cite{paulson-final} is an alternative to adopting |
|
938 Aczel's Anti-Foundation Axiom~\cite{aczel88}. |
|
939 |
936 |
940 \subsection{The case analysis operator} |
937 \subsection{The case analysis operator} |
941 The (co)datatype package automatically defines a case analysis operator, |
938 The (co)datatype package automatically defines a case analysis operator, |
942 called {\tt$R$\_case}. A mutually recursive definition still has only one |
939 called {\tt$R$\_case}. A mutually recursive definition still has only one |
943 operator, whose name combines those of the recursive sets: it is called |
940 operator, whose name combines those of the recursive sets: it is called |
952 \case(f,g,\Inr(y)) & = & g(y) |
949 \case(f,g,\Inr(y)) & = & g(y) |
953 \end{eqnarray*} |
950 \end{eqnarray*} |
954 Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then |
951 Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then |
955 its case operator takes $k+1$ arguments and satisfies an equation for each |
952 its case operator takes $k+1$ arguments and satisfies an equation for each |
956 constructor: |
953 constructor: |
957 \begin{eqnarray*} |
954 \[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}), |
958 R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) & = & f_i(\vec{x}), |
|
959 \qquad i = 1, \ldots, k |
955 \qquad i = 1, \ldots, k |
960 \end{eqnarray*} |
956 \] |
961 The case operator's definition takes advantage of Isabelle's representation |
957 The case operator's definition takes advantage of Isabelle's representation of |
962 of syntax in the typed $\lambda$-calculus; it could readily be adapted to a |
958 syntax in the typed $\lambda$-calculus; it could readily be adapted to a |
963 theorem prover for higher-order logic. If $f$ and~$g$ have meta-type |
959 theorem prover for higher-order logic. If $f$ and~$g$ have meta-type $i\To i$ |
964 $i\To i$ then so do $\split(f)$ and |
960 then so do $\split(f)$ and $\case(f,g)$. This works because $\split$ and |
965 $\case(f,g)$. This works because $\split$ and $\case$ operate on their last |
961 $\case$ operate on their last argument. They are easily combined to make |
966 argument. They are easily combined to make complex case analysis |
962 complex case analysis operators. For example, $\case(f,\case(g,h))$ performs |
967 operators. Here are two examples: |
963 case analysis for $A+(B+C)$; let us verify one of the three equations: |
968 \begin{itemize} |
964 \[ \case(f,\case(g,h), \Inr(\Inl(b))) = \case(g,h,\Inl(b)) = g(b) \] |
969 \item $\split(\lambda x.\split(f(x)))$ performs case analysis for |
|
970 $A\times (B\times C)$, as is easily verified: |
|
971 \begin{eqnarray*} |
|
972 \split(\lambda x.\split(f(x)), \pair{a,b,c}) |
|
973 & = & (\lambda x.\split(f(x))(a,\pair{b,c}) \\ |
|
974 & = & \split(f(a), \pair{b,c}) \\ |
|
975 & = & f(a,b,c) |
|
976 \end{eqnarray*} |
|
977 |
|
978 \item $\case(f,\case(g,h))$ performs case analysis for $A+(B+C)$; let us |
|
979 verify one of the three equations: |
|
980 \begin{eqnarray*} |
|
981 \case(f,\case(g,h), \Inr(\Inl(b))) |
|
982 & = & \case(g,h,\Inl(b)) \\ |
|
983 & = & g(b) |
|
984 \end{eqnarray*} |
|
985 \end{itemize} |
|
986 Codatatype definitions are treated in precisely the same way. They express |
965 Codatatype definitions are treated in precisely the same way. They express |
987 case operators using those for the variant products and sums, namely |
966 case operators using those for the variant products and sums, namely |
988 $\qsplit$ and~$\qcase$. |
967 $\qsplit$ and~$\qcase$. |
989 |
968 |
990 \medskip |
969 \medskip |
991 |
970 |
992 \ifCADE The package has processed all the datatypes discussed in |
|
993 my earlier paper~\cite{paulson-set-II} and the codatatype of lazy lists. |
|
994 Space limitations preclude discussing these examples here, but they are |
|
995 distributed with Isabelle. \typeout{****Omitting datatype examples from |
|
996 CADE version!} \else |
|
997 |
|
998 To see how constructors and the case analysis operator are defined, let us |
971 To see how constructors and the case analysis operator are defined, let us |
999 examine some examples. These include lists and trees/forests, which I have |
972 examine some examples. These include lists and trees/forests, which I have |
1000 discussed extensively in another paper~\cite{paulson-set-II}. |
973 discussed extensively in another paper~\cite{paulson-set-II}. |
1001 |
974 |
1002 |
975 |
1003 \subsection{Example: lists and lazy lists}\label{lists-sec} |
976 \subsection{Example: lists and lazy lists}\label{lists-sec} |
1004 Here is a theory file that declares the datatype of lists: |
977 Here is a declaration of the datatype of lists, as it might appear in a theory |
|
978 file: |
1005 \begin{ttbox} |
979 \begin{ttbox} |
1006 List = Datatype + |
|
1007 consts list :: i=>i |
980 consts list :: i=>i |
1008 datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)") |
981 datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)") |
1009 end |
|
1010 \end{ttbox} |
982 \end{ttbox} |
1011 And here is the theory file that declares the codatatype of lazy lists: |
983 And here is a declaration of the codatatype of lazy lists: |
1012 \begin{ttbox} |
984 \begin{ttbox} |
1013 LList = Datatype + |
|
1014 consts llist :: i=>i |
985 consts llist :: i=>i |
1015 codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)") |
986 codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)") |
1016 end |
|
1017 \end{ttbox} |
987 \end{ttbox} |
1018 They highlight the (many) similarities and (few) differences between |
|
1019 datatype and codatatype definitions.\footnote{The real theory files contain |
|
1020 many more declarations, mainly of functions over lists; the declaration |
|
1021 of lazy lists is followed by the coinductive definition of lazy list |
|
1022 equality.} |
|
1023 |
988 |
1024 Each form of list has two constructors, one for the empty list and one for |
989 Each form of list has two constructors, one for the empty list and one for |
1025 adding an element to a list. Each takes a parameter, defining the set of |
990 adding an element to a list. Each takes a parameter, defining the set of |
1026 lists over a given set~$A$. Each specifies {\tt Datatype} as the parent |
991 lists over a given set~$A$. Each requires {\tt Datatype} as a parent theory; |
1027 theory; this implicitly specifies {\tt Univ} and {\tt QUniv} as ancestors, |
992 this makes available the definitions of $\univ$ and $\quniv$. Each is |
1028 making available the definitions of $\univ$ and $\quniv$. Each is |
993 automatically given the appropriate domain: $\univ(A)$ for $\lst(A)$ and |
1029 automatically given the appropriate domain: |
994 $\quniv(A)$ for $\llist(A)$. The default can be overridden. |
1030 \begin{itemize} |
|
1031 \item $\lst(A)$ uses the domain $\univ(A)$ (the default choice can be |
|
1032 overridden). |
|
1033 |
|
1034 \item $\llist(A)$ uses the domain $\quniv(A)$. |
|
1035 \end{itemize} |
|
1036 |
995 |
1037 Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt |
996 Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt |
1038 List.induct}: |
997 list.induct}: |
1039 \[ \infer{P(x)}{x\in\lst(A) & P(\Nil) |
998 \[ \infer{P(x)}{x\in\lst(A) & P(\Nil) |
1040 & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } |
999 & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } |
1041 \] |
1000 \] |
1042 Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this, |
1001 Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this, |
1043 Isabelle/ZF defines the rank of a set and proves that the standard pairs and |
1002 Isabelle/\textsc{zf} defines the rank of a set and proves that the standard pairs and |
1044 injections have greater rank than their components. An immediate consequence, |
1003 injections have greater rank than their components. An immediate consequence, |
1045 which justifies structural recursion on lists \cite[\S4.3]{paulson-set-II}, |
1004 which justifies structural recursion on lists \cite[\S4.3]{paulson-set-II}, |
1046 is |
1005 is |
1047 \[ \rank(l) < \rank(\Cons(a,l)). \] |
1006 \[ \rank(l) < \rank(\Cons(a,l)). \] |
1048 |
1007 |
1049 Since $\llist(A)$ is a codatatype, it has no induction rule. Instead it has |
1008 Since $\llist(A)$ is a codatatype, it has no induction rule. Instead it has |
1050 the coinduction rule shown in \S\ref{coind-sec}. Since variant pairs and |
1009 the coinduction rule shown in \S\ref{coind-sec}. Since variant pairs and |
1051 injections are monotonic and need not have greater rank than their |
1010 injections are monotonic and need not have greater rank than their |
1052 components, fixedpoint operators can create cyclic constructions. For |
1011 components, fixedpoint operators can create cyclic constructions. For |
1053 example, the definition |
1012 example, the definition |
1054 \begin{eqnarray*} |
1013 \[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \] |
1055 \lconst(a) & \equiv & \lfp(\univ(a), \lambda l. \LCons(a,l)) |
|
1056 \end{eqnarray*} |
|
1057 yields $\lconst(a) = \LCons(a,\lconst(a))$. |
1014 yields $\lconst(a) = \LCons(a,\lconst(a))$. |
1058 |
1015 |
1059 \medskip |
1016 \medskip |
1060 It may be instructive to examine the definitions of the constructors and |
1017 It may be instructive to examine the definitions of the constructors and |
1061 case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar. |
1018 case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar. |
1143 \Fnil & = & \Inr(\Inl(\emptyset)) \\ |
1093 \Fnil & = & \Inr(\Inl(\emptyset)) \\ |
1144 \Fcons(a,l) & = & \Inr(\Inr(\pair{a,l})) |
1094 \Fcons(a,l) & = & \Inr(\Inr(\pair{a,l})) |
1145 \end{eqnarray*} |
1095 \end{eqnarray*} |
1146 There is only one case operator; it works on the union of the trees and |
1096 There is only one case operator; it works on the union of the trees and |
1147 forests: |
1097 forests: |
1148 \begin{eqnarray*} |
1098 \[ {\tt tree\_forest\_case}(f,c,g) \equiv |
1149 {\tt tree\_forest\_case}(f,c,g) & \equiv & |
1099 \case(\split(f),\, \case(\lambda u.c, \split(g))) \] |
1150 \case(\split(f),\, \case(\lambda u.c, \split(g))) |
|
1151 \end{eqnarray*} |
|
1152 |
1100 |
1153 |
1101 |
1154 \subsection{A four-constructor datatype} |
1102 \subsection{A four-constructor datatype} |
1155 Finally let us consider a fairly general datatype. It has four |
1103 Finally let us consider a fairly general datatype. It has four |
1156 constructors $\Con_0$, \ldots, $\Con_3$, with the corresponding arities. |
1104 constructors $\Con_0$, \ldots, $\Con_3$, with the corresponding arities. |
1157 \begin{ttbox} |
1105 \begin{ttbox} |
1158 Data = Datatype + |
|
1159 consts data :: [i,i] => i |
1106 consts data :: [i,i] => i |
1160 datatype "data(A,B)" = Con0 |
1107 datatype "data(A,B)" = Con0 |
1161 | Con1 ("a: A") |
1108 | Con1 ("a: A") |
1162 | Con2 ("a: A", "b: B") |
1109 | Con2 ("a: A", "b: B") |
1163 | Con3 ("a: A", "b: B", "d: data(A,B)") |
1110 | Con3 ("a: A", "b: B", "d: data(A,B)") |
1164 end |
|
1165 \end{ttbox} |
1111 \end{ttbox} |
1166 Because this datatype has two set parameters, $A$ and~$B$, the package |
1112 Because this datatype has two set parameters, $A$ and~$B$, the package |
1167 automatically supplies $\univ(A\un B)$ as its domain. The structural |
1113 automatically supplies $\univ(A\un B)$ as its domain. The structural |
1168 induction rule has four minor premises, one per constructor: |
1114 induction rule has four minor premises, one per constructor, and only the last |
1169 \[ \infer{P(x)}{x\in\data(A,B) & |
1115 has an induction hypothesis. (Details are left to the reader.) |
1170 P(\Con_0) & |
|
1171 \infer*{P(\Con_1(a))}{[a\in A]_a} & |
|
1172 \infer*{P(\Con_2(a,b))} |
|
1173 {\left[\begin{array}{l} a\in A \\ b\in B \end{array} |
|
1174 \right]_{a,b}} & |
|
1175 \infer*{P(\Con_3(a,b,d))} |
|
1176 {\left[\begin{array}{l} a\in A \\ b\in B \\ |
|
1177 d\in\data(A,B) \\ P(d) |
|
1178 \end{array} |
|
1179 \right]_{a,b,d}} } |
|
1180 \] |
|
1181 |
1116 |
1182 The constructor definitions are |
1117 The constructor definitions are |
1183 \begin{eqnarray*} |
1118 \begin{eqnarray*} |
1184 \Con_0 & = & \Inl(\Inl(\emptyset)) \\ |
1119 \Con_0 & = & \Inl(\Inl(\emptyset)) \\ |
1185 \Con_1(a) & = & \Inl(\Inr(a)) \\ |
1120 \Con_1(a) & = & \Inl(\Inr(a)) \\ |
1186 \Con_2(a,b) & = & \Inr(\Inl(\pair{a,b})) \\ |
1121 \Con_2(a,b) & = & \Inr(\Inl(\pair{a,b})) \\ |
1187 \Con_3(a,b,c) & = & \Inr(\Inr(\pair{a,b,c})). |
1122 \Con_3(a,b,c) & = & \Inr(\Inr(\pair{a,b,c})). |
1188 \end{eqnarray*} |
1123 \end{eqnarray*} |
1189 The case operator is |
1124 The case operator is |
1190 \begin{eqnarray*} |
1125 \[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv |
1191 {\tt data\_case}(f_0,f_1,f_2,f_3) & \equiv & |
|
1192 \case(\begin{array}[t]{@{}l} |
1126 \case(\begin{array}[t]{@{}l} |
1193 \case(\lambda u.f_0,\; f_1),\, \\ |
1127 \case(\lambda u.f_0,\; f_1),\, \\ |
1194 \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) ) |
1128 \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) ) |
1195 \end{array} |
1129 \end{array} |
1196 \end{eqnarray*} |
1130 \] |
1197 This may look cryptic, but the case equations are trivial to verify. |
1131 This may look cryptic, but the case equations are trivial to verify. |
1198 |
1132 |
1199 In the constructor definitions, the injections are balanced. A more naive |
1133 In the constructor definitions, the injections are balanced. A more naive |
1200 approach is to define $\Con_3(a,b,c)$ as |
1134 approach is to define $\Con_3(a,b,c)$ as |
1201 $\Inr(\Inr(\Inr(\pair{a,b,c})))$; instead, each constructor has two |
1135 $\Inr(\Inr(\Inr(\pair{a,b,c})))$; instead, each constructor has two |
1202 injections. The difference here is small. But the ZF examples include a |
1136 injections. The difference here is small. But the \textsc{zf} examples include a |
1203 60-element enumeration type, where each constructor has 5 or~6 injections. |
1137 60-element enumeration type, where each constructor has 5 or~6 injections. |
1204 The naive approach would require 1 to~59 injections; the definitions would be |
1138 The naive approach would require 1 to~59 injections; the definitions would be |
1205 quadratic in size. It is like the difference between the binary and unary |
1139 quadratic in size. It is like the difference between the binary and unary |
1206 numeral systems. |
1140 numeral systems. |
1207 |
1141 |
1208 The result structure contains the case operator and constructor definitions as |
1142 The result structure contains the case operator and constructor definitions as |
1209 the theorem list \verb|con_defs|. It contains the case equations, such as |
1143 the theorem list \verb|con_defs|. It contains the case equations, such as |
1210 \begin{eqnarray*} |
1144 \[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \] |
1211 {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) & = & f_3(a,b,c), |
|
1212 \end{eqnarray*} |
|
1213 as the theorem list \verb|case_eqns|. There is one equation per constructor. |
1145 as the theorem list \verb|case_eqns|. There is one equation per constructor. |
1214 |
1146 |
1215 \subsection{Proving freeness theorems} |
1147 \subsection{Proving freeness theorems} |
1216 There are two kinds of freeness theorems: |
1148 There are two kinds of freeness theorems: |
1217 \begin{itemize} |
1149 \begin{itemize} |
1218 \item {\bf injectiveness} theorems, such as |
1150 \item \defn{injectiveness} theorems, such as |
1219 \[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \] |
1151 \[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \] |
1220 |
1152 |
1221 \item {\bf distinctness} theorems, such as |
1153 \item \defn{distinctness} theorems, such as |
1222 \[ \Con_1(a) \not= \Con_2(a',b') \] |
1154 \[ \Con_1(a) \not= \Con_2(a',b') \] |
1223 \end{itemize} |
1155 \end{itemize} |
1224 Since the number of such theorems is quadratic in the number of constructors, |
1156 Since the number of such theorems is quadratic in the number of constructors, |
1225 the package does not attempt to prove them all. Instead it returns tools for |
1157 the package does not attempt to prove them all. Instead it returns tools for |
1226 proving desired theorems --- either explicitly or `on the fly' during |
1158 proving desired theorems --- either manually or during |
1227 simplification or classical reasoning. |
1159 simplification or classical reasoning. |
1228 |
1160 |
1229 The theorem list \verb|free_iffs| enables the simplifier to perform freeness |
1161 The theorem list \verb|free_iffs| enables the simplifier to perform freeness |
1230 reasoning. This works by incremental unfolding of constructors that appear in |
1162 reasoning. This works by incremental unfolding of constructors that appear in |
1231 equations. The theorem list contains logical equivalences such as |
1163 equations. The theorem list contains logical equivalences such as |
1247 Such incremental unfolding combines freeness reasoning with other proof |
1179 Such incremental unfolding combines freeness reasoning with other proof |
1248 steps. It has the unfortunate side-effect of unfolding definitions of |
1180 steps. It has the unfortunate side-effect of unfolding definitions of |
1249 constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should |
1181 constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should |
1250 be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs} |
1182 be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs} |
1251 restores the defined constants. |
1183 restores the defined constants. |
1252 \fi %CADE |
1184 |
1253 |
1185 |
1254 \section{Related work}\label{related} |
1186 \section{Related work}\label{related} |
1255 The use of least fixedpoints to express inductive definitions seems |
1187 The use of least fixedpoints to express inductive definitions seems |
1256 obvious. Why, then, has this technique so seldom been implemented? |
1188 obvious. Why, then, has this technique so seldom been implemented? |
1257 |
1189 |
1258 Most automated logics can only express inductive definitions by asserting |
1190 Most automated logics can only express inductive definitions by asserting |
1259 new axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if |
1191 new axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if |
1260 their shell principle were removed. With ALF the situation is more |
1192 their shell principle were removed. With \textsc{alf} the situation is more |
1261 complex; earlier versions of Martin-L\"of's type theory could (using |
1193 complex; earlier versions of Martin-L\"of's type theory could (using |
1262 wellordering types) express datatype definitions, but the version |
1194 wellordering types) express datatype definitions, but the version |
1263 underlying ALF requires new rules for each definition~\cite{dybjer91}. |
1195 underlying \textsc{alf} requires new rules for each definition~\cite{dybjer91}. |
1264 With Coq the situation is subtler still; its underlying Calculus of |
1196 With Coq the situation is subtler still; its underlying Calculus of |
1265 Constructions can express inductive definitions~\cite{huet88}, but cannot |
1197 Constructions can express inductive definitions~\cite{huet88}, but cannot |
1266 quite handle datatype definitions~\cite{paulin92}. It seems that |
1198 quite handle datatype definitions~\cite{paulin92}. It seems that |
1267 researchers tried hard to circumvent these problems before finally |
1199 researchers tried hard to circumvent these problems before finally |
1268 extending the Calculus with rule schemes for strictly positive operators. |
1200 extending the Calculus with rule schemes for strictly positive operators. |
1269 |
1201 |
1270 Higher-order logic can express inductive definitions through quantification |
1202 Higher-order logic can express inductive definitions through quantification |
1271 over unary predicates. The following formula expresses that~$i$ belongs to the |
1203 over unary predicates. The following formula expresses that~$i$ belongs to the |
1272 least set containing~0 and closed under~$\succ$: |
1204 least set containing~0 and closed under~$\succ$: |
1273 \[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \] |
1205 \[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \] |
1274 This technique can be used to prove the Knaster-Tarski Theorem, but it is |
1206 This technique can be used to prove the Knaster-Tarski theorem, which (in its |
1275 little used in the Cambridge HOL system. Melham~\cite{melham89} clearly |
1207 general form) is little used in the Cambridge \textsc{hol} system. |
1276 describes the development. The natural numbers are defined as shown above, |
1208 Melham~\cite{melham89} describes the development. The natural numbers are |
1277 but lists are defined as functions over the natural numbers. Unlabelled |
1209 defined as shown above, but lists are defined as functions over the natural |
1278 trees are defined using G\"odel numbering; a labelled tree consists of an |
1210 numbers. Unlabelled trees are defined using G\"odel numbering; a labelled |
1279 unlabelled tree paired with a list of labels. Melham's datatype package |
1211 tree consists of an unlabelled tree paired with a list of labels. Melham's |
1280 expresses the user's datatypes in terms of labelled trees. It has been |
1212 datatype package expresses the user's datatypes in terms of labelled trees. |
1281 highly successful, but a fixedpoint approach might have yielded greater |
1213 It has been highly successful, but a fixedpoint approach might have yielded |
1282 functionality with less effort. |
1214 greater power with less effort. |
1283 |
1215 |
1284 Melham's inductive definition package~\cite{camilleri92} uses |
1216 Melham's inductive definition package~\cite{camilleri92} also uses |
1285 quantification over predicates, which is implicitly a fixedpoint approach. |
1217 quantification over predicates. But instead of formalizing the notion of |
1286 Instead of formalizing the notion of monotone function, it requires |
1218 monotone function, it requires definitions to consist of finitary rules, a |
1287 definitions to consist of finitary rules, a syntactic form that excludes |
1219 syntactic form that excludes many monotone inductive definitions. |
1288 many monotone inductive definitions. |
1220 |
1289 |
1221 The earliest use of least fixedpoints is probably Robin Milner's. Brian |
1290 The earliest use of least fixedpoints is probably Robin Milner's datatype |
1222 Monahan extended this package considerably~\cite{monahan84}, as did I in |
1291 package for Edinburgh LCF~\cite{milner-ind}. Brian Monahan extended this |
1223 unpublished work.\footnote{The datatype package described in my \textsc{lcf} |
1292 package considerably~\cite{monahan84}, as did I in unpublished |
1224 book~\cite{paulson87} does {\it not\/} make definitions, but merely asserts |
1293 work.\footnote{The datatype package described in my LCF |
1225 axioms.} \textsc{lcf} is a first-order logic of domain theory; the relevant |
1294 book~\cite{paulson87} does {\it not\/} make definitions, but merely |
1226 fixedpoint theorem is not Knaster-Tarski but concerns fixedpoints of |
1295 asserts axioms.} |
1227 continuous functions over domains. \textsc{lcf} is too weak to express |
1296 LCF is a first-order logic of domain theory; the relevant fixedpoint |
1228 recursive predicates. The Isabelle package might be the first to be based on |
1297 theorem is not Knaster-Tarski but concerns fixedpoints of continuous |
1229 the Knaster-Tarski theorem. |
1298 functions over domains. LCF is too weak to express recursive predicates. |
|
1299 Thus it would appear that the Isabelle package is the first to be based |
|
1300 on the Knaster-Tarski Theorem. |
|
1301 |
1230 |
1302 |
1231 |
1303 \section{Conclusions and future work} |
1232 \section{Conclusions and future work} |
1304 Higher-order logic and set theory are both powerful enough to express |
1233 Higher-order logic and set theory are both powerful enough to express |
1305 inductive definitions. A growing number of theorem provers implement one |
1234 inductive definitions. A growing number of theorem provers implement one |
1307 definition package to write is one that asserts new axioms, not one that |
1236 definition package to write is one that asserts new axioms, not one that |
1308 makes definitions and proves theorems about them. But asserting axioms |
1237 makes definitions and proves theorems about them. But asserting axioms |
1309 could introduce unsoundness. |
1238 could introduce unsoundness. |
1310 |
1239 |
1311 The fixedpoint approach makes it fairly easy to implement a package for |
1240 The fixedpoint approach makes it fairly easy to implement a package for |
1312 (co)inductive definitions that does not assert axioms. It is efficient: it |
1241 (co)in\-duc\-tive definitions that does not assert axioms. It is efficient: |
1313 processes most definitions in seconds and even a 60-constructor datatype |
1242 it processes most definitions in seconds and even a 60-constructor datatype |
1314 requires only two minutes. It is also simple: the package consists of |
1243 requires only a few minutes. It is also simple: The first working version took |
1315 under 1100 lines (35K bytes) of Standard ML code. The first working |
1244 under a week to code, consisting of under 1100 lines (35K bytes) of Standard |
1316 version took under a week to code. |
1245 \textsc{ml}. |
1317 |
1246 |
1318 In set theory, care is required to ensure that the inductive definition |
1247 In set theory, care is needed to ensure that the inductive definition yields |
1319 yields a set (rather than a proper class). This problem is inherent to set |
1248 a set (rather than a proper class). This problem is inherent to set theory, |
1320 theory, whether or not the Knaster-Tarski Theorem is employed. We must |
1249 whether or not the Knaster-Tarski theorem is employed. We must exhibit a |
1321 exhibit a bounding set (called a domain above). For inductive definitions, |
1250 bounding set (called a domain above). For inductive definitions, this is |
1322 this is often trivial. For datatype definitions, I have had to formalize |
1251 often trivial. For datatype definitions, I have had to formalize much set |
1323 much set theory. To justify infinitely branching datatype definitions, I |
1252 theory. To justify infinitely branching datatype definitions, I have had to |
1324 have had to develop a theory of cardinal arithmetic, such as the theorem |
1253 develop a theory of cardinal arithmetic~\cite{paulson-gr}, such as the theorem |
1325 that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for |
1254 that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for all |
1326 all $\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$. |
1255 $\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$. |
1327 The need for such efforts is not a drawback of the fixedpoint |
1256 The need for such efforts is not a drawback of the fixedpoint approach, for |
1328 approach, for the alternative is to take such definitions on faith. |
1257 the alternative is to take such definitions on faith. |
1329 |
1258 |
1330 Inductive and datatype definitions can take up considerable storage. The |
1259 Care is also needed to ensure that the greatest fixedpoint really yields a |
1331 introduction rules are replicated in slightly different forms as fixedpoint |
1260 coinductive definition. In set theory, standard pairs admit only well-founded |
1332 definitions, elimination rules and induction rules. Here are two examples. |
1261 constructions. Aczel's anti-foundation axiom~\cite{aczel88} could be used to |
1333 Three datatypes and three inductive definitions specify the operational |
1262 get non-well-founded objects, but it does not seem easy to mechanize. |
1334 semantics of a simple imperative language; they occupy over 600K in total. |
1263 Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which |
1335 One datatype definition, an enumeration type with 60 constructors, requires |
1264 can be generalized to a variant notion of function. Elsewhere I have |
1336 nearly 560K\@. |
1265 proved that this simple approach works (yielding final coalgebras) for a broad |
1337 |
1266 class of definitions~\cite{paulson-final}. |
1338 The approach is not restricted to set theory. It should be suitable for |
1267 |
1339 any logic that has some notion of set and the Knaster-Tarski Theorem. I |
1268 Several large studies make heavy use of inductive definitions. L\"otzbeyer |
1340 have ported the (co)inductive definition package from Isabelle/ZF to |
1269 and Sandner have formalized two chapters of a semantics book~\cite{winskel93}, |
1341 Isabelle/HOL (higher-order logic). I hope to port the (co)datatype package |
1270 proving the equivalence between the operational and denotational semantics of |
1342 later. HOL represents sets by unary predicates; defining the corresponding |
1271 a simple imperative language. A single theory file contains three datatype |
1343 types may cause complications. |
1272 definitions (of arithmetic expressions, boolean expressions and commands) and |
1344 |
1273 three inductive definitions (the corresponding operational rules). Using |
1345 |
1274 different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95} |
|
1275 have both proved the Church-Rosser theorem. A datatype specifies the set of |
|
1276 $\lambda$-terms, while inductive definitions specify several reduction |
|
1277 relations. |
|
1278 |
|
1279 To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the |
|
1280 consistency of the dynamic and static semantics for a small functional |
|
1281 language. The example is due to Milner and Tofte~\cite{milner-coind}. It |
|
1282 concerns an extended correspondence relation, which is defined coinductively. |
|
1283 A codatatype definition specifies values and value environments in mutual |
|
1284 recursion. Non-well-founded values represent recursive functions. Value |
|
1285 environments are variant functions from variables into values. This one key |
|
1286 definition uses most of the package's novel features. |
|
1287 |
|
1288 The approach is not restricted to set theory. It should be suitable for any |
|
1289 logic that has some notion of set and the Knaster-Tarski theorem. I have |
|
1290 ported the (co)inductive definition package from Isabelle/\textsc{zf} to |
|
1291 Isabelle/\textsc{hol} (higher-order logic). V\"olker~\cite{voelker95} |
|
1292 is investigating how to port the (co)datatype package. \textsc{hol} |
|
1293 represents sets by unary predicates; defining the corresponding types may |
|
1294 cause complications. |
|
1295 |
|
1296 |
|
1297 \begin{footnotesize} |
1346 \bibliographystyle{springer} |
1298 \bibliographystyle{springer} |
1347 \bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref} |
1299 \bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref} |
|
1300 \end{footnotesize} |
1348 %%%%%\doendnotes |
1301 %%%%%\doendnotes |
1349 |
1302 |
1350 \ifCADE\typeout{****Omitting appendices from CADE version!} |
1303 \ifshort\typeout{****Omitting appendices from short version!} |
1351 \else |
1304 \else |
1352 \newpage |
1305 \newpage |
1353 \appendix |
1306 \appendix |
1354 \section{Inductive and coinductive definitions: users guide} |
1307 \section{Inductive and coinductive definitions: users guide} |
1355 A theory file may contain any number of inductive and coinductive |
1308 A theory file may contain any number of inductive and coinductive |
1356 definitions. They may be intermixed with other declarations; in |
1309 definitions. They may be intermixed with other declarations; in |
1357 particular, the (co)inductive sets {\bf must} be declared separately as |
1310 particular, the (co)inductive sets \defn{must} be declared separately as |
1358 constants, and may have mixfix syntax or be subject to syntax translations. |
1311 constants, and may have mixfix syntax or be subject to syntax translations. |
1359 |
1312 |
1360 Each (co)inductive definition adds definitions to the theory and also |
1313 Each (co)inductive definition adds definitions to the theory and also proves |
1361 proves some theorems. Each definition creates an ML structure, which is a |
1314 some theorems. Each definition creates an \textsc{ml} structure, which is a |
1362 substructure of the main theory structure. |
1315 substructure of the main theory structure. |
|
1316 |
|
1317 Inductive and datatype definitions can take up considerable storage. The |
|
1318 introduction rules are replicated in slightly different forms as fixedpoint |
|
1319 definitions, elimination rules and induction rules. L\"otzbeyer and Sandner's |
|
1320 six definitions occupy over 600K in total. Defining the 60-constructor |
|
1321 datatype requires nearly 560K\@. |
1363 |
1322 |
1364 \subsection{The result structure} |
1323 \subsection{The result structure} |
1365 Many of the result structure's components have been discussed |
1324 Many of the result structure's components have been discussed |
1366 in~\S\ref{basic-sec}; others are self-explanatory. |
1325 in~\S\ref{basic-sec}; others are self-explanatory. |
1367 \begin{description} |
1326 \begin{description} |