Implementation of an algorithm for checking subject reduction #200

wujuihsuan2016 · 2019-03-25T16:56:52Z

The following code defines the relation used in our algorithm for checking subject reduction.
There might be some modifications after since some details in the algorithm still need to be clarified.

fblanqui · 2019-03-25T17:06:06Z

src/subject_reduction.ml

+
+module Eset = Set.Make(
+  struct
+    type t = (term * term) 


Parentheses are useless here.

fblanqui · 2019-03-25T17:08:40Z

Hi Jui-Hsuan. Thanks for your first PR!

Note that this PR should modify the file sr.ml.

fblanqui · 2019-03-25T17:11:44Z

The set of equations is already computed by the type inference algorithm. You don't have to compute it again. The main problem is to turn this set of equations into a confluent and terminating rewrite systems using completion. To this end, you should export this set of equations to some external tool, call it, and get back the convergent rewrite system if any. Then, you can check that the RHS has the type of the LHS modulo these rewrite rules using the current type-checking function.

rlepigre · 2019-03-25T19:36:06Z

src/subject_reduction.ml

+module Eset = Set.Make(
+  struct
+    type t = (term * term) 
+    let compare = Pervasives.compare


Note that Pervasives.compare will not work to compare terms, since their representation contains closures (in Bindlib Binders).

wujuihsuan2016 · 2019-03-26T14:36:26Z

The set of equations is already computed by the type inference algorithm. You don't have to compute it again. The main problem is to turn this set of equations into a confluent and terminating rewrite systems using completion. To this end, you should export this set of equations to some external tool, call it, and get back the convergent rewrite system if any. Then, you can check that the RHS has the type of the LHS modulo these rewrite rules using the current type-checking function.

I took a look at the MKBtt tool (http://cl-informatik.uibk.ac.at/software/mkbtt/index.php) today. According to the documentation, yices 1.11 headers and libs are required in order to compile the source code but I haven't found them online yet. I also tried to use the binary executable file which is available online. It works well for the generation of complete systems. However, I always get the message "the process terminated with exit code 127" when using the option -cert in order to get certifiable proofs and I am still trying to figure out where it comes from. Besides, it seems that there exists already a function in confluence.ml that allows to print in the TRS format and it can be adapted for our purpose (adding equations).

rlepigre · 2019-03-26T15:04:58Z

The main problem is to turn this set of equations into a confluent and terminating rewrite systems using completion. To this end, you should export this set of equations to some external tool, call it, and get back the convergent rewrite system if any.

Wouldn't it be easier to implement completion directly? That is not very hard, and it would be a lot faster than having to call an external tool and converting the data both ways.

wujuihsuan2016 · 2019-03-26T15:20:32Z

Wouldn't it be easier to implement completion directly? That is not very hard, and it would be a lot faster than having to call an external tool and converting the data both ways.

In fact, in the traditional Knuth-Bendix completion algorithm, a reduction ordering on terms is required and it is in general given by users, which is not very convenient in practice. In the MKBtt tool, some termination tools are used to deal with this issue. There are more details here (http://cl-informatik.uibk.ac.at/software/mkbtt/papers/SWKM08.pdf). I am not sure if this feature can be easily implemented.

fblanqui · 2019-03-26T16:18:41Z

Rodolphe, completion is very hard in general (harder than termination alone!). And, as we can already export rules to the TRS (for confluence) and XTC (for termination) formats, it should not be too difficult to use these exports to call external completion tools too. But, you are right, as we only have closed equations, we could also implement an adhoc optimized completion algorithm using any total reduction ordering on terms (e.g. LPO over an arbitrary total ordering on symbols). This is fine if, in the end, we get no critical pairs with user-defined rewriting rules. Otherwise, we may have to rely on a general completion tool. More theoretical work would be useful in this case. So, it may be interesting to have both.

fblanqui · 2019-03-26T16:26:56Z

By the way, I see that the exports to TRS and XTC are not documented. @GuillaumeGen : could you please add a PR with at the beginning of termination.ml some details about the corresponding export functions? In particular, it should explain what is done with abstractions and products as TRS is an untyped first-order setting. As for XTC, it should explain how dependent types are handled. Is it the current simply-typed version of XTC or its extension with dependent types? @wujuihsuan2016 : you can probably do the same thing for confluence.ml by reverse-engineering the code.

fblanqui · 2019-03-26T16:30:43Z

@wujuihsuan2016 : there exist various completion tools. It would be good to try several.

wujuihsuan2016 · 2019-03-29T14:20:54Z

In termination.ml, a qualified identifier dir1. ... .dirn.id is translated to c_dir1_..._dirn_id. It is impossible to retrieve information of symbols using their translations (c_a_b_id is the translation of both a.b.id and a_b.id for example). Thus, it might be useful to keep a mapping : translation(sym) -> sym.

fblanqui · 2019-03-29T16:55:01Z

Is there any restriction on identifiers in the XTC format? If not, as I suspect for XTC is an XML format, then there is no reason for changing names. This should be fixed.

It's different perhaps for the TRS format. Question: what are the restrictions on identifiers in the TRS format? In particular, is "." forbidden? If not, then there is no reason for changing names and should be fixed.

fblanqui · 2019-03-29T17:48:18Z

In the TRS format (see http://project-coco.uibk.ac.at/problems/trs.php), we have:

id is any nonempty sequence of characters not containing
whitespace
the characters ( ) " , |
the sequences -> == COMMENT VAR RULES

So, dots can be used in names.

In the XTC format (see http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/file/tip/xml/xtc.xsd), there are no restrictions on names.

rlepigre · 2019-03-29T18:19:24Z

For the record, I implemented the translation to the TRS format based on what was done in Dedukti, hence using the same translation conventions. It would indeed be great if we could preserve more identifiers. To rule out any problem with variables named COMMENT, VAR or RULES, I don't see any other solution than to prefix every identifier coming from Lambdapi with some sequence of character (e.g., c_). And that also prevents name clashes with the locally defined symbol (see the prelude).

For the XTC format, one has to be careful with special characters (as in any XML format), but they can be easily escaped.

In both cases, somewhat arbitrary sequences of characters can arise in Lambdapi through the {|...|} syntax. Thus some care should be taken, and a first approximation could be to fail when the translation reaches such an identifier.

For exchanging arbitrary identifiers, one solution is to use some bijective encoding. As an example, sequences of characters like {|...|} could be base-64-encoded, and then prefixed with some reserved prefix. And decoding would then be the obvious thing. In any case, it may be a good idea to define encoding / decoding functions that would always be used by the translation.

Syncing the fork

fblanqui · 2019-04-10T12:35:36Z

src/completion.ml

@@ -0,0 +1,147 @@
+(** Completion procedure *)


Precise that this is a completion procedure for closed equations.

fblanqui · 2019-04-10T12:37:22Z

General remark: for computing critical pairs, do not use the unification algorithm implemented in unif.ml, but define your own syntactic first-order unification algorithm.

fblanqui · 2019-04-10T12:40:32Z

src/completion.ml

+open Extra
+
+(** total strict order *)
+type 'a order = 'a -> 'a -> bool


Please, use:

type 'a cmp = 'a -> 'a -> int (* [cmp x y] returns - [0] when x=y - [r<0] when x<y - (r>0] when x>y *)

Then, there is no need to introduce gt, ge, etc.

fblanqui · 2019-04-10T12:41:15Z

src/completion.ml

+
+(** [ord_lex ord] calculates the lexicographic order corresponding to the
+    alphabetical order [ord] *)
+let ord_lex : 'a order -> ('a list) order = fun ord l1 l2 ->


parentheses are not needed

Moving from ord to cmp, we need:

let lex : 'a cmp -> 'a list cmp'

Idem for lpo.

fblanqui · 2019-04-10T12:42:10Z

src/completion.ml

+(** [ord_lex ord] calculates the lexicographic order corresponding to the
+    alphabetical order [ord] *)
+let ord_lex : 'a order -> ('a list) order = fun ord l1 l2 ->
+  let rec elim_comm l1 l2 = match (l1, l2) with


Please, follow the style and indentation of master files.

What is the meaning of "elim_comm"?

fblanqui · 2019-04-10T12:52:30Z

src/completion.ml

+
+type rule_ = sym * pp_hint * rule
+
+(** [cp builtins r1 r2] calculates the critical pairs of the rules r1 and r2


calculates -> computes

fblanqui · 2019-04-10T12:54:26Z

src/completion.ml

+  let tk = _Meta mk (Array.map _Vari vs) in
+  Bindlib.unbox (build_prod k tk)
+
+type rule_ = sym * pp_hint * rule


rule_ is not nice

pp_hint doesn't seem useful. Please remove it.

Then, you can do:

type rule = sym * Term.rule

fblanqui · 2019-04-10T13:04:56Z

src/completion.ml

+  let arity1 = Bindlib.mbinder_arity r1.rhs in
+  let arity2 = Bindlib.mbinder_arity r2.rhs in
+  let cps = ref [] in
+  let rec to_m : int -> (meta option) array -> term -> tbox = fun k metas t ->


If this function is taken from somewhere else, it would be better to not duplicate the code, but factorize it instead.

fblanqui · 2019-04-10T13:05:40Z

src/completion.ml

+(** [build_meta_type k] builds the type “∀(x₁:A₁) (x₂:A₂) ⋯ (xk:Ak), B” where
+    “x₁” through “xk” are fresh variables, “Ai = Mi[x₁,⋯,x(i-1)]”, “Mi” is a
+    new metavar of arity “i-1” and type “∀(x₁:A₂) ⋯ (x(i-1):A(i-1), TYPE”. *)
+let build_meta_type : int -> term = fun k ->


If this function is taken from somewhere else, it would be better to not duplicate the code, but factorize it instead.

fblanqui · 2019-06-05T08:43:35Z

src/completion.ml

+
+(** [to_rule (lhs, rhs)] tranlates the pair [(lhs, rhs)] of closed terms into
+    a rule. *)
+let to_rule : term * term -> sym * rule = fun (lhs, rhs) ->


rename into make_rule?

fblanqui · 2019-06-05T08:44:10Z

src/completion.ml

+    a rule. *)
+let to_rule : term * term -> sym * rule = fun (lhs, rhs) ->
+  let (s, args) = get_args lhs in
+  let s = get_symb s in


remove this let

fblanqui · 2019-06-05T08:47:25Z

src/completion.ml

+    is added into [deps] iff there is a equation (l, r) in [eqs] such that
+    (l = s and t is a proper subterm of r) or (r = s and t is a proper subterm
+    of l). In this case, we also add s and t into [symbs]. *)
+let find_deps : (term * term) list -> string list * (string * string) list


This seems to be related to the computation of dependency pairs. Check with @GuillaumeGen whether you could factorize/share some code.

Complexity of the algorithm?

fblanqui · 2019-06-05T08:48:20Z

src/completion.ml

+    (fun (t1, t2) -> find_dep_aux (t1, t2); find_dep_aux (t2, t1)) eqs;
+  (!symbs, !deps)
+
+module StrMap = Map.Make(struct


This is already defined in basics.

fblanqui · 2019-06-05T08:48:32Z

src/completion.ml

+  let compare = compare
+end)
+
+exception Not_DAG


Comment missing!

fblanqui · 2019-06-05T08:49:20Z

src/completion.ml

+
+(** [topo_sort symbs edges] computes a topological sort on the directed graph
+    [(symbs, edges)]. *)
+let topo_sort : string list -> (string * string) list -> int StrMap.t


This should be defined in Extra.

More explanations required. What is the resulting map?

You should add more comments inside the code for explaining what you are doing.

Complexity of the algorithm?

You should say that this function may raise some exception. When? Why?

fblanqui · 2019-06-05T08:57:17Z

src/completion.ml

+      | true, false  -> 1
+      | false, true  -> -1
+      | false, false -> Pervasives.compare s1.sym_name s2.sym_name
+  with Not_DAG ->


This exception is raised by topo_sort only, right? If so, you should instead write:

let ord = try topo_sort ... with Pervasives.compare in fun s1 s2 -> ....

fblanqui · 2019-06-05T08:59:26Z

src/confluence.ml

+  | _, Abst _                     -> assert false
+  | Appl (t1, u1), Appl (t2, u2)  -> unif ((t1, t2) :: (u1, u2) :: eqs)
+  | Meta (m1, ts1), Meta (_, ts2) ->
+      assert (ts1 = [||] && ts2 = [||]);


replace by | Meta(m1,[||]), Meta(_,[||]) ->

Why do you have this special case? Why can't this be done by the following case?

fblanqui · 2019-06-05T09:06:26Z

src/confluence.ml

+  | (t2, Meta (m1, ts1))          ->
+      if occurs m1 t2 then raise Unsolvable
+      else
+        assert (ts1 = [||]);


Should be in the pattern.

fblanqui · 2019-06-05T09:07:47Z

src/confluence.ml

+        assert (ts1 = [||]);
+        let vs = Bindlib.new_mvar mkfree [||] in
+        let bt2 = Bindlib.bind_mvar vs (lift t2) in
+        set_meta m1 (Bindlib.unbox bt2);


Can't this be simplified/optimized @rlepigre ?

@rlepigre : In addition, as references are timed, and all these meta and meta substitutions are only used for checking subject reduction, shouldn't we through all these references away after subject reduction using save/restore to limit memory usage? Idem for TRef instantiations used in eq when calling the tactic rewrite.

We could maybe avoid a lifting/unboxing here. Is the term t2 guaranteed to be closed here?

For the second point, I don't think this would make much difference. The memory is collected for every undo that is not reachable from a reachable saved time, so I would not worry too much about that.

fblanqui · 2019-06-05T09:08:12Z

src/confluence.ml

+
+(** [unif_aux t1 t2 eqs] attempts to solve the first-order unification
+    problem [(t1 = t2) :: eqs]. *)
+let rec unif_aux : term -> term -> unif_constrs -> unit = fun t1 t2 eqs ->


Should be in basics.

fblanqui · 2019-06-05T09:21:30Z

src/handle.ml

      in
      let rs = List.map handle_rule rs in
      (* Adding the rules all at once. *)
      let add_rule (s,h,r) =
        out 3 "(rule) %a\n" Print.pp_rule (s,h,r.elt);
        Sign.add_rule ss.signature s r.elt
      in
-      List.iter add_rule rs; (ss, None)
+      List.iter add_rule rs;
+      List.iter (Sr.check_rule ss.builtins) rs; (ss, None)


SR must be checked BEFORE adding the rules. So these modifications should be reverted.

When we check SR for the rule fl -> r, we should consider all the rules defining f. This is the reason why the SR should be checked in this way.

I don't understand. Checking SR for a rule or set of rules should not depend on the rules themselves.

fblanqui · 2019-06-05T09:22:18Z

src/handle.ml

@@ -208,6 +209,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option =
            wrn cmd.pos "Proof aborted."; ss
        | P_proof_admit ->
            (* If the proof is finished, display a warning. *)
+


remove this useless modification to minimize the diff

fblanqui · 2019-06-05T09:22:48Z

src/sr.ml

 open Print
 open Extra
+open Terms


Minimize the diff

fblanqui · 2019-06-05T09:23:53Z

src/sr.ml

-  Meta(m,[||])
-*)
+let sr_not_preserved_msg (s, h, r) =
+  fatal r.pos "Rule [%a] does not preserve typing." pp_rule (s, h, r.elt)


does not -> may not

fblanqui · 2019-06-05T09:29:31Z

src/sr.ml

+(** [check_rule symbs builtins r] checks whether rule [r] is well-typed. The
+    program fails gracefully in case of error. *)
+let check_rule :
+  sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit


Is the pp_hint argument useful?

src/unif.ml

fblanqui · 2019-06-05T14:54:52Z

make sanity_check fails. Thanks to fix it.

fblanqui · 2020-04-05T08:53:50Z

This PR is probably too old now. It should be completely rewritten after #328.

Define the relation used in the algorithm

89a6072

wujuihsuan2016 requested a review from fblanqui March 25, 2019 16:56

fblanqui reviewed Mar 25, 2019

View reviewed changes

src/subject_reduction.ml Outdated

module Eset = Set.Make(

struct

type t = (term * term)

Copy link

Member

fblanqui Mar 25, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Parentheses are useless here.

rlepigre reviewed Mar 25, 2019

View reviewed changes

wujuihsuan2016 changed the title ~~Define the relation used in our algorithm for checking subject reduction~~ Implementation of an algorithm for checking subject reduction Mar 26, 2019

wujuihsuan2016 added 4 commits April 1, 2019 12:01

Merge pull request #2 from Deducteam/master

c764164

Syncing the fork

Add the translation from Xml-light to Lambdapi

6b01d06

Fix some bugs

66be875

Add the function calculating critical pairs for algebraic LHS

09bf732

fblanqui reviewed Apr 10, 2019

View reviewed changes

fblanqui reviewed Jun 5, 2019

View reviewed changes

src/completion.ml

let compare = compare

end)

exception Not_DAG

Copy link

Member

fblanqui Jun 5, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Comment missing!

fblanqui reviewed Jun 5, 2019

View reviewed changes

src/sr.ml Outdated

open Print

open Extra

open Terms

Copy link

Member

fblanqui Jun 5, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Minimize the diff

fblanqui reviewed Jun 5, 2019

View reviewed changes

src/unif.ml Outdated Show resolved Hide resolved

wujuihsuan2016 added 9 commits June 5, 2019 19:32

Rename some functions

11e8428

Add an function for checking injectivity of symbols

6c69f32

Add some comments and make some modifications

abe4a3c

Modify the main funciton of SR-checking

1c2a2e4

Fix some bugs in the function for injectivity checking

47d1ffd

Rename some functions

2f7a5e7

Fix some bugs

f13d037

Fix some bugs

71eacf8

Add missing comments

9aa4992

fblanqui mentioned this pull request Dec 6, 2019

Extending the type preservation check Deducteam/Dedukti#189

Merged

6 tasks

fblanqui mentioned this pull request Apr 5, 2020

Work on inference, unification and subject-reduction #328

Merged


		type rule_ = sym * pp_hint * rule

		(** [cp builtins r1 r2] calculates the critical pairs of the rules r1 and r2

Implementation of an algorithm for checking subject reduction #200

Are you sure you want to change the base?

Implementation of an algorithm for checking subject reduction #200

Conversation

wujuihsuan2016 commented Mar 25, 2019

Choose a reason for hiding this comment

fblanqui commented Mar 25, 2019

fblanqui commented Mar 25, 2019

Choose a reason for hiding this comment

wujuihsuan2016 commented Mar 26, 2019

rlepigre commented Mar 26, 2019

wujuihsuan2016 commented Mar 26, 2019

fblanqui commented Mar 26, 2019 • edited Loading

fblanqui commented Mar 26, 2019

fblanqui commented Mar 26, 2019

wujuihsuan2016 commented Mar 29, 2019

fblanqui commented Mar 29, 2019

fblanqui commented Mar 29, 2019

rlepigre commented Mar 29, 2019

Choose a reason for hiding this comment

fblanqui commented Apr 10, 2019

fblanqui Apr 10, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

wujuihsuan2016 Jun 5, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fblanqui commented Jun 5, 2019

fblanqui commented Apr 5, 2020

fblanqui commented Mar 26, 2019 •

edited

Loading

fblanqui Apr 10, 2019 •

edited

Loading

wujuihsuan2016 Jun 5, 2019 •

edited

Loading