CoALP-0.0.6: Coalgebraic logic programming library

Safe HaskellNone
LanguageHaskell2010

CoALP.Guards

Contents

Description

Guardednes checks

Synopsis

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

derToUnc :: Int -> DerTree1 -> DerTree1

Select leftmost branch of a derivation tree that is not closed up to given depth

derToUng :: Int -> DerTree1 -> DerTree1

Select leftmost branch containing an unguarded rewriting tree in the given or less depth