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)
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)
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)
term_size(Var) = 0 term_size(Const) = 1 term_size(F(T1,...,Tn)) = 1 + term_size(T1) + ... + term_size(Tn).
size_bound(
+Term,
+Bound)
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)