Thus, Dyna's items resemble the variables in a procedural language like C++.
bar might likewise have value 3.14 of type
(Why not just call them variables? Dyna already has something else called "variables," which resemble the variables in a logic programming language like Prolog. The name item is taken from traditional deductive parsing terminology.)
The value of an item may be stored, computed on demand, or both.
You can declare any structure type to be an item type. For example, if
bar is a structure type that you have already declared with
then you can write
:- item(bar, double, 0).
to say that every
bar term has a
double value, which is 0 by default.
Like many Dyna declarations, the
item declaration can take a union type as its first argument. For example,
:- item(list, boolean, false).
says that both
nil have boolean values. A common use is
:- item(item, int, 0).
which can be read as saying "all items are
int items" (unless declared otherwise). This works because
item is an automatically declared union type over all structure types that appear to be used as items in the program.
- Need link to a page about declarations that explains precisely what "unless declared otherwise" means. (Namely, a declaration is overridden by one that is strictly more specific.)
Theorems vs. axioms
A program's items can be partitioned into theorems and axioms.
A theorem is any item that can be derived by inference rule. Suppose
bar is an item type. If any
inference rule has a left-hand-side of the form
bar is considered to be a theorem type. Otherwise,
bar is an axiom type.
By contrast, axioms must get their values from "outside of the Dyna program," in one of the following ways.
The value of an axiom is ordinarily provided as input to the Dyna program. Typically, the C++ driver program asserts the values of certain axioms by using chart methods. These values are stored (in the Dyna chart).
If an axiom has not been asserted, its value is the default value for its type.
Suppose you are using Dyna to write an algorithm on weighted graphs. Your Dyna program makes use of
edge axioms that specify the graph:
:- structure(edge(int startvertex, int endvertex)). :- item(edge, double, 0). % an edge's value denotes its weight
However, sometimes there may be too many axioms to assert. For example, you might want to run an algorithm on an astronomically large or infinite graph (such as a Markov chain or game tree on a very large state space). It is infeasible to assert all the edges of the graph.
Of course, you cannot hope to run the algorithm without knowing mathematically what all the vertices and edges are. Presumably you are deriving the huge graph from some more compact underlying specification.
One option is to allow Dyna to do this derivation for you. Instead of asserting
edge axioms directly, you can assert axioms that encode the compact underlying specification, and then define inference rules that derive the
edge items as theorems.
However, you might prefer to use C++ to derive the edges from your underlying specification. In this case, you should declare
edge to be a foreign axiom:
The value of
edge(35,103) is still a
(by the previous declaration), but now it will be found by calling a C++ method that
You may also have to define additional C++ methods that return iterators over edges. In particular, if your program contains a rule such as
pathsum(V) += pathsum(U)*edge(U,V).
then you will have to write a method that can return an iterator over all edges
of the form
edge(35,V) that have non-default value, where
35 is passed in as a parameter to your method.
- The exact interface is still being worked out. The Dyna compiler will provide you with commented skeletons of the methods that you need to write, including the method for looking up particular values such as
edge(35,103). (The latter method should be marked optional if the Dyna program doesn't actually need to call it, but a skeleton should probably be included (and show how to obtain and return the default value), so that you can write it in case the user wants to do c[edge(35,103)] from the C++ side. Including this one is merely for consistency with other items, which I assume will invariably support value lookup even if the Dyna program doesn't specifically call for it -- I don't see any efficiency loss in declaring that query automatically for other items, since declaring a query does not commit to an efficient implementation.
- What if the user, rather than writing all the indices, wants to say that one index should be implemented as a subset of another? I guess they could declare that via a pragma, and then the skeleton for the former index wouldn't be generated.
Item types that are declared as foreign can only be used as axioms, never as theorems.
The C++ methods that define a foreign axiom type must provide behavior that is both consistent and stable. Consistent means that, for example, the iterators
edge(U,103) should agree on the weight of
edge(35,103). Stable means that this weight should not change without notification. (For assertable axioms, asserting a new value also ensures that derived theorems are updated. For foreign axioms, the value is under control of a user-defined function, and so the user must explicitly trigger an update if the value changes.)
- Typical case: a lexicalized parser with foreign grammar axioms. When we update parameters, the grammar axioms change. Even if there are currently no words (and hence no constits) asserted, there might still be some stored items derived by closure of the grammar axioms alone. (These might be backward-chained and memoized, or they might be forward-chained with the help of some other persistent axioms.) To handle this, the user should call a method that says that all the axioms that match a particular query have in effect been retracted and reasserted. (There might be two versions -- one that ensures that the set of axioms has not changed, only the values.) This should do whatever's necessary to retract memoized or forward-chained theorems, and in the latter case, enqueue fresh updates of a particular sort.
- Maybe we can separate the retraction and reassertion steps. So one could "turn off" all the grammar axioms, examine or modify the resulting chart, then turn the grammar axioms back on with new values. The simplest way to turn off an entire type of foreign axiom: while that type is retracted, Dyna could just skip calling the foreign methods, acting instead as if they returned no items. However, this isn't flexible enough to deal with retraction of arbitrary queries over foreign axioms. So in general, I think the support for retraction would really need to be provided by the user's implementation. That sounds like perhaps too much burden on the user, but I guess we only have to generate a skeleton interface for it if those queries are declared as retractable, so the user only has to lie in the bed he's made.
Future possibility: Formulas
It's possible that in future, Dyna will have another item type, the formula, in addition to theorems and axioms.
A formula item is like a theorem item in that its value is computed from other items. However, the actual formula for computing its value would be specified at runtime by the driver program, rather than at compile time by inference rules.
For example, if
foo is a formula type with accumulation operator
:=, then the driver program could define
foo(69) := 3*foo(20)+bar(8). Or if the accumulation operator is
+=, then the driver program could introduce a new addend via
foo(69) += 3*foo(20)+bar(8). These
foo items must store information about how they're computed, but otherwise they behave like theorems, with the same options for when to recompute their values, whether and how to store their antecedents and consequents, etc.
This makes it possible to use Dyna for efficient storage, recomputation, differentiation, and optimization of formulas that are specified at runtime.
To make this even more efficient, we should probably have a notion of anonymous formulas: terms of formula type
foo that are C++ objects (so they have names in C++) but don't have Dyna names like