Safe Haskell | None |
---|---|
Language | Haskell2010 |
Guardednes checks
- gc1 :: (Eq a, Eq c) => Program a b c -> Bool
- gc2 :: (Eq a, Eq b, Eq c, Ord c, Freshable c) => Program a b c -> Clause a b c -> Bool
- gc3 :: (Freshable c, Ord c, Eq a, Eq b) => Program a b c -> Bool
- gc3one :: (Freshable c, Ord c, Eq a, Eq b) => Program a b c -> Clause a b c -> Bool
- guardingContext :: (Eq a, Eq b, Ord c) => Program a b c -> RewTree a b c d -> Maybe (Int, Subst a b c, Term a b c) -> GuardingContext a b c
- gcRewTree :: (Eq a, Eq b, Eq c) => RewTree a b c Integer -> Bool
- derToObs :: DerTree1 -> OTree1
- derToUnc :: Int -> DerTree1 -> DerTree1
- derToUng :: Int -> DerTree1 -> DerTree1
Guardedness checks
gc1 :: (Eq a, Eq c) => Program a b c -> Bool
Guardendes check GC1 on clauses
Given program P check that all program clauses are guarded, i. e.
whenever C(ε)
and C(i)
have same predicate check that C(i)
is a reduct of C(ε)
gc2 :: (Eq a, Eq b, Eq c, Ord c, Freshable c) => Program a b c -> Clause a b c -> Bool
Guardedness check GC2
Given program P and a clause C check guardednees of the rewriting tree
rew (P, C, id)
gc3 :: (Freshable c, Ord c, Eq a, Eq b) => Program a b c -> Bool
Guradedness check GC3 according to Defintion 5.6
for the whole program
gc3one :: (Freshable c, Ord c, Eq a, Eq b) => Program a b c -> Clause a b c -> Bool
Guradedness check GC3 according to Defintion 5.6
for a single clause
Guarding context
guardingContext :: (Eq a, Eq b, Ord c) => Program a b c -> RewTree a b c d -> Maybe (Int, Subst a b c, Term a b c) -> GuardingContext a b c
Given a program P, rewriting tree D(wi) = rew(P, C, σ)
and the external
resolvent σ' with its contraction measure compute guarding context
gc(D(wi)) = {(P(k), t', v) ∈ π(wi) | ... }
GC on a rewriting tree
gcRewTree :: (Eq a, Eq b, Eq c) => RewTree a b c Integer -> Bool
Check GC2 guardedness of a rewritng tree
Derivation tree transformations
derToObs :: DerTree1 -> OTree1
Construct observation tree from a derivation tree
according to the Definition 5.5