From 3efe270ea7c67c40b8b4761ea3968605c7da9e5a Mon Sep 17 00:00:00 2001
From: Raphael Cauderlier
Date: Thu, 14 Dec 2017 12:18:08 +0100
Subject: [PATCH] [doc] Documentation of the unification module
---
manual.org | 68 +++++++++++++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 67 insertions(+), 1 deletion(-)
diff --git a/manual.org b/manual.org
index dc4d39a..5e72b83 100644
--- a/manual.org
+++ b/manual.org
@@ -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/unif.dk][meta/unif.dk]] 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
+ problem.
+
+ - =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
--
2.24.1