(**** ML Programs from Chapter 10 of   ML for the Working Programmer, 2nd edition  by Lawrence C. Paulson, Computer Laboratory, University of Cambridge.  (Cambridge University Press, 1996) Copyright (C) 1996 by Cambridge University Press.Permission to copy without fee is granted provided that this copyrightnotice and the DISCLAIMER OF WARRANTY are included in any copy. DISCLAIMER OF WARRANTY.  These programs are provided `as is' withoutwarranty of any kind.  We make no warranties, express or implied, that theprograms are free of error, or are consistent with any particular standardof merchantability, or that they will meet your requirements for anyparticular application.  They should not be relied upon for solving aproblem whose incorrect solution could result in injury to a person or lossof property.  If you do use the programs or functions in such a manner, itis at your own risk.  The author and publisher disclaim all liability fordirect, incidental or consequential damages resulting from your use ofthese programs or functions.****)  (*TACTIC-BASED PROVER FOR CLASSICAL FIRST-ORDER LOGIC*) (*variables      a,b,c: string     qnt: string (quantifier name)      i,j: int    (Bound indices)    t,u: term    p,q: form    x,y: any     f,g: functions *) (**** Terms and Formulae ****)signature FOL =  sig  datatype term = Var   of string		| Param of string * string list		| Bound of int		| Fun   of string * term list  datatype form = Pred  of string * term list		| Conn  of string * form list		| Quant of string * string * form  type goal = form list * form list  val precOf: string -> int  val abstract: int -> term -> form -> form  val subst: int -> term -> form -> form  val termVars: term * string list -> string list  val goalVars: goal * string list -> string list  val termParams: term * (string * string list) list                   -> (string * string list) list  val goalParams: goal * (string * string list) list                   -> (string * string list) list  end;  structure Fol : FOL =  struct  datatype term = Var   of string		| Param of string * string list		| Bound of int		| Fun   of string * term list;  datatype form = Pred  of string * term list		| Conn  of string * form list		| Quant of string * string * form;   type goal = form list * form list;   (*Replace the term u1 by u2 throughout a term t*)  fun replace (u1,u2) t =      if t=u1 then u2 else	  case t of Fun(a,ts) => Fun(a, map (replace(u1,u2)) ts)		  | _         => t;   (*Abstraction of a formula over the atomic term t. *)  fun abstract i t (Pred(a,ts)) = Pred(a, map (replace (t, Bound i)) ts)    | abstract i t (Conn(b,ps)) = Conn(b, map (abstract i t) ps)    | abstract i t (Quant(qnt,b,p)) = Quant(qnt, b, abstract (i+1) t p);   (*Replace (Bound i) by t in formula. t may contain no bound vars *)  fun subst i t (Pred(a,ts)) = Pred(a, map (replace (Bound i, t)) ts)    | subst i t (Conn(b,ps)) = Conn(b, map (subst i t) ps)    | subst i t (Quant(qnt,b,p)) = Quant(qnt, b, subst (i+1) t p);   (*Precedence table: used by parsing AND display! *)  fun precOf "~"   = 4    | precOf "&"   = 3    | precOf "|"   = 2    | precOf "<->" = 1    | precOf "-->" = 1    | precOf _     = ~1    (*means not an infix*);   (*Accumulate a term function over all terms in a formula*)  fun accumForm f (Pred(_,ts), z) = foldr f z ts    | accumForm f (Conn(_,ps), z) = foldr (accumForm f) z ps    | accumForm f (Quant(_,_,p), z) = accumForm f (p,z);   (*Accumulate a form function over all formulae in a goal [POLYMORHPIC]*)  fun accumGoal f ((ps,qs), z) = foldr f (foldr f z qs) ps;   (*insertion into ordered list of strings*)  fun insert (a,[]) = [a]    | insert (a,b::bs) = case String.compare (a,b) of                             LESS => a::b::bs			   | EQUAL => b::bs			   | GREATER => b::insert(a,bs);   (*Accumulate all Vars in the term (except in a Param).*)  fun termVars (Var a, bs) = insert(a,bs)    | termVars (Fun(_,ts), bs) = foldr termVars bs ts    | termVars (_, bs) = bs;  val goalVars = accumGoal (accumForm termVars);   (*Accumulate all Params*)  fun termParams (Param(a,bs), pairs) = (a,bs) :: pairs    | termParams (Fun(_,ts), pairs) = foldr termParams pairs ts    | termParams (_, pairs) = pairs;  val goalParams = accumGoal (accumForm termParams);  end; (**** Syntax: scanning, parsing, and display ****) structure FolKey =     struct val alphas = ["ALL","EX"]           and symbols = ["(", ")", ".", ",", "?", "~", "&", "|",                           "<->", "-->", "|-"]    end;structure FolLex = Lexical (FolKey);structure FolParsing = Parsing (FolLex);     (*** Parsing of First-order terms & formulae ***)signature PARSE_FOL =  sig  val read: string -> Fol.form  end; structure ParseFol : PARSE_FOL =  struct  local      open FolParsing     (*One or more phrases separated by commas*)    fun list ph = ph -- repeat ("," $-- ph) >> (op::);     (*Either (ph,...,ph) or empty. *)    fun pack_ ph =    "(" $-- list ph -- $")" >> #1		  || empty;     (*Make a quantifier from parsed information*)    fun makeQuant ((qnt,b),p) = 	Fol.Quant(qnt, b, Fol.abstract 0 (Fol.Fun(b,[])) p);     (*Make a connective*)    fun makeConn a p q = Fol.Conn(a, [p,q]);    fun makeNeg p = Fol.Conn("~", [p]);     fun term toks =      (   id   -- pack_ term		>> Fol.Fun       || "?" $-- id			>> Fol.Var   ) toks;     fun form toks =      (   $"ALL" -- id -- "." $-- form 	>> makeQuant       || $"EX"  -- id -- "." $-- form 	>> makeQuant       || infixes (primary, Fol.precOf, makeConn)  ) toks    and primary toks =      (   "~" $-- primary      		>> makeNeg       || "(" $-- form -- $")" 		>> #1       || id -- pack_ term		>> Fol.Pred   )  toks;    in        val read = reader form    end  end;  (*** Pretty Printing of terms, formulae, and goals ***) signature DISPLAY_FOL =  sig  val form: Fol.form -> unit  val goal: int -> Fol.goal -> unit  end; structure DisplayFol : DISPLAY_FOL =  struct  fun enclose sexp = Pretty.blo(1, [Pretty.str"(", sexp, Pretty.str")"]);    fun commas [] = []    | commas (sexp::sexps) = Pretty.str"," :: Pretty.brk 1 :: 			     sexp :: commas sexps;   fun list (sexp::sexps) = Pretty.blo(0, sexp :: commas sexps);     fun term (Fol.Param(a,_)) = Pretty.str a     | term (Fol.Var a) = Pretty.str ("?"^a)    | term (Fol.Bound i) = Pretty.str "??UNMATCHED INDEX??"    | term (Fol.Fun (a,ts)) = Pretty.blo(0, [Pretty.str a, args ts])  and args [] = Pretty.str""    | args ts = enclose (list (map term ts));   (*display formula in context of operator with precedence k *)  fun formp k (Fol.Pred (a,ts)) = Pretty.blo(0, [Pretty.str a, args ts])    | formp k (Fol.Conn("~", [p])) =           Pretty.blo(0, [Pretty.str "~", formp (Fol.precOf "~") p])    | formp k (Fol.Conn(C, [p,q])) =	  let val pf = formp (Int.max(Fol.precOf C, k))	      val sexp = Pretty.blo(0, [pf p, 					Pretty.str(" "^C), 					Pretty.brk 1, 					pf q])	  in  if (Fol.precOf C <= k) then (enclose sexp) else sexp	  end    | formp k (Fol.Quant(qnt,b,p)) =	  let val q = Fol.subst 0 (Fol.Fun(b,[])) p	      val sexp = Pretty.blo(2, 				    [Pretty.str(qnt ^ " " ^ b ^ "."), 				     Pretty.brk 1,  				     formp 0 q])	  in  if  k>0  then  (enclose sexp)  else sexp  end    | formp k _ = Pretty.str"??UNKNOWN FORMULA??";   fun formList [] = Pretty.str"empty"    | formList ps = list (map (formp 0) ps);   fun form p = Pretty.pr (TextIO.stdOut, formp 0 p, 50);   fun goal (n:int) (ps,qs) =      Pretty.pr (TextIO.stdOut, 		Pretty.blo (4, [Pretty.str(" " ^ Int.toString n ^  ". "), 				formList ps,				Pretty.brk 2,				Pretty.str"|-  ",				formList qs]),	 50);  end;  (**** UNIFICATION ****) signature UNIFY =  sig  exception Failed  val atoms: Fol.form * Fol.form -> Fol.term StringDict.t  val instTerm: Fol.term StringDict.t -> Fol.term -> Fol.term  val instForm: Fol.term StringDict.t -> Fol.form -> Fol.form  val instGoal: Fol.term StringDict.t -> Fol.goal -> Fol.goal  end; structure Unify : UNIFY =  struct  exception Failed;   (*Naive unification of terms containing no bound variables*)  fun unifyLists env =    let fun chase (Fol.Var a) =  (*Chase variable assignments*)	      (chase(StringDict.lookup(env,a)) 	       handle StringDict.E _ => Fol.Var a)	  | chase t = t	fun occurs a (Fol.Fun(_,ts)) = occsl a ts	  | occurs a (Fol.Param(_,bs)) = occsl a (map Fol.Var bs)	  | occurs a (Fol.Var b) = 	        (a=b) orelse (occurs a (StringDict.lookup(env,b))  			      handle StringDict.E _ => false)	  | occurs a _ = false	and occsl a = List.exists (occurs a)	and unify (Fol.Var a, t) = 	      if t = Fol.Var a then env               else if occurs a t then raise Failed  	                         else StringDict.update(env,a,t)	  | unify (t, Fol.Var a) = unify (Fol.Var a, t)	  | unify (Fol.Param(a,_), Fol.Param(b,_)) =	      if a=b then env  else  raise Failed	  | unify (Fol.Fun(a,ts), Fol.Fun(b,us)) =  	      if a=b then unifyl(ts,us) else raise Failed	  | unify _ =  raise Failed       and unifyl ([],[]) = env	 | unifyl (t::ts, u::us) =               unifyLists (unify (chase t, chase u)) (ts,us)	 | unifyl _ =  raise Failed      in  unifyl  end   (*Unification of atomic formulae*)  fun atoms (Fol.Pred(a,ts), Fol.Pred(b,us)) =  	  if a=b then unifyLists StringDict.empty (ts,us)  	         else raise Failed    | atoms _ =  raise Failed;   (*Instantiate a term by an environment*)  fun instTerm env (Fol.Fun(a,ts)) = Fol.Fun(a, map (instTerm env) ts)    | instTerm env (Fol.Param(a,bs)) =	Fol.Param(a, foldr Fol.termVars [] 		           (map (instTerm env o Fol.Var) bs))    | instTerm env (Fol.Var a) = (instTerm env (StringDict.lookup(env,a))			      handle StringDict.E _ => Fol.Var a)    | instTerm env t = t;   (*Instantiate a formula*)  fun instForm env (Fol.Pred(a,ts))   = Fol.Pred(a, map (instTerm env) ts)    | instForm env (Fol.Conn(b,ps))   = Fol.Conn(b, map (instForm env) ps)    | instForm env (Fol.Quant(qnt,b,p)) = Fol.Quant(qnt, b, instForm env p);   fun instGoal env (ps,qs) =         (map (instForm env) ps, map (instForm env) qs);  end;   (**** Rules and proof states -- the abstract type "state" ****) signature RULE =  sig  type state  type tactic = state -> state ImpSeq.t  val main: state -> Fol.form  val subgoals: state -> Fol.goal list  val initial: Fol.form -> state  val final: state -> bool  val basic: int -> tactic  val unify: int -> tactic  val conjL: int -> tactic  val conjR: int -> tactic  val disjL: int -> tactic  val disjR: int -> tactic  val impL: int -> tactic  val impR: int -> tactic  val negL: int -> tactic  val negR: int -> tactic  val iffL: int -> tactic  val iffR: int -> tactic  val allL: int -> tactic  val allR: int -> tactic  val exL: int -> tactic  val exR: int -> tactic  end;  (*Note use of :> for abstraction*)structure Rule :> RULE =  struct   (*A state contains subgoals, main goal, variable counter *)  datatype state = State of Fol.goal list * Fol.form * int;   type tactic = state -> state ImpSeq.t;   fun main (State(gs,p,_)) = p  and subgoals (State(gs,p,_)) = gs;   (*initial state has one subgoal *)  fun initial p = State([ ([],[p]) ], p, 0);   (*final state has no subgoals.*)  fun final (State(gs,_,_)) = null gs;   (*add the goals "newgs" to replace subgoal i*)  fun spliceGoals gs newgs i = List.take(gs,i-1) @ newgs @ List.drop(gs,i);   (*goalF maps goal -> goal list; operator makes a deterministic tactic*)  fun propRule goalF i (State(gs,p,n)) =      let val gs2 = spliceGoals gs (goalF (List.nth(gs,i-1))) i      in  ImpSeq.fromList [State(gs2, p, n)]  end      handle _ => ImpSeq.empty;   (*for basic sequents: with identical formulae on opposite sides*)  val basic = propRule	       (fn (ps,qs) => 		if List.exists (fn p => List.exists (fn q => p=q) qs) ps		then [] else raise Match);   (*Solves goal p|-q by unifying p with q.    Returns list of successful environments. *)  fun unifiable ([], _) = ImpSeq.empty    | unifiable (p::ps, qs) = 	let fun find [] = unifiable (ps,qs)	      | find (q::qs) = ImpSeq.cons(Unify.atoms(p,q), fn() => find qs)			       handle Unify.Failed => find qs	in  find qs  end;   fun inst env (gs,p,n) =	State (map (Unify.instGoal env) gs,  Unify.instForm env p, n);   (*for solvable goals with unifiable formulae on opposite sides*)  fun unify i (State(gs,p,n)) =    let val (ps,qs) = List.nth(gs,i-1)	fun next env = inst env (spliceGoals gs [] i, p, n)    in  ImpSeq.map next (unifiable(ps,qs))  end    handle Subscript => ImpSeq.empty;    (*** Tactics for propositional rules ***)   (* return & delete first formula of the form Conn(a,_,_) *)  fun splitConn a qs =    let fun get [] = raise Match	  | get (Fol.Conn(b,ps) :: qs) = if a=b then ps else get qs	  | get (q::qs) = get qs;	fun del [] = []	  | del ((q as Fol.Conn(b,_)) :: qs) = if a=b then qs 					       else q :: del qs	  | del (q::qs) = q :: del qs    in (get qs, del qs)  end;   (*leftF transforms left-side formulae to new subgoals*)  fun propL a leftF = propRule (fn (ps,qs) => leftF (splitConn a ps, qs));   (*rightF transforms right-side formulae to new subgoals*)  fun propR a rightF = propRule (fn (ps,qs) => rightF (ps, splitConn a qs));   val conjL = propL "&" (fn (([p1,p2], ps), qs) => [(p1::p2::ps, qs)]);   val conjR = propR "&"       (fn (ps, ([q1,q2], qs)) => [(ps, q1::qs),  (ps, q2::qs)]);   val disjL = propL "|"       (fn (([p1,p2], ps), qs) => [(p1::ps, qs),  (p2::ps, qs)]);   val disjR = propR "|" (fn (ps, ([q1,q2], qs)) => [(ps, q1::q2::qs)]);   val impL = propL "-->"       (fn (([p1,p2], ps), qs) => [(p2::ps, qs),  (ps, p1::qs)]);   val impR = propR "-->" (fn (ps, ([q1,q2], qs)) => [(q1::ps, q2::qs)]);   val negL = propL "~" (fn (([p], ps), qs) => [(ps, p::qs)]);   val negR = propR "~" (fn (ps, ([q], qs)) => [(q::ps, qs)]);   val iffL = propL "<->"       (fn (([p1,p2], ps), qs) => [(p1::p2::ps, qs),  (ps, p1::p2::qs)]);   val iffR = propR "<->"      (fn (ps, ([q1,q2], qs)) => [(q1::ps, q2::qs),  (q2::ps, q1::qs)]);    (*** Tactics for quantifier rules ***)   (* return & delete first formula of the form Quant(qnt,_,_) *)  fun splitQuant qnt qs =    let fun get [] = raise Match	  | get ((q as Fol.Quant(qnt2,_,p)) :: qs) = if qnt=qnt2 then q						     else get qs	  | get (q::qs) = get qs;	fun del [] = []	  | del ((q as Fol.Quant(qnt2,_,p)) :: qs) = if qnt=qnt2 then qs						     else q :: del qs	  | del (q::qs) = q :: del qs    in (get qs, del qs)  end;   fun letter n = String.substring("abcdefghijklmnopqrstuvwxyz", n, 1)   fun gensym n = (* the "_" prevents clashes with user's variable names*)     if n<26 then "_" ^ letter n     else gensym(n div 26) ^ letter(n mod 26);   fun quantRule goalF i (State(gs,p,n)) =      let val gs2 = spliceGoals gs (goalF (List.nth(gs,i-1), gensym n)) i      in  ImpSeq.fromList [State(gs2, p, n+1)]  end      handle _ => ImpSeq.empty;   val allL = quantRule (fn ((ps,qs), b) =>      let val (qntForm as Fol.Quant(_,_,p), ps') = splitQuant "ALL" ps	  val px = Fol.subst 0 (Fol.Var b) p      in  [(px :: ps' @ [qntForm], qs)]  end);   val allR = quantRule (fn ((ps,qs), b) =>      let val (Fol.Quant(_,_,q), qs') = splitQuant "ALL" qs	  val vars = Fol.goalVars ((ps,qs), [])	  val qx = Fol.subst 0 (Fol.Param(b, vars)) q      in  [(ps, qx::qs')]  end);   val exL = quantRule (fn ((ps,qs), b) =>      let val (Fol.Quant(_,_,p), ps') = splitQuant "EX" ps	  val vars = Fol.goalVars ((ps,qs), [])	  val px = Fol.subst 0 (Fol.Param(b, vars)) p      in  [(px::ps', qs)]  end);   val exR = quantRule (fn ((ps,qs), b) =>      let val (qntForm as Fol.Quant(_,_,q), qs') = splitQuant "EX" qs	  val qx = Fol.subst 0 (Fol.Var b) q      in  [(ps, qx :: qs' @ [qntForm])]  end);   end;  (**** Commands to modify the top-level proof state   Each level of goal stack includes a proof state and alternative states,  the output of the tactic applied to the preceeding level.       EXERCISE: design and implement better undo facilities. ****) signature COMMAND =  sig  val goal: string -> unit  val by: Rule.tactic -> unit  val pr: Rule.state -> unit  val getState: unit -> Rule.state  end; structure Command : COMMAND =  struct 

Lines 1–500 of 642. Load more