library(termdepth)

Many resolution-based theorem provers impose a depth bound on the terms they create. Not the least of the reasons for this is to prevent infinite loops. library(termdepth) provides five predicates:

term_depth(+Term, -Depth)

Depth is unified with the depth of Term, calculated according to the following definition:

          term_depth(Var) = 0
          term_depth(Const) = 0
          term_depth(F(T1,...,Tn)) =
              1 + max(term_depth(T1), ..., term_depth(Tn))
          

depth_bound(+Term, +Bound)

This succeeds when the depth of Term, as calculated by term_depth/2, is less than or equal to Bound. Bound is assumed to be a strictly positive integer. Note that depth_bound/2 will terminate even if Term is cyclic.

term_size(+Term, -Size)

Unify Size with the size of Term, where the size is the number of constants and function symbols in the term. (Note that this is a lower bound on the size of any term instantiated from Term, and that instantiating any variable to a non-variable must increase the size. This latter property is why variables are counted as 0 rather than as 1.) The definition is

          term_size(Var) = 0
          term_size(Const) = 1
          term_size(F(T1,...,Tn)) =
              1 + term_size(T1) + ... + term_size(Tn).
          

size_bound(+Term, +Bound)

This succeeds when the size of Term, as calculated by term_size/2, is less than or equal to Bound. Bound is assumed to be a non-negative integer. Note that size_bound/2 will always terminate even if Term is cyclic.

length_bound(+List, +Bound)

is true when List is a list having at most Bound elements. Bound must be instantiated. If List ends with a variable, it will be instantiated to successively longer proper lists, up to the length permitted by Bound. Note that the depth of a list of constants is its length.