Agda
Safe HaskellNone
LanguageHaskell2010

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

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.9.0-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.9.0-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).

terminates does not use guardedness, terminatesFilter is more general.

terminatesFilter Source #

Arguments

:: (Monoid cinfo, ?cutoff :: CutOff) 
=> Bool

Use guardedness?

-> (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.

While no counterexample to termination is found, complete the given call graph step-by-step.

terminationCounterexample Source #

Arguments

:: (Monoid cinfo, ?cutoff :: CutOff) 
=> Bool

Use guardedness?

-> (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.

Does the given callgraph contain a counterexample to termination?

idempotentEndos :: (?cutoff :: CutOff) => CallGraph cinfo -> [CallMatrixAug cinfo] Source #

Get all idempotent call-matrixes of loops in the call graph.