968 *} |
968 *} |
969 |
969 |
970 text {* |
970 text {* |
971 Unification of abstractions is more thoroughly studied in the context of |
971 Unification of abstractions is more thoroughly studied in the context of |
972 higher-order pattern unification and higher-order pattern matching. A |
972 higher-order pattern unification and higher-order pattern matching. A |
973 \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that |
973 \emph{\index*{pattern}} is a well-formed beta-normal term in which the arguments to |
974 is the first symbol under an abstraction) is either a constant, a schematic |
974 every schematic variable are distinct bounds. |
975 variable or a free variable. If it is a schematic variable then it can only |
975 In particular this excludes terms where a |
976 have distinct bound variables as arguments. This excludes terms where a |
|
977 schematic variable is an argument of another one and where a schematic |
976 schematic variable is an argument of another one and where a schematic |
978 variable is applied twice with the same bound variable. The function |
977 variable is applied twice with the same bound variable. The function |
979 @{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests |
978 @{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests |
980 whether a term satisfies these restrictions. |
979 whether a term satisfies these restrictions under the assumptions |
|
980 that it is beta-normal, well-typed and has no loose bound variables. |
981 |
981 |
982 @{ML_response [display, gray] |
982 @{ML_response [display, gray] |
983 "let |
983 "let |
984 val trm_list = |
984 val trm_list = |
985 [@{term_pat \"?X\"}, @{term_pat \"a\"}, |
985 [@{term_pat \"?X\"}, @{term_pat \"a\"}, |
991 end" |
991 end" |
992 "[true, true, true, true, true, false, false, false]"} |
992 "[true, true, true, true, true, false, false, false]"} |
993 |
993 |
994 The point of the restriction to patterns is that unification and matching |
994 The point of the restriction to patterns is that unification and matching |
995 are decidable and produce most general unifiers, respectively matchers. |
995 are decidable and produce most general unifiers, respectively matchers. |
|
996 Note that \emph{both} terms to be unified have to be higher-order patterns |
|
997 for this to work. The exception @{ML_ind Pattern in Pattern} indicates failure |
|
998 in this regard. |
996 In this way, matching and unification can be implemented as functions that |
999 In this way, matching and unification can be implemented as functions that |
997 produce a type and term environment (unification actually returns a |
1000 produce a type and term environment (unification actually returns a |
998 record of type @{ML_type Envir.env} containing a max-index, a type environment |
1001 record of type @{ML_type Envir.env} containing a max-index, a type environment |
999 and a term environment). The corresponding functions are @{ML_ind match in Pattern} |
1002 and a term environment). The corresponding functions are @{ML_ind match in Pattern} |
1000 and @{ML_ind unify in Pattern}, both implemented in the structure |
1003 and @{ML_ind unify in Pattern}, both implemented in the structure |