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.
- 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.
- Read the introductions to Twelf to learn more about %total. The following sections of Proving metatheorems with Twelf are particularly relevant: Proving totality assertions about the natural numbers, Proving metatheorems about the natural numbers, Proving totality assertions in non-empty contexts.
- Totality in the User's Guide
This page is incomplete. We should expand it.