ocaml write match sequent function

Question

I have to write a function match_sequent with 4 parameters :

1. first sequent
2. second sequent
3. optional subst Γ, with type form list option
4. list subst of Var

and return optional subst Γ and a list of Var.

We have some defined types:

type unop = Neg
type binop = Conj | Disj | Impl | Equiv

type form = 
  Const of bool
| Var of string
| Unop of unop * form
| Binop of binop * form * form

type sequent = Seq of form list * form

I wrote a function match_form that matches two forms and calculates a subst if it exists.

like this :

let rec match_form = function
   ((Const c1,Const c2)::e,sbst)->
     if c1=c2 then match_form(e,sbst)
.....
.....
.....

let form1 = Binop(Conj,Var "a",Var "b");; (* a/\b *)

let form2 = Binop(Conj, Binop(Disj, Const true, Const false), Const true);; (* ((p\/q)/\r) *)

(* Test match_form *)

match_form([(form1, form2)],[]);;
(* Output 
- : (string * form) list = 
    [("a", Binop (Disj, Const true, Const false)); ("b", Const true)]
*)

But really I'm struggling with this function match_sequent.

I try to deal with it but I have no idea how I can do that.

let rec match_sequent (s1 : sequent) (s2 : sequent) ?sopt svar = 
   match s1,s2 with 

   |.....;;

Thanks for any help

Answer 1

If my understanding is correct, you wish to unify two sequent calculus formulas, each made of first order logic formulas, for which you already have an unification algorithm.

From this premise, it's relatively straightforward to implement the algorithm: recall that a sequent formula is a formula whose "left hand side" is a conjunction of first order logic formulas (or forms as you named them) expressed as a tuple (the ∧ operator is implicit), and the right hand side, in your case, a single form (though it might theorically be a disjunction of formulas). Unification is therefore just unifying each pair of corresponding forms from the sequents.

let match_sequent s1 s2 ?sopt svar =
    match s1, s2 with
    Seq (lhs1,rhs1), Seq(lhs2,rhs2) -> 
    List.fold_left2 (fun l f1 f2 -> match_form (f1,f2)::l) [] (rhs1::lhs1) (rhs2::lhs2) 

My "guess" with regard to svar and/or sopt is that you would need to check that existing substitutions are not incompatible with the ones found by unification: that would require to compare the latter and the former, and for matching variable names, verify that their substitutions are either equals or that one is more general than the other, and keep the less general one.

Also note that the above algorithm is expecting lhs forms to have the exact same shape, so if lhs1 is simply a it will not unify with a lhs2 of b,c although b,c literally means b∧c, and would unify with a in first order logic. If your algorithm requires this unification to be acceptable, I suggest making the conjunction explicit by combining the lhs forms into a single one and then apply match_form unification on them.

let match_sequent (Seq (lhs1,rhs1)) (Seq (lhs2,rhs2)) ?opt svar =
    match lhs1,lhs2 with
      f1::lhs1, f2::lhs2 -> 
(match_form (List.fold_left conj f1 lhs1) (List.fold_left conj f2 lhs2)) @ (match_form rhs1 rhs2)
    | [], lhs
    | lhs, [] -> (* empty premises for at least one of the sequent *)
        match_form rhs1 rhs2

Where conj is a function constructing a conjunction of formulas:

val conj: form -> form -> form

Again, the last parameters need to be integrated in the algorithm somehow.

One last consideration I would like to point out is that a∧b∧c could be written in 2 different ways, depending on the application ordering of the ∧ operators in there. I suppose that either your match_form function or the conj pseudo constructor take care of rebalancing formulas to a "normal form".