# Tabled logic programming

This is Literate Twelf Code: here Status: %% OK %% Output: here. |

The operational semantics of Twelf are similar to those of Prolog,
a style known as *backward chaining* or *goal-directed* proof
search. **Tabled logic programming**, which uses Twelf's
`%tabled` and `%querytabled` directives to
allow Twelf to prove theorems that might be time-consuming or
impossible to prove otherwise. The tabled logic programming
capabilities are a
part of Twelf'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.

## Contents

## Defining the graph

### Nodes

node : type. a : node. b : node. c : node. d : node. e : node. f : node. g : node. h : node.

### Edges

While we will consider edges in our graph to be undirected, we will only define the edge in one, arbitrary, direction.

edge : node -> node -> type. ab : edge a b. ac : edge a c. bc : edge b c. bd : edge b d. cd : edge c d. ce : edge c e. de : edge d e. df : edge d f. fg : edge f g.

### 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 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.

path : node -> node -> type. %tabled path. path/link : edge A B -> path A B. path/refl : path A B -> path B A. path/trans : path A B -> path B C -> path A C.

## 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 Twelf 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 * * D : path a g.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)%querytabled * * path a g. ---------- Solutions 1 ---------- Empty Substitution. path/refl path/trans path/refl path/link ab path/refl path/trans path/link fg path/refl path/trans path/link ab path/refl path/trans path/link df path/trans path/link bd path/link ab D = path/refl (path/trans (path/refl (path/trans (path/refl (path/trans (path/refl (path/trans (path/trans (path/link ab) (path/link bd)) (path/link df))) (path/link ab))) (path/link fg))) (path/refl (path/link ab))). More solutions? ====================== Stage 1 finished =================== ====================== Stage 2 finished =================== ====================== Stage 3 finished =================== ====================== Stage 4 finished =================== ____________________________________________ number of stages: tried * terminated after 4 stages Tabled evaluation COMPLETE ____________________________________________ Table Indexing parameters: Table Strategy := Variant Strengthening := false Number of table indices : 64 Number of suspended goals : 849 ____________________________________________

%% OK %%

We can also run a terminating search for a path that does not exist,
such as one from `a` to `h`.

%querytabled * * D : path a h.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)%querytabled * * path a h. ====================== Stage 1 finished =================== ====================== Stage 2 finished =================== ====================== Stage 3 finished =================== ====================== Stage 4 finished =================== ====================== Stage 5 finished =================== ____________________________________________ number of stages: tried * terminated after 5 stages NO solution exists to query Tabled evaluation COMPLETE ____________________________________________ Table Indexing parameters: Table Strategy := Variant Strengthening := false Number of table indices : 80 Number of suspended goals : 963 ____________________________________________

%% OK %%