Commit 3efe270e authored by Raphael Cauderlier's avatar Raphael Cauderlier

[doc] Documentation of the unification module

parent 481f3b33
......@@ -693,6 +693,72 @@ combinator) and then uses the classical lemma
* TODO Checking output of automatic theorem provers
** Reasoning modulo AC, ACU, symmetry
** Substitution and unification
** Shallow substitutions and unification
This section describes the features provided by the file
[[./meta/][meta/]] related to the handling of substitution and
unification. Usually, substitutions are not defined in shallow
embeddings relying on Higher-Order Abstract Syntax (HOAS) because
we have no access to the variables. However, unification is an
important tool for checking proof certificates that are not precise
enough to tell us which substitution to apply.
*** Substitutions
A substitution is usually defined as a finite mapping from
variables to terms. Since we have no precise type for variables in
our shallow embedding, we use lists of pairs of terms (both terms
having the same type).
- =unif.substition : Type=
- =unif.empty_subst : unif.substitution=
- =unif.cons_subst : A : fol.type -> fol.term A -> fol.term A -> unif.substitution -> unif.substitution=
Substitutions can be applied on propositions, terms, and list of terms.
- =unif.subst_prop : unif.substitution -> fol.prop -> fol.prop=
- =unif.subst_term : unif.substitution -> B : fol.type -> fol.term B -> fol.term B=
- =unif.subst_terms : unif.substitution -> Bs : fol.types -> fol.terms Bs -> fol.terms Bs=
These functions are defined by a non-confluent rewrite system
which means that the behaviour of substitution depends on the
order in which the rewrite rules are given. The rules with the
highest priorities are those traversing the structure of the term
or formula such as
=[s,a,b] unif.subst_prop s (fol.and a b) --> fol.and (unif.subst_prop s a) (unif.subst_prop s b)=
If none of these rules is applicable, the term is assumed to be a
variable so we look into the substitution (seen as a list) for
corresponding pair. The comparison is performed by a non-linear
rewrite rule (the second rule):
- =[a] unif.subst_term unif.empty_subst _ a --> a=
- =[A,x,a] unif.subst_term (unif.cons_subst A x a _) A x --> a=
- =[As,s,A,x] unif.subst_term (unif.cons_subst _ _ As s) A x -->
unif.subst_term s A x=
Finally, for technical reasons (see the next section about
unification), the following two rewrite rules are added:
- =[A,a,s,p] unif.subst_prop (unif.cons_subst A a a s) p --> unif.subst_prop s p=
- =[A,a,s,p] unif.subst_prop unif.empty_subst p --> p=
*** Rewrite rules for unification
A (first-order) unification problem is a list of pairs of terms
(both terms having the same type). Unification can either fail or
return a substitution, the most general unifier of the unification
- =unif.unify_problem : Type=
- =unif.unify_nil : unif.unify_problem=
- =unif.unify_cons : A : fol.type -> fol.term A -> fol.term A -> unif.unify_problem -> unif.unify_problem=
- =unif.unify_result : Type=
- =unif.unify_success : unif.substitution -> unif.unify_result=
- =unif.unify_failure : unif.unify_result=
We will not enter the details of the unification algorithm here,
the entry-point of the unification procedure is =unif.unify :
unif.unify_problem -> unif.unify_result=.
** Resolution
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment