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 -> () #

Bounded GuardednessHelps Source #

Instance details

Defined in Agda.Termination.Termination

Methods

minBound :: GuardednessHelps #

maxBound :: GuardednessHelps #

Enum GuardednessHelps Source #

Instance details

Defined in Agda.Termination.Termination

Methods

succ :: GuardednessHelps -> GuardednessHelps #

pred :: GuardednessHelps -> GuardednessHelps #

toEnum :: Int -> GuardednessHelps #

fromEnum :: GuardednessHelps -> Int #

enumFrom :: GuardednessHelps -> [GuardednessHelps] #

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

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

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

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.7.20250510-inplace" 'False) (C1 ('MetaCons "GuardednessHelpsYes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GuardednessHelpsNot" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: GuardednessHelps -> Rep GuardednessHelps x #

to :: Rep GuardednessHelps x -> GuardednessHelps #

Show GuardednessHelps Source #

Instance details

Defined in Agda.Termination.Termination

Methods

showsPrec :: Int -> GuardednessHelps -> ShowS #

show :: GuardednessHelps -> String #

showList :: [GuardednessHelps] -> ShowS #

Eq GuardednessHelps Source #

Instance details

Defined in Agda.Termination.Termination

Methods

(==) :: GuardednessHelps -> GuardednessHelps -> Bool #

(/=) :: GuardednessHelps -> GuardednessHelps -> Bool #

type Rep GuardednessHelps Source #

Instance details

Defined in Agda.Termination.Termination

type Rep GuardednessHelps = D1 ('MetaData "GuardednessHelps" "Agda.Termination.Termination" "Agda-2.7.20250510-inplace" '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.