104
|
1 |
%%%%Currently UNDOCUMENTED low-level functions! from previous manual
|
|
2 |
|
|
3 |
%%%%Low level information about terms and module Logic.
|
|
4 |
%%%%Mainly used for implementation of Pure.
|
|
5 |
|
|
6 |
%move to ML sources?
|
|
7 |
|
|
8 |
\subsection{Basic declarations}
|
|
9 |
The implication symbol is {\tt implies}.
|
|
10 |
|
|
11 |
The term \verb|all T| is the universal quantifier for type {\tt T}\@.
|
|
12 |
|
|
13 |
The term \verb|equals T| is the equality predicate for type {\tt T}\@.
|
|
14 |
|
|
15 |
|
|
16 |
There are a number of basic functions on terms and types.
|
|
17 |
|
|
18 |
\index{--->}
|
|
19 |
\beginprog
|
|
20 |
op ---> : typ list * typ -> typ
|
|
21 |
\endprog
|
|
22 |
Given types \([ \tau_1, \ldots, \tau_n]\) and \(\tau\), it
|
|
23 |
forms the type \(\tau_1\to \cdots \to (\tau_n\to\tau)\).
|
|
24 |
|
|
25 |
Calling {\prog{}type_of \${t}}\index{type_of} computes the type of the
|
|
26 |
term~$t$. Raises exception {\tt TYPE} unless applications are well-typed.
|
|
27 |
|
|
28 |
|
|
29 |
Calling \verb|subst_bounds|$([u_{n-1},\ldots,u_0],\,t)$\index{subst_bounds}
|
|
30 |
substitutes the $u_i$ for loose bound variables in $t$. This achieves
|
|
31 |
\(\beta\)-reduction of \(u_{n-1} \cdots u_0\) into $t$, replacing {\tt
|
|
32 |
Bound~i} with $u_i$. For \((\lambda x y.t)(u,v)\), the bound variable
|
|
33 |
indices in $t$ are $x:1$ and $y:0$. The appropriate call is
|
|
34 |
\verb|subst_bounds([v,u],t)|. Loose bound variables $\geq n$ are reduced
|
|
35 |
by $n$ to compensate for the disappearance of $n$ lambdas.
|
|
36 |
|
|
37 |
\index{maxidx_of_term}
|
|
38 |
\beginprog
|
|
39 |
maxidx_of_term: term -> int
|
|
40 |
\endprog
|
|
41 |
Computes the maximum index of all the {\tt Var}s in a term.
|
|
42 |
If there are no {\tt Var}s, the result is \(-1\).
|
|
43 |
|
|
44 |
\index{term_match}
|
|
45 |
\beginprog
|
|
46 |
term_match: (term*term)list * term*term -> (term*term)list
|
|
47 |
\endprog
|
|
48 |
Calling \verb|term_match(vts,t,u)| instantiates {\tt Var}s in {\tt t} to
|
|
49 |
match it with {\tt u}. The resulting list of variable/term pairs extends
|
|
50 |
{\tt vts}, which is typically empty. First-order pattern matching is used
|
|
51 |
to implement meta-level rewriting.
|
|
52 |
|
|
53 |
|
|
54 |
\subsection{The representation of object-rules}
|
|
55 |
The module {\tt Logic} contains operations concerned with inference ---
|
|
56 |
especially, for constructing and destructing terms that represent
|
|
57 |
object-rules.
|
|
58 |
|
|
59 |
\index{occs}
|
|
60 |
\beginprog
|
|
61 |
op occs: term*term -> bool
|
|
62 |
\endprog
|
|
63 |
Does one term occur in the other?
|
|
64 |
(This is a reflexive relation.)
|
|
65 |
|
|
66 |
\index{add_term_vars}
|
|
67 |
\beginprog
|
|
68 |
add_term_vars: term*term list -> term list
|
|
69 |
\endprog
|
|
70 |
Accumulates the {\tt Var}s in the term, suppressing duplicates.
|
|
71 |
The second argument should be the list of {\tt Var}s found so far.
|
|
72 |
|
|
73 |
\index{add_term_frees}
|
|
74 |
\beginprog
|
|
75 |
add_term_frees: term*term list -> term list
|
|
76 |
\endprog
|
|
77 |
Accumulates the {\tt Free}s in the term, suppressing duplicates.
|
|
78 |
The second argument should be the list of {\tt Free}s found so far.
|
|
79 |
|
|
80 |
\index{mk_equals}
|
|
81 |
\beginprog
|
|
82 |
mk_equals: term*term -> term
|
|
83 |
\endprog
|
|
84 |
Given $t$ and $u$ makes the term $t\equiv u$.
|
|
85 |
|
|
86 |
\index{dest_equals}
|
|
87 |
\beginprog
|
|
88 |
dest_equals: term -> term*term
|
|
89 |
\endprog
|
|
90 |
Given $t\equiv u$ returns the pair $(t,u)$.
|
|
91 |
|
|
92 |
\index{list_implies:}
|
|
93 |
\beginprog
|
|
94 |
list_implies: term list * term -> term
|
|
95 |
\endprog
|
|
96 |
Given the pair $([\phi_1,\ldots, \phi_m], \phi)$
|
|
97 |
makes the term \([\phi_1;\ldots; \phi_m] \Imp \phi\).
|
|
98 |
|
|
99 |
\index{strip_imp_prems}
|
|
100 |
\beginprog
|
|
101 |
strip_imp_prems: term -> term list
|
|
102 |
\endprog
|
|
103 |
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
|
|
104 |
returns the list \([\phi_1,\ldots, \phi_m]\).
|
|
105 |
|
|
106 |
\index{strip_imp_concl}
|
|
107 |
\beginprog
|
|
108 |
strip_imp_concl: term -> term
|
|
109 |
\endprog
|
|
110 |
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
|
|
111 |
returns the term \(\phi\).
|
|
112 |
|
|
113 |
\index{list_equals}
|
|
114 |
\beginprog
|
|
115 |
list_equals: (term*term)list * term -> term
|
|
116 |
\endprog
|
|
117 |
For adding flex-flex constraints to an object-rule.
|
|
118 |
Given $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$,
|
|
119 |
makes the term \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\).
|
|
120 |
|
|
121 |
\index{strip_equals}
|
|
122 |
\beginprog
|
|
123 |
strip_equals: term -> (term*term) list * term
|
|
124 |
\endprog
|
|
125 |
Given \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\),
|
|
126 |
returns $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$.
|
|
127 |
|
|
128 |
\index{rule_of}
|
|
129 |
\beginprog
|
|
130 |
rule_of: (term*term)list * term list * term -> term
|
|
131 |
\endprog
|
|
132 |
Makes an object-rule: given the triple
|
|
133 |
\[ ([(t_1,u_1),\ldots, (t_k,u_k)], [\phi_1,\ldots, \phi_m], \phi) \]
|
|
134 |
returns the term
|
|
135 |
\([t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m]\Imp \phi\)
|
|
136 |
|
|
137 |
\index{strip_horn}
|
|
138 |
\beginprog
|
|
139 |
strip_horn: term -> (term*term)list * term list * term
|
|
140 |
\endprog
|
|
141 |
Breaks an object-rule into its parts: given
|
|
142 |
\[ [t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m] \Imp \phi \]
|
|
143 |
returns the triple
|
|
144 |
\(([(t_k,u_k),\ldots, (t_1,u_1)], [\phi_1,\ldots, \phi_m], \phi).\)
|
|
145 |
|
|
146 |
\index{strip_assums}
|
|
147 |
\beginprog
|
|
148 |
strip_assums: term -> (term*int) list * (string*typ) list * term
|
|
149 |
\endprog
|
|
150 |
Strips premises of a rule allowing a more general form,
|
|
151 |
where $\Forall$ and $\Imp$ may be intermixed.
|
|
152 |
This is typical of assumptions of a subgoal in natural deduction.
|
|
153 |
Returns additional information about the number, names,
|
|
154 |
and types of quantified variables.
|
|
155 |
|
|
156 |
|
|
157 |
\index{strip_prems}
|
|
158 |
\beginprog
|
|
159 |
strip_prems: int * term list * term -> term list * term
|
|
160 |
\endprog
|
|
161 |
For finding premise (or subgoal) $i$: given the triple
|
|
162 |
\( (i, [], \phi_1;\ldots \phi_i\Imp \phi) \)
|
|
163 |
it returns another triple,
|
|
164 |
\((\phi_i, [\phi_{i-1},\ldots, \phi_1], \phi)\),
|
|
165 |
where $\phi$ need not be atomic. Raises an exception if $i$ is out of
|
|
166 |
range.
|
|
167 |
|
|
168 |
|
|
169 |
\subsection{Environments}
|
|
170 |
The module {\tt Envir} (which is normally closed)
|
|
171 |
declares a type of environments.
|
|
172 |
An environment holds variable assignments
|
|
173 |
and the next index to use when generating a variable.
|
|
174 |
\par\indent\vbox{\small \begin{verbatim}
|
|
175 |
datatype env = Envir of {asol: term xolist, maxidx: int}
|
|
176 |
\end{verbatim}}
|
|
177 |
The operations of lookup, update, and generation of variables
|
|
178 |
are used during unification.
|
|
179 |
|
|
180 |
\beginprog
|
|
181 |
empty: int->env
|
|
182 |
\endprog
|
|
183 |
Creates the environment with no assignments
|
|
184 |
and the given index.
|
|
185 |
|
|
186 |
\beginprog
|
|
187 |
lookup: env * indexname -> term option
|
|
188 |
\endprog
|
|
189 |
Looks up a variable, specified by its indexname,
|
|
190 |
and returns {\tt None} or {\tt Some} as appropriate.
|
|
191 |
|
|
192 |
\beginprog
|
|
193 |
update: (indexname * term) * env -> env
|
|
194 |
\endprog
|
|
195 |
Given a variable, term, and environment,
|
|
196 |
produces {\em a new environment\/} where the variable has been updated.
|
|
197 |
This has no side effect on the given environment.
|
|
198 |
|
|
199 |
\beginprog
|
|
200 |
genvar: env * typ -> env * term
|
|
201 |
\endprog
|
|
202 |
Generates a variable of the given type and returns it,
|
|
203 |
paired with a new environment (with incremented {\tt maxidx} field).
|
|
204 |
|
|
205 |
\beginprog
|
|
206 |
alist_of: env -> (indexname * term) list
|
|
207 |
\endprog
|
|
208 |
Converts an environment into an association list
|
|
209 |
containing the assignments.
|
|
210 |
|
|
211 |
\beginprog
|
|
212 |
norm_term: env -> term -> term
|
|
213 |
\endprog
|
|
214 |
|
|
215 |
Copies a term,
|
|
216 |
following assignments in the environment,
|
|
217 |
and performing all possible \(\beta\)-reductions.
|
|
218 |
|
|
219 |
\beginprog
|
|
220 |
rewrite: (env * (term*term)list) -> term -> term
|
|
221 |
\endprog
|
|
222 |
Rewrites a term using the given term pairs as rewrite rules. Assignments
|
|
223 |
are ignored; the environment is used only with {\tt genvar}, to generate
|
|
224 |
unique {\tt Var}s as placeholders for bound variables.
|
|
225 |
|
|
226 |
|
|
227 |
\subsection{The unification functions}
|
|
228 |
|
|
229 |
|
|
230 |
\beginprog
|
|
231 |
unifiers: env * ((term*term)list) -> (env * (term*term)list) seq
|
|
232 |
\endprog
|
|
233 |
This is the main unification function.
|
|
234 |
Given an environment and a list of disagreement pairs,
|
|
235 |
it returns a sequence of outcomes.
|
|
236 |
Each outcome consists of an updated environment and
|
|
237 |
a list of flex-flex pairs (these are discussed below).
|
|
238 |
|
|
239 |
\beginprog
|
|
240 |
smash_unifiers: env * (term*term)list -> env seq
|
|
241 |
\endprog
|
|
242 |
This unification function maps an environment and a list of disagreement
|
|
243 |
pairs to a sequence of updated environments. The function obliterates
|
|
244 |
flex-flex pairs by choosing the obvious unifier. It may be used to tidy up
|
|
245 |
any flex-flex pairs remaining at the end of a proof.
|
|
246 |
|
|
247 |
|
|
248 |
\subsubsection{Multiple unifiers}
|
|
249 |
The unification procedure performs Huet's {\sc match} operation
|
|
250 |
\cite{huet75} in big steps.
|
|
251 |
It solves \(\Var{f}(t_1,\ldots,t_p) \equiv u\) for \(\Var{f}\) by finding
|
|
252 |
all ways of copying \(u\), first trying projection on the arguments
|
|
253 |
\(t_i\). It never copies below any variable in \(u\); instead it returns a
|
|
254 |
new variable, resulting in a flex-flex disagreement pair.
|
|
255 |
|
|
256 |
|
|
257 |
\beginprog
|
|
258 |
type_assign: cterm -> cterm
|
|
259 |
\endprog
|
|
260 |
Produces a cterm by updating the signature of its argument
|
|
261 |
to include all variable/type assignments.
|
|
262 |
Type inference under the resulting signature will assume the
|
|
263 |
same type assignments as in the argument.
|
|
264 |
This is used in the goal package to give persistence to type assignments
|
|
265 |
within each proof.
|
|
266 |
(Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulson-book}.)
|
|
267 |
|
|
268 |
|