# HG changeset patch # User Christian Urban # Date 1257851828 -3600 # Node ID 72a53b07d264d1fb73a4a36e517bd4317315b9f9 # Parent 3f153aa4f2311635b4ef036e272be70d9cccf84a tuned diff -r 3f153aa4f231 -r 72a53b07d264 ProgTutorial/General.thy --- 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 "\x. P x"} against the pattern @{text "\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} *} diff -r 3f153aa4f231 -r 72a53b07d264 progtutorial.pdf Binary file progtutorial.pdf has changed