joshua/nominal-lstar
1
Fork 0
mirror of https://github.com/Jaxan/nominal-lstar.git synced 2025-04-28 07:07:46 +02:00
Code Issues Releases Activity

Adds definition for inconsistency by Bartek

Browse source
This commit is contained in:
Joshua Moerman 2016-06-17 08:47:19 +02:00
parent cb09b2d306
commit e403d7dbd6
1 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Main.hs
View file

@ -24,8 +24,8 @@ incompleteness State{..} = filter (not . hasEqRow) ssa
-- We can determine its consistency with the following -- We can determine its consistency with the following
-- Returns equivalent rows (fst) with all inequivalent extensions (snd) -- Returns equivalent rows (fst) with all inequivalent extensions (snd)
inconsistency :: NominalType i => State i -> Set (([i], [i], i), Set [i]) inconsistencyJoshua :: NominalType i => State i -> Set (([i], [i], i), Set [i])
inconsistency State{..} = inconsistencyJoshua State{..} =
triplesWithFilter ( triplesWithFilter (
\s1 s2 a -> maybeIf (candidate s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a)) \s1 s2 a -> maybeIf (candidate s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a))
) ss ss aa ) ss ss aa
@ -36,6 +36,19 @@ inconsistency State{..} =
/\ row t s1 `eq` row t s2 /\ row t s1 `eq` row t s2
/\ rowa t s1 a `neq` rowa t s2 a /\ 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 can be written for all monads. Unfortunately (a,) is also a monad and -- This can be written for all monads. Unfortunately (a,) is also a monad and
-- this gives rise to overlapping instances, so I only do it for IO here. -- this gives rise to overlapping instances, so I only do it for IO here.
-- Note that it is not really well defined, but it kinda works. -- Note that it is not really well defined, but it kinda works.