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

Summary of exported operations:

terminationAnalysis :: Analysis Bool  Deterministic 
showTermination :: AOutFormat -> Bool -> String  Deterministic 
productivityAnalysis :: Analysis Productivity  Non-deterministic 
showProductivity :: AOutFormat -> Productivity -> String  Deterministic 

Exported datatypes:

Productivity

Data type to represent productivity status of an operation.

Constructors:

  • NoInfo :: Productivity
  • Terminating :: Productivity
  • DCalls :: [QName] -> Productivity
  • Looping :: Productivity

Exported operations:

showTermination :: AOutFormat -> Bool -> String  Deterministic 

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

showProductivity :: AOutFormat -> Productivity -> String  Deterministic