lambdapi 2.2.0 · OCaml Package

Incremental verification of local confluence

by checking the joinability of critical pairs.

CP(l-->r, p, g-->d) = (s(r), s(l[d]_p) | s = mgu(l|_p,g) is the critical pair between l|_p and g.

CP*(l-->r, g-->d) = U CP(l-->r, p, g-->d) | p in FPos(l)

CP*(R,S) = U CP*(l-->r, g-->d) | l-->r in R, g-->d in S

The set of critical pairs of a rewrite system R is CP(R) = CP*(R,R).

We have CP(R U S) = CP*(R,R) U CP*(R,S) U CP*(S,R) U CP*(S,S).

As a consequence, assuming that we already checked the local confluence of R and add a new set S of rules, we do not need to check CP*(R,R) again.

Warning: we currently do not take into account the rules having higher-order pattern variables and critical pairs on AC symbols.

Remark: When trying to unify a subterm of a rule LHS with the LHS of another rule, we need to rename the pattern variables of one of the LHS to avoid name clashes. To this end, we use the shift function below which replaces Patt(i,n,_) by Patt(-i-1,n ^ "'",_). The printing function subs below takes this into account.

val log_cp : 'a Lplib.Base.outfmt -> 'a

val rule_of_pair : (Core.Term.term * Core.Term.term) Lplib.Base.pp

rule_of_pair ppf x prints on ppf the pair of term x as a rule.

val is_ho : Core.Term.rule -> bool

is_ho r says if r uses higher-order variables.

val is_definable : Core.Term.sym -> bool

is_definable s says if s is definable and non opaque but not AC.

val rule_of_def : Core.Term.sym -> Core.Term.term -> Core.Term.rule

rule_of_def s d creates the rule s --> d.

val replace : 
  Core.Term.term ->
  Core.Term.subterm_pos ->
  Core.Term.term ->
  Core.Term.term

replace t p u replaces the subterm of t at position p by u.

val occurs : int -> Core.Term.term -> bool

occurs i t returns true iff Patt(i,_,_) is a subterm of t.

val shift : Core.Term.term -> Core.Term.term

shift t replaces in t every pattern index i by -i-1.

type subs = Core.Term.term Lplib.Extra.IntMap.t

Type for pattern variable substitutions.

val subs : Core.Term.term Lplib.Extra.IntMap.t Lplib.Base.pp

val apply_subs : subs -> Core.Term.term -> Core.Term.term

apply_subs s t applies the pattern substitution s to t.

type iter =
  Common.Pos.popt ->
  (Core.Term.sym -> Core.Term.subterm_pos -> Core.Term.term -> unit) ->
  Core.Term.term ->
  unit

Type of subterm iterators.

val iter_subterms_from_pos : Core.Term.subterm_pos -> iter

iter_subterms_eq pos f p t iterates f on all subterms of t headed by a defined function symbol. p is the position of t in reverse order.

val iter_subterms_eq : iter

iter_subterms_eq pos f t iterates f on all subterms of t headed by a defined function symbol.

val iter_subterms : iter

iter_subterms pos f t iterates f on all strict subterms of t headed by a defined function symbol.

val unif : 
  Common.Pos.popt ->
  Core.Term.term ->
  Core.Term.term ->
  Core.Term.term Lplib.Extra.IntMap.t option

unif pos t u returns None if t and u are not unifiable, and Some s with s an idempotent mgu otherwise. Precondition: l and r must have distinct indexes in Patt subterms.

val can_handle : Core.Term.sym_rule -> bool

can_handle r says if the sym_rule r can be handled.

val iter_rules : 
  (Core.Term.rule -> unit) ->
  Core.Term.sym ->
  Core.Term.rule list ->
  unit

iter_rules h rs iterates function f on every rule of rs.

val iter_sym_rules : 
  (Core.Term.sym_rule -> unit) ->
  Core.Term.sym_rule list ->
  unit

iter_sym_rules h rs iterates function f on every rule of rs.

val iter_rules_of_sym : (Core.Term.rule -> unit) -> Core.Term.sym -> unit

iter_rules_of_sym h s iterates f on every rule of s.

type rule_id = Common.Pos.pos

Type of rule identifiers. Hack: we use the rule position to distinguish between user-defined and generated rules (in completion), by giving a unique negative start_line to every generated rule.

val id_sym_rule : Core.Term.sym_rule -> rule_id

id_sym_rule r returns the rule id of r.

val new_rule_id : unit -> rule_id

new_rule_id() generates a new unique rule id.

val is_generated : rule_id -> bool

is_generated i says if i is a generated rule id.

val int_of_rule_id : rule_id -> int

int_of_rule_id i returns a unique integer from i. /!\ i must be a generated rule.

type cp_fun =
  Common.Pos.popt ->
  rule_id ->
  Core.Term.term ->
  Core.Term.term ->
  Core.Term.subterm_pos ->
  Core.Term.term ->
  rule_id ->
  Core.Term.term ->
  Core.Term.term ->
  subs ->
  unit

Type of functions on critical pairs.

type cp_cand_fun =
  Common.Pos.popt ->
  rule_id ->
  Core.Term.term ->
  Core.Term.term ->
  Core.Term.subterm_pos ->
  Core.Term.term ->
  rule_id ->
  Core.Term.term ->
  Core.Term.term ->
  unit

Type of functions on critical pair candidates.

val cp_cand_fun : cp_fun -> cp_cand_fun

cp_cand_fun turns a cp_fun into a cp_cand_fun.

val iter_cps_with_rule : 
  iter ->
  cp_fun ->
  Common.Pos.popt ->
  Core.Term.sym_rule ->
  Core.Term.sym_rule ->
  unit

iter_cps_with_rule iter_subterms h pos sr1 sr2 applies h on all the critical pairs between all the subterms of the sr1 LHS and the sr2 LHS using the iterator iter_subterms.

val iter_cps_of_rules : 
  cp_fun ->
  Common.Pos.popt ->
  Core.Term.sym_rule list ->
  unit

iter_cps_of_rules h pos rs applies h on all the critical pairs of rs with itself.

val typability_constraints : Common.Pos.popt -> Core.Term.term -> subs option

typability_constraints pos t returns None if t is not typable, and Some s where s is a substitution implied by the typability of t.

val check_cp : cp_fun

check_cp pos _ l r p l_p _ g d s checks that, if l_p and g are unifiable with mgu s, then s(r) and s(l[d]_p) are joinable. Precondition: l and r must have distinct indexes in Patt subterms.

val check_cps_subterms_eq : Common.Pos.popt -> Core.Term.sym_rule -> unit

check_cps_subterms_eq pos sr1 checks the critical pairs between all the subterms of the sr1 LHS and all the possible rule LHS's.

val check_cps_sign_with : 
  Common.Pos.popt ->
  Core.Sign.t ->
  Core.Term.rule list Core.Term.SymMap.t ->
  unit

check_cps_sign_with pos rs' checks all the critical pairs between all the rules of the signature and rs'.

val check_cps : 
  Common.Pos.popt ->
  Core.Sign.t ->
  Core.Term.sym_rule list ->
  Core.Term.rule list Core.Term.SymMap.t ->
  unit

check_cps rs checks all the critical pairs generated by adding rs.

val update_cp_pos : 
  Common.Pos.popt ->
  Core.Term.cp_pos list Core.Term.SymMap.t ->
  Core.Term.rule list Core.Term.SymMap.t ->
  Core.Term.cp_pos list Core.Term.SymMap.t

update_cp_pos pos map rs extends map by mapping every definable symbol s' such that there is a rule l-->r of rs and a position p of l such that l_p is headed by s' to (l,r,p,l_p).

package lambdapi