From c2b2907555755dc0075d192b069fb895a0d64d68 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 22 Feb 2021 13:28:42 +0100 Subject: [PATCH] Adds a class for tables --- nominal-lstar.cabal | 3 +- src/Bollig.hs | 34 ++++----- src/ObservationTableClass.hs | 43 +++++++++++ src/SimpleObservationTable.hs | 138 ++++++++++++++++++++-------------- 4 files changed, 142 insertions(+), 76 deletions(-) create mode 100644 src/ObservationTableClass.hs diff --git a/nominal-lstar.cabal b/nominal-lstar.cabal index 653d9aa..777da0e 100644 --- a/nominal-lstar.cabal +++ b/nominal-lstar.cabal @@ -11,9 +11,7 @@ common stuff ghc-options: -O2 -Wall build-depends: base >= 4.8 && < 5, - containers, haskeline, - mtl, NLambda >= 1.1 library @@ -32,6 +30,7 @@ library Examples.RunningExample, Examples.Stack, ObservationTable, + ObservationTableClass, SimpleObservationTable, Teacher, Teachers.Teacher, diff --git a/src/Bollig.hs b/src/Bollig.hs index 1749a7c..53b4ef0 100644 --- a/src/Bollig.hs +++ b/src/Bollig.hs @@ -1,9 +1,9 @@ {-# language PartialTypeSignatures #-} -{-# language RecordWildCards #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} module Bollig where import AbstractLStar +import ObservationTableClass import SimpleObservationTable import Teacher @@ -31,55 +31,53 @@ mqToBool teacher words = answer answer = map (setB True) inw `union` map (setB False) outw setB b (w, _) = (w, b) -tableAt :: NominalType i => BTable i -> [i] -> [i] -> Formula -tableAt t s e = singleton True `eq` mapFilter (\(i, o) -> maybeIf ((s ++ e) `eq` i) o) (content t) - rfsaClosednessTest :: NominalType i => Set (BRow i) -> BTable i -> TestResult i -rfsaClosednessTest primesUpp t@Table{..} = case solve (isEmpty defect) of +rfsaClosednessTest primesUpp t = case solve (isEmpty defect) of Just True -> Succes Just False -> trace "Not closed" $ Failed defect empty Nothing -> trace "@@@ Unsolved Formula (rfsaClosednessTest) @@@" $ Failed defect empty where - defect = filter (\ua -> brow t ua `neq` sum (filter (`isSubsetOf` brow t ua) primesUpp)) (rowsExt t) + defect = filter (\ua -> row t ua `neq` sum (filter (`isSubsetOf` row t ua) primesUpp)) (rowsExt t) rfsaConsistencyTest :: NominalType i => BTable i -> TestResult i -rfsaConsistencyTest t@Table{..} = case solve (isEmpty defect) of +rfsaConsistencyTest t = case solve (isEmpty defect) of Just True -> Succes Just False -> trace "Not consistent" $ Failed empty defect Nothing -> trace "@@@ Unsolved Formula (rfsaConsistencyTest) @@@" $ Failed empty defect where - candidates = pairsWithFilter (\u1 u2 -> maybeIf (brow t u2 `isSubsetOf` brow t u1) (u1, u2)) rows rows - defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (not (tableAt t (u1 ++ [a]) v) /\ tableAt t (u2 ++ [a]) v) (a:v)) candidates alph columns + candidates = pairsWithFilter (\u1 u2 -> maybeIf (row t u2 `isSubsetOf` row t u1) (u1, u2)) (rows t) (rows t) + defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (not (tableAt2 (u1 ++ [a]) v) /\ tableAt2 (u2 ++ [a]) v) (a:v)) candidates (alph t) (cols t) + tableAt2 s e = singleton True `eq` tableAt t s e constructHypothesisBollig :: NominalType i => Set (BRow i) -> BTable i -> Automaton (BRow i) i -constructHypothesisBollig primesUpp t@Table{..} = automaton q alph d i f +constructHypothesisBollig primesUpp t = automaton q (alph t) d i f where q = primesUpp - i = filter (`isSubsetOf` brow t []) q + i = filter (`isSubsetOf` rowEps t) q f = filter (`contains` []) q -- TODO: compute indices of primesUpp only once - d0 = triplesWithFilter (\s a bs2 -> maybeIf (bs2 `isSubsetOf` brow t (s ++ [a])) (brow t s, a, bs2)) rows alph q + d0 = triplesWithFilter (\s a bs2 -> maybeIf (bs2 `isSubsetOf` row t (s ++ [a])) (row t s, a, bs2)) (rows t) (alph t) q d = filter (\(q1, _, _) -> q1 `member` q) d0 -- Adds all suffixes as columns -- TODO: do actual Rivest and Schapire addCounterExample :: NominalType i => MQ i Bool -> Set [i] -> BTable i -> BTable i -addCounterExample mq ces t@Table{..} = +addCounterExample mq ces t = let newColumns = sum . map (fromList . tails) $ ces - newColumnsRed = newColumns \\ columns + newColumnsRed = newColumns \\ cols t in addColumns mq newColumnsRed t learnBollig :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton (BRow i) i -learnBollig k n teacher = learnBolligLoop teacher (initialTableSize (mqToBool teacher) (alphabet teacher) k n) +learnBollig k n teacher = learnBolligLoop teacher (initialBTableSize (mqToBool teacher) (alphabet teacher) k n) learnBolligLoop :: (NominalType i, _) => Teacher i -> BTable i -> Automaton (BRow i) i -learnBolligLoop teacher t@Table{..} = +learnBolligLoop teacher t = let -- These simplify's do speed up - allRowsUpp = simplify $ map (brow t) rows - allRows = simplify $ allRowsUpp `union` map (brow t) (rowsExt t) + allRowsUpp = simplify $ map (row t) (rows t) + allRows = simplify $ allRowsUpp `union` map (row t) (rowsExt t) primesUpp = simplify $ filter (\r -> isNotEmpty r /\ r `neq` sum (filter (`isSubsetOf` r) (allRows \\ orbit [] r))) allRowsUpp -- No worry, these are computed lazily diff --git a/src/ObservationTableClass.hs b/src/ObservationTableClass.hs new file mode 100644 index 0000000..0b0b351 --- /dev/null +++ b/src/ObservationTableClass.hs @@ -0,0 +1,43 @@ +{-# language TypeFamilies #-} +{-# language FunctionalDependencies #-} + +module ObservationTableClass where + +import NLambda +import Prelude ((++)) + +-- Words are indices to our table +type RowIndex i = [i] +type ColumnIndex i = [i] + +-- Membership queries (TODO: move to Teacher) +type MQ i o = Set [i] -> Set ([i], o) + +-- This is a fat class, so that instances could give more efficient implementations +class (NominalType table, NominalType i, NominalType o) => ObservationTable table i o | table -> i o where + -- The type of data in a row is determined by the table + type Row table :: * + + -- getters + rows :: table -> Set (RowIndex i) + cols :: table -> Set (ColumnIndex i) + alph :: table -> Set i + row :: table -> RowIndex i -> Row table + + -- perhaps not needed + tableAt :: table -> RowIndex i -> ColumnIndex i -> Set o + + -- compound getters + rowsExt :: table -> Set (RowIndex i) + colsExt :: table -> Set (ColumnIndex i) + + rowEps :: table -> Row table + + -- updaters + addRows :: MQ i o -> Set (RowIndex i) -> table -> table + addColumns :: MQ i o -> Set (ColumnIndex i) -> table -> table + + -- default implementations + rowsExt t = pairsWith (\r a -> r ++ [a]) (rows t) (alph t) + colsExt t = pairsWith (:) (alph t) (cols t) + rowEps t = row t [] diff --git a/src/SimpleObservationTable.hs b/src/SimpleObservationTable.hs index 7b60628..7bf5d70 100644 --- a/src/SimpleObservationTable.hs +++ b/src/SimpleObservationTable.hs @@ -1,14 +1,22 @@ {-# language DeriveAnyClass #-} {-# language DeriveGeneric #-} {-# language RecordWildCards #-} +{-# language FlexibleInstances #-} +{-# language MultiParamTypeClasses #-} +{-# language TypeFamilies #-} +{-# language PartialTypeSignatures #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} module SimpleObservationTable where +import ObservationTableClass + import NLambda hiding (fromJust) import GHC.Generics (Generic) -import Prelude (Bool (..), Eq, Int, Ord, Show (..), fst, (++)) +import Prelude (Bool (..), Eq, Int, Ord, Show (..), fst, (++), (.)) import qualified Prelude () +import Data.Coerce (coerce) -- We represent functions as their graphs @@ -18,55 +26,88 @@ type Fun i o = Set (i, o) dom :: (NominalType i, NominalType o) => Fun i o -> Set i dom = map fst --- Words are indices to our table -type RowIndex i = [i] -type ColumnIndex i = [i] - -- A table is nothing more than a part of the language. -- Invariant: content is always defined for elements in -- `rows * columns` and `rows * alph * columns`. data Table i o = Table { content :: Fun [i] o - , rows :: Set (RowIndex i) - , columns :: Set (ColumnIndex i) - , alph :: Set i + , rowIndices :: Set (RowIndex i) + , colIndices :: Set (ColumnIndex i) + , aa :: Set i } deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual) -rowsExt :: (NominalType i, NominalType o) => Table i o -> Set (RowIndex i) -rowsExt Table{..} = pairsWith (\r a -> r ++ [a]) rows alph +instance (NominalType i, NominalType o) => ObservationTable (Table i o) i o where + type Row (Table i o) = Fun [i] o + rows = rowIndices + cols = colIndices + alph = aa + row Table{..} r = pairsWithFilter (\e (a, b) -> maybeIf (a `eq` (r ++ e)) (e, b)) colIndices content + tableAt Table{..} r c = mapFilter (\(i, o) -> maybeIf ((r ++ c) `eq` i) o) content -columnsExt :: (NominalType i, NominalType o) => Table i o -> Set (RowIndex i) -columnsExt Table{..} = pairsWith (:) alph columns + -- Assumption: newRows is disjoint from rows (for efficiency) + addRows mq newRows t@Table{..} = + t { content = content `union` newContent + , rowIndices = rowIndices `union` newRows + } + where + newRowsExt = pairsWith (\r a -> r ++ [a]) newRows aa + newPart = pairsWith (++) (newRows `union` newRowsExt) colIndices + newPartRed = newPart \\ dom content + newContent = mq newPartRed --- I could make a more specific implementation for booleans --- But for now we reuse the above. -type BTable i = Table i Bool - --- A row is the data in a table, i.e. a function from columns to the output -type Row i o = Fun [i] o - -row :: (NominalType i, NominalType o) => Table i o -> RowIndex i -> Row i o -row Table{..} r = pairsWithFilter (\e (a, b) -> maybeIf (a `eq` (r ++ e)) (e, b)) columns content - --- Special case of a boolean: functions to Booleans are subsets -type BRow i = Set [i] - --- TODO: slightly inefficient -brow :: NominalType i => BTable i -> RowIndex i -> BRow i -brow Table{..} r = let lang = mapFilter (\(i, o) -> maybeIf (fromBool o) i) content - in filter (\a -> lang `contains` (r ++ a)) columns + -- Assumption: newColumns is disjoint from columns (for efficiency) + addColumns mq newColumns t@Table{..} = + t { content = content `union` newContent + , colIndices = colIndices `union` newColumns + } + where + newColumnsExt = pairsWith (:) aa newColumns + newPart = pairsWith (++) rowIndices (newColumns `union` newColumnsExt) + newPartRed = newPart \\ dom content + newContent = mq newPartRed --- Membership queries (TODO: move to Teacher) -type MQ i o = Set [i] -> Set ([i], o) +-- I could make a more specific implementation for booleans. +-- But for now we reuse the above, and do minor optimisations + +newtype Boolean table = B { unB :: table } + deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual) + +type BTable i = Boolean (Table i Bool) + +instance (NominalType i) => ObservationTable (BTable i) i Bool where + -- Special case of a boolean: functions to Booleans are subsets + type Row (BTable i) = Set [i] + rows = coerce (rows :: _ => Table i Bool -> _) + cols = coerce (cols :: _ => Table i Bool -> _) + rowsExt = coerce (rowsExt :: _ => Table i Bool -> _) + colsExt = coerce (colsExt :: _ => Table i Bool -> _) + alph = coerce (alph :: _ => Table i Bool -> _) + tableAt = coerce (tableAt :: _ => Table i Bool -> _) + --rows = rowIndices . unB + --cols = colIndices . unB + --alph = aa . unB + --tableAt = tableAt . unB + + -- TODO: slightly inefficient + row (B Table{..}) r = let lang = mapFilter (\(i, o) -> maybeIf (fromBool o) i) content + in filter (\a -> lang `contains` (r ++ a)) colIndices + rowEps (B Table{..}) = mapFilter (\(i, o) -> maybeIf (fromBool o /\ i `member` colIndices) i) content + + --addRows mq newRows = B . addRows mq newRows . unB + addRows = coerce (addRows :: _ => _ -> _ -> Table i Bool -> Table i Bool) + --addColumns mq newColumns = B . addColumns mq newColumns . unB + addColumns = coerce (addColumns :: _ => _ -> _ -> Table i Bool -> Table i Bool) + +type BRow i = Row (BTable i) initialTableWith :: (NominalType i, NominalType o) => MQ i o -> Set i -> Set (RowIndex i) -> Set (ColumnIndex i) -> Table i o initialTableWith mq alphabet newRows newColumns = Table { content = content - , rows = newRows - , columns = newColumns - , alph = alphabet + , rowIndices = newRows + , colIndices = newColumns + , aa = alphabet } where newColumnsExt = pairsWith (:) alphabet newColumns @@ -79,26 +120,11 @@ initialTable mq alphabet = initialTableWith mq alphabet (singleton []) (singleto initialTableSize :: (NominalType i, NominalType o) => MQ i o -> Set i -> Int -> Int -> Table i o initialTableSize mq alphabet rs cs = initialTableWith mq alphabet (replicateSetUntil rs alphabet) (replicateSetUntil cs alphabet) --- Assumption: newRows is disjoint from rows (for efficiency) -addRows :: (NominalType i, NominalType o) => MQ i o -> Set (RowIndex i) -> Table i o -> Table i o -addRows mq newRows t@Table{..} = - t { content = content `union` newContent - , rows = rows `union` newRows - } - where - newRowsExt = pairsWith (\r a -> r ++ [a]) newRows alph - newPart = pairsWith (++) (newRows `union` newRowsExt) columns - newPartRed = newPart \\ dom content - newContent = mq newPartRed +initialBTableWith :: NominalType i => MQ i Bool -> Set i -> Set (RowIndex i) -> Set (ColumnIndex i) -> BTable i +initialBTableWith = coerce initialTableWith --- Assumption: newColumns is disjoint from columns (for efficiency) -addColumns :: (NominalType i, NominalType o) => MQ i o -> Set (ColumnIndex i) -> Table i o -> Table i o -addColumns mq newColumns t@Table{..} = - t { content = content `union` newContent - , columns = columns `union` newColumns - } - where - newColumnsExt = pairsWith (:) alph newColumns - newPart = pairsWith (++) rows (newColumns `union` newColumnsExt) - newPartRed = newPart \\ dom content - newContent = mq newPartRed +initialBTable :: NominalType i => MQ i Bool -> Set i -> BTable i +initialBTable = coerce initialTable + +initialBTableSize :: NominalType i => MQ i Bool -> Set i -> Int -> Int -> BTable i +initialBTableSize = coerce initialTableSize