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.

Author
Michael Hanus
Version
November 2024
Exported Datatypes:
Productivity
Exported Functions:
productivityAnalysisshowProductivityshowTerminationterminationAnalysis

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  Deterministic 

showTermination :: AOutFormat -> Bool -> String  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

productivityAnalysis :: Analysis Productivity  Non-deterministic 

showProductivity :: AOutFormat -> Productivity -> String  Deterministic