Ground

A term is ground if it does not contain any existential (unification) variables. For example, we can make the following queries on plus:

(options removed from twelftag: hidden=“true”)

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term plus-z plus z N N %.
%term plus-s %pi (plus (s N1) N2 (s N3)) %<- (plus N1 N2 N3) %.

(options removed from twelftag: discard=“true” check=“decl”)

%mode plus %in %in %out %.
%solve D1 : plus (s z) (s (s z)) X %.
%solve D2 : plus (s z) (s Y) (s (s z)) %.

In the query for D1, the first two arguments to plus are ground. The third is not; it is an existential variable. This is the typical situation: that the input arguments are ground and the output is an unconstrained existential variable. A %total declaration for plus guarantees that such queries will always succeed. However, we can still issue queries like the second, where the middle argument is not ground. In this case, the query does succeed, but the totality declaration does not guarantee that it will.