author  paulson 
Fri, 27 Nov 1998 13:13:22 +0100  
changeset 5980  2e9314c07146 
parent 4276  a770eae2cdb0 
permissions  rwrr 
104  1 
%%%%Currently UNDOCUMENTED lowlevel 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 \verball T is the universal quantifier for type {\tt T}\@. 

12 

13 
The term \verbequals 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 welltyped. 

27 

28 

29 
Calling \verbsubst_bounds$([u_{n1},\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_{n1} \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 
\verbsubst_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 \verbterm_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. Firstorder pattern matching is used 

51 
to implement metalevel rewriting. 

52 

53 

54 
\subsection{The representation of objectrules} 

55 
The module {\tt Logic} contains operations concerned with inference  

56 
especially, for constructing and destructing terms that represent 

57 
objectrules. 

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 flexflex constraints to an objectrule. 

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 objectrule: 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 objectrule 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_{i1},\ldots, \phi_1], \phi)\), 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
327
diff
changeset

165 
where $\phi$ need not be atomic. Raises an exception if $i$ is out of 
104  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 

4276  231 
unifiers: env * ((term*term)list) > (env * (term*term)list) Seq.seq 
104  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 flexflex pairs (these are discussed below). 

238 

239 
\beginprog 

4276  240 
smash_unifiers: env * (term*term)list > env Seq.seq 
104  241 
\endprog 
242 
This unification function maps an environment and a list of disagreement 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
327
diff
changeset

243 
pairs to a sequence of updated environments. The function obliterates 
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
327
diff
changeset

244 
flexflex pairs by choosing the obvious unifier. It may be used to tidy up 
104  245 
any flexflex 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 flexflex 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]{paulsonbook}.) 

267 

268 