doc-src/Logics/Old_HOL.tex
changeset 9695 ec7d7f877712
parent 2975 230f456956a2
     1.1 --- a/doc-src/Logics/Old_HOL.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/Logics/Old_HOL.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -3,33 +3,32 @@
     1.4  \index{higher-order logic|(}
     1.5  \index{HOL system@{\sc hol} system}
     1.6  
     1.7 -The theory~\thydx{HOL} implements higher-order logic.
     1.8 -It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is
     1.9 -based on Church's original paper~\cite{church40}.  Andrews's
    1.10 -book~\cite{andrews86} is a full description of higher-order logic.
    1.11 -Experience with the {\sc hol} system has demonstrated that higher-order
    1.12 -logic is useful for hardware verification; beyond this, it is widely
    1.13 -applicable in many areas of mathematics.  It is weaker than {\ZF} set
    1.14 -theory but for most applications this does not matter.  If you prefer {\ML}
    1.15 -to Lisp, you will probably prefer \HOL\ to~{\ZF}.
    1.16 +The theory~\thydx{HOL} implements higher-order logic.  It is based on
    1.17 +Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
    1.18 +Church's original paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a
    1.19 +full description of higher-order logic.  Experience with the {\sc hol} system
    1.20 +has demonstrated that higher-order logic is useful for hardware verification;
    1.21 +beyond this, it is widely applicable in many areas of mathematics.  It is
    1.22 +weaker than ZF set theory but for most applications this does not matter.  If
    1.23 +you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
    1.24  
    1.25 -Previous releases of Isabelle included a different version of~\HOL, with
    1.26 +Previous releases of Isabelle included a different version of~HOL, with
    1.27  explicit type inference rules~\cite{paulson-COLOG}.  This version no longer
    1.28  exists, but \thydx{ZF} supports a similar style of reasoning.
    1.29  
    1.30 -\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
    1.31 -identifies object-level types with meta-level types, taking advantage of
    1.32 -Isabelle's built-in type checker.  It identifies object-level functions
    1.33 -with meta-level functions, so it uses Isabelle's operations for abstraction
    1.34 -and application.  There is no `apply' operator: function applications are
    1.35 -written as simply~$f(a)$ rather than $f{\tt`}a$.
    1.36 +HOL has a distinct feel, compared with ZF and CTT.  It identifies object-level
    1.37 +types with meta-level types, taking advantage of Isabelle's built-in type
    1.38 +checker.  It identifies object-level functions with meta-level functions, so
    1.39 +it uses Isabelle's operations for abstraction and application.  There is no
    1.40 +`apply' operator: function applications are written as simply~$f(a)$ rather
    1.41 +than $f{\tt`}a$.
    1.42  
    1.43 -These identifications allow Isabelle to support \HOL\ particularly nicely,
    1.44 -but they also mean that \HOL\ requires more sophistication from the user
    1.45 ---- in particular, an understanding of Isabelle's type system.  Beginners
    1.46 -should work with {\tt show_types} set to {\tt true}.  Gain experience by
    1.47 -working in first-order logic before attempting to use higher-order logic.
    1.48 -This chapter assumes familiarity with~{\FOL{}}.
    1.49 +These identifications allow Isabelle to support HOL particularly nicely, but
    1.50 +they also mean that HOL requires more sophistication from the user --- in
    1.51 +particular, an understanding of Isabelle's type system.  Beginners should work
    1.52 +with {\tt show_types} set to {\tt true}.  Gain experience by working in
    1.53 +first-order logic before attempting to use higher-order logic.  This chapter
    1.54 +assumes familiarity with~FOL.
    1.55  
    1.56  
    1.57  \begin{figure} 
    1.58 @@ -115,7 +114,7 @@
    1.59           & | & "EX!~" id~id^* " . " formula
    1.60    \end{array}
    1.61  \]
    1.62 -\caption{Full grammar for \HOL} \label{hol-grammar}
    1.63 +\caption{Full grammar for HOL} \label{hol-grammar}
    1.64  \end{figure} 
    1.65  
    1.66  
    1.67 @@ -140,7 +139,7 @@
    1.68  $\neg(a=b)$.
    1.69  
    1.70  \begin{warn}
    1.71 -  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
    1.72 +  HOL has no if-and-only-if connective; logical equivalence is expressed
    1.73    using equality.  But equality has a high priority, as befitting a
    1.74    relation, while if-and-only-if typically has the lowest priority.  Thus,
    1.75    $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
    1.76 @@ -155,7 +154,7 @@
    1.77  belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
    1.78  over functions.
    1.79  
    1.80 -Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
    1.81 +Types in HOL must be non-empty; otherwise the quantifier rules would be
    1.82  unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
    1.83  
    1.84  \index{type definitions}
    1.85 @@ -178,11 +177,10 @@
    1.86  
    1.87  \subsection{Binders}
    1.88  Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
    1.89 -satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
    1.90 -something, a description is always meaningful, but we do not know its value
    1.91 -unless $P[x]$ defines it uniquely.  We may write descriptions as
    1.92 -\cdx{Eps}($P$) or use the syntax
    1.93 -\hbox{\tt \at $x$.$P[x]$}.
    1.94 +satisfying~$P[a]$, if such exists.  Since all terms in HOL denote something, a
    1.95 +description is always meaningful, but we do not know its value unless $P[x]$
    1.96 +defines it uniquely.  We may write descriptions as \cdx{Eps}($P$) or use the
    1.97 +syntax \hbox{\tt \at $x$.$P[x]$}.
    1.98  
    1.99  Existential quantification is defined by
   1.100  \[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]
   1.101 @@ -193,14 +191,14 @@
   1.102  exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
   1.103  
   1.104  \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
   1.105 -Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
   1.106 +Quantifiers have two notations.  As in Gordon's {\sc hol} system, HOL
   1.107  uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
   1.108  existential quantifier must be followed by a space; thus {\tt?x} is an
   1.109  unknown, while \verb'? x.f(x)=y' is a quantification.  Isabelle's usual
   1.110 -notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
   1.111 -available.  Both notations are accepted for input.  The {\ML} reference
   1.112 +notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also available.  Both
   1.113 +notations are accepted for input.  The {\ML} reference
   1.114  \ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt
   1.115 -true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
   1.116 +  true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
   1.117  to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
   1.118  
   1.119  All these binders have priority 10. 
   1.120 @@ -212,7 +210,7 @@
   1.121  the constant~\cdx{Let}.  It can be expanded by rewriting with its
   1.122  definition, \tdx{Let_def}.
   1.123  
   1.124 -\HOL\ also defines the basic syntax
   1.125 +HOL also defines the basic syntax
   1.126  \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
   1.127  as a uniform means of expressing {\tt case} constructs.  Therefore {\tt
   1.128    case} and \sdx{of} are reserved words.  However, so far this is mere
   1.129 @@ -259,8 +257,8 @@
   1.130  
   1.131  
   1.132  \section{Rules of inference}
   1.133 -Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
   1.134 -their~{\ML} names.  Some of the rules deserve additional comments:
   1.135 +Figure~\ref{hol-rules} shows the inference rules of~HOL, with their~{\ML}
   1.136 +names.  Some of the rules deserve additional comments:
   1.137  \begin{ttdescription}
   1.138  \item[\tdx{ext}] expresses extensionality of functions.
   1.139  \item[\tdx{iff}] asserts that logically equivalent formulae are
   1.140 @@ -273,14 +271,14 @@
   1.141      shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
   1.142  \end{ttdescription}
   1.143  
   1.144 -\HOL{} follows standard practice in higher-order logic: only a few
   1.145 -connectives are taken as primitive, with the remainder defined obscurely
   1.146 +HOL follows standard practice in higher-order logic: only a few connectives
   1.147 +are taken as primitive, with the remainder defined obscurely
   1.148  (Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
   1.149  corresponding definitions \cite[page~270]{mgordon-hol} using
   1.150 -object-equality~({\tt=}), which is possible because equality in
   1.151 -higher-order logic may equate formulae and even functions over formulae.
   1.152 -But theory~\HOL{}, like all other Isabelle theories, uses
   1.153 -meta-equality~({\tt==}) for definitions.
   1.154 +object-equality~({\tt=}), which is possible because equality in higher-order
   1.155 +logic may equate formulae and even functions over formulae.  But theory~HOL,
   1.156 +like all other Isabelle theories, uses meta-equality~({\tt==}) for
   1.157 +definitions.
   1.158  
   1.159  Some of the rules mention type variables; for
   1.160  example, {\tt refl} mentions the type variable~{\tt'a}.  This allows you to
   1.161 @@ -344,7 +342,7 @@
   1.162  \subcaption{Logical equivalence}
   1.163  
   1.164  \end{ttbox}
   1.165 -\caption{Derived rules for \HOL} \label{hol-lemmas1}
   1.166 +\caption{Derived rules for HOL} \label{hol-lemmas1}
   1.167  \end{figure}
   1.168  
   1.169  
   1.170 @@ -521,8 +519,8 @@
   1.171  \section{A formulation of set theory}
   1.172  Historically, higher-order logic gives a foundation for Russell and
   1.173  Whitehead's theory of classes.  Let us use modern terminology and call them
   1.174 -{\bf sets}, but note that these sets are distinct from those of {\ZF} set
   1.175 -theory, and behave more like {\ZF} classes.
   1.176 +{\bf sets}, but note that these sets are distinct from those of ZF set theory,
   1.177 +and behave more like ZF classes.
   1.178  \begin{itemize}
   1.179  \item
   1.180  Sets are given by predicates over some type~$\sigma$.  Types serve to
   1.181 @@ -534,20 +532,19 @@
   1.182  Although sets may contain other sets as elements, the containing set must
   1.183  have a more complex type.
   1.184  \end{itemize}
   1.185 -Finite unions and intersections have the same behaviour in \HOL\ as they
   1.186 -do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
   1.187 -denoting the universal set for the given type.
   1.188 +Finite unions and intersections have the same behaviour in HOL as they do
   1.189 +in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the
   1.190 +universal set for the given type.
   1.191  
   1.192  
   1.193  \subsection{Syntax of set theory}\index{*set type}
   1.194 -\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
   1.195 -essentially the same as $\alpha\To bool$.  The new type is defined for
   1.196 -clarity and to avoid complications involving function types in unification.
   1.197 -Since Isabelle does not support type definitions (as mentioned in
   1.198 -\S\ref{HOL-types}), the isomorphisms between the two types are declared
   1.199 -explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
   1.200 -$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
   1.201 -argument order).
   1.202 +HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is essentially
   1.203 +the same as $\alpha\To bool$.  The new type is defined for clarity and to
   1.204 +avoid complications involving function types in unification.  Since Isabelle
   1.205 +does not support type definitions (as mentioned in \S\ref{HOL-types}), the
   1.206 +isomorphisms between the two types are declared explicitly.  Here they are
   1.207 +natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt
   1.208 +  op :} maps in the other direction (ignoring argument order).
   1.209  
   1.210  Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
   1.211  translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
   1.212 @@ -563,11 +560,11 @@
   1.213    {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
   1.214  \end{eqnarray*}
   1.215  
   1.216 -The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
   1.217 -that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
   1.218 -occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda
   1.219 -x.P[x])$.  It defines sets by absolute comprehension, which is impossible
   1.220 -in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
   1.221 +The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type) that
   1.222 +satisfy~$P[x]$, where $P[x]$ is a formula that may contain free occurrences
   1.223 +of~$x$.  This syntax expands to \cdx{Collect}$(\lambda x.P[x])$.  It defines
   1.224 +sets by absolute comprehension, which is impossible in~ZF; the type of~$x$
   1.225 +implicitly restricts the comprehension.
   1.226  
   1.227  The set theory defines two {\bf bounded quantifiers}:
   1.228  \begin{eqnarray*}
   1.229 @@ -811,14 +808,13 @@
   1.230  
   1.231  
   1.232  Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
   1.233 -obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
   1.234 -such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
   1.235 -are designed for classical reasoning; the rules \tdx{subsetD},
   1.236 -\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
   1.237 -strictly necessary but yield more natural proofs.  Similarly,
   1.238 -\tdx{equalityCE} supports classical reasoning about extensionality,
   1.239 -after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
   1.240 -proofs pertaining to set theory.
   1.241 +obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such
   1.242 +as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
   1.243 +reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
   1.244 +not strictly necessary but yield more natural proofs.  Similarly,
   1.245 +\tdx{equalityCE} supports classical reasoning about extensionality, after the
   1.246 +fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for proofs pertaining
   1.247 +to set theory.
   1.248  
   1.249  Figure~\ref{hol-fun} presents derived inference rules involving functions.
   1.250  They also include rules for \cdx{Inv}, which is defined in theory~{\tt
   1.251 @@ -905,13 +901,12 @@
   1.252  
   1.253  
   1.254  \section{Generic packages and classical reasoning}
   1.255 -\HOL\ instantiates most of Isabelle's generic packages;
   1.256 -see {\tt HOL/ROOT.ML} for details.
   1.257 +HOL instantiates most of Isabelle's generic packages; see {\tt HOL/ROOT.ML}
   1.258 +for details.
   1.259  \begin{itemize}
   1.260 -\item 
   1.261 -Because it includes a general substitution rule, \HOL\ instantiates the
   1.262 -tactic {\tt hyp_subst_tac}, which substitutes for an equality
   1.263 -throughout a subgoal and its hypotheses.
   1.264 +\item Because it includes a general substitution rule, HOL instantiates the
   1.265 +  tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
   1.266 +  subgoal and its hypotheses.
   1.267  \item 
   1.268  It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
   1.269  simplification set for higher-order logic.  Equality~($=$), which also
   1.270 @@ -921,14 +916,14 @@
   1.271  \item 
   1.272  It instantiates the classical reasoner, as described below. 
   1.273  \end{itemize}
   1.274 -\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
   1.275 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
   1.276 -rule; recall Fig.\ts\ref{hol-lemmas2} above.
   1.277 +HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
   1.278 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
   1.279 +Fig.\ts\ref{hol-lemmas2} above.
   1.280  
   1.281 -The classical reasoner is set up as the structure
   1.282 -{\tt Classical}.  This structure is open, so {\ML} identifiers such
   1.283 -as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
   1.284 -\HOL\ defines the following classical rule sets:
   1.285 +The classical reasoner is set up as the structure {\tt Classical}.  This
   1.286 +structure is open, so {\ML} identifiers such as {\tt step_tac}, {\tt
   1.287 +  fast_tac}, {\tt best_tac}, etc., refer to it.  HOL defines the following
   1.288 +classical rule sets:
   1.289  \begin{ttbox} 
   1.290  prop_cs    : claset
   1.291  HOL_cs     : claset
   1.292 @@ -1075,13 +1070,12 @@
   1.293  called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described
   1.294  similar constructions in the context of set theory~\cite{paulson-set-II}.
   1.295  
   1.296 -Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
   1.297 -overloads $<$ and $\leq$ on the natural numbers.  As of this writing,
   1.298 -Isabelle provides no means of verifying that such overloading is sensible;
   1.299 -there is no means of specifying the operators' properties and verifying
   1.300 -that instances of the operators satisfy those properties.  To be safe, the
   1.301 -\HOL\ theory includes no polymorphic axioms asserting general properties of
   1.302 -$<$ and~$\leq$.
   1.303 +Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which overloads
   1.304 +$<$ and $\leq$ on the natural numbers.  As of this writing, Isabelle provides
   1.305 +no means of verifying that such overloading is sensible; there is no means of
   1.306 +specifying the operators' properties and verifying that instances of the
   1.307 +operators satisfy those properties.  To be safe, the HOL theory includes no
   1.308 +polymorphic axioms asserting general properties of $<$ and~$\leq$.
   1.309  
   1.310  Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
   1.311  defines addition, multiplication, subtraction, division, and remainder.
   1.312 @@ -1190,9 +1184,9 @@
   1.313  \subsection{The type constructor for lists, {\tt list}}
   1.314  \index{*list type}
   1.315  
   1.316 -\HOL's definition of lists is an example of an experimental method for
   1.317 -handling recursive data types.  Figure~\ref{hol-list} presents the theory
   1.318 -\thydx{List}: the basic list operations with their types and properties.
   1.319 +HOL's definition of lists is an example of an experimental method for handling
   1.320 +recursive data types.  Figure~\ref{hol-list} presents the theory \thydx{List}:
   1.321 +the basic list operations with their types and properties.
   1.322  
   1.323  The \sdx{case} construct is defined by the following translation:
   1.324  {\dquotes
   1.325 @@ -1740,8 +1734,8 @@
   1.326  proves the two equivalent.  It contains several datatype and inductive
   1.327  definitions, and demonstrates their use.
   1.328  
   1.329 -Directory {\tt HOL/ex} contains other examples and experimental proofs in
   1.330 -{\HOL}.  Here is an overview of the more interesting files.
   1.331 +Directory {\tt HOL/ex} contains other examples and experimental proofs in HOL.
   1.332 +Here is an overview of the more interesting files.
   1.333  \begin{itemize}
   1.334  \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
   1.335    predicate calculus theorems, ranging from simple tautologies to
   1.336 @@ -1770,12 +1764,12 @@
   1.337    as filter, which can compute indefinitely before yielding the next
   1.338    element (if any!) of the lazy list.  A coinduction principle is defined
   1.339    for proving equations on lazy lists.
   1.340 -
   1.341 -\item Theory {\tt PropLog} proves the soundness and completeness of
   1.342 -  classical propositional logic, given a truth table semantics.  The only
   1.343 -  connective is $\imp$.  A Hilbert-style axiom system is specified, and its
   1.344 -  set of theorems defined inductively.  A similar proof in \ZF{} is
   1.345 -  described elsewhere~\cite{paulson-set-II}.
   1.346 +  
   1.347 +\item Theory {\tt PropLog} proves the soundness and completeness of classical
   1.348 +  propositional logic, given a truth table semantics.  The only connective is
   1.349 +  $\imp$.  A Hilbert-style axiom system is specified, and its set of theorems
   1.350 +  defined inductively.  A similar proof in ZF is described
   1.351 +  elsewhere~\cite{paulson-set-II}.
   1.352  
   1.353  \item Theory {\tt Term} develops an experimental recursive type definition;
   1.354    the recursion goes through the type constructor~\tydx{list}.
   1.355 @@ -1804,8 +1798,8 @@
   1.356  of~$\alpha$.  This version states that for every function from $\alpha$ to
   1.357  its powerset, some subset is outside its range.  
   1.358  
   1.359 -The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
   1.360 -the operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
   1.361 +The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and the
   1.362 +operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
   1.363  quantified variable so that we may inspect the subset found by the proof.
   1.364  \begin{ttbox}
   1.365  goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
   1.366 @@ -1870,12 +1864,11 @@
   1.367  {\out No subgoals!}
   1.368  \end{ttbox}
   1.369  How much creativity is required?  As it happens, Isabelle can prove this
   1.370 -theorem automatically.  The classical set \ttindex{set_cs} contains rules
   1.371 -for most of the constructs of \HOL's set theory.  We must augment it with
   1.372 -\tdx{equalityCE} to break up set equalities, and then apply best-first
   1.373 -search.  Depth-first search would diverge, but best-first search
   1.374 -successfully navigates through the large search space.
   1.375 -\index{search!best-first}
   1.376 +theorem automatically.  The classical set \ttindex{set_cs} contains rules for
   1.377 +most of the constructs of HOL's set theory.  We must augment it with
   1.378 +\tdx{equalityCE} to break up set equalities, and then apply best-first search.
   1.379 +Depth-first search would diverge, but best-first search successfully navigates
   1.380 +through the large search space.  \index{search!best-first}
   1.381  \begin{ttbox}
   1.382  choplev 0;
   1.383  {\out Level 0}