- Sequent:
A
sequent
represents a theorem by a sequence of hypotheses and the sequence of possible theses they imply. This formalism underlines a symmetry hypotheses/theses ruled by negation and is used in
sequent calculus
to formalise proofs and to study their properties.
- Unproductive:
A part of a program is
unproductive
if it performs an infinite number of computing steps without any interaction with the rest of the program or external devices.
Unproductive
code is basically useless, and may even be unsafe, and detecting parts of code that are unproductive is important to improve software quality.