> {-# 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 = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFiniteM (SynMon n e -> Bool) -> (FSA n e -> SynMon n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> SynMon n e
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 = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM (SynMon n e -> Bool) -> (FSA n e -> SynMon n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> SynMon n e
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 = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isPTM SynMon n e
s Bool -> Bool -> Bool
&& (Set (State ([Maybe n], [Symbol e])) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State ([Maybe n], [Symbol e]))
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) Bool -> Bool -> Bool
&& Bool -> Bool
not (Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e])) -> Bool
forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (SynMon n e -> Set (State ([Maybe n], [Symbol e]))
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 = SynMon n e -> Set (State ([Maybe n], [Symbol e]))
forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e -> Set (State (n, [Symbol 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 = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isPTM SynMon n e
s Bool -> Bool -> Bool
&& (Set (State ([Maybe n], [Symbol e])) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State ([Maybe n], [Symbol e]))
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) Bool -> Bool -> Bool
&& Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e])) -> Bool
forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (SynMon n e -> Set (State ([Maybe n], [Symbol e]))
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 = SynMon n e -> Set (State ([Maybe n], [Symbol e]))
forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e -> Set (State (n, [Symbol 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 = FSA n e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFinite (FSA n e -> Bool) -> (FSA n e -> FSA n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA n e
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 = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFiniteM (SynMon n e -> Bool)
-> (SynMon n e -> SynMon n e) -> SynMon n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynMon n e -> SynMon n e
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 = FSA n e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isCofinite (FSA n e -> Bool) -> (FSA n e -> FSA n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA n e
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 = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM (SynMon n e -> Bool)
-> (SynMon n e -> SynMon n e) -> SynMon n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynMon n e -> SynMon n e
forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project