--- a/ProgTutorial/General.thy Tue Nov 10 06:24:00 2009 +0100
+++ b/ProgTutorial/General.thy Tue Nov 10 12:17:08 2009 +0100
@@ -674,7 +674,7 @@
\end{exercise}
*}
-section {* Unification and Matching (TBD) *}
+section {* Unification and Matching *}
text {*
Isabelle's terms and types may contain schematic term variables
@@ -690,8 +690,8 @@
schematic variables.
Let us begin with describing the unification and matching function for
- types. Both return type environments, ML-type @{ML_type "Type.tyenv"},
- which map schematic type variables to types (and sorts). Below we use the
+ types. Both return type environments (ML-type @{ML_type "Type.tyenv"})
+ which map schematic type variables to types and sorts. Below we use the
function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}
for unifying the types @{text "?'a * ?'b"} and @{text "?'b list *
nat"}. This will produce the mapping, or type environment, @{text "[?'a :=
@@ -706,13 +706,13 @@
end*}
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. In case of a 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 structure
- @{ML_struct Vartab}.
+ 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
+ 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
+ structure @{ML_struct Vartab}.
@{ML_response_fake [display,gray]
"Vartab.dest tyenv_unif"
@@ -749,49 +749,57 @@
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 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:
@{ML_response_fake [display, gray]
"pretty_tyenv @{context} tyenv_unif"
"[?'a := ?'b list, ?'b := nat]"}
- The index @{text 0} in Line 5 in the example above is the maximal index of
- the schematic type variables occuring in @{text ty1} and @{text ty2}. This
- index will be increased whenever a new schematic type variable is introduced
- during unification. This is for example the case when two schematic type
- variables have different, incomparable sorts. Then a new schematic type
- variable is introduced with the combined sorts. To show this let us assume two
- sorts, say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
- variables @{text "?'a"} and @{text "?'b"}. Since we do not make any assumption
- about the sors, they are incomparable, leading to the type environment:
+ The way the unification function @{ML typ_unify in Sign} is implemented
+ using an initial type environment and initial index makes it easy to
+ unify more than two terms. For example
+*}
+
+ML %linenosgray{*val (tyenvs, _) = let
+ val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
+ val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
+in
+ fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0)
+end*}
+
+text {*
+ The index @{text 0} in Line 5 is the maximal index of the schematic type
+ variables occurring in @{text ty1} and @{text ty2}. This index will be
+ increased whenever a new schematic type variable is introduced during
+ unification. This is for example the case when two schematic type variables
+ have different, incomparable sorts. Then a new schematic type variable is
+ introduced with the combined sorts. To show this let us assume two sorts,
+ say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
+ variables @{text "?'a"} and @{text "?'b"}. Since we do not make any
+ assumption about the sorts, they are incomparable.
*}
ML{*val (tyenv, index) = let
- val ty2 = @{typ_pat "?'a::s1"}
- val ty1 = @{typ_pat "?'b::s2"}
+ val ty1 = @{typ_pat "?'a::s1"}
+ val ty2 = @{typ_pat "?'b::s2"}
in
Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
end*}
text {*
- To print out this type environment we switch on the printing of sort
- information.
-*}
-
-ML{*show_sorts := true*}
-
-text {*
- Now we can see
+ To print out the result type environment we switch on the printing
+ of sort information by setting @{ML_ind show_sorts in Syntax} to
+ true. This allows us to inspect the typing environment.
@{ML_response_fake [display,gray]
"pretty_tyenv @{context} tyenv"
"[?'a::s1 := ?'a1::{s1,s2}, ?'b::s2 := ?'a1::{s1,s2}]"}
- the type variables @{text "?'a"} and @{text "?'b"} are instantiated
+ As can be seen, the type variables @{text "?'a"} and @{text "?'b"} are instantiated
with a new type variable @{text "?'a1"} with sort @{text "{s1,s2}"}. Since a new
type variable has been introduced the @{ML index}, originally being @{text 0},
has been increased by @{text 1}.
@@ -799,24 +807,10 @@
@{ML_response [display,gray]
"index"
"1"}
-*}(*<*)ML %linenos{*show_sorts := false*}(*>*)
-
-text {*
- The way the unification function @{ML typ_unify in Sign} is implemented
- using an initial type environment and initial index makes it easy to
- unify more than two terms. For example
-*}
-
-ML{*val (tyenvs, _) = let
- val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
- val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
-in
- fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0)
-end*}
-
-text {*
- Let us now return again to the unifier from the first example in this
- section.
+
+ 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
+ calculated type environment @{ML tyenv_unif}:
@{ML_response_fake [display, gray]
"pretty_tyenv @{context} tyenv_unif"
@@ -839,8 +833,8 @@
correctly instantiated.
Matching of types can be done with the function @{ML_ind typ_match in Sign}
- from the structure @{ML_struct Sign}. It also returns a @{ML_type
- Type.tyenv} and might raise the exception @{text TYPE_MATCH} in case
+ 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
of failure. For example
*}
@@ -858,7 +852,7 @@
"pretty_tyenv @{context} tyenv_match"
"[?'a := bool list, ?'b := nat]"}
- Unlike the unification, which uses the function @{ML norm_type in Envir},
+ 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}.
@@ -881,23 +875,23 @@
text {*
Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply
- @{ML norm_type in Envir} to the matcher we obtain
+ @{ML norm_type in Envir} to the type @{text "?'a * ?'b"} we obtain
@{ML_response_fake [display, gray]
"Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
"nat list * nat"}
- which is not a matcher for the second matching problem, and if
- we apply @{ML subst_type in Envir} to the unifyier we obtain
+ which does not solve the matching problem, and if
+ we apply @{ML subst_type in Envir} to the same type we obtain
@{ML_response_fake [display, gray]
"Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
"?'b list * nat"}
- which is not the correct unifier for the unification problem.
+ which does not solve the unification problem.
\begin{readmore}
- Unification and matching of types is implemented
+ Unification and matching for types is implemented
in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them
are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments
as results. These are implemented in @{ML_file "Pure/envir.ML"}.
@@ -909,9 +903,9 @@
text {*
Unification and matching of terms is substantially more complicated than the
- type-case. The reason is that terms have abstractions and unification
- or matching modulo plain equality is often not meaningful in this
- context. Nevertheless, Isabelle implements the function @{ML_ind
+ type-case. The reason is that terms have abstractions and, in this context,
+ unification or matching modulo plain equality is often not meaningful.
+ Nevertheless, Isabelle implements the function @{ML_ind
first_order_match in Pattern} for terms. This matching function returns a
type environment and a term environment. To pretty print the latter we use
the function @{text "pretty_env"}:
@@ -944,7 +938,7 @@
text {*
In this example we annotated explicitly types because then
the type environment is empty and can be ignored. The
- resulting term environment is:
+ resulting term environment is
@{ML_response_fake [display, gray]
"pretty_env @{context} fo_env"
@@ -952,8 +946,8 @@
The matcher can be applied to a term using the function @{ML_ind subst_term
in Envir} (remember the same convention for types applies to terms: @{ML
- subst_term in Envir} is for matchers and @{ML norm_term in Envir} is for
- unifyiers). The function @{ML subst_term in Envir} expects a type environment,
+ subst_term in Envir} is for matchers and @{ML norm_term in Envir} for
+ unifiers). The function @{ML subst_term in Envir} expects a type environment,
which is set to empty in the example below, and a term environment.
@{ML_response_fake [display, gray]
@@ -969,7 +963,7 @@
First-order matching is useful for matching against applications and
variables. It can deal also with abstractions and a limited form of
alpha-equivalence, but this kind of matching should be used with care, since
- it is not clear whether the result is meaningful. A working example is
+ it is not clear whether the result is meaningful. A meaningful example is
matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this
case first-order matching produces @{text "[?X := P]"}.
@@ -987,18 +981,17 @@
*}
text {*
- In the context of unifying abstractions, more thouroughly studied is
- higher-order pattern unification and higher-order pattern matching. A
+ 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
distinct bound variables. This excludes that a schematic variable is an
- argument of a schematic variable and that a schematic variable is applied
- twice to the same bound variable. The function @{ML_ind pattern in Pattern}
+ argument of another one and that a schematic variable is applied
+ twice with the same bound variable. The function @{ML_ind pattern in Pattern}
in the structure @{ML_struct Pattern} tests whether a term satisfies these
restrictions.
-
@{ML_response [display, gray]
"let
val trm_list =
@@ -1011,20 +1004,62 @@
end"
"[true, true, true, true, true, false, false, false]"}
- The point of restricting unification and matching to patterns is that
- it is decidable and produces most general unifiers. In this way
- matching and unify can be implemented so that they produce a type
- and term environment (the latter actually produces only a term
- environment).
+ The point of the restriction to patterns is that unification and matching
+ are decidable and produce most general unifiers, respectively matchers.
+ 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
+ @{ML_struct Pattern}. An example for higher-order pattern unification is
+
+ \ldots
*}
+ML{*let
+ val pat = @{term_pat "?X"}
+ val trm = @{term "a"}
+ val init = (Vartab.empty, Vartab.empty)
+in
+ Pattern.match @{theory} (pat, trm) init
+end *}
text {*
+ An assumption of this function is that the terms to be unified have
+ 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
+
+ \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.
+
+ \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
+ can be solved by first-order matching.
+
\begin{readmore}
- For term, unification and matching of higher-order patterns is implemented in
+ Unification and matching of higher-order patterns is implemented in
@{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher
for terms. Full higher-order unification is implemented
- in @{ML_file "Pure/unify.ML"}.
+ in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented
+ in @{ML_file "Pure/General/seq.ML"}.
\end{readmore}
*}