Ground

From The Twelf Project
Jump to: navigation, search

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

%mode plus +M +N -O.
%solve D1 : plus (s z) (s (s z)) X.
%solve D2 : plus (s z) (s Y) (s (s z)).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%mode +{M:nat} +{N:nat} -{O:nat} (plus M N O). %solve plus (s z) (s (s z)) X. OK D1 : plus (s z) (s (s z)) (s (s (s z))) = plus-s plus-z. %solve plus (s z) (s Y) (s (s z)). OK D2 : plus (s z) (s z) (s (s z)) = plus-s plus-z.

%% OK %%

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.