From The Twelf Project
Jump to: navigation, search

In Twelf, 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 Twelf to attempt to verify the specified totality assertion. Twelf 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 Twelf to run a number of analyses:

  • Termination analysis - The syntax of a %total declaration is the same as a %terminates declaration, and Twelf runs its termination analysis with that information. This verifies that the logic program always terminates when given ground inputs.
  • Input coverage checking - Twelf 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 - Twelf 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 Twelf 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

This page is incomplete. We should expand it.