equal
deleted
inserted
replaced
5 section{* The General Construction Principle \label{sec:ind-general-method} *} |
5 section{* The General Construction Principle \label{sec:ind-general-method} *} |
6 |
6 |
7 text {* |
7 text {* |
8 |
8 |
9 Before we start with the implementation, it is useful to describe the general |
9 Before we start with the implementation, it is useful to describe the general |
10 form of inductive definitions that our package should accept. We closely follow |
10 form of inductive definitions that our package should accept. |
11 the notation for inductive definitions introduced by Schwichtenberg |
11 Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be |
12 \cite{Schwichtenberg-MLCF} for the Minlog system. |
12 some fixed parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have |
13 Let $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be |
|
14 parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have |
|
15 the form |
13 the form |
16 |
14 |
17 \[ |
15 \[ |
18 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
16 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
19 R_{k_{ij}}~\vec{p}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow R_{l_i}~\vec{p}~\vec{t}_i |
17 R_{k_{ij}}~\vec{p}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow R_{l_i}~\vec{p}~\vec{t}_i |
22 |
20 |
23 where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$. |
21 where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$. |
24 Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure |
22 Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure |
25 that all occurrences of the predicates in the premises of the introduction rules are |
23 that all occurrences of the predicates in the premises of the introduction rules are |
26 \emph{strictly positive}. This condition guarantees the existence of predicates |
24 \emph{strictly positive}. This condition guarantees the existence of predicates |
27 that are closed under the introduction rules shown above. The inductive predicates |
25 that are closed under the introduction rules shown above. Then the definitions of the |
28 $R_1,\ldots,R_n$ can then be defined as follows: |
26 inductive predicates $R_1,\ldots,R_n$ is: |
29 |
27 |
30 \[ |
28 \[ |
31 \begin{array}{l@ {\qquad}l} |
29 \begin{array}{l@ {\qquad}l} |
32 R_i \equiv \lambda\vec{p}~\vec{z}_i.~\forall P_1 \ldots P_n.~K_1 \longrightarrow \cdots \longrightarrow K_r \longrightarrow P_i~\vec{z}_i & |
30 R_i \equiv \lambda\vec{p}~\vec{z}_i.~\forall P_1 \ldots P_n.~K_1 \longrightarrow \cdots \longrightarrow K_r \longrightarrow P_i~\vec{z}_i & |
33 \mbox{for\ } i=1,\ldots,n \\[1.5ex] |
31 \mbox{for\ } i=1,\ldots,n \\[1.5ex] |