Check-in [1252a63f55]

Not logged in

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 | bc-subst
Files: files | file ages | folders
SHA1:1252a63f557d9df9b659bfc3ee61d81289ba9928
User & Date: andy 2015-04-20 09:54:43
Context
2015-04-20
20:57
Fixed (maybe) the filtering of substitutions for "interesting" variables. check-in: abb4d08745 user: andy tags: bc-subst
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). check-in: 1252a63f55 user: andy tags: bc-subst
09:52
Fixed a minor typo. Leaf check-in: adaef9d668 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

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 n-th member of the
                             context. A case analysis may require multiple 
                             sub-proofs. (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 n-th member of the
                             context. A case analysis may require multiple 
                             sub-proofs. (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
    % re-apply 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,[D|Ds],[C|Cs]) :-
    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 non-empty 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
    % re-apply 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,[D|Ds],[C|Cs]) :-
    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 non-empty 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.length-1]];

        // 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.length-1]];

        // Product
        case "product":