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 
\index{loose_bnos}


26 
\beginprog


27 
loose_bnos: term > int list


28 
\endprog


29 
Calling \verbloose_bnos t returns the list of all 'loose' bound variable


30 
references. In particular, {\tt Bound~0} is loose unless it is enclosed in


31 
an abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in


32 
at least two abstractions; if enclosed in just one, the list will contain


33 
the number 0. A wellformed term does not contain any loose variables.


34 


35 
Calling {\prog{}type_of \${t}}\index{type_of} computes the type of the


36 
term~$t$. Raises exception {\tt TYPE} unless applications are welltyped.


37 


38 
\index{aconv}


39 
\beginprog


40 
op aconv: term*term > bool


41 
\endprog


42 
Calling $t\Term{ aconv }u$ tests whether terms~$t$ and~$u$ are


43 
\(\alpha\)convertible: identical up to renaming of bound variables.


44 
\begin{itemize}


45 
\item


46 
Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)convertible


47 
just when their names and types are equal.


48 
(Variables having the same name but different types are thus distinct.


49 
This confusing situation should be avoided!)


50 
\item


51 
Two bound variables are \(\alpha\)convertible


52 
just when they have the same number.


53 
\item


54 
Two abstractions are \(\alpha\)convertible


55 
just when their bodies are, and their bound variables have the same type.


56 
\item


57 
Two applications are \(\alpha\)convertible


58 
just when the corresponding subterms are.


59 
\end{itemize}


60 


61 


62 
\index{incr_boundvars}


63 
\beginprog


64 
incr_boundvars: int > term > term


65 
\endprog


66 
This increments a term's `loose' bound variables by a given offset,


67 
required when moving a subterm into a context


68 
where it is enclosed by a different number of lambdas.


69 


70 
\index{abstract_over}


71 
\beginprog


72 
abstract_over: term*term > term


73 
\endprog


74 
For abstracting a term over a subterm \(v\):


75 
replaces every occurrence of \(v\) by a {\tt Bound} variable


76 
with the correct index.


77 


78 
Calling \verbsubst_bounds$([u_{n1},\ldots,u_0],\,t)$\index{subst_bounds}


79 
substitutes the $u_i$ for loose bound variables in $t$. This achieves


80 
\(\beta\)reduction of \(u_{n1} \cdots u_0\) into $t$, replacing {\tt


81 
Bound~i} with $u_i$. For \((\lambda x y.t)(u,v)\), the bound variable


82 
indices in $t$ are $x:1$ and $y:0$. The appropriate call is


83 
\verbsubst_bounds([v,u],t). Loose bound variables $\geq n$ are reduced


84 
by $n$ to compensate for the disappearance of $n$ lambdas.


85 


86 
\index{maxidx_of_term}


87 
\beginprog


88 
maxidx_of_term: term > int


89 
\endprog


90 
Computes the maximum index of all the {\tt Var}s in a term.


91 
If there are no {\tt Var}s, the result is \(1\).


92 


93 
\index{term_match}


94 
\beginprog


95 
term_match: (term*term)list * term*term > (term*term)list


96 
\endprog


97 
Calling \verbterm_match(vts,t,u) instantiates {\tt Var}s in {\tt t} to


98 
match it with {\tt u}. The resulting list of variable/term pairs extends


99 
{\tt vts}, which is typically empty. Firstorder pattern matching is used


100 
to implement metalevel rewriting.


101 


102 


103 
\subsection{The representation of objectrules}


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


105 
especially, for constructing and destructing terms that represent


106 
objectrules.


107 


108 
\index{occs}


109 
\beginprog


110 
op occs: term*term > bool


111 
\endprog


112 
Does one term occur in the other?


113 
(This is a reflexive relation.)


114 


115 
\index{add_term_vars}


116 
\beginprog


117 
add_term_vars: term*term list > term list


118 
\endprog


119 
Accumulates the {\tt Var}s in the term, suppressing duplicates.


120 
The second argument should be the list of {\tt Var}s found so far.


121 


122 
\index{add_term_frees}


123 
\beginprog


124 
add_term_frees: term*term list > term list


125 
\endprog


126 
Accumulates the {\tt Free}s in the term, suppressing duplicates.


127 
The second argument should be the list of {\tt Free}s found so far.


128 


129 
\index{mk_equals}


130 
\beginprog


131 
mk_equals: term*term > term


132 
\endprog


133 
Given $t$ and $u$ makes the term $t\equiv u$.


134 


135 
\index{dest_equals}


136 
\beginprog


137 
dest_equals: term > term*term


138 
\endprog


139 
Given $t\equiv u$ returns the pair $(t,u)$.


140 


141 
\index{list_implies:}


142 
\beginprog


143 
list_implies: term list * term > term


144 
\endprog


145 
Given the pair $([\phi_1,\ldots, \phi_m], \phi)$


146 
makes the term \([\phi_1;\ldots; \phi_m] \Imp \phi\).


147 


148 
\index{strip_imp_prems}


149 
\beginprog


150 
strip_imp_prems: term > term list


151 
\endprog


152 
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)


153 
returns the list \([\phi_1,\ldots, \phi_m]\).


154 


155 
\index{strip_imp_concl}


156 
\beginprog


157 
strip_imp_concl: term > term


158 
\endprog


159 
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)


160 
returns the term \(\phi\).


161 


162 
\index{list_equals}


163 
\beginprog


164 
list_equals: (term*term)list * term > term


165 
\endprog


166 
For adding flexflex constraints to an objectrule.


167 
Given $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$,


168 
makes the term \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\).


169 


170 
\index{strip_equals}


171 
\beginprog


172 
strip_equals: term > (term*term) list * term


173 
\endprog


174 
Given \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\),


175 
returns $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$.


176 


177 
\index{rule_of}


178 
\beginprog


179 
rule_of: (term*term)list * term list * term > term


180 
\endprog


181 
Makes an objectrule: given the triple


182 
\[ ([(t_1,u_1),\ldots, (t_k,u_k)], [\phi_1,\ldots, \phi_m], \phi) \]


183 
returns the term


184 
\([t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m]\Imp \phi\)


185 


186 
\index{strip_horn}


187 
\beginprog


188 
strip_horn: term > (term*term)list * term list * term


189 
\endprog


190 
Breaks an objectrule into its parts: given


191 
\[ [t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m] \Imp \phi \]


192 
returns the triple


193 
\(([(t_k,u_k),\ldots, (t_1,u_1)], [\phi_1,\ldots, \phi_m], \phi).\)


194 


195 
\index{strip_assums}


196 
\beginprog


197 
strip_assums: term > (term*int) list * (string*typ) list * term


198 
\endprog


199 
Strips premises of a rule allowing a more general form,


200 
where $\Forall$ and $\Imp$ may be intermixed.


201 
This is typical of assumptions of a subgoal in natural deduction.


202 
Returns additional information about the number, names,


203 
and types of quantified variables.


204 


205 


206 
\index{strip_prems}


207 
\beginprog


208 
strip_prems: int * term list * term > term list * term


209 
\endprog


210 
For finding premise (or subgoal) $i$: given the triple


211 
\( (i, [], \phi_1;\ldots \phi_i\Imp \phi) \)


212 
it returns another triple,


213 
\((\phi_i, [\phi_{i1},\ldots, \phi_1], \phi)\),


214 
where $\phi$ need not be atomic. Raises an exception if $i$ is out of


215 
range.


216 


217 


218 
\subsection{Environments}


219 
The module {\tt Envir} (which is normally closed)


220 
declares a type of environments.


221 
An environment holds variable assignments


222 
and the next index to use when generating a variable.


223 
\par\indent\vbox{\small \begin{verbatim}


224 
datatype env = Envir of {asol: term xolist, maxidx: int}


225 
\end{verbatim}}


226 
The operations of lookup, update, and generation of variables


227 
are used during unification.


228 


229 
\beginprog


230 
empty: int>env


231 
\endprog


232 
Creates the environment with no assignments


233 
and the given index.


234 


235 
\beginprog


236 
lookup: env * indexname > term option


237 
\endprog


238 
Looks up a variable, specified by its indexname,


239 
and returns {\tt None} or {\tt Some} as appropriate.


240 


241 
\beginprog


242 
update: (indexname * term) * env > env


243 
\endprog


244 
Given a variable, term, and environment,


245 
produces {\em a new environment\/} where the variable has been updated.


246 
This has no side effect on the given environment.


247 


248 
\beginprog


249 
genvar: env * typ > env * term


250 
\endprog


251 
Generates a variable of the given type and returns it,


252 
paired with a new environment (with incremented {\tt maxidx} field).


253 


254 
\beginprog


255 
alist_of: env > (indexname * term) list


256 
\endprog


257 
Converts an environment into an association list


258 
containing the assignments.


259 


260 
\beginprog


261 
norm_term: env > term > term


262 
\endprog


263 


264 
Copies a term,


265 
following assignments in the environment,


266 
and performing all possible \(\beta\)reductions.


267 


268 
\beginprog


269 
rewrite: (env * (term*term)list) > term > term


270 
\endprog


271 
Rewrites a term using the given term pairs as rewrite rules. Assignments


272 
are ignored; the environment is used only with {\tt genvar}, to generate


273 
unique {\tt Var}s as placeholders for bound variables.


274 


275 


276 
\subsection{The unification functions}


277 


278 


279 
\beginprog


280 
unifiers: env * ((term*term)list) > (env * (term*term)list) seq


281 
\endprog


282 
This is the main unification function.


283 
Given an environment and a list of disagreement pairs,


284 
it returns a sequence of outcomes.


285 
Each outcome consists of an updated environment and


286 
a list of flexflex pairs (these are discussed below).


287 


288 
\beginprog


289 
smash_unifiers: env * (term*term)list > env seq


290 
\endprog


291 
This unification function maps an environment and a list of disagreement


292 
pairs to a sequence of updated environments. The function obliterates


293 
flexflex pairs by choosing the obvious unifier. It may be used to tidy up


294 
any flexflex pairs remaining at the end of a proof.


295 


296 
\subsubsection{Flexibleflexible disagreement pairs}


297 


298 


299 
\subsubsection{Multiple unifiers}


300 
The unification procedure performs Huet's {\sc match} operation


301 
\cite{huet75} in big steps.


302 
It solves \(\Var{f}(t_1,\ldots,t_p) \equiv u\) for \(\Var{f}\) by finding


303 
all ways of copying \(u\), first trying projection on the arguments


304 
\(t_i\). It never copies below any variable in \(u\); instead it returns a


305 
new variable, resulting in a flexflex disagreement pair.


306 


307 


308 
\beginprog


309 
type_assign: cterm > cterm


310 
\endprog


311 
Produces a cterm by updating the signature of its argument


312 
to include all variable/type assignments.


313 
Type inference under the resulting signature will assume the


314 
same type assignments as in the argument.


315 
This is used in the goal package to give persistence to type assignments


316 
within each proof.


317 
(Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulsonbook}.)


318 


319 
