Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Termination.Termination

Description

Termination checker, based on "A Predicative Analysis of Structural Recursion" by Andreas Abel and Thorsten Altenkirch (JFP'01), and "The Size-Change Principle for Program Termination" by Chin Soon Lee, Neil Jones, and Amir Ben-Amram (POPL'01).

Synopsis

- data Terminates cinfo
  - = Terminates
  - | TerminatesNot GuardednessHelps cinfo
- data GuardednessHelps
  - = GuardednessHelpsYes
  - | GuardednessHelpsNot
- terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Terminates cinfo
- terminatesFilter :: (Monoid cinfo, ?cutoff :: CutOff) => (Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
- endos :: [Call cinfo] -> [CallMatrixAug cinfo]
- idempotent :: (?cutoff :: CutOff) => CallMatrixAug cinfo -> Bool

# Documentation

data Terminates cinfo Source #

Result of running the termination checker.

Constructors

Terminates | Termination proved without considering guardedness.
TerminatesNot GuardednessHelps cinfo | Termination could not be proven, witnessed by the supplied problematic call path. Guardedness could help, though.

data GuardednessHelps Source #

Would termination go through with guardedness?

Constructors

GuardednessHelpsYes | Guardedness would provide termination evidence.
GuardednessHelpsNot | Guardedness does not help with termination.

#### Instances

Instances details

Boolean GuardednessHelps Source # |

Instance details

Defined in Agda.Termination.Termination

Methods

fromBool :: Bool -> GuardednessHelps Source #

true :: GuardednessHelps Source #

false :: GuardednessHelps Source #

not :: GuardednessHelps -> GuardednessHelps Source #

(&&) :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #

(||) :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #

implies :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #

butNot :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #

IsBool GuardednessHelps Source # |
Instance details Defined in Agda.Termination.Termination Methods toBool :: GuardednessHelps -> Bool Source # ifThenElse :: GuardednessHelps -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> GuardednessHelps -> GuardednessHelps Source # fromBool2 :: (Bool -> Bool -> Bool) -> GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #
Null GuardednessHelps Source # |
Instance details Defined in Agda.Termination.Termination Methods empty :: GuardednessHelps Source # null :: GuardednessHelps -> Bool Source #
NFData GuardednessHelps Source # |
Instance details Defined in Agda.Termination.Termination Methods rnf :: GuardednessHelps -> () Source #
Bounded GuardednessHelps Source # |
Instance details Defined in Agda.Termination.Termination Methods minBound :: GuardednessHelps Source # maxBound :: GuardednessHelps Source #
Enum GuardednessHelps Source # |

Instance details

Defined in Agda.Termination.Termination

Methods

succ :: GuardednessHelps -> GuardednessHelps Source #

pred :: GuardednessHelps -> GuardednessHelps Source #

toEnum :: Int -> GuardednessHelps Source #

fromEnum :: GuardednessHelps -> Int Source #

enumFrom :: GuardednessHelps -> [GuardednessHelps] Source #

enumFromThen :: GuardednessHelps -> GuardednessHelps -> [GuardednessHelps] Source #

enumFromTo :: GuardednessHelps -> GuardednessHelps -> [GuardednessHelps] Source #

enumFromThenTo :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps -> [GuardednessHelps] Source #

Generic GuardednessHelps Source # |

Instance details

Defined in Agda.Termination.Termination

Associated Types

type Rep GuardednessHelps |
Instance details Defined in Agda.Termination.Termination type Rep GuardednessHelps = D1 ('MetaData "GuardednessHelps" "Agda.Termination.Termination" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "GuardednessHelpsYes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GuardednessHelpsNot" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: GuardednessHelps -> Rep GuardednessHelps x Source #

to :: Rep GuardednessHelps x -> GuardednessHelps Source #

Show GuardednessHelps Source # |
Instance details Defined in Agda.Termination.Termination Methods showsPrec :: Int -> GuardednessHelps -> ShowS Source # show :: GuardednessHelps -> String Source # showList :: [GuardednessHelps] -> ShowS Source #
Eq GuardednessHelps Source # |
Instance details Defined in Agda.Termination.Termination Methods (==) :: GuardednessHelps -> GuardednessHelps -> Bool Source # (/=) :: GuardednessHelps -> GuardednessHelps -> Bool Source #
type Rep GuardednessHelps Source # |
Instance details Defined in Agda.Termination.Termination type Rep GuardednessHelps = D1 ('MetaData "GuardednessHelps" "Agda.Termination.Termination" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "GuardednessHelpsYes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GuardednessHelpsNot" 'PrefixI 'False) (U1 :: Type -> Type))

terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Terminates cinfo Source #

``terminates` cs` checks if the functions represented by `cs` terminate. The call graph `cs` should have one entry (`Call`) per recursive function application.

The termination criterion is taken from Jones et al. In the completed call graph, each idempotent call-matrix from a function to itself must have a decreasing argument. Idempotency is wrt. matrix multiplication.

This criterion is strictly more liberal than searching for a lexicographic order (and easier to implement, but harder to justify).

terminatesFilter Source #

Arguments

:: (Monoid cinfo, ?cutoff :: CutOff) |
=> (Node -> Bool) | Only consider calls whose source and target satisfy this predicate.
-> CallGraph cinfo | Callgraph augmented with `cinfo`.
-> Terminates cinfo | A bad call path of type `cinfo`, if termination could not be proven.

endos :: [Call cinfo] -> [CallMatrixAug cinfo] Source #

idempotent :: (?cutoff :: CutOff) => CallMatrixAug cinfo -> Bool Source #

A call `c` is idempotent if it is an endo (``source` == `target``) of order 1. (Endo-calls of higher orders are e.g. argument permutations). We can test idempotency by self-composition. Self-composition `c >*< c` should not make any parameter-argument relation worse.