> {-# OPTIONS_HADDOCK show-extensions #-}
>
> module LTK.Decide.Finite ( isFinite, isFiniteM
> , isCofinite, isCofiniteM
> , isTFinite, isTFiniteM
> , isTCofinite, isTCofiniteM
> ) where
> import LTK.FSA
> import LTK.Algebra
> import LTK.Tiers (project)
> import LTK.Decide.PT (isPTM)
>
> isFinite :: (Ord n, Ord e) => FSA n e -> Bool
> isFinite :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFinite = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFiniteM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid
>
> isCofinite :: (Ord n, Ord e) => FSA n e -> Bool
> isCofinite :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isCofinite = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid
>
>
>
>
> isFiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFiniteM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFiniteM SynMon n e
s = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isPTM SynMon n e
s Bool -> Bool -> Bool
&& (forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State ([Maybe n], [Symbol e]))
i forall a. Eq a => a -> a -> Bool
== Integer
1) Bool -> Bool -> Bool
&& Bool -> Bool
not (forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (forall n e. FSA n e -> Set (State n)
finals SynMon n e
s) Set (State ([Maybe n], [Symbol e]))
i)
> where i :: Set (State ([Maybe n], [Symbol e]))
i = forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents SynMon n e
s
>
>
>
>
> isCofiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
> isCofiniteM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM SynMon n e
s = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isPTM SynMon n e
s Bool -> Bool -> Bool
&& (forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State ([Maybe n], [Symbol e]))
i forall a. Eq a => a -> a -> Bool
== Integer
1) Bool -> Bool -> Bool
&& forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (forall n e. FSA n e -> Set (State n)
finals SynMon n e
s) Set (State ([Maybe n], [Symbol e]))
i
> where i :: Set (State ([Maybe n], [Symbol e]))
i = forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents SynMon n e
s
>
>
>
> isTFinite :: (Ord n, Ord e) => FSA n e -> Bool
> isTFinite :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isTFinite = forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFinite forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project
>
>
>
>
> isTFiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
> isTFiniteM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isTFiniteM = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFiniteM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project
>
>
>
> isTCofinite :: (Ord n, Ord e) => FSA n e -> Bool
> isTCofinite :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isTCofinite = forall n e. (Ord n, Ord e) => FSA n e -> Bool
isCofinite forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project
>
>
>
>
> isTCofiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
> isTCofiniteM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isTCofiniteM = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project