From 9ac25c4d9b1edf8f2eb53eb8426cc9e92e4929a1 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 23 Jun 2016 16:20:33 +0200 Subject: [PATCH] Refactors code to be more modular. Now all three variations: Angluin, Bollig and homebrew NL* are using the same framework. I did not extensively test the refactor. --- src/Angluin.hs | 93 +++++++++++++++++++++++ src/Bollig.hs | 18 ++--- src/Functions.hs | 32 -------- src/Main.hs | 158 +--------------------------------------- src/NLStar.hs | 132 +++++++-------------------------- src/ObservationTable.hs | 20 ++++- 6 files changed, 148 insertions(+), 305 deletions(-) create mode 100644 src/Angluin.hs delete mode 100644 src/Functions.hs diff --git a/src/Angluin.hs b/src/Angluin.hs new file mode 100644 index 0000000..6afeaa4 --- /dev/null +++ b/src/Angluin.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE RecordWildCards #-} +module Angluin where + +import AbstractLStar +import ObservationTable +import Teacher + +import Data.List (inits, tails) +import Debug.Trace +import NLambda +import qualified Prelude hiding () +import Prelude (Bool(..), Maybe(..), id, ($), (.), (++), fst, show) + +-- We can determine its completeness with the following +-- It returns all witnesses (of the form sa) for incompleteness +closednessTest :: NominalType i => State i -> TestResult i +closednessTest State{..} = case solve (isEmpty defect) of + Just True -> Succes + Just False -> trace "Not closed" $ Failed defect empty + where + sss = map (row t) ss -- all the rows + hasEqRow = contains sss . row t -- has equivalent upper row + defect = filter (not . hasEqRow) ssa -- all rows without equivalent guy + +-- We can determine its consistency with the following +consistencyTestJ :: NominalType i => State i -> TestResult i -- Set (([i], [i], i), Set [i]) +consistencyTestJ State{..} = case solve (isEmpty defect) of + Just True -> Succes + Just False -> trace "Not consistent" $ Failed empty columns + where + -- true for equal rows, but unequal extensions + -- we can safely skip equal sequences + candidate s1 s2 a = s1 `neq` s2 + /\ row t s1 `eq` row t s2 + /\ rowa t s1 a `neq` rowa t s2 a + defect = triplesWithFilter ( + \s1 s2 a -> maybeIf (candidate s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a)) + ) ss ss aa + columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect + +-- Bartek's faster version +consistencyTestB :: NominalType i => State i -> TestResult i -- Set (([i], [i], i), Set [i]) +consistencyTestB State{..} = case solve (isEmpty defect) of + Just True -> Succes + Just False -> trace "Not consistent" $ Failed empty columns + where + rowPairs = pairsWithFilter (\s1 s2 -> maybeIf (candidate0 s1 s2) (s1,s2)) ss ss + candidate0 s1 s2 = s1 `neq` s2 /\ row t s1 `eq` row t s2 + candidate1 s1 s2 a = rowa t s1 a `neq` rowa t s2 a + defect = pairsWithFilter ( + \(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a)) + ) rowPairs aa + columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect + +-- Given a C&C table, constructs an automaton. The states are given by 2^E (not +-- necessarily equivariant functions) +constructHypothesis :: NominalType i => State i -> Automaton (BRow i) i +constructHypothesis State{..} = automaton q a d i f + where + q = map (row t) ss + a = aa + d = pairsWith (\s a -> (row t s, a, rowa t s a)) ss aa + i = singleton $ row t [] + f = mapFilter (\s -> maybeIf (toform $ apply t (s, [])) (row t s)) ss + toform s = forAll id . map fromBool $ s + +-- Extends the table with all prefixes of a set of counter examples. +useCounterExampleAngluin :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i +useCounterExampleAngluin teacher state@State{..} ces = + trace ("Using ce: " ++ show ces) $ + let ds = sum . map (fromList . inits) $ ces in + addRows teacher ds state + +-- This is the variant by Maler and Pnueli +-- I used to think it waw Rivest and Schapire, but they add less columns +useCounterExampleMP :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i +useCounterExampleMP teacher state@State{..} ces = + trace ("Using ce: " ++ show ces) $ + let de = sum . map (fromList . tails) $ ces in + addColumns teacher de state + +makeCompleteAngluin :: LearnableAlphabet i => TableCompletionHandler i +makeCompleteAngluin = makeCompleteWith [closednessTest, consistencyTestB] + +-- Default: use counter examples in columns, which is slightly faster +learnAngluin :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i +learnAngluin teacher = learn makeCompleteAngluin useCounterExampleMP constructHypothesis teacher initial + where initial = constructEmptyState teacher + +-- The "classical" version, where counter examples are added as rows +learnAngluinRows :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i +learnAngluinRows teacher = learn makeCompleteAngluin useCounterExampleAngluin constructHypothesis teacher initial + where initial = constructEmptyState teacher diff --git a/src/Bollig.hs b/src/Bollig.hs index 730656c..a4c783c 100644 --- a/src/Bollig.hs +++ b/src/Bollig.hs @@ -2,6 +2,7 @@ module Bollig where import AbstractLStar +import Angluin import ObservationTable import Teacher @@ -11,7 +12,11 @@ import NLambda import qualified Prelude hiding () import Prelude (Bool(..), Maybe(..), ($), (.), (++), fst, show) --- See also NLStar.hs for this hack +-- So at the moment we only allow sums of the form a + b and a + b + c +-- Of course we should approximate the powerset a bit better +-- But for the main examples, we know this is enough! +-- I (Joshua) believe it is possible to give a finite-orbit +-- approximation, but the code will not be efficient... hackApproximate :: NominalType a => Set a -> Set (Set a) hackApproximate set = empty `union` map singleton set @@ -51,7 +56,7 @@ rfsaClosednessTest State{..} = case solve (isEmpty defect) of rfsaConsistencyTest :: LearnableAlphabet i => State i -> TestResult i rfsaConsistencyTest State{..} = case solve (isEmpty defect) of Just True -> Succes - Just False -> trace "Not consistent" $ Failed empty defect + Just False -> trace ("Not consistent, defect = " ++ show defect) $ Failed empty defect Nothing -> trace "@@@ Unsolved Formula (rfsaConsistencyTest) @@@" $ Failed empty defect where @@ -68,16 +73,9 @@ constructHypothesisBollig State{..} = automaton q a d i f d0 = triplesWithFilter (\s a s2 -> maybeIf (row t s2 `sublang` rowa t s a) (row t s, a, row t s2)) ss aa ss d = filter (\(q1,a,q2) -> q1 `member` q /\ q2 `member` q) d0 --- Copied from the classical DFA-algorithm, column version -useCECopy :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i -useCECopy teacher state@State{..} ces = - trace ("Using ce:" ++ show ces) $ - let de = sum . map (fromList . tails) $ ces in - addColumns teacher de state - makeCompleteBollig :: LearnableAlphabet i => TableCompletionHandler i makeCompleteBollig = makeCompleteWith [rfsaClosednessTest, rfsaConsistencyTest] learnBollig :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i -learnBollig teacher = learn makeCompleteBollig useCECopy constructHypothesisBollig teacher initial +learnBollig teacher = learn makeCompleteBollig useCounterExampleMP constructHypothesisBollig teacher initial where initial = constructEmptyState teacher diff --git a/src/Functions.hs b/src/Functions.hs deleted file mode 100644 index 31779f9..0000000 --- a/src/Functions.hs +++ /dev/null @@ -1,32 +0,0 @@ -module Functions where - -import NLambda -import Prelude (($)) -import qualified Prelude () - --- We represent functions as their graphs -type Fun a b = Set (a, b) - --- Basic manipulations on functions --- Note that this returns a set, rather than an element --- because we cannot extract a value from a singleton set -apply :: (NominalType a, NominalType b) => Fun a b -> a -> Set b -apply f a1 = mapFilter (\(a2, b) -> maybeIf (eq a1 a2) b) f - --- AxB -> c is adjoint to A -> C^B --- curry and uncurry witnesses both ways of the adjunction -curry :: (NominalType a, NominalType b, NominalType c) => Fun (a, b) c -> Fun a (Fun b c) -curry f = map (\a1 -> (a1, mapFilter (\((a2,b),c) -> maybeIf (eq a1 a2) (b,c)) f)) as - where as = map (\((a, _), _) -> a) f - -uncurry :: (NominalType a, NominalType b, NominalType c) => Fun a (Fun b c) -> Fun (a, b) c -uncurry f = sum $ map (\(a,s) -> map (\(b,c) -> ((a, b), c)) s) f - --- Returns the subset (of the domain) which exhibits --- different return values for the two functions --- I am not sure about its correctness... -discrepancy :: (NominalType a, NominalType b) => Fun a b -> Fun a b -> Set a -discrepancy f1 f2 = - pairsWithFilter ( - \(a1,b1) (a2,b2) -> maybeIf (eq a1 a2 /\ neq b1 b2) a1 - ) f1 f2 diff --git a/src/Main.hs b/src/Main.hs index 388eb4a..2f3438b 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,165 +1,11 @@ -{-# LANGUAGE RecordWildCards #-} - +import Angluin import Bollig import Examples -import Functions -import ObservationTable import Teacher import NLStar -import NLambda - -import Control.DeepSeq -import Data.List (inits, tails) -import Debug.Trace -import Prelude hiding (and, curry, filter, lookup, map, not, - sum, uncurry) - - --- We can determine its completeness with the following --- It returns all witnesses (of the form sa) for incompleteness -incompleteness :: NominalType i => State i -> Set [i] -incompleteness State{..} = filter (not . hasEqRow) ssa - where - sss = map (row t) ss - -- true if the sequence sa has an equivalent row in ss - hasEqRow = contains sss . row t - --- We can determine its consistency with the following --- Returns equivalent rows (fst) with all inequivalent extensions (snd) -inconsistencyJoshua :: NominalType i => State i -> Set (([i], [i], i), Set [i]) -inconsistencyJoshua State{..} = - triplesWithFilter ( - \s1 s2 a -> maybeIf (candidate s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a)) - ) ss ss aa - where - -- true for equal rows, but unequal extensions - -- we can safely skip equal sequences - candidate s1 s2 a = s1 `neq` s2 - /\ row t s1 `eq` row t s2 - /\ rowa t s1 a `neq` rowa t s2 a - -inconsistencyBartek :: NominalType i => State i -> Set (([i], [i], i), Set [i]) -inconsistencyBartek State{..} = - pairsWithFilter ( - \(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a)) - ) rowPairs aa - where - rowPairs = pairsWithFilter (\s1 s2 -> maybeIf (candidate0 s1 s2) (s1,s2)) ss ss - candidate0 s1 s2 = s1 `neq` s2 /\ row t s1 `eq` row t s2 - candidate1 s1 s2 a = rowa t s1 a `neq` rowa t s2 a - -inconsistency :: NominalType i => State i -> Set (([i], [i], i), Set [i]) -inconsistency = inconsistencyBartek - --- This function will (recursively) make the table complete and consistent. --- This is in the IO monad purely because I want some debugging information. --- (Same holds for many other functions here) -makeCompleteConsistent :: LearnableAlphabet i => Teacher i -> State i -> State i -makeCompleteConsistent teacher state@State{..} = - -- inc is the set of rows witnessing incompleteness, that is the sequences - -- 's1 a' which do not have their equivalents of the form 's2'. - let inc = incompleteness state in - ite (isNotEmpty inc) - ( -- If that set is non-empty, we should add new rows - trace "Incomplete! Adding rows:" $ - -- These will be the new rows, ... - let ds = inc in - traceShow ds $ - let state2 = addRows teacher ds state in - makeCompleteConsistent teacher state2 - ) - ( -- inc2 is the set of inconsistencies. - let inc2 = inconsistency state in - ite (isNotEmpty inc2) - ( -- If that set is non-empty, we should add new columns - trace "Inconsistent! Adding columns:" $ - -- The extensions are in the second component - let de = sum $ map (\((s1,s2,a),es) -> map (a:) es) inc2 in - traceShow de $ - let state2 = addColumns teacher de state in - makeCompleteConsistent teacher state2 - ) - ( -- If both sets are empty, the table is complete and - -- consistent, so we are done. - trace " => Complete + Consistent :D!" $ - state - ) - ) - --- Given a C&C table, constructs an automaton. The states are given by 2^E (not --- necessarily equivariant functions) -constructHypothesis :: NominalType i => State i -> Automaton (BRow i) i -constructHypothesis State{..} = automaton q a d i f - where - q = map (row t) ss - a = aa - d = pairsWith (\s a -> (row t s, a, rowa t s a)) ss aa - i = singleton $ row t [] - f = mapFilter (\s -> maybeIf (toform $ apply t (s, [])) (row t s)) ss - toform s = forAll id . map fromBool $ s - --- Extends the table with all prefixes of a set of counter examples. -useCounterExampleAngluin :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i -useCounterExampleAngluin teacher state@State{..} ces = - trace "Using ce:" $ - traceShow ces $ - let ds = sum . map (fromList . inits) $ ces in - trace " -> Adding rows:" $ - traceShow ds $ - addRows teacher ds state - --- I am not quite sure whether this variant is due to Rivest & Schapire or Maler & Pnueli. -useCounterExampleRS :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i -useCounterExampleRS teacher state@State{..} ces = - trace "Using ce:" $ - traceShow ces $ - let de = sum . map (fromList . tails) $ ces in - trace " -> Adding columns:" $ - traceShow de $ - addColumns teacher de state - -useCounterExample :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i -useCounterExample = useCounterExampleRS - --- The main loop, which results in an automaton. Will stop if the hypothesis --- exactly accepts the language we are learning. -loop :: LearnableAlphabet i => Teacher i -> State i -> Automaton (BRow i) i -loop teacher s = - -- I put a deepseq here in order to let all traces be evaluated - -- in a decent order. Also it will be used anyways. - deepseq s $ - trace "##################" $ - trace "1. Making it complete and consistent" $ - let s2 = makeCompleteConsistent teacher s in - trace "2. Constructing hypothesis" $ - let h = constructHypothesis s2 in - traceShow h $ - trace "3. Equivalent? " $ - let eq = equivalent teacher h in - traceShow eq $ - case eq of - Nothing -> h - Just ce -> do - let s3 = useCounterExample teacher s2 ce - loop teacher s3 - -constructEmptyState :: LearnableAlphabet i => Teacher i -> State i -constructEmptyState teacher = - let aa = Teacher.alphabet teacher in - let ss = singleton [] in - let ssa = pairsWith (\s a -> s ++ [a]) ss aa in - let ee = singleton [] in - let t = fillTable teacher (ss `union` ssa) ee in - State{..} - -learn :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i -learn teacher = loop teacher s - where s = constructEmptyState teacher - --- Initializes the table and runs the algorithm. main :: IO () main = do - let h = learn (teacherWithTarget (Examples.fifoExample 3)) + let h = learnAngluin (teacherWithTarget (Examples.fifoExample 3)) putStrLn "Finished! Final hypothesis =" print h diff --git a/src/NLStar.hs b/src/NLStar.hs index 880874b..ee3b5e6 100644 --- a/src/NLStar.hs +++ b/src/NLStar.hs @@ -1,8 +1,9 @@ {-# LANGUAGE RecordWildCards #-} module NLStar where -import Examples -import Functions +import AbstractLStar +import Angluin +import Bollig import ObservationTable import Teacher @@ -13,21 +14,10 @@ import Data.List (inits, tails) import Prelude hiding (and, curry, filter, lookup, map, not, sum) --- So at the moment we only allow sums of the form a + b --- Of course we should approximate the powerset a bit better --- But for the main example, we know this is enough! --- I (Joshua) believe it is possible to give a finite-orbit --- approximation, but the code will not be efficient ;-). -hackApproximate :: NominalType a => Set a -> Set (Set a) -hackApproximate set = empty `union` map singleton set `union` pairsWith (\x y -> singleton x `union` singleton y) set set - -rowUnion :: NominalType i => Set (BRow i) -> BRow i -rowUnion set = Prelude.uncurry union . setTrueFalse . partition (\(_, f) -> f) $ map (\is -> (is, exists fromBool (mapFilter (\(is2, b) -> maybeIf (is `eq` is2) b) flatSet))) allIs - where - flatSet = sum set - allIs = map fst flatSet - setTrueFalse (trueSet, falseSet) = (map (setSecond True) trueSet, map (setSecond False) falseSet) - setSecond a (x, _) = (x, a) +{- This is not NL* from the Bollig et al paper. This is a more abstract version + wich uses different notions for closedness and consistency. + Joshua argues this version is closer to the categorical perspective. +-} -- lifted row functions rowP t = rowUnion . map (row t) @@ -35,64 +25,28 @@ rowPa t set a = rowUnion . map (\s -> rowa t s a) $ set -- We can determine its completeness with the following -- It returns all witnesses (of the form sa) for incompleteness -incompletenessNonDet :: NominalType i => State i -> Set [i] -incompletenessNonDet State{..} = filter (not . hasEqRow) ssa +nonDetClosednessTest :: NominalType i => State i -> TestResult i +nonDetClosednessTest State{..} = case solve (isEmpty defect) of + Just True -> Succes + Just False -> trace "Not closed" $ Failed defect empty where sss = map (rowP t) . hackApproximate $ ss -- true if the sequence sa has an equivalent row in ss hasEqRow = contains sss . row t + defect = filter (not . hasEqRow) ssa -inconsistencyNonDet :: NominalType i => State i -> Set ((Set [i], Set [i], i), Set [i]) -inconsistencyNonDet State{..} = - pairsWithFilter ( - \(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowPa t s1 a) (rowPa t s2 a)) - ) rowPairs aa +nonDetConsistencyTest :: NominalType i => State i -> TestResult i -- Set ((Set [i], Set [i], i), Set [i]) +nonDetConsistencyTest State{..} = case solve (isEmpty defect) of + Just True -> Succes + Just False -> trace "Not consistent" $ Failed empty columns where rowPairs = pairsWithFilter (\s1 s2 -> maybeIf (candidate0 s1 s2) (s1,s2)) (hackApproximate ss) (hackApproximate ss) candidate0 s1 s2 = s1 `neq` s2 /\ rowP t s1 `eq` rowP t s2 candidate1 s1 s2 a = rowPa t s1 a `neq` rowPa t s2 a - --- This function will (recursively) make the table complete and consistent. --- This is in the IO monad purely because I want some debugging information. --- (Same holds for many other functions here) -makeCompleteConsistentNonDet :: LearnableAlphabet i => Teacher i -> State i -> State i -makeCompleteConsistentNonDet teacher state@State{..} = - -- inc is the set of rows witnessing incompleteness, that is the sequences - -- 's1 a' which do not have their equivalents of the form 's2'. - let inc = incompletenessNonDet state in - ite (isNotEmpty inc) - ( -- If that set is non-empty, we should add new rows - trace "Incomplete! Adding rows:" $ - -- These will be the new rows, ... - let ds = inc in - traceShow ds $ - let state2 = addRows teacher ds state in - makeCompleteConsistentNonDet teacher state2 - ) - ( -- inc2 is the set of inconsistencies. - let inc2 = inconsistencyNonDet state in - ite (isNotEmpty inc2) - ( -- If that set is non-empty, we should add new columns - trace "Inconsistent! Adding columns:" $ - -- The extensions are in the second component - let de = sum $ map (\((s1,s2,a),es) -> map (a:) es) inc2 in - traceShow de $ - let state2 = addColumns teacher de state in - makeCompleteConsistentNonDet teacher state2 - ) - ( -- If both sets are empty, the table is complete and - -- consistent, so we are done. - trace " => Complete + Consistent :D!" $ - state - ) - ) - -boolImplies :: Bool -> Bool -> Bool -boolImplies True False = False -boolImplies _ _ = True - -sublang :: NominalType i => BRow i -> BRow i -> Formula -sublang r1 r2 = forAll fromBool $ pairsWithFilter (\(i1, f1) (i2, f2) -> maybeIf (i1 `eq` i2) (f1 `boolImplies` f2)) r1 r2 + defect = pairsWithFilter ( + \(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowPa t s1 a) (rowPa t s2 a)) + ) rowPairs aa + columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect -- Given a C&C table, constructs an automaton. The states are given by 2^E (not -- necessarily equivariant functions) @@ -101,49 +55,15 @@ constructHypothesisNonDet State{..} = automaton q a d i f where q = map (row t) ss a = aa - d = triplesWithFilter (\s a s2 -> maybeIf (sublang (row t s2) (rowa t s a)) (row t s, a, row t s2)) ss aa ss + d = triplesWithFilter (\s a s2 -> maybeIf (row t s2 `sublang` rowa t s a) (row t s, a, row t s2)) ss aa ss i = singleton $ row t [] f = mapFilter (\s -> maybeIf (toform $ apply t (s, [])) (row t s)) ss toform s = forAll id . map fromBool $ s --- I am not quite sure whether this variant is due to Rivest & Schapire or Maler & Pnueli. -useCounterExampleNonDet :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i -useCounterExampleNonDet teacher state@State{..} ces = - trace "Using ce:" $ - traceShow ces $ - let de = sum . map (fromList . tails) $ ces in - trace " -> Adding columns:" $ - traceShow de $ - addColumns teacher de state - --- The main loop, which results in an automaton. Will stop if the hypothesis --- exactly accepts the language we are learning. -loopNonDet :: LearnableAlphabet i => Teacher i -> State i -> Automaton (BRow i) i -loopNonDet teacher s = - trace "##################" $ - trace "1. Making it complete and consistent" $ - let s2 = makeCompleteConsistentNonDet teacher s in - trace "2. Constructing hypothesis" $ - let h = constructHypothesisNonDet s2 in - traceShow h $ - trace "3. Equivalent? " $ - let eq = equivalent teacher h in - traceShow eq $ - case eq of - Nothing -> h - Just ce -> do - let s3 = useCounterExampleNonDet teacher s2 ce - loopNonDet teacher s3 - -constructEmptyStateNonDet :: LearnableAlphabet i => Teacher i -> State i -constructEmptyStateNonDet teacher = - let aa = Teacher.alphabet teacher in - let ss = singleton [] in - let ssa = pairsWith (\s a -> s ++ [a]) ss aa in - let ee = singleton [] in - let t = fillTable teacher (ss `union` ssa) ee in - State{..} +makeCompleteNonDet :: LearnableAlphabet i => TableCompletionHandler i +makeCompleteNonDet = makeCompleteWith [nonDetClosednessTest, nonDetConsistencyTest] +-- Default: use counter examples in columns, which is slightly faster learnNonDet :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i -learnNonDet teacher = loopNonDet teacher s - where s = constructEmptyStateNonDet teacher +learnNonDet teacher = learn makeCompleteNonDet useCounterExampleMP constructHypothesisNonDet teacher initial + where initial = constructEmptyState teacher diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs index c01cc1f..4e5844b 100644 --- a/src/ObservationTable.hs +++ b/src/ObservationTable.hs @@ -7,7 +7,6 @@ module ObservationTable where -import Functions import NLambda hiding (fromJust) import Teacher @@ -19,6 +18,25 @@ import Prelude (Bool (..), Eq, Ord, Show (..), ($), (++), (.), un import qualified Prelude () +-- We represent functions as their graphs +type Fun a b = Set (a, b) + +-- Basic manipulations on functions +-- Note that this returns a set, rather than an element +-- because we cannot extract a value from a singleton set +apply :: (NominalType a, NominalType b) => Fun a b -> a -> Set b +apply f a1 = mapFilter (\(a2, b) -> maybeIf (eq a1 a2) b) f + +-- Returns the subset (of the domain) which exhibits +-- different return values for the two functions +-- I am not sure about its correctness... +discrepancy :: (NominalType a, NominalType b) => Fun a b -> Fun a b -> Set a +discrepancy f1 f2 = + pairsWithFilter ( + \(a1,b1) (a2,b2) -> maybeIf (eq a1 a2 /\ neq b1 b2) a1 + ) f1 f2 + + -- An observation table is a function S x E -> O -- (Also includes SA x E -> O) type Table i o = Fun ([i], [i]) o