> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module    : LTK.Decide.Finite
> Copyright : (c) 2021-2022 Dakotah Lambert
> License   : MIT

> This module implements an algorithm to decide whether a given FSA
> is finite.  Also included for convenience is a test for cofiniteness.
>
> @since 1.0
> -}
> 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)

> -- |True iff the automaton accepts only finitely many words.
> 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

> -- |True iff the automaton accepts all but finitely many words.
> 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

> -- |True iff the syntactic monoid is nilpotent
> -- and the sole idempotent is rejecting
> --
> -- @since 1.1
> 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

> -- |True iff the syntactic monoid is nilpotent
> -- and the sole idempotent is accepting
> --
> -- @since 1.1
> 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

> -- |True iff the automaton is finite on a tier.
> --
> -- @since 1.1
> 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

> -- |True iff the syntactic monoid is nilpotent without its identity,
> -- and the sole other idempotent is rejecting
> --
> -- @since 1.1
> 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

> -- |True iff the automaton is cofinite on a tier.
> --
> -- @since 1.1
> 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

> -- |True iff the syntactic monoid is nilpotent without its identity,
> -- and the sole other idempotent is accepting
> --
> -- @since 1.1
> 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