Chart object
From Dyna
oralro cnaeltc4tbod orcnapaser erricvarrac ricrolc4tace
Contents |
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
mychart.fassert("filename")
Discuss file format, e.g.,
word("hello",3,4) := 1.0.
Retraction
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
pathto("foo")+edge("foo","myvertex")
start("myvertex")
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_iteratortopathto::antecedent::iterator. So don't use the default nameiteratorfor any other queries that you might define overpathto::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;
if(i.is_times()){
times t = i.to_times();
backtrace(c, t.field0(), recursion + 1);
backtrace(c, t.field1(), recursion + 1);
}else {
if(c.has_best_antecedent(i)){
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
c.peek
Forcing computation
build
dequeue_build (with sample loop)
