# HG changeset patch # User Christian Urban # Date 1258016786 -3600 # Node ID 5f7ca76f94e3a64b930d82ce0caafcdbf89bfc2c # Parent 78c91a629602032f16475bfccd0785bc91237bca tuned diff -r 78c91a629602 -r 5f7ca76f94e3 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Wed Nov 11 12:15:48 2009 +0100 +++ b/ProgTutorial/General.thy Thu Nov 12 10:06:26 2009 +0100 @@ -677,7 +677,7 @@ section {* Unification and Matching *} text {* - Isabelle's terms and types may contain schematic term variables + As seen earlier, Isabelle's terms and types may contain schematic term variables (term-constructor @{ML Var}) and schematic type variables (term-constructor @{ML TVar}). These variables stand for unknown entities, which can be made more concrete by instantiations. Such instantiations might be a result of @@ -708,10 +708,10 @@ text {* The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type environment, which is needed for starting the unification without any - (pre)instantiations. The @{text 0} is an integer index that we will explain + (pre)instantiations. The @{text 0} is an integer index that will be explained below. In case of failure @{ML typ_unify in Sign} will throw the exception - @{text TUNIFY}. We can print out the resulting type environment @{ML - tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the + @{text TUNIFY}. We can print out the resulting type environment bound to + @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the structure @{ML_struct Vartab}. @{ML_response_fake [display,gray] @@ -750,10 +750,11 @@ text {* The first components in this list stand for the schematic type variables and the second are the associated sorts and types. In this example the sort is - the default sort @{text "HOL.type"}. We will use in what follows the - pretty-printing function from Figure~\ref{fig:prettyenv} for @{ML_type - "Type.tyenv"}s. For the type environment in the example this function prints - out the more legible: + the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will + use in what follows our own pretty-printing function from + Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type + environment in the example this function prints out the more legible: + @{ML_response_fake [display, gray] "pretty_tyenv @{context} tyenv_unif" @@ -808,8 +809,8 @@ "index" "1"} - Let us now return again to the unification problem @{text "?'a * ?'b"} and - @{text "?'b list * nat"} from the beginning of the section, and the + Let us now return to the unification problem @{text "?'a * ?'b"} and + @{text "?'b list * nat"} from the beginning of this section, and the calculated type environment @{ML tyenv_unif}: @{ML_response_fake [display, gray] @@ -820,18 +821,15 @@ Sign} returns is in \emph{not} an instantiation in fully solved form: while @{text "?'b"} is instantiated to @{typ nat}, this is not propagated to the instantiation for @{text "?'a"}. In unification theory, this is often - called an instantiation in \emph{triangular form}. These not fully solved - instantiations are used because of performance reasons. - To apply a type environment in triangular form to a type, say @{text "?'a * + called an instantiation in \emph{triangular form}. These triangular + instantiations, or triangular type environments, are used because of + performance reasons. To apply such a type environment to a type, say @{text "?'a * ?'b"}, you should use the function @{ML_ind norm_type in Envir}: @{ML_response_fake [display, gray] "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}" "nat list * nat"} - With this function the type variables @{text "?'a"} and @{text "?'b"} are - correctly instantiated. - Matching of types can be done with the function @{ML_ind typ_match in Sign} also from the structure @{ML_struct Sign}. This function returns a @{ML_type Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case @@ -854,7 +852,7 @@ Unlike unification, which uses the function @{ML norm_type in Envir}, applying the matcher to a type needs to be done with the function - @{ML_ind subst_type in Envir}. + @{ML_ind subst_type in Envir}. For example @{ML_response_fake [display, gray] "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}" @@ -862,7 +860,7 @@ Be careful to observe the difference: use always @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} - for unifiers. To make the difference explicit, let us calculate the + for unifiers. To show the difference, let us calculate the following matcher: *} @@ -896,7 +894,7 @@ are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments as results. These are implemented in @{ML_file "Pure/envir.ML"}. This file also includes the substitution and normalisation functions, - that apply a type environment to a type. Type environments are lookup + which apply a type environment to a type. Type environments are lookup tables which are implemented in @{ML_file "Pure/term_ord.ML"}. \end{readmore} *} @@ -984,8 +982,8 @@ Unification of abstractions is more thoroughly studied in the context of higher-order pattern unification and higher-order pattern matching. A \emph{\index*{pattern}} is a lambda term whose ``head symbol'' (that is the - first symbol under abstractions) is either a constant, or a schematic or a free - variable. If it is a schematic variable then it can be only applied by + first symbol under an abstraction) is either a constant, a schematic or a free + variable. If it is a schematic variable then it can be only applied with distinct bound variables. This excludes that a schematic variable is an argument of another one and that a schematic variable is applied twice with the same bound variable. The function @{ML_ind pattern in Pattern} @@ -1009,8 +1007,8 @@ In this way, matching and unification can be implemented as functions that produce a type and term environment (unification actually returns a record of type @{ML_type Envir.env} containing a maxind, a type environment - and a term environment). The former function is @{ML_ind match in Pattern}, - the latter @{ML_ind unify in Pattern} both implemented in the structure + and a term environment). The corresponding functions are @{ML_ind match in Pattern}, + and @{ML_ind unify in Pattern} both implemented in the structure @{ML_struct Pattern}. An example for higher-order pattern unification is @{ML_response_fake [display, gray] @@ -1029,29 +1027,25 @@ already the same type. In case of failure, the exceptions that are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}. - As mentioned before, ``full'' higher-order unification, respectively, matching - problems are in general undecidable and might in general not posses a single - most general solution. Therefore Isabelle implements Huet's pre-unification - algorithm which does not return a single result, rather a lazy list of potentially - infinite unifiers. The corresponding function is called @{ML_ind unifiers in Unify}. - An example is as follows + As mentioned before, ``full'' higher-order unification, respectively + higher-order matching problems, are in general undecidable and might also not posses a + single most general solution. Therefore Isabelle implements the unification + function @{ML_ind unifiers in Unify} so that it returns a lazy list of + potentially infinite unifiers. An example is as follows \ldots In case of failure this function does not raise an exception, rather returns the empty sequence. In order to find a reasonable solution for a unification problem, Isabelle also tries first to solve the problem by higher-order - pattern unification. + pattern unification. For higher-order matching the function is called + @{ML_ind matchers in Unify}. Also this function might potentially return + sequences with more than one matcher. \ldots - - For higher-order matching the function is called @{ML_ind matchers in Unify}. - Also this function might potentially return sequences with more than one - element. - Like @{ML unifiers in Unify}, this function does not raise an exception - in case of failure. It also tries out first whether the matching problem + in case of failure. It also first tries out whether the matching problem can be solved by first-order matching. \begin{readmore} diff -r 78c91a629602 -r 5f7ca76f94e3 progtutorial.pdf Binary file progtutorial.pdf has changed