Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
Overview
Comment:  Started work on making backchaining of goals a) apply the substitution to the expansion, rather than appending it as a conjunction of unifications, b) return the substitution along with each branch of the expansion, and c), return the name of the branch that was chosen (analogous to the index N parameter in `choice` proofs). 

Downloads:  Tarball  ZIP archive  SQL archive 
Timelines:  family  ancestors  descendants  both  bcsubst 
Files:  files  file ages  folders 
SHA1:  1252a63f557d9df9b659bfc3ee61d81289ba9928 
User & Date:  andy 20150420 09:54:43 
Context
20150420
 
20:57  Fixed (maybe) the filtering of substitutions for "interesting" variables. checkin: abb4d08745 user: andy tags: bcsubst  
09:54  Started work on making backchaining of goals a) apply the substitution to the expansion, rather than appending it as a conjunction of unifications, b) return the substitution along with each branch of the expansion, and c), return the name of the branch that was chosen (analogous to the index N parameter in `choice` proofs). checkin: 1252a63f55 user: andy tags: bcsubst  
09:52  Fixed a minor typo. Leaf checkin: adaef9d668 user: andy tags: trunk  
Changes
Changes to plsrc/checker.pl.
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 
* implies(Proof) proves A > B by adding A to the context and then
recursively proving B.
* ctxmem(Index) proves a term that is a member of the context
(I.e., this is the assumption rule)
* backchain(Proof) proves a term by backchaining a rule from the
program.
* unify(A,B) prove a unification by adding another binding to
the substitution.
* case(T,N,Keep,[Proofs]) perform case analysis on the nth member of the
context. A case analysis may require multiple
subproofs. (Case analysis amounts to using a Left

  > > 
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 
* implies(Proof) proves A > B by adding A to the context and then recursively proving B. * ctxmem(Index) proves a term that is a member of the context (I.e., this is the assumption rule) * backchain(Name,Proof) proves a term by backchaining a rule from the program. Name identifies the particular clause of the definition that was used. (Akin to N for disjunctions.) * unify(A,B) prove a unification by adding another binding to the substitution. * case(T,N,Keep,[Proofs]) perform case analysis on the nth member of the context. A case analysis may require multiple subproofs. (Case analysis amounts to using a Left 
Changes to plsrc/program.pl.
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 ... 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 ... 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 
call_goal_h(Program,BVars,Goal,Unnormalized), normalize(Unnormalized,Expansion). call_goal_h(Program,BVars,Goal,or(Clauses)) : % For inductive goals we split out the base goal, call it, and then % reapply the smaller inductive size to the resulting subgoals. inductive(Goal,Base,Size), !, call_goal_h(Program,BVars,Base,or(NIClauses)), inductive_shrink(Size,NewSize), maplist(inductify_subgoals(NewSize),NIClauses,Clauses). % To call a normal goal, just get its definition and then call each clause. call_goal_h(Program,BVars,Goal,or(Clauses)) : % Get all matching clauses (based on functor and arity only). % Defs will be a list of rule()s get_defs(Program,Goal,Defs), ( Defs = [] > % We have to explicitly fail here, as call_clauses won't fail ................................................................................ call_clauses(BVars,Goal,[DDs],[CCs]) : call_clause(BVars,Goal,D,C), !, call_clauses(BVars,Goal,Ds,Cs). call_clauses(BVars,Goal,[_Ds],Cs) : call_clauses(BVars,Goal,Ds,Cs). % To call a single clause, rename its variables, unify its head with the % goal, and then add the resulting substitution to the (renamed) body. call_clause(BVars,Goal,rule(Name,Head,Body),and(FullBody)) : % Rename variables in the definition so they do not collide. make_safe_def(BVars,rule(Name,Head,Body),rule(_,SHead,and(SBody))), % Unify SHead with Goal get_subst(SHead,Goal,Subst), % Merge substitution (list of V = T) with body % TODO: make this apply the substitution to the body, rather than prepend. % The trouble with this is that we also need to return the substitution, % which, since we return a disjunction, we have no way of doing. Embedding % the substitution as a conjunction of A = B goals has the side effect of % constructing the substitution to be returned in each clause. append(Subst, SBody, FullBody). %%%  %%% Execution %%%  % Running goals in the specification language: We only support the features that % are allowed in specification programs. See checker.pl for the full % (reasoning) execution/checking system. Note that the derivations produced by % run/3 are compatible with (a subset of) those produced by check/3. run(Program,Goal,proof(Goal,Ctx,FSubst,Deriv)) : get_vars(Goal,Vars), run(Program,Vars,Goal,_,proof(Goal,Ctx,Subst,Deriv)), subst_filter(Subst,Vars,FSubst). % run(Program,Vars,Goal,Vout,Proof) %  Program: The current program %  Vars: incoming list of bound variables %  Goal: goal to prove %  Vout: returned list of bound vars ................................................................................ %  Proof: a proof object of the form proof(Subst,Derivation) % Trivial cases run(_,Vars,true,Vars,proof(true,[],[],trivial)). run(_,_,false,_,_) : fail. % User goals run(Program,BVars,Goal,VOut,proof(Goal,[],Subst,backchain(SubProof))) : is_user_goal(Goal), % Get the variables used in the goal, and add it to the set of bound % variables. get_vars(Goal,NVars), union(BVars,NVars,Vars), % Call the goal, getting its expansion call_goal(Program, Vars, Goal, Expansion), get_vars(Expansion,V2), union(Vars,V2,MoreVars), % Run the expansion, returning its substitution and proof. run(Program,MoreVars,Expansion,VOut,SubProof), SubProof = proof(_,_,Subst,_). % Conjunction: %  The empty conjunction is proved by the empty substitution and product() %  A nonempty conj. runs the head, collecting its proof and substitution. % After each subgoal, we apply the resulting substitution to the remainder % of the conjunction. run(_,BVars,and([]),BVars,proof(and([]),[],[],product([]))). 
    >  < < < < <       > > < > > > > > > > > > > >  > 
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 ... 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 ... 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 
call_goal_h(Program,BVars,Goal,Unnormalized), normalize(Unnormalized,Expansion). call_goal_h(Program,BVars,Goal,or(Clauses)) : % For inductive goals we split out the base goal, call it, and then % reapply the smaller inductive size to the resulting subgoals. inductive(Goal,Base,Size), !, call_goal_h(Program,BVars,Base,NIClauses), inductive_shrink(Size,NewSize), maplist(inductify_subgoals(NewSize),NIClauses,Clauses). % To call a normal goal, just get its definition and then call each clause. call_goal_h(Program,BVars,Goal,Clauses) : % Get all matching clauses (based on functor and arity only). % Defs will be a list of rule()s get_defs(Program,Goal,Defs), ( Defs = [] > % We have to explicitly fail here, as call_clauses won't fail ................................................................................ call_clauses(BVars,Goal,[DDs],[CCs]) : call_clause(BVars,Goal,D,C), !, call_clauses(BVars,Goal,Ds,Cs). call_clauses(BVars,Goal,[_Ds],Cs) : call_clauses(BVars,Goal,Ds,Cs). % To call a single clause, rename its variables, unify its head with the % goal, and then return a clause() with the resulting substitution. call_clause(BVars,Goal,rule(Name,Head,Body), clause(Name,Subst,and(FullBody))) : % Rename variables in the definition so they do not collide. make_safe_def(BVars,rule(Name,Head,Body),rule(Name,SHead,and(SBody))), % Unify SHead with Goal get_subst(SHead,Goal,Subst), % Merge substitution (list of V = T) with body apply_subst(Subst, SBody, FullBody). %%%  %%% Execution %%%  % Running goals in the specification language: We only support the features that % are allowed in specification programs. See checker.pl for the full % (reasoning) execution/checking system. Note that the derivations produced by % run/3 are compatible with (a subset of) those produced by check/3. run(Program,Goal,proof(Goal,Ctx,FSubst,Deriv)) : get_vars(Goal,Vars), run(Program,Vars,Goal,_,proof(Goal,Ctx,FSubst,Deriv)). %subst_filter(Subst,Vars,FSubst). % run(Program,Vars,Goal,Vout,Proof) %  Program: The current program %  Vars: incoming list of bound variables %  Goal: goal to prove %  Vout: returned list of bound vars ................................................................................ %  Proof: a proof object of the form proof(Subst,Derivation) % Trivial cases run(_,Vars,true,Vars,proof(true,[],[],trivial)). run(_,_,false,_,_) : fail. % User goals run(Program,BVars,Goal,VOut,proof(Goal,[],Subst,backchain(Name,SubProof))) : is_user_goal(Goal), % Get the variables used in the goal, and add it to the set of bound % variables. get_vars(Goal,NVars), union(BVars,NVars,Vars), % Call the goal, getting its expansion call_goal(Program, Vars, Goal, Clauses), get_vars(Clauses,V2), union(Vars,V2,MoreVars), % Run the clauses, returning the substitution of the one(s) that works. % Run the expansion, returning its substitution and proof. run_clauses(Program,MoreVars,VOut,Clauses,SubProof,Subst,Name). % Helper for running the clauses returned by call_goal. run_clauses(Program,BVars,VOut,Clauses, Proof,Subst,Name) : member(clause(Name,Sub1,Clause),Clauses), run(Program,BVars,Clause,VOut,Proof), % Merge the substitution from the clause with the substitution from its % execution. Proof = proof(_,_,Sub2,_), subst:merge(Sub1,Sub2,Subst). % Conjunction: %  The empty conjunction is proved by the empty substitution and product() %  A nonempty conj. runs the head, collecting its proof and substitution. % After each subgoal, we apply the resulting substitution to the remainder % of the conjunction. run(_,BVars,and([]),BVars,proof(and([]),[],[],product([]))). 
Changes to src/proof.js.
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 
// 0 subproofs case "trivial": case "hole": case "unify": case "ctxmem": return []; // 1 subproof, first argument case "ih": case "generic": case "implies": case "backchain": return [pr.body[0]]; // 1 subproof, last argument case "induction": case "instan": case "choice": return [pr.body[pr.body.length1]]; // Product case "product": 
 < < < 
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 
// 0 subproofs case "trivial": case "hole": case "unify": case "ctxmem": return []; // 1 subproof, always in the last argument. case "ih": case "generic": case "implies": case "backchain": case "induction": case "instan": case "choice": return [pr.body[pr.body.length1]]; // Product case "product": 