Tabled logic programming
The operational semantics of STELF are similar to those of Prolog,
a style known as backward chaining or goal-directed proof
search. Tabled logic programming, which uses STELF’s
%tabled and %querytabled directives to
allow STELF to prove theorems that might be time-consuming or
impossible to prove otherwise. The tabled logic programming
capabilities are a
part of STELF’s capabilities as a logical framework, but not as a
metalogical framework; in other worlds, tabled logic programming
cannot be used to prove metatheorems.
The simplest examples of the power of tabled logic programming in practice involve judgments that involve transitive and/or symmetric closures, such as searching for a path in a graph or formalizing a language with subtyping. Using standard backward-chaining proof search, it is almost impossible to write terminating programs that search for paths, and using backward-chaining search for subtyping typically requires a separate definition of “algorithmic subtyping” that must be shown to be sound and complete with respect to the clearer, simpler definition of subtyping that uses transitivity.
This article will use as its example a path-finding algorithm on an undirected graphs.
Defining the graph
Section titled “Defining the graph”%sort node %.%term a node %.%term b node %.%term c node %.%term d node %.%term e node %.%term f node %.%term g node %.%term h node %.While we will consider edges in our graph to be undirected, we will only define the edge in one, arbitrary, direction.
%sort edge {_ node} {_ node} %.%term ab edge a b %.%term ac edge a c %.%term bc edge b c %.%term bd edge b d %.%term cd edge c d %.%term ce edge c e %.%term de edge d e %.%term df edge d f %.%term fg edge f g %.Paths in the graph
Section titled “Paths in the graph”This is normally where we would get into trouble; in standard
logic programming, it is difficult if not impossible to avoid
non-terminating behavior when writing a judgment defining a
transitive-symmetric closure like path. However, by
adding the directive [%tabled](/reference/Syntax/percent-tabled/) path, we will be able
to use %querytabled directives to cause each instance
of path A B to be derived at most once during the course
of a search: the result is a query that terminates rapidly,
instead of not at all.
%sort path {_ node} {_ node} %.%tabled path %.%term path/link %pi (edge A B) %-> (path A B) %.%term path/refl %pi (path A B) %-> (path B A) %.%term path/trans %pi (path A B) %-> (path B C) %-> (path A C) %.Searching the graph
Section titled “Searching the graph”It is crucial that we use %querytabled rather than
%query in our queries if we wish for them to terminate.
Even though we ask STELF for as many solutions as it can find, the
tabled proof search ensures that we can only find one proof of any
given path, and the path that is found is by not necessarily the shortest.
While the path that is found is shown on the graph above, the edge ab
actually appears three times here - if we use parenthesis to show the order in which
tabled search connected paths, the path that is found is
a - ((b - ((a - b - d) - f))
g).
%querytabled _ _ %the (path a g) D %.We can also run a terminating search for a path that does not exist,
such as one from a to h.
%querytabled _ _ %the (path a h) D %.