Module Analysis.Termination
Termination analysis: checks whether an operation is terminating, i.e., whether all evaluations on ground argument terms are finite. The method used here checks whether the arguments in all recursive calls of an operation are smaller than the arguments passed to the operation.
Exported Datatypes
data Productivity
Data type to represent productivity status of an operation.
Constructors:
-
NoInfo :: Productivity -
Terminating :: Productivity -
DCalls :: [QName] -> Productivity -
Looping :: Productivity
Known instances:
Exported Functions
terminationAnalysis
:: Analysis Bool 
The termination analysis is a global function dependency analysis. It assigns to a FlatCurry function definition a flag which is True if this operation is terminating, i.e., whether all evaluations
showTermination
:: AOutFormat -> Bool -> String
Show termination information as a string.
- Further infos:
-
- solution complete, i.e., able to compute all solutions
productivityAnalysis
:: Analysis Productivity 
The productivity analysis is a global function dependency analysis which depends on the termination analysis. An operation is considered as being productive if it cannot perform an infinite number of steps without producing outermost constructors. It assigns to a FlatCurry function definition an abstract value indicating whether the function is looping or productive.
showProductivity
:: AOutFormat -> Productivity -> String
Show productivity information as a string.