Skip to content
STELF
Documentation out of dateLearn more

%total

In STELF, a totality assertion for an LF type family is specified by a %mode declaration and a %worlds declarations. A %total declaration for a type family causes STELF to attempt to verify the specified totality assertion. STELF does so by attempting to prove that the type family defines a total logic program. The %total declaration is used both to verify properties of object-language judgments and to check proofs of general metatheorems.

A %total declaration requires that %mode checking and %worlds checking have already succeeded.
Then a %total declaration causes STELF to run a number of analyses:

  • Termination analysis - The syntax of a %total declaration is the same as a %terminates declaration, and STELF runs its termination analysis with that information. This verifies that the logic program always terminates when given ground inputs.
  • Input coverage checking - STELF uses the modes specified by the %mode declaration (%mode and %covers declarations also have the same syntax) to check input coverage. This verifies that the logic program will match all possible ground inputs in the specified set of contexts.
  • Output coverage checking - STELF checks that the output of a subgoal can never fail to unify. First, it checks for incorrect constant pattern-matching; next, it checks for output freeness violations.

Taken together, these analyses verify that if the type family is run as a logic program in STELF with ground derivations in the input positions, then it the execution will terminate successfully and will derive ground derivations in the output positions. This proves the totality assertion for the type family: in any context conforming to the %worlds declaration, for any ground derivations in the input positions (as specified by the %mode declaration), there exist ground derivations for the output positions such that the type family is inhabited.

See also

Section titled “See also”