Chart object

From Dyna
Jump to: navigation, search


What is a chart?

A chart is an instance of a Dyna program on particular input.

As discussed earlier, a chart object stores non-default values for the program's axioms, and enables you to retrieve the values of those axioms or of theorems derived from them.

For example, suppose you have a Dyna program for Dijkstra's algorithm, dijkstra.dyna. The program's axioms are the edges of some weighted graph. You can create several instances of dijkstra::chart, each one representing a different graph. You can ask each chart for the lengths of the shortest paths to vertices in its graph. You can also modify each graph by modifying its chart.

Constructing a chart

A chart constructor takes no arguments:

chart c;

Setting and querying chart values

Your primary tool for accessing the C++ chart is the [] operator.

Suppose you have the following declarations in Dyna:

:- structure(word(string, int, int)).
:- structure(constit(string, int, int)).
:- item(item, double, 0).         % all items have double values

Then you can write C++ code like this:

chart c;
c[word("time",0,1)] = 1.0;    // set value of an axiom
c[word("flies",1,2)] = 1.0;   // set value of an axiom
double d0 = c[word("time",0,1)];                            // get value of an axiom
double d1 = c[constit("s",0,2)];                            // get value of a theorem
double d2 = c[times(constit("s",0,2),word("quickly",2,3))]; // get value of a multiplicative expression

In general, you can use c[t] as a double value if the C++ type of t is any subtype of expr_double.

In general, you can write c[t]=some_double_value if the C++ type of t is any subtype of axiom_double (possibly a union type). This is known as asserting a value into the chart.

Note alternative syntax c.assertval(t, some_double_value). Shouldn't it be tassert, not assertval?

It is possible that the use of [] will be extended to deal with union types that do not have a consistent value type. For example, suppose we have

:- item(foo, int, 0).
:- item(bar, string, "").
:- union(foobar, [foo,bar]).

Suppose a and b are both variables of type foobar, If they are known to have the same value type, it would be nice to be able to write c[a]=c[b]. Notice that c[b] would have to return the union type [int,string], and assigning it to c[a] would have to do a runtime check for type compatibility.

The accumulation operator for an axiom is := by default. Discuss other options to be added.

Asserting input from a file


Discuss file format, e.g.,

word("hello",3,4) := 1.0.


The complement to assertion is retraction. You can retract a group of axioms, making their values return to default. Typically this will also change the values of some theorems. It may also release some memory.

A standard usage pattern is to assert some permanent axioms into a chart c, and then solve a sequence of problems. For each problem, one asserts some problem-specific axioms into c, reads off c[goal], and then retracts the problem-specific axioms as a group before moving on to the next problem. In the case of a parser, the permanent axioms describe the grammar, and the problem-specific axioms describe the sequence of words in the sentence to be parsed.

You need to specify in advance what kinds of things you will want to retract. The syntax in Dyna is exactly the same as declaring a query, except that you use the word retractable instead of query, and you are limited to queries that can only return axioms. The retractable declaration causes dynac to generate a retraction method that will retract everything that the query would have returned.

Here are some examples, showing a Dyna retractable declaration and the C++ method that is created as a result:

:- retractable(word).                            ==>      mychart.retract_word();
:- union(sentence_specific, [word,length]).
:- retractable(sentence_specific).               ==>      mychart.retract_sentence_specific();
:- structure(constit(string nonterm, int start, int end)).
:- retractable(constit(end)).                    ==>      mychart.retract_constit(23);
:- retractable(constit(end), constit_ending_at). ==>      mychart.retract_constit_ending_at(23);
:- retractable(constit(nonterm,start,end), specific_constit)
                                                 ==>      mychart.retract_specific_constit("np",3,8);
:- pattern(mypattern, constit("np",I,I)).
:- retractable(mypattern(I)).                    ==>      mychart.retract_mypattern(3);
At present, only the first two will work. The implementation is not yet able to retract arbitrary queries, nor even the special case of arbitrary items: here's why it's hard.

Retrieving antecedents and consequents

Once the chart has told you that c[goal] or c[pathto("Nirvana")] equals 42, you might wonder why. You might also wonder whether this information could help you prove any more theorems.

You should probably use the visual debugger to find out. However, perhaps you insist on writing your own program to walk through the proof forest -- for example, you want to print a proof tree to standard output.

Assume the inference rules

pathto(V) min= pathto(U)+edge(U,V).
pathto(V) min= start(V).

You can iterate as follows over all antecedent expressions that contributed to the value of a given pathto item in mychart:

pathto mypathto = pathto("myvertex");   // item whose antecedents we want
for (pathto::antecedent_iterator iter(mychart,mypathto); iter; iter++) {
   pathto::antecedent ant = *iter;
   cout << ant;

This will print expressions such as


You can analyze each of these expression terms to pull out an individual antecedent item, such as pathto("foo"). Then you can trace back further to its antecedent expressions.

The iterator class here works just like a query iterator, except that its constructor takes an unusual argument that is not available to queries, namely the item whose antecedents are to be returned.

The class name will probably change soon from pathto::antecedent_iterator to pathto::antecedent::iterator. So don't use the default name iterator for any other queries that you might define over pathto::antecedent, as in :- query('pathto::antecedent'(U)).
Temporarily, you need to declare :- pragma(keep_all_antecedents(item)) if you want this iterator class. This tells Dyna to store backpointers to the antecedents. A later version of Dyna will be able to recompute the backpointers on demand if they are not stored, so that whether to store them is just an efficiency decision or pragma.

The objects returned by the iterator are of type pathto::antecedent, which is a pattern over expressions. As explained earlier, such pattern types are automatically declared.

Consequent patterns and iterators are not implemented yet. We might also want to add antecedent_rule and consequent_rule patterns and iterators; these would match the full rule, pathto(V) min= pathto(U)+edge(U,V).

Retrieving the best antecedent

Often, you just want to get the "best" antecedent of an item -- for example, as part of finding the best path or parse tree. Add the following pragms to your dyna file:

:- pragma(keep_best_antecedents(item)).

This makes two chart functions available that you can call from your C++ driver program (only Dyna versions later than 0.3.6):

 bool has_best_antecedent(item i);
 item get_best_antecedent(item i);

Typically, you call them recursively like this:

int main(){
   chart c;
   backtrace(c, goal, 0);	
void backtrace(const chart& c, item i, unsigned recursion){
   cout << get_blanks(recursion) << i << endl;
       times t = i.to_times();
       backtrace(c, t.field0(), recursion + 1);
       backtrace(c, t.field1(), recursion + 1);
   }else {
           item best = c.get_best_antecedent(i);        
           backtrace(c, best, recursion + 1);

where get_blanks returns blanks according to the recursion level:

inline string get_blanks(unsigned n){
   stringstream blanks;
   for(unsigned cnt = n; cnt > 0; --cnt)
       blanks << "  ";
   return blanks.str();

Computation in the chart

what happens inside when you use []

controlling stopping criteria (to convergence, to first find, to priority threshold, etc.)

Avoiding computation


Forcing computation


dequeue_build (with sample loop)

Personal tools