1
-- | Lexicographic order search, more or less as defined in
2
-- \"A Predicative Analysis of Structural Recursion\" by
3
-- Andreas Abel and Thorsten Altenkirch.
5
module Agda.Termination.Lexicographic
9
, recBehaviourInvariant
12
, Agda.Termination.Lexicographic.tests
15
import Agda.Utils.QuickCheck
16
import Agda.Termination.Matrix (Size (..))
17
import qualified Agda.Termination.Matrix as M
18
import Agda.Utils.Either
19
import Agda.Utils.List
20
import Agda.Utils.TestHelpers
21
import Agda.Termination.CallGraph
24
import Data.Map (Map, (!))
25
import qualified Data.Map as Map
26
import Data.Array (Array, Ix)
27
import qualified Data.Array as Array
29
import qualified Data.Set as Set
31
-- | A lexicographic ordering for the recursion behaviour of a
32
-- given function is a permutation of the argument indices which can
33
-- be used to show that the function terminates. See the paper
34
-- referred to above for more details.
36
type LexOrder arg = [arg]
38
-- | A recursion behaviour expresses how a certain function calls
39
-- itself (transitively). For every argument position there is a value
40
-- ('Column') describing how the function calls itself for that
41
-- particular argument. See also 'recBehaviourInvariant'.
43
data RecBehaviour arg call =
44
RB { columns :: Map arg (Column call)
46
-- ^ The indices to the columns.
47
, size :: Size Integer
51
-- | A column expresses how the size of a certain argument changes in
52
-- the various recursive calls a function makes to itself
55
type Column call = Map call Order
57
-- | 'RecBehaviour' invariant: the size must match the real size of
58
-- the recursion behaviour, and all columns must have the same
61
recBehaviourInvariant :: Eq call => RecBehaviour arg call -> Bool
62
recBehaviourInvariant rb =
63
genericLength (Map.elems $ columns rb) == cols (size rb)
65
all (== rows (size rb))
66
(map (genericLength . Map.elems) $ Map.elems $ columns rb)
68
allEqual (calls rb : (map Map.keysSet $ Map.elems $ columns rb))
70
-- Generates a recursion behaviour.
72
instance (Arbitrary call, Arbitrary arg, Ord arg, Ord call)
73
=> Arbitrary (RecBehaviour call arg) where
75
calls <- fmap nub $ listOf arbitrary
76
args <- fmap nub $ listOf arbitrary
77
let rows = genericLength calls
78
cols = genericLength args
79
sz = Size { rows = rows, cols = cols }
81
col <- vectorOf (fromIntegral rows) arbitrary
82
return $ Map.fromList (zip calls col)
83
cols <- fmap (zip args) $ vectorOf (fromIntegral cols) colGen
84
return $ RB { columns = Map.fromList cols
85
, calls = Set.fromList calls
88
instance (CoArbitrary call, CoArbitrary arg) => CoArbitrary (RecBehaviour call arg) where
89
coarbitrary (RB c cs s) =
90
coarbitrary (map (id *** Map.toList) $ Map.toList c) .
91
coarbitrary (Set.toList cs) .
94
prop_recBehaviour_Arbitrary :: RecBehaviour Integer Integer -> Bool
95
prop_recBehaviour_Arbitrary = recBehaviourInvariant
97
-- | Checks whether there are any calls left in the recursion
100
noCallsLeft :: RecBehaviour arg call -> Bool
101
noCallsLeft rb = rows (size rb) == 0
103
-- | Constructs a recursion behaviour from a list of matrix diagonals
104
-- (\"rows\"). Note that the @call@ indices do not need to be
105
-- distinct, since they are paired up with unique 'Integer's.
107
-- Precondition: all arrays should have the same bounds.
109
fromDiagonals :: (Ord call, Ix arg)
110
=> [(call, Array arg Order)] -> RecBehaviour arg (Integer, call)
111
fromDiagonals [] = RB { columns = Map.fromList []
114
fromDiagonals rows = RB { columns = Map.fromList $ zip args cols
115
, calls = Set.fromList calls
116
, size = Size { rows = genericLength rows
117
, cols = genericLength cols }
120
calls = zip [1 ..] $ map fst rows
121
cols = map Map.fromList $ map (zip calls) $ transpose $
122
map (Array.elems . snd) rows
123
args = Array.range $ Array.bounds $ snd $ head rows
125
prop_fromDiagonals m =
126
forAll (vectorOf (fromIntegral $ rows $ M.size m) arbitrary) $ \calls ->
127
let oss = zip calls $
128
map (Array.listArray (1, cols $ M.size m)) $
130
rb = fromDiagonals oss :: RecBehaviour Integer (Integer, Bool)
132
recBehaviourInvariant rb
134
if rows (M.size m) == 0 then
139
-- | Checks if this \"column\" is well-behaved (all calls decreasing,
140
-- at least one strictly decreasing).
142
okColumn :: Column call -> Bool
143
okColumn col = any (== Lt) col' && all (/= Unknown) col'
144
where col' = Map.elems col
146
-- | @'newBehaviour' n rb@ computes a new recursion behaviour from
147
-- @rb@ by removing all \"rows\" (calls) for which the @n@-th element
148
-- is 'Lt', and also completely removing the @n@-th column.
150
-- Precondition: there has to be an @n@-th column.
152
newBehaviour :: (Ord arg, Ord call)
153
=> arg -> RecBehaviour arg call -> RecBehaviour arg call
155
RB { columns = Map.map remove $ Map.delete n $ columns rb
156
, calls = Set.difference (calls rb)
157
(Set.fromList indicesToRemove)
158
, size = Size { rows = rows (size rb) -
159
genericLength indicesToRemove
160
, cols = cols (size rb) - 1 }
163
Just colN = Map.lookup n $ columns rb
164
indicesToRemove = map fst $ filter ((== Lt) . snd) $ Map.toList colN
165
remove colJ = foldr Map.delete colJ indicesToRemove
167
prop_newBehaviour :: RecBehaviour Integer Integer -> Property
168
prop_newBehaviour rb =
169
not (cols (size rb) == 0) ==>
170
forAll (elements $ Map.keys $ columns rb) $ \n ->
171
recBehaviourInvariant (newBehaviour n rb)
173
-- | @'correctLexOrder' rs ps@ checks that the permutation @ps@ really
174
-- induces a lexicographic ordering which shows that the function
175
-- represented by the recursion behaviour @rs@ terminates.
177
correctLexOrder :: (Ord arg, Ord call)
178
=> RecBehaviour arg call -> LexOrder arg -> Bool
179
correctLexOrder rb [] = noCallsLeft rb
180
correctLexOrder rb (p0 : ps) =
181
okColumn (columns rb ! p0) && correctLexOrder (newBehaviour p0 rb) ps
183
-- | Tries to compute a lexicographic ordering for the given recursion
184
-- behaviour. This algorithm should be complete.
186
-- If no lexicographic ordering can be found, then two sets are
189
-- * A set of argument positions which are not properly decreasing, and
191
-- * the calls where these problems show up.
193
lexOrder :: (Ord arg, Ord call) =>
194
RecBehaviour arg call -> Either (Set arg, Set call) (LexOrder arg)
195
lexOrder rb | noCallsLeft rb = Right []
196
| otherwise = case okColumns of
197
[] -> Left (Map.keysSet $ columns rb, calls rb)
198
(n : _) -> case lexOrder (newBehaviour n rb) of
200
Right ps -> Right $ n : ps
202
okColumns = map fst $ filter snd $
203
map (id *** okColumn) $
204
Map.toList $ columns rb
206
prop_lexOrder :: RecBehaviour Integer Integer -> Property
208
let mPerm = lexOrder rb
212
classify (cols (size rb) >= 2) "interesting" $
213
correctLexOrder rb perm
215
prop_lexOrder_noArgs =
216
forAll positive $ \n ->
217
isLeft (lexOrder $ rb n)
218
where rb :: Integer -> RecBehaviour Integer Integer
219
rb n = RB { columns = Map.empty
220
, calls = Set.fromList [1 .. n]
221
, size = Size { rows = n, cols = 0 }
224
------------------------------------------------------------------------
228
tests = runTests "Agda.Termination.Lexicographic"
229
[ quickCheck' prop_recBehaviour_Arbitrary
230
, quickCheck' prop_fromDiagonals
231
, quickCheck' prop_newBehaviour
232
, quickCheckWith' Args{ replay = Nothing
238
, quickCheck' prop_lexOrder_noArgs
added
removed
src/full/Agda/Termination/Lexicographic.hs
